Port interval validation to new semantics

hol4/IntervalValidationScript.sml

@@ -69,8 +69,7 @@ val validIntervalboundsCmd_def = Define `
          then validIntervalboundsCmd g absenv P (Insert x validVars)
          else F
    | Ret e =>
-     (validIntervalbounds e absenv P validVars /\
-      (FST (absenv e) = FST (absenv (Var 0))))`;
+     (validIntervalbounds e absenv P validVars)`;
 
 val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecond_sound",
 ``!(f:real exp) (absenv:analysisResult) (P:precond) (V:num_set).
@@ -313,43 +312,71 @@ val getRetExp_def = Define `
      |Ret e => e`;
 
 val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
-  ``!f absenv E vR (fVars dVars outVars:num_set) elo ehi err P.
-      ssaPrg f ((domain fVars) UNION (domain dVars)) outVars /\
+  ``!f (absenv:analysisResult) E vR (fVars dVars outVars:num_set) elo ehi err P.
+      ssa f (union fVars dVars) outVars /\
       bstep f E 0 vR /\
       (!v. v IN (domain dVars) ==>
          ?vR.
            (E v = SOME vR) /\
-           (FST (FST (absenv (Var v))) <= VarEnv v /\
-            VarEnv v <= SND (FST (absenv (Var v))))) /\
-      ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
+           (FST (FST (absenv (Var v))) <= vR /\
+            vR <= SND (FST (absenv (Var v))))) /\
+       (!v. v IN (domain fVars) ==>
+          ?vR.
+            (E v = SOME vR) /\
+            (FST (P v)) <= vR /\ vR <= SND (P v)) /\
+      (((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
       validIntervalboundsCmd f absenv P dVars /\
       (absenv (getRetExp f) = ((elo, ehi), err)) ==>
-      elo <= vR /\ R <= ehi``,
-  gen_tac \\ Induct_on `f` \\
-  once_rewrite_tac [validIntervalboundsCmd_def] \\
-  rpt gen_tac \\ strip_tac
-  >- (inversion `ssaPrg _ _ _` ssaPrg_cases \\
-      inversion `bstep _  _ _ _ _ _ _` bstep_cases \\
-      fs [] \\
-      first_x_assum match_mp_tac \\
-      asm_exists_tac \\
-      qexistsl_tac [`absenv`, `updEnv n v VarEnv`, `ParamEnv`, `err`, `P`] \\
-      fs [updEnv_def] \\
-      gen_tac \\
-      Cases_on `v' = n` \\ strip_tac \\ fs[]
-      >- (Cases_on `absenv e` \\ Cases_on `absenv (Var n)` \\
-          drule validIntervalbounds_sound \\
-          disch_then (qspecl_then [`VarEnv`, `ParamEnv`, `v`] ASSUME_TAC) \\
-          qpat_x_assum `absenv e = _` (fn thm => fs[thm]) \\
-          qpat_x_assum `q = q'` (fn thm => fs [thm]))
-      >- (CCONTR_TAC \\
-          qpat_x_assum `v' = _` (fn thm => fs[thm])))
-  >- (inversion `ssaPrg _ _ _` ssaPrg_cases \\
-      inversion `bstep _  _ _ _ _ _ _` bstep_cases \\
-      fs [updEnv_def] \\
-      drule validIntervalbounds_sound \\
-      disch_then (qspecl_then [`VarEnv`, `ParamEnv`, `v`] ASSUME_TAC) \\
-      qpat_x_assum `FST (absenv e) = _` (fn thm => fs[thm]))
-  >- (CCONTR_TAC \\ fs[]));
+      elo <= vR /\ vR <= ehi``,
+  gen_tac \\ Induct_on `f`
+  \\ once_rewrite_tac [validIntervalboundsCmd_def]
+  \\ rpt gen_tac \\ strip_tac
+  >- (inversion `ssa _ _ _` ssa_cases
+      \\ inversion `bstep _  _ _ _` bstep_cases
+      \\ fs []
+      \\ first_x_assum match_mp_tac
+      \\ qexistsl_tac [`absenv`, `updEnv n v E`, `fVars`, `Insert n dVars`, `outVars`, `err`, `P`]
+      \\ fs [updEnv_def]
+      \\ rpt conj_tac
+      >- (match_mp_tac ssa_equal_set
+          \\ qexists_tac `(Insert n (union fVars dVars))`
+          \\ fs [domain_union, Insert_def, domain_insert]
+          \\ once_rewrite_tac [UNION_COMM]
+          \\ fs [INSERT_UNION_EQ, UNION_COMM])
+      >- (rpt strip_tac
+          \\ Cases_on `v' = n`
+          >- (rveq
+              \\ qexists_tac `v` \\ fs []
+              \\ rw_sym_asm `FST (absenv e) = _`
+              \\ match_mp_tac validIntervalbounds_sound
+              \\ qexistsl_tac [`P`, `fVars`, `dVars`, `E`] \\ fs [SUBSET_DEF]
+              \\ rpt strip_tac
+              \\ first_x_assum match_mp_tac \\ fs [Once freeVars_def, domain_union]
+              \\ metis_tac [])
+          >- (rw[]
+              \\ first_x_assum match_mp_tac
+              \\ fs [Insert_def, domain_insert]))
+      >- (rpt strip_tac
+          \\ Cases_on `v' = n` \\ fs[domain_union])
+      >- (fs [Insert_def, domain_insert, SUBSET_DEF]
+          \\ rpt strip_tac
+          \\ first_x_assum match_mp_tac
+          \\ once_rewrite_tac [freeVars_def, domain_union]
+          \\ fs [domain_union])
+      >- (fs [Once getRetExp_def]))
+  >- (inversion `ssa _ _ _` ssa_cases
+      \\ inversion `bstep _ _ _ _` bstep_cases
+      \\ fs [updEnv_def, getRetExp_def]
+      \\ drule validIntervalbounds_sound
+      \\ disch_then (qspecl_then [`fVars`, `E`, `vR`] ASSUME_TAC)
+      \\ qpat_x_assum `absenv _ = _` (fn thm => fs [thm])
+      \\ first_x_assum match_mp_tac
+      \\ fs [SUBSET_DEF]
+      \\ rpt strip_tac
+      \\ qpat_x_assum `domain (union fVars dVars) = _` (fn thm => fs [GSYM thm])
+      \\ specialize `!x'. x' IN domain (usedVars e) ==> _` `x`
+      \\ specialize `x IN domain (usedVars e) ==> _` `x IN domain (usedVars e)`
+      \\ fs [domain_union]
+      \\ CCONTR_TAC \\ metis_tac []));
 
 val _ = export_theory();