(**
    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
open simpLib realTheory realLib RealArith pred_setTheory sptreeTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory MachineTypeTheory
open sptreeLib sptreeTheory

val _ = new_theory "IntervalValidation";

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

val validIntervalbounds_def = Define `
  validIntervalbounds f (absenv:analysisResult) (P:precond) (validVars:num_set) =
    let (intv, _) = absenv f in
      case f of
        | Var v =>
          if (lookup v validVars = SOME ())
          then T
          else (isSupersetInterval (P v) intv /\ IVlo (P v) <= IVhi (P v))
        | Const m n => isSupersetInterval (n,n) intv
        | 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
            else F)
        | Downcast m f1 =>
          (let (iv1, _) = absenv f1 in
              if (validIntervalbounds f1 absenv P validVars) then
                  ((isSupersetInterval intv iv1) /\ (isSupersetInterval iv1 intv))
              else F)
        | 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 =>
                     let new_iv = multInterval iv1 iv2 in
                       isSupersetInterval new_iv intv
                  | Div =>
                     if (IVhi iv2 < 0 \/ 0 < IVlo iv2)
                       then
                         let new_iv = divideInterval iv1 iv2 in
                           isSupersetInterval new_iv intv
                       else F
            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)`;

val validIntervalboundsCmd_def = Define `
  validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num_set) =
    case f of
     | Let m x e g =>
       if (validIntervalbounds e absenv P validVars /\
          (FST (absenv e) = FST (absenv (Var x))))
         then validIntervalboundsCmd g absenv P (insert x () validVars)
         else F
   | Ret e =>
     (validIntervalbounds e absenv P validVars)`;

val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecond_sound",
``!(f:real exp) (absenv:analysisResult) (P:precond) (V:num_set).
   validIntervalbounds f absenv P V ==>
   (!(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[])
  >- (rpt (
        first_x_assum
          (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
      \\ `validIntervalbounds f absenv P V`
           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])
  >- (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])
  >- (rpt (
        first_x_assum
          (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm))
      \\ `validIntervalbounds f absenv P V`
           by (Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f` \\ fs [Once validIntervalbounds_def])
      \\ fs []));

val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
  ``!(f:real exp) (absenv:analysisResult) (P:precond) (fVars:num_set) (dVars:num_set) E Gamma.
       validIntervalbounds f absenv P dVars /\ (* The checker succeeded *)
       (* All defined vars have already been analyzed *)
       (!v. v IN (domain dVars) ==>
         (?vR. (E v = SOME vR) /\
         (FST (FST (absenv (Var v))) <= vR /\ vR <= SND (FST (absenv (Var v)))))) /\
       (* The variables in term f without the the defined variable set are a subset of the free variables *)
       (((domain (usedVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
       (* All free variables are defined in the execution environment and
          the values respect the precondition *)
       (!v. v IN (domain fVars) ==>
         (?vR. (E v = SOME vR) /\
         (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) ==>
       ? vR.
         eval_exp E (toRMap Gamma) (toREval f) vR M0 /\
         (FST (FST (absenv f))) <= vR /\ vR <= (SND (FST (absenv f)))``,
  Induct_on `f` \\ once_rewrite_tac [toREval_def,eval_exp_cases] \\ rpt strip_tac
  (* 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]
          \\ `?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])
          \\ qexists_tac `vR` \\ fs [toREval_def]
	  \\ fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ fs [] \\ rveq
          \\ conj_tac
          >- (match_mp_tac REAL_LE_TRANS
              \\ asm_exists_tac
              \\ fs [] \\ rveq \\ simp[])
          >- (match_mp_tac REAL_LE_TRANS
              \\ qexists_tac `SND (P n)`
              \\ fs [] \\ rveq \\ simp []))
      >- (specialize `!v. v IN domain dVars ==> _` `n`
          \\ `n IN domain dVars` by (fs [domain_lookup])
          \\ `?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])))
  (* Const case *)
  >- (Cases_on `absenv (Const m v)`
      \\ fs []
      \\ `eval_exp E (toRMap Gamma) (toREval (Const m v)) v M0`
           by (fs [toREval_def] \\ match_mp_tac Const_dist'
               \\ fs[mTypeToQ_def]
               \\ fs[perturb_def])
      \\ qexists_tac `v`
      \\ fs [mTypeToQ_def]
      \\ fs [validIntervalbounds_def, isSupersetInterval_def, IVhi_def, IVlo_def, toREval_def])
  (* Unary operator case *)
  >- (simp[evalUnop_def]
      \\ 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)`
          \\ 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]
          \\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`,`v1`] assume_tac thm)
          \\ qpat_x_assum `absenv f = _` (fn thm => fs[thm])
          \\ `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
             >- (qexists_tac `- SND iv_f` \\ conj_tac \\ simp [])
             >- (qexists_tac `- FST iv_f` \\ conj_tac \\ simp []))
          (* Inversion case *)
      >- (`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]
          \\ rw_thm_asm `validIntervalbounds a b c d` validIntervalbounds_def
          \\ 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)`
          \\ Cases_on `absenv f`
          \\ qmatch_assum_rename_tac `absenv f = (iv_f, err_f)`
          \\ rveq
          \\ rpt (qpat_x_assum `!v. _ ==> _` kall_tac)
          \\ rpt (qpat_x_assum `validIntervalbounds f absenv P dVars /\ _ /\ _ /\ _ /\ _ ==> _` kall_tac)
          \\ 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
                    \\ `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)
                    \\ `inv(-(SND iv_f)) = - (inv (SND iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
                    \\ `-(inv v) <= - (inv (SND iv_f))` by fs []
                    \\ fs[])
                >- (`0 < v` by REAL_ASM_ARITH_TAC \\
                    `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
                    \\ `0 < -v` by REAL_ASM_ARITH_TAC
                    \\ `0 < - (FST iv_f)` by REAL_ASM_ARITH_TAC
                    \\ `- v <= - (FST iv_f)` by REAL_ASM_ARITH_TAC
                    \\ `inv (- FST iv_f) <= inv (- v)` by fs[REAL_INV_LE_ANTIMONO]
                    \\ `inv(- FST iv_f) = - (inv (FST iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
                        \\ `inv(- v) = - (inv v)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
                    \\ `-(inv (FST iv_f)) <= - (inv v)` by fs []
                    \\ fs[])
                >- (`0 < v` by REAL_ASM_ARITH_TAC \\
                    `0 < FST iv_f` by REAL_ASM_ARITH_TAC \\
                    fs[REAL_INV_LE_ANTIMONO]))))
  (* Binary operator case *)
  >- (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 []
      \\ rw_thm_asm `validIntervalbounds (Binop b f f') absenv P V` validIntervalbounds_def
      \\ 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`
      \\ Cases_on `b` \\ simp[evalBinop_def]
     (* Plus case *)
     >- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, addInterval_def]
         \\ 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')`
            \\metis_tac []))
     (* Sub case *)
     >- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, subtractInterval_def, addInterval_def, negateInterval_def]
         \\ 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 []))
     (* Mult case *)
     >- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def]
         \\ 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')`
            \\ metis_tac []))
     (* Div case *)
     >- (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'`
                  \\ fs[]))
         >- (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')))`
                 \\ metis_tac []))))
  (* 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 []
      \\ rw_thm_asm `validIntervalbounds (Fma f1 f2 f3) absenv P V` validIntervalbounds_def
      \\ 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)`
      \\ 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)`
      \\ qexists_tac `evalFma v1 v2 v3`
      \\ fs[evalFma_def, evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def, addInterval_def]
      \\ qspecl_then [`iv_f2`, `iv_f3`, `v2`, `v3`]
         assume_tac
         (REWRITE_RULE
              [validIntervalAdd_def,
               multInterval_def,
               absIntvUpd_def,
               contained_def,
               IVhi_def,
               IVlo_def] interval_multiplication_valid)
      \\ qspecl_then [`iv_f1`, `multInterval iv_f2 iv_f3`, `v1`, `v2 * v3`]
          assume_tac
          (REWRITE_RULE
              [validIntervalAdd_def,
                  addInterval_def,
                  multInterval_def,
                  absIntvUpd_def,
                  contained_def,
                  IVhi_def, IVlo_def] interval_addition_valid)
      \\ fs[multInterval_def, absIntvUpd_def, IVlo_def, IVhi_def] \\ res_tac
      \\ 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
          \\ asm_exists_tac
          \\ conj_tac \\ fs[])
      >- (match_mp_tac REAL_LE_TRANS
          \\ 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[]))
  (* Downcast case *)
  >- (`?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])
      \\ qexists_tac `v` \\ fs []
      \\ 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])
      \\ first_x_assum (fn thm => qspecl_then [`absenv`,`P`, `fVars`, `dVars`, `E`, `vR`] assume_tac thm)
      \\ qpat_x_assum `absenv f = _` (fn thm => fs [thm])
      \\ first_assum match_mp_tac
      \\ qexists_tac `defVars`
      \\ conj_tac \\ fs []));

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

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[])
  >- (qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta`] \\ fs[])
  >- (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[]));

val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
  ``!f (absenv:analysisResult) E fVars dVars outVars elo ehi err P Gamma.
      ssa f (union fVars dVars) outVars /\
      (!v. v IN (domain dVars) ==>
         ?vR.
           (E v = SOME vR) /\
           (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)) /\
      (!v. v IN (domain fVars) \/ v IN (domain dVars) ==>
         ?m. Gamma v = SOME m) /\
      validIntervalboundsCmd f absenv P dVars /\
      (absenv (getRetExp f) = ((elo, ehi), err)) ==>
      ?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 = _`));

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]);

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 []))
  >- (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 [])
  >- (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[]));

val _ = export_theory();