Add validator functions, currently unproven

hol/ErrorValidation.hl

+needs "Expressions.hl";;
+needs "IntervalArith.hl";;
+
+let maxAbs = define
+  `maxAbs (iv:real#real) = max (abs (FST iv)) (abs (SND iv))`;;
+
+let validErrorbound = define
+  `(validErrorbound (Const n) (absenv:(real)exp->(real#real)#real) =
+      let (intv, err) = absenv (Const n) in
+        (maxAbs intv * machineEpsilon) <= err) /\
+  (validErrorbound (Param v) (absenv:(real)exp->(real#real)#real) =
+      let (intv, err) = absenv (Param v) in
+        (maxAbs intv * machineEpsilon) <= err ) /\
+  (validErrorbound (Binop b e1 e2) (absenv:(real)exp->(real#real)#real) =
+      let (intv, err) = absenv (Binop b e1 e2) in
+      let (ive1, err1) = absenv e1 in
+      let (ive2, err2) = absenv e2 in
+      let upperBoundE1 = maxAbs ive1 in
+      let upperBoundE2 = maxAbs ive2 in
+      let e1F = upperBoundE1 + err1 in
+      let e2F = upperBoundE2 + err2 in
+        if (b = Plus \/ b = Sub)
+        then (err1 + err2 + (abs e1F + abs e2F) * machineEpsilon) <= err
+        else
+          if b = Mult
+          then (abs (upperBoundE1 * upperBoundE2 - (e1F * e2F)) + abs (e1F * e2F) * machineEpsilon) <= err
+          else F)`;;

hol/IntervalArith.hl

@@ -161,14 +161,14 @@ let interval_add_valid =
         THEN right THEN right THEN right
         THEN REWRITE_TAC[REAL_LE_REFL]]);;
 
-let substractInterval = define
-  `substractInterval I1 I2 = addInterval I1 (negateInterval I2)`;;
+let subtractInterval = define
+  `subtractInterval I1 I2 = addInterval I1 (negateInterval I2)`;;
 
-let interval_substraction_valid =
+let interval_subtraction_valid =
   prove (
     `!(iv1:interval) (iv2:interval).
-      validIntervalSub iv1 iv2 (substractInterval iv1 iv2)`,
-    SIMP_TAC[validIntervalSub; substractInterval; contained; absIntvUpd]
+      validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)`,
+    SIMP_TAC[validIntervalSub; subtractInterval; contained; absIntvUpd]
       THEN intros "!iv1 iv2 a b; contained_a lo_leq_b b_leq_hi"
     THEN destruct "contained_a" "lo_leq_a a_leq_hi"
       THEN ASM_REWRITE_TAC [Rsub_eq_Ropp_Rplus]
@@ -213,12 +213,18 @@ e (LABEL_TAC "cases_a" (SPECL [`a:real`; `&0:real`] REAL_LTE_TOTAL));;
 e (destruct "cases_a" "a_lt_0 | 0_leq_a");;
 e (LABEL_TAC "cases_hi2" (SPECL [`(SND I2):real`; `&0:real`] REAL_LTE_TOTAL));;
 e (destruct "cases_hi2" "hi2_lt_0 | 0_leq_hi2");;
-e (MATCH_MP_TAC REAL_MULT_LE);;
+(*
+  TODO FIXME!
+ e (MATCH_MP_TAC REAL_MULT_LE);;
 search [`(x:real)*y <= w* z`];;
 
 search [`(<=):real->real->bool`];;
-
+*)
+e (CHEAT_TAC);;
+e (CHEAT_TAC);;
+e (CHEAT_TAC);;
+e (CHEAT_TAC);;
 
 let intv_div_err = define
-  `intv_div_err (I1:intv) (e1:err) (I2:intv) (e2:err)=
+  `intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err)=
   intv_mult_err I1 e1 ((&1) / IVlo (I2), (&1) / IVhi (I2)) e2`;;

hol/IntervalValidation.hl

+
+needs "Expressions.hl";;
+needs "IntervalArith.hl";;
+
+let validIntervalBounds = define
+  `(validIntervalBounds (Const n) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
+      (FST (FST (absenv (Const n))) <= n /\ n <= SND (FST (absenv (Const n))))) /\
+  (validIntervalBounds (Param v) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
+      (FST (P v) = FST (FST (absenv (Param v))) /\ (SND (P v) = SND (FST (absenv (Param v)))))) /\
+  (validIntervalBounds (Binop Plus e1 e2) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
+      (validIntervalBounds e1 absenv P /\
+         validIntervalBounds e2 absenv P /\
+         isSupersetInterval (addInterval (FST (absenv e1)) (FST (absenv e2))) (FST (absenv (Binop Plus e1 e2))))) /\
+  (validIntervalBounds (Binop Sub e1 e2) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
+      (validIntervalBounds e1 absenv P /\
+         validIntervalBounds e2 absenv P /\
+      isSupersetInterval (subtractInterval (FST (absenv e1)) (FST (absenv e2))) (FST (absenv (Binop Sub e1 e2))))) /\
+  (validIntervalBounds (Binop Mult e1 e2) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) =
+      (validIntervalBounds e1 absenv P /\
+         validIntervalBounds e2 absenv P /\
+         isSupersetInterval (multInterval (FST (absenv e1)) (FST (absenv e2))) (FST (absenv (Binop Mult e1 e2))))) /\
+  (validIntervalBounds (Binop Div e1 e2) (absenv:(real)exp->(real#real)#real) (P:num->(real#real)) = F)`;;