Add variable soundness proof

hol4/ErrorValidationScript.sml

@@ -69,38 +69,45 @@ val err_always_positive = store_thm ("err_always_positive",
   Cases_on `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
 
 val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable",
-  ``!(VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult) (v:num)
-     (nR nF err nlo nhi:real) (P:precond).
-      approxEnv VarEnv1 absenv VarEnv2 /\
+  ``!(ParamEnv:env) (v:num)
+     (nR nF err nlo nhi:real) (P:precond) VarEnv1 absenv VarEnv2.
+      approxEnv VarEnv1 absenv VarEnv2 ==>
       eval_exp 0 VarEnv1 ParamEnv P (Var v) nR /\
       eval_exp machineEpsilon VarEnv2 ParamEnv P (Var v) nF /\
       validErrorbound (Var v) absenv /\
       (absenv (Var v) = ((nlo, nhi),err)) ==>
       abs (nR - nF) <= err``,
+  gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\
+  gen_tac \\ gen_tac \\
+  ho_match_mp_tac approxEnv_ind \\
   once_rewrite_tac [validErrorbound_def] \\
-  Induct_on `` \\
   rpt strip_tac \\
-  inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\
-  inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\
-  fs[] \\
-  >- (rpt strip_tac \\)
-  >- ()
+  fs[]
+  >- (inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\
+      inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\
+      fs[])
+  >- (inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\
+      inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\
+      fs[updEnv_def] \\
+      Cases_on `v = x` \\ fs[] \\
+      first_x_assum match_mp_tac \\
+      conj_tac \\ metis_tac [eval_exp_rules]));
 
 val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant",
-  ``!(cenv:env) (absenv:analysisResult) (n:real) (nR:real) (nF:real) (e:real) (nlo:real) (nhi:real) (P:precond).
-      eval_exp 0 cenv P (Const n) nR /\
-      eval_exp machineEpsilon cenv P (Const n) nF /\
+  ``!(VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) (P:precond).
+      approxEnv VarEnv1 absenv VarEnv2 /\
+      eval_exp 0 VarEnv1 ParamEnv P (Const n) nR /\
+      eval_exp machineEpsilon VarEnv2 ParamEnv P (Const n) nF /\
       validErrorbound (Const n) absenv /\
-      validIntervalbounds (Const n) absenv P /\
+      FST (FST (absenv (Const n))) <= nR /\
+      nR <= SND (FST (absenv (Const  n))) /\
       (absenv (Const n) = ((nlo,nhi),e)) ==>
       (abs (nR - nF)) <= e``,
   once_rewrite_tac [validErrorbound_def] \\
   rpt strip_tac \\ fs[] \\
-  `FST (FST (absenv (Const n))) <= nR /\ nR <= SND (FST (absenv (Const n)))`
-    by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ simp[]) \\
-  inversion `eval_exp 0 cenv P (Const n) nR` eval_exp_cases \\ rveq \\
+  inversion `eval_exp 0 _ _ P (Const n) nR` eval_exp_cases \\ rveq \\
   simp [delta_0_deterministic] \\
-  inversion `eval_exp machineEpsilon _ _ _ _` eval_exp_cases \\ rveq \\
+  inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\ rveq \\
   simp[perturb_def] \\
   rename1 `abs deltaF <= machineEpsilon` \\
   simp [Rabs_err_simpl, ABS_MUL] \\
@@ -114,23 +121,24 @@ val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant"
   simp[]);
 
 val validErrorboundCorrectParam = store_thm ("validErrorboundCorrectParam",
-  ``!(cenv:env) (absenv:analysisResult) (v:num) (nR:real) (nF:real) (e:real) (nlo:real) (nhi:real) (P:precond).
-      eval_exp 0 cenv P (Param v) nR /\
-      eval_exp machineEpsilon cenv P (Param v) nF /\
+  ``!(VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult) (v:num) (nR nF e nlo nhi:real) (P:precond).
+      approxEnv VarEnv1 absenv VarEnv2 /\
+      eval_exp 0 VarEnv1 ParamEnv P (Param v) nR /\
+      eval_exp machineEpsilon VarEnv2 ParamEnv P (Param v) nF /\
       validErrorbound (Param v) absenv /\
-      validIntervalbounds (Param v) absenv P /\
+      FST (FST (absenv (Param v))) <= nR /\
+      nR <= SND (FST (absenv (Param v))) /\
+      (!(v1:num).
+         MEM v1 (freeVars ((Param v):real exp)) ==>
+         isSupersetInterval (P v1) (FST (absenv (Param v1)))) /\
       (absenv (Param v) = ((nlo,nhi),e)) ==>
-      (abs (nR - nF)) <= e``,
+      (abs (nR - nF)) <= e``
   once_rewrite_tac [validErrorbound_def] \\
   rpt strip_tac \\ fs[] \\
-  `!(v1:num). MEM v1 (freeVars ((Param v):real exp)) ==> isSupersetInterval (P v1) (FST (absenv (Param v1)))`
-    by (drule ivbounds_approximatesPrecond_sound \\ rpt strip_tac \\ first_x_assum (match_mp_tac) \\ simp[]) \\
-  `FST (FST (absenv (Param v))) <= nR  /\ nR <= SND (FST (absenv (Param v)))`
-    by (match_mp_tac validIntervalbounds_sound \\ qexists_tac `P` \\ qexists_tac `cenv` \\ simp[]) \\
   qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2)) \\
-  inversion `eval_exp 0 _ _ _ _` eval_exp_cases \\ rveq \\
+  inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\ rveq \\
   simp [delta_0_deterministic] \\
-  inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\
+  inversion `eval_exp _ _ _ _ _ _` eval_exp_cases \\ rveq \\
   simp [perturb_def] \\
   rename1 `abs deltaF <= machineEpsilon` \\
   simp [Rabs_err_simpl, ABS_MUL] \\