Simplify some proofs in Coq and IV validation for expression to new semantics in HOL4

coq/Commands.v

@@ -43,4 +43,14 @@ Fixpoint definedVars V (f:cmd V) :NatSet.t :=
   match f with
   | Let x _ g => NatSet.add x (definedVars g)
   | Ret _ => NatSet.empty
+  end.
+
+(**
+  The live variables of a command are all variables which occur on the right
+  hand side of an assignment or at a return statement
+ **)
+Fixpoint liveVars V (f:cmd V) :NatSet.t :=
+  match f with
+  | Let _ e g => NatSet.union (usedVars e) (liveVars g)
+  | Ret e => usedVars e
   end.
\ No newline at end of file

coq/ErrorBounds.v

@@ -60,21 +60,21 @@ Proof.
   rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in plus_real.
+  rewrite (meps_0_deterministic H3 e1_real) in plus_real.
   rewrite (meps_0_deterministic H5 e2_real) in plus_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion plus_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   unfold updEnv; simpl.
   unfold updEnv in H0,H1; simpl in *.
   symmetry in H0, H1.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear plus_float H4 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
+  clear plus_float H3 H5 plus_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -123,21 +123,21 @@ Proof.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in sub_real.
+  rewrite (meps_0_deterministic H3 e1_real) in sub_real.
   rewrite (meps_0_deterministic H5 e2_real) in sub_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion sub_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   unfold updEnv; simpl.
   symmetry in H0, H1.
   unfold updEnv in H0, H1; simpl in H0, H1.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear sub_float H4 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
+  clear sub_float H3 H5 sub_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
@@ -177,20 +177,20 @@ Proof.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in mult_real.
+  rewrite (meps_0_deterministic H3 e1_real) in mult_real.
   rewrite (meps_0_deterministic H5 e2_real) in mult_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion mult_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   symmetry in H0, H1;
     unfold updEnv in *; simpl in *.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear mult_float H4 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
+  clear mult_float H3 H5 mult_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -224,20 +224,20 @@ Proof.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
   clear delta H2.
-  rewrite (meps_0_deterministic H4 e1_real);
+  rewrite (meps_0_deterministic H3 e1_real);
     rewrite (meps_0_deterministic H5 e2_real).
-  rewrite (meps_0_deterministic H4 e1_real) in div_real.
+  rewrite (meps_0_deterministic H3 e1_real) in div_real.
   rewrite (meps_0_deterministic H5 e2_real) in div_real.
-  clear H4 H5 v1 v2.
+  clear H3 H5 H6 v1 v2.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion div_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H5; subst.
+  inversion H3; subst; inversion H5; subst.
   symmetry in H0, H1;
     unfold updEnv in *; simpl in *.
   inversion H0; inversion H1; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear div_float H4 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
+  clear div_float H3 H5 div_real e1_real e1_float e2_real e2_float H0 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.

coq/Expressions.v

+
 (**
   Formalization of the base expression language for the daisy framework
  **)
@@ -120,6 +121,7 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
     Rle (Rabs delta) eps ->
     eval_exp eps E f1 v1 ->
     eval_exp eps E f2 v2 ->
+    ((op = Div) -> (~ v2 = 0)%R) ->
     eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
 
 (**

coq/IntervalValidation.v

@@ -137,32 +137,6 @@ Qed.
 Ltac env_assert absenv e name :=
   assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
 
-Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err:
-  absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
-  validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
-  (ivhi_e2 < 0) \/ (0 < ivlo_e2).
-Proof.
-  intros absenv_eq validBounds.
-  unfold validIntervalbounds in validBounds.
-  env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]].
-  env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]].
-  rewrite abs_div, abs_e1, absenv_eq in validBounds.
-  repeat (rewrite <- andb_lazy_alt in validBounds).
-  apply Is_true_eq_left in validBounds.
-  apply andb_prop_elim in validBounds.
-  destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds.
-  destruct validBounds as [nodiv0 _].
-  apply Is_true_eq_true in nodiv0.
-  unfold isSupersetIntv in *; simpl in *.
-  apply le_neq_bool_to_lt_prop; auto.
-Qed.
-
-Fixpoint getRetExp (V:Type) (f:cmd V) :=
-  match f with
-  |Let x e g => getRetExp g
-  | Ret e => e
-  end.
-
 Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars E:
   forall vR,
     validIntervalbounds f absenv P dVars = true ->
@@ -490,6 +464,12 @@ Proof.
                     rewrite <- Q2R_max4 in valid_div_hi; auto. } }
 Qed.
 
+Fixpoint getRetExp (V:Type) (f:cmd V) :=
+  match f with
+  |Let x e g => getRetExp g
+  | Ret e => e
+  end.
+
 Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
   forall E vR fVars dVars outVars elo ehi err P,
     ssa f (NatSet.union fVars dVars) outVars ->
@@ -502,7 +482,7 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
           exists vR,
             E v = Some vR /\
             (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
+    NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
     validIntervalboundsCmd f absenv P dVars = true ->
     absenv (getRetExp f) = ((elo, ehi), err) ->
     (Q2R elo <=  vR <= Q2R ehi)%R.

coq/ssaPrgs.v

@@ -37,6 +37,7 @@ Proof.
       rewrite NatSet.union_spec; auto.
 Qed.
 
+(*
 Lemma validVars_non_stuck (e:exp Q) inVars E:
  NatSet.Subset (usedVars e) inVars ->
   (forall v, NatSet.In v (usedVars e) ->
@@ -80,7 +81,7 @@ Proof.
           destruct eval_e2_def as [vR2 eval_e2_def].
         exists (perturb (evalBinop b vR1 vR2) 0); constructor; auto.
         rewrite Rabs_R0; lra.
-Qed.
+Qed. *)
 
 Inductive ssa (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
  ssaLet x e s inVars Vterm:
@@ -95,7 +96,7 @@ Inductive ssa (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
 
 Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
   ssa f inVars outVars ->
-  NatSet.Subset (Commands.freeVars f) inVars.
+  NatSet.Subset (freeVars f) inVars.
 Proof.
   intros ssa_f; induction ssa_f.
   - simpl in *. hnf; intros a in_fVars.
@@ -399,6 +400,129 @@ Fixpoint let_subst (f:cmd Q) :=
   | Ret e1 =>  Some e1
   end.
 
+Lemma eval_subst_subexp E e' n e vR:
+  NatSet.In n (usedVars e) ->
+  eval_exp 0 E (toRExp (exp_subst e n e')) vR ->
+  exists v, eval_exp 0 E (toRExp e') v.
+Proof.
+  revert E e' n vR.
+  induction e;
+  intros E e' n' vR n_fVar eval_subst; simpl in *; try eauto.
+  - case_eq (n =? n'); intros case_n; rewrite case_n in *; eauto.
+    rewrite NatSet.singleton_spec in n_fVar.
+    exfalso.
+    rewrite Nat.eqb_neq in case_n.
+    apply case_n; auto.
+  - inversion n_fVar.
+  - inversion eval_subst; subst;
+      eapply IHe; eauto.
+  - inversion eval_subst; subst.
+    rewrite NatSet.union_spec in n_fVar.
+    destruct n_fVar as [n_fVar_e1 | n_fVare2];
+      [eapply IHe1; eauto | eapply IHe2; eauto].
+Qed.
+
+Lemma bstep_subst_subexp_any E e x f vR:
+  NatSet.In x (liveVars f) ->
+  bstep (toRCmd (map_subst f x e)) E 0 vR ->
+  exists E' v, eval_exp 0 E' (toRExp e) v.
+Proof.
+  revert E e x vR;
+    induction f;
+    intros E e' x vR x_live eval_f.
+  - inversion eval_f; subst.
+    simpl in x_live.
+    rewrite NatSet.union_spec in x_live.
+    destruct x_live as [x_used | x_live].
+    + exists E. eapply eval_subst_subexp; eauto.
+    + eapply IHf; eauto.
+  - simpl in *.
+    inversion eval_f; subst.
+    exists E. eapply eval_subst_subexp; eauto.
+Qed.
+
+Lemma bstep_subst_subexp_ret E e x e' vR:
+  NatSet.In x (liveVars (Ret e')) ->
+  bstep (toRCmd (map_subst (Ret e') x e)) E 0 vR ->
+  exists v, eval_exp 0 E (toRExp e) v.
+Proof.
+  simpl; intros x_live bstep_ret.
+  inversion bstep_ret; subst.
+  eapply eval_subst_subexp; eauto.
+Qed.
+Lemma no_forward_refs V (f:cmd V) inVars outVars:
+  ssa f inVars outVars ->
+  forall v, NatSet.In v (definedVars f) ->
+       NatSet.mem v inVars = false.
+Proof.
+  intros ssa_f; induction ssa_f; simpl.
+  - intros v v_defVar.
+    rewrite NatSet.add_spec in v_defVar.
+    destruct v_defVar as [v_x | v_defVar].
+    + subst; auto.
+    + specialize (IHssa_f v v_defVar).
+      case_eq (NatSet.mem v inVars); intros mem_inVars; try auto.
+      assert (NatSet.mem v (NatSet.add x inVars) = true) by (rewrite NatSet.mem_spec, NatSet.add_spec, <- NatSet.mem_spec; auto).
+      congruence.
+  - intros v v_in_empty; inversion v_in_empty.
+Qed.
+
+Lemma bstep_subst_subexp_let E e x y e' g vR:
+  NatSet.In x (liveVars (Let y e' g)) ->
+  (forall x, NatSet.In x (usedVars e) ->
+        exists v, E x = v) ->
+  bstep (toRCmd (map_subst (Let y e' g) x e)) E 0 vR ->
+  exists v, eval_exp 0 E (toRExp e) v.
+Proof.
+  revert E e x y e' vR;
+    induction g;
+    intros E e0 x y e' vR x_live uedVars_def bstep_f.
+  - simpl in *.
+    inversion bstep_f; subst.
+    specialize (IHg (updEnv y v E) e0 x n e).
+    rewrite NatSet.union_spec in x_live.
+    destruct x_live as [x_used | x_live].
+    + eapply eval_subst_subexp; eauto.
+    + edestruct IHg as [v0 eval_v0]; eauto.
+
+      dummy_bind_ok
+
+Theorem let_free_agree f E vR inVars outVars e:
+  ssa f inVars outVars ->
+  (forall v, NatSet.In v (definedVars f) ->
+        NatSet.In v (liveVars f)) ->
+  let_subst f = Some e ->
+  bstep (toRCmd (Ret e)) E 0 vR ->
+  bstep (toRCmd f) E 0 vR.
+Proof.
+  intros ssa_f.
+  revert E vR e;
+    induction ssa_f;
+    intros E vR e_subst dVars_live subst_step bstep_e;
+    simpl in *.
+  (* Let Case, prove that the value of the let binding must be used somewhere *)
+  - case_eq (let_subst s).
+    + intros e0 subst_s; rewrite subst_s in *.
+      inversion subst_step; subst.
+      clear subst_s subst_step.
+      inversion bstep_e; subst.
+      specialize (dVars_live x).
+      rewrite NatSet.add_spec in dVars_live.
+      assert (NatSet.In x (NatSet.union (usedVars e) (liveVars s)))
+        as x_used_or_live
+          by (apply dVars_live; auto).
+      rewrite NatSet.union_spec in x_used_or_live.
+      destruct x_used_or_live as [x_used | x_live].
+      * specialize (H x x_used).
+        rewrite <- NatSet.mem_spec in H; congruence.
+      *
+
+    eapply let_b.
+    Focus 2.
+    eapply IHssa_f; try auto.
+
+
+
 Theorem let_free_form f E vR inVars outVars e:
   ssa f inVars outVars ->
   bstep (toRCmd f) E 0 vR ->

hol4/CommandsScript.sml

@@ -21,23 +21,27 @@ val _ = Datatype `
   result value
  **)
 val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
-  (!x e s s' E v eps vR.
+  (!x e s E v eps vR.
       eval_exp eps E e v /\
-      bstep s (updEnv x v E) eps s' vR ==>
-      bstep (Let x e s) E eps s' vR) /\
+      bstep s (updEnv x v E) eps vR ==>
+      bstep (Let x e s) E eps vR) /\
   (!e E v eps.
       eval_exp eps E e v ==>
-      bstep (Ret e) E eps Nop v)`;
+      bstep (Ret e) E eps v)`;
 
 (**
   Generate a better case lemma again
 **)
 val bstep_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
-    [``bstep (Let x e s) E eps s' VarEnv2``,
-     ``bstep (Ret e) E eps Nop VarEnv2``]
+    [``bstep (Let x e s) E eps vR``,
+     ``bstep (Ret e) E eps vR``]
   |> LIST_CONJ |> curry save_thm "bstep_cases";
 
+val [let_b, ret_b] = CONJ_LIST 2 bstep_rules;
+save_thm ("let_b", let_b);
+save_thm ("ret_b", ret_b);
+
 (**
   The free variables of a command are all used variables of expressions
   without the let bound variables

hol4/ExpressionsScript.sml

@@ -94,6 +94,13 @@ val eval_exp_cases =
      ``eval_exp eps E (Binop n e1 e2) res``]
   |> LIST_CONJ |> curry save_thm "eval_exp_cases";
 
+val [Var_load, Const_dist, Unop_neg, Unop_inv, Binop_dist] = CONJ_LIST 5 eval_exp_rules;
+save_thm ("Var_load", Var_load);
+save_thm ("Const_dist", Const_dist);
+save_thm ("Unop_neg", Unop_neg);
+save_thm ("Unop_inv", Unop_inv);
+save_thm ("Binop_dist", Binop_dist);
+
 (**
   Define the set of "used" variables of an expression to be the set of variables
   occuring in it

hol4/Infra/DaisyTactics.sml

@@ -52,4 +52,26 @@ fun qexistsl_tac termlist =
 	 [] => ALL_TAC
      | t::tel => qexists_tac t \\ qexistsl_tac tel;
 
+fun specialize pat_hyp pat_thm =
+  qpat_x_assum pat_hyp
+    (fn hyp =>
+      (qspec_then pat_thm ASSUME_TAC hyp) ORELSE
+      (qpat_assum pat_thm
+         (fn asm => ASSUME_TAC (MP hyp asm))));
+
+fun rw_asm pat_asm =
+  qpat_x_assum pat_asm
+    (fn asm =>
+      (once_rewrite_tac [asm]));
+
+fun rw_sym_asm pat_asm =
+  qpat_x_assum pat_asm
+    (fn asm =>
+      (once_rewrite_tac [GSYM asm]));
+
+fun rw_thm_asm pat_asm thm =
+  qpat_x_assum pat_asm
+    (fn asm =>
+      (ASSUME_TAC (ONCE_REWRITE_RULE[thm] asm)));
+
 end

hol4/ssaPrgsScript.sml

@@ -63,11 +63,11 @@ val (ssa_rules, ssa_ind, ssa_cases) = Hol_reln `
   (!x e s inVars Vterm.
      (domain (usedVars e)) SUBSET (domain inVars) /\
      (~ (x IN (domain inVars)))  /\
-     ssa s (Insert x inVars) Vterm ==>
+     (ssa:'a cmd -> num_set -> num_set -> bool) s (Insert x inVars) Vterm ==>
      ssa (Let x e s) inVars Vterm) /\
   (!e inVars Vterm.
-     (domain (usedVars e))SUBSET  (domain inVars) /\
-     (inVars = Vterm) ==>
+     (domain (usedVars e)) SUBSET (domain inVars) /\
+     (domain inVars = domain Vterm) ==>
      ssa (Ret e) inVars Vterm)`;
 
 (*
@@ -77,17 +77,317 @@ val ssa_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once ssa_cases])
     [``ssa (Let x e s) inVars Vterm``,
      ``ssa (Ret e) inVars Vterm``]
-  |> LIST_CONJ |> curry save_thm "ssaPrg_cases";
+  |> LIST_CONJ |> curry save_thm "ssa_cases";
+
+val [ssaLet, ssaRet] = CONJ_LIST 2 ssa_rules;
+save_thm ("ssaLet",ssaLet);
+save_thm ("ssaRet",ssaRet);
 
 val ssa_subset_freeVars = store_thm ("ssa_subset_freeVars",
-  ``!(f:'a cmd) inVars outVars inVars'.
-      (domain inVars' = domain inVars) /\
+  ``!(f:'a cmd) inVars outVars.
       ssa f inVars outVars ==>
-      ssa f inVars' outVars``,
-  once_rewrite_tac[CONJ_SYM]
-  \\ once_rewrite_tac [GSYM AND_IMP_INTRO]
-  (* THIS DOES NOT WORK *)
-  \\ recInduct ssa_ind
-  metis_tac[]);
+      (domain (freeVars f)) SUBSET (domain inVars)``,
+  ho_match_mp_tac ssa_ind \\ rw []
+  >- (once_rewrite_tac [freeVars_def, domain_insert] \\ simp []
+      \\ once_rewrite_tac [domain_union]
+      \\ fs[SUBSET_DEF]
+      \\ rpt strip_tac
+      >- (first_x_assum match_mp_tac
+          \\ simp [])
+      >- (fs [Insert_def, domain_insert]
+          \\ metis_tac[]))
+  >- (once_rewrite_tac[freeVars_def]
+      \\ fs []));
+
+val ssa_equal_set_ind = prove(
+  ``!(f:'a cmd) inVars outVars.
+       ssa f inVars outVars ==>
+        (!inVars'.
+           (domain inVars' = domain inVars) ==>
+           ssa f inVars' outVars)``,
+  qspec_then `\f inVars outVars.
+    ∀inVars'. (domain inVars' = domain inVars) ==> ssa f inVars' outVars` (fn thm => ASSUME_TAC (SIMP_RULE std_ss [] thm)) ssa_ind
+  \\ first_x_assum match_mp_tac
+  \\ conj_tac \\ rw[]
+  >- (match_mp_tac ssaLet \\ fs[]
+      \\ first_x_assum match_mp_tac
+      \\ simp[Insert_def, domain_insert])
+  >- (match_mp_tac ssaRet \\ fs[]));
+
+val ssa_equal_set = store_thm ("ssa_equal_set",
+  ``!(f:'a cmd) inVars outVars inVars'.
+       (domain inVars' = domain inVars) /\
+       ssa f inVars outVars ==>
+       ssa f inVars' outVars``,
+  rpt strip_tac
+  \\ qspecl_then [`f`, `inVars`, `outVars`] ASSUME_TAC ssa_equal_set_ind
+  \\ specialize `ssa _ _ _ ==> _` `ssa f inVars outVars`
+  \\ specialize `!inVars'. A ==> B` `inVars'`
+  \\ first_x_assum match_mp_tac \\ fs[]);
+
+val validSSA_def = Define `
+  validSSA (f:real cmd) (inVars:num_set) =
+    case f of
+      |Let x e g =>
+        ((lookup x inVars = NONE) /\
+         (subspt (usedVars e) inVars) /\
+         (validSSA g (Insert x inVars)))
+      |Ret e =>
+       (subspt (usedVars e) inVars)`;
+
+val validSSA_sound = store_thm ("validSSA_sound",
+  ``!(f:real cmd) (inVars:num_set).
+       (validSSA f inVars) ==>
+       ?outVars.
+         ssa f inVars outVars``,
+  Induct \\ once_rewrite_tac [validSSA_def] \\ rw[]
+  >- (specialize `!inVars. _ ==> _` `Insert n inVars`
+      \\ `?outVars. ssa f (Insert n inVars) outVars` by (first_x_assum match_mp_tac \\ simp[])
+      \\ qexists_tac `outVars`
+      \\ match_mp_tac ssaLet
+      \\ fs [subspt_def, SUBSET_DEF, lookup_NONE_domain])
+  >- (qexists_tac `inVars`
+      \\ match_mp_tac ssaRet
+      \\ fs[subspt_def, SUBSET_DEF]));
+
+val ssa_shadowing_free = store_thm ("ssa_shadowing_free",
+  ``!x y v v' e f inVars outVars E.
+      ssa (Let x e f) inVars outVars /\
+      (y IN (domain inVars)) /\
+      eval_exp 0 E e v ==>
+      !E n. updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n``,
+  rpt strip_tac
+  \\ inversion `ssa (Let x e f) _ _` ssa_cases
+  \\ fs[updEnv_def]
+  \\ Cases_on `n = x` \\ rveq
+  >- (simp[]
+      \\ Cases_on `n = y` \\ rveq \\ rw[]
+      \\ metis_tac[])
+  >- (simp[]));
+
+val shadowing_free_rewriting_exp = store_thm ("shadowing_free_rewriting_exp",
+  ``!e v E1 E2.
+      (!n. E1 n = E2 n) ==>
+      (eval_exp 0 E1 e v <=>
+      eval_exp 0 E2 e v)``,
+  Induct \\ rpt strip_tac \\ fs[eval_exp_cases, EQ_IMP_THM] \\ metis_tac[]);
+
+val shadowing_free_rewriting_cmd = store_thm ("shadowing_free_rewriting_cmd",
+  ``!f E1 E2 vR.
+      (!n. E1 n = E2 n) ==>
+      (bstep f E1 0 vR <=>
+       bstep f E2 0 vR)``,
+  Induct \\ rpt strip_tac \\ fs[EQ_IMP_THM] \\ metis_tac[]);
+
+val dummy_bind_ok = store_thm ("dummy_bind_ok",
+  ``!e v x v' (inVars:num_set) E.
+      (domain (usedVars e)) SUBSET (domain inVars) /\
+      (~ (x IN (domain inVars))) /\
+      eval_exp 0 E e v ==>
+      eval_exp 0 (updEnv x v' E) e v``,
+  Induct \\ rpt strip_tac \\ inversion `eval_exp _ _ _ _` eval_exp_cases \\ rveq
+  >- (match_mp_tac Var_load
+      \\ fs[usedVars_def, updEnv_def]
+      \\ Cases_on `n = x` \\ rveq \\ fs[] )
+  >- (match_mp_tac Const_dist \\ simp[])
+  >- (Cases_on `u` \\ rveq \\ fs[updEnv_def]
+      >- (match_mp_tac Unop_neg
+          \\ first_x_assum match_mp_tac
+          \\ qexists_tac `inVars`
+          \\ qpat_x_assum `domain _ SUBSET _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [usedVars_def] thm))
+          \\ fs[])
+      >- (match_mp_tac Unop_inv \\ fs[]
+          \\ first_x_assum match_mp_tac
+          \\ qexists_tac `inVars`
+          \\ qpat_x_assum `domain _ SUBSET _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [usedVars_def] thm))
+          \\ fs[]))
+  >- (match_mp_tac Binop_dist \\ fs[]
+      \\ qpat_x_assum `domain _ SUBSET _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [usedVars_def] thm))
+      \\ conj_tac \\ first_x_assum match_mp_tac \\ qexists_tac `inVars` \\ fs[domain_union]));
+
+val exp_subst_def = Define `
+  exp_subst (e:real exp) x e_new =
+    case e of
+      |Var v => if v = x then e_new else Var v
+      |Unop u e => Unop u (exp_subst e x e_new)
+      |Binop b e1 e2 => Binop b (exp_subst e1 x e_new) (exp_subst e2 x e_new)
+      |e => e`;
+
+val exp_subst_correct = store_thm ("exp_subst_correct",
+  ``!e e_sub E x v v_res.
+      eval_exp 0 E e_sub v ==>
+      (eval_exp 0 (updEnv x v E) e v_res <=>
+       eval_exp 0 E (exp_subst e x e_sub) v_res)``,
+  Induct \\ rpt strip_tac \\ once_rewrite_tac [EQ_IMP_THM]
+  >- (conj_tac \\ strip_tac \\ inversion `eval_exp _ _ _ _` eval_exp_cases
+      \\ fs [exp_subst_def, updEnv_def] \\ Cases_on `n = x` \\ rveq \\ fs[]
+      >- (match_mp_tac Var_load \\ fs [])
+      >- (match_mp_tac Var_load \\ fs [updEnv_def]