Add new evaluation semantics to HOL4, without proofs

hol4/CommandsScript.sml

@@ -12,6 +12,7 @@ val _ = Datatype `
        | Ret ('v exp)
        | Nop`;
 
+(*
 val (sstep_rules, sstep_ind, sstep_cases) = Hol_reln `
   (! x e s VarEnv ParamEnv P v eps.
     eval_exp eps VarEnv ParamEnv P e v ==>
@@ -19,20 +20,21 @@ val (sstep_rules, sstep_ind, sstep_cases) = Hol_reln `
   (! e VarEnv ParamEnv P v eps.
     eval_exp eps VarEnv ParamEnv P e v ==>
     sstep (Ret e) VarEnv ParamEnv P eps Nop (updEnv 0 v VarEnv))`;
+*)
 
 val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
-  (! x e s s' VarEnv ParamEnv P v eps VarEnv2.
-    eval_exp eps VarEnv ParamEnv P e v /\
-    bstep s (updEnv x v VarEnv) ParamEnv P eps s' VarEnv2 ==>
-    bstep (Let x e s) VarEnv ParamEnv P eps s' VarEnv2) /\
-  (! e VarEnv ParamEnv P v eps.
-    eval_exp eps VarEnv ParamEnv P e v ==>
-    bstep (Ret e) VarEnv ParamEnv P eps Nop (updEnv 0 v VarEnv))`;
+  (! x e s s' E v eps VarEnv2.
+    eval_exp eps E e v /\
+    bstep s (updEnv x v E) eps s' VarEnv2 ==>
+    bstep (Let x e s) E eps s' VarEnv2) /\
+  (! e E v eps.
+    eval_exp eps E e v ==>
+    bstep (Ret e) E eps Nop (updEnv 0 v VarEnv))`;
 
 val bstep_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
-    [``bstep (Let x e s) VarEnv ParamEnv P eps s' VarEnv2``,
-     ``bstep (Ret e) VarEnv ParamEnv P eps Nop VarEnv2``]
+    [``bstep (Let x e s) E eps s' VarEnv2``,
+     ``bstep (Ret e) E eps Nop VarEnv2``]
   |> LIST_CONJ |> curry save_thm "bstep_cases";
 
 val _ = export_theory ();

hol4/abbrevsScript.sml

@@ -21,13 +21,13 @@ val _ = type_abbrev ("precond", ``:num->interval``);
 (**
   Abbreviations for the environment types
 **)
-val _ = type_abbrev("env",``:num->real``);
+val _ = type_abbrev("env",``:num->real option``);
 
 (**
   Define environment update function as abbreviation.
 **)
 val updEnv_def = Define `
-updEnv (x:num) (v:real) (E:env) (y:num) :real = if y = x then v else E y`;
+updEnv (x:num) (v:real) (E:env) (y:num) :real option = if y = x then SOME v else E y`;
 
 
 val - = export_theory();

hol4/expressionsScript.sml

@@ -10,32 +10,32 @@ val _ = new_theory "expressions";
   Define them first
 **)
 val _ = Datatype `
-binop = Plus | Sub | Mult | Div`;
+  binop = Plus | Sub | Mult | Div`;
 
 (**
   Next define an evaluation function for binary operators.
   Errors are added on the expression evaluation level later
 *)
 val evalBinop_def = Define `
-evalBinop Plus v1 v2 = v1 + v2 /\
-evalBinop Sub  v1 v2 = v1 - v2 /\
-evalBinop Mult v1 v2 = v1 * v2 /\
-evalBinop Div  v1 v2 = v1 / (v2:real)`;
+  evalBinop Plus v1 v2 = v1 + v2 /\
+  evalBinop Sub  v1 v2 = v1 - v2 /\
+  evalBinop Mult v1 v2 = v1 * v2 /\
+  evalBinop Div  v1 v2 = v1 / (v2:real)`;
 
 (**
 Expressions will use unary operators.
 Define them first
 **)
 val _ = Datatype `
-unop = Neg | Inv`
+  unop = Neg | Inv`
 
 (**
 Define evaluation for unary operators on reals.
 Errors are added in the expression evaluation level later
 **)
 val evalUnop_def = Define `
-evalUnop Neg v = - v /\
-evalUnop Inv v = inv(v:real)`
+  evalUnop Neg v = - v /\
+  evalUnop Inv v = inv(v:real)`
 (**
   Define expressions parametric over some value type 'v.  Will ease
   reasoning about different instantiations later.  Note that we
@@ -47,7 +47,6 @@ evalUnop Inv v = inv(v:real)`
 **)
 val _ = Datatype `
   exp = Var num
-      | Param num
       | Const 'v
       | Unop unop exp
       | Binop binop exp exp`
@@ -56,7 +55,7 @@ val _ = Datatype `
   Define a perturbation function to ease writing of basic definitions
 **)
 val perturb_def = Define `
-perturb (r:real) (e:real) = r * (1 + e)`
+  perturb (r:real) (e:real) = r * (1 + e)`
 
 (**
   Define expression evaluation relation parametric by an "error"
@@ -64,38 +63,31 @@ perturb (r:real) (e:real) = r * (1 + e)`
   using a perturbation of the real valued computation by (1 + d)
 **)
 val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
-   (!eps VarEnv ParamEnv P x.
-         eval_exp eps VarEnv ParamEnv P (Var x) (VarEnv x)) /\
-   (!eps VarEnv ParamEnv P x delta delta_lo delta_hi.
-         abs delta <= eps /\
-         abs delta_lo <= eps /\
-         abs delta_hi <= eps /\
-         perturb (FST (P x)) delta_lo  <= perturb (ParamEnv x) delta /\
-         perturb (ParamEnv x) delta <= perturb (SND (P x)) delta_hi ==>
-         eval_exp eps VarEnv ParamEnv P (Param x) (perturb (ParamEnv x) delta)) /\
-   (!eps VarEnv ParamEnv P n delta.
+   (!eps E x v.
+           E x = SOME v ==>
+           eval_exp eps E (Var x) v) /\
+   (!eps E n delta.
          abs delta <= eps ==>
-         eval_exp eps VarEnv ParamEnv P (Const n) (perturb n delta)) /\
-    (!eps VarEnv ParamEnv P f1 v1.
-          eval_exp eps VarEnv ParamEnv P f1 v1 ==>
-          eval_exp eps VarEnv ParamEnv P (Unop Neg f1) (evalUnop Neg v1)) /\
-    (!eps VarEnv ParamEnv P f1 v1 delta.
+         eval_exp eps E (Const n) (perturb n delta)) /\
+    (!eps E f1 v1.
+          eval_exp eps E f1 v1 ==>
+          eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)) /\
+    (!eps E f1 v1 delta.
           abs delta <= eps /\
-          eval_exp eps VarEnv ParamEnv P f1 v1 ==>
-          eval_exp eps VarEnv ParamEnv P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
-    (!eps VarEnv ParamEnv P b f1 f2 v1 v2 delta.
+          eval_exp eps E f1 v1 ==>
+          eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
+    (!eps E b f1 f2 v1 v2 delta.
           abs delta <= eps /\
-          eval_exp eps VarEnv ParamEnv P f1 v1 /\
-          eval_exp eps VarEnv ParamEnv P f2 v2 ==>
-          eval_exp eps VarEnv ParamEnv P (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
+          eval_exp eps E f1 v1 /\
+          eval_exp eps E f2 v2 ==>
+          eval_exp eps E (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
 
 val eval_exp_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases])
-    [``eval_exp eps VarEnv ParamEnv P (Var v) res``,
-     ``eval_exp eps VarEnv ParamEnv P (Param v) res``,
-     ``eval_exp eps VarEnv ParamEnv P (Const n) res``,
-     ``eval_exp eps VarEnv ParamEnv P (Unop u e) res``,
-     ``eval_exp eps VarEnv ParamEnv P (Binop n e1 e2) res``]
+    [``eval_exp eps E (Var v) res``,
+     ``eval_exp eps E (Const n) res``,
+     ``eval_exp eps E (Unop u e) res``,
+     ``eval_exp eps E (Binop n e1 e2) res``]
   |> LIST_CONJ |> curry save_thm "eval_exp_cases";
 
 val delta_0_deterministic = store_thm("delta_0_deterministic",
@@ -103,12 +95,29 @@ val delta_0_deterministic = store_thm("delta_0_deterministic",
   fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
 
 val meps_0_deterministic = store_thm("meps_0_deterministic",
-  ``!(e: real exp) v1:real v2:real VarEnv ParamEnv P.
-      eval_exp (&0) VarEnv ParamEnv P e v1 /\ eval_exp (&0) VarEnv ParamEnv P e v2 ==> v1 = v2``,
+  ``!(e: real exp) v1:real v2:real E.
+      eval_exp (&0) E e v1 /\ eval_exp (&0) E e v2 ==> v1 = v2``,
   Induct \\ fs [eval_exp_cases]
   \\ rw [] \\ fs [delta_0_deterministic]
   \\ res_tac \\ fs []);
 
+(**
+Helping lemma. Needed in soundness proof.
+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 Eironment.
+This relies on the property that variables are not perturbed as opposed to parameters
+**)
+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 E)) (Binop b (Var 1) (Var 2)) v))``,
+  fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
+  \\ metis_tac []);
+
 (*
   Using the parametric expressions, define boolean expressions for conditionals
 *)
@@ -120,40 +129,23 @@ val _ = Datatype `
   Define evaluation of boolean expressions
 *)
 val (bval_exp_rules, bval_exp_ind, bval_exp_cases) = Hol_reln `
-  (!eps VarEnv ParamEnv P e1 e2 v1 v2.
-      eval_exp eps VarEnv ParamEnv P e1 v1 /\
-      eval_exp eps VarEnv ParamEnv P e2 v2 ==>
-      bval eps VarEnv ParamEnv P (Leq e1 e2) (v1 <= v2))/\
-  (!eps VarEnv ParamEnv P e1 e2 v1 v2.
-      eval_exp eps VarEnv ParamEnv P e1 v1 /\
-      eval_exp eps VarEnv ParamEnv P e2 v2 ==>
-      bval eps VarEnv ParamEnv P (Less 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 (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))`;
 
 val bval_exp_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bval_exp_cases])
-    [``bval eps VarEnv ParamEnv P (Leq e1 e2) res``,
-     ``bval eps VarEnv ParamEnv P (Less e1 e2) res``]
+    [``bval eps E (Leq e1 e2) res``,
+     ``bval eps E (Less e1 e2) res``]
   |> LIST_CONJ |> curry save_thm "bval_exp_cases";
 
 (* Simplify arithmetic later by making > >= only abbreviations *)
 val _ = overload_on("Gr",``\(e1:('v)exp). \(e2:('v)exp). Less e2 e1``);
 val _ = overload_on("Greq",``\(e1:('v)exp). \(e2:('v)exp). Leq e2 e1``);
 
-(**
-Helping lemma. Needed in soundness proof.
-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 Eironment.
-This relies on the property that variables are not perturbed as opposed to parameters
-**)
-val binary_unfolding = store_thm("binary_unfolding",
-``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) VarEnv ParamEnv (P:precond) (v:real).
-      (eval_exp eps VarEnv ParamEnv P (Binop b e1 e2) v <=>
-        (?(v1:real) (v2:real).
-           eval_exp eps VarEnv ParamEnv P e1 v1 /\
-           eval_exp eps VarEnv ParamEnv P e2 v2 /\
-           eval_exp eps (updEnv 2 v2 (updEnv 1 v1 VarEnv)) ParamEnv P (Binop b (Var 1) (Var 2)) v))``,
-  fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
-  \\ metis_tac []);
-
 val _ = export_theory();