diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml index 64ceb56dd5c1742d9e6ccc668f2869c51f12483a..e0bd75371875af8944d75ee409bc4ae32cc19615 100644 --- a/hol4/ErrorBoundsScript.sml +++ b/hol4/ErrorBoundsScript.sml @@ -201,6 +201,52 @@ val div_abs_err_bounded = store_thm ("div_abs_err_bounded", \\ once_rewrite_tac[REAL_ABS_MUL] \\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS])); +val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded", + ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (e3:real exp) (e3R:real) (e3F:real) (err1:real) (err2:real) (err3:real) + (vR:real) (vF:real) (E1 E2 :env) (m m1 m2 m3:mType) (defVars: num -> mType option). + eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\ + eval_exp E2 defVars e1 e1F m1 /\ + eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\ + eval_exp E2 defVars e2 e2F m2 /\ + eval_exp E1 (toRMap defVars) (toREval e3) e3R M0 /\ + eval_exp E2 defVars e3 e3F m3 /\ + eval_exp E1 (toRMap defVars) (toREval (Fma e1 e2 e3)) vR M0 /\ + eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars))) (Fma (Var 1) (Var 2) (Var 3)) vF m /\ + abs (e1R - e1F) <= err1 /\ + abs (e2R - e2F) <= err2 /\ + abs (e3R - e3F) <= err3 ==> + abs (vR - vF) <= abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + abs (e1F + e2F * e3F) * (mTypeToQ m)``, + rpt strip_tac + \\ qpat_x_assum `eval_exp E1 _ (toREval (Fma e1 e2 e3)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)) + \\ fs [] + \\ inversion `eval_exp E1 _ (Fma _ _ _) _ _` eval_exp_cases + \\ rename1 `vR = perturb (evalFma v1R v2R v3R) deltaR` + \\ inversion `eval_exp _ _ (Fma (Var 1) (Var 2) (Var 3)) _ _` eval_exp_cases + \\ rename1 `vF = perturb (evalFma v1F v2F v3F) deltaF` + \\ `(m1' = M0) /\ (m2' = M0) /\ (m3' = M0)` by (rpt conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs [] + \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm])) + \\ `perturb (evalFma v1R v2R v3R) deltaR = evalFma v1R v2R v3R` by (match_mp_tac delta_M0_deterministic \\ fs[]) + \\ `vR = evalFma v1R v2R v3R` by simp[] + \\ `v1R = e1R` by metis_tac[meps_0_deterministic] + \\ `v2R = e2R` by metis_tac[meps_0_deterministic] + \\ `v3R = e3R` by metis_tac[meps_0_deterministic] + \\ fs[evalFma_def, evalBinop_def, perturb_def] + \\ rpt (inversion `eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) _ _ _ _` eval_exp_cases) + \\ fs [updEnv_def] \\ rveq + \\ fs [updDefVars_def] \\ rveq + \\ rewrite_tac [real_sub] + \\ `e1R + e2R * e3R + -((e1F + e2F * e3F) * (1 + deltaF)) = (e1R + e2R * e3R + -(e1F + e2F * e3F)) + (- (e1F + e2F * e3F) * deltaF)` by REAL_ASM_ARITH_TAC + \\ simp[] + \\ qspecl_then [`abs (e1R + e2R * e3R + -(e1F + e2F * e3F)) + abs (-(e1F + e2F * e3F) * deltaF)`] match_mp_tac real_le_trans2 + \\ conj_tac + >- (REAL_ASM_ARITH_TAC) + >- (match_mp_tac REAL_LE_ADD2 + \\ conj_tac \\ TRY (REAL_ASM_ARITH_TAC) + \\ once_rewrite_tac[REAL_ABS_MUL] + \\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS] + \\ once_rewrite_tac[GSYM REAL_NEG_LMUL, REAL_ABS_MUL] + \\ once_rewrite_tac[ABS_NEG] \\ fs[])); + val round_abs_err_bounded = store_thm ("round_abs_err_bounded", ``!(e:real exp) (nR:real) (nF1:real) (nF:real) (E1:env) (E2:env) (err:real) (machineEpsilon:mType) (m:mType) (defVars: num -> mType option). eval_exp E1 (toRMap defVars) (toREval e) nR M0 /\ diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml index 9991cbf6de2d2828e69e1da0c8115ec355938ba1..ad0088744c0f346aae0733d3f0585ab6fef86528 100644 --- a/hol4/ErrorValidationScript.sml +++ b/hol4/ErrorValidationScript.sml @@ -55,6 +55,23 @@ val validErrorbound_def = Define ` ((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 @@ -85,6 +102,7 @@ val err_always_positive = store_thm ( >- (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 ( @@ -362,6 +380,597 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra \\ 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. @@ -417,583 +1026,7 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult", (widenInterval (e2lo,e2hi) err2)) * (mTypeToQ (join m1 m2))` \\ conj_tac \\ TRY(simp[]) \\ match_mp_tac REAL_LE_ADD2 \\ conj_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]))))))) + >- (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] @@ -2121,6 +2154,111 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv", 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. @@ -2424,6 +2562,142 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ 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)` diff --git a/hol4/ExpressionsScript.sml b/hol4/ExpressionsScript.sml index 8ab22ef11fcd78c71a2da834897c74ae54c8754f..3f2ce863ee9665e82ef86c963eada61e177e26de 100644 --- a/hol4/ExpressionsScript.sml +++ b/hol4/ExpressionsScript.sml @@ -52,15 +52,24 @@ val _ = Datatype ` | Const mType 'v | Unop unop exp | Binop binop exp exp + | Fma exp exp exp | Downcast mType exp` +(** + Define evaluation of FMA (fused multiply-add) on reals + Errors are added on the expression evaluation level later +**) +val evalFma_def = Define ` + evalFma v1 v2 v3 = evalBinop Plus v1 (evalBinop Mult v2 v3)` + val toREval_def = Define ` toREval e :real exp = case e of | (Var n) => Var n | (Const m n) => Const M0 n - | (Unop u e1) => Unop u (toREval e1) + | (Unop u e1) => Unop u (toREval e1) | (Binop bop e1 e2) => Binop bop (toREval e1) (toREval e2) + | (Fma e1 e2 e3) => Fma (toREval e1) (toREval e2) (toREval e3) | (Downcast m e1) => (toREval e1)`; (** @@ -101,7 +110,13 @@ val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln ` eval_exp E defVars f1 v1 m1 /\ eval_exp E defVars f2 v2 m2 /\ ((b = Div) ==> (v2 <> 0)) ==> - eval_exp E defVars (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2))`; + eval_exp E defVars (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2)) /\ + (!E defVars m1 m2 m3 f1 f2 f3 v1 v2 v3 delta. + abs delta <= (mTypeToQ (join3 m1 m2 m3)) /\ + eval_exp E defVars f1 v1 m1 /\ + eval_exp E defVars f2 v2 m2 /\ + eval_exp E defVars f3 v3 m3 ==> + eval_exp E defVars (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3))`; val eval_exp_cases_old = save_thm ("eval_exp_cases_old", eval_exp_cases); @@ -114,15 +129,17 @@ val eval_exp_cases = ``eval_exp E defVars (Const m1 n) res m2``, ``eval_exp E defVars (Unop u e) res m``, ``eval_exp E defVars (Binop n e1 e2) res m``, + ``eval_exp E defVars (Fma e1 e2 e3) res m``, ``eval_exp E defVars (Downcast m1 e1) res m2``] |> LIST_CONJ |> curry save_thm "eval_exp_cases"; -val [Var_load, Const_dist, Unop_neg, Unop_inv, Downcast_dist, Binop_dist] = CONJ_LIST 6 eval_exp_rules; +val [Var_load, Const_dist, Unop_neg, Unop_inv, Downcast_dist, Binop_dist, Fma_dist] = CONJ_LIST 7 eval_exp_rules; save_thm ("Var_load", Var_load); save_thm ("Const_dist", Const_dist); save_thm ("Unop_neg", Unop_neg); save_thm ("Unop_inv", Unop_inv); save_thm ("Binop_dist", Binop_dist); +save_thm ("Fma_dist", Fma_dist); save_thm ("Downcast_dist", Downcast_dist); (** @@ -182,6 +199,17 @@ val Binop_dist' = store_thm ("Binop_dist'", eval_exp E Gamma (Binop op f1 f2) v m'``, fs [Binop_dist]); +val Fma_dist' = store_thm ("Fma_dist'", + ``!m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma. + (abs delta) <= (mTypeToQ m') /\ + eval_exp E Gamma f1 v1 m1 /\ + eval_exp E Gamma f2 v2 m2 /\ + eval_exp E Gamma f3 v3 m3 /\ + v = perturb (evalFma v1 v2 v3) delta /\ + m' = join3 m1 m2 m3 ==> + eval_exp E Gamma (Fma f1 f2 f3) v m'``, + fs [Fma_dist]); + (** Define the set of "used" variables of an expression to be the set of variables occuring in it @@ -192,6 +220,7 @@ val usedVars_def = Define ` | Var x => insert x () (LN) | Unop u e1 => usedVars e1 | Binop b e1 e2 => union (usedVars e1) (usedVars e2) + | Fma e1 e2 e3 => union (usedVars e1) (union (usedVars e2) (usedVars e3)) | Downcast m e1 => usedVars e1 | _ => LN`; @@ -223,7 +252,11 @@ val toRMap_eval_M0 = store_thm ( >- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[]) >- (`m1 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) \\ `m2 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) - \\ rveq \\ fs[join_def])); + \\ rveq \\ fs[join_def]) + >- (`m1 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) + \\ `m2 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) + \\ `m3 = M0` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) + \\ rveq \\ fs[join3_def] \\ fs[join_def])); (** Evaluation with 0 as machine epsilon is deterministic @@ -264,6 +297,20 @@ val meps_0_deterministic = store_thm("meps_0_deterministic", \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`vf11`,`vf12`] ASSUME_TAC thm) \\ res_tac \\ rw[]) + >- (rw[] + \\ rpt ( + qpat_x_assum `eval_exp _ _ (toREval _) _ _` + (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))) + \\ fs [eval_exp_cases] + \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs []) + \\ `m3 = M0` by (irule toRMap_eval_M0 \\ asm_exists_tac \\ fs []) + \\ `m1' = M0 /\ m2' = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs []) + \\ `m3' = M0` by (irule toRMap_eval_M0 \\ asm_exists_tac \\ fs []) + \\ rw[] + \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v3`,`v3'`, `E`, `defVars`] ASSUME_TAC thm) + \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v2'`,`v2''`, `E`, `defVars`] ASSUME_TAC thm) + \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v1'`,`v1''`, `E`, `defVars`] ASSUME_TAC thm) + \\ fs [join3_def, join_def, mTypeToQ_def, delta_0_deterministic]) >- (rw[] \\ rpt ( qpat_x_assum `eval_exp _ _ (toREval (Downcast _ _)) _ _` @@ -272,10 +319,10 @@ val meps_0_deterministic = store_thm("meps_0_deterministic", \\ res_tac)); (** -Helping lemma. Needed in soundness proof. +Helping lemmas. Needed in soundness proof. For each evaluation of using an arbitrary epsilon, we can replace it by evaluating the subExpressions and then binding the result values to different -variables in the Eironment. +variables in the Environment. **) val binary_unfolding = store_thm("binary_unfolding", ``!(b:binop) (f1:(real)exp) (f2:(real)exp) E Gamma (v:real) v1 v2 m1 m2 delta. @@ -290,6 +337,21 @@ val binary_unfolding = store_thm("binary_unfolding", fs [updEnv_def,updDefVars_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS] \\ metis_tac []); +val fma_unfolding = store_thm("fma_unfolding", + ``!(f1:(real)exp) (f2:(real)exp) (f3:(real)exp) E Gamma (v:real) v1 v2 v3 m1 m2 m3 delta. + (abs delta) <= (mTypeToQ (join3 m1 m2 m3)) /\ + eval_exp E Gamma f1 v1 m1 /\ + eval_exp E Gamma f2 v2 m2 /\ + eval_exp E Gamma f3 v3 m3 /\ + eval_exp E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3) ==> + eval_exp (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv))) + (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 Gamma))) + (Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) delta) (join3 m1 m2 m3)``, + fs [updEnv_def,updDefVars_def,join3_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS] + \\ rpt strip_tac + \\ qexists_tac `delta'` + \\ conj_tac \\ fs[]); + val eval_eq_env = store_thm ( "eval_eq_env", ``!e E1 E2 Gamma v m. @@ -307,6 +369,8 @@ val eval_eq_env = store_thm ( \\ first_x_assum drule \\ disch_then irule \\ fs[]) >- (rveq \\ qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta'`] \\ fs[] \\ conj_tac \\ first_x_assum irule \\ asm_exists_tac \\ fs[]) + >- (rveq \\ qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta'`] + \\ fs[] \\ prove_tac []) >- (rveq \\ qexistsl_tac [`m1'`, `v1`, `delta'`] \\ fs[] \\ first_x_assum drule \\ disch_then irule \\ fs[])); diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml index 238fb449da7b237b0cc381e1b4760de6472b653d..62fc24e47c679e683939270d64ab77942c93a54d 100644 --- a/hol4/FPRangeValidatorScript.sml +++ b/hol4/FPRangeValidatorScript.sml @@ -31,6 +31,10 @@ val FPRangeValidator_def = Define ` | Binop b e1 e2 => FPRangeValidator e1 A typeMap dVars /\ FPRangeValidator e2 A typeMap dVars + | Fma e1 e2 e3 => + FPRangeValidator e1 A typeMap dVars /\ + FPRangeValidator e2 A typeMap dVars /\ + FPRangeValidator e3 A typeMap dVars | Unop u e => FPRangeValidator e A typeMap dVars | Downcast m e => FPRangeValidator e A typeMap dVars diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml index 876b3fd7ada24587bdd63054b5dee973f84cccfa..c07465a061f2192a5369859616c2d1174e65189a 100644 --- a/hol4/IEEE_connectionScript.sml +++ b/hol4/IEEE_connectionScript.sml @@ -39,6 +39,9 @@ val eval_exp_float_def = Define ` | Mult => SOME (fp64_mul dmode v1 v2) | Div => SOME (fp64_div dmode v1 v2)) | _, _ => NONE)) /\ + (eval_exp_float (Fma e1 e2 e3) E = + (case (eval_exp_float e1 E), (eval_exp_float e2 E), (eval_exp_float e2 E) of + | _, _, _ => NONE)) /\ (eval_exp_float (Downcast m e) E = NONE)`; val bstep_float_def = Define ` @@ -75,6 +78,24 @@ val eval_exp_valid_def = Define ` normal_or_zero (evalBinop b v1_real v2_real)) T) T)) /\ + (eval_exp_valid (Fma e1 e2 e3) E = + (eval_exp_valid e1 E /\ eval_exp_valid e2 E /\ eval_exp_valid e3 E /\ + let e1_res = eval_exp_float e1 E in + let e2_res = eval_exp_float e2 E in + let e3_res = eval_exp_float e3 E in + optionLift (e1_res) + (\ v1. let v1_real = float_to_real (fp64_to_float v1) + in + optionLift e2_res + (\ v2. + let v2_real = float_to_real (fp64_to_float v2) + in + optionLift e3_res + (\ v3. let v3_real = float_to_real (fp64_to_float v3) in + F) + T) + T) + T)) /\ (eval_exp_valid (Downcast m e) E = eval_exp_valid e E)`; val bstep_valid_def = Define ` @@ -90,6 +111,7 @@ val toRExp_def = Define ` (toRExp (Const m c) = Const m (float_to_real (fp64_to_float c))) /\ (toRExp (Unop u e1) = Unop u (toRExp e1)) /\ (toRExp (Binop b e1 e2) = Binop b (toRExp e1) (toRExp e2)) /\ + (toRExp (Fma e1 e2 e3) = Fma (toRExp e1) (toRExp e2) (toRExp e3)) /\ (toRExp (Downcast m e1) = Downcast m (toRExp e1))`; val toRCmd_def = Define ` @@ -436,6 +458,7 @@ val noDowncast_def = Define ` (noDowncast (Const _ _) = T) /\ (noDowncast (Unop _ e) = noDowncast e) /\ (noDowncast (Binop b e1 e2) = (noDowncast e1 /\ noDowncast e2)) /\ + (noDowncast (Fma e1 e2 e3) = (noDowncast e1 /\ noDowncast e2 /\ noDowncast e3)) /\ (noDowncast (Downcast _ _) = F)`; val noDowncastFun_def = Define ` @@ -453,6 +476,7 @@ val is64BitEval_def = Define ` (is64BitEval ((Const m c):real exp) = (m = M64)) /\ (is64BitEval (Unop _ e) = is64BitEval e) /\ (is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\ + (is64BitEval (Fma e1 e2 e3) = (is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3)) /\ (is64BitEval (Downcast m e) = is64BitEval e) /\ (is64BitEval ((Var v):real exp) = T)`; @@ -502,7 +526,30 @@ Induct \\ qexists_tac `Gamma` \\ rpt strip_tac >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union]) \\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ fs[]) - \\ fs[join_def])); + \\ fs[join_def]) +>- (rename1 `Fma e1 e2 e3` + \\ rw_thm_asm `typeCheck (Fma e1 e2 e3) _ _` typeCheck_def + \\ fs[] + \\ Cases_on `tMap (Fma e1 e2 e3)` \\ fs[] + \\ `tMap e3 = SOME M64` + by (first_x_assum irule + >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[]) + \\ qexists_tac `Gamma` \\ rpt strip_tac + >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union]) + \\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ Cases_on `tMap e3` \\ fs[]) + \\ `tMap e2 = SOME M64` + by (first_x_assum irule + >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[]) + \\ qexists_tac `Gamma` \\ rpt strip_tac + >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union]) + \\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ Cases_on `tMap e3` \\ fs[]) + \\ `tMap e1 = SOME M64` + by (first_x_assum irule + >- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[]) + \\ qexists_tac `Gamma` \\ rpt strip_tac + >- (first_x_assum irule \\ simp[Once usedVars_def, domain_union]) + \\ Cases_on `tMap e1` \\ Cases_on `tMap e2` \\ Cases_on `tMap e3` \\ fs[]) + \\ fs[join3_def, join_def])); val typing_cmd_64bit = store_thm ( "typing_cmd_64bit", @@ -563,6 +610,18 @@ val typing_agrees_exp = store_thm ( \\ rpt (disch_then drule) \\ fs[]) \\ `m2' = x'` by (first_x_assum drule\\ rpt (disch_then drule) \\ fs[]) \\ rveq \\ fs[]) + >- (rw_thm_asm `typeCheck _ _ _` typeCheck_def + \\ fs[] + \\ qpat_x_assum `tMap (Fma _ _ _) = SOME _` (fn thm => fs[thm]) + \\ Cases_on `tMap e` \\ Cases_on `tMap e'` \\ Cases_on `tMap e''` \\ fs[] + \\ `m1' = x` + by (qpat_x_assum `!E Gamma tMap v m1 m2. typeCheck e _ _ /\ _ /\ _ ==> _` drule + \\ rpt (disch_then drule) \\ fs[]) + \\ `m2' = x'` + by (qpat_x_assum `!E Gamma tMap v m1 m2. typeCheck e' _ _ /\ _ /\ _ ==> _` drule + \\ rpt (disch_then drule) \\ fs[]) + \\ `m3 = x''` by (first_x_assum drule\\ rpt (disch_then drule) \\ fs[]) + \\ rveq \\ fs[]) >- (rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ fs[] \\ qpat_x_assum `tMap (Downcast m e) = SOME _` (fn thm => fs[thm]) @@ -1074,7 +1133,87 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", by (fs[GSYM float_is_zero_to_real, float_is_zero_def]) \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `0:real`] - \\ fs[perturb_def, join_def, mTypeToQ_pos]))); + \\ fs[perturb_def, join_def, mTypeToQ_pos])) + >- (rename1 `Fma (toRExp e1) (toRExp e2) (toRExp e3)` + \\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm]) + \\ `tMap (toRExp e1) = SOME M64 /\ tMap(toRExp e2) = SOME M64 /\ tMap (toRExp e3) = SOME M64 /\ tMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) = SOME M64` + by (rpt conj_tac \\ irule typing_exp_64bit \\ fs[is64BitEval_def, noDowncast_def] + \\ qexists_tac `Gamma` \\ fs[] + \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def \\ fs[] + \\ Cases_on `tMap (toRExp e1)` \\ Cases_on `tMap (toRExp e2)` \\ Cases_on `tMap (toRExp e3)` + \\ Cases_on `tMap (Fma (toRExp e1) (toRExp e2) (toRExp e3))` \\ fs[] + \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union]) + \\ `m1 = M64 /\ m2 = M64 /\ m3 = M64` + by (rpt conj_tac + \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def + \\ irule typing_agrees_exp + \\ qexistsl_tac [`toREnv E2`, `Gamma`] + THENL [qexists_tac `toRExp e1`, qexists_tac `toRExp e2`, qexists_tac `toRExp e3`] + \\ qexistsl_tac [`tMap`] + THENL [qexists_tac `v1`, qexists_tac `v2`, qexists_tac `v3`] + \\ fs[] + \\ rw_asm_star `tMap (toRExp e1) = _` + \\ rw_asm_star `tMap (toRExp e2) = _` + \\ rw_asm_star `tMap (toRExp e3) = _` + \\ rw_asm_star `tMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) = _`) + \\ rveq + \\ ntac 3 (first_x_assum (qspecl_then [`E1`, `E2`,`E2_real`, `Gamma`, `tMap`] assume_tac)) + \\ first_x_assum (qspecl_then [`v1`, `A`, `P`, `fVars`, `dVars`] destruct) + >- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def + \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def + \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def + \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def + \\ rw_thm_asm `is64BitEval _` is64BitEval_def + \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def + \\ rw_thm_asm `noDowncast _` noDowncast_def + \\ Cases_on `A (Fma (toRExp e1) (toRExp e2) (toRExp e3))` + \\ Cases_on `A (toRExp e1)` + \\ Cases_on `A (toRExp e2)` + \\ Cases_on `A (toRExp e3)` \\ fs[] + \\ rpt (qpat_x_assum `tMap _ = _` (fn thm => fs[thm])) + \\ fs[] + \\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) + \\ fs[domain_union, DIFF_DEF, SUBSET_DEF] + \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union]) + \\ first_x_assum (qspecl_then [`v2`, `A`, `P`, `fVars`, `dVars`] destruct) + >- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def + \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def + \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def + \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def + \\ rw_thm_asm `is64BitEval _` is64BitEval_def + \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def + \\ rw_thm_asm `noDowncast _` noDowncast_def + \\ Cases_on `A (Fma (toRExp e1) (toRExp e2) (toRExp e3))` + \\ Cases_on `A (toRExp e1)` + \\ Cases_on `A (toRExp e2)` + \\ Cases_on `A (toRExp e3)` \\ fs[] + \\ rpt (qpat_x_assum `tMap _ = _` (fn thm => fs[thm])) + \\ fs[] + \\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) + \\ fs[domain_union, DIFF_DEF, SUBSET_DEF] + \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union]) + \\ first_x_assum (qspecl_then [`v3`, `A`, `P`, `fVars`, `dVars`] destruct) + >- (rw_thm_asm `validErrorbound _ _ _ _` validErrorbound_def + \\ rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def + \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def + \\ rw_thm_asm `typeCheck _ _ _` typeCheck_def + \\ rw_thm_asm `is64BitEval _` is64BitEval_def + \\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def + \\ rw_thm_asm `noDowncast _` noDowncast_def + \\ Cases_on `A (Fma (toRExp e1) (toRExp e2) (toRExp e3))` + \\ Cases_on `A (toRExp e1)` + \\ Cases_on `A (toRExp e2)` + \\ Cases_on `A (toRExp e3)` \\ fs[] + \\ rpt (qpat_x_assum `tMap _ = _` (fn thm => fs[thm])) + \\ fs[] + \\ rpt conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC) + \\ fs[domain_union, DIFF_DEF, SUBSET_DEF] + \\ rpt strip_tac \\ first_x_assum irule \\ simp[Once usedVars_def, domain_union]) + \\ fs[] + \\ rename1 `eval_exp_float e1 _ = SOME vF1` + \\ rename1 `eval_exp_float e2 _ = SOME vF2` + \\ rename1 `eval_exp_float e3 _ = SOME vF3` + \\ fs[optionLift_def])); val bstep_gives_IEEE = store_thm ( "bstep_gives_IEEE", diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml index aa63ec3bed4e1eb74d8664d4d949b80c66764b24..4786155453189bf81bef7fc70be5ca9c78408ced 100644 --- a/hol4/Infra/MachineTypeScript.sml +++ b/hol4/Infra/MachineTypeScript.sml @@ -64,6 +64,9 @@ val join_def = Define ` join (m1:mType) (m2:mType) = if (isMorePrecise m1 m2) then m1 else m2`; +val join3_def = Define ` + join3 (m1: mType) (m2: mType) (m3: mType) = join m1 (join m2 m3)`; + (* val M0_join_is_M0 = store_thm ("M0_join_is_M0", *) (* ``!m1 m2. *) (* join m1 m2 = M0 ==> *) diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml index a8f1e6888d6333b86b66fdb389b928737a5dcb6d..dd076b9cd4425c75a86af7680f629afd1baca4cc 100644 --- a/hol4/IntervalValidationScript.sml +++ b/hol4/IntervalValidationScript.sml @@ -69,7 +69,18 @@ val validIntervalbounds_def = Define ` let new_iv = divideInterval iv1 iv2 in isSupersetInterval new_iv intv else F - else F)`; + else F) + | Fma f1 f2 f3 => + (if (validIntervalbounds f1 absenv P validVars /\ + validIntervalbounds f2 absenv P validVars /\ + validIntervalbounds f3 absenv P validVars) + then + let (iv1, _ ) = absenv f1 in + let (iv2, _) = absenv f2 in + let (iv3, _) = absenv f3 in + let new_iv = addInterval iv1 (multInterval iv2 iv3) in + isSupersetInterval new_iv intv + else F)`; val validIntervalboundsCmd_def = Define ` validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num_set) = @@ -108,6 +119,13 @@ val ivbounds_approximatesPrecond_sound = store_thm ("ivbounds_approximatesPrecon \\ `validIntervalbounds f1 absenv P V /\ validIntervalbounds f2 absenv P V` by (Cases_on `absenv (Binop b f1 f2)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ fs [Once validIntervalbounds_def]) \\ fs [domain_union]) + >- (rpt ( + first_x_assum + (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm)) + \\ rename1 `Fma f1 f2 f3` + \\ `validIntervalbounds f1 absenv P V /\ validIntervalbounds f2 absenv P V /\ validIntervalbounds f3 absenv P V` + by (Cases_on `absenv (Fma f1 f2 f3)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` \\ fs [Once validIntervalbounds_def]) + \\ fs [domain_union]) >- (rpt ( first_x_assum (fn thm => qspecl_then [`absenv`, `P`, `V`] assume_tac thm)) @@ -425,6 +443,103 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", (SND iv_f * (inv (SND iv_f'))) (SND iv_f * (inv (FST iv_f')))` \\ metis_tac [])))) + (* FMA case *) + >- (rename1 `Fma f1 f2 f3` + \\ `?v1. eval_exp E (toRMap Gamma) (toREval f1) v1 M0 /\ + (FST (FST (absenv f1))) <= v1 /\ (v1 <= SND (FST (absenv f1)))` + by (first_x_assum match_mp_tac + \\ qexistsl_tac [`P`, `fVars`, `dVars`] + \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def + \\ Cases_on `absenv (Fma f1 f2 f3)` + \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` + \\ fs [] + \\ conj_tac + \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF] + \\ rpt strip_tac + \\ first_x_assum match_mp_tac \\ fs[] + \\ DISJ1_TAC + \\ simp[Once usedVars_def]) + \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f1) _ _ /\ _ /\ _` kall_tac + \\ `?v2. eval_exp E (toRMap Gamma) (toREval f2) v2 M0 /\ + (FST (FST (absenv f2))) <= v2 /\ (v2 <= SND (FST (absenv f2)))` + by (first_x_assum match_mp_tac + \\ qexistsl_tac [`P`, `fVars`, `dVars`] + \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def + \\ Cases_on `absenv (Fma f1 f2 f3)` + \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` + \\ fs [] + \\ conj_tac \\ fs [] + \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF] + \\ rpt strip_tac + \\ first_x_assum match_mp_tac \\ fs[] + \\ DISJ2_TAC + \\ simp[Once usedVars_def]) + \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f2) _ _ /\ _ /\ _` kall_tac + \\ `?v3. eval_exp E (toRMap Gamma) (toREval f3) v3 M0 /\ + (FST (FST (absenv f3))) <= v3 /\ (v3 <= SND (FST (absenv f3)))` + by (first_x_assum match_mp_tac + \\ qexistsl_tac [`P`, `fVars`, `dVars`] + \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def + \\ Cases_on `absenv (Fma f1 f2 f3)` + \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` + \\ fs [] + \\ conj_tac \\ fs [] + \\ fs[Once usedVars_def, domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF] + \\ rpt strip_tac + \\ first_x_assum match_mp_tac \\ fs[] + \\ DISJ2_TAC \\ DISJ2_TAC + \\ simp[Once usedVars_def]) + \\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f3) _ _ /\ _ /\ _` kall_tac + \\ fs [] + \\ rw_thm_asm `validIntervalbounds (Fma f1 f2 f3) absenv P V` validIntervalbounds_def + \\ Cases_on `absenv (Fma f1 f2 f3)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` + \\ qmatch_assum_rename_tac `absenv (Fma f1 f2 f3) = (iv_b,err_b)` + \\ qmatch_assum_rename_tac `absenv f1 = (iv_f1,err_f1)` + \\ qmatch_assum_rename_tac `absenv f2 = (iv_f2,err_f2)` + \\ qmatch_assum_rename_tac `absenv f3 = (iv_f3,err_f3)` + \\ qexists_tac `evalFma v1 v2 v3` + \\ fs[evalFma_def, evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def, addInterval_def] + \\ qspecl_then [`iv_f2`, `iv_f3`, `v2`, `v3`] + assume_tac + (REWRITE_RULE + [validIntervalAdd_def, + multInterval_def, + absIntvUpd_def, + contained_def, + IVhi_def, + IVlo_def] interval_multiplication_valid) + \\ qspecl_then [`iv_f1`, `multInterval iv_f2 iv_f3`, `v1`, `v2 * v3`] + assume_tac + (REWRITE_RULE + [validIntervalAdd_def, + addInterval_def, + multInterval_def, + absIntvUpd_def, + contained_def, + IVhi_def, IVlo_def] interval_addition_valid) + \\ fs[multInterval_def, absIntvUpd_def, IVlo_def, IVhi_def] \\ res_tac + \\ rpt conj_tac + >- (match_mp_tac Fma_dist' + \\ qexistsl_tac [`M0`, `M0`, `M0`, `v1`, `v2`, `v3`, `0:real`] + \\ fs [mTypeToQ_def, perturb_def, evalFma_def, evalBinop_def, join3_def, join_def]) + >- (match_mp_tac REAL_LE_TRANS + \\ asm_exists_tac + \\ conj_tac \\ fs[]) + >- (match_mp_tac REAL_LE_TRANS + \\ qexists_tac `max4 + (FST iv_f1 + + min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3) + (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3)) + (FST iv_f1 + + max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3) + (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3)) + (SND iv_f1 + + min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3) + (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3)) + (SND iv_f1 + + max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3) + (SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))` + \\conj_tac \\ fs[])) (* Downcast case *) >- (`?v. eval_exp E (toRMap Gamma) (toREval f) v M0 /\ FST(FST(absenv f)) <= v /\ v <= SND (FST(absenv f))` @@ -483,6 +598,7 @@ val swap_Gamma_eval_exp = store_thm ( >- (qexists_tac `v1` \\ fs[]) >- (qexistsl_tac [`v1`, `delta`] \\ fs[]) >- (qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta`] \\ fs[]) + >- (qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta`] \\ fs[]) >- (qexistsl_tac [`m1'`, `v1`, `delta`] \\ fs[])); val swap_Gamma_bstep = store_thm ( @@ -678,6 +794,36 @@ val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates \\ asm_exists_tac \\ fs [] \\ match_mp_tac REAL_LE_TRANS \\ asm_exists_tac \\ fs [])) + >- (rename1 `Fma f1 f2 f3` + \\ qpat_x_assum `validIntervalbounds _ _ _ _` + (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm)) + \\ Cases_on `absenv (Fma f1 f2 f3)` \\ rename1 `absenv (Fma f1 f2 f3) = (iv,err)` + \\ fs[] + \\ `valid (FST (absenv f1))` + by (first_x_assum match_mp_tac + \\ qexists_tac `P` \\ qexists_tac `dVars` + \\ fs[]) + \\ `valid (FST (absenv f2))` + by (first_x_assum match_mp_tac + \\ qexists_tac `P` \\ qexists_tac `dVars` + \\ fs[]) + \\ `valid (FST (absenv f3))` + by (first_x_assum match_mp_tac + \\ qexists_tac `P` \\ qexists_tac `dVars` + \\ fs[]) + \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3` + \\ rename1 `absenv f1 = (iv_f1, err_f1)` + \\ rename1 `absenv f2 = (iv_f2, err_f2)` + \\ rename1 `absenv f3 = (iv_f3, err_f3)` + \\ fs[] + \\ `valid (addInterval iv_f1 (multInterval iv_f2 iv_f3))` + by (match_mp_tac iv_add_preserves_valid \\ fs[] + \\ match_mp_tac iv_mult_preserves_valid \\ fs[]) + \\ fs[valid_def, isSupersetInterval_def] + \\ match_mp_tac REAL_LE_TRANS + \\ asm_exists_tac \\ fs [] + \\ match_mp_tac REAL_LE_TRANS + \\ asm_exists_tac \\ fs []) >- (qpat_x_assum `validIntervalbounds _ _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm)) \\ Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f` \\ fs[] diff --git a/hol4/TypingScript.sml b/hol4/TypingScript.sml index 2591f57bff3e36c4af0d094008aa4bde04000764..e81c64f5b75b379da6b2cb0fc0e641f961af7eb5 100644 --- a/hol4/TypingScript.sml +++ b/hol4/TypingScript.sml @@ -17,6 +17,13 @@ val typeExpression_def = Define ` (case (tm1, tm2) of | SOME m1, SOME m2 => SOME (join m1 m2) | _, _ => NONE) + | Fma e1 e2 e3 => + let tm1 = typeExpression Gamma e1 in + let tm2 = typeExpression Gamma e2 in + let tm3 = typeExpression Gamma e3 in + (case (tm1, tm2, tm3) of + | SOME m1, SOME m2, SOME m3 => SOME (join3 m1 m2 m3) + | _, _, _ => NONE) | Downcast m e1 => let tm1 = typeExpression Gamma e1 in case tm1 of @@ -35,6 +42,10 @@ val typeMap_def = Define ` | SOME m1, NONE => SOME m1 | NONE, SOME m2 => SOME m2 | NONE, NONE => NONE) + | Fma e1 e2 e3 => if e = e' then typeExpression Gamma e + else (case (typeMap Gamma e1 e'), (typeMap Gamma e2 e'), (typeMap Gamma e3 e') of + | SOME m1, SOME m2, SOME m3 => SOME (join3 m1 m2 m3) + | _, _, _ => NONE) | Downcast m e1 => if e = e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'` val typeCmd_def = Define ` @@ -82,6 +93,12 @@ val typeCheck_def = Define ` /\ typeCheck e1 Gamma tMap /\ typeCheck e2 Gamma tMap) | _, _, _ => F) + | Fma e1 e2 e3 => (case tMap e, tMap e1, tMap e2, tMap e3 of + | SOME m, SOME m1, SOME m2, SOME m3 => ((m = join3 m1 m2 m3) + /\ typeCheck e1 Gamma tMap + /\ typeCheck e2 Gamma tMap + /\ typeCheck e3 Gamma tMap) + | _, _, _, _ => F) | Downcast m_ e1 => (case tMap e, tMap e1 of | SOME m', SOME m1 => (m' = m_) /\ isMorePrecise m1 m_ /\ typeCheck e1 Gamma tMap @@ -126,6 +143,17 @@ val typingSoundnessExp = store_thm("typingSoundnessExp", \\ `x' = m1` by (fs [SOME_11]) \\ `x'' = m2` by (fs [SOME_11]) \\ rveq \\ fs []) + >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs [] + \\ Cases_on `expTypes (Fma e e' e'')` \\ rveq \\ fs [] + \\ Cases_on `expTypes e` \\ rveq \\ fs [] + \\ Cases_on `expTypes e'` \\ rveq \\ fs [] + \\ Cases_on `expTypes e''` \\ rveq \\ fs [] + \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs [] + \\ res_tac + \\ `x' = m1` by (fs [SOME_11]) + \\ `x'' = m2` by (fs [SOME_11]) + \\ `x''' = m3` by (fs [SOME_11]) + \\ rveq \\ fs []) >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs [] \\ `m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq \\ fs [] \\ Cases_on `expTypes (Downcast m e)` \\ rveq \\ fs [] diff --git a/hol4/transScript.sml b/hol4/transScript.sml index ceeb7b6b7bdd211ccff5c3c46dcc9ed27f4ca2b5..82d350a44995c2a75b59086360823839f72deaa9 100644 --- a/hol4/transScript.sml +++ b/hol4/transScript.sml @@ -1,4 +1,3 @@ - open preamble open simpLib realTheory realLib RealArith stringTheory @@ -190,7 +189,7 @@ val precond_validErrorbound_true = prove (`` \\ first_x_assum irule \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def \\ rw_asm_star `absenv _ = _` - \\ Cases_on `absenv x12` + \\ Cases_on `absenv x15` \\ fs []) \\ conj_tac >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm) @@ -240,6 +239,10 @@ val precond_validErrorbound_true = prove (`` \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm]) \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def] \\ REAL_ASM_ARITH_TAC)) + \\ conj_tac + >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm) + \\ rpt conj_tac \\ first_x_assum match_mp_tac + \\ fs [Once validIntervalbounds_def]) \\ rpt strip_tac \\ rveq \\ fs[]