(** This file contains the HOL4 implementation of the error bound validator as well as its soundness proof. The function validErrorbound is the Error bound validator from the certificate checking process. Under the assumption that a valid range arithmetic result has been computed, it can validate error bounds encoded in the analysis result. The validator is used in the file CertificateChecker.v to build the complete checker. **) open preamble open simpLib realTheory realLib RealArith pred_setTheory open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeTheory open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory TypingTheory open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory val _ = new_theory "ErrorValidation"; val _ = Parse.hide "delta"; (* so that it can be used as a variable *) val _ = temp_overload_on("abs",``real$abs``); val validErrorbound_def = Define ` validErrorbound e (typeMap: real exp -> mType option) (absenv:analysisResult) (dVars:num_set)= let (intv, err) = absenv e in let mopt = typeMap e in case mopt of | NONE => F | SOME m => if (0 <= err) then case e of | Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * (mTypeToQ m) <= err) | Const _ n => (maxAbs intv * (mTypeToQ m) <= err) | Unop Neg f => if (validErrorbound f typeMap absenv dVars) then err = (SND (absenv f)) else F | Unop Inv f => F | Binop op f1 f2 => (if (validErrorbound f1 typeMap absenv dVars /\ validErrorbound f2 typeMap absenv dVars) then let (ive1, err1) = absenv f1 in let (ive2, err2) = absenv f2 in let errIve1 = widenInterval ive1 err1 in let errIve2 = widenInterval ive2 err2 in let upperBoundE1 = maxAbs ive1 in let upperBoundE2 = maxAbs ive2 in case op of | Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (mTypeToQ m)) <= err | Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (mTypeToQ m)) <= err | Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (mTypeToQ m)) <= err | Div => (if (IVhi errIve2 < 0 \/ 0 < IVlo errIve2) then let upperBoundInvE2 = maxAbs (invertInterval ive2) in let minAbsIve2 = minAbsFun (errIve2) in let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToQ m)) <= err) else F) else F) | Fma f1 f2 f3 => (if (validErrorbound f1 typeMap absenv dVars /\ validErrorbound f2 typeMap absenv dVars /\ validErrorbound f3 typeMap absenv dVars) then let (ive1, err1) = absenv f1 in let (ive2, err2) = absenv f2 in let (ive3, err3) = absenv f3 in let errIve1 = widenInterval ive1 err1 in let errIve2 = widenInterval ive2 err2 in let errIve3 = widenInterval ive3 err3 in let upperBoundE1 = maxAbs ive1 in let upperBoundE2 = maxAbs ive2 in let upperBoundE3 = maxAbs ive3 in let errIntv_prod = multInterval errIve2 errIve3 in let mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in (err1 + mult_error_bound + (maxAbs (addInterval errIve1 errIntv_prod)) * (mTypeToQ m)) <= err else F) | Downcast m1 e1 => let (ive1, err1) = absenv e1 in let rec_res = validErrorbound e1 typeMap absenv dVars in let errIve1 = widenInterval ive1 err1 in rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToQ m1)) <= err) else F`; val validErrorboundCmd_def = Define ` validErrorboundCmd (f:real cmd) (typeMap: real exp -> mType option) (env:analysisResult) (dVars:num_set)= case f of | Let m x e g => if (validErrorbound e typeMap env dVars /\ (env e = env (Var x))) then validErrorboundCmd g typeMap env (insert x () dVars) else F | Ret e => validErrorbound e typeMap env dVars`; val err_always_positive = store_thm ( "err_always_positive", ``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars (tmap: real exp -> mType option). (validErrorbound e tmap absenv dVars) /\ ((iv,err) = absenv e) ==> 0 <= err``, once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\ Cases_on `e` \\ qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm]) >- (Cases_on `tmap (Var n)` \\ fs []) >- (Cases_on `tmap (Const m v)` \\ fs []) >- (Cases_on `tmap (Unop u e')` \\ fs []) >- (Cases_on `tmap (Binop b e' e0)` \\ fs []) >- (Cases_on `tmap (Fma e' e0 e1)` \\ fs []) >- (Cases_on `tmap (Downcast m e')` \\ fs [])); val validErrorboundCorrectVariable_eval = store_thm ( "validErrorboundCorrectVariable_eval", ``!E1 E2 absenv v e nR nlo nhi P fVars dVars Gamma expTypes. eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR M0 /\ typeCheck (Var v) Gamma expTypes /\ approxEnv E1 Gamma absenv fVars dVars E2 /\ validIntervalbounds (Var v) absenv P dVars /\ (domain (usedVars ((Var v):real exp)) DIFF (domain dVars)) SUBSET (domain fVars) /\ (!v. v IN domain dVars ==> ?r. E1 v = SOME r /\ FST(FST(absenv (Var v))) <= r /\ r <= SND (FST (absenv (Var v)))) /\ (!v. v IN domain fVars ==> ?r. E1 v = SOME r /\ FST (P v) <= r /\ r <= SND (P v)) /\ (!v. v IN ((domain fVars) UNION (domain dVars)) ==> ?m. Gamma v = SOME m) /\ absenv (Var v) = ((nlo, nhi),e) ==> ? nF m. eval_exp E2 Gamma (Var v) nF m``, rpt strip_tac \\ `?n. eval_exp E1 (toRMap Gamma) (toREval (Var v)) n M0 /\ FST(FST(absenv (Var v))) <= n /\ n <= SND (FST (absenv (Var v)))` by (irule validIntervalbounds_sound \\ qexistsl_tac[`P`, `dVars`, `fVars`] \\ fs[SUBSET_DEF, domain_union] \\ rpt strip_tac \\ first_x_assum irule \\ fs[]) \\ `nR = n` by (metis_tac[meps_0_deterministic]) \\ rveq \\ fs[toREval_def] \\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases \\ `?m. Gamma v = SOME m` by (Cases_on `Gamma v` \\ fs [toRMap_def]) \\ `?vF. E2 v = SOME vF` by (irule approxEnv_gives_value \\ qexistsl_tac [`E1`, `Gamma`, `absenv`, `dVars`, `fVars`, `n`] \\ fs[domain_union, SUBSET_DEF, usedVars_def] \\ Cases_on `v IN (domain dVars)` \\ fs[]) \\ qexistsl_tac [`vF`, `m`] \\ fs[eval_exp_cases]); val validErrorboundCorrectVariable = store_thm ( "validErrorboundCorrectVariable", ``!(E1 E2:env) absenv fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m expTypes Gamma. eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR M0 /\ eval_exp E2 Gamma (Var v) nF m /\ typeCheck (Var v) Gamma expTypes /\ approxEnv E1 Gamma absenv fVars dVars E2 /\ validIntervalbounds (Var v) absenv P dVars /\ validErrorbound (Var v) expTypes absenv dVars /\ (domain (usedVars ((Var v):real exp)) DIFF domain dVars) SUBSET domain fVars /\ (!v. v IN domain dVars ==> ?r. (E1 v = SOME r) /\ FST (FST (absenv (Var v))) <= r /\ r <= SND (FST (absenv (Var v)))) /\ (!v. v IN domain fVars ==> ?r. (E1 v = SOME r) /\ FST (P v) <= r /\ r <= SND (P v)) /\ (!v. v IN domain fVars \/ v IN domain dVars ==> ?m. Gamma v = SOME m) /\ (absenv (Var v) = ((nlo, nhi),err)) ==> abs (nR - nF) <= err``, rpt strip_tac \\ `?vR. eval_exp E1 (toRMap Gamma) (toREval (Var v)) vR M0 /\ FST (FST (absenv (Var v))) <= vR /\ vR <= SND(FST(absenv (Var v)))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[] \\ first_x_assum MATCH_ACCEPT_TAC) \\ `vR = nR` by (metis_tac[meps_0_deterministic]) \\ rveq \\ fs[toREval_def] \\ rpt (inversion `eval_exp _ _ _ _ _` eval_exp_cases) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def \\ rw_asm_star `absenv (Var v) = _` \\ rw_asm_star `Gamma v = _` \\ Cases_on `expTypes (Var v)` >- (fs[]) >- (Cases_on `lookup v dVars` \\ fs[] >- (fs[usedVars_def,domain_lookup] \\ irule REAL_LE_TRANS \\ qexists_tac `maxAbs (nlo,nhi) * mTypeToQ x` \\ fs[] \\ `abs (nR - nF) <= abs nR * mTypeToQ m` by (irule approxEnv_fVar_bounded \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `dVars`, `fVars`, `v`] \\ fs[domain_lookup]) \\ irule REAL_LE_TRANS \\ qexists_tac `abs nR * mTypeToQ m` \\ fs[] \\ irule REAL_LE_RMUL_IMP >- (irule contained_leq_maxAbs \\ fs[contained_def, IVlo_def, IVhi_def]) >- (irule mTypeToQ_pos)) >- (irule approxEnv_dVar_bounded \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `dVars`, `fVars`, `m`, `v`] \\ fs[domain_lookup]))); val validErrorboundCorrectConstant_eval = store_thm ( "validErrorboundCorrectConstant_eval", ``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars m expTypes Gamma. eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR M0 /\ typeCheck (Const m n) Gamma expTypes /\ validErrorbound (Const m n) expTypes absenv dVars /\ FST (FST (absenv (Const m n))) <= nR /\ nR <= SND (FST (absenv (Const m n))) /\ (absenv (Const m n) = ((nlo,nhi),e)) ==> ?nF m1. eval_exp E2 Gamma (Const m n) nF m1``, rpt strip_tac \\ qexistsl_tac [`perturb n (mTypeToQ m)`,`m`] \\ irule Const_dist' \\ fs[] \\ qexists_tac `mTypeToQ m` \\ fs[realTheory.abs, mTypeToQ_pos]); val validErrorboundCorrectConstant = store_thm ( "validErrorboundCorrectConstant", ``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars m expTypes Gamma. eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR M0 /\ eval_exp E2 Gamma (Const m n) nF m /\ typeCheck (Const m n) Gamma expTypes /\ validErrorbound (Const m n) expTypes absenv dVars /\ FST (FST (absenv (Const m n))) <= nR /\ nR <= SND (FST (absenv (Const m n))) /\ (absenv (Const m n) = ((nlo,nhi),e)) ==> (abs (nR - nF)) <= e``, once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\ fs[] \\ fs [toREval_def] \\ inversion `eval_exp _ _ _ _ M0` eval_exp_cases \\ simp [delta_M0_deterministic] \\ inversion `eval_exp _ _ _ _ m` eval_exp_cases \\ simp[perturb_def] \\ rename1 `abs deltaF <= (mTypeToQ m)` \\ simp [Rabs_err_simpl, ABS_MUL] \\ fs [typeCheck_def] \\ `expTypes (Const m n) = SOME m` by (Cases_on `expTypes (Const m n)` \\ fs [] \\ rveq) \\ fs [] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (nlo, nhi) * (mTypeToQ m)` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS]) \\ simp[maxAbs_def] \\ match_mp_tac maxAbs \\ qspecl_then [`delta`] (fn thm => fs [thm]) delta_M0_deterministic \\ qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2)) \\ simp[]); val validErrorboundCorrectAddition = store_thm ( "validErrorboundCorrectAddition", ``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp) (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ eval_exp E1 (toRMap Gamma) (toREval (Binop Plus e1 e2)) nR M0 /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 Gamma)) (Binop Plus (Var 1) (Var 2)) nF m /\ typeCheck (Binop Plus e1 e2) Gamma expTypes /\ validErrorbound (Binop Plus e1 e2) expTypes absenv dVars /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1)) /\ FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2)) /\ (absenv e1 = ((e1lo,e1hi),err1)) /\ (absenv e2 = ((e2lo, e2hi),err2)) /\ (absenv (Binop Plus e1 e2) = ((alo,ahi),e)) /\ abs (nR1 - nF1) <= err1 /\ abs (nR2 - nF2) <= err2 ==> abs (nR - nF) <= e``, once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\ fs[] \\ rw_asm `absenv _ = _` \\ rw_asm `absenv e1 = _` \\ fs [Once typeCheck_def] \\ Cases_on `expTypes (Binop Plus e1 e2)` \\ rveq \\ fs [] \\ Cases_on `expTypes e1` \\ rveq \\ fs [] \\ Cases_on `expTypes e2` \\ rveq \\ fs [] \\ `expTypes e1 = SOME m1` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ `expTypes e2 = SOME m2` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ fs [] \\ rveq \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `err1 + err2 + (abs (nF1 + nF2) * (mTypeToQ (join m1 m2)))` \\ conj_tac >- (match_mp_tac add_abs_err_bounded \\ qexistsl_tac [`e1`, `nR1`, `e2`, `nR2`, `E1`, `E2`, `m1`, `m2`, `Gamma`] \\ rpt (conj_tac) \\ simp[]) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `err1 + err2 + maxAbs ( addInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2)) * (mTypeToQ (join m1 m2))` \\ conj_tac \\ simp[maxAbs_def] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[mTypeToQ_def,mTypeToQ_pos] \\ match_mp_tac maxAbs \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained (nF1 + nF2) (addInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalAdd_def] interval_addition_valid) \\ conj_tac \\ simp[]) \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\ simp[])); val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtraction", ``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp) (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi:real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ eval_exp E1 (toRMap Gamma) (toREval (Binop Sub e1 e2)) nR M0 /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 Gamma)) (Binop Sub (Var 1) (Var 2)) nF m /\ typeCheck (Binop Sub e1 e2) Gamma expTypes /\ validErrorbound (Binop Sub e1 e2) expTypes absenv dVars /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1)) /\ FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2)) /\ (absenv e1 = ((e1lo,e1hi),err1)) /\ (absenv e2 = ((e2lo, e2hi),err2)) /\ (absenv (Binop Sub e1 e2) = ((alo,ahi),e)) /\ abs (nR1 - nF1) <= err1 /\ abs (nR2 - nF2) <= err2 ==> abs (nR - nF) <= e``, once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\ fs[] \\ fs [Once typeCheck_def] \\ Cases_on `expTypes (Binop Sub e1 e2)` \\ rveq \\ fs [] \\ Cases_on `expTypes e1` \\ rveq \\ fs [] \\ Cases_on `expTypes e2` \\ rveq \\ fs [] \\ `expTypes e1 = SOME m1` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ `expTypes e2 = SOME m2` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ fs [] \\ rveq \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `err1 + err2 + (abs (nF1 - nF2) * (mTypeToQ (join m1 m2)))` \\ conj_tac >- (match_mp_tac subtract_abs_err_bounded \\ qexistsl_tac [`e1`, `nR1`, `e2`, `nR2`, `E1`, `E2`, `m1`, `m2`, `Gamma`] \\ rpt (conj_tac) \\ simp[]) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `err1 + err2 + maxAbs ( subtractInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2)) * (mTypeToQ (join m1 m2))` \\ conj_tac \\ simp[maxAbs_def] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[mTypeToQ_def,mTypeToQ_pos] \\ match_mp_tac maxAbs \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained (nF1 - nF2) (subtractInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalSub_def] interval_subtraction_valid) \\ conj_tac \\ simp[]) \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\ simp[])); val multiplicationErroBounded = store_thm ("multiplicationErrorBounded", ``!(nR1 nR2 nF1 nF2: real) (err1 err2: real) (e1lo e1hi e2lo e2hi: real). e1lo ≤ nR1 /\ nR1 ≤ e1hi /\ e2lo ≤ nR2 /\ nR2 ≤ e2hi /\ abs (nR1 − nF1) ≤ err1 /\ abs (nR2 − nF2) ≤ err2 /\ 0 ≤ err1 /\ 0 ≤ err2 ==> abs (nR1 * nR2 − nF1 * nF2) ≤ maxAbs (e1lo,e1hi) * err2 + maxAbs (e2lo,e2hi) * err1 + err1 * err2``, (rpt strip_tac \\`nR1 <= maxAbs (e1lo, e1hi)` by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\ `nR2 <= maxAbs (e2lo, e2hi)` by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\`-nR1 <= maxAbs (e1lo, e1hi)` by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\ `-nR2 <= maxAbs (e2lo, e2hi)` by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\ `nR1 * err2 <= maxAbs (e1lo, e1hi) * err2` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `nR2 * err1 <= maxAbs (e2lo, e2hi) * err1` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `-nR2 * err1 <= maxAbs (e2lo, e2hi) * err1` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `- (err1 * err2) <= err1 * err2` by (fs[REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC) \\ `0 <= maxAbs (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC \\ `maxAbs (e1lo, e1hi) * err2 <= maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` by REAL_ASM_ARITH_TAC \\ `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1 <= maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1 + err1 * err2` by REAL_ASM_ARITH_TAC \\ rpt (qpat_x_assum `eval_exp _ _ _ _ _` kall_tac) \\ rpt (qpat_x_assum `validErrorbound _ _` kall_tac) \\ `! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)` by REAL_ASM_ARITH_TAC (* Large case distinction for a) different cases of the value of Rabs (...) and b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *) \\ qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 - nF1` ] DISJ_CASES_TAC thm) \\ qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR2 - nF2` ] DISJ_CASES_TAC thm) \\ fs[] \\ rpt (qpat_x_assum `abs _ = _` (fn thm => RULE_ASSUM_TAC (fn thm2 => ONCE_REWRITE_RULE [thm] thm2))) (* All positive *) >- (`nF1 <= nR1 + err1` by (match_mp_tac err_up \\ simp[]) \\ `nF2 <= nR2 + err2` by (match_mp_tac err_up \\ simp[]) \\ qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\ fs[real_sub] (* Absolute value positive *) >-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * (- (nR2 + err2))` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (simp[REAL_LE_NEG])) >- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 - err1) * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`nR1 * nR2 + (nR1 - err1) * - (nR2 + err2) = - nR1 * err2 + nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\ match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]) >- (qspecl_then [`- (nR2 - err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 - err1) * - (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`nR1 * nR2 + (nR1 - err1) * - (nR2 - err2) = nR1 * err2 + nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - (nR2 - err2) = nR1 * err2 + - nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] ))))) (* Absolute value negative *) >- (simp[REAL_NEG_ADD] \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (qspecl_then [`nR2 - err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 - err1) * (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`-(nR1 * nR2) + (nR1 - err1) * (nR2 - err2) = - nR1 * err2 + - nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 - err2) = - nR1 * err2 + nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG]) >- (qspecl_then [`nR2 + err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 - err1) * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`-(nR1 * nR2) + (nR1 - err1) * (nR2 + err2) = nR1 * err2 + - nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2) = nR1 * err2 + nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL])))))) (* First positive, second negative *) >- (`nF1 <= nR1 + err1` by (match_mp_tac err_up \\ simp[]) \\ `nF2 <= nR2 + err2` by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\ once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[] ) \\ qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\ fs[real_sub] (* Absolute value positive *) >-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * (- (nR2 + err2))` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (simp[REAL_LE_NEG])) >- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 - err1) * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`nR1 * nR2 + (nR1 - err1) * - (nR2 + err2) = - nR1 * err2 + nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * -nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\ qpat_x_assum `nR2 + - nF2 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\ simp[]) >- (qspecl_then [`- nR2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 - err1) * - nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`nR1 * nR2 + (nR1 - err1) * - nR2 = nR2 * err1` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ once_rewrite_tac [REAL_ADD_COMM] \\ simp [REAL_LE_ADDR])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - nR2 = - nR2 * err1` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ once_rewrite_tac [REAL_ADD_COMM] \\ simp [REAL_LE_ADDR]))))) (* Absolute value negative *) >- (simp[REAL_NEG_ADD] \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (qpat_x_assum `nR2 + - nF2 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[])) >- (qspecl_then [`nR2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 - err1) * nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`-(nR1 * nR2) + (nR1 - err1) * nR2 = - nR2 * err1` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ once_rewrite_tac [REAL_ADD_COMM] \\ simp [REAL_LE_ADDR])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * nR2 = nR2 * err1` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e2lo,e2hi) * err1` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ once_rewrite_tac [REAL_ADD_COMM] \\ simp [REAL_LE_ADDR])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG]) >- (qspecl_then [`nR2 + err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 - err1) * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (`-(nR1 * nR2) + (nR1 - err1) * (nR2 + err2) = nR1 * err2 + - nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2) = nR1 * err2 + nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL])))))) (* First negative, second positive *) >- (`nF2 <= nR2 + err2` by (match_mp_tac err_up \\ simp[]) \\ `nF1 <= nR1 + err1` by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\ once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[]) \\ qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\ fs[real_sub] (* Absolute value positive *) >-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (simp[REAL_LE_NEG])) >- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (qpat_x_assum `nR1 + - nF1 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm))\\ simp[])) >- (`nR1 * nR2 + nR1 * - (nR2 + err2) = - nR1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\ match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]) >- (qspecl_then [`- (nR2 - err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (qpat_x_assum `nR1 + - nF1 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[])) >- (`nR1 * nR2 + nR1 * - (nR2 - err2) = nR1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - (nR2 - err2) = nR1 * err2 + - nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL] ))))) (* Absolute value negative *) >- (simp[REAL_NEG_ADD] \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub])) >- (qspecl_then [`nR2 - err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nR1 * (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (qpat_x_assum `nR1 + - nF1 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[])) >- (`-(nR1 * nR2) + nR1 * (nR2 - err2) = - nR1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 - err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 - err2) = - nR1 * err2 + nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG]) >- (qspecl_then [`nR2 + err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nR1 * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (qpat_x_assum `nR1 + - nF1 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[])) >- (`-(nR1 * nR2) + nR1 * (nR2 + err2) = nR1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2) = nR1 * err2 + nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL])))))) (* Both negative *) >- (`nF1 <= nR1 + err1` by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\ once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[]) \\ `nF2 <= nR2 + err2` by (once_rewrite_tac[REAL_ADD_COMM] \\ simp [GSYM REAL_LE_SUB_RADD] \\ once_rewrite_tac [REAL_ADD_COMM, GSYM REAL_NEG_SUB] \\ simp[]) \\ `nR1 <= nF1` by (qpat_x_assum `nR1 - nF1 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[]) \\ `nR2 <= nF2` by (qpat_x_assum `nR2 - nF2 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[]) \\ qpat_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR1 * nR2 - nF1 * nF2` ] DISJ_CASES_TAC thm) \\ fs[real_sub] (* Absolute value positive *) >-(qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (simp[REAL_LE_NEG])) >- (qspecl_then [`- (nR2 + err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (qpat_x_assum `nR1 + - nF1 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[])) >- (`nR1 * nR2 + nR1 * - (nR2 + err2) = - nR1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[REAL_NEG_LMUL])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nF1 * - nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG] \\ match_mp_tac REAL_LE_ADD_FLIP \\ simp[real_sub]) >- (qspecl_then [`- nR2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + nR1 * - nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (simp[])) >- (`nR1 * nR2 + nR1 * - nR2 = 0` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`nR1 * nR2 + (nR1 + err1) * - nR2 = - nR2 * err1` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ once_rewrite_tac [REAL_ADD_COMM] \\ simp[REAL_LE_ADDR]))))) (* Absolute value negative *) >- (simp[REAL_NEG_ADD] \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (simp[])) >- (qspecl_then [`nR2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nR1 * nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (simp[])) >- (`-(nR1 * nR2) + nR1 * nR2 = 0` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * nR2` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * nR2 = nR2 * err1` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[] \\ once_rewrite_tac [REAL_ADD_COMM] \\ simp[REAL_LE_ADDR])))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nF1 * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[REAL_LE_NEG]) >- (qspecl_then [`nR2 + err2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + nR1 * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac >- (fs[] \\ match_mp_tac REAL_LT_IMP_LE \\ simp[]) >- (qpat_x_assum `nR1 + - nF1 <= _ ` (fn thm => assume_tac (SIMP_RULE bool_ss [GSYM real_sub, REAL_LE_SUB_RADD, REAL_ADD_LID] thm)) \\ simp[])) >- (`-(nR1 * nR2) + nR1 * (nR2 + err2) = nR1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2` \\ conj_tac \\ simp[] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo, e1hi) * err2 + maxAbs (e2lo, e2hi) * err1` \\ conj_tac \\ simp[])) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2)` \\ conj_tac >- (fs [REAL_NEG_RMUL] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ fs[]) >- (`-(nR1 * nR2) + (nR1 + err1) * (nR2 + err2) = nR1 * err2 + nR2 * err1 + err1 * err2` by (fs[real_sub,REAL_RDISTRIB] \\ fs [GSYM REAL_SUB_LNEG, real_sub, REAL_LDISTRIB, REAL_NEG_MUL2, REAL_ADD_ASSOC] \\ fs [GSYM real_sub, REAL_SUB_REFL, GSYM REAL_NEG_RMUL, REAL_MUL_COMM]) \\ simp[] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL])))))))); val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult", ``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp) (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ eval_exp E1 (toRMap Gamma) (toREval (Binop Mult e1 e2)) nR M0 /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 Gamma)) (Binop Mult (Var 1) (Var 2)) nF m /\ typeCheck (Binop Mult e1 e2) Gamma expTypes /\ validErrorbound (Binop Mult e1 e2) expTypes absenv dVars /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1)) /\ FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2)) /\ (absenv e1 = ((e1lo,e1hi),err1)) /\ (absenv e2 = ((e2lo, e2hi),err2)) /\ (absenv (Binop Mult e1 e2) = ((alo,ahi),e)) /\ abs (nR1 - nF1) <= err1 /\ abs (nR2 - nF2) <= err2 ==> abs (nR - nF) <= e``, once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\ fs[] \\ qpat_x_assum `absenv (Binop _ _ _) = _` (fn thm => fs [thm] \\ assume_tac thm) \\ qpat_x_assum `absenv e1 = _` (fn thm => fs [thm] \\ assume_tac thm) \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm] \\ assume_tac thm) \\ fs [Once typeCheck_def] \\ Cases_on `expTypes (Binop Mult e1 e2)` \\ rveq \\ fs [] \\ Cases_on `expTypes e1` \\ rveq \\ fs [] \\ Cases_on `expTypes e2` \\ rveq \\ fs [] \\ `expTypes e1 = SOME m1` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ `expTypes e2 = SOME m2` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ fs [] \\ rveq \\ `0 <= err1` by (match_mp_tac err_always_positive \\ qexistsl_tac [`e1`, `absenv`, `(e1lo,e1hi)`, `dVars`, `expTypes`] \\ fs[]) \\ `0 <= err2` by (match_mp_tac err_always_positive \\ qexistsl_tac [`e2`, `absenv`, `(e2lo,e2hi)`, `dVars`, `expTypes`] \\ fs[]) \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * (mTypeToQ (join m1 m2))` \\ conj_tac >- (match_mp_tac mult_abs_err_bounded \\ qexistsl_tac [`e1`, `e2`, `err1`, `err2`, `E1`, `E2`, `m1`, `m2`, `Gamma`] \\ fs []) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `maxAbs (e1lo,e1hi) * err2 + maxAbs (e2lo,e2hi) * err1 + err1 * err2 + maxAbs (multInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2)) * (mTypeToQ (join m1 m2))` \\ conj_tac \\ TRY(simp[]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac multiplicationErroBounded \\ fs[]) >- (simp[maxAbs_def] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[mTypeToQ_def,mTypeToQ_pos] \\ match_mp_tac maxAbs \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained (nF1 * nF2) (multInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` by (match_mp_tac interval_multiplication_valid \\ conj_tac \\ simp[]) \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\ simp[]))); val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv", ``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp) (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ eval_exp E1 (toRMap Gamma) (toREval (Binop Div e1 e2)) nR M0 /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 Gamma)) (Binop Div (Var 1) (Var 2)) nF m /\ typeCheck (Binop Div e1 e2) Gamma expTypes /\ validErrorbound (Binop Div e1 e2) expTypes absenv dVars /\ (e2hi < 0 \/ 0 < e2lo) /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1)) /\ FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2)) /\ (absenv e1 = ((e1lo,e1hi),err1)) /\ (absenv e2 = ((e2lo, e2hi),err2)) /\ (absenv (Binop Div e1 e2) = ((alo,ahi),e)) /\ abs (nR1 - nF1) <= err1 /\ abs (nR2 - nF2) <= err2 ==> abs (nR - nF) <= e``, rewrite_tac [Once validErrorbound_def, GSYM noDivzero_def] \\ rpt (strip_tac) \\ fs[] \\ fs [Once typeCheck_def] \\ Cases_on `expTypes (Binop Div e1 e2)` \\ rveq \\ fs [] \\ Cases_on `expTypes e1` \\ rveq \\ fs [] \\ Cases_on `expTypes e2` \\ rveq \\ fs [] \\ `expTypes e1 = SOME m1` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ `expTypes e2 = SOME m2` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ fs [] \\ rveq \\ `0 <= err1` by (match_mp_tac err_always_positive \\ qexistsl_tac [`e1`, `absenv`, `(e1lo,e1hi)`, `dVars`, `expTypes`] \\ fs[]) \\ `0 <= err2` by (match_mp_tac err_always_positive \\ qexistsl_tac [`e2`, `absenv`, `(e2lo,e2hi)`, `dVars`, `expTypes`] \\ fs[]) \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + abs (nF1 / nF2) * (mTypeToQ (join m1 m2))` \\ conj_tac >- (match_mp_tac div_abs_err_bounded \\ qexistsl_tac [`e1`, `e2`, `err1`, `err2`, `E1`, `E2`, `m1`, `m2`, `Gamma`] \\ fs []) >- (match_mp_tac REAL_LE_TRANS \\ once_rewrite_tac [CONJ_SYM] \\ asm_exists_tac \\ once_rewrite_tac [CONJ_SYM] \\ conj_tac \\ rw[] \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (rpt (qpat_x_assum `eval_exp _ _ _ _ _ _` kall_tac) \\ `contained (inv nR2) (invertInterval (e2lo, e2hi))` by (match_mp_tac interval_inversion_valid \\ conj_tac \\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def]) \\ `contained (inv nF2) (invertInterval (widenInterval (e2lo, e2hi) err2))` by (match_mp_tac interval_inversion_valid \\ conj_tac \\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def]) \\ `nR1 <= maxAbs (e1lo, e1hi)` by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\ `inv nR2 <= maxAbs (invertInterval(e2lo, e2hi))` by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\ `-nR1 <= maxAbs (e1lo, e1hi)` by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\ `- inv nR2 <= maxAbs (invertInterval (e2lo, e2hi))` by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\ `nR1 * err2 <= maxAbs (e1lo, e1hi) * err2` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `- inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1` by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\ `- (err1 * err2) <= err1 * err2` by (fs[REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC) \\ `0 <= maxAbs (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC \\ `0 <= maxAbs (invertInterval (e2lo, e2hi)) * err1` by REAL_ASM_ARITH_TAC \\ `maxAbs (e1lo, e1hi) * err2 <= maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1` by (REAL_ASM_ARITH_TAC) \\ `maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1 <= maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1 + err1 * err2` by REAL_ASM_ARITH_TAC (* Case distinction for divisor range positive or negative in float and real valued execution *) \\ rpt (qpat_x_assum `validErrorbound _ _ ` kall_tac) \\ rpt (qpat_x_assum `absenv _ = _` kall_tac) \\ rpt (qpat_x_assum `isSupersetInterval _ _` kall_tac) \\ rpt (qpat_x_assum `maxAbs (e1lo,e1hi) * (1 / (minAbsFun (widenInterval (e2lo,e2hi) err2) * minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) + maxAbs (invertInterval (e2lo,e2hi)) * err1 + err1 * (1 / (minAbsFun (widenInterval (e2lo,e2hi) err2) * minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) + maxAbs (divideInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2)) * machineEpsilon <= e` kall_tac) \\ fs [IVlo_def, IVhi_def, widenInterval_def, contained_def, noDivzero_def] (* The range of the divisor lies in the range from -infinity until 0 *) >- (`abs (inv nR2 - inv nF2) <= err2 * inv ((e2hi + err2) * (e2hi + err2))` by (match_mp_tac err_prop_inversion_neg \\ qexists_tac `e2lo` \\simp[]) \\ fs [widenInterval_def, IVlo_def, IVhi_def] \\ `minAbsFun (e2lo - err2, e2hi + err2) = - (e2hi + err2)` by (match_mp_tac minAbs_negative_iv_is_hi \\ REAL_ASM_ARITH_TAC) \\ simp[] \\ qpat_x_assum `minAbsFun _ = _ ` kall_tac \\ `nF1 <= err1 + nR1` by REAL_ASM_ARITH_TAC \\ `nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC \\ `(nR2 - nF2 > 0 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)` by REAL_ASM_ARITH_TAC (* Positive case for abs (nR2 - nF2) <= err2 *) >- (`nF2 < nR2` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `nF2 < nR2` (fn thm => assume_tac (ONCE_REWRITE_RULE [GSYM REAL_LT_NEG] thm)) \\ `inv (- nF2) < inv (- nR2)` by (match_mp_tac REAL_LT_INV \\ REAL_ASM_ARITH_TAC) \\ `inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\ `inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\ rpt ( qpat_x_assum `inv (- _) = - (inv _)` (fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp))) \\ `inv nR2 < inv nF2` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `- _ < - _` kall_tac \\ `inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC \\ `- (nR2⁻¹ − nF2⁻¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))⁻¹` by REAL_ASM_ARITH_TAC \\ `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))` by REAL_ASM_ARITH_TAC \\ `inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2` by REAL_ASM_ARITH_TAC (* Next do a case distinction for the absolute value *) \\ `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `!x. A /\ B \/ C` (fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm) (* Case 1: Absolute value positive *) >- (fs[real_sub, real_div, REAL_NEG_LMUL] \\ qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* -nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) = nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) = nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) = - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) = - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* Case 2: Absolute value negative *) >- (fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD] \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) = - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) = - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) = nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL, REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) = nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((-e2hi + -err2) * (-e2hi + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)))))) (* Negative case for abs (nR2 - nF2) <= err2 *) >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ `nR2 <= nF2` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `nR2 <= nF2` (fn thm => assume_tac (ONCE_REWRITE_RULE [GSYM REAL_LE_NEG] thm)) \\ `inv (- nR2) <= inv (- nF2)` by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ REAL_ASM_ARITH_TAC) \\ `inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\ `inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\ rpt ( qpat_x_assum `inv (- _) = - (inv _)` (fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp))) \\ `inv nF2 <= inv nR2` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `- _ <= - _` kall_tac \\ `0 <= inv nR2 - inv nF2` by REAL_ASM_ARITH_TAC \\ `(nR2⁻¹ − nF2⁻¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))⁻¹` by REAL_ASM_ARITH_TAC \\ `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))` by REAL_ASM_ARITH_TAC \\ `inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\ (* Next do a case distinction for the absolute value *) `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `!x. A /\ B \/ C` (fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm) \\ fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD] (* Case 1: Absolute value positive *) >- (qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* -nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) = nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) = nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) = - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) = - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* Case 2: Absolute value negative *) >- (qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) = - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) = - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) = nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) = nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))))) >- (CCONTR_TAC \\ rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\ `e2lo <= e2hi` by REAL_ASM_ARITH_TAC \\ `e2lo <= e2hi + err2` by REAL_ASM_ARITH_TAC \\ `e2lo <= e2hi + err2` by REAL_ASM_ARITH_TAC \\ REAL_ASM_ARITH_TAC) >- (CCONTR_TAC \\ rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\ `e2lo <= e2hi` by REAL_ASM_ARITH_TAC \\ `e2lo - err2 <= e2hi` by REAL_ASM_ARITH_TAC \\ REAL_ASM_ARITH_TAC) (* The range of the divisor lies in the range from 0 to infinity *) >- (rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def, contained_def, invertInterval_def] thm) \\ `abs (inv nR2 - inv nF2) <= err2 * (inv ((e2lo - err2) * (e2lo -err2)))` by (match_mp_tac err_prop_inversion_pos \\ qexists_tac `e2hi` \\ rpt(conj_tac) \\ fs[contained_def, IVlo_def, IVhi_def]) \\ fs [widenInterval_def, IVlo_def, IVhi_def, invertInterval_def] \\ `minAbsFun (e2lo - err2, e2hi + err2) = (e2lo - err2)` by (match_mp_tac minAbs_positive_iv_is_lo \\ REAL_ASM_ARITH_TAC) \\ simp[] \\ qpat_x_assum `minAbsFun _ = _ ` kall_tac \\ `nF1 <= err1 + nR1` by REAL_ASM_ARITH_TAC \\ `nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC \\ `(nR2 - nF2 > 0 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)` by REAL_ASM_ARITH_TAC (* Positive case for abs (nR2 - nF2) <= err2 *) >- (`nF2 < nR2` by REAL_ASM_ARITH_TAC \\ `inv nR2 < inv nF2` by (match_mp_tac REAL_LT_INV \\ TRY REAL_ASM_ARITH_TAC) \\ `inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC \\ `nR2⁻¹ − nF2⁻¹ ≤ err2 * ((e2lo - err2) * (e2lo - err2))⁻¹` by REAL_ASM_ARITH_TAC \\ `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by REAL_ASM_ARITH_TAC \\ `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\ (* Next do a case distinction for the absolute value *) `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `!x. A /\ B \/ C` (fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm) (* Case 1: Absolute value positive *) >- (fs[real_sub, real_div, REAL_NEG_LMUL] \\ qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* -nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) = nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + - err2) * (e2lo + - err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp[GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) = nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) = - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) = - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp [GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* Case 2: Absolute value negative *) >- (fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD] \\ qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) = - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp [GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) = - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) = nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) = nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp [GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)))))) (* Negative case for abs (nR2 - nF2) <= err2 *) >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ `nR2 <= nF2` by REAL_ASM_ARITH_TAC \\ `inv nF2 <= inv nR2` by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ REAL_ASM_ARITH_TAC) \\ `0 <= inv nR2 - inv nF2` by REAL_ASM_ARITH_TAC \\ `(nR2⁻¹ − nF2⁻¹) ≤ err2 * ((e2lo - err2) * (e2lo - err2))⁻¹` by REAL_ASM_ARITH_TAC \\ `inv nF2 <= inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2))` by REAL_ASM_ARITH_TAC \\ `inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\ (* Next do a case distinction for the absolute value *) `! (x:real). ((abs x = x) /\ 0 <= x) \/ ((abs x = - x) /\ x < 0)` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `!x. A /\ B \/ C` (fn thm => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm) \\ fs[real_sub, real_div, REAL_NEG_LMUL, REAL_NEG_ADD] (* Case 1: Absolute value positive *) >- (qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* -nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) = nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp [GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) = nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 + err_inv) = - nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (simp [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 + err_inv) = - nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp [GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* Case 2: Absolute value negative *) >- (qspecl_then [`nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL (* nF1 < 0 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 - err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 - err_inv) = - nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp [GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 - err_inv) = - nR1 * err_inv + inv nR2 * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp [real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [GSYM REAL_NEG_ADD, REAL_NEG_MUL2, REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))))) (* 0 <= - nF1 *) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + nF1 * (inv nR2 + err2 * inv ((e2lo - err2) * (e2lo - err2)))` \\ conj_tac >- (fs[REAL_LE_LADD] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (qabbrev_tac `err_inv = (err2 * ((e2lo - err2) * (e2lo - err2))⁻¹)` \\ qspecl_then [`inv nR2 + err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `-nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ fs [REAL_LE_NEG]) >- (`- nR1 * inv nR2 + (nR1 - err1) * (inv nR2 + err_inv) = nR1 * err_inv + - (inv nR2) * err1 - err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ simp[real_sub] \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (fs [REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC))) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv)` \\ conj_tac >- (fs [REAL_LE_ADD] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC) >- (`- nR1 * inv nR2 + (nR1 + err1) * (inv nR2 + err_inv) = nR1 * err_inv + inv nR2 * err1 + err1 * err_inv` by REAL_ASM_ARITH_TAC \\ simp[REAL_NEG_MUL2] \\ qspecl_then [`inv ((e2lo + -err2) * (e2lo + -err2))`,`err2`] (fn thm => once_rewrite_tac [thm]) REAL_MUL_COMM \\ qunabbrev_tac `err_inv` \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC \\ simp [GSYM real_sub] \\ match_mp_tac REAL_LE_RMUL_IMP \\ conj_tac \\ REAL_ASM_ARITH_TAC)))))))) >- (simp[maxAbs_def] \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[mTypeToQ_def,mTypeToQ_pos] \\ match_mp_tac maxAbs \\ `contained (nF1 / nF2) (divideInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` by (match_mp_tac interval_division_valid \\ conj_tac \\ fs[noDivzero_def]) \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\ fs[widenInterval_def, IVlo_def, IVhi_def,noDivzero_def]))); val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma", ``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp) (e3: real exp) (nR nR1 nR2 nR3 nF nF1 nF2 nF3:real) (e err1 err2 err3:real) (alo ahi e1lo e1hi e2lo e2hi e3lo e3hi :real) dVars m m1 m2 m3 expTypes Gamma. (m = join3 m1 m2 m3) /\ eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ eval_exp E1 (toRMap Gamma) (toREval e3) nR3 M0 /\ eval_exp E1 (toRMap Gamma) (toREval (Fma e1 e2 e3)) nR M0 /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp E2 Gamma e3 nF3 m3 /\ eval_exp (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))) (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma))) (Fma (Var 1) (Var 2) (Var 3)) nF m /\ typeCheck (Fma e1 e2 e3) Gamma expTypes /\ validErrorbound (Fma e1 e2 e3) expTypes absenv dVars /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1)) /\ FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2)) /\ FST (FST (absenv e3)) <= nR3 /\ nR3 <= SND (FST (absenv e3)) /\ (absenv e1 = ((e1lo,e1hi),err1)) /\ (absenv e2 = ((e2lo, e2hi),err2)) /\ (absenv e3 = ((e3lo, e3hi),err3)) /\ (absenv (Fma e1 e2 e3) = ((alo,ahi),e)) /\ abs (nR1 - nF1) <= err1 /\ abs (nR2 - nF2) <= err2 /\ abs (nR3 - nF3) <= err3 ==> abs (nR - nF) <= e``, once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\ fs[] \\ qpat_x_assum `absenv (Fma _ _ _) = _` (fn thm => fs [thm] \\ assume_tac thm) \\ qpat_x_assum `absenv e1 = _` (fn thm => fs [thm] \\ assume_tac thm) \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm] \\ assume_tac thm) \\ qpat_x_assum `absenv e3 = _` (fn thm => fs [thm] \\ assume_tac thm) \\ fs [Once typeCheck_def] \\ Cases_on `expTypes (Fma e1 e2 e3)` \\ rveq \\ fs [] \\ Cases_on `expTypes e1` \\ rveq \\ fs [] \\ Cases_on `expTypes e2` \\ rveq \\ fs [] \\ Cases_on `expTypes e3` \\ rveq \\ fs [] \\ `expTypes e1 = SOME m1` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ `expTypes e2 = SOME m2` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ `expTypes e3 = SOME m3` by (match_mp_tac typingSoundnessExp \\ metis_tac []) \\ fs [] \\ rveq \\ `0 <= err1` by (match_mp_tac err_always_positive \\ qexistsl_tac [`e1`, `absenv`, `(e1lo,e1hi)`, `dVars`, `expTypes`] \\ fs[]) \\ `0 <= err2` by (match_mp_tac err_always_positive \\ qexistsl_tac [`e2`, `absenv`, `(e2lo,e2hi)`, `dVars`, `expTypes`] \\ fs[]) \\ `0 <= err3` by (match_mp_tac err_always_positive \\ qexistsl_tac [`e3`, `absenv`, `(e3lo,e3hi)`, `dVars`, `expTypes`] \\ fs[]) \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `abs ((nR1 - nF1) + (nR2 * nR3 - nF2 * nF3)) + abs (nF1 + nF2 * nF3) * (mTypeToQ (join3 m1 m2 m3))` \\ conj_tac >- (match_mp_tac fma_abs_err_bounded \\ qexistsl_tac [`e1`, `e2`, `e3`, `err1`, `err2`, `err3`, `E1`, `E2`, `m1`, `m2`, `m3`, `Gamma`] \\ rpt (conj_tac) \\ simp[]) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `err1 + (maxAbs (e2lo,e2hi) * err3 + maxAbs (e3lo,e3hi) * err2 + err2 * err3) + maxAbs (addInterval (widenInterval (e1lo,e1hi) err1) (multInterval (widenInterval (e2lo,e2hi) err2) (widenInterval (e3lo,e3hi) err3))) * mTypeToQ (join3 m1 m2 m3)` \\ conj_tac >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac >- (qspecl_then [`abs (nR1 - nF1) + abs (nR2 * nR3 − nF2 * nF3)`] match_mp_tac real_le_trans2 \\ conj_tac >- (REAL_ASM_ARITH_TAC) >- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\ fs[] \\ match_mp_tac multiplicationErroBounded \\ fs[])) >- (`contained nF2 (widenInterval (e2lo,e2hi) err2)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained nF3 (widenInterval (e3lo,e3hi) err3)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR3` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained (nF2 * nF3) (multInterval (widenInterval (e2lo, e2hi) err2) (widenInterval (e3lo, e3hi) err3))` by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalMult_def] interval_multiplication_valid) \\ conj_tac \\ simp[]) \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` by (match_mp_tac distance_gives_iv \\ qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\ `contained (nF1 + (nF2 * nF3)) (addInterval (widenInterval (e1lo,e1hi) err1) (multInterval (widenInterval (e2lo,e2hi) err2) (widenInterval (e3lo,e3hi) err3)))` by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalAdd_def] interval_addition_valid) \\ conj_tac \\ simp[]) \\ once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[mTypeToQ_def,mTypeToQ_pos] \\ fs [maxAbs_def] \\ match_mp_tac maxAbs \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\ fs[])) >- (fs []))); val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding", ``!(E1 E2:env) (absenv:analysisResult) (e:real exp) (nR nF nF1:real) (err err':real) (alo ahi elo ehi:real) dVars m machineEpsilon expTypes Gamma. eval_exp E1 (toRMap Gamma) (toREval e) nR M0 /\ eval_exp E2 Gamma e nF1 m /\ eval_exp (updEnv 1 nF1 emptyEnv) (updDefVars 1 m Gamma) (Downcast machineEpsilon (Var 1)) nF machineEpsilon /\ typeCheck (Downcast machineEpsilon e) Gamma expTypes /\ validErrorbound (Downcast machineEpsilon e) expTypes absenv dVars /\ elo <= nR /\ nR <= ehi /\ (absenv e = ((elo,ehi),err)) /\ (absenv (Downcast machineEpsilon e) = ((alo,ahi),err')) /\ abs (nR - nF1) <= err ==> abs (nR - nF) <= err'``, rpt strip_tac \\ fs [Once validErrorbound_def] \\ Cases_on `expTypes (Downcast machineEpsilon' e)` \\ fs [] \\ match_mp_tac REAL_LE_TRANS \\ qexists_tac `err + (abs nF1) * mTypeToQ machineEpsilon'` \\ fs [] \\ conj_tac >- (match_mp_tac round_abs_err_bounded \\ qexistsl_tac [`e`, `E1`, `E2`, `m`, `Gamma`] \\ fs []) >- (match_mp_tac REAL_LE_TRANS \\ qexists_tac `err + maxAbs (widenInterval (elo,ehi) err) * mTypeToQ machineEpsilon'` \\ fs [] \\ fs [REAL_MUL_SYM] \\ `abs nF1 * mTypeToQ machineEpsilon' = mTypeToQ machineEpsilon' * abs nF1` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `abs nF1 * _ = _ * abs nF1` (fn thm => fs [thm]) \\ match_mp_tac REAL_LE_LMUL_IMP \\ fs [mTypeToQ_def,mTypeToQ_pos] \\ fs [maxAbs_def] \\ match_mp_tac maxAbs \\ fs [widenInterval_def,IVlo_def,IVhi_def] \\ qpat_x_assum `abs (nR - nF1) <= err` (fn thm => assume_tac (ONCE_REWRITE_RULE [ABS_BOUNDS] thm)) \\ REAL_ASM_ARITH_TAC)); val validErrorbound_sound = store_thm ("validErrorbound_sound", ``!(e:real exp) (E1 E2:env) (absenv:analysisResult) (nR err:real) (P:precond) (elo ehi:real) (fVars:num_set) dVars expTypes Gamma. typeCheck e Gamma expTypes /\ approxEnv E1 Gamma absenv fVars dVars E2 /\ ((domain (usedVars e)) DIFF (domain dVars)) SUBSET (domain fVars) /\ eval_exp E1 (toRMap Gamma) (toREval e) nR M0 /\ validErrorbound e expTypes absenv dVars /\ validIntervalbounds e absenv P dVars /\ (!v. v IN domain dVars ==> ?r. (E1 v = SOME r) /\ FST (FST (absenv (Var v))) <= r /\ r <= SND (FST (absenv (Var v)))) /\ (!v. v IN domain fVars ==> ?r. (E1 v = SOME r) /\ FST (P v) <= r /\ r <= SND (P v)) /\ (!v. v IN domain fVars \/ v IN domain dVars ==> ?m. Gamma v = SOME m) /\ (absenv e = ((elo,ehi),err)) ==> (?nF m. eval_exp E2 Gamma e nF m) /\ (!nF m. eval_exp E2 Gamma e nF m ==> abs (nR - nF) <= err)``, Induct_on `e` \\ rpt gen_tac \\ rpt (disch_then assume_tac) \\ fs[] \\ rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def \\ rw_asm_star `absenv _ = _` >- (conj_tac >- (irule validErrorboundCorrectVariable_eval \\ fs[] >- (qexists_tac `expTypes` \\ fs[]) >- (qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `err`, `fVars`, `nR`, `ehi`, `elo`] \\ fs[] \\ first_x_assum MATCH_ACCEPT_TAC)) >- (rpt strip_tac \\ irule validErrorboundCorrectVariable \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `P`, `absenv`, `dVars`, `expTypes`, `fVars`, `m`, `ehi`, `elo`, `n`] \\ fs [validErrorbound_def] \\ first_x_assum MATCH_ACCEPT_TAC)) >- (conj_tac >- (irule validErrorboundCorrectConstant_eval \\ qexistsl_tac [`E1`, `absenv`, `dVars`, `err`, `expTypes`, `nR`, `ehi`, `elo`] \\ fs[toREval_def] \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def \\ Cases_on `expTypes (Const m v)` \\ fs[isSupersetInterval_def, IVlo_def, IVhi_def, validErrorbound_def, toREval_def] \\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases \\ rw_asm_star `absenv _ = _` \\ `perturb v delta = v` by (irule delta_0_deterministic \\ fs[mTypeToQ_def]) \\ fs[]) >- (rpt strip_tac \\ `m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq \\ irule validErrorboundCorrectConstant \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `dVars`, `expTypes`, `m`, `v`, `ehi`, `elo`] \\ fs[validErrorbound_def] \\ drule validIntervalbounds_sound \\ qpat_x_assum `absenv _ = _` (fn thm => rewrite_tac [thm] \\ assume_tac thm) \\ disch_then ( qspecl_then [`fVars`, `E1`, `Gamma`] drule ) \\ disch_then assume_tac \\ `?vR. eval_exp E1 (toRMap Gamma) (toREval (Const m v)) vR M0 /\ elo <= vR /\ vR <= ehi` by (first_x_assum irule \\ fs[] \\ first_x_assum MATCH_ACCEPT_TAC) \\ `vR = nR` by (metis_tac[meps_0_deterministic]) \\ fs[])) >- (Cases_on `expTypes (Unop u e)` \\ Cases_on `u` \\ fs[] \\ Cases_on `absenv e` \\ rename1 `absenv e = (iv_e, err_e)` \\ Cases_on `iv_e` \\ rename1 `absenv e= ((e_lo, e_hi), err_e)` \\ rw_thm_asm `eval_exp E1 _ _ _ _` toREval_def \\ fs[] \\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases \\ fs[] \\ `(?nF m. eval_exp E2 Gamma e nF m) /\ (!nF m. eval_exp E2 Gamma e nF m ==> abs (v1 - nF) <= err_e)` by (first_x_assum irule \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e_hi`, `e_lo`, `expTypes`, `fVars`] \\ fs[Once usedVars_def, Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_asm_star `expTypes _ = _` \\ Cases_on `expTypes e` \\ fs[]) \\ conj_tac >- (qexistsl_tac [`evalUnop Neg nF`, `m`] \\ fs[eval_exp_cases] \\ qexists_tac `nF` \\ fs[]) >- (rpt strip_tac \\ inversion `eval_exp E2 _ (Unop Neg e) _ _` eval_exp_cases \\ fs[evalUnop_def] \\ once_rewrite_tac [real_sub] \\ rewrite_tac [GSYM REAL_NEG_ADD, ABS_NEG, GSYM real_sub] \\ first_x_assum irule \\ asm_exists_tac \\ fs[])) >- (rename1 `Binop op e1 e2` \\ Cases_on `expTypes (Binop op e1 e2)` \\ fs[] \\ Cases_on `absenv e1` \\ rename1 `absenv e1 = (iv_e1, err_e1)` \\ Cases_on `iv_e1` \\ rename1 `absenv e1= ((e1_lo, e1_hi), err_e1)` \\ Cases_on `absenv e2` \\ rename1 `absenv e2 = (iv_e2, err_e2)` \\ Cases_on `iv_e2` \\ rename1 `absenv e2 = ((e2_lo, e2_hi), err_e2)` \\ rw_thm_asm `eval_exp E1 _ _ _ _` toREval_def \\ fs[] \\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[]) \\ rveq \\ `(?nF1 m1. eval_exp E2 Gamma e1 nF1 m1) /\ (!nF1 m1. eval_exp E2 Gamma e1 nF1 m1 ==> abs (v1 - nF1) <= err_e1)` by (first_x_assum irule \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e1_hi`, `e1_lo`, `expTypes`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_asm_star `expTypes _ = _` \\ Cases_on `expTypes e1` \\ Cases_on `expTypes e2` \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `(?nF2 m2. eval_exp E2 Gamma e2 nF2 m2) /\ (!nF2 m2. eval_exp E2 Gamma e2 nF2 m2 ==> abs (v2 - nF2) <= err_e2)` by (first_x_assum irule \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e2_hi`, `e2_lo`, `expTypes`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_asm_star `expTypes _ = _` \\ Cases_on `expTypes e1` \\ Cases_on `expTypes e2` \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?nR1. eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ fs [DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?nR2. eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ fs [DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `nR1 = v1 /\ nR2 = v2` by (metis_tac[meps_0_deterministic]) \\ rveq \\ rw_asm_star `absenv e1 = _` \\ rw_asm_star `absenv e2 = _` \\ `contained nF1 (widenInterval (e1_lo,e1_hi) err_e1)` by (irule distance_gives_iv \\ qexists_tac `nR1` \\ fs[contained_def, IVlo_def, IVhi_def] \\ first_x_assum irule \\ qexists_tac `m1` \\ fs[]) \\ `contained nF2 (widenInterval (e2_lo, e2_hi) err_e2)` by (irule distance_gives_iv \\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def] \\ first_x_assum irule \\ qexists_tac `m2` \\ fs[]) \\ `op = Div ==> nF2 <> 0` by (strip_tac \\ fs[IVhi_def, IVlo_def, widenInterval_def, contained_def] >- (CCONTR_TAC \\ fs[] \\ rveq \\ `0 < 0:real` by (irule REAL_LET_TRANS \\ qexists_tac `e2_hi + err_e2` \\ fs[]) \\ fs[]) >- (CCONTR_TAC \\ fs[] \\ rveq \\ `0 < 0:real` by (irule REAL_LTE_TRANS \\ qexists_tac `e2_lo - err_e2` \\ fs[]) \\ fs[])) \\ conj_tac >- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) 0`, `join m1 m2`] \\ irule Binop_dist' \\ qexistsl_tac [`0`, `m1`, `m2`, `nF1`, `nF2`] \\ fs[mTypeToQ_pos]) \\ rpt strip_tac \\ `perturb (evalBinop op nR1 nR2) delta = evalBinop op nR1 nR2` by (irule delta_0_deterministic \\ fs[mTypeToQ_def, join_def]) \\ fs[] \\ inversion `eval_exp E2 _ (Binop op e1 e2) _ _` eval_exp_cases \\ rename1 `abs delta2 <= mTypeToQ (join mF1 mF2)` \\ `eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv)) (updDefVars 2 mF2 (updDefVars 1 mF1 Gamma)) (Binop op (Var 1) (Var 2)) (perturb (evalBinop op v1 v2) delta2) (join mF1 mF2)` by (irule binary_unfolding \\ fs[] \\ qexistsl_tac [`E2`, `e1`, `e2`] \\ fs[eval_exp_cases] \\ qexistsl_tac [`mF1`, `mF2`, `v1`, `v2`, `delta2`] \\ fs[]) \\ Cases_on `op` \\ rveq >- (irule validErrorboundCorrectAddition \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`, `e1`, `e1_hi`, `e1_lo`, `e2`,`e2_hi`, `e2_lo`, `err_e1`, `err_e2`, `expTypes`, `join mF1 mF2`, `mF1`, `mF2`, `v1`, `v2`, `nR1`, `nR2`] \\ fs[] \\ rpt conj_tac \\ TRY (first_x_assum irule) >- (qexists_tac `mF1` \\ fs[]) >- (qexists_tac `mF2` \\ fs[]) >- (once_rewrite_tac [validErrorbound_def] \\ fs[]) >- (simp [Once toREval_def] \\ irule Binop_dist' \\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`] \\ fs[perturb_def, mTypeToQ_pos])) >- (irule validErrorboundCorrectSubtraction \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`, `e1`, `e1_hi`, `e1_lo`, `e2`,`e2_hi`, `e2_lo`, `err_e1`, `err_e2`, `expTypes`, `join mF1 mF2`, `mF1`, `mF2`, `v1`, `v2`, `nR1`, `nR2`] \\ fs[] \\ rpt conj_tac \\ TRY (first_x_assum irule) >- (qexists_tac `mF1` \\ fs[]) >- (qexists_tac `mF2` \\ fs[]) >- (once_rewrite_tac [validErrorbound_def] \\ fs[]) >- (simp [Once toREval_def] \\ irule Binop_dist' \\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`] \\ fs[perturb_def, mTypeToQ_pos])) >- (irule validErrorboundCorrectMult \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`, `e1`, `e1_hi`, `e1_lo`, `e2`,`e2_hi`, `e2_lo`, `err_e1`, `err_e2`, `expTypes`, `join mF1 mF2`, `mF1`, `mF2`, `v1`, `v2`, `nR1`, `nR2`] \\ fs[] \\ rpt conj_tac \\ TRY (first_x_assum irule) >- (qexists_tac `mF1` \\ fs[]) >- (qexists_tac `mF2` \\ fs[]) >- (once_rewrite_tac [validErrorbound_def] \\ fs[]) >- (simp [Once toREval_def] \\ irule Binop_dist' \\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`] \\ fs[perturb_def, mTypeToQ_pos])) >- (irule validErrorboundCorrectDiv \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`, `e1`, `e1_hi`, `e1_lo`, `e2`,`e2_hi`, `e2_lo`, `err_e1`, `err_e2`, `expTypes`, `join mF1 mF2`, `mF1`, `mF2`, `v1`, `v2`, `nR1`, `nR2`] \\ rpt conj_tac \\ TRY (first_x_assum irule) \\ TRY (fs[] \\ FAIL_TAC "") >- (fs [IVlo_def, IVhi_def, widenInterval_def] >- (DISJ1_TAC \\ irule REAL_LET_TRANS \\ qexists_tac `e2_hi + err_e2` \\ fs[realTheory.REAL_LE_ADDR] \\ irule err_always_positive \\ qexistsl_tac [`absenv`, `dVars`, `e2`, `(e2_lo, e2_hi)`, `expTypes`] \\ fs[]) >- (DISJ2_TAC \\ irule REAL_LTE_TRANS \\ qexists_tac `e2_lo - err_e2` \\ fs[] \\ fs[real_sub] \\ irule REAL_LE_TRANS \\ qexists_tac `e2_lo + 0:real` \\ fs[] \\ irule err_always_positive \\ qexistsl_tac [`absenv`, `dVars`, `e2`, `(e2_lo, e2_hi)`, `expTypes`] \\ fs[])) >- (qexists_tac `mF1` \\ fs[]) >- (qexists_tac `mF2` \\ fs[]) >- (once_rewrite_tac [validErrorbound_def] \\ fs[]) >- (simp [Once toREval_def] \\ irule Binop_dist' \\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`] \\ fs[perturb_def, mTypeToQ_pos]))) >- (rename1 `Fma e1 e2 e3` \\ Cases_on `expTypes (Fma e1 e2 e3)` \\ fs[] \\ Cases_on `absenv e1` \\ rename1 `absenv e1 = (iv_e1, err_e1)` \\ Cases_on `iv_e1` \\ rename1 `absenv e1= ((e1_lo, e1_hi), err_e1)` \\ Cases_on `absenv e2` \\ rename1 `absenv e2 = (iv_e2, err_e2)` \\ Cases_on `iv_e2` \\ rename1 `absenv e2 = ((e2_lo, e2_hi), err_e2)` \\ Cases_on `absenv e3` \\ rename1 `absenv e3 = (iv_e3, err_e3)` \\ Cases_on `iv_e3` \\ rename1 `absenv e3 = ((e3_lo, e3_hi), err_e3)` \\ rw_thm_asm `eval_exp E1 _ _ _ _` toREval_def \\ fs[] \\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases \\ `m1 = M0 /\ m2 = M0 /\ m3 = M0` by (rpt (conj_tac) \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[]) \\ rveq \\ `(?nF1 m1. eval_exp E2 Gamma e1 nF1 m1) /\ (!nF1 m1. eval_exp E2 Gamma e1 nF1 m1 ==> abs (v1 - nF1) <= err_e1)` by (first_x_assum irule \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e1_hi`, `e1_lo`, `expTypes`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_asm_star `expTypes _ = _` \\ Cases_on `expTypes e1` \\ Cases_on `expTypes e2` \\ Cases_on `expTypes e3` \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `(?nF2 m2. eval_exp E2 Gamma e2 nF2 m2) /\ (!nF2 m2. eval_exp E2 Gamma e2 nF2 m2 ==> abs (v2 - nF2) <= err_e2)` by (first_x_assum irule \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e2_hi`, `e2_lo`, `expTypes`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_asm_star `expTypes _ = _` \\ Cases_on `expTypes e1` \\ Cases_on `expTypes e2` \\ Cases_on `expTypes e3` \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `(?nF3 m3. eval_exp E2 Gamma e3 nF3 m3) /\ (!nF3 m3. eval_exp E2 Gamma e3 nF3 m3 ==> abs (v3 - nF3) <= err_e3)` by (first_x_assum irule \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e3_hi`, `e3_lo`, `expTypes`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_asm_star `expTypes _ = _` \\ Cases_on `expTypes e1` \\ Cases_on `expTypes e2` \\ Cases_on `expTypes e3` \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?nR1. eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ fs [DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?nR2. eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ FST (FST (absenv e2)) <= nR2 /\ nR2 <= SND (FST (absenv e2))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ fs [DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?nR3. eval_exp E1 (toRMap Gamma) (toREval e3) nR3 M0 /\ FST (FST (absenv e3)) <= nR3 /\ nR3 <= SND (FST (absenv e3))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ fs [DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `nR1 = v1 /\ nR2 = v2 /\ nR3 = v3` by (metis_tac[meps_0_deterministic]) \\ rveq \\ rw_asm_star `absenv e1 = _` \\ rw_asm_star `absenv e2 = _` \\ rw_asm_star `absenv e3 = _` \\ `contained nF1 (widenInterval (e1_lo,e1_hi) err_e1)` by (irule distance_gives_iv \\ qexists_tac `nR1` \\ fs[contained_def, IVlo_def, IVhi_def] \\ first_x_assum irule \\ qexists_tac `m1` \\ fs[]) \\ `contained nF2 (widenInterval (e2_lo, e2_hi) err_e2)` by (irule distance_gives_iv \\ qexists_tac `nR2` \\ fs [contained_def, IVlo_def, IVhi_def] \\ first_x_assum irule \\ qexists_tac `m2` \\ fs[]) \\ `contained nF3 (widenInterval (e3_lo, e3_hi) err_e3)` by (irule distance_gives_iv \\ qexists_tac `nR3` \\ fs [contained_def, IVlo_def, IVhi_def] \\ first_x_assum irule \\ qexists_tac `m3` \\ fs[]) \\ conj_tac >- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) 0`, `join3 m1 m2 m3`] \\ irule Fma_dist' \\ qexistsl_tac [`0`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`] \\ fs[mTypeToQ_pos]) \\ rpt strip_tac \\ `perturb (evalFma nR1 nR2 nR3) delta = evalFma nR1 nR2 nR3` by (irule delta_0_deterministic \\ fs[mTypeToQ_def, join3_def, join_def]) \\ fs[] \\ inversion `eval_exp E2 _ (Fma e1 e2 e3) _ _` eval_exp_cases \\ rename1 `abs delta2 <= mTypeToQ (join3 mF1 mF2 mF3)` \\ `eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv))) (updDefVars 3 mF3 (updDefVars 2 mF2 (updDefVars 1 mF1 Gamma))) (Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) delta2) (join3 mF1 mF2 mF3)` by (irule fma_unfolding \\ fs[] \\ qexistsl_tac [`E2`, `e1`, `e2`, `e3`] \\ fs[eval_exp_cases] \\ qexistsl_tac [`mF1`, `mF2`, `mF3`, `v1`, `v2`, `v3`, `delta2`] \\ fs[]) \\ rveq >- (irule validErrorboundCorrectFma \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`, `e1`, `e1_hi`, `e1_lo`, `e2`,`e2_hi`, `e2_lo`, `e3`, `e3_hi`, `e3_lo`, `err_e1`, `err_e2`, `err_e3`, `expTypes`, `join3 mF1 mF2 mF3`, `mF1`, `mF2`, `mF3`, `v1`, `v2`, `v3`, `nR1`, `nR2`, `nR3`] \\ fs[] \\ rpt conj_tac \\ TRY (first_x_assum irule) >- (qexists_tac `mF1` \\ fs[]) >- (qexists_tac `mF2` \\ fs[]) >- (qexists_tac `mF3` \\ fs[]) >- (once_rewrite_tac [validErrorbound_def] \\ fs[]) >- (simp [Once toREval_def] \\ irule Fma_dist' \\ qexistsl_tac [`0`, `M0`, `M0`, `M0`, `nR1`, `nR2`, `nR3`] \\ fs[perturb_def, mTypeToQ_pos]))) >- (rename1 `Downcast m1 e1` \\ Cases_on `expTypes (Downcast m1 e1)` \\ fs[] \\ Cases_on `absenv e1` \\ rename1 `absenv e1 = (iv_e1, err_e1)` \\ Cases_on `iv_e1` \\ rename1 `absenv e1= ((e1_lo, e1_hi), err_e1)` \\ rw_thm_asm `eval_exp E1 _ _ _ _` toREval_def \\ fs[] \\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases \\ rveq \\ `(?nF1 m1. eval_exp E2 Gamma e1 nF1 m1) /\ (!nF1 m1. eval_exp E2 Gamma e1 nF1 m1 ==> abs (nR - nF1) <= err_e1)` by (first_x_assum irule \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e1_hi`, `e1_lo`, `expTypes`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_thm_asm `domain _ DIFF _ SUBSET _` usedVars_def \\ rw_asm_star `expTypes _ = _` \\ Cases_on `expTypes e1` \\ fs[]) \\ `?nR1. eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ FST (FST (absenv e1)) <= nR1 /\ nR1 <= SND (FST (absenv e1))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[Once validIntervalbounds_def] \\ rw_thm_asm `domain _ DIFF _ SUBSET _` usedVars_def \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ fs []) \\ `nR1 = nR` by (metis_tac[meps_0_deterministic]) \\ rveq \\ rw_asm_star `absenv e1 = _` \\ `contained nF1 (widenInterval (e1_lo,e1_hi) err_e1)` by (irule distance_gives_iv \\ qexists_tac `nR` \\ fs[contained_def, IVlo_def, IVhi_def] \\ first_x_assum irule \\ asm_exists_tac \\ fs[]) \\ conj_tac >- (qexistsl_tac [`perturb nF1 (mTypeToQ m1)`, `m1`] \\ fs[eval_exp_cases] \\ rename1 `eval_exp E2 Gamma e1 nF1 me1` \\ qexistsl_tac [`me1`, `nF1`, `mTypeToQ m1`] \\ fs[] \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ rw_asm_star `expTypes (Downcast m1 e1) = _` \\ Cases_on `expTypes e1` \\ fs[] \\ `expTypes e1 = SOME me1` by (irule typingSoundnessExp \\ qexistsl_tac [`E2`, `Gamma`, `nF1`] \\ fs[]) \\ rw_asm_star `expTypes e1 = _` \\ `abs (mTypeToQ m1) = mTypeToQ m1` by (fs [realTheory.ABS_REFL, mTypeToQ_pos]) \\ fs[]) >- (rpt strip_tac \\ irule validErrorboundCorrectRounding \\ qpat_x_assum `eval_exp E2 _ e1 _ _` kall_tac \\ inversion `eval_exp E2 _ (Downcast m1 e1) _ _` eval_exp_cases \\ rename1 `eval_exp E2 Gamma e1 v1 me1` \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `absenv`, `ehi`, `elo`, `dVars`, `e1`, `e1_hi`, `e1_lo`, `err_e1`, `expTypes`, `me1`, `m1`, `v1`] \\ fs[] \\ rpt conj_tac >- (first_x_assum irule \\ qexists_tac `me1` \\ fs[]) >- (simp [Once validErrorbound_def]) >- (irule Downcast_dist' \\ fs[] \\ qexistsl_tac [`delta`, `me1`, `v1`] \\ fs[] \\ irule Var_load \\ fs[updDefVars_def, updEnv_def])))); val validErrorboundCmd_gives_eval = store_thm ( "validErrorboundCmd_gives_eval", ``!(f:real cmd) (absenv:analysisResult) (E1 E2:env) (outVars fVars dVars:num_set) (vR elo ehi err:real) (P:precond) (m:mType) expTypes Gamma. typeCheckCmd f Gamma expTypes /\ approxEnv E1 Gamma absenv fVars dVars E2 /\ ssa f (union fVars dVars) outVars /\ ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\ bstep (toREvalCmd f) E1 (toRMap Gamma) vR M0 /\ validErrorboundCmd f expTypes absenv dVars /\ validIntervalboundsCmd f absenv P dVars /\ (!v. v IN domain dVars ==> ?r. (E1 v = SOME r) /\ FST (FST (absenv (Var v))) <= r /\ r <= SND (FST (absenv (Var v)))) /\ (!v. v IN domain fVars ==> ?r. (E1 v = SOME r) /\ FST (P v) <= r /\ r <= SND (P v)) /\ (!v. v IN domain fVars \/ v IN domain dVars ==> ?m. Gamma v = SOME m) /\ (absenv (getRetExp f) = ((elo,ehi),err)) ==> ?vF m. bstep f E2 Gamma vF m``, Induct_on `f` \\ rpt strip_tac >- (rw_thm_asm `bstep (toREvalCmd _) _ _ _ _` toREvalCmd_def \\ rw_thm_asm `absenv (getRetExp _) = _` getRetExp_def \\ rw_thm_asm `validErrorboundCmd _ _ _ _` validErrorboundCmd_def \\ fs[] \\ inversion `bstep _ _ _ _ _` bstep_cases \\ inversion `ssa _ _ _` ssa_cases \\ Cases_on `absenv e` \\ rename1 `absenv e = (iv_e, err_e)` \\ Cases_on `iv_e` \\ rename1 `absenv e = ((e_lo,e_hi), err_e)` \\ `(?vF m. eval_exp E2 Gamma e vF m) /\ !vF m. eval_exp E2 Gamma e vF m ==> abs (v - vF) <= SND (absenv e)` by (irule validErrorbound_sound \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `e_hi`, `e_lo`, `expTypes`, `fVars`] \\ qpat_x_assum `((e_lo,e_hi), err_e) = absenv (Var n)` kall_tac (* Hypothesis confuses HOL4...*) \\ rw_thm_asm `domain (freeVars _) DIFF _ SUBSET _` freeVars_def \\ fs[Once typeCheckCmd_def, Once validIntervalboundsCmd_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rpt strip_tac \\ first_assum irule \\ fs[] \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[SUBSET_DEF, domain_union] \\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[])) \\ rename1 `eval_exp E2 Gamma e vF mF` \\ `approxEnv (updEnv n v E1) (updDefVars n m Gamma) absenv fVars (insert n () dVars) (updEnv n vF E2)` by (irule approxUpdBound \\ fs[lookup_NONE_domain] \\ `absenv (Var n) = absenv e` by (fs[]) \\ qpat_x_assum `absenv (Var n) = absenv e` (fn thm => once_rewrite_tac [thm]) \\ first_x_assum irule \\ qexists_tac `mF` \\ fs[]) \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def \\ `expTypes e = SOME mF` by (irule typingSoundnessExp \\ qexistsl_tac [`E2`, `Gamma`, `vF`] \\ fs[]) \\ fs[] \\ Cases_on `expTypes (Var n)` \\ fs[] \\ `?vF_res m_res. bstep f (updEnv n vF E2) (updDefVars n mF Gamma) vF_res m_res` by (first_x_assum irule \\ qexistsl_tac [`updEnv n v E1`, `P`, `absenv`, `insert n () dVars`, `ehi`, `elo`, `err`, `expTypes`, `fVars`, `outVars`, `vR`] \\ rw_thm_asm `validIntervalboundsCmd _ _ _ _` validIntervalboundsCmd_def \\ fs[] \\ rpt conj_tac >- (rpt gen_tac \\ disch_then assume_tac \\ simp[updEnv_def] \\ rename1 `v2 = n \/ v2 IN domain dVars` \\ Cases_on `v2 = n` \\ fs[] \\ `absenv (Var n) = absenv e` by (fs[]) \\ qpat_x_assum `absenv (Var n) = absenv e` (fn thm => once_rewrite_tac [thm]) \\ `?vR. eval_exp E1 (toRMap Gamma) (toREval e) vR M0 /\ FST( FST(absenv e)) <= vR /\ vR <= SND (FST (absenv e))` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] \\ fs[Once freeVars_def, domain_union, DIFF_DEF, SUBSET_DEF] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rpt strip_tac \\ first_x_assum irule \\ fs[] \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[SUBSET_DEF, domain_union] \\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[])) \\ rename1 `eval_exp E1 _ (toREval e) vR2 M0` \\ `v = vR2` by (metis_tac[meps_0_deterministic]) \\ rveq \\ conj_tac \\ (first_x_assum MATCH_ACCEPT_TAC)) >- (rpt strip_tac \\ simp[updEnv_def] \\ IF_CASES_TAC \\ fs[] \\ rveq \\ fs[domain_union]) >- (rpt gen_tac \\ disch_then assume_tac \\ fs[updDefVars_def] \\ IF_CASES_TAC \\ fs[]) >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ fs[Once freeVars_def] \\ simp[Once freeVars_def, domain_union]) >- (irule ssa_equal_set \\ qexists_tac `insert n () (union fVars dVars)` \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "") \\ rewrite_tac [domain_union, domain_insert] \\ rewrite_tac [UNION_DEF, INSERT_DEF] \\ fs[EXTENSION] \\ rpt strip_tac \\ metis_tac[]) >- (irule swap_Gamma_bstep \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[] \\ MATCH_ACCEPT_TAC Rmap_updVars_comm)) \\ qexistsl_tac [`vF_res`, `m_res`] \\ fs[bstep_cases] \\ qexists_tac `vF` \\ rveq \\ fs[]) >- (rw_thm_asm `validErrorboundCmd _ _ _ _` validErrorboundCmd_def \\ rw_thm_asm `validIntervalboundsCmd _ _ _ _` validIntervalboundsCmd_def \\ rw_thm_asm `domain (freeVars _) DIFF _ SUBSET _` freeVars_def \\ rw_thm_asm `bstep (toREvalCmd _) _ _ _ _` toREvalCmd_def \\ fs[getRetExp_def] \\ inversion `ssa _ _ _` ssa_cases \\ inversion `bstep _ _ _ _ _` bstep_cases \\ once_rewrite_tac [bstep_cases] \\ `(?vF m. eval_exp E2 Gamma e vF m) /\ (!vF m. eval_exp E2 Gamma e vF m ==> abs (vR - vF) <= err)` by (irule validErrorbound_sound \\ qexistsl_tac [`E1`, `P`, `absenv`, `dVars`, `ehi`, `elo`, `expTypes`, `fVars`] \\ fs[typeCheckCmd_def] \\ first_x_assum MATCH_ACCEPT_TAC) \\ qexistsl_tac [`vF`, `m`] \\ fs[])); val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound", ``!(f:real cmd) (absenv:analysisResult) (E1 E2:env) (outVars fVars dVars:num_set) (vR vF elo ehi err:real) (P:precond) (m:mType) expTypes Gamma. typeCheckCmd f Gamma expTypes /\ approxEnv E1 Gamma absenv fVars dVars E2 /\ ssa f (union fVars dVars) outVars /\ ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\ bstep (toREvalCmd f) E1 (toRMap Gamma) vR M0 /\ bstep f E2 Gamma vF m /\ validErrorboundCmd f expTypes absenv dVars /\ validIntervalboundsCmd f absenv P dVars /\ (!v. v IN domain dVars ==> ?r. (E1 v = SOME r) /\ FST (FST (absenv (Var v))) <= r /\ r <= SND (FST (absenv (Var v)))) /\ (!v. v IN domain fVars ==> ?r. (E1 v = SOME r) /\ FST (P v) <= r /\ r <= SND (P v)) /\ (!v. v IN domain fVars \/ v IN domain dVars ==> ?m. Gamma v = SOME m) /\ (absenv (getRetExp f) = ((elo,ehi),err)) ==> abs (vR - vF) <= err``, Induct_on `f` \\ rpt strip_tac >- (qpat_x_assum `bstep (toREvalCmd _) _ _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREvalCmd_def] thm)) \\ fs [] \\ inversion `bstep _ _ _ _ M0` bstep_cases \\ rveq \\ inversion `bstep _ _ _ _ m'` bstep_cases \\ rveq \\ inversion `ssa _ _ _` ssa_cases \\ rveq \\ rename1 `eval_exp _ _ _ vr M0` \\ rename1 `eval_exp _ _ _ vf m` \\ first_x_assum match_mp_tac \\ rw_thm_asm `validErrorboundCmd _ _ _ _` validErrorboundCmd_def \\ rw_thm_asm `validIntervalboundsCmd _ _ _ _` validIntervalboundsCmd_def \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def \\ `expTypes e = SOME m` by (irule typingSoundnessExp \\ qexistsl_tac [`E2`, `Gamma`, `vf`] \\ fs[]) \\ Cases_on `expTypes (Var n)` \\ fs[] \\ qexistsl_tac [`absenv`, `updEnv n vr E1`, `updEnv n vf E2`, `outVars`, `fVars`, `insert n () dVars`, `elo`, `ehi`, `P`, `m'`, `expTypes`, `updDefVars n m Gamma`] \\ fs [Once getRetExp_def] \\ rpt conj_tac >- (irule approxUpdBound \\ fs[] \\ qpat_x_assum `absenv e = _` (fn thm => simp[GSYM thm]) >- (Cases_on `lookup n (union fVars dVars)` \\ fs [domain_lookup]) >- (Cases_on `absenv e` \\ rename1 `absenv e = (iv, err_e)` \\ fs [] \\ Cases_on `iv` \\ rename1 `absenv e = ((e_lo, e_hi), err_e)` \\ qspecl_then [`e`, `E1`, `E2`, `absenv`, `vr`, `err_e`, `P`, `e_lo`, `e_hi`, `fVars`, `dVars`, `expTypes`, `Gamma`] destruct validErrorbound_sound \\ fs [Once freeVars_def, domain_union, SUBSET_DEF] >- (conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ rpt strip_tac \\ first_x_assum irule \\ fs[] \\ CCONTR_TAC \\ fs[] \\ rveq \\ `n IN domain fVars \/ n IN domain dVars` by metis_tac[]) >- (first_x_assum irule \\ asm_exists_tac \\ fs[]))) >- (match_mp_tac ssa_equal_set \\ qexists_tac `insert n () (union fVars dVars)` \\ fs [ domain_union] \\ once_rewrite_tac [UNION_COMM] \\ fs [INSERT_UNION_EQ]) >- (fs [SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum match_mp_tac \\ once_rewrite_tac [freeVars_def] \\ fs [domain_union]) >- (irule swap_Gamma_bstep \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[Rmap_updVars_comm]) >- (rpt gen_tac \\ disch_then assume_tac \\ simp[updEnv_def] \\ Cases_on `(v = n)` \\ fs [] \\ rveq \\ qpat_x_assum `FST (absenv e) = FST (absenv _)` (fn thm => once_rewrite_tac [GSYM thm]) \\ qpat_x_assum `absenv e = absenv _` kall_tac \\ qspecl_then [`e`, `absenv`, `P`, `fVars`, `dVars`, `E1`, `Gamma`] destruct validIntervalbounds_sound \\ TRY (metis_tac[meps_0_deterministic]) \\ fs [Once validIntervalboundsCmd_def] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) \\ fs [DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule \\ fs[] \\ simp [Once freeVars_def, domain_union] \\ metis_tac[]) >- (rpt strip_tac \\ fs [updEnv_def] \\ Cases_on `n = v` \\ rveq \\ fs [] \\ fs [domain_union]) >- (rpt gen_tac \\ disch_then assume_tac \\ simp[updDefVars_def] \\ Cases_on `v = n` \\ fs[])) >- (fs [Once toREvalCmd_def] \\ inversion `bstep _ _ _ _ M0` bstep_cases \\ rveq \\ inversion `bstep _ _ _ _ m` bstep_cases \\ rveq \\ rw_thm_asm `validErrorboundCmd _ _ _ _` validErrorboundCmd_def \\ rw_thm_asm `validIntervalboundsCmd _ _ _ _` validIntervalboundsCmd_def \\ fs [] \\ qspecl_then [`e`, `E1`, `E2`, `absenv`, `vR`, `err`, `P`, `elo`, `ehi`, `fVars`, `dVars`, `expTypes`, `Gamma`] destruct validErrorbound_sound \\ fs[freeVars_def, getRetExp_def, typeCheckCmd_def] >- (first_x_assum MATCH_ACCEPT_TAC) >- (first_x_assum irule \\ asm_exists_tac \\ fs[]))); val _ = export_theory();