Show error bound of parameters sound

hol4/ErrorValidationScript.sml

@@ -62,11 +62,11 @@ val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant"
       validErrorbound (Const n) absenv /\
       validIntervalbounds (Const n) absenv P /\
       (absenv (Const n) = ((nlo,nhi),e)) ==>
-      (abs (nR - nF)) <= 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 \\ exists_tac ``P:precond`` \\ exists_tac ``cenv:env`` \\ simp[]) \\
+    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 \\
   simp [delta_0_deterministic] \\
   inversion `eval_exp machineEpsilon _ _ _ _` eval_exp_cases \\ rveq \\
@@ -74,7 +74,7 @@ val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant"
   rename1 `abs deltaF <= machineEpsilon` \\
   simp [Rabs_err_simpl, ABS_MUL] \\
   match_mp_tac REAL_LE_TRANS \\
-  exists_tac ``maxAbsFun (nlo, nhi) * machineEpsilon`` \\ conj_tac \\ TRY (simp[]) \\
+  qexists_tac `maxAbsFun (nlo, nhi) * machineEpsilon` \\ conj_tac \\ TRY (simp[]) \\
   match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS]) \\
   simp[maxAbsFun_def] \\
   match_mp_tac maxAbs \\
@@ -82,4 +82,33 @@ val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant"
   qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2)) \\
   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 /\
+      validErrorbound (Param v) absenv /\
+      validIntervalbounds (Param v) absenv P /\
+      (absenv (Param v) = ((nlo,nhi),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 \\
+  simp [delta_0_deterministic] \\
+  inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\
+  simp [perturb_def] \\
+  rename1 `abs deltaF <= machineEpsilon` \\
+  simp [Rabs_err_simpl, ABS_MUL] \\
+  match_mp_tac REAL_LE_TRANS \\
+  qexists_tac `maxAbsFun (nlo, nhi) * machineEpsilon` \\
+  conj_tac \\ TRY (simp []) \\
+  match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp [ABS_POS]) \\
+  simp[maxAbsFun_def] \\
+  match_mp_tac maxAbs \\
+  qspecl_then [`delta`, `n`] (fn thm => fs [thm]) delta_0_deterministic);
+
 val _ = export_theory();