Show soundness of let Bindings in HOL4

hol4/CertificateCheckerScript.sml

@@ -15,7 +15,11 @@ val _ = new_theory "CertificateChecker";
 (** Certificate checking function **)
 val CertificateChecker_def = Define
   `CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) =
-	  ((validIntervalbounds e absenv P) /\ (validErrorbound e absenv))`;
+   ((validIntervalbounds e absenv P EMPTY) /\ (validErrorbound e absenv))`;
+
+val CertificateCheckerCmd_def = Define
+  `CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond) =
+   ((validIntervalboundsCmd f absenv P EMPTY) /\ (validErrorboundCmd f absenv))`;
 
 (**
    Soundness proof for the certificate checker.
@@ -23,9 +27,11 @@ val CertificateChecker_def = Define
    the real valued execution respects the precondition.
 **)
 val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
-  ``!(e:real exp) (absenv:analysisResult) P (cenv:env) (vR:real) (vF:real).
-      eval_exp 0 cenv P e vR /\
-      eval_exp machineEpsilon cenv P e vF /\
+  ``!(e:real exp) (absenv:analysisResult) P (VarEnv1 VarEnv2 ParamEnv:env)
+     (vR:real) (vF:real).
+      approxEnv VarEnv1 absenv VarEnv2 /\
+      eval_exp 0 VarEnv1 ParamEnv P e vR /\
+      eval_exp machineEpsilon VarEnv2 ParamEnv P e vF /\
       CertificateChecker e absenv P ==>
       abs (vR - vF) <= (SND (absenv e))``,
 (**
@@ -39,7 +45,26 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
   Cases_on `iv` \\
   rename1 `absenv e = ((elo, ehi), err)` \\
   match_mp_tac validErrorbound_sound \\
-  qexistsl_tac [`e`, `cenv`, `absenv`, `P`, `elo`, `ehi`] \\
+  qexistsl_tac [`e`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `absenv`, `P`, `elo`, `ehi`, `EMPTY`] \\
+  fs[]);
+
+val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_sound",
+  ``!(f:real cmd) (absenv:analysisResult) (P:precond)
+     (VarEnv1 VarEnv2 ParamEnv:env) (outVars:num set) (envR envF:env).
+      approxEnv VarEnv1 absenv VarEnv2 /\
+      ssaPrg f EMPTY outVars /\
+      bstep f VarEnv1 ParamEnv P 0 Nop envR /\
+      bstep f VarEnv2 ParamEnv P machineEpsilon Nop envF /\
+      CertificateCheckerCmd f absenv P ==>
+      abs (envR 0 - envF 0) <= (SND (absenv (Var 0)))``,
+  simp [CertificateCheckerCmd_def] \\
+  rpt strip_tac \\
+  match_mp_tac validErrorboundCmd_sound \\
+  Cases_on `absenv (Var 0)` \\
+  rename1 `absenv (Var 0) = (iv, err)` \\
+  Cases_on `iv` \\
+  rename1 `absenv (Var 0) = ((elo, ehi), err)` \\
+  qexistsl_tac [`f`, `absenv`, `VarEnv1`, `VarEnv2`, `ParamEnv`, `EMPTY`, `outVars`, `elo`, `ehi`, `P`] \\
   fs[]);
 
 val _ = export_theory();

hol4/ErrorValidationScript.sml

@@ -10,7 +10,7 @@ open preamble
 open simpLib realTheory realLib RealArith
 open abbrevsTheory expressionsTheory RealSimpsTheory
 open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
-open IntervalValidationTheory EnvironmentsTheory
+open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
 
 val _ = new_theory "ErrorValidation";
 
@@ -2288,4 +2288,63 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
          >- (rpt (qpat_x_assum `absenv _ = _ ` (fn thm => fs [thm])))
          >- (rpt (qpat_x_assum `absenv _ = _ ` (fn thm => fs [thm]))))));
 
+val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
+  ``!(f:real cmd) (absenv:analysisResult) (VarEnv1 VarEnv2 ParamEnv:env)
+     (inVars outVars:num set) (envR envF:env) (elo ehi err:real) (P:precond).
+      approxEnv VarEnv1 absenv VarEnv2 /\
+      ssaPrg f inVars outVars /\
+      bstep f VarEnv1 ParamEnv P 0 Nop envR /\
+      bstep f VarEnv2 ParamEnv P machineEpsilon Nop envF /\
+      validErrorboundCmd f absenv /\
+      validIntervalboundsCmd f absenv P inVars /\
+     (!v. v IN inVars ==>
+          (FST (FST (absenv (Var v))) <= VarEnv1 v /\ VarEnv1 v <= SND (FST (absenv (Var v))))) /\
+      (absenv (Var 0) = ((elo,ehi),err)) ==>
+     abs ((envR 0) - (envF 0)) <= err``,
+  Induct_on `f` \\ rpt strip_tac
+  >- (inversion `bstep _ _ _ _ 0 _ _` bstep_cases \\ rveq \\
+      inversion `bstep _ _ _ _ machineEpsilon _ _` bstep_cases \\ rveq \\
+      inversion `ssaPrg _ _ _` ssaPrg_cases \\ rveq \\
+      first_x_assum match_mp_tac \\
+      rename1 `eval_exp 0 _ _ _ e vR` \\
+      rename1 `eval_exp machineEpsilon _ _ _ e vF` \\
+      qpat_x_assum `validErrorboundCmd _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorboundCmd_def] thm)) \\
+      qpat_x_assum `validIntervalboundsCmd _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalboundsCmd_def] thm))\\
+      qexistsl_tac [`absenv`, `updEnv n vR VarEnv1`, `updEnv n vF VarEnv2`, `ParamEnv`, `n INSERT inVars`, `outVars`, `elo`, `ehi`, `P`] \\
+      fs [] \\
+      rpt conj_tac
+      >- (match_mp_tac (snd (CONJ_PAIR approxEnv_rules)) \\
+          fs[] \\
+          qpat_x_assum `absenv e = _` (fn thm => simp[GSYM thm]) \\
+          drule validErrorbound_sound \\
+          Cases_on `absenv e` \\
+          rename1 `absenv e = (iv, err_e)` \\
+          Cases_on `iv` \\ rename1 `absenv e = ((ivlo, ivhi), err_e)` \\
+          simp[] \\
+          disch_then (
+            qspecl_then [`e`, `ParamEnv`, `vR`, `vF`, `err_e`, `P`, `ivlo`, `ivhi`, `inVars`]
+            match_mp_tac) \\
+          fs[])
+      >- (gen_tac \\
+          Cases_on `v = n` \\ fs[updEnv_def] \\
+          qpat_x_assum `absenv e = _` (fn thm => once_rewrite_tac [GSYM thm]) \\
+          match_mp_tac validIntervalbounds_sound \\
+          qexistsl_tac [`P`, `inVars`, `VarEnv1`, `ParamEnv`] \\ fs[]))
+  >- (inversion `bstep _ _ _ _ 0 _ _` bstep_cases \\ rveq \\
+      inversion `bstep _ _ _ _ machineEpsilon _ _` bstep_cases \\ rveq \\
+      rename1 `eval_exp 0 _ _ _ e vR` \\
+      rename1 `eval_exp machineEpsilon _ _ _ e vF` \\
+      qpat_x_assum `validErrorboundCmd _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorboundCmd_def] thm)) \\
+      qpat_x_assum `validIntervalboundsCmd _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalboundsCmd_def] thm))\\
+      fs [updEnv_def] \\
+      drule validErrorbound_sound \\
+      disch_then (
+        qspecl_then [`e`, `ParamEnv`, `vR`, `vF`, `err`, `P`, `elo`, `ehi`, `inVars`]
+        match_mp_tac) \\
+      fs[])
+  >- (CCONTR_TAC \\
+      qpat_x_assum `validErrorboundCmd _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorboundCmd_def] thm)) \\
+      qpat_x_assum `validIntervalboundsCmd _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalboundsCmd_def] thm))\\
+      fs []));
+
 val _ = export_theory();