Prove error bound sound for constants

hol4/ErrorValidationScript.sml

@@ -47,25 +47,39 @@ let (intv, err) = absenv e in
                                   in rec /\ errPos /\ theVal`;
 
 val err_always_positive = store_thm ("err_always_positive",
-``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real).
+  ``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real).
     (validErrorbound (e:real exp) (absenv:analysisResult)) /\ ((iv,err) = absenv e) ==>
       0 <= err``,
-once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
-Cases_on `e` \\
-qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm]) \\
-Cases_on `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
+  once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
+  Cases_on `e` \\
+  qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm]) \\
+  Cases_on `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
 
-(**
 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 /\
-    validErrorbound (Const n) absenv /\
-    validIntervalbounds (Const n) absenv P /\
-    (absenv (Const n) = ((nlo,nhi),e)) ==>
-    (abs (nR - nF)) <= e`,
-``,
-)
-**)
+  ``!(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 /\
+      validErrorbound (Const n) absenv /\
+      validIntervalbounds (Const n) absenv P /\
+      (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 \\ exists_tac ``P:precond`` \\ exists_tac ``cenv:env`` \\ 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 \\
+  simp[perturb_def] \\
+  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[]) \\
+  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 \\
+  qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2)) \\
+  simp[]);
 
 val _ = export_theory();

hol4/IntervalValidationScript.sml

@@ -11,7 +11,7 @@ open abbrevsTheory expressionsTheory RealSimpsTheory
 open ExpressionAbbrevsTheory IntervalArithTheory
 
 val _ = new_theory "IntervalValidation";
-                             
+ 
 val freeVars_def = Define `
 (freeVars (Const n) = []) /\
 (freeVars (Var v) = []) /\