Commit 56ddcb3a authored by ='s avatar =

IntervalValidation and ssaPrg are now ported

parent 86eec2be
......@@ -97,8 +97,8 @@ Proof.
apply andb_prop_elim in approx_true.
destruct approx_true; auto.
- intros approx_true v0 v_in_fV; simpl in *.
inversion v_in_fV.
- intros approx_unary_true v v_in_fV; simpl in *.
inversion v_in_fV.
- intros approx_unary_true v v_in_fV; simpl in *.
apply Is_true_eq_left in approx_unary_true.
simpl in *.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
......@@ -170,7 +170,7 @@ Proof.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) defVars:
forall vR,
validIntervalbounds f absenv P dVars = true ->
......@@ -351,7 +351,7 @@ Proof.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
destruct m1; destruct m2; cbv in H2; inversion H2.
specialize (IHf1 v1 valid_e1 valid_definedVars).
specialize (IHf1 v1 valid_e1 valid_definedVars).
specialize (IHf2 v2 valid_e2 valid_definedVars).
rewrite absenv_f1 in IHf1.
rewrite absenv_f2 in IHf2.
......
......@@ -173,6 +173,11 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ fs [])
>- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ res_tac));
val toREvalVars_def = Define `
toREvalVars (d:num -> mType option) (n:num) : mType option =
case d n of
| SOME m => SOME M0
| NONE => NONE`;
(**
Helping lemma. Needed in soundness proof.
......
......@@ -8,7 +8,7 @@
open preamble
open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
open ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory MachineTypeTheory
open sptreeLib sptreeTheory
val _ = new_theory "IntervalValidation";
......@@ -23,7 +23,7 @@ val validIntervalbounds_def = Define `
if (lookup v validVars = SOME ())
then T
else (isSupersetInterval (P v) intv /\ IVlo (P v) <= IVhi (P v))
| Const n => isSupersetInterval (n,n) intv
| Const m n => isSupersetInterval (n,n) intv
| Unop op f =>
(if validIntervalbounds f absenv P validVars
then
......@@ -61,12 +61,17 @@ val validIntervalbounds_def = Define `
let new_iv = divideInterval iv1 iv2 in
isSupersetInterval new_iv intv
else F
else F)`;
else F)
| Downcast m f1 =>
let (iv1, _) = absenv f1 in
if (validIntervalbounds f1 absenv P validVars) then
((isSupersetInterval intv iv1) /\ (isSupersetInterval iv1 intv))
else F`;
val validIntervalboundsCmd_def = Define `
validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num_set) =
case f of
| Let x e g =>
| Let m x e g =>
if (validIntervalbounds e absenv P validVars /\
(FST (absenv e) = FST (absenv (Var x))))
then validIntervalboundsCmd g absenv P (insert x () validVars)
......@@ -102,7 +107,14 @@ val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecon
\\ `validIntervalbounds f' absenv P V`
by (qpat_x_assum `validIntervalbounds (Binop b f f') _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm))
\\ Cases_on `absenv (Binop b f f')` \\ fs[])
\\ fs[domain_union]));
\\ fs[domain_union])
>- (rpt (first_x_assum (fn thm => qspecl_then [`absenv`, `P`, `V`] ASSUME_TAC thm))
\\ `validIntervalbounds f absenv P V`
by (qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm))
\\ Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f` \\ fs[])
\\ specialize `validIntervalbounds f _ _ _ ==> _` `validIntervalbounds f _ _ _`
\\ first_x_assum match_mp_tac
\\ simp[]));
val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
``!(f:real exp) (absenv:analysisResult) (P:precond) (fVars:num_set) dVars E vR.
......@@ -114,9 +126,9 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
(!v. v IN (domain fVars) ==>
(?vR. (E v = SOME vR) /\
(FST (P v) <= vR /\ vR <= SND (P v)))) /\
eval_exp 0 E f vR ==>
eval_exp E (toREvalVars defVars) (toREval f) vR M0 ==>
(FST (FST (absenv f))) <= vR /\ vR <= (SND (FST (absenv f)))``,
Induct \\ once_rewrite_tac [eval_exp_cases] \\ rpt gen_tac \\ strip_tac
Induct \\ once_rewrite_tac [toREval_def,eval_exp_cases] \\ rpt gen_tac \\ strip_tac
(* Variable case *)
>- (rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ Cases_on `absenv (Var n)` \\ Cases_on `lookup n dVars` \\ fs[]
......@@ -125,6 +137,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ `~ (n IN (domain dVars))` by (fs[domain_lookup])
\\ `n IN domain fVars` by fs[]
\\ fs [isSupersetInterval_def, IVlo_def, IVhi_def]
\\ fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ fs [] \\ rveq
\\ conj_tac
>- (match_mp_tac REAL_LE_TRANS \\ asm_exists_tac
\\ fs [] \\ rveq \\ simp[])
......@@ -132,77 +145,84 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
>- (specialize `!v. v IN domain dVars ==> _` `n`
\\ `n IN domain dVars` by (fs [domain_lookup])
\\ qpat_x_assum `absenv (Var n) = _` (fn thm => fs[thm])
\\ qpat_x_assum `E n = Some vR` (fn thm => fs[thm])))
\\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ fs [] \\ rveq))
(* Const case *)
>- (Cases_on `absenv (Const v)`
>- (Cases_on `absenv (Const m v)`
\\ fs []
\\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ fs [meps_def,inj_eps_Q_def]
\\ `perturb v delta = v` by (qspecl_then [`v`, `delta`] match_mp_tac delta_0_deterministic \\ fs[])
\\fs [validIntervalbounds_def, isSupersetInterval_def, IVhi_def, IVlo_def])
\\ fs [validIntervalbounds_def, isSupersetInterval_def, IVhi_def, IVlo_def])
(* Negation case *)
>- (simp[evalUnop_def]
\\ rw_thm_asm `validIntervalbounds (unop u f) absenv P dVars` validIntervalbounds_def
\\ Cases_on `absenv (Unop u f)`
\\ qmatch_assum_rename_tac `absenv (Unop u f) = (iv_u, err_u)`
\\ Cases_on `absenv f`
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ rveq
\\ fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, negateInterval_def]
\\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`,`v1`] ASSUME_TAC thm)
\\ qpat_x_assum `absenv f = _` (fn thm => fs[thm])
\\ `FST iv_f <= v1 /\ v1 <= SND iv_f`
by (first_x_assum match_mp_tac
\\ conj_tac \\ fs [Once usedVars_def])
\\ qpat_x_assum `! _. Q ==> R` kall_tac
\\ fs[] \\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `- SND iv_f` \\ conj_tac \\ simp [])
>- (qexists_tac `- FST iv_f` \\ conj_tac \\ simp []))
(* Inversion case *)
>- (simp[evalUnop_def]
\\ `perturb (evalUnop Inv v1) delta = evalUnop Inv v1`
by (qspecl_then [`evalUnop Inv v1`, `delta`] match_mp_tac delta_0_deterministic \\ fs[])
\\ `perturb (inv v1) delta = inv v1` by (fs[evalUnop_def])
\\ simp[]
\\ rw_thm_asm `validIntervalbounds a b c d` validIntervalbounds_def
\\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`, `v1`] ASSUME_TAC thm)
\\ Cases_on `absenv (Unop u f)`
\\ qmatch_assum_rename_tac `absenv (Unop u f) = (iv_u, err_u)`
\\ Cases_on `absenv f`
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ rveq
\\ qpat_x_assum `validIntervalbounds _ _ _ _ /\ _ /\ _ /\ _ /\ _ ==> _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [FST, SND] thm))
\\ `FST iv_f <= v1 /\ v1 <= SND iv_f` by (first_x_assum match_mp_tac \\ fs[Once usedVars_def])
\\ rpt (qpat_x_assum `!v. _ ==> _` kall_tac)
\\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `inv (SND iv_f)` \\ conj_tac
\\ TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
\\ `0 < -v1` by REAL_ASM_ARITH_TAC
\\ `-SND iv_f <= -v1` by REAL_ASM_ARITH_TAC
\\ `inv (-v1) <= inv (- SND iv_f)` by fs[REAL_INV_LE_ANTIMONO]
\\ `inv(-v1) = - (inv v1)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `inv(-(SND iv_f)) = - (inv (SND iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `-(inv v1) <= - (inv (SND iv_f))` by fs []
\\ fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < SND iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))
>- (qexists_tac `inv (FST iv_f)` \\ conj_tac
\\ TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
\\ `0 < -v1` by REAL_ASM_ARITH_TAC
\\ `0 < - (FST iv_f)` by REAL_ASM_ARITH_TAC
\\ `- v1 <= - (FST iv_f)` by REAL_ASM_ARITH_TAC
\\ `inv (- FST iv_f) <= inv (- v1)` by fs[REAL_INV_LE_ANTIMONO]
\\ `inv(- FST iv_f) = - (inv (FST iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `inv(- v1) = - (inv v1)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `-(inv (FST iv_f)) <= - (inv v1)` by fs []
\\ fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < FST iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO])))
\\ fs [] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ fs[]
>- (rw_thm_asm `validIntervalbounds (Unop u f) absenv P dVars` validIntervalbounds_def
\\ Cases_on `absenv (Unop u f)`
\\ qmatch_assum_rename_tac `absenv (Unop u f) = (iv_u, err_u)`
\\ Cases_on `absenv f`
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ rveq
\\ fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, negateInterval_def]
\\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`,`v1`] ASSUME_TAC thm)
\\ qpat_x_assum `absenv f = _` (fn thm => fs[thm])
\\ `FST iv_f <= v1 /\ v1 <= SND iv_f`
by (first_x_assum match_mp_tac
\\ conj_tac \\ fs [Once usedVars_def])
\\ qpat_x_assum `! _. Q ==> R` kall_tac
\\ fs[] \\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `- SND iv_f` \\ conj_tac \\ simp [])
>- (qexists_tac `- FST iv_f` \\ conj_tac \\ simp []))
(* Inversion case *)
>- (fs [meps_def,inj_eps_Q_def]
\\ `perturb (evalUnop Inv v1) delta = evalUnop Inv v1`
by (qspecl_then [`evalUnop Inv v1`, `delta`] match_mp_tac delta_0_deterministic \\ fs[])
\\ `perturb (inv v1) delta = inv v1` by (fs[evalUnop_def])
\\ simp[]
\\ rw_thm_asm `validIntervalbounds a b c d` validIntervalbounds_def
\\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`, `v1`] ASSUME_TAC thm)
\\ Cases_on `absenv (Unop u f)`
\\ qmatch_assum_rename_tac `absenv (Unop u f) = (iv_u, err_u)`
\\ Cases_on `absenv f`
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ rveq
\\ qpat_x_assum `validIntervalbounds _ _ _ _ /\ _ /\ _ /\ _ /\ _ ==> _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [FST, SND] thm))
\\ `FST iv_f <= v1 /\ v1 <= SND iv_f` by (first_x_assum match_mp_tac \\ fs[Once usedVars_def])
\\ rpt (qpat_x_assum `!v. _ ==> _` kall_tac)
\\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `inv (SND iv_f)` \\ conj_tac
\\ TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
\\ `0 < -v1` by REAL_ASM_ARITH_TAC
\\ `-SND iv_f <= -v1` by REAL_ASM_ARITH_TAC
\\ `inv (-v1) <= inv (- SND iv_f)` by fs[REAL_INV_LE_ANTIMONO]
\\ `inv(-v1) = - (inv v1)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `inv(-(SND iv_f)) = - (inv (SND iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `-(inv v1) <= - (inv (SND iv_f))` by fs []
\\ fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < SND iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))
>- (qexists_tac `inv (FST iv_f)` \\ conj_tac
\\ TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
\\ `0 < -v1` by REAL_ASM_ARITH_TAC
\\ `0 < - (FST iv_f)` by REAL_ASM_ARITH_TAC
\\ `- v1 <= - (FST iv_f)` by REAL_ASM_ARITH_TAC
\\ `inv (- FST iv_f) <= inv (- v1)` by fs[REAL_INV_LE_ANTIMONO]
\\ `inv(- FST iv_f) = - (inv (FST iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `inv(- v1) = - (inv v1)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `-(inv (FST iv_f)) <= - (inv v1)` by fs []
\\ fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < FST iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))))
(* Binary operator case *)
>- (`perturb (evalBinop b v1 v2) delta = evalBinop b v1 v2`
>- (fs [] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
\\ `(m1 = M0) /\ (m2 = M0)` by (match_mp_tac ifJoinIs0 \\ fs[]) \\ rveq \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ fs [meps_def,inj_eps_Q_def]
\\ `perturb (evalBinop b v1 v2) delta = evalBinop b v1 v2`
by (qspecl_then [`evalBinop b v1 v2`, `delta`] match_mp_tac delta_0_deterministic \\ fs[])
\\ `vR = evalBinop b v1 v2` by fs[]
(* \\ `vR = evalBinop b v1 v2` by fs[]*)
\\ rw_thm_asm `validIntervalbounds (Binop b f f') absenv P V` validIntervalbounds_def
\\ rpt (first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`] ASSUME_TAC thm))
\\ Cases_on `absenv (Binop b f f')` \\ Cases_on `absenv f` \\ Cases_on `absenv f'`
......@@ -306,18 +326,35 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
metis_tac [])
>- (qexists_tac `max4 (FST iv_f * (inv (SND iv_f')))
(FST iv_f * (inv (FST iv_f'))) (SND iv_f * (inv (SND iv_f'))) (SND iv_f * (inv (FST iv_f')))` \\
metis_tac []))));
metis_tac [])))
(* Downcast case *)
>- (fs []
\\ rw_thm_asm `validIntervalbounds (Downcast m f) absenv P dVars` validIntervalbounds_def
\\ Cases_on `absenv (Downcast m f)`
\\ qmatch_assum_rename_tac `absenv (Downcast m f) = (iv_u, err_u)`
\\ Cases_on `absenv f`
\\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
\\ rveq
\\ fs[isSupersetInterval_def, IVlo_def, IVhi_def]
(* TODO: following lines are ugly *)
\\ `domain (usedVars f) DIFF domain dVars domain fVars` by (fs[Once usedVars_def])
\\ `FST iv_u = FST iv_f` by (metis_tac [REAL_LE_ANTISYM])
\\ `SND iv_u = SND iv_f` by (metis_tac [REAL_LE_ANTISYM])
\\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`, `vR`] ASSUME_TAC thm)
\\ qpat_x_assum `absenv f = _` (fn thm => fs [thm])
\\ first_x_assum match_mp_tac
\\ `FST (FST (absenv f)) <= vR vR SND (FST (absenv f))` by (first_x_assum match_mp_tac \\ fs [])));
val getRetExp_def = Define `
getRetExp (f:'a cmd) =
case f of
|Let x e g => getRetExp g
|Let m x e g => getRetExp g
|Ret e => e`;
val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
``!f (absenv:analysisResult) E vR (fVars dVars outVars:num_set) elo ehi err P.
ssa f (union fVars dVars) outVars /\
bstep f E 0 vR /\
bstep (toREvalCmd f) E (toREvalVars defVars) vR M0 /\
(!v. v IN (domain dVars) ==>
?vR.
(E v = SOME vR) /\
......@@ -332,10 +369,10 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
(absenv (getRetExp f) = ((elo, ehi), err)) ==>
elo <= vR /\ vR <= ehi``,
gen_tac \\ Induct_on `f`
\\ once_rewrite_tac [validIntervalboundsCmd_def]
\\ once_rewrite_tac [validIntervalboundsCmd_def,toREvalCmd_def]
\\ rpt gen_tac \\ strip_tac
>- (inversion `ssa _ _ _` ssa_cases
\\ inversion `bstep _ _ _ _` bstep_cases
\\ fs [] \\ inversion `bstep _ _ _ _ _` bstep_cases
\\ fs []
\\ first_x_assum match_mp_tac
\\ qexistsl_tac [`absenv`, `updEnv n v E`, `fVars`, `insert n () dVars`, `outVars`, `err`, `P`]
......@@ -371,7 +408,7 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
\\ fs [domain_union])
>- (fs [Once getRetExp_def]))
>- (inversion `ssa _ _ _` ssa_cases
\\ inversion `bstep _ _ _ _` bstep_cases
\\ fs [] \\ inversion `bstep _ _ _ _ _` bstep_cases
\\ fs [updEnv_def, getRetExp_def]
\\ drule validIntervalbounds_sound
\\ disch_then (qspecl_then [`fVars`, `E`, `vR`] ASSUME_TAC)
......
......@@ -204,168 +204,168 @@ val dummy_bind_ok = store_thm ("dummy_bind_ok",
\\ qexists_tac `inVars`
\\ qpat_x_assum `domain _ SUBSET _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [usedVars_def] thm))
\\ fs[]))
>- (qpat_assum `v = perturb _ _` (fn thm => once_rewrite_tac [thm])
>- (`(m1 = M0) /\ (m2 = M0)` by (match_mp_tac ifJoinIs0 \\ fs[])
\\ rveq
\\ qpat_assum `M0 = _` (fn thm => once_rewrite_tac [thm])
\\ match_mp_tac Binop_dist \\ fs[]
`m1 = M0 /\ m2 = M0` by (qpat_x_assum `M0 = computeJoin m1 m2` (fn thm => ASSUME_TAC ifJoinIs0 \\ 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]));
\\ conj_tac \\ first_x_assum match_mp_tac \\ qexists_tac `inVars` \\ fs[domain_union])
>- (qpat_x_assum `domain _ SUBSET _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [usedVars_def] thm))
\\ fs [] \\ first_x_assum match_mp_tac \\ qexists_tac `inVars` \\ fs[]));
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
|Const m v => Const m 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`;
|Downcast m e1 => Downcast m (exp_subst e1 x e_new)`;
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]
\\ match_mp_tac meps_0_deterministic \\ asm_exists_tac \\ simp[])
>- (match_mp_tac Var_load \\ fs[updEnv_def]
\\ inversion `eval_exp 0 E (Var n) _` eval_exp_cases \\ fs[]))
>- (conj_tac \\ strip_tac \\ inversion `eval_exp _ _ _ _` eval_exp_cases
\\ fs [exp_subst_def, updEnv_def]
>- (metis_tac [eval_exp_rules])
>- (inversion `eval_exp _ _ (Const v) _` eval_exp_cases \\ rveq
\\ match_mp_tac Const_dist \\ fs[]))
>- (conj_tac \\ once_rewrite_tac [exp_subst_def, updEnv_def] \\ strip_tac
\\ inversion `eval_exp _ _ _ _` eval_exp_cases \\ rveq \\ fs []
>- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1`
by (first_x_assum match_mp_tac \\ fs[])
\\ match_mp_tac Unop_neg
\\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [GSYM thm])
\\ fs[])
>- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1`
by (first_x_assum match_mp_tac \\ fs[])
\\ match_mp_tac Unop_inv
\\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [GSYM thm])
\\ fs[])
>- (inversion `eval_exp 0 E (Unop u _) _` eval_exp_cases
\\ fs[]
>- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1`
by (first_x_assum match_mp_tac \\ fs[])
\\ match_mp_tac Unop_neg
\\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [thm])
\\ fs[])
>- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1`
by (first_x_assum match_mp_tac \\ fs[])
\\ match_mp_tac Unop_inv
\\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [thm])
\\ fs[])))
>- (rename1 `Binop b e1 e2`
\\ conj_tac \\ once_rewrite_tac [updEnv_def, exp_subst_def] \\ simp[]
\\ strip_tac \\ inversion `eval_exp _ _ _ _` eval_exp_cases \\ rveq
>- (`eval_exp 0 (updEnv x v E) e1 v1 eval_exp 0 E (exp_subst e1 x e_sub) v1`
by (first_x_assum match_mp_tac \\ fs[])
\\ `eval_exp 0 (updEnv x v E) e2 v2 eval_exp 0 E (exp_subst e2 x e_sub) v2`
by (first_x_assum match_mp_tac \\ fs[])
\\ match_mp_tac Binop_dist
\\ fs[])
>- (`eval_exp 0 (updEnv x v E) e1 v1 eval_exp 0 E (exp_subst e1 x e_sub) v1`
by (first_x_assum match_mp_tac \\ fs[])
\\ `eval_exp 0 (updEnv x v E) e2 v2 eval_exp 0 E (exp_subst e2 x e_sub) v2`
by (first_x_assum match_mp_tac \\ fs[])
\\ match_mp_tac Binop_dist
\\ fs[])));
(* 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] *)
(* \\ match_mp_tac meps_0_deterministic \\ asm_exists_tac \\ simp[]) *)
(* >- (match_mp_tac Var_load \\ fs[updEnv_def] *)
(* \\ inversion `eval_exp 0 E (Var n) _` eval_exp_cases \\ fs[])) *)
(* >- (conj_tac \\ strip_tac \\ inversion `eval_exp _ _ _ _` eval_exp_cases *)
(* \\ fs [exp_subst_def, updEnv_def] *)
(* >- (metis_tac [eval_exp_rules]) *)
(* >- (inversion `eval_exp _ _ (Const v) _` eval_exp_cases \\ rveq *)
(* \\ match_mp_tac Const_dist \\ fs[])) *)
(* >- (conj_tac \\ once_rewrite_tac [exp_subst_def, updEnv_def] \\ strip_tac *)
(* \\ inversion `eval_exp _ _ _ _` eval_exp_cases \\ rveq \\ fs [] *)
(* >- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ match_mp_tac Unop_neg *)
(* \\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [GSYM thm]) *)
(* \\ fs[]) *)
(* >- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ match_mp_tac Unop_inv *)
(* \\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [GSYM thm]) *)
(* \\ fs[]) *)
(* >- (inversion `eval_exp 0 E (Unop u _) _` eval_exp_cases *)
(* \\ fs[] *)
(* >- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ match_mp_tac Unop_neg *)
(* \\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [thm]) *)
(* \\ fs[]) *)
(* >- (`eval_exp 0 (updEnv x v E) e v1 <=> eval_exp 0 E (exp_subst e x e_sub) v1` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ match_mp_tac Unop_inv *)
(* \\ qpat_x_assum `eval_exp _ _ _ _ <=> eval_exp _ _ _ _` (fn thm => once_rewrite_tac [thm]) *)
(* \\ fs[]))) *)
(* >- (rename1 `Binop b e1 e2` *)
(* \\ conj_tac \\ once_rewrite_tac [updEnv_def, exp_subst_def] \\ simp[] *)
(* \\ strip_tac \\ inversion `eval_exp _ _ _ _` eval_exp_cases \\ rveq *)
(* >- (`eval_exp 0 (updEnv x v E) e1 v1 ⇔ eval_exp 0 E (exp_subst e1 x e_sub) v1` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ `eval_exp 0 (updEnv x v E) e2 v2 ⇔ eval_exp 0 E (exp_subst e2 x e_sub) v2` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ match_mp_tac Binop_dist *)
(* \\ fs[]) *)
(* >- (`eval_exp 0 (updEnv x v E) e1 v1 ⇔ eval_exp 0 E (exp_subst e1 x e_sub) v1` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ `eval_exp 0 (updEnv x v E) e2 v2 ⇔ eval_exp 0 E (exp_subst e2 x e_sub) v2` *)
(* by (first_x_assum match_mp_tac \\ fs[]) *)
(* \\ match_mp_tac Binop_dist *)
(* \\ fs[]))); *)
val map_subst_def = Define `
map_subst (f:real cmd) x e =
case f of
|Let y e_y g => Let y (exp_subst e_y x e) (map_subst g x e)
|Ret e_r => Ret (exp_subst e_r x e)`;
(* val map_subst_def = Define ` *)
(* map_subst (f:real cmd) x e = *)
(* case f of *)
(* |Let y e_y g => Let y (exp_subst e_y x e) (map_subst g x e) *)
(* |Ret e_r => Ret (exp_subst e_r x e)`; *)
val stepwise_substitution = store_thm ("stepwise_substitution",
``!x e v f E vR inVars outVars.
ssa f inVars outVars /\
x IN (domain inVars) /\
(domain (usedVars e)) SUBSET (domain inVars) /\
eval_exp 0 E e v ==>
(bstep f (updEnv x v E) 0 vR <=>
bstep (map_subst f x e) E 0 vR)``,
Induct_on `f`
\\ once_rewrite_tac [map_subst_def] \\ rpt strip_tac
\\ once_rewrite_tac [EQ_IMP_THM] \\ simp []
\\ inversion `ssa _ _ _` ssa_cases
\\ conj_tac \\ strip_tac \\ inversion `bstep _ _ _ _` bstep_cases
>- (match_mp_tac let_b
\\ qexists_tac `v'`
\\ conj_tac
>- (`eval_exp 0 (updEnv x v E) e v' <=> eval_exp 0 E (exp_subst e x e') v'`
by (match_mp_tac exp_subst_correct \\ fs[])
\\ fs [])
>- (`bstep f (updEnv x v (updEnv n v' E)) 0 vR <=> bstep (map_subst f x e') (updEnv n v' E) 0 vR`
by (first_x_assum match_mp_tac \\ qexistsl_tac [`insert n () inVars`, `outVars`]
\\ fs[ domain_insert] \\ conj_tac
>- (match_mp_tac SUBSET_TRANS \\ qexists_tac `domain inVars`
\\ fs [])
>- (match_mp_tac dummy_bind_ok \\ asm_exists_tac \\ fs[]))
\\ first_x_assum (fn thm => once_rewrite_tac [GSYM thm])
\\ `bstep f (updEnv n v' (updEnv x v E)) 0 vR <=>
bstep f (updEnv x v (updEnv n v' E)) 0 vR`
by (match_mp_tac shadowing_free_rewriting_cmd \\ strip_tac \\ fs[updEnv_def]
\\ Cases_on `n' = n` \\ Cases_on `n' = x` \\ fs[])
\\ rw_sym_asm `bstep _ _ _ _ <=> _`
\\ fs[]))
>- (match_mp_tac let_b
\\ qexists_tac `v'`
\\ conj_tac
>- (`eval_exp 0 (updEnv x v E) e v' <=> eval_exp 0 E (exp_subst e x e') v'`
by (match_mp_tac exp_subst_correct \\ fs[])
\\ fs [])
>- (`bstep f (updEnv x v (updEnv n v' E)) 0 vR <=> bstep (map_subst f x e') (updEnv n v' E) 0 vR`
by (first_x_assum match_mp_tac \\ qexistsl_tac [`insert n () inVars`, `outVars`]
\\ fs[domain_insert] \\ conj_tac
>- (match_mp_tac SUBSET_TRANS \\ qexists_tac `domain inVars`
\\ fs [])
>- (match_mp_tac dummy_bind_ok \\ asm_exists_tac \\ fs[]))
\\ `bstep f (updEnv n v' (updEnv x v E)) 0 vR <=>
bstep f (updEnv x v (updEnv n v' E)) 0 vR`
by (match_mp_tac shadowing_free_rewriting_cmd \\ strip_tac \\ fs[updEnv_def]
\\ Cases_on `n' = n` \\ Cases_on `n' = x` \\ fs[])
\\ rw_asm `bstep _ _ _ _ <=> bstep f (updEnv _ _ _) _ _`
\\ first_x_assum (fn thm => once_rewrite_tac [thm])
\\ fs[]))
>- (match_mp_tac ret_b
\\ `eval_exp 0 (updEnv x v E) e vR <=> eval_exp 0 E (exp_subst e x e') vR`
by (match_mp_tac exp_subst_correct \\ fs[])
\\ rw_sym_asm `eval_exp _ _ _ _ <=> eval_exp _ _ _ _`
\\ fs[])
>- (match_mp_tac ret_b
\\ `eval_exp 0 (updEnv x v E) e vR <=> eval_exp 0 E (exp_subst e x e') vR`
by (match_mp_tac exp_subst_correct \\ fs[])
\\ rw_asm `eval_exp _ _ _ _ <=> eval_exp _ _ _ _`
\\ fs[]));
(* val stepwise_substitution = store_thm ("stepwise_substitution", *)
(* ``!x e v f E vR inVars outVars. *)
(* ssa f inVars outVars /\ *)
(* x IN (domain inVars) /\ *)
(* (domain (usedVars e)) SUBSET (domain inVars) /\ *)
(* eval_exp 0 E e v ==> *)
(* (bstep f (updEnv x v E) 0 vR <=> *)
(* bstep (map_subst f x e) E 0 vR)``, *)
(* Induct_on `f` *)
(* \\ once_rewrite_tac [map_subst_def] \\ rpt strip_tac *)
(* \\ once_rewrite_tac [EQ_IMP_THM] \\ simp [] *)
(* \\ inversion `ssa _ _ _` ssa_cases *)
(* \\ conj_tac \\ strip_tac \\ inversion `bstep _ _ _ _` bstep_cases *)
(* >- (match_mp_tac let_b *)
(* \\ qexists_tac `v'` *)
(* \\ conj_tac *)
(* >- (`eval_exp 0 (updEnv x v E) e v' <=> eval_exp 0 E (exp_subst e x e') v'` *)
(* by (match_mp_tac exp_subst_correct \\ fs[]) *)
(* \\ fs []) *)
(* >- (`bstep f (updEnv x v (updEnv n v' E)) 0 vR <=> bstep (map_subst f x e') (updEnv n v' E) 0 vR` *)
(* by (first_x_assum match_mp_tac \\ qexistsl_tac [`insert n () inVars`, `outVars`] *)
(* \\ fs[ domain_insert] \\ conj_tac *)
(* >- (match_mp_tac SUBSET_TRANS \\ qexists_tac `domain inVars` *)
(* \\ fs []) *)
(* >- (match_mp_tac dummy_bind_ok \\ asm_exists_tac \\ fs[])) *)
(* \\ first_x_assum (fn thm => once_rewrite_tac [GSYM thm]) *)
(* \\ `bstep f (updEnv n v' (updEnv x v E)) 0 vR <=> *)