Commit 86eec2be authored by ='s avatar =

hol4 port in progress; ExpressionScript+CommandScript done

parent 9a465adf
......@@ -346,7 +346,7 @@ For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different
variables in the Environment.
**)
(* TODO: write updDefVars function as well *)
Lemma binary_unfolding b f1 f2 m E vF defVars:
eval_exp E defVars (Binop b f1 f2) vF m ->
exists vF1 vF2 m1 m2,
......
......@@ -2,7 +2,7 @@
This file contains some type abbreviations, to ease writing.
**)
open preamble
open realTheory realLib sptreeTheory
open realTheory realLib sptreeTheory MachineTypeTheory
val _ = new_theory "Abbrevs";
(**
......@@ -36,4 +36,8 @@ val emptyEnv_def = Define `
val updEnv_def = Define `
updEnv (x:num) (v:real) (E:env) (y:num) :real option = if y = x then SOME v else E y`;
val updDefVars_def = Define `
updDefVars (x:num) (m:mType) (defVars:num -> mType option) (y:num) :mType option =
if y = x then SOME m else defVars y`;
val - = export_theory();
......@@ -3,7 +3,7 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionAbbrevsTheory
open AbbrevsTheory ExpressionAbbrevsTheory MachineTypeTheory
val _ = new_theory "Commands";
......@@ -13,29 +13,37 @@ val _ = new_theory "Commands";
Only assignments and return statement
**)
val _ = Datatype `
cmd = Let num ('v exp) cmd
cmd = Let mType num ('v exp) cmd
| Ret ('v exp)`;
val toREvalCmd_def = Define `
toREvalCmd (f:real cmd) : real cmd =
case f of
| Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
| Ret e => Ret (toREval e)`;
(**
Define big step semantics for the Daisy language, terminating on a "returned"
result value
**)
val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
(!x e s E v eps vR.
eval_exp eps E e v /\
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 v)`;
(!m m' x e s E v res defVars.
eval_exp E defVars e v m /\
(defVars x = SOME m) /\
bstep s (updEnv x v E) defVars res m' ==>
bstep (Let m x e s) E defVars res m') /\
(!m e E v defVars.
eval_exp E defVars e v m ==>
bstep (Ret e) E defVars v m)`;
(**
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 vR``,
``bstep (Ret e) E eps vR``]
[``bstep (Let m x e s) E defVars vR m'``,
``bstep (Ret e) E defVars vR m``]
|> LIST_CONJ |> curry save_thm "bstep_cases";
val [let_b, ret_b] = CONJ_LIST 2 bstep_rules;
......@@ -49,7 +57,7 @@ save_thm ("ret_b", ret_b);
val freeVars_def = Define `
freeVars (f: 'a cmd) :num_set =
case f of
|Let x e g => delete x (union (usedVars e) (freeVars g))
|Let m x e g => delete x (union (usedVars e) (freeVars g))
|Ret e => usedVars e`;
(**
......@@ -58,7 +66,7 @@ val freeVars_def = Define `
val definedVars_def = Define `
definedVars (f:'a cmd) :num_set =
case f of
|Let (x:num) e g => insert x () (definedVars g)
|Let m (x:num) e g => insert x () (definedVars g)
|Ret e => LN`;
val _ = export_theory ();
......@@ -4,13 +4,14 @@
open preamble miscTheory
open realTheory realLib sptreeTheory
open AbbrevsTheory MachineTypeTheory
open DaisyTactics
val _ = ParseExtras.temp_tight_equality()
val _ = new_theory "Expressions";
(**
Expressions will use binary operators.
EXPRESSIONS WILL use binary operators.
Define them first
**)
val _ = Datatype `
......@@ -143,35 +144,35 @@ val delta_0_deterministic = store_thm("delta_0_deterministic",
(**
Evaluation with 0 as machine epsilon is deterministic
**)
val ifJoinIs0 = store_thm("ifJoinIs0",
``!m1 m2. M0 = computeJoin m1 m2 ==> m1 = M0 /\ m2 = M0``,
strip_tac \\ strip_tac \\ strip_tac \\ fs [computeJoin_def]
\\ Cases_on `isMorePrecise m1 m2` \\ fs [] \\ fs [isMorePrecise_def] \\ rw []);
val meps_0_deterministic = store_thm("meps_0_deterministic",
``!(e: real exp) v1:real v2:real E defVars.
eval_exp E defVars (toREval e) v1 M0 /\ eval_exp E defVars (toREval e) v2 M0 ==> v1 = v2``,
Induct \\ fs [eval_exp_cases]
\\ rw [toREval_def]
\\ rw [] \\ fs [meps_def,inj_eps_Q_def,delta_0_deterministic]
\\ res_tac \\ fs []);
Induct
>- (rw [toREval_def] >> fs [eval_exp_cases] >> rw [] >> fs [delta_0_deterministic] >> res_tac >> fs [])
>- (rw [toREval_def] \\ fs [eval_exp_cases] \\ rw [] \\ fs [meps_def,inj_eps_Q_def] \\ fs [delta_0_deterministic] \\ res_tac \\ fs [])
>- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases]
>- (res_tac \\ fs [REAL_NEG_EQ])
>- rw []
>- rw []
>- (res_tac \\ fs [meps_def,inj_eps_Q_def,delta_0_deterministic]))
>- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases] \\
`abs delta <= meps M0` by fs [] \\ res_tac
qpat_x_assum `abs delta <= meps (computeJoin m1 m2)` kall_tac
qpat_x_assum `_ = computeJoin m1 m2` kall_tac
`abs delta' <= meps M0` by fs [] \\ res_tac
qpat_x_assum `abs delta' <= meps (computeJoin m1' m2')` kall_tac
qpat_x_assum `_ = computeJoin _ _ ` kall_tac
fs [meps_def,inj_eps_Q_def,delta_0_deterministic]
`v1'' = v1'` by res_tac
simp [toREval_def] \\ fs [eval_exp_cases] \\ rw [] \\ fs [meps_def,inj_eps_Q_def] \\ fs [delta_0_deterministic] \\ res_tac \\ fs []
Induct
>- (rw [toREval_def] >> fs [eval_exp_cases] >> rw [] >> fs [delta_0_deterministic] >> res_tac >> fs [])
>- (rw [toREval_def] \\ fs [eval_exp_cases] \\ rw [] \\ fs [meps_def,inj_eps_Q_def] \\ fs [delta_0_deterministic] \\ res_tac \\ fs [])
>- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases]
>- (res_tac \\ fs [REAL_NEG_EQ])
>- rw []
>- rw []
>- (res_tac \\ fs [meps_def,inj_eps_Q_def,delta_0_deterministic]))
>- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases]
\\ `m1' = M0 /\ m2' = M0` by
(qpat_x_assum `M0 = computeJoin m1 m2` (fn thm => ASSUME_TAC ifJoinIs0 \\ fs []))
\\ `m1 = M0 /\ m2 = M0` by (qpat_x_assum `M0 = computeJoin m1' m2'` (fn thm => ASSUME_TAC ifJoinIs0
\\ fs []))
\\ rveq
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ fs [meps_def,inj_eps_Q_def,delta_0_deterministic]
\\ res_tac
\\ fs [])
>- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ res_tac));
(**
Helping lemma. Needed in soundness proof.
......@@ -180,25 +181,28 @@ evaluating the subExpressions and then binding the result values to different
variables in the Eironment.
**)
val binary_unfolding = store_thm("binary_unfolding",
``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) E (v:real).
(eval_exp eps E (Binop b e1 e2) v <=>
(?(v1:real) (v2:real).
eval_exp eps E e1 v1 /\
eval_exp eps E e2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 emptyEnv)) (Binop b (Var 1) (Var 2)) v))``,
fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
``!(b:binop) (e1:(real)exp) (e2:(real)exp) (m:mType) E defVars (v:real).
(eval_exp E defVars (Binop b e1 e2) v m <=>
(?(v1:real) (v2:real) (m1:mType) (m2:mType).
m = computeJoin m1 m2 /\
eval_exp E defVars e1 v1 m1 /\
eval_exp E defVars e2 v2 m2 /\
eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop b (Var 1) (Var 2)) v m))``,
fs [updEnv_def,updDefVars_def,computeJoin_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ metis_tac []);
(**
Analogous lemma for unary expressions
**)
val unary_unfolding = store_thm("unary_unfolding",
``!(u:unop) (e1:(real)exp) (eps:real) E (v:real).
(eval_exp eps E (Unop Inv e1) v <=>
``!(u:unop) (e1:(real)exp) (m:mType) E defVars (v:real).
(eval_exp E defVars (Unop Inv e1) v m <=>
(?(v1:real).
eval_exp eps E e1 v1 /\
eval_exp eps (updEnv 1 v1 emptyEnv) (Unop Inv (Var 1)) v))``,
fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
eval_exp E defVars e1 v1 m /\
eval_exp (updEnv 1 v1 emptyEnv) (updDefVars 1 m defVars) (Unop Inv (Var 1)) v m))``,
fs [updEnv_def, updDefVars_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ metis_tac []);
(*
......@@ -212,19 +216,19 @@ val _ = Datatype `
Define evaluation of boolean expressions
*)
val (bval_exp_rules, bval_exp_ind, bval_exp_cases) = Hol_reln `
(!eps E e1 e2 v1 v2.
eval_exp eps E e1 v1 /\
eval_exp eps E e2 v2 ==>
bval eps E (Leq e1 e2) (v1 <= v2))/\
(!eps E e1 e2 v1 v2.
eval_exp eps E e1 v1 /\
eval_exp eps E e2 v2 ==>
bval eps E (Less e1 e2) (v1 < v2))`;
(!E defVars e1 e2 v1 v2 m.
eval_exp E defVars e1 v1 m /\
eval_exp E defVars e2 v2 m ==>
bval E defVars m (Leq e1 e2) (v1 <= v2))/\
(!E defVars e1 e2 v1 v2 m.
eval_exp E defVars e1 v1 m /\
eval_exp E defVars e2 v2 m ==>
bval E defVars m (Less e1 e2) (v1 < v2))`;
val bval_exp_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bval_exp_cases])
[``bval eps E (Leq e1 e2) res``,
``bval eps E (Less e1 e2) res``]
[``bval E defVars m (Leq e1 e2) res``,
``bval E defVars m (Less e1 e2) res``]
|> LIST_CONJ |> curry save_thm "bval_exp_cases";
(**
......
......@@ -7,7 +7,7 @@
**)
open preamble
open pred_setSyntax pred_setTheory
open AbbrevsTheory ExpressionsTheory CommandsTheory DaisyTactics
open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory DaisyTactics CommandsTheory MachineTypeTheory
val _ = new_theory "ssaPrgs";
......@@ -62,11 +62,11 @@ val validVars_non_stuck = store_thm ("validVars_non_stuck",
ssa f
**)
val (ssa_rules, ssa_ind, ssa_cases) = Hol_reln `
(!x e s inVars (Vterm:num_set).
(!m x e s inVars (Vterm:num_set).
(domain (usedVars e)) SUBSET (domain inVars) /\
(~ (x IN (domain inVars))) /\
ssa s (insert x () inVars) Vterm ==>
ssa (Let x e s) inVars Vterm) /\
ssa (Let m x e s) inVars Vterm) /\
(!e inVars Vterm.
(domain (usedVars e)) SUBSET (domain inVars) /\
(domain inVars = domain Vterm) ==>
......@@ -77,7 +77,7 @@ val (ssa_rules, ssa_ind, ssa_cases) = Hol_reln `
*)
val ssa_cases =
map (GEN_ALL o SIMP_CONV (srw_ss()) [Once ssa_cases])
[``ssa (Let x e s) inVars Vterm``,
[``ssa (Let m x e s) inVars Vterm``,
``ssa (Ret e) inVars Vterm``]
|> LIST_CONJ |> curry save_thm "ssa_cases";
......@@ -130,7 +130,7 @@ val ssa_equal_set = store_thm ("ssa_equal_set",
val validSSA_def = Define `
validSSA (f:real cmd) (inVars:num_set) =
case f of
|Let x e g =>
|Let m x e g =>
((lookup x inVars = NONE) /\
(subspt (usedVars e) inVars) /\
(validSSA g (insert x () inVars)))
......@@ -153,13 +153,13 @@ val validSSA_sound = store_thm ("validSSA_sound",
\\ 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 /\
``!m x y v v' e f inVars outVars E defVars.
ssa (Let m x (toREval e) (toREvalCmd f)) inVars outVars /\
(y IN (domain inVars)) /\
eval_exp 0 E e v ==>
eval_exp E defVars (toREval e) v M0 ==>
!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
\\ inversion `ssa (Let m x (toREval e) (toREvalCmd f)) _ _` ssa_cases
\\ fs[updEnv_def]
\\ Cases_on `n = x` \\ rveq
>- (simp[]
......@@ -168,30 +168,31 @@ val ssa_shadowing_free = store_thm ("ssa_shadowing_free",
>- (simp[]));
val shadowing_free_rewriting_exp = store_thm ("shadowing_free_rewriting_exp",
``!e v E1 E2.
``!e v E1 E2 defVars.
(!n. E1 n = E2 n) ==>
(eval_exp 0 E1 e v <=>
eval_exp 0 E2 e v)``,
(eval_exp E1 defVars (toREval e) v M0 <=>
eval_exp E2 defVars (toREval e) v M0)``,
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.
``!f E1 E2 vR defVars.
(!n. E1 n = E2 n) ==>
(bstep f E1 0 vR <=>
bstep f E2 0 vR)``,
(bstep (toREvalCmd f) E1 defVars vR M0 <=>
bstep (toREvalCmd f) E2 defVars vR M0)``,
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.
``!e v x v' (inVars:num_set) E defVars.
(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
eval_exp E defVars (toREval e) v M0 ==>
eval_exp (updEnv x v' E) defVars (toREval e) v M0``,
Induct \\ rpt strip_tac \\ once_rewrite_tac [toREval_def] \\ qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm)) \\ fs [] \\ rveq \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
>- (match_mp_tac Var_load
\\ fs[usedVars_def, updEnv_def]
\\ Cases_on `n = x` \\ rveq \\ fs[] )
>- (match_mp_tac Const_dist \\ simp[])
\\ Cases_on `n = x` \\ rveq \\ fs[])
>- (qpat_x_assum `v' = perturb _ _` (fn thm => once_rewrite_tac [thm])
\\ match_mp_tac Const_dist \\ simp[])
>- (Cases_on `u` \\ rveq \\ fs[updEnv_def]
>- (match_mp_tac Unop_neg
\\ first_x_assum match_mp_tac
......@@ -203,7 +204,13 @@ 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[]))
>- (match_mp_tac Binop_dist \\ fs[]
>- (qpat_assum `v = perturb _ _` (fn thm => once_rewrite_tac [thm])
\\ 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]));
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment