Move computing functions to new semantics

hol4/ErrorValidationScript.sml

@@ -15,48 +15,49 @@ open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
 val _ = new_theory "ErrorValidation";
 
 val validErrorbound_def = Define `
-validErrorbound e (absenv:analysisResult) =
-let (intv, err) = absenv e in
-    let errPos = 0 <= err in
-        case e of
-          | Var v => errPos
-          | Param v => (errPos /\ (maxAbsFun intv * machineEpsilon <= err))
-          | Const n => (errPos /\ (maxAbsFun intv * machineEpsilon <= err))
-          | Unop op f => F
-          | Binop op f1 f2 =>
-            let rec = (validErrorbound f1 absenv /\ validErrorbound f2 absenv) in
-            let (ive1, err1) = absenv f1 in
-            let (ive2, err2) = absenv f2 in
-            let errIve1 = widenInterval ive1 err1 in
-            let errIve2 = widenInterval ive2 err2 in
-            let upperBoundE1 = maxAbsFun ive1 in
-            let upperBoundE2 = maxAbsFun ive2 in
-            let theVal =
-                case op of
-                   | Plus => err1 + err2 + (maxAbsFun (addInterval errIve1 errIve2) * machineEpsilon) <= err
-                   | Sub => err1 + err2 + (maxAbsFun (subtractInterval errIve1 errIve2) * machineEpsilon) <= err
-                   | Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbsFun (multInterval errIve1 errIve2) * machineEpsilon) <= err
-                   | Div =>
-                     let upperBoundInvE2 = maxAbsFun (invertInterval ive2) in
-                     let nodiv0_fl = (IVhi errIve2 < 0 \/ 0 < IVlo errIve2) in
-                         if nodiv0_fl
-                         then let minAbsIve2 = minAbsFun (errIve2) in
-                              let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
-                                  (upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbsFun (divideInterval errIve1 errIve2) * machineEpsilon) <= err
-                         else F
-                                  in rec /\ errPos /\ theVal`;
+  validErrorbound e (absenv:analysisResult) (dVars:num_set)=
+    let (intv, err) = absenv e in
+      if (0 <= err)
+        then
+          case e of
+            | Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * machineEpsilon <= err)
+            | Const n => (maxAbs intv * machineEpsilon <= err)
+            | Unop op f => F
+            | Binop op f1 f2 =>
+              (if (validErrorbound f1 absenv dVars /\ validErrorbound f2 absenv dVars)
+                then
+                  let (ive1, err1) = absenv f1 in
+                  let (ive2, err2) = absenv f2 in
+                  let errIve1 = widenInterval ive1 err1 in
+                  let errIve2 = widenInterval ive2 err2 in
+                  let upperBoundE1 = maxAbs ive1 in
+                  let upperBoundE2 = maxAbs ive2 in
+                    case op of
+                      | Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * machineEpsilon) <= err
+                      | Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * machineEpsilon) <= err
+                      | Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * machineEpsilon) <= err
+                      | Div =>
+                        (if (IVhi errIve2 < 0 \/ 0 < IVlo errIve2)
+                          then
+                            let upperBoundInvE2 = maxAbs (invertInterval ive2) in
+                            let minAbsIve2 = minAbsFun (errIve2) in
+                            let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
+                              ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * machineEpsilon) <= err)
+                          else F)
+                  else F)
+        else F`;
 
 val validErrorboundCmd_def = Define `
-  validErrorboundCmd (f:real cmd) (env:analysisResult) =
-  case f of
-    | Let x e g  =>
-      validErrorbound e env /\
-      (env e = env (Var x)) /\
-      validErrorboundCmd g env
+  validErrorboundCmd (f:real cmd) (env:analysisResult) (dVars:num_set)=
+    case f of
+      | Let x e g  =>
+        if validErrorboundCmd g env (Insert x dVars)
+          then
+            (validErrorbound e env dVars/\
+            (env e = env (Var x)))
+          else F
     | Ret e =>
-      validErrorbound e env /\
-      (env e = env (Var 0))
-    | Nop => F`;
+      validErrorbound e env dVars`;
 
 val err_always_positive = store_thm ("err_always_positive",
   ``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real).