IntervalValidationScript.sml 41.1 KB
Newer Older
1 2 3 4 5 6 7 8
(**
    Interval arithmetic checker and its soundness proof.
    The function validIntervalbounds checks wether the given analysis result is
    a valid range arithmetic for each sub term of the given expression e.
    The computation is done using our formalized interval arithmetic.
    The function is used in CertificateChecker.v to build the full checker.
**)
open preamble
9 10
open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
11
open ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory MachineTypeTheory
12
open sptreeLib sptreeTheory
13

14
val _ = new_theory "IntervalValidation";
15

16
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
17 18 19
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
20

21
val validIntervalbounds_def = Define `
22 23 24
  validIntervalbounds f (absenv:analysisResult) (P:precond) (validVars:num_set) =
    let (intv, _) = absenv f in
      case f of
25
        | Var v =>
26 27 28
          if (lookup v validVars = SOME ())
          then T
          else (isSupersetInterval (P v) intv /\ IVlo (P v) <= IVhi (P v))
29
        | Const m n => isSupersetInterval (n,n) intv
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
        | Unop op f1 =>
          let (iv, _) = absenv f1 in
              (if validIntervalbounds f1 absenv P validVars
               then
                   case op of
                      | Neg =>
                        let new_iv = negateInterval iv in
                            isSupersetInterval new_iv intv
                      | Inv =>
                        if IVhi iv < 0 \/ 0 < IVlo iv
                        then
                            let new_iv = invertInterval iv in
                                isSupersetInterval new_iv intv
                        else
                            F
45
            else F)
46 47 48 49 50
        | Downcast m f1 =>
          (let (iv1, _) = absenv f1 in
              if (validIntervalbounds f1 absenv P validVars) then
                  ((isSupersetInterval intv iv1) /\ (isSupersetInterval iv1 intv))
              else F)
51 52 53 54 55 56 57 58 59 60 61 62 63
        | Binop op f1 f2 =>
          (if (validIntervalbounds f1 absenv P validVars /\ validIntervalbounds f2 absenv P validVars)
            then
              let (iv1, _ ) = absenv f1 in
              let (iv2, _) = absenv f2 in
                case op of
                  | Plus =>
                    let new_iv = addInterval iv1 iv2 in
                      isSupersetInterval new_iv intv
                  | Sub =>
                    let new_iv = subtractInterval iv1 iv2 in
                      isSupersetInterval new_iv intv
                  | Mult =>
64
                     let new_iv = multInterval iv1 iv2 in
65 66
                       isSupersetInterval new_iv intv
                  | Div =>
67
                     if (IVhi iv2 < 0 \/ 0 < IVlo iv2)
68
                       then
69
                         let new_iv = divideInterval iv1 iv2 in
70 71
                           isSupersetInterval new_iv intv
                       else F
72 73 74 75 76 77 78 79 80 81 82 83
            else F)
        | Fma f1 f2 f3 =>
          (if (validIntervalbounds f1 absenv P validVars /\
               validIntervalbounds f2 absenv P validVars /\
               validIntervalbounds f3 absenv P validVars)
            then
              let (iv1, _ ) = absenv f1 in
              let (iv2, _) = absenv f2 in
              let (iv3, _) = absenv f3 in
              let new_iv = addInterval iv1 (multInterval iv2 iv3) in
              isSupersetInterval new_iv intv
           else F)`;
84 85

val validIntervalboundsCmd_def = Define `
86
  validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num_set) =
87
    case f of
88
     | Let m x e g =>
89 90
       if (validIntervalbounds e absenv P validVars /\
          (FST (absenv e) = FST (absenv (Var x))))
91
         then validIntervalboundsCmd g absenv P (insert x () validVars)
92
         else F
93
   | Ret e =>
94
     (validIntervalbounds e absenv P validVars)`;
95

96
val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecond_sound",
97
``!(f:real exp) (absenv:analysisResult) (P:precond) (V:num_set).
98
   validIntervalbounds f absenv P V ==>
99 100 101 102 103 104 105 106 107 108
   (!(v:num). v IN ((domain (usedVars f)) DIFF (domain V)) ==>
           isSupersetInterval (P v) (FST (absenv (Var v))))``,
  Induct_on `f` \\ once_rewrite_tac [usedVars_def] \\ rpt strip_tac \\ fs[]
  >- (rule_assum_tac (ONCE_REWRITE_RULE [validIntervalbounds_def])
      \\ fs [domain_lookup, usedVars_def, lookup_insert]
      \\ `v = n` by (Cases_on `v = n` \\ fs[lookup_def])
      \\ rveq
      \\ Cases_on `absenv (Var n)`
      \\ Cases_on `lookup n V`
      \\ fs[])
109 110 111
  >- (rpt (
        first_x_assum
          (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
112
      \\ `validIntervalbounds f absenv P V`
113 114 115 116 117 118 119 120 121
           by ( Cases_on `absenv (Unop u f)` \\ Cases_on `absenv f` \\ fs [Once validIntervalbounds_def])
      \\ fs [])
  >- (rpt (
        first_x_assum
          (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
      \\ rename1 `Binop b f1 f2`
      \\ `validIntervalbounds f1 absenv P V /\ validIntervalbounds f2 absenv P V`
           by (Cases_on `absenv (Binop b f1 f2)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ fs [Once validIntervalbounds_def])
      \\ fs [domain_union])
122 123 124 125 126 127 128
  >- (rpt (
        first_x_assum
          (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
      \\ rename1 `Fma f1 f2 f3`
      \\ `validIntervalbounds f1 absenv P V /\ validIntervalbounds f2 absenv P V /\ validIntervalbounds f3 absenv P V`
           by (Cases_on `absenv (Fma f1 f2 f3)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` \\ fs [Once validIntervalbounds_def])
      \\ fs [domain_union])
129 130 131
  >- (rpt (
        first_x_assum
          (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
132
      \\ `validIntervalbounds f absenv P V`
133 134
           by (Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f` \\ fs [Once validIntervalbounds_def])
      \\ fs []));
135 136

val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
137
  ``!(f:real exp) (absenv:analysisResult) (P:precond) (fVars:num_set) (dVars:num_set) E Gamma.
138 139
       validIntervalbounds f absenv P dVars /\ (* The checker succeeded *)
       (* All defined vars have already been analyzed *)
140 141 142
       (!v. v IN (domain dVars) ==>
         (?vR. (E v = SOME vR) /\
         (FST (FST (absenv (Var v))) <= vR /\ vR <= SND (FST (absenv (Var v)))))) /\
143
       (* The variables in term f without the the defined variable set are a subset of the free variables *)
144
       (((domain (usedVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
145 146
       (* All free variables are defined in the execution environment and
          the values respect the precondition *)
147 148
       (!v. v IN (domain fVars) ==>
         (?vR. (E v = SOME vR) /\
149 150 151 152
         (FST (P v) <= vR /\ vR <= SND (P v)))) /\
       (* All variables that are either free or defined have a type *)
       (!v. v IN ((domain fVars) UNION (domain dVars)) ==>
          ?m. Gamma v = SOME m) ==>
Heiko Becker's avatar
Heiko Becker committed
153
       ? vR.
154
         eval_exp E (toRMap Gamma) (toREval f) vR M0 /\
Heiko Becker's avatar
Heiko Becker committed
155 156
         (FST (FST (absenv f))) <= vR /\ vR <= (SND (FST (absenv f)))``,
  Induct_on `f` \\ once_rewrite_tac [toREval_def,eval_exp_cases] \\ rpt strip_tac
157 158 159 160 161 162 163 164
  (* Variable case *)
  >- (rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
      \\ Cases_on `absenv (Var n)` \\ Cases_on `lookup n dVars` \\ fs[]
      >- (specialize `!v. v IN domain fVars ==> _` `n`
          \\ fs [usedVars_def]
          \\ `~ (n IN (domain dVars))` by (fs[domain_lookup])
          \\ `n IN domain fVars` by fs[]
          \\ fs [isSupersetInterval_def, IVlo_def, IVhi_def]
165 166 167 168
          \\ `?m. Gamma n = SOME m`
               by (first_x_assum match_mp_tac \\fs [])
          \\ `eval_exp E (toRMap Gamma) (toREval (Var n)) vR M0`
               by (fs[toREval_def] \\ match_mp_tac Var_load \\ fs[toRMap_def])
Heiko Becker's avatar
WIP  
Heiko Becker committed
169
          \\ qexists_tac `vR` \\ fs [toREval_def]
170
	  \\ fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ fs [] \\ rveq
171
          \\ conj_tac
172 173
          >- (match_mp_tac REAL_LE_TRANS
              \\ asm_exists_tac
174
              \\ fs [] \\ rveq \\ simp[])
175 176 177
          >- (match_mp_tac REAL_LE_TRANS
              \\ qexists_tac `SND (P n)`
              \\ fs [] \\ rveq \\ simp []))
178 179
      >- (specialize `!v. v IN domain dVars ==> _` `n`
          \\ `n IN domain dVars` by (fs [domain_lookup])
180 181 182 183 184 185
          \\ `?m. Gamma n = SOME m` by (first_x_assum match_mp_tac \\ fs[])
          \\ fs[]
          \\ `eval_exp E (toRMap Gamma) (toREval (Var n)) vR M0`
               by (fs [toREval_def] \\ match_mp_tac Var_load \\ fs[toRMap_def])
          \\ qexists_tac `vR` \\ fs[]
          \\ qpat_x_assum `absenv (Var n) = _` (fn thm => fs[thm, toREval_def])))
186
  (* Const case *)
187 188
  >- (Cases_on `absenv (Const m v)`
      \\ fs []
189 190 191
      \\ `eval_exp E (toRMap Gamma) (toREval (Const m v)) v M0`
           by (fs [toREval_def] \\ match_mp_tac Const_dist'
               \\ fs[mTypeToQ_def]
Heiko Becker's avatar
Heiko Becker committed
192
               \\ fs[perturb_def])
193 194 195 196
      \\ qexists_tac `v`
      \\ fs [mTypeToQ_def]
      \\ fs [validIntervalbounds_def, isSupersetInterval_def, IVhi_def, IVlo_def, toREval_def])
  (* Unary operator case *)
197
  >- (simp[evalUnop_def]
198 199 200 201 202 203 204 205 206 207 208 209
      \\ fs []
      \\ `?v. eval_exp E (toRMap Gamma) (toREval f) v M0 /\ FST (FST (absenv f)) <= v /\ v <= SND (FST (absenv f))`
           by (first_x_assum match_mp_tac
               \\ qexistsl_tac [`P`, `fVars`, `dVars`]
               \\ fs []
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `absenv (Unop u f)` \\ Cases_on `absenv f` \\ fs[Once usedVars_def]
               \\ rpt strip_tac \\ first_x_assum match_mp_tac \\ fs[])
      \\ Cases_on `u`
      >- (rw_thm_asm `validIntervalbounds (Unop Neg f) absenv P dVars` validIntervalbounds_def
          \\ Cases_on `absenv (Unop Neg f)`
          \\ qmatch_assum_rename_tac `absenv (Unop Neg f) = (iv_u, err_u)`
210 211 212 213
          \\ Cases_on `absenv f`
          \\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
          \\ rveq
          \\ fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, negateInterval_def]
214
          \\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`,`v1`] assume_tac thm)
215
          \\ qpat_x_assum `absenv f = _` (fn thm => fs[thm])
216 217 218 219 220
          \\ `eval_exp E (toRMap Gamma) (Unop Neg (toREval f)) (evalUnop Neg v) M0`
               by (fs[] \\ match_mp_tac Unop_neg'
                   \\ qexistsl_tac [`M0`, `v`] \\ fs[])
          \\ qexists_tac `(evalUnop Neg v)` \\ fs[]
          \\ fs[evalUnop_def, Once toREval_def] \\ conj_tac \\ match_mp_tac REAL_LE_TRANS
221 222 223
             >- (qexists_tac `- SND iv_f` \\ conj_tac \\ simp [])
             >- (qexists_tac `- FST iv_f` \\ conj_tac \\ simp []))
          (* Inversion case *)
224 225 226 227 228 229 230 231 232 233 234 235 236
      >- (`eval_exp E (toRMap Gamma) (Unop Inv (toREval f)) (evalUnop Inv v) M0`
            by (fs[]
                \\ match_mp_tac Unop_inv'
                \\ qexistsl_tac [`M0`, `v`,`0`] \\ fs[mTypeToQ_def, perturb_def, evalUnop_def]
                \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
                \\ Cases_on `absenv (Unop Inv f)` \\ Cases_on `absenv f` \\ fs[IVhi_def, IVlo_def]
                \\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
                \\ CCONTR_TAC \\ fs[] \\ rveq
                >- (`0 < 0:real` by (match_mp_tac REAL_LET_TRANS \\ qexists_tac `SND iv_f` \\ fs[]) \\ fs[] )
                >- (`0 < 0:real` by (match_mp_tac REAL_LTE_TRANS \\ qexists_tac `FST iv_f` \\fs[]) \\ fs[]))
          \\ qexists_tac `evalUnop Inv v` \\ fs []
          \\ fs [mTypeToQ_def]
          \\ simp[evalUnop_def]
237
          \\ rw_thm_asm `validIntervalbounds a b c d` validIntervalbounds_def
238 239 240
          \\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`, `Gamma`] assume_tac thm)
          \\ Cases_on `absenv (Unop Inv f)`
          \\ qmatch_assum_rename_tac `absenv (Unop Inv f) = (iv_u, err_u)`
241 242 243 244
          \\ Cases_on `absenv f`
          \\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
          \\ rveq
          \\ rpt (qpat_x_assum `!v. _ ==> _` kall_tac)
245
          \\ rpt (qpat_x_assum `validIntervalbounds f absenv P dVars /\ _ /\ _ /\ _ /\ _ ==> _` kall_tac)
246 247 248 249
          \\ conj_tac \\ match_mp_tac REAL_LE_TRANS
             >- (qexists_tac `inv (SND iv_f)` \\ conj_tac
                 \\ TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
                >- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
250 251 252 253
                    \\ `0 < -v` by REAL_ASM_ARITH_TAC
                    \\ `-SND iv_f <= -v` by REAL_ASM_ARITH_TAC
                    \\ `inv (-v) <= inv (- SND iv_f)` by fs[REAL_INV_LE_ANTIMONO]
                    \\ `inv(-v) = - (inv v)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
254
                    \\ `inv(-(SND iv_f)) = - (inv (SND iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
255
                    \\ `-(inv v) <= - (inv (SND iv_f))` by fs []
256
                    \\ fs[])
257
                >- (`0 < v` by REAL_ASM_ARITH_TAC \\
258 259 260 261 262
                    `0 < SND iv_f` by REAL_ASM_ARITH_TAC \\
                    fs[REAL_INV_LE_ANTIMONO]))
             >- (qexists_tac `inv (FST iv_f)` \\ conj_tac
                 \\  TRY(fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER])
                >- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC
263
                    \\ `0 < -v` by REAL_ASM_ARITH_TAC
264
                    \\ `0 < - (FST iv_f)` by REAL_ASM_ARITH_TAC
265 266
                    \\ `- v <= - (FST iv_f)` by REAL_ASM_ARITH_TAC
                    \\ `inv (- FST iv_f) <= inv (- v)` by fs[REAL_INV_LE_ANTIMONO]
267
                    \\ `inv(- FST iv_f) = - (inv (FST iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
268 269
                        \\ `inv(- v) = - (inv v)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
                    \\ `-(inv (FST iv_f)) <= - (inv v)` by fs []
270
                    \\ fs[])
271
                >- (`0 < v` by REAL_ASM_ARITH_TAC \\
272 273
                    `0 < FST iv_f` by REAL_ASM_ARITH_TAC \\
                    fs[REAL_INV_LE_ANTIMONO]))))
274
  (* Binary operator case *)
275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306
  >- (rename1 `Binop b f1 f2`
      \\ `?v1. eval_exp E (toRMap Gamma) (toREval f1) v1 M0 /\
               (FST (FST (absenv f1))) <= v1 /\ (v1 <= SND (FST (absenv f1)))`
           by (first_x_assum match_mp_tac
               \\ qexistsl_tac [`P`, `fVars`, `dVars`]
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `absenv (Binop b f1 f2)`
               \\ Cases_on `absenv f1` \\ Cases_on `absenv f2`
               \\ fs []
               \\ conj_tac
               \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac
               \\ first_x_assum match_mp_tac \\ fs[]
               \\ DISJ1_TAC
               \\ simp[Once usedVars_def])
      \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f1) _ _ /\ _ /\ _` kall_tac
      \\ `?v2. eval_exp E (toRMap Gamma) (toREval f2) v2 M0 /\
               (FST (FST (absenv f2))) <= v2 /\ (v2 <= SND (FST (absenv f2)))`
           by (first_x_assum match_mp_tac
               \\ qexistsl_tac [`P`, `fVars`, `dVars`]
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `absenv (Binop b f1 f2)`
               \\ Cases_on `absenv f1` \\ Cases_on `absenv f2`
               \\ fs []
               \\ conj_tac \\ fs []
               \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac
               \\ first_x_assum match_mp_tac \\ fs[]
               \\ DISJ2_TAC
               \\ simp[Once usedVars_def])
      \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f2) _ _ /\ _ /\ _` kall_tac
      \\ fs []
307
      \\ rw_thm_asm `validIntervalbounds (Binop b f f') absenv P V` validIntervalbounds_def
308 309 310 311 312
      \\ Cases_on `absenv (Binop b f1 f2)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2`
      \\ qmatch_assum_rename_tac `absenv (Binop b f1 f2) = (iv_b,err_b)`
      \\ qmatch_assum_rename_tac `absenv f1 = (iv_f,err_f)`
      \\ qmatch_assum_rename_tac `absenv f2 = (iv_f',err_f')`
      \\ qexists_tac `evalBinop b v1 v2`
313
      \\ Cases_on `b` \\ simp[evalBinop_def]
314
     (* Plus case *)
315
     >- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, addInterval_def]
316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
         \\ qspecl_then [`iv_f`, `iv_f'`, `v1`, `v2`]
              assume_tac
              (REWRITE_RULE
                   [validIntervalAdd_def,
                    addInterval_def,
                    absIntvUpd_def,
                    contained_def,
                    IVhi_def, IVlo_def] interval_addition_valid)
         \\ rpt conj_tac
         >- (match_mp_tac Binop_dist'
             \\ qexistsl_tac [`M0`, `M0`, `v1`, `v2`, `0:real`]
             \\ fs [mTypeToQ_def, perturb_def, evalBinop_def, join_def])
         >- (match_mp_tac REAL_LE_TRANS
             \\ qexists_tac `min4 (FST iv_f + FST iv_f')
                                  (FST iv_f + SND iv_f')
                                  (SND iv_f + FST iv_f')
                                  (SND iv_f + SND iv_f')`
             \\ metis_tac[])
        >- (match_mp_tac REAL_LE_TRANS
            \\ qexists_tac `max4 (FST iv_f + FST iv_f')
                                 (FST iv_f + SND iv_f')
                                 (SND iv_f + FST iv_f')
                                 (SND iv_f + SND iv_f')`
339
            \\metis_tac []))
340
     (* Sub case *)
341
     >- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, subtractInterval_def, addInterval_def, negateInterval_def]
342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368
         \\ qspecl_then [`iv_f`, `iv_f'`, `v1`, `v2`]
              assume_tac
              (REWRITE_RULE
                   [validIntervalSub_def,
                    subtractInterval_def,
                    addInterval_def,
                    negateInterval_def,
                    absIntvUpd_def,
                    contained_def,
                    IVhi_def,
                    IVlo_def] interval_subtraction_valid)
         \\ rpt conj_tac
         >- (match_mp_tac Binop_dist'
             \\ qexistsl_tac [`M0`, `M0`, `v1`, `v2`, `0:real`]
             \\ fs[mTypeToQ_def, perturb_def, evalBinop_def, join_def])
         >- (match_mp_tac REAL_LE_TRANS
             \\ qexists_tac `min4 (FST iv_f + -SND iv_f')
                                  (FST iv_f + -FST iv_f')
                                  (SND iv_f + -SND iv_f')
                                  (SND iv_f + -FST iv_f')`
             \\ metis_tac [])
        >- (match_mp_tac REAL_LE_TRANS
            \\ qexists_tac `max4 (FST iv_f + -SND iv_f')
                                 (FST iv_f + -FST iv_f')
                                 (SND iv_f + -SND iv_f')
                                 (SND iv_f + -FST iv_f')`
            \\ metis_tac []))
369
     (* Mult case *)
370
     >- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def]
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394
         \\ qspecl_then [`iv_f`, `iv_f'`, `v1`, `v2`]
            assume_tac
            (REWRITE_RULE
                 [validIntervalAdd_def,
                  multInterval_def,
                  absIntvUpd_def,
                  contained_def,
                  IVhi_def,
                  IVlo_def] interval_multiplication_valid)
         \\ rpt conj_tac
         >- (match_mp_tac Binop_dist'
             \\ qexistsl_tac [`M0`, `M0`, `v1`, `v2`, `0:real`]
             \\ fs[mTypeToQ_def, perturb_def, evalBinop_def, join_def])
         >- (match_mp_tac REAL_LE_TRANS
             \\ qexists_tac `min4 (FST iv_f * FST iv_f')
                                  (FST iv_f * SND iv_f')
                                  (SND iv_f * FST iv_f')
                                  (SND iv_f * SND iv_f')`
              \\ metis_tac [])
         >- (match_mp_tac REAL_LE_TRANS
             \\ qexists_tac `max4 (FST iv_f * FST iv_f')
                                  (FST iv_f * SND iv_f')
                                  (SND iv_f * FST iv_f')
                                  (SND iv_f * SND iv_f')`
395
            \\ metis_tac []))
396
     (* Div case *)
397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420
     >- (qspecl_then [`iv_f`, `iv_f'`, `v1`, `v2`]
                     assume_tac
                     (REWRITE_RULE
                          [validIntervalSub_def,
                           divideInterval_def,
                           multInterval_def,
                           invertInterval_def,
                           absIntvUpd_def,
                           contained_def,
                           IVhi_def,
                           IVlo_def,
                           GSYM REAL_INV_1OVER] interval_division_valid)
         \\ conj_tac
         >- (match_mp_tac Binop_dist'
             \\ qexistsl_tac [`M0`,`M0`,`v1`,`v2`,`0:real`]
             \\ fs[mTypeToQ_def, perturb_def, evalBinop_def, join_def]
             \\ CCONTR_TAC \\ fs[IVhi_def, IVlo_def]
             >- ( `0 < 0:real` suffices_by (fs [])
                  \\ match_mp_tac REAL_LET_TRANS
                  \\ qexists_tac `SND iv_f'`
                  \\ fs[] )
             >- ( `0 < 0:real` suffices_by (fs[])
                  \\ match_mp_tac REAL_LTE_TRANS
                  \\ qexists_tac `FST iv_f'`
421
                  \\ fs[]))
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444
         >- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def,
                IVhi_def, divideInterval_def, multInterval_def,
                invertInterval_def, GSYM REAL_INV_1OVER]
             \\ rpt conj_tac \\ match_mp_tac REAL_LE_TRANS
             >- (qexists_tac `min4 (FST iv_f * (inv (SND iv_f')))
                                   (FST iv_f * (inv (FST iv_f')))
                                   (SND iv_f * (inv (SND iv_f')))
                                   (SND iv_f * (inv (FST iv_f')))`
                 \\ metis_tac [])
             >- (qexists_tac `max4 (FST iv_f * (inv (SND iv_f')))
                                   (FST iv_f * (inv (FST iv_f')))
                                   (SND iv_f * (inv (SND iv_f')))
                                   (SND iv_f * (inv (FST iv_f')))`
                 \\ metis_tac [])
             >- (qexists_tac `min4 (FST iv_f * (inv (SND iv_f')))
                                   (FST iv_f * (inv (FST iv_f')))
                                   (SND iv_f * (inv (SND iv_f')))
                                   (SND iv_f * (inv (FST iv_f')))`
                 \\ metis_tac [])
             >- (qexists_tac `max4 (FST iv_f * (inv (SND iv_f')))
                                   (FST iv_f * (inv (FST iv_f')))
                                   (SND iv_f * (inv (SND iv_f')))
                                   (SND iv_f * (inv (FST iv_f')))`
445
                 \\ metis_tac []))))
446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493
  (* FMA case *)
  >- (rename1 `Fma f1 f2 f3`
      \\ `?v1. eval_exp E (toRMap Gamma) (toREval f1) v1 M0 /\
               (FST (FST (absenv f1))) <= v1 /\ (v1 <= SND (FST (absenv f1)))`
           by (first_x_assum match_mp_tac
               \\ qexistsl_tac [`P`, `fVars`, `dVars`]
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `absenv (Fma f1 f2 f3)`
               \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
               \\ fs []
               \\ conj_tac
               \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac
               \\ first_x_assum match_mp_tac \\ fs[]
               \\ DISJ1_TAC
               \\ simp[Once usedVars_def])
      \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f1) _ _ /\ _ /\ _` kall_tac
      \\ `?v2. eval_exp E (toRMap Gamma) (toREval f2) v2 M0 /\
               (FST (FST (absenv f2))) <= v2 /\ (v2 <= SND (FST (absenv f2)))`
           by (first_x_assum match_mp_tac
               \\ qexistsl_tac [`P`, `fVars`, `dVars`]
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `absenv (Fma f1 f2 f3)`
               \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
               \\ fs []
               \\ conj_tac \\ fs []
               \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac
               \\ first_x_assum match_mp_tac \\ fs[]
               \\ DISJ2_TAC
               \\ simp[Once usedVars_def])
      \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f2) _ _ /\ _ /\ _` kall_tac
      \\ `?v3. eval_exp E (toRMap Gamma) (toREval f3) v3 M0 /\
               (FST (FST (absenv f3))) <= v3 /\ (v3 <= SND (FST (absenv f3)))`
           by (first_x_assum match_mp_tac
               \\ qexistsl_tac [`P`, `fVars`, `dVars`]
               \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
               \\ Cases_on `absenv (Fma f1 f2 f3)`
               \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
               \\ fs []
               \\ conj_tac \\ fs []
               \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
               \\ rpt strip_tac
               \\ first_x_assum match_mp_tac \\ fs[]
               \\ DISJ2_TAC \\ DISJ2_TAC
               \\ simp[Once usedVars_def])
      \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f3) _ _ /\ _ /\ _` kall_tac
      \\ fs []
494
      \\ rw_thm_asm `validIntervalbounds (Fma f1 f2 f3) absenv P V` validIntervalbounds_def
495 496
      \\ Cases_on `absenv (Fma f1 f2 f3)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
      \\ qmatch_assum_rename_tac `absenv (Fma f1 f2 f3) = (iv_b,err_b)`
497 498 499
      \\ qmatch_assum_rename_tac `absenv f1 = (iv_f1,err_f1)`
      \\ qmatch_assum_rename_tac `absenv f2 = (iv_f2,err_f2)`
      \\ qmatch_assum_rename_tac `absenv f3 = (iv_f3,err_f3)`
500 501
      \\ qexists_tac `evalFma v1 v2 v3`
      \\ fs[evalFma_def, evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def, addInterval_def]
502
      \\ qspecl_then [`iv_f2`, `iv_f3`, `v2`, `v3`]
503 504 505 506 507 508 509 510
         assume_tac
         (REWRITE_RULE
              [validIntervalAdd_def,
               multInterval_def,
               absIntvUpd_def,
               contained_def,
               IVhi_def,
               IVlo_def] interval_multiplication_valid)
511
      \\ qspecl_then [`iv_f1`, `multInterval iv_f2 iv_f3`, `v1`, `v2 * v3`]
512 513 514 515
          assume_tac
          (REWRITE_RULE
              [validIntervalAdd_def,
                  addInterval_def,
516
                  multInterval_def,
517 518 519
                  absIntvUpd_def,
                  contained_def,
                  IVhi_def, IVlo_def] interval_addition_valid)
520
      \\ fs[multInterval_def, absIntvUpd_def, IVlo_def, IVhi_def] \\ res_tac
521 522 523 524 525
      \\ rpt conj_tac
      >- (match_mp_tac Fma_dist'
          \\ qexistsl_tac [`M0`, `M0`, `M0`, `v1`, `v2`, `v3`, `0:real`]
          \\ fs [mTypeToQ_def, perturb_def, evalFma_def, evalBinop_def, join3_def, join_def])
      >- (match_mp_tac REAL_LE_TRANS
526 527
          \\ asm_exists_tac
          \\ conj_tac \\ fs[])
528
      >- (match_mp_tac REAL_LE_TRANS
529 530 531 532 533 534 535 536 537 538 539 540 541 542
          \\ qexists_tac `max4
            (FST iv_f1 +
            min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
                (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
            (FST iv_f1 +
            max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
                (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
            (SND iv_f1 +
            min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
                (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
            (SND iv_f1 +
            max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
                (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))`
          \\conj_tac \\ fs[]))
543
  (* Downcast case *)
544 545 546 547 548 549 550 551 552 553 554
  >- (`?v. eval_exp E (toRMap Gamma) (toREval f) v M0 /\
           FST(FST(absenv f)) <= v /\ v <= SND (FST(absenv f))`
        by (first_x_assum match_mp_tac
            \\ qexistsl_tac [`P`, `fVars`, `dVars`]
            \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
            \\ Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f`
            \\ fs [] \\ conj_tac
            \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]
            \\ rpt strip_tac
            \\ first_x_assum match_mp_tac \\ fs[]
            \\ simp[Once usedVars_def])
555
      \\ qexists_tac `v` \\ fs []
556 557 558 559 560 561 562 563 564 565
      \\ rw_thm_asm `validIntervalbounds (Downcast m f) absenv P dVars` validIntervalbounds_def
      \\ Cases_on `absenv (Downcast m f)`
      \\ qmatch_assum_rename_tac `absenv (Downcast m f) = (iv_u, err_u)`
      \\ Cases_on `absenv f`
      \\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
      \\ rveq
      \\ fs[isSupersetInterval_def, IVlo_def, IVhi_def]
      \\ `domain (usedVars f) DIFF domain dVars  domain fVars` by (fs[Once usedVars_def])
      \\ `FST iv_u = FST iv_f` by (metis_tac [REAL_LE_ANTISYM])
      \\ `SND iv_u = SND iv_f` by (metis_tac [REAL_LE_ANTISYM])
566
      \\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`, `vR`] assume_tac thm)
567
      \\ qpat_x_assum `absenv f = _` (fn thm => fs [thm])
568 569 570
      \\ first_assum match_mp_tac
      \\ qexists_tac `defVars`
      \\ conj_tac \\ fs []));
571

572 573 574
val getRetExp_def = Define `
  getRetExp (f:'a cmd) =
    case f of
575
     |Let m x e g => getRetExp g
576 577
     |Ret e => e`;

578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600
val Rmap_updVars_comm = store_thm (
  "Rmap_updVars_comm",
  ``!Gamma n m x.
      updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x``,
  fs [updDefVars_def, toRMap_def]
  \\ rpt strip_tac
  \\ Cases_on `x = n` \\ fs[]);

val swap_Gamma_eval_exp = store_thm (
  "swap_Gamma_exp_exp",
  ``!e E vR m Gamma1 Gamma2.
      (!n. Gamma1 n = Gamma2 n) /\
      eval_exp E Gamma1 e vR m ==>
      eval_exp E Gamma2 e vR m``,
  Induct_on `e`
  \\ rpt strip_tac
  \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
  \\ fs[eval_exp_cases] \\ res_tac
  >- (qpat_x_assum `!n. _ = _` (fn thm => fs [GSYM thm]))
  >- (qexists_tac `delta` \\ fs[])
  >- (qexists_tac `v1` \\ fs[])
  >- (qexistsl_tac [`v1`, `delta`] \\ fs[])
  >- (qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta`] \\ fs[])
601
  >- (qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta`] \\ fs[])
602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
  >- (qexistsl_tac [`m1'`, `v1`, `delta`] \\ fs[]));

val swap_Gamma_bstep = store_thm (
  "swap_Gamma_bstep",
  ``!f E vR m Gamma1 Gamma2.
      (!n. Gamma1 n = Gamma2 n) /\
      bstep f E Gamma1 vR m ==>
      bstep f E Gamma2 vR m``,
  Induct_on `f`
  \\ rpt strip_tac \\ inversion `bstep _ _ _ _ _` bstep_cases
  \\ fs[bstep_cases]
  >- (qexists_tac `v` \\ conj_tac
      >- (irule swap_Gamma_eval_exp \\ qexists_tac `Gamma1` \\ fs[])
      >- (res_tac \\ first_x_assum irule
          \\ fs [updDefVars_def]))
  >- (irule swap_Gamma_eval_exp \\ qexists_tac `Gamma1` \\ fs[]));

619
val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
620
  ``!f (absenv:analysisResult) E fVars dVars outVars elo ehi err P Gamma.
621
      ssa f (union fVars dVars) outVars /\
622 623 624
      (!v. v IN (domain dVars) ==>
         ?vR.
           (E v = SOME vR) /\
625 626 627 628 629 630 631
           (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)) /\
632 633
      (!v. v IN (domain fVars) \/ v IN (domain dVars) ==>
         ?m. Gamma v = SOME m) /\
634 635
      validIntervalboundsCmd f absenv P dVars /\
      (absenv (getRetExp f) = ((elo, ehi), err)) ==>
636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698
      ?vR.
        (bstep (toREvalCmd f) E (toRMap Gamma) vR M0 /\
        elo <= vR /\ vR <= ehi)``,
  Induct_on `f`
  \\ rpt gen_tac
  \\ once_rewrite_tac [validIntervalboundsCmd_def, toREvalCmd_def, getRetExp_def]
  \\ rpt strip_tac
  >- (inversion `ssa _ _ _` ssa_cases \\ rveq
      \\ fs[]
      \\ Cases_on `absenv e` \\ rename1 `absenv e = (iv_e, err_e)`
      \\ `?v. eval_exp E (toRMap Gamma) (toREval e) v M0 /\ FST (FST (absenv e)) <= v /\ v <= SND (FST (absenv e))`
           by (irule validIntervalbounds_sound
               \\ qexistsl_tac [`P`, `dVars`, `fVars`]
               \\ fs []
               \\ conj_tac
               \\ fs [SUBSET_DEF, domain_union]
               \\ rpt strip_tac
               \\ `x IN domain fVars \/ x IN domain dVars` by (first_x_assum irule \\ fs[]))
      \\ `? vR. bstep (toREvalCmd f) (updEnv n v E) (toRMap (updDefVars n M0 Gamma)) vR M0 /\ elo <= vR /\ vR <= ehi`
           by (first_x_assum irule
               \\ qexistsl_tac [`P`, `absenv`, `insert n () dVars`, `err`, `fVars`, `outVars`]
               \\ fs [domain_insert]
               \\ rpt conj_tac
               >- (rpt strip_tac \\ fs[updEnv_def]
                   >- (rw_sym_asm `iv_e = FST _`
                       \\ rw_asm_star `absenv e = _ ` \\ fs[])
                   >- (rename1 `v2 IN domain dVars`
                       \\ Cases_on `v2 = n` \\ fs[]
                       \\ rveq \\ fs [domain_union]))
               >- (rpt strip_tac \\ fs[updEnv_def]
                   \\ rename1 `v2 IN domain fVars`
                   \\ Cases_on `v2 = n` \\ rveq \\ fs[domain_union])
               >- (rpt strip_tac \\ rveq \\ fs [updDefVars_def]
                   \\ rename1 `v2 IN domain _` \\ Cases_on `v2 = n` \\ fs[])
               >- (fs [domain_insert, SUBSET_DEF]
                   \\ rpt strip_tac
                   \\ first_x_assum match_mp_tac
                   \\ once_rewrite_tac [freeVars_def, domain_union]
                   \\ fs [domain_union])
               >- (match_mp_tac ssa_equal_set
                   \\ qexists_tac `(insert n () (union fVars dVars))`
                   \\ fs [domain_union,  domain_insert]
                   \\ once_rewrite_tac [UNION_COMM]
                   \\ fs [INSERT_UNION_EQ, UNION_COMM]))
       \\ qexists_tac `vR` \\ fs[bstep_cases]
       \\ qexists_tac `v` \\ fs[]
       \\ irule swap_Gamma_bstep
       \\ qexists_tac `(toRMap (updDefVars n M0 Gamma))` \\ fs[Rmap_updVars_comm])
  >- (fs []
      \\ inversion `ssa _ _ _` ssa_cases
      \\ `? v. eval_exp E (toRMap Gamma) (toREval e) v M0 /\ FST (FST (absenv e)) <= v /\ v <= SND (FST (absenv e))`
           by (irule validIntervalbounds_sound
               \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[]
               \\ conj_tac \\ fs[SUBSET_DEF, domain_union]
               \\ rpt strip_tac
               \\ rw_sym_asm `_ = domain outVars`
               \\ `x IN domain outVars` by (first_x_assum irule \\ fs[])
               \\ qpat_x_assum `_ = domain outVars` (fn thm => fs[GSYM thm])
               \\ fs[])
      \\ `bstep (Ret (toREval e)) E (toRMap Gamma) v M0`
           by (fs[bstep_cases])
      \\ qexists_tac `v` \\ fs[]
      \\ rw_asm_star `absenv e = _`));
699

700 701 702 703 704 705 706 707
val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzero_real",
  ``!(f1 f2:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set).
      validIntervalbounds (Binop Div f1 f2) absenv P dVars ==>
      noDivzero (SND (FST (absenv f2))) (FST (FST (absenv f2)))``,
  rpt strip_tac
  \\ Cases_on `absenv f2` \\ Cases_on `absenv f1` \\ Cases_on `absenv (Binop Div f1 f2)`
  \\ fs [Once validIntervalbounds_def, noDivzero_def, IVhi_def, IVlo_def]);

708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796
val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv",
  ``!(f:real exp) (absenv:analysisResult) (P:precond) (dVars:num_set).
      (!v. v IN domain dVars ==>
           valid (FST (absenv (Var v)))) /\
      validIntervalbounds f absenv P dVars ==>
      valid (FST (absenv f))``,
  Induct_on `f`
  \\ rpt strip_tac
  >- (first_x_assum (fn thm => qspecl_then [`n`] ASSUME_TAC thm)
      \\ Cases_on `absenv (Var n)`
      \\ fs[domain_lookup, valid_def, isSupersetInterval_def, validIntervalbounds_def]
      \\ REAL_ASM_ARITH_TAC)
  >- (rpt strip_tac
      \\ Cases_on `absenv (Const m v)` \\ fs[isSupersetInterval_def, valid_def, validIntervalbounds_def]
      \\ match_mp_tac REAL_LE_TRANS
      \\ asm_exists_tac \\ CONJ_TAC \\ fs[IVlo_def, IVhi_def])
  >- (qpat_x_assum `validIntervalbounds _ _ _ _`
        (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
      \\ Cases_on `absenv (Unop u f)` \\ Cases_on `absenv f` \\ fs[]
      \\ `valid (FST (absenv f))`
           by (first_x_assum match_mp_tac \\
               qexists_tac `P` \\ qexists_tac `dVars`
               \\ fs[])
      \\ Cases_on `u`
      \\ qpat_x_assum `absenv f = _` (fn thm => asm_rewrite_tac [thm] \\ ASSUME_TAC thm)
      >- (`valid (negateInterval q')`
            by (match_mp_tac iv_neg_preserves_valid \\ fs[])
          \\ fs[valid_def, isSupersetInterval_def]
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs[]
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs[])
      >- (`valid (invertInterval q')`
            by (match_mp_tac iv_inv_preserves_valid \\ fs[])
          \\ fs[valid_def, isSupersetInterval_def]
          >- (match_mp_tac REAL_LE_TRANS
              \\ asm_exists_tac \\ fs[]
              \\ match_mp_tac REAL_LE_TRANS
              \\ asm_exists_tac \\ fs[])
          >- (match_mp_tac REAL_LE_TRANS
              \\ asm_exists_tac \\ fs[]
              \\ match_mp_tac REAL_LE_TRANS
              \\ asm_exists_tac \\ fs[])))
  >- (rename1 `Binop b f1 f2`
      \\ qpat_x_assum `validIntervalbounds _ _ _ _`
           (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
      \\ Cases_on `absenv (Binop b f1 f2)` \\ rename1 `absenv (Binop b f1 f2) = (iv,err)`
      \\ fs[]
      \\ `valid (FST (absenv f1))`
           by (first_x_assum match_mp_tac
               \\ qexists_tac `P` \\ qexists_tac `dVars`
               \\ fs[])
      \\ `valid (FST (absenv f2))`
           by (first_x_assum match_mp_tac
               \\ qexists_tac `P` \\ qexists_tac `dVars`
               \\ fs[])
      \\ Cases_on `absenv f1` \\ Cases_on `absenv f2`
      \\ rename1 `absenv f1 = (iv_f1, err_f1)`
      \\ rename1 `absenv f2 = (iv_f2, err_f2)`
      \\ fs[]
      \\ Cases_on `b`
      >- (`valid (addInterval iv_f1 iv_f2)`
            by (match_mp_tac iv_add_preserves_valid \\ fs[])
          \\ fs[valid_def, isSupersetInterval_def]
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs []
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs [])
      >- (`valid (subtractInterval iv_f1 iv_f2)`
            by (match_mp_tac iv_sub_preserves_valid \\ fs[])
          \\ fs[valid_def, isSupersetInterval_def]
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs []
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs [])
      >- (`valid (multInterval iv_f1 iv_f2)`
            by (match_mp_tac iv_mult_preserves_valid \\ fs[])
          \\ fs[valid_def, isSupersetInterval_def]
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs []
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs [])
      >- (`valid (divideInterval iv_f1 iv_f2)`
            by (match_mp_tac iv_div_preserves_valid \\ fs[])
          \\ fs[valid_def, isSupersetInterval_def]
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs []
          \\ match_mp_tac REAL_LE_TRANS
          \\ asm_exists_tac \\ fs []))
797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
  >- (rename1 `Fma f1 f2 f3`
      \\ qpat_x_assum `validIntervalbounds _ _ _ _`
           (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
      \\ Cases_on `absenv (Fma f1 f2 f3)` \\ rename1 `absenv (Fma f1 f2 f3) = (iv,err)`
      \\ fs[]
      \\ `valid (FST (absenv f1))`
           by (first_x_assum match_mp_tac
               \\ qexists_tac `P` \\ qexists_tac `dVars`
               \\ fs[])
      \\ `valid (FST (absenv f2))`
           by (first_x_assum match_mp_tac
               \\ qexists_tac `P` \\ qexists_tac `dVars`
               \\ fs[])
      \\ `valid (FST (absenv f3))`
           by (first_x_assum match_mp_tac
               \\ qexists_tac `P` \\ qexists_tac `dVars`
               \\ fs[])
      \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
      \\ rename1 `absenv f1 = (iv_f1, err_f1)`
      \\ rename1 `absenv f2 = (iv_f2, err_f2)`
      \\ rename1 `absenv f3 = (iv_f3, err_f3)`
      \\ fs[]
      \\ `valid (addInterval iv_f1 (multInterval iv_f2 iv_f3))`
        by (match_mp_tac iv_add_preserves_valid \\ fs[]
            \\ match_mp_tac iv_mult_preserves_valid \\ fs[])
        \\ fs[valid_def, isSupersetInterval_def]
        \\ match_mp_tac REAL_LE_TRANS
        \\ asm_exists_tac \\ fs []
        \\ match_mp_tac REAL_LE_TRANS
        \\ asm_exists_tac \\ fs [])
827 828 829 830 831 832 833 834 835 836 837 838 839 840
  >- (qpat_x_assum `validIntervalbounds _ _ _ _`
        (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
      \\ Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f` \\ fs[]
      \\ `valid (FST (absenv f))`
           by (first_x_assum match_mp_tac \\
               qexists_tac `P` \\ qexists_tac `dVars`
               \\ fs[])
      \\ rename1 `absenv f = (iv_f, err_f)`
      \\ qpat_x_assum `absenv f = _` (fn thm => qpat_x_assum `valid (FST (absenv f))` (fn thm2 => ASSUME_TAC (REWRITE_RULE [thm] thm2)))
      \\ fs [valid_def, isSupersetInterval_def]
      \\ match_mp_tac REAL_LE_TRANS
      \\ qexists_tac `IVlo iv_f` \\ fs []
      \\ match_mp_tac REAL_LE_TRANS
      \\ qexists_tac `IVhi iv_f` \\ fs[]));
841 842

val _ = export_theory();