diff --git a/hol4/CertificateCheckerScript.sml b/hol4/CertificateCheckerScript.sml index 948d47f2eae381efae7dc193d208db1ec82e5c31..1b51f183929a7b2eb374ee0df46abc6e519ea98e 100644 --- a/hol4/CertificateCheckerScript.sml +++ b/hol4/CertificateCheckerScript.sml @@ -44,7 +44,7 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound", CertificateChecker e A P defVars ==> ?iv err vR vF m. FloverMapTree_find e A = SOME (iv,err) /\ - eval_exp E1 (toRMap defVars) (toREval e) vR M0 /\ + eval_exp E1 (toRMap defVars) (toREval e) vR REAL /\ eval_exp E2 defVars e vF m /\ (!vF m. eval_exp E2 defVars e vF m ==> @@ -99,7 +99,7 @@ val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_so CertificateCheckerCmd f A P defVars ==> ?iv err vR vF m. FloverMapTree_find (getRetExp f) A = SOME (iv, err) /\ - bstep (toREvalCmd f) E1 (toRMap defVars) vR M0 /\ + bstep (toREvalCmd f) E1 (toRMap defVars) vR REAL /\ bstep f E2 defVars vF m /\ (!vF m. bstep f E2 defVars vF m ==> abs (vR - vF) <= err)``, simp [CertificateCheckerCmd_def] diff --git a/hol4/CommandsScript.sml b/hol4/CommandsScript.sml index efd1699474b3885b822462a9dc15941723c7d79f..afadfe4dee3b9fdafb7a034e6eabf2641f70c96a 100644 --- a/hol4/CommandsScript.sml +++ b/hol4/CommandsScript.sml @@ -20,7 +20,7 @@ val _ = Datatype ` val toREvalCmd_def = Define ` toREvalCmd (f:real cmd) : real cmd = case f of - | Let m x e g => Let M0 x (toREval e) (toREvalCmd g) + | Let m x e g => Let REAL x (toREval e) (toREvalCmd g) | Ret e => Ret (toREval e)`; (** diff --git a/hol4/EnvironmentsScript.sml b/hol4/EnvironmentsScript.sml index f4cca502f39bd0448d477fb8e191ad57d226594c..bda4b99466ac5228736c4c08cda5d9b9cd4c19b3 100644 --- a/hol4/EnvironmentsScript.sml +++ b/hol4/EnvironmentsScript.sml @@ -12,7 +12,7 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln ` (!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x. approxEnv E1 defVars A fVars dVars E2 /\ (defVars x = SOME m) /\ - (abs (v1 - v2) <= abs v1 * (mTypeToR m)) /\ + (abs (v1 - v2) <= computeError v1 m) /\ (lookup x (union fVars dVars) = NONE) ==> approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (insert x () fVars) dVars (updEnv x v2 E2)) /\ (!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) @@ -58,7 +58,7 @@ val approxEnv_fVar_bounded = store_thm ( E2 x = SOME v2 /\ x IN (domain fVars) /\ Gamma x = SOME m ==> - abs (v - v2) <= (abs v) * (mTypeToR m)``, + abs (v - v2) <= computeError v m``, rpt strip_tac \\ qspec_then `\E1 Gamma absenv fVars dVars E2. @@ -67,7 +67,7 @@ val approxEnv_fVar_bounded = store_thm ( E2 x = SOME v2 /\ x IN (domain fVars) /\ Gamma x = SOME m ==> - abs (v - v2) <= (abs v) * (mTypeToR m)` + abs (v - v2) <= computeError v m` (fn thm => irule (SIMP_RULE std_ss [] thm)) approxEnv_ind \\ rpt strip_tac diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml index 8e5acfb69c03ac101c8f89b4cf6c1f2e8ac1186f..b651b0a0a3013097b458f7e7467c862937dbad9f 100644 --- a/hol4/ErrorBoundsScript.sml +++ b/hol4/ErrorBoundsScript.sml @@ -13,263 +13,370 @@ val _ = new_theory "ErrorBounds"; val _ = Parse.hide "delta"; (* so that it can be used as a variable *) val _ = temp_overload_on("abs",``real$abs``); +val triangle_trans = store_thm ( + "triangle_trans", + ``!a b c. + abs (a + b) <= abs a + abs b /\ + abs a + abs b <= c ==> + abs (a + b) <= c``, + rpt strip_tac + \\ REAL_ASM_ARITH_TAC); + +val triangle_tac = + irule triangle_trans \\ fs[REAL_ABS_TRIANGLE]; + val const_abs_err_bounded = store_thm ("const_abs_err_bounded", ``!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) (defVars: num -> mType option). - eval_exp E1 (toRMap defVars) (Const M0 n) nR M0 /\ + eval_exp E1 (toRMap defVars) (Const REAL n) nR REAL /\ eval_exp E2 defVars (Const m n) nF m ==> - abs (nR - nF) <= abs n * (mTypeToR m)``, + abs (nR - nF) <= computeError n m``, rpt strip_tac \\ fs[eval_exp_cases] - \\ `perturb n delta = n` by (irule delta_0_deterministic \\ fs[mTypeToR_def]) - \\ simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL] - \\ irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC); + \\ Cases_on `m` \\ fs[perturb_def, Rabs_err_simpl, REAL_ABS_MUL, computeError_def] + >- (irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC) + >- (irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC) + >- (irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC) + \\ REAL_ASM_ARITH_TAC); + +val float_add_tac = + (`e1R + e2R + -((e1F + e2F) * (1 + deltaF)) = + (e1R + - e1F) + ((e2R + - e2F) + - (e1F + e2F) * deltaF)` + by REAL_ASM_ARITH_TAC + \\ simp [] + \\ triangle_tac + \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC] + \\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] + \\ once_rewrite_tac [REAL_ADD_ASSOC] + \\ triangle_tac + \\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] + \\ once_rewrite_tac [REAL_ABS_MUL] + \\ simp[computeError_def] + \\ match_mp_tac REAL_LE_MUL2 + \\ fs [REAL_ABS_POS, ABS_NEG]); val add_abs_err_bounded = store_thm ("add_abs_err_bounded", - ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real) - (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType) (defVars: num -> mType option). - eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\ + ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) + (err1:real) (err2:real) (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType) + (defVars: num -> mType option). + eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\ eval_exp E2 defVars e1 e1F m1 /\ - eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\ eval_exp E2 defVars e2 e2F m2 /\ - eval_exp E1 (toRMap defVars) (toREval (Binop Plus e1 e2)) vR M0 /\ - eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Plus (Var 1) (Var 2)) vF m /\ + eval_exp E1 (toRMap defVars) (toREval (Binop Plus e1 e2)) vR REAL /\ + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) + (updDefVars 2 m2 (updDefVars 1 m1 defVars)) + (Binop Plus (Var 1) (Var 2)) vF m /\ abs (e1R - e1F) <= err1 /\ abs (e2R - e2F) <= err2 ==> - abs (vR - vF) <= err1 + err2 + (abs (e1F + e2F) * (mTypeToR m))``, - rpt strip_tac - \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Plus e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)) - \\ fs [] + abs (vR - vF) <= err1 + err2 + (computeError (e1F + e2F) m)``, + rpt strip_tac \\ fs[toREval_def] \\ inversion `eval_exp E1 _ (Binop Plus _ _) _ _` eval_exp_cases - \\ rename1 `vR = perturb (evalBinop Plus v1R v2R) deltaR` + \\ rename1 `vR = perturb (evalBinop Plus v1R v2R) (join m1R m2R) deltaR` \\ inversion `eval_exp _ _ (Binop Plus (Var 1) (Var 2)) _ _` eval_exp_cases - \\ rename1 `vF = perturb (evalBinop Plus v1F v2F) deltaF` - \\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[]) \\ fs [] - \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm])) - \\ `perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[]) - \\ `vR = evalBinop Plus v1R v2R` by simp[] + \\ rename1 `vF = perturb (evalBinop Plus v1F v2F) (join m1F m2F) deltaF` + \\ `(m1R = REAL) /\ (m2R = REAL)` + by (conj_tac \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs[]) \\ fs [] + \\ rpt (qpat_x_assum `REAL = _` (fn thm => fs [GSYM thm])) + \\ rveq \\ fs[perturb_def] \\ `v1R = e1R` by metis_tac [meps_0_deterministic] \\ `v2R = e2R` by metis_tac [meps_0_deterministic] - \\ rveq \\ fs[evalBinop_def, perturb_def] + \\ rveq \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases) \\ fs [updEnv_def] \\ rveq - \\ fs [updDefVars_def] \\ rveq \\ once_rewrite_tac[real_sub] - \\ `e1R + e2R + -((e1F + e2F) * (1 + deltaF)) = (e1R + - e1F) + ((e2R + - e2F) + - (e1F + e2F) * deltaF)` by REAL_ASM_ARITH_TAC - \\ simp [] - (** Currently the best way I could find to get around skolem variables, as used in Coq **) - \\ qspecl_then [`abs (e1R + - e1F) + abs ((e2R + - e2F) + - (e1F + e2F) * deltaF)`] match_mp_tac real_le_trans2 - \\ fs [REAL_ABS_TRIANGLE] - \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC] - \\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] - \\ once_rewrite_tac [REAL_ADD_ASSOC] - \\ qspecl_then [`abs (e2R + - e2F) + abs (-(e1F + e2F) * deltaF)`] match_mp_tac real_le_trans2 - \\ fs [REAL_ABS_TRIANGLE] - \\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] - \\ once_rewrite_tac [REAL_ABS_MUL] - \\ match_mp_tac REAL_LE_MUL2 - \\ fs [REAL_ABS_POS, ABS_NEG]); + \\ Cases_on `join m1 m2` \\ fs[perturb_def, evalBinop_def] + >- (`e1R + e2R + -(e1F + e2F) = (e1R + - e1F) + ((e2R + - e2F))` + by REAL_ASM_ARITH_TAC + \\ simp[computeError_def] + \\ irule REAL_LE_TRANS + \\ qexists_tac `abs (e1R + - e1F) + abs (e2R + - e2F)` + \\ fs[REAL_ABS_TRIANGLE] + \\ REAL_ASM_ARITH_TAC) + >- (float_add_tac) + >- (float_add_tac) + >- (float_add_tac) + \\ simp[computeError_def] + \\ `e1R + e2R + - (e1F + e2F + deltaF) = (e1R + - e1F) + (e2R + - e2F + - deltaF)` + by (REAL_ASM_ARITH_TAC) + \\ simp[] + \\ triangle_tac + \\ rewrite_tac [GSYM REAL_ADD_ASSOC] + \\ irule REAL_LE_ADD2 \\ fs[real_sub] + \\ rewrite_tac [REAL_ADD_ASSOC] + \\ triangle_tac + \\ irule REAL_LE_ADD2 \\ fs[real_sub] + \\ REAL_ASM_ARITH_TAC); + +val float_sub_tac = + (`e1R + -e2R + -((e1F + -e2F) * (1 + deltaF)) = + (e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)` + by REAL_ASM_ARITH_TAC + \\ simp [] + \\ triangle_tac + \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC] + \\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] + \\ once_rewrite_tac [REAL_ADD_ASSOC] + \\ triangle_tac + \\ match_mp_tac REAL_LE_ADD2 \\ conj_tac + >- REAL_ASM_ARITH_TAC + \\ once_rewrite_tac [REAL_ABS_MUL, ABS_NEG] + \\ match_mp_tac REAL_LE_MUL2 + \\ fs [REAL_ABS_POS, ABS_NEG]); val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded", ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real) (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType) (defVars: num -> mType option). - eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\ eval_exp E2 defVars e1 e1F m1 /\ - eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\ eval_exp E2 defVars e2 e2F m2 /\ - eval_exp E1 (toRMap defVars) (toREval (Binop Sub e1 e2)) vR M0 /\ - eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Sub (Var 1) (Var 2)) vF m /\ + eval_exp E1 (toRMap defVars) (toREval (Binop Sub e1 e2)) vR REAL /\ + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) + (updDefVars 2 m2 (updDefVars 1 m1 defVars)) + (Binop Sub (Var 1) (Var 2)) vF m /\ abs (e1R - e1F) <= err1 /\ abs (e2R - e2F) <= err2 ==> - abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F) * (mTypeToR m))``, + abs (vR - vF) <= err1 + err2 + computeError (e1F - e2F) m``, rpt strip_tac - \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Sub e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)) - \\ fs [] + \\ fs[toREval_def] \\ inversion `eval_exp E1 _ (Binop Sub _ _) _ _` eval_exp_cases - \\ rename1 `vR = perturb (evalBinop Sub v1R v2R) deltaR` + \\ rename1 `vR = perturb (evalBinop Sub v1R v2R) (join m1R m2R) deltaR` \\ inversion `eval_exp _ _ (Binop Sub (Var 1) (Var 2)) _ _` eval_exp_cases - \\ rename1 `vF = perturb (evalBinop Sub v1F v2F) deltaF` - \\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs [] - \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm])) - \\ `perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[]) - \\ `vR = evalBinop Sub v1R v2R` by simp[] + \\ rename1 `vF = perturb (evalBinop Sub v1F v2F) (join m1F m2F) deltaF` + \\ `(m1R = REAL) /\ (m2R = REAL)` + by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[]) + \\ rveq \\ `v1R = e1R` by metis_tac[meps_0_deterministic] \\ `v2R = e2R` by metis_tac[meps_0_deterministic] - \\ fs[evalBinop_def, perturb_def] - \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases) + \\ rveq + \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` + eval_exp_cases) \\ fs [updEnv_def] \\ rveq - \\ fs [updDefVars_def] \\ rveq + \\ Cases_on `join m1 m2` + \\ fs[perturb_def, join_def, evalBinop_def, computeError_def] \\ rewrite_tac[real_sub] - \\ `e1R + -e2R + -((e1F + -e2F) * (1 + deltaF)) = (e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)` - by REAL_ASM_ARITH_TAC - \\ simp [] - (** Currently the best way I could find to get around skolem variables, as used in Coq **) - \\ qspecl_then [`abs (e1R + - e1F) + abs ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`] match_mp_tac real_le_trans2 - \\ fs [REAL_ABS_TRIANGLE] - \\ once_rewrite_tac [GSYM REAL_ADD_ASSOC] - \\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] - \\ once_rewrite_tac [REAL_ADD_ASSOC] - \\ qspecl_then [`abs (- e2R + e2F) + abs (-(e1F - e2F) * deltaF)`] match_mp_tac real_le_trans2 - \\ fs [REAL_ABS_TRIANGLE] - \\ match_mp_tac REAL_LE_ADD2 + >- (`e1R - e2R + - (e1F - e2F) = e1R + - e1F + (- e2R + e2F)` + by REAL_ASM_ARITH_TAC + \\ simp[] + \\ irule REAL_LE_TRANS + \\ qexists_tac `abs (e1R + - e1F) + abs (-e2R + e2F)` + \\ fs[REAL_ABS_TRIANGLE] + \\ REAL_ASM_ARITH_TAC) + >- (float_sub_tac) + >- (float_sub_tac) + >- (float_sub_tac) + \\ `e1R + - e2R + - (e1F + - e2F + deltaF) = (e1R + - e1F) + (- e2R + e2F + - deltaF)` + by (REAL_ASM_ARITH_TAC) + \\ simp[] + \\ triangle_tac + \\ rewrite_tac [GSYM REAL_ADD_ASSOC] + \\ irule REAL_LE_ADD2 \\ fs[real_sub] + \\ rewrite_tac [REAL_ADD_ASSOC] + \\ triangle_tac + \\ irule REAL_LE_ADD2 \\ fs[real_sub] + \\ REAL_ASM_ARITH_TAC); + +val float_mul_tac = + (`e1R * e2R + -(e1F * e2F * (1 + deltaF)) = + (e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)` + by REAL_ASM_ARITH_TAC + \\ simp[] + \\ irule REAL_LE_TRANS + \\ qexists_tac `abs (e1R * e2R + - (e1F * e2F)) + abs(- (e1F * e2F * deltaF))` \\ conj_tac - >- (`-e2R + e2F = e2F - e2R` by REAL_ASM_ARITH_TAC \\ simp[] - \\ once_rewrite_tac [ABS_SUB] \\ fs[]) - >- (once_rewrite_tac [REAL_ABS_MUL] - \\ match_mp_tac REAL_LE_MUL2 - \\ fs [REAL_ABS_POS, ABS_NEG])); + >- (REAL_ASM_ARITH_TAC) + \\ irule REAL_LE_ADD2 \\ fs[ABS_NEG, computeError_def] + \\ 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] \\ fs[]); val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded", ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real) (vR:real) (vF:real) (E1 E2 :env) (m m1 m2:mType) (defVars: num -> mType option). - eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\ eval_exp E2 defVars e1 e1F m1 /\ - eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\ eval_exp E2 defVars e2 e2F m2 /\ - eval_exp E1 (toRMap defVars) (toREval (Binop Mult e1 e2)) vR M0 /\ - eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Mult (Var 1) (Var 2)) vF m /\ + eval_exp E1 (toRMap defVars) (toREval (Binop Mult e1 e2)) vR REAL /\ + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) + (updDefVars 2 m2 (updDefVars 1 m1 defVars)) + (Binop Mult (Var 1) (Var 2)) vF m /\ abs (e1R - e1F) <= err1 /\ abs (e2R - e2F) <= err2 ==> - abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + (abs (e1F * e2F) * (mTypeToR m))``, + abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + computeError (e1F * e2F) m``, rpt strip_tac - \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Mult e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)) - \\ fs [] + \\ fs[toREval_def] \\ inversion `eval_exp E1 _ (Binop Mult _ _) _ _` eval_exp_cases - \\ rename1 `vR = perturb (evalBinop Mult v1R v2R) deltaR` + \\ rename1 `vR = perturb (evalBinop Mult v1R v2R) (join m1R m2R) deltaR` \\ inversion `eval_exp _ _ (Binop Mult (Var 1) (Var 2)) _ _` eval_exp_cases - \\ rename1 `vF = perturb (evalBinop Mult v1F v2F) deltaF` - \\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs [] - \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm])) - \\ `perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[]) - \\ `vR = evalBinop Mult v1R v2R` by simp[] + \\ rename1 `vF = perturb (evalBinop Mult v1F v2F) (join m1F m2F) deltaF` + \\ `(m1R = REAL) /\ (m2R = REAL)` + by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[]) + \\ rveq + \\ fs[perturb_def, evalBinop_def] \\ `v1R = e1R` by metis_tac[meps_0_deterministic] \\ `v2R = e2R` by metis_tac[meps_0_deterministic] - \\ fs[evalBinop_def, perturb_def] - \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases) + \\ rveq + \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` + eval_exp_cases) \\ fs [updEnv_def] \\ rveq - \\ fs [updDefVars_def] \\ rveq \\ rewrite_tac [real_sub] - \\ `e1R * e2R + -(e1F * e2F * (1 + deltaF)) = (e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)` by REAL_ASM_ARITH_TAC + \\ Cases_on `join m1 m2` \\ fs[join_def, perturb_def] + >- (rewrite_tac [REAL_LE_ADDR] \\ fs[computeError_def]) + >- (float_mul_tac) + >- (float_mul_tac) + >- (float_mul_tac) + \\ `e1R * e2R + - (e1F * e2F + deltaF) = + (e1R * e2R + - (e1F * e2F)) + - deltaF` + by REAL_ASM_ARITH_TAC + \\ simp[] + \\ triangle_tac + \\ fs[ABS_NEG, computeError_def]); + +val float_div_tac = + (`e1R / e2R + -(e1F / e2F * (1 + deltaF)) = + (e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)` + by REAL_ASM_ARITH_TAC \\ simp[] - \\ qspecl_then [`abs (e1R * e2R + -(e1F * e2F)) + abs (- e1F * e2F * deltaF)`] match_mp_tac real_le_trans2 + \\ irule REAL_LE_TRANS + \\ qexists_tac `abs (e1R / e2R + - (e1F / e2F)) + abs(- (e1F / e2F * deltaF))` \\ 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[])); + \\ irule REAL_LE_ADD2 \\ fs[ABS_NEG, computeError_def] + \\ once_rewrite_tac[REAL_ABS_MUL] + \\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]); val div_abs_err_bounded = store_thm ("div_abs_err_bounded", ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real) (vR:real) (vF:real) (E1 E2 :env) (m m1 m2:mType) (defVars: num -> mType option). - eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\ eval_exp E2 defVars e1 e1F m1 /\ - eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\ eval_exp E2 defVars e2 e2F m2 /\ - eval_exp E1 (toRMap defVars) (toREval (Binop Div e1 e2)) vR M0 /\ - eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Div (Var 1) (Var 2)) vF m /\ + eval_exp E1 (toRMap defVars) (toREval (Binop Div e1 e2)) vR REAL /\ + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) + (updDefVars 2 m2 (updDefVars 1 m1 defVars)) + (Binop Div (Var 1) (Var 2)) vF m /\ abs (e1R - e1F) <= err1 /\ abs (e2R - e2F) <= err2 ==> - abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + (abs (e1F / e2F) * (mTypeToR m))``, - rpt strip_tac - \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Div e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)) - \\ fs [] + abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + computeError (e1F / e2F) m``, + rpt strip_tac \\ fs[toREval_def] \\ inversion `eval_exp E1 _ (Binop Div _ _) _ _` eval_exp_cases - \\ rename1 `vR = perturb (evalBinop Div v1R v2R) deltaR` + \\ rename1 `vR = perturb (evalBinop Div v1R v2R) (join m1R m2R) deltaR` \\ inversion `eval_exp _ _ (Binop Div (Var 1) (Var 2)) _ _` eval_exp_cases - \\ rename1 `vF = perturb (evalBinop Div v1F v2F) deltaF` - \\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs [] - \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm])) - \\ `perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[]) - \\ `vR = evalBinop Div v1R v2R` by simp[] + \\ rename1 `vF = perturb (evalBinop Div v1F v2F) (join m1F m2F) deltaF` + \\ `(m1R = REAL) /\ (m2R = REAL)` + by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[]) + \\ rveq + \\ fs[perturb_def, evalBinop_def] \\ `v1R = e1R` by metis_tac[meps_0_deterministic] \\ `v2R = e2R` by metis_tac[meps_0_deterministic] - \\ fs[evalBinop_def, perturb_def] - \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases) + \\ rveq + \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` + eval_exp_cases) \\ fs [updEnv_def] \\ rveq - \\ fs [updDefVars_def] \\ rveq \\ rewrite_tac [real_sub] - \\ `e1R / e2R + -(e1F / e2F * (1 + deltaF)) = (e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)` by REAL_ASM_ARITH_TAC + \\ Cases_on `join m1 m2` \\ fs[join_def, perturb_def] + >- (rewrite_tac [REAL_LE_ADDR] \\ fs[computeError_def]) + >- (float_div_tac) + >- (float_div_tac) + >- (float_div_tac) + \\ `e1R / e2R + - (e1F / e2F + deltaF) = + (e1R / e2R + - (e1F / e2F)) + - deltaF` + by REAL_ASM_ARITH_TAC \\ simp[] - \\ qspecl_then [`abs (e1R / e2R + -(e1F / e2F)) + abs (- (e1F / e2F * 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 [ABS_NEG] - \\ once_rewrite_tac[REAL_ABS_MUL] - \\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS])); + \\ triangle_tac + \\ fs[ABS_NEG, computeError_def]); + +val float_fma_tac = + ( `e1R + e2R * e3R + -((e1F + e2F * e3F) * (1 + deltaF)) = + (e1R + e2R * e3R + -(e1F + e2F * e3F)) + (- (e1F + e2F * e3F) * deltaF)` + by REAL_ASM_ARITH_TAC + \\ simp[] + \\ triangle_tac + \\ irule REAL_LE_ADD2 + \\ TRY (REAL_ASM_ARITH_TAC) + \\ once_rewrite_tac[REAL_ABS_MUL] + \\ irule REAL_LE_MUL2 \\ fs[REAL_ABS_POS] + \\ once_rewrite_tac[GSYM REAL_NEG_LMUL, REAL_ABS_MUL] + \\ once_rewrite_tac[ABS_NEG] \\ fs[]); 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) + ``!(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 E1 (toRMap defVars) (toREval e1) e1R REAL /\ eval_exp E2 defVars e1 e1F m1 /\ - eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\ eval_exp E2 defVars e2 e2F m2 /\ - eval_exp E1 (toRMap defVars) (toREval e3) e3R M0 /\ + eval_exp E1 (toRMap defVars) (toREval e3) e3R REAL /\ 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 /\ + eval_exp E1 (toRMap defVars) (toREval (Fma e1 e2 e3)) vR REAL /\ + 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) * (mTypeToR 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 [] + abs (vR - vF) <= + abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + + computeError (e1F + e2F * e3F) m``, + rpt strip_tac \\ fs[toREval_def] \\ inversion `eval_exp E1 _ (Fma _ _ _) _ _` eval_exp_cases - \\ rename1 `vR = perturb (evalFma v1R v2R v3R) deltaR` + \\ rename1 `vR = perturb (evalFma v1R v2R v3R) (join3 m1R m2R m3R) 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[] + \\ rename1 `vF = perturb (evalFma v1F v2F v3F) (join3 m1F m2F m3F) deltaF` + \\ `(m1R = REAL) /\ (m2R = REAL) /\ (m3R = REAL)` + by (rpt conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[]) + \\ rveq + \\ fs[evalFma_def, evalBinop_def] \\ `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) + \\ rveq + \\ 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 + \\ Cases_on `join3 m1 m2 m3` + \\ fs[computeError_def, join3_def, join_def, perturb_def] + \\ rewrite_tac[real_sub] + >- (`e1R + e2R * e3R + - (e1F + e2F * e3F) = + e1R + - e1F + (e2R * e3R + - (e2F * e3F))` + by REAL_ASM_ARITH_TAC + \\ simp[]) + >- (float_fma_tac) + >- (float_fma_tac) + >- (float_fma_tac) + \\ `e1R + e2R * e3R + -(e1F + e2F * e3F + deltaF) = + (e1R + e2R * e3R + - (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[])); + \\ triangle_tac + \\ irule REAL_LE_ADD2 + \\ REAL_ASM_ARITH_TAC); 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 /\ + ``!(e:real exp) (nR:real) (nF1:real) (nF:real) (E1:env) (E2:env) (err:real) + (m1:mType) (m:mType) (defVars: num -> mType option). + eval_exp E1 (toRMap defVars) (toREval e) nR REAL /\ eval_exp E2 defVars e nF1 m /\ eval_exp (updEnv 1 nF1 emptyEnv) (updDefVars 1 m defVars) - (Downcast machineEpsilon (Var 1)) nF machineEpsilon /\ + (Downcast m1 (Var 1)) nF m1 /\ abs (nR - nF1) <= err ==> - abs (nR - nF) <= err + (abs nF1) * (mTypeToR machineEpsilon)``, + abs (nR - nF) <= err + computeError nF1 m1``, rpt strip_tac \\ `nR - nF = (nR - nF1) + (nF1 - nF)` by REAL_ASM_ARITH_TAC \\ fs [] - \\ match_mp_tac REAL_LE_TRANS - \\ qexists_tac `abs (nR - nF1) + abs (nF1 - nF)` \\ fs [ABS_TRIANGLE] - \\ match_mp_tac REAL_LE_TRANS - \\ qexists_tac `err + abs(nF1-nF)` \\ fs[] + \\ triangle_tac + \\ irule REAL_LE_ADD2 \\ fs[] \\ inversion `eval_exp (updEnv _ _ _) _ _ _ _` eval_exp_cases \\ inversion `eval_exp (updEnv _ _ _) _ _ _ _` eval_exp_cases \\ fs [updEnv_def] \\ rveq \\ fs[] - \\ fs [perturb_def] - \\ `nF1 - nF1 * (1 + delta) = - (nF1 * delta)` by REAL_ASM_ARITH_TAC - \\ fs [] \\ fs[ABS_NEG,ABS_MUL] - \\ match_mp_tac REAL_LE_LMUL_IMP \\ fs[ABS_POS]); - + \\ Cases_on `m1` \\ fs[perturb_def, computeError_def] + \\ once_rewrite_tac [REAL_LDISTRIB] + \\ simp[real_sub, REAL_NEG_ADD, REAL_ADD_ASSOC, ABS_NEG, ABS_MUL] + \\ irule REAL_LE_LMUL_IMP \\ fs[ABS_POS]); val err_prop_inversion_pos = store_thm ("err_prop_inversion_pos", ``!(nF:real) (nR:real) (err:real) (elo:real) (ehi:real). diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml index 9b4f7f49ded2f6f6a08dcf94a7d36b537928bf9c..8c9043b550c6defd84b9c18c77fc3ab9e0899f99 100644 --- a/hol4/ErrorValidationScript.sml +++ b/hol4/ErrorValidationScript.sml @@ -21,69 +21,88 @@ val _ = temp_overload_on("abs",``real$abs``); val validErrorbound_def = Define ` validErrorbound e (typeMap: (real exp # mType) binTree) (A:analysisResult) (dVars:num_set)= case FloverMapTree_find e A, FloverMapTree_find e typeMap of - | SOME (intv, err), SOME m => - (if (0 <= err) then - case e of - | Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * (mTypeToR m) <= err) - | Const _ n => (maxAbs intv * (mTypeToR m) <= err) - | Unop Neg e1 => - if (validErrorbound e1 typeMap A dVars) - then - case (FloverMapTree_find e1 A) of - | SOME (_, err1) => err = err1 - | _ => F - else F - | Unop Inv e1 => F - | Binop op e1 e2 => - (if (validErrorbound e1 typeMap A dVars /\ validErrorbound e2 typeMap A dVars) - then - case FloverMapTree_find e1 A, FloverMapTree_find e2 A of - | SOME (ive1, err1), SOME (ive2, err2) => - let errIve1 = widenInterval ive1 err1 in - let errIve2 = widenInterval ive2 err2 in - let upperBoundE1 = maxAbs ive1 in - let upperBoundE2 = maxAbs ive2 in - (case op of - | Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (mTypeToR m)) <= err - | Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (mTypeToR m)) <= err - | Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (mTypeToR m)) <= err - | Div => - (if (noDivzero (IVhi errIve2) (IVlo errIve2)) - then - let upperBoundInvE2 = maxAbs (invertInterval ive2) in - let minAbsIve2 = minAbsFun (errIve2) in - let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in - ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToR m)) <= err) - else F)) - | _, _ => F - else F) - | Fma e1 e2 e3 => - (if (validErrorbound e1 typeMap A dVars /\ - validErrorbound e2 typeMap A dVars /\ - validErrorbound e3 typeMap A dVars) then - case (FloverMapTree_find e1 A, - FloverMapTree_find e2 A, - FloverMapTree_find e3 A) of - | SOME (ive1, err1), SOME (ive2, err2), SOME (ive3, err3) => - 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)) * (mTypeToR m)) <= err - |_, _, _ => F - else F) - | Downcast m1 e1 => - case FloverMapTree_find e1 A of - | SOME (ive1, err1) => - let rec_res = validErrorbound e1 typeMap A dVars in - let errIve1 = widenInterval ive1 err1 in - rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToR m1)) <= err) - else F) - | _, _ => F`; + | NONE, _ => F + | _, NONE => F + | SOME (intv, err), SOME m => + (if (0 <= err) + then + case e of + | Var v => + if (lookup v dVars = SOME ()) + then T + else computeError (maxAbs intv) m <= err + | Const _ n => (computeError (maxAbs intv) m <= err) + | Unop Neg e1 => + if (validErrorbound e1 typeMap A dVars) + then + case (FloverMapTree_find e1 A) of + | SOME (_, err1) => err = err1 + | _ => F + else F + | Unop Inv e1 => F + | Binop op e1 e2 => + (if (validErrorbound e1 typeMap A dVars /\ validErrorbound e2 typeMap A dVars) + then + case FloverMapTree_find e1 A, FloverMapTree_find e2 A of + | NONE, _ => F + | _, NONE => F + | SOME (ive1, err1), SOME (ive2, err2) => + let errIve1 = widenInterval ive1 err1 in + let errIve2 = widenInterval ive2 err2 in + let upperBoundE1 = maxAbs ive1 in + let upperBoundE2 = maxAbs ive2 in + (case op of + | Plus => + let mAbs = maxAbs (addInterval errIve1 errIve2) in + err1 + err2 + computeError mAbs m <= err + | Sub => + let mAbs = maxAbs (subtractInterval errIve1 errIve2) in + err1 + err2 + computeError mAbs m <= err + | Mult => + let mAbs = maxAbs (multInterval errIve1 errIve2); + eProp = upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2 in + eProp + computeError mAbs m <= err + | Div => + (if (noDivzero (IVhi errIve2) (IVlo errIve2)) + then + let upperBoundInvE2 = maxAbs (invertInterval ive2); + minAbsIve2 = minAbsFun (errIve2); + errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2; + mAbs = maxAbs (divideInterval errIve1 errIve2); + eProp = upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv in + eProp + computeError mAbs m <= err + else F)) + else F) + | Fma e1 e2 e3 => + (if (validErrorbound e1 typeMap A dVars /\ + validErrorbound e2 typeMap A dVars /\ + validErrorbound e3 typeMap A dVars) then + case (FloverMapTree_find e1 A, + FloverMapTree_find e2 A, + FloverMapTree_find e3 A) of + | SOME (ive1, err1), SOME (ive2, err2), SOME (ive3, err3) => + let errIve1 = widenInterval ive1 err1; + errIve2 = widenInterval ive2 err2; + errIve3 = widenInterval ive3 err3; + upperBoundE1 = maxAbs ive1; + upperBoundE2 = maxAbs ive2; + upperBoundE3 = maxAbs ive3; + errIntv_prod = multInterval errIve2 errIve3; + mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3); + mAbs = maxAbs (addInterval errIve1 errIntv_prod) in + err1 + mult_error_bound + computeError mAbs m <= err + |_, _, _ => F + else F) + | Downcast m1 e1 => + if (validErrorbound e1 typeMap A dVars) + then + case FloverMapTree_find e1 A of + | SOME (ive1, err1) => + let errIve1 = widenInterval ive1 err1; + mAbs = maxAbs errIve1 in + err1 + computeError mAbs m1 <= err + else F + else F)`; add_unevaluated_function ``validErrorbound``; @@ -115,7 +134,7 @@ val err_always_positive = store_thm ( val validErrorboundCorrectVariable_eval = store_thm ( "validErrorboundCorrectVariable_eval", ``!E1 E2 A v e nR nlo nhi P fVars dVars Gamma expTypes. - eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR REAL /\ typeCheck (Var v) Gamma expTypes /\ approxEnv E1 Gamma A fVars dVars E2 /\ validIntervalbounds (Var v) A P dVars /\ @@ -142,7 +161,7 @@ val validErrorboundCorrectVariable_eval = store_thm ( val validErrorboundCorrectVariable = store_thm ( "validErrorboundCorrectVariable", ``!(E1 E2:env) A fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m expTypes Gamma. - eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval (Var v)) nR REAL /\ eval_exp E2 Gamma (Var v) nF m /\ typeCheck (Var v) Gamma expTypes /\ approxEnv E1 Gamma A fVars dVars E2 /\ @@ -155,8 +174,8 @@ val validErrorboundCorrectVariable = store_thm ( FloverMapTree_find (Var v) A = SOME ((nlo,nhi),err) ==> abs (nR - nF) <= err``, rpt strip_tac - \\ qspecl_then [`Var v`, `A`, `P`, `fVars`, `dVars`, `E1`, `Gamma`] destruct validIntervalbounds_sound - \\ fs[] + \\ drule validIntervalbounds_sound + \\ rpt (disch_then drule) \\ strip_tac \\ fs[] \\ rveq \\ `vR = nR` by (metis_tac[meps_0_deterministic]) \\ rveq \\ fs[toREval_def] \\ rpt (inversion `eval_exp _ _ _ _ _` eval_exp_cases) @@ -167,35 +186,34 @@ val validErrorboundCorrectVariable = store_thm ( \\ disch_then (qspecl_then [`m`, `(nlo,nhi)`, `e`] irule) \\ fs[domain_lookup]) \\ fs[usedVars_def,domain_lookup] - \\ irule REAL_LE_TRANS - \\ qexists_tac `maxAbs (nlo,nhi) * mTypeToR m` \\ fs[] + \\ irule REAL_LE_TRANS \\ find_exists_tac \\ fs[] \\ drule approxEnv_fVar_bounded \\ rpt (disch_then drule) \\ disch_then (qspec_then `m` assume_tac) \\ irule REAL_LE_TRANS - \\ qexists_tac `abs nR * mTypeToR m` + \\ res_tac + \\ qexists_tac `computeError nR m` \\ conj_tac \\ TRY (first_x_assum irule \\ fs[domain_lookup]) - \\ irule REAL_LE_RMUL_IMP - >- (irule contained_leq_maxAbs - \\ fs[contained_def, IVlo_def, IVhi_def]) - \\ irule mTypeToR_pos); + \\ irule computeError_up + \\ irule contained_leq_maxAbs \\ fs[contained_def, IVlo_def, IVhi_def]); val validErrorboundCorrectConstant_eval = store_thm ( "validErrorboundCorrectConstant_eval", ``!(E1 E2:env) (n nR:real) m Gamma. - eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR M0 ==> + eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR REAL ==> ?nF m1. eval_exp E2 Gamma (Const m n) nF m1``, rpt strip_tac - \\ qexistsl_tac [`perturb n (mTypeToR m)`,`m`] \\ irule Const_dist' + \\ qexistsl_tac [`perturb n m (mTypeToR m)`,`m`] \\ irule Const_dist' \\ fs[] \\ qexists_tac `mTypeToR m` - \\ fs[realTheory.abs, mTypeToR_pos]); + \\ fs[mTypeToR_def, realTheory.abs] + \\ Cases_on `m` \\ fs[mTypeToR_pos]); val validErrorboundCorrectConstant = store_thm ( "validErrorboundCorrectConstant", ``!(E1 E2:env) (A:analysisResult) (n nR nF e nlo nhi:real) dVars m expTypes Gamma. - eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval (Const m n)) nR REAL /\ eval_exp E2 Gamma (Const m n) nF m /\ typeCheck (Const m n) Gamma expTypes /\ validErrorbound (Const m n) expTypes A dVars /\ @@ -205,17 +223,21 @@ val validErrorboundCorrectConstant = store_thm ( rpt strip_tac \\ fs[toREval_def] \\ Flover_compute ``validErrorbound`` \\ Flover_compute ``typeCheck`` \\ rveq \\ fs[] - \\ inversion `eval_exp _ _ _ _ M0` eval_exp_cases - \\ `nR = n` by (metis_tac [delta_M0_deterministic]) \\ rveq - \\ inversion `eval_exp _ _ _ _ m` eval_exp_cases - \\ simp[perturb_def] - \\ rename1 `abs deltaF <= (mTypeToR m)` - \\ simp [Rabs_err_simpl, ABS_MUL] \\ irule REAL_LE_TRANS - \\ qexists_tac `maxAbs (nlo, nhi) * (mTypeToR m)` \\ conj_tac \\ simp[] - \\ irule REAL_LE_MUL2 \\ rpt (conj_tac) \\ TRY (simp[ABS_POS]) - \\ simp[maxAbs_def] \\ irule maxAbs - \\ qspecl_then [`delta`] (fn thm => fs [thm]) delta_M0_deterministic \\ fs[]); + \\ find_exists_tac \\ fs[] + \\ irule REAL_LE_TRANS + \\ qexists_tac `computeError nR m` + \\ inversion `eval_exp _ _ _ _ REAL` eval_exp_cases + \\ `nR = n` by (rveq \\ irule delta_REAL_deterministic \\ fs[]) + \\ rveq + \\ conj_tac + >- (irule const_abs_err_bounded + \\ qexistsl_tac [`E1`, `E2`, `Gamma`] + \\ conj_tac \\ irule Const_dist' \\ fs[] + \\ inversion `eval_exp _ _ _ _ m` eval_exp_cases + \\ find_exists_tac \\ fs[]) + \\ irule computeError_up + \\ fs[maxAbs_def] \\ irule maxAbs \\ fs[]); val validErrorboundCorrectAddition = store_thm ( "validErrorboundCorrectAddition", @@ -223,9 +245,9 @@ val validErrorboundCorrectAddition = store_thm ( (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ - eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval (Binop Plus e1 e2)) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval e2) nR2 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval (Binop Plus e1 e2)) nR REAL /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -250,41 +272,36 @@ val validErrorboundCorrectAddition = store_thm ( by (irule typingSoundnessExp \\ metis_tac []) \\ fs [] \\ rveq \\ irule REAL_LE_TRANS - \\ qexists_tac `err1 + err2 + (abs (nF1 + nF2) * (mTypeToR (join m1 m2)))` + \\ qexists_tac `err1 + err2 + (computeError (nF1 + nF2) (join m1 m2))` \\ conj_tac >- (irule add_abs_err_bounded \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `e1`, `nR1`, `e2`, `nR2`, `m1`, `m2`] \\ rpt (conj_tac) \\ simp[]) - >- (irule REAL_LE_TRANS - \\ qexists_tac - `err1 + err2 + maxAbs ( - addInterval (widenInterval (e1lo,e1hi) err1) - (widenInterval (e2lo,e2hi) err2)) * (mTypeToR (join m1 m2))` - \\ conj_tac \\ fs[maxAbs_def, join_def] - \\ once_rewrite_tac [REAL_MUL_COMM] \\ irule REAL_LE_LMUL_IMP - \\ simp[mTypeToR_def,mTypeToR_pos] - \\ match_mp_tac maxAbs - \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` - by (match_mp_tac distance_gives_iv - \\ qexists_tac `nR1` \\ conj_tac - \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` - by (match_mp_tac distance_gives_iv - \\ qexists_tac `nR2` \\ conj_tac - \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ `contained (nF1 + nF2) (addInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` - by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalAdd_def] interval_addition_valid) - \\ conj_tac \\ simp[]) - \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) - \\ simp[])); + \\ irule REAL_LE_TRANS \\ find_exists_tac + \\ conj_tac \\ fs[join_def] + \\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _` + \\ PairCases_on `iv` \\ irule computeError_up + \\ unabbrev_all_tac \\ fs[maxAbs_def] + \\ match_mp_tac maxAbs + \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR1` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR2` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ irule (REWRITE_RULE [validIntervalAdd_def, contained_def, IVlo_def, IVhi_def] interval_addition_valid) + \\ fs[contained_def, IVlo_def, IVhi_def]); val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtraction", ``!(E1 E2:env) (A: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. + (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) + (alo ahi e1lo e1hi e2lo e2hi:real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ - eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval (Binop Sub e1 e2)) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval e2) nR2 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval (Binop Sub e1 e2)) nR REAL /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -309,33 +326,27 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra by (irule typingSoundnessExp \\ metis_tac []) \\ fs [] \\ rveq \\ irule REAL_LE_TRANS - \\ qexists_tac `err1 + err2 + (abs (nF1 - nF2) * (mTypeToR (join m1 m2)))` + \\ qexists_tac `err1 + err2 + computeError (nF1 - nF2) (join m1 m2)` \\ conj_tac >- (irule subtract_abs_err_bounded \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `e1`, `nR1`, `e2`, `nR2`, `m1`, `m2`] \\ rpt (conj_tac) \\ simp[]) - >- (irule REAL_LE_TRANS - \\ qexists_tac - `err1 + err2 + maxAbs ( - subtractInterval (widenInterval (e1lo,e1hi) err1) - (widenInterval (e2lo,e2hi) err2)) * (mTypeToR (join m1 m2))` - \\ conj_tac \\ fs[maxAbs_def, join_def] - \\ once_rewrite_tac [REAL_MUL_COMM] \\ irule REAL_LE_LMUL_IMP - \\ simp[mTypeToR_def,mTypeToR_pos] - \\ match_mp_tac maxAbs - \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` - by (match_mp_tac distance_gives_iv - \\ qexists_tac `nR1` \\ conj_tac - \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` - by (match_mp_tac distance_gives_iv - \\ qexists_tac `nR2` \\ conj_tac - \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ `contained (nF1 - nF2) (subtractInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` - by (match_mp_tac (ONCE_REWRITE_RULE [validIntervalSub_def] interval_subtraction_valid) - \\ conj_tac \\ simp[]) - \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) - \\ simp[])); + \\ irule REAL_LE_TRANS \\ find_exists_tac + \\ conj_tac \\ fs[join_def] + \\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _` + \\ PairCases_on `iv` \\ irule computeError_up + \\ unabbrev_all_tac \\ fs[maxAbs_def] + \\ match_mp_tac maxAbs + \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR1` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR2` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ irule (REWRITE_RULE [validIntervalSub_def, contained_def, IVlo_def, IVhi_def] interval_subtraction_valid) + \\ fs[contained_def, IVlo_def, IVhi_def]); val multiplicationErroBounded = store_thm ("multiplicationErrorBounded", ``!(nR1 nR2 nF1 nF2: real) (err1 err2: real) (e1lo e1hi e2lo e2hi: real). @@ -933,9 +944,9 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult", (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ - eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval (Binop Mult e1 e2)) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval e2) nR2 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval (Binop Mult e1 e2)) nR REAL /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -968,33 +979,29 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult", \\ rpt (disch_then drule) \\ fs[]) \\ irule REAL_LE_TRANS - \\ qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * (mTypeToR (join m1 m2))` + \\ qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + computeError (nF1 * nF2) (join m1 m2)` \\ conj_tac >- (irule mult_abs_err_bounded \\ TRY asm_exists_tac \\ fs[] \\ qexistsl_tac [`E2`, `e2`, `m1`, `m2`] \\ fs []) - >- (irule REAL_LE_TRANS - \\ qexists_tac `maxAbs (e1lo,e1hi) * err2 + maxAbs (e2lo,e2hi) * err1 + - err1 * err2 + - maxAbs (multInterval (widenInterval (e1lo,e1hi) err1) - (widenInterval (e2lo,e2hi) err2)) * (mTypeToR (join m1 m2))` - \\ conj_tac \\ fs[join_def] - \\ irule REAL_LE_ADD2 - >- (irule multiplicationErroBounded \\ fs[]) - >- (simp[maxAbs_def] - \\ once_rewrite_tac [REAL_MUL_COMM] \\ irule REAL_LE_LMUL_IMP - \\ simp[mTypeToR_def,mTypeToR_pos] - \\ match_mp_tac maxAbs - \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` - by (irule distance_gives_iv - \\ qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` - by (irule distance_gives_iv - \\ qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ `contained (nF1 * nF2) (multInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` - by (irule interval_multiplication_valid \\ simp[]) - \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) - \\ simp[]))); + \\ irule REAL_LE_TRANS \\ find_exists_tac + \\ conj_tac \\ fs[join_def] + \\ irule REAL_LE_ADD2 + >- (irule multiplicationErroBounded \\ fs[]) + \\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _` + \\ PairCases_on `iv` \\ irule computeError_up + \\ unabbrev_all_tac \\ fs[maxAbs_def] + \\ match_mp_tac maxAbs + \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR1` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR2` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ irule (REWRITE_RULE [contained_def, IVlo_def, IVhi_def] interval_multiplication_valid) + \\ fs[contained_def, IVlo_def, IVhi_def]); val divisionErrorBounded = store_thm ( "divisionErrorBounded", @@ -2053,11 +2060,12 @@ val divisionErrorBounded = store_thm ( val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv", ``!(E1 E2:env) (A: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. + (nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) + (alo ahi e1lo e1hi e2lo e2hi :real) dVars m m1 m2 expTypes Gamma. (m = join m1 m2) /\ - eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ - eval_exp E1 (toRMap Gamma) (toREval (Binop Div e1 e2)) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval e2) nR2 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval (Binop Div e1 e2)) nR REAL /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) @@ -2090,42 +2098,37 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv", \\ rpt (disch_then drule) \\ fs[]) \\ irule REAL_LE_TRANS - \\ qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + abs (nF1 / nF2) * (mTypeToR (join m1 m2))` + \\ qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + computeError (nF1 / nF2) (join m1 m2)` \\ conj_tac >- (irule div_abs_err_bounded \\ asm_exists_tac \\ fs[] \\ qexistsl_tac [`E2`, `e2`, `m1`, `m2`] \\ fs []) - >- (irule REAL_LE_TRANS - \\ once_rewrite_tac [CONJ_SYM] \\ asm_exists_tac - \\ once_rewrite_tac [CONJ_SYM] \\ conj_tac \\ fs[] - \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` - by (irule distance_gives_iv - \\ qexists_tac `nR1` \\ conj_tac - \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` - by (irule distance_gives_iv - \\ qexists_tac `nR2` \\ conj_tac - \\ simp[contained_def, IVlo_def, IVhi_def]) - \\ irule REAL_LE_ADD2 - >- (irule divisionErrorBounded \\ fs[]) - >- (simp[maxAbs_def] - \\ once_rewrite_tac [REAL_MUL_COMM] - \\ fs[join_def] \\ irule REAL_LE_LMUL_IMP - \\ simp[mTypeToR_def,mTypeToR_pos] - \\ match_mp_tac maxAbs - \\ `contained (nF1 / nF2) (divideInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))` - by (match_mp_tac interval_division_valid - \\ conj_tac \\ fs[noDivzero_def]) - \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) - \\ fs[widenInterval_def, IVlo_def, IVhi_def,noDivzero_def]))); + \\ irule REAL_LE_TRANS \\ find_exists_tac + \\ conj_tac \\ fs[join_def] + \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR1` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ `contained nF2 (widenInterval (e2lo,e2hi) err2)` + by (match_mp_tac distance_gives_iv + \\ qexists_tac `nR2` \\ conj_tac + \\ simp[contained_def, IVlo_def, IVhi_def]) + \\ irule REAL_LE_ADD2 + >- (irule divisionErrorBounded \\ fs[]) + \\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _` + \\ PairCases_on `iv` \\ irule computeError_up + \\ unabbrev_all_tac \\ fs[maxAbs_def] + \\ match_mp_tac maxAbs + \\ irule (REWRITE_RULE [contained_def, IVlo_def, IVhi_def] interval_division_valid) + \\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def]); val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma", ``!(E1 E2:env) (A: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 E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval e2) nR2 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval e3) nR3 REAL /\ + eval_exp E1 (toRMap Gamma) (toREval (Fma e1 e2 e3)) nR REAL /\ eval_exp E2 Gamma e1 nF1 m1 /\ eval_exp E2 Gamma e2 nF2 m2 /\ eval_exp E2 Gamma e3 nF3 m3 /\ @@ -2166,58 +2169,47 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma", by (irule err_always_positive \\ rpt (asm_exists_tac \\ fs[])) \\ irule REAL_LE_TRANS - \\ qexists_tac `abs ((nR1 - nF1) + (nR2 * nR3 - nF2 * nF3)) + abs (nF1 + nF2 * nF3) * (mTypeToR (join3 m1 m2 m3))` + \\ qexists_tac `abs ((nR1 - nF1) + (nR2 * nR3 - nF2 * nF3)) + + computeError (nF1 + nF2 * nF3) (join3 m1 m2 m3)` \\ conj_tac - >- (irule fma_abs_err_bounded \\ TRY (asm_exists_tac \\ fs[]) - \\ rpt (asm_exists_tac \\ fs[toREval_def])) - >- (irule REAL_LE_TRANS - \\ once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac - \\ conj_tac \\ fs[] - \\ match_mp_tac REAL_LE_ADD2 - \\ conj_tac - >- (irule REAL_LE_TRANS - \\ qexists_tac `abs (nR1 - nF1) + abs (nR2 * nR3 − nF2 * nF3)` - \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC - \\ irule REAL_LE_ADD2 \\ fs[] - \\ irule 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] \\ fs[join3_def] - \\ ntac 2 (once_rewrite_tac [join_def]) - \\ irule REAL_LE_LMUL_IMP - \\ simp[mTypeToR_def,mTypeToR_pos] - \\ fs [maxAbs_def] - \\ match_mp_tac maxAbs - \\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) - \\ fs[])); + >- (irule fma_abs_err_bounded \\ rpt (find_exists_tac \\ fs[toREval_def])) + \\ irule REAL_LE_TRANS \\ find_exists_tac + \\ conj_tac \\ fs[join_def] + \\ irule REAL_LE_ADD2 + >- (irule triangle_trans \\ fs[REAL_ABS_TRIANGLE] + \\ irule REAL_LE_ADD2 \\ fs[] + \\ irule 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]) + \\ fs[join3_def, join_def] + \\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _` + \\ PairCases_on `iv` \\ irule computeError_up + \\ unabbrev_all_tac \\ fs[maxAbs_def] + \\ match_mp_tac maxAbs + \\ irule (REWRITE_RULE [validIntervalAdd_def, contained_def, IVlo_def, IVhi_def] interval_addition_valid) + \\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def]); val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding", ``!(E1 E2:env) (A:analysisResult) (e:real exp) (nR nF nF1:real) (err err1:real) (alo ahi elo ehi:real) dVars m mEps expTypes Gamma. - eval_exp E1 (toRMap Gamma) (toREval e) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e) nR REAL /\ eval_exp E2 Gamma e nF1 m /\ eval_exp (updEnv 1 nF1 emptyEnv) (updDefVars 1 m Gamma) @@ -2236,19 +2228,17 @@ val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding" by (irule typingSoundnessExp \\ metis_tac []) \\ fs[] \\ rveq \\ irule REAL_LE_TRANS - \\ qexists_tac `err1 + (abs nF1) * mTypeToR mEps` \\ fs [] + \\ qexists_tac `err1 + computeError nF1 mEps` \\ fs [] \\ conj_tac >- (irule round_abs_err_bounded \\ fs[] \\ rpt (asm_exists_tac \\ fs[])) - >- (irule REAL_LE_TRANS - \\ once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[] - \\ irule REAL_LE_RMUL_IMP - \\ fs [mTypeToR_pos] - \\ fs [maxAbs_def] - \\ match_mp_tac maxAbs - \\ fs [widenInterval_def,IVlo_def,IVhi_def] - \\ fs [ABS_BOUNDS] - \\ REAL_ASM_ARITH_TAC)); + \\ irule REAL_LE_TRANS \\ find_exists_tac \\ fs[] + \\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _` + \\ PairCases_on `iv` \\ irule computeError_up + \\ unabbrev_all_tac \\ fs[maxAbs_def] + \\ match_mp_tac maxAbs + \\ irule (REWRITE_RULE [contained_def, IVlo_def, IVhi_def] distance_gives_iv) + \\ find_exists_tac \\ fs[]); val validErrorbound_sound = store_thm ("validErrorbound_sound", ``!(e:real exp) (E1 E2:env) (A:analysisResult) (nR err:real) (P:precond) @@ -2256,7 +2246,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", typeCheck e Gamma expTypes /\ approxEnv E1 Gamma A fVars dVars E2 /\ ((domain (usedVars e)) DIFF (domain dVars)) SUBSET (domain fVars) /\ - eval_exp E1 (toRMap Gamma) (toREval e) nR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e) nR REAL /\ validErrorbound e expTypes A dVars /\ validIntervalbounds e A P dVars /\ dVars_range_valid dVars E1 A /\ @@ -2274,21 +2264,17 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ fs[] >- (conj_tac >- (irule validErrorboundCorrectVariable_eval \\ fs[] - \\ once_rewrite_tac [CONJ_COMM] - \\ rpt (asm_exists_tac \\ fs[]) - \\ once_rewrite_tac [validErrorbound_def] \\ fs[] - \\ asm_exists_tac \\ fs[]) + \\ rpt (find_exists_tac \\ fs[])) \\ rpt strip_tac \\ irule validErrorboundCorrectVariable - \\ ntac 2 (once_rewrite_tac [CONJ_COMM] - \\ rpt (asm_exists_tac \\ fs[]))) + \\ rpt (find_exists_tac \\ fs[])) >- (conj_tac \\ rpt strip_tac >- (irule validErrorboundCorrectConstant_eval \\ asm_exists_tac \\ fs[]) - \\ `m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq + \\ rename1 `eval_exp E2 Gamma (Const m v) nF mF` + \\ `m = mF` by (fs [Once eval_exp_cases_old]) \\ rveq \\ irule validErrorboundCorrectConstant - \\ ntac 2 (once_rewrite_tac [CONJ_COMM] - \\ rpt (asm_exists_tac \\ fs[])) + \\ rpt (find_exists_tac \\ fs[]) \\ qexistsl_tac [`E1`, `E2`, `Gamma`, `dVars`, `expTypes`] \\ fs[] \\ drule validIntervalbounds_sound @@ -2329,7 +2315,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ Flover_compute ``validIntervalbounds`` \\ rveq \\ fs[toREval_def] \\ inversion `eval_exp E1 _ _ _ _` eval_exp_cases \\ fs[] - \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[]) + \\ `m1 = REAL /\ m2 = REAL` by (conj_tac \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs[]) \\ rveq \\ fs[join_def] \\ first_x_assum (fn thm => @@ -2353,7 +2339,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?iv err nR1. FloverMapTree_find e1 A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ FST iv <= nR1 /\ nR1 <= SND iv` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] @@ -2362,7 +2348,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?iv err nR2. FloverMapTree_find e2 A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e2) nR2 REAL /\ FST iv <= nR2 /\ nR2 <= SND iv` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] @@ -2401,18 +2387,18 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ fs[] \\ FAIL_TAC "") \\ irule REAL_LTE_TRANS \\ qexists_tac `FST iv2 - err2` \\ fs[]) \\ conj_tac \\ rpt strip_tac - >- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) 0`, `join m1 m2`] + >- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) (join m1 m2) 0`, `join m1 m2`] \\ irule Binop_dist' - \\ qexistsl_tac [`0`, `m1`, `m2`, `nF1`, `nF2`] \\ fs[mTypeToR_pos]) + \\ qexistsl_tac [`0`, `m1`, `m2`, `nF1`, `nF2`] \\ fs[ABS_0, mTypeToR_pos]) \\ rpt strip_tac - \\ `perturb (evalBinop op nR1 nR2) delta = evalBinop op nR1 nR2` + \\ `perturb (evalBinop op nR1 nR2) REAL delta = evalBinop op nR1 nR2` by (irule delta_0_deterministic \\ fs[mTypeToR_def, join_def]) \\ fs[] \\ inversion `eval_exp E2 _ (Binop op e1 e2) _ _` eval_exp_cases \\ rename1 `abs delta2 <= mTypeToR (join mF1 mF2)` \\ `eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv)) (updDefVars 2 mF2 (updDefVars 1 mF1 Gamma)) - (Binop op (Var 1) (Var 2)) (perturb (evalBinop op v1 v2) delta2) + (Binop op (Var 1) (Var 2)) (perturb (evalBinop op v1 v2) (join mF1 mF2) delta2) (join mF1 mF2)` by (irule binary_unfolding \\ fs[] \\ qexistsl_tac [`E2`, `e1`, `e2`] \\ fs[eval_exp_cases] @@ -2433,7 +2419,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ TRY (once_rewrite_tac [typeCheck_def] \\ fs[join_def] \\ FAIL_TAC "") \\ TRY (once_rewrite_tac [validErrorbound_def] \\ fs[] \\ FAIL_TAC "") \\ irule Binop_dist' - \\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`] + \\ qexistsl_tac [`0`, `REAL`, `REAL`, `nR1`, `nR2`] \\ fs[perturb_def, mTypeToR_pos, join_def]) >- (rename1 `Fma e1 e2 e3` \\ Flover_compute ``validErrorbound`` @@ -2441,8 +2427,8 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ Flover_compute ``typeCheck`` \\ rveq \\ fs[toREval_def] \\ 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[]) + \\ `m1 = REAL /\ m2 = REAL /\ m3 = REAL` + by (rpt (conj_tac) \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs[]) \\ rveq \\ first_x_assum (fn thm => @@ -2486,7 +2472,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ rveq \\ fs[] \\ `?iv err nR1. FloverMapTree_find e1 A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ FST iv <= nR1 /\ nR1 <= SND iv` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] @@ -2495,7 +2481,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?iv err nR2. FloverMapTree_find e2 A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval e2) nR2 M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e2) nR2 REAL /\ FST iv <= nR2 /\ nR2 <= SND iv` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] @@ -2504,7 +2490,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?iv err nR3. FloverMapTree_find e3 A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval e3) nR3 M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e3) nR3 REAL /\ FST iv <= nR3 /\ nR3 <= SND iv` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] @@ -2533,19 +2519,19 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ first_x_assum irule \\ qexists_tac `m3` \\ fs[]) \\ conj_tac - >- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) 0`, `join3 m1 m2 m3`] + >- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) (join3 m1 m2 m3) 0`, `join3 m1 m2 m3`] \\ irule Fma_dist' \\ qexistsl_tac [`0`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`] \\ fs[mTypeToR_pos]) \\ rpt strip_tac - \\ `perturb (evalFma nR1 nR2 nR3) delta = evalFma nR1 nR2 nR3` + \\ `perturb (evalFma nR1 nR2 nR3) (join3 REAL REAL REAL) delta = evalFma nR1 nR2 nR3` by (irule delta_0_deterministic \\ fs[mTypeToR_def, join3_def, join_def]) \\ fs[] \\ inversion `eval_exp E2 _ (Fma e1 e2 e3) _ _` eval_exp_cases \\ rename1 `abs delta2 <= mTypeToR (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) + (Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) (join3 mF1 mF2 mF3) delta2) (join3 mF1 mF2 mF3)` by (irule fma_unfolding \\ fs[] \\ qexistsl_tac [`E2`, `e1`, `e2`, `e3`] \\ fs[eval_exp_cases] @@ -2564,7 +2550,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", >- (once_rewrite_tac [validErrorbound_def] \\ fs[]) >- (simp [Once toREval_def] \\ irule Fma_dist' - \\ qexistsl_tac [`0`, `M0`, `M0`, `M0`, `nR1`, `nR2`, `nR3`] + \\ qexistsl_tac [`0`, `REAL`, `REAL`, `REAL`, `nR1`, `nR2`, `nR3`] \\ fs[perturb_def, mTypeToR_pos])) >- (rename1 `Downcast m1 e1` \\ Flover_compute ``validErrorbound`` @@ -2584,7 +2570,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ once_rewrite_tac [usedVars_def] \\ fs[domain_union]) \\ `?iv err nR1. FloverMapTree_find e1 A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval e1) nR1 M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e1) nR1 REAL /\ FST iv <= nR1 /\ nR1 <= SND iv` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] @@ -2603,7 +2589,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", \\ first_x_assum irule \\ qexists_tac `m` \\ fs[]) \\ conj_tac \\ rpt strip_tac - >- (qexistsl_tac [`perturb nF 0`, `m1`] + >- (qexistsl_tac [`perturb nF m1 0`, `m1`] \\ irule Downcast_dist' \\ fs[] \\ qexistsl_tac [`0`, `m`, `nF`] \\ fs[mTypeToR_pos, isMorePrecise_morePrecise]) @@ -2622,11 +2608,11 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound", >- (first_x_assum irule \\ asm_exists_tac \\ fs[]) >- (once_rewrite_tac [typeCheck_def] \\ fs[join_def]) >- (once_rewrite_tac [validErrorbound_def] \\ fs[]) - >- (irule Downcast_dist' \\ fs[] - \\ qexistsl_tac [`delta`, `me1`, `v1`] - \\ fs[] - \\ irule Var_load - \\ fs[updDefVars_def, updEnv_def]))); + \\ irule Downcast_dist' \\ fs[] + \\ qexistsl_tac [`delta`, `me1`, `v1`] + \\ fs[] + \\ irule Var_load + \\ fs[updDefVars_def, updEnv_def])); val validErrorboundCmd_gives_eval = store_thm ( "validErrorboundCmd_gives_eval", @@ -2637,7 +2623,7 @@ val validErrorboundCmd_gives_eval = store_thm ( approxEnv E1 Gamma A fVars dVars E2 /\ ssa f (union fVars dVars) outVars /\ ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\ - bstep (toREvalCmd f) E1 (toRMap Gamma) vR M0 /\ + bstep (toREvalCmd f) E1 (toRMap Gamma) vR REAL /\ validErrorboundCmd f expTypes A dVars /\ validIntervalboundsCmd f A P dVars /\ dVars_range_valid dVars E1 A /\ @@ -2693,7 +2679,7 @@ val validErrorboundCmd_gives_eval = store_thm ( \\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[SUBSET_DEF, domain_union] \\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[])) - \\ rename1 `eval_exp E1 _ (toREval e) vR2 M0` + \\ rename1 `eval_exp E1 _ (toREval e) vR2 REAL` \\ `v = vR2` by (metis_tac[meps_0_deterministic]) \\ rveq \\ fs [dVars_range_valid_def] @@ -2716,7 +2702,7 @@ val validErrorboundCmd_gives_eval = store_thm ( \\ rpt strip_tac \\ metis_tac[]) >- (irule swap_Gamma_bstep - \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[] + \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[] \\ conj_tac >- (fs[updDefVars_def, ONCE_REWRITE_RULE [updDefVars_def] Rmap_updVars_comm]) \\ rw_thm_asm `bstep (toREvalCmd f) _ _ _ _` toREvalCmd_def @@ -2743,7 +2729,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound", approxEnv E1 Gamma A fVars dVars E2 /\ ssa f (union fVars dVars) outVars /\ ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\ - bstep (toREvalCmd f) E1 (toRMap Gamma) vR M0 /\ + bstep (toREvalCmd f) E1 (toRMap Gamma) vR REAL /\ bstep f E2 Gamma vF m /\ validErrorboundCmd f expTypes A dVars /\ validIntervalboundsCmd f A P dVars /\ @@ -2757,10 +2743,10 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound", \\ Flover_compute ``validIntervalboundsCmd`` \\ Flover_compute ``typeCheckCmd`` \\ rveq \\ fs[Once toREvalCmd_def] - >- (inversion `bstep _ _ _ _ M0` bstep_cases \\ rveq + >- (inversion `bstep _ _ _ _ REAL` bstep_cases \\ rveq \\ inversion `bstep _ _ _ _ m'` bstep_cases \\ rveq \\ inversion `ssa _ _ _` ssa_cases \\ rveq - \\ rename1 `eval_exp _ _ _ vr M0` + \\ rename1 `eval_exp _ _ _ vr REAL` \\ rename1 `eval_exp _ _ _ vf m` \\ first_x_assum match_mp_tac \\ `FloverMapTree_find e expTypes = SOME m` by (irule typingSoundnessExp \\ qexistsl_tac [`E2`, `Gamma`, `vf`] \\ fs[]) @@ -2791,7 +2777,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound", \\ once_rewrite_tac [freeVars_def] \\ fs [domain_union]) >- (irule swap_Gamma_bstep - \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` + \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[Rmap_updVars_comm] \\ rw_thm_asm `bstep (toREvalCmd f) _ _ _ _` toREvalCmd_def \\ fs[]) >- (fs[dVars_range_valid_def] @@ -2809,7 +2795,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound", \\ fs[] \\ simp [Once freeVars_def, domain_union] \\ metis_tac[]) - \\ rename1 `eval_exp E1 _ (toREval e) vr2 M0` + \\ rename1 `eval_exp E1 _ (toREval e) vr2 REAL` \\ `vr = vr2` by (metis_tac [meps_0_deterministic]) \\ rveq \\ fs[]) >- (fs[fVars_P_sound_def] @@ -2820,7 +2806,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound", >- (fs[vars_typed_def] \\ rpt gen_tac \\ disch_then assume_tac \\ simp[updDefVars_def] \\ Cases_on `v = n` \\ fs[])) - >- (inversion `bstep _ _ _ _ M0` bstep_cases \\ rveq + >- (inversion `bstep _ _ _ _ REAL` bstep_cases \\ rveq \\ inversion `bstep _ _ _ _ m` bstep_cases \\ rveq \\ qspecl_then [`e`, `E1`, `E2`, `A`, `vR`, `err`, `P`, `elo`, `ehi`, `fVars`, diff --git a/hol4/ExpressionsScript.sml b/hol4/ExpressionsScript.sml index 54b36951859a15f9e84ff086adfecf5ba7ae3f06..bfe03d16bcdbed80b9757d554559b3614c8b90d0 100644 --- a/hol4/ExpressionsScript.sml +++ b/hol4/ExpressionsScript.sml @@ -61,7 +61,7 @@ val evalFma_def = Define ` val toREval_def = Define ` (toREval (Var n) = Var n) /\ - (toREval (Const m n) = Const M0 n) /\ + (toREval (Const m n) = Const REAL n) /\ (toREval (Unop u e1) = Unop u (toREval e1)) /\ (toREval (Binop b e1 e2) = Binop b (toREval e1) (toREval e2)) /\ (toREval (Fma e1 e2 e3) = Fma (toREval e1) (toREval e2) (toREval e3)) /\ @@ -71,7 +71,9 @@ val toREval_def = Define ` Define a perturbation function to ease writing of basic definitions **) val perturb_def = Define ` - perturb (r:real) (e:real) = r * (1 + e)` + perturb (rVal:real) (REAL) (delta:real) = rVal /\ + perturb rVal (F w f) delta = rVal + delta /\ + perturb rVal _ delta = rVal * (1 + delta)`; (** Define expression evaluation relation parametric by an "error" epsilon. @@ -80,38 +82,38 @@ using a perturbation of the real valued computation by (1 + delta), where |delta| <= machine epsilon. **) val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln ` - (!E defVars m x v. - defVars x = SOME m /\ + (!E Gamma m x v. + Gamma x = SOME m /\ E x = SOME v ==> - eval_exp E defVars (Var x) v m) /\ - (!E defVars m n delta. + eval_exp E Gamma (Var x) v m) /\ + (!E Gamma m n delta. abs delta <= (mTypeToR m) ==> - eval_exp E defVars (Const m n) (perturb n delta) m) /\ - (!E defVars m f1 v1. - eval_exp E defVars f1 v1 m ==> - eval_exp E defVars (Unop Neg f1) (evalUnop Neg v1) m) /\ - (!E defVars m f1 v1 delta. + eval_exp E Gamma (Const m n) (perturb n m delta) m) /\ + (!E Gamma m f1 v1. + eval_exp E Gamma f1 v1 m ==> + eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m) /\ + (!E Gamma m f1 v1 delta. abs delta <= (mTypeToR m) /\ - (v1 <> 0) /\ - eval_exp E defVars f1 v1 m ==> - eval_exp E defVars (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m) /\ - (!E defVars m m1 f1 v1 delta. + eval_exp E Gamma f1 v1 m /\ + (v1 <> 0) ==> + eval_exp E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) m delta) m) /\ + (!E Gamma m m1 f1 v1 delta. isMorePrecise m1 m /\ abs delta <= (mTypeToR m) /\ - eval_exp E defVars f1 v1 m1 ==> - eval_exp E defVars (Downcast m f1) (perturb v1 delta) m) /\ - (!E defVars m1 m2 b f1 f2 v1 v2 delta. + eval_exp E Gamma f1 v1 m1 ==> + eval_exp E Gamma (Downcast m f1) (perturb v1 m delta) m) /\ + (!E Gamma m1 m2 b f1 f2 v1 v2 delta. abs delta <= (mTypeToR (join m1 m2)) /\ - eval_exp E defVars f1 v1 m1 /\ - eval_exp E defVars f2 v2 m2 /\ + eval_exp E Gamma f1 v1 m1 /\ + eval_exp E Gamma f2 v2 m2 /\ ((b = Div) ==> (v2 <> 0)) ==> - 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. + eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) (join m1 m2) delta) (join m1 m2)) /\ + (!E Gamma m1 m2 m3 f1 f2 f3 v1 v2 v3 delta. abs delta <= (mTypeToR (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))`; + 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) (join3 m1 m2 m3) delta) (join3 m1 m2 m3))`; val eval_exp_cases_old = save_thm ("eval_exp_cases_old", eval_exp_cases); @@ -145,7 +147,7 @@ val Const_dist' = store_thm ( "Const_dist'", ``!m n delta v m' E Gamma. (abs delta) <= (mTypeToR m) /\ - v = perturb n delta /\ + v = perturb n m delta /\ m' = m ==> eval_exp E Gamma (Const m n) v m'``, fs [Const_dist]); @@ -165,7 +167,7 @@ val Unop_inv' = store_thm ( (abs delta) <= (mTypeToR m) /\ eval_exp E Gamma f1 v1 m /\ (v1 <> 0) /\ - v = perturb (evalUnop Inv v1) delta /\ + v = perturb (evalUnop Inv v1) m delta /\ m' = m ==> eval_exp E Gamma (Unop Inv f1) v m'``, fs [Unop_inv]); @@ -175,7 +177,7 @@ val Downcast_dist' = store_thm ("Downcast_dist'", isMorePrecise m1 m /\ (abs delta) <= (mTypeToR m) /\ eval_exp E Gamma f1 v1 m1 /\ - v = perturb v1 delta /\ + v = perturb v1 m delta /\ m' = m ==> eval_exp E Gamma (Downcast m f1) v m'``, rpt strip_tac @@ -189,7 +191,7 @@ val Binop_dist' = store_thm ("Binop_dist'", eval_exp E Gamma f1 v1 m1 /\ eval_exp E Gamma f2 v2 m2 /\ ((op = Div) ==> (v2 <> 0)) /\ - v = perturb (evalBinop op v1 v2) delta /\ + v = perturb (evalBinop op v1 v2) m' delta /\ m' = join m1 m2 ==> eval_exp E Gamma (Binop op f1 f2) v m'``, fs [Binop_dist]); @@ -200,7 +202,7 @@ val Fma_dist' = store_thm ("Fma_dist'", 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 /\ + v = perturb (evalFma v1 v2 v3) m' delta /\ m' = join3 m1 m2 m3 ==> eval_exp E Gamma (Fma f1 f2 f3) v m'``, fs [Fma_dist]); @@ -222,35 +224,40 @@ val usedVars_def = Define ` (** If |delta| <= 0 then perturb v delta is exactly v. **) -val delta_0_deterministic = store_thm("delta_0_deterministic", - ``!(v:real) (delta:real). abs delta <= 0 ==> perturb v delta = v``, +val delta_0_deterministic = store_thm( + "delta_0_deterministic", + ``!(v:real) (m:mType) (delta:real). + abs delta <= 0 ==> perturb v m delta = v``, + Cases_on `m` \\ fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]); -val delta_M0_deterministic = store_thm("delta_M0_deterministic", - ``!(v:real) (delta:real). abs delta <= mTypeToR M0 ==> perturb v delta = v``, - fs [mTypeToR_def,perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]); +val delta_REAL_deterministic = store_thm( + "delta_REAL_deterministic", + ``!(v:real) (m:mType) (delta:real). + abs delta <= mTypeToR REAL ==> perturb v m delta = v``, + Cases_on `m` \\ fs[mTypeToR_def, delta_0_deterministic]); val toRMap_def = Define ` toRMap (d:num -> mType option) (n:num) : mType option = case d n of - | SOME m => SOME M0 + | SOME m => SOME REAL | NONE => NONE`; -val toRMap_eval_M0 = store_thm ( - "toRMap_eval_M0", +val toRMap_eval_REAL = store_thm ( + "toRMap_eval_REAL", ``!f v E Gamma m. - eval_exp E (toRMap Gamma) (toREval f) v m ==> m = M0``, + eval_exp E (toRMap Gamma) (toREval f) v m ==> m = REAL``, Induct \\ fs[toREval_def] \\ fs[eval_exp_cases, toRMap_def] \\ rpt strip_tac \\ fs[] >- (every_case_tac \\ fs[]) >- (rveq \\ first_x_assum drule \\ strip_tac \\ fs[]) >- (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[]) + >- (`m1 = REAL` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) + \\ `m2 = REAL` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) \\ 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[]) + >- (`m1 = REAL` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) + \\ `m2 = REAL` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) + \\ `m3 = REAL` by (rpt (first_x_assum drule \\ strip_tac) \\ fs[]) \\ rveq \\ fs[join3_def] \\ fs[join_def])); (** @@ -258,8 +265,8 @@ Evaluation with 0 as machine epsilon is deterministic **) val meps_0_deterministic = store_thm("meps_0_deterministic", ``!(f: real exp) v1:real v2:real E defVars. - eval_exp E (toRMap defVars) (toREval f) v1 M0 /\ - eval_exp E (toRMap defVars) (toREval f) v2 M0 ==> + eval_exp E (toRMap defVars) (toREval f) v1 REAL /\ + eval_exp E (toRMap defVars) (toREval f) v2 REAL ==> v1 = v2``, Induct_on `f` >- (rw [toREval_def] \\ fs [eval_exp_cases]) @@ -279,13 +286,13 @@ val meps_0_deterministic = store_thm("meps_0_deterministic", qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))) \\ Cases_on `b` \\ fs [eval_exp_cases] - \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs []) + \\ `m1 = REAL /\ m2 = REAL` by (conj_tac \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs []) \\ rw[] - \\ rename1 `eval_exp E _ (toREval f1) vf11 M0` + \\ rename1 `eval_exp E _ (toREval f1) vf11 REAL` \\ rename1 `eval_exp E _ (toREval f1) vf12 m1` - \\ rename1 `eval_exp E _ (toREval f2) vf21 M0` + \\ rename1 `eval_exp E _ (toREval f2) vf21 REAL` \\ rename1 `eval_exp _ _ (toREval f2) vf22 m2` - \\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs []) + \\ `m1 = REAL /\ m2 = REAL` by (conj_tac \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs []) \\ rw [] \\ fs [join_def, mTypeToR_def, delta_0_deterministic] \\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`vf21`,`vf22`] ASSUME_TAC thm) @@ -297,10 +304,10 @@ val meps_0_deterministic = store_thm("meps_0_deterministic", 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 []) + \\ `m1 = REAL /\ m2 = REAL` by (conj_tac \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs []) + \\ `m3 = REAL` by (irule toRMap_eval_REAL \\ asm_exists_tac \\ fs []) + \\ `m1' = REAL /\ m2' = REAL` by (conj_tac \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs []) + \\ `m3' = REAL` by (irule toRMap_eval_REAL \\ 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) @@ -325,10 +332,10 @@ val binary_unfolding = store_thm("binary_unfolding", (abs delta) <= (mTypeToR (join m1 m2)) /\ eval_exp E Gamma f1 v1 m1 /\ eval_exp E Gamma f2 v2 m2 /\ - eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2) ==> + eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) (join m1 m2) delta) (join m1 m2) ==> eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 Gamma)) - (Binop b (Var 1) (Var 2)) (perturb (evalBinop b v1 v2) delta) (join m1 m2)``, + (Binop b (Var 1) (Var 2)) (perturb (evalBinop b v1 v2) (join m1 m2) delta) (join m1 m2)``, fs [updEnv_def,updDefVars_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS] \\ metis_tac []); @@ -338,10 +345,10 @@ val fma_unfolding = store_thm("fma_unfolding", 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 E Gamma (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) (join3 m1 m2 m3) 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)``, + (Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) (join3 m1 m2 m3) 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'` diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml index 5156f6932e446f22712b7967ac8b33410a14aa05..2a1f4f4887eb1e3540cba868f8aee3408a65dd35 100644 --- a/hol4/FPRangeValidatorScript.sml +++ b/hol4/FPRangeValidatorScript.sml @@ -150,7 +150,7 @@ val FPRangeValidator_sound = store_thm ( \\ disch_then drule \\ fs[]) \\ once_rewrite_tac [validFloatValue_def] \\ `?iv err vR. FloverMapTree_find e A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval e) vR M0 /\ + eval_exp E1 (toRMap Gamma) (toREval e) vR REAL /\ FST iv <= vR /\ vR <= SND iv` by (drule validIntervalbounds_sound \\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`] impl_subgoal_tac) @@ -256,7 +256,7 @@ val FPRangeValidatorCmd_sound = store_thm ( \\ rpt strip_tac \\ metis_tac[]) >- (irule swap_Gamma_bstep - \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[] + \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[] \\ fs [updDefVars_def, REWRITE_RULE [updDefVars_def] Rmap_updVars_comm]) >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml index 9b86fb232bdc1f1fc6b610b0c3c6f065eca9191a..72dc8a1bc967c92ba13e3cc00a0877a13ef453ad 100644 --- a/hol4/IEEE_connectionScript.sml +++ b/hol4/IEEE_connectionScript.sml @@ -51,7 +51,7 @@ val bstep_float_def = Define ` val normal_or_zero_def = Define ` normal_or_zero (v:real) = - (minValue M64 <= abs v \/ v = 0)`; + (minValue_pos M64 <= abs v \/ v = 0)`; val isValid_def = Define ` isValid e = @@ -155,7 +155,7 @@ val normalValue_implies_normalization = store_thm ("validFloatValue_implies_norm normal v M64 ==> normalizes (:52 #11) v``, rpt strip_tac - \\ fs[normal_def, normalizes_def, wordsTheory.INT_MAX_def, minValue_def, + \\ fs[normal_def, normalizes_def, wordsTheory.INT_MAX_def, minValue_pos_def, minExponentPos_def, wordsTheory.INT_MIN_def, wordsTheory.dimindex_11, wordsTheory.UINT_MAX_def, wordsTheory.dimword_11] \\ irule REAL_LET_TRANS @@ -179,11 +179,11 @@ val denormalValue_implies_finiteness = store_thm ("normalValue_implies_finitenes \\ fs [real_to_float_def, denormal_def, dmode_def] \\ irule float_round_finite \\ irule REAL_LT_TRANS - \\ qexists_tac `minValue M64` \\ fs[] + \\ qexists_tac `minValue_pos M64` \\ fs[] \\ irule REAL_LET_TRANS \\ qexists_tac `maxValue M64` - \\ `minValue M64 <= 1` + \\ `minValue_pos M64 <= 1` by (once_rewrite_tac [GSYM REAL_INV1] - \\ fs[minValue_def, minExponentPos_def] + \\ fs[minValue_pos_def, minExponentPos_def] \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]) \\ fs[threshold_64_bit_lt_maxValue] \\ irule REAL_LE_TRANS \\ qexists_tac `1` @@ -198,7 +198,7 @@ val normal_value_is_float_value = store_thm ( \\rewrite_tac[float_value_def] \\rw_thm_asm `normal _ _` normal_def \\fs[float_to_real_def] - \\ every_case_tac \\ fs[maxValue_def, maxExponent_def, minValue_def, minExponentPos_def] + \\ every_case_tac \\ fs[maxValue_def, maxExponent_def, minValue_pos_def, minExponentPos_def] >-( Cases_on `ff.Sign` \\ fs[] \\ Cases_on `n` \\ fs[] \\ Cases_on `n'` \\ fs[]) @@ -275,7 +275,7 @@ val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value", \\ `w2n (-1w:word11) = 2047` by EVAL_TAC \\ `w2n c0 = 2047` by fs[] \\ fs[] - \\ TOP_CASE_TAC \\ fs[minValue_def, minExponentPos_def] + \\ TOP_CASE_TAC \\ fs[minValue_pos_def, minExponentPos_def] \\ fs[REAL_ABS_MUL, POW_M1] >- (`44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <= inv 1` by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]) @@ -638,7 +638,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ fs[eval_exp_float_def, optionLift_def] \\ Cases_on `E2 n` \\ fs[optionLift_def, normal_or_zero_def]) >- (rveq \\ fs[eval_exp_cases] - \\ fs[optionLift_def, normal_or_zero_def, minValue_def, + \\ fs[optionLift_def, normal_or_zero_def, minValue_pos_def, minExponentPos_def, REAL_LT_INV_EQ] \\ qexists_tac `0:real` \\ fs[mTypeToR_pos, perturb_def, fp64_to_float_float_to_fp64, @@ -721,7 +721,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ rename1 `eval_exp_float e1 _ = SOME vF1` \\ rename1 `eval_exp_float e2 _ = SOME vF2` \\ `?iv err nR2. FloverMapTree_find (toRExp e2) A = SOME (iv, err) /\ - eval_exp E1 (toRMap Gamma) (toREval (toRExp e2)) nR2 M0 /\ + eval_exp E1 (toRMap Gamma) (toREval (toRExp e2)) nR2 REAL /\ FST iv <= nR2 /\ nR2 <= SND iv` by (irule validIntervalbounds_sound \\ qexistsl_tac [`P`, `dVars`, `fVars`] @@ -769,24 +769,23 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ `validFloatValue (evalBinop b (float_to_real (fp64_to_float vF1)) (float_to_real (fp64_to_float vF2))) M64` - by (drule FPRangeValidator_sound - \\ disch_then - (qspecl_then - [`(Binop b (toRExp e1) (toRExp e2))`, - `evalBinop b (float_to_real (fp64_to_float vF1)) - (float_to_real (fp64_to_float vF2))`, - `M64`, `tMap`, `P`] irule) - \\ fs[] - \\ qexistsl_tac [`P`, `e1`, `e2`, `tMap`] - \\ fs[] - \\ irule eval_eq_env - \\ asm_exists_tac \\ fs[eval_exp_cases] - \\ rewrite_tac [CONJ_ASSOC] - \\ rpt (once_rewrite_tac [CONJ_COMM] - \\ asm_exists_tac \\ fs[]) - \\ qexists_tac ` 0:real` - \\ Cases_on `b` - \\ fs[perturb_def, evalBinop_def, mTypeToR_pos, join_def]) + by (drule FPRangeValidator_sound + \\ disch_then + (qspecl_then + [`(Binop b (toRExp e1) (toRExp e2))`, + `evalBinop b (float_to_real (fp64_to_float vF1)) + (float_to_real (fp64_to_float vF2))`, + `M64`, `tMap`, `P`] irule) + \\ fs[] + \\ qexistsl_tac [`P`, `e1`, `e2`, `tMap`] + \\ fs[] + \\ irule eval_eq_env + \\ asm_exists_tac \\ fs[eval_exp_cases] + \\ rewrite_tac [CONJ_ASSOC] + \\ rpt (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[]) + \\ qexists_tac ` 0:real` + \\ Cases_on `b` + \\ fs[perturb_def, evalBinop_def, mTypeToR_pos, join_def]) \\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64` by (drule FPRangeValidator_sound \\ disch_then @@ -862,18 +861,19 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `err`] \\ fs[perturb_def, evalBinop_def] - \\ fs[mTypeToR_def, join_def]) + \\ fs[mTypeToR_def, join_def, perturb_def]) (* result = 0 *) - >- (fs[REAL_LNEG_UNIQ, evalBinop_def] + >- (IMP_RES_TAC validValue_gives_float_value + \\ fs[REAL_LNEG_UNIQ, evalBinop_def] \\ fs[fp64_add_def, dmode_def, fp64_to_float_float_to_fp64] - \\ fs[float_add_def] + \\ fs[float_add_def, float_round_with_flags_def] \\ fs[join_def] - \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `0:real`] + \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, + `float_to_real (fp64_to_float vF2)`, `0:real`] \\ fs[perturb_def, mTypeToR_pos, evalBinop_def] - \\ fs[validValue_gives_float_value, float_round_with_flags_def] \\ `2 * abs (0:real) <= ulp (:52 #11)` by (fs[ulp_def, ULP_def]) - \\ fs[ float_to_real_round_zero_is_zero]) + \\ fs[float_to_real_round_zero_is_zero]) (* Subtraction, normal value *) >- (fs[fp64_sub_def, fp64_to_float_float_to_fp64, evalBinop_def] \\ `normal (evalBinop Sub (float_to_real (fp64_to_float vF1)) @@ -905,7 +905,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `err`] \\ fs[perturb_def, evalBinop_def] - \\ fs[mTypeToR_def, join_def]) + \\ fs[mTypeToR_def, join_def, perturb_def]) >- (fs[evalBinop_def] \\ qpat_x_assum `float_to_real (fp64_to_float _) = _` MP_TAC \\ simp[real_sub, REAL_LNEG_UNIQ, evalBinop_def] @@ -955,7 +955,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `err`] \\ fs[perturb_def, evalBinop_def] - \\ fs[mTypeToR_def, join_def]) + \\ fs[mTypeToR_def, join_def, perturb_def]) >- (fs[evalBinop_def, REAL_ENTIRE, fp64_mul_def, float_mul_def, GSYM float_is_zero_to_real, float_is_zero_def] THENL [ Cases_on `float_value (fp64_to_float vF1)`, @@ -971,7 +971,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `0:real`] \\ rveq - \\ fs[GSYM float_is_zero_to_real, float_is_zero_def, join_def, mTypeToR_pos]) + \\ fs[GSYM float_is_zero_to_real, float_is_zero_def, join_def, mTypeToR_pos, perturb_def]) (* Division *) >- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def] \\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1)) @@ -1002,7 +1002,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE", \\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `err`] \\ fs[perturb_def, evalBinop_def] - \\ fs[mTypeToR_def, join_def]) + \\ fs[mTypeToR_def, join_def, perturb_def]) >- (fs[fp64_div_def, dmode_def, fp64_to_float_float_to_fp64, float_div_def, evalBinop_def] \\ `float_to_real (fp64_to_float vF1) = 0` @@ -1104,7 +1104,7 @@ val bstep_gives_IEEE = store_thm ( validIntervalboundsCmd (toRCmd f) A P dVars /\ validErrorboundCmd (toRCmd f) tMap A dVars /\ FPRangeValidatorCmd (toRCmd f) A tMap dVars /\ - bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR M0 /\ + bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR REAL /\ bstep (toRCmd f) (toREnv E2) Gamma vF M64 /\ domain (freeVars (toRCmd f)) DIFF domain dVars ⊆ domain fVars ∧ is64BitBstep (toRCmd f) /\ @@ -1232,7 +1232,7 @@ val bstep_gives_IEEE = store_thm ( \\ fs[Once freeVars_def] \\ simp[Once freeVars_def, domain_union]) >- (irule swap_Gamma_bstep - \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[] + \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[] \\ strip_tac \\ qspecl_then [`Gamma`, `n`, `M64`, `n'`] assume_tac Rmap_updVars_comm \\ fs[updDefVars_def]) @@ -1303,7 +1303,7 @@ val bstep_gives_IEEE = store_thm ( \\ rpt strip_tac \\ metis_tac[]) >- (irule swap_Gamma_bstep - \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[] + \\ qexists_tac `updDefVars n REAL (toRMap Gamma)` \\ fs[] \\ rpt strip_tac \\ qspecl_then [`Gamma`, `n`, `M64`, `n'`] assume_tac Rmap_updVars_comm \\ fs[updDefVars_def]) @@ -1393,7 +1393,7 @@ val IEEE_connection_exp = store_thm ( CertificateChecker (toRExp e) A P defVars ==> ?iv err vR vF. (* m, currently = M64 *) FloverMapTree_find (toRExp e) A = SOME (iv, err) /\ - eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\ + eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\ eval_exp_float e E2 = SOME vF /\ eval_exp (toREnv E2) defVars (toRExp e) (float_to_real (fp64_to_float vF)) M64 /\ abs (vR - (float_to_real (fp64_to_float vF))) <= err``, @@ -1435,7 +1435,7 @@ val IEEE_connection_cmds = store_thm ( CertificateCheckerCmd (toRCmd f) A P defVars ==> ?iv err vR vF. (* m, currently = M64 *) FloverMapTree_find (getRetExp (toRCmd f)) A = SOME (iv, err) /\ - bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\ + bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\ bstep_float f E2 = SOME vF /\ bstep (toRCmd f) (toREnv E2) defVars (float_to_real (fp64_to_float vF)) M64 /\ abs (vR - (float_to_real (fp64_to_float vF))) <= err``, diff --git a/hol4/Infra/FloverTactics.sml b/hol4/Infra/FloverTactics.sml index e282e248ccd59aa415c71610e23dd9b1462cec33..90a16980c72b5b37322a71bef2ea6b220c2734a1 100644 --- a/hol4/Infra/FloverTactics.sml +++ b/hol4/Infra/FloverTactics.sml @@ -196,6 +196,27 @@ fun Flover_compute t = (split_pair_case_tac)) \\ fs[]))) end; +fun iter_exists_tac ind n = + fn tm => + if ind < n + then + (part_match_exists_tac + (fn concl => List.nth (strip_conj concl, ind)) tm) + ORELSE (iter_exists_tac (ind+1) n tm) + else + FAIL_TAC (concat ["No matching clause found for ", term_to_string tm]) ; + +val try_all:term -> tactic = + fn tm => + fn (asl, g) => + let + val len = length (strip_conj (snd (dest_exists g))) in + iter_exists_tac 0 len tm (asl, g) + end; + +val find_exists_tac = + first_assum (try_all o concl); + (* val Flover_compute:tactic = *) (* fn (g:goal) => *) (* let *) diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml index 3c103a9804dbfac8d6b4a141bdfc26a27edc02c4..d235a5eb0b5d4e7443623379bcd66215b5f23b29 100644 --- a/hol4/Infra/MachineTypeScript.sml +++ b/hol4/Infra/MachineTypeScript.sml @@ -4,8 +4,8 @@ @author: Raphael Monat @maintainer: Heiko Becker **) -open miscTheory realTheory realLib sptreeTheory; -open RealSimpsTheory; +open realTheory realLib sptreeTheory; +open RealSimpsTheory; open preamble; val _ = new_theory "MachineType"; @@ -13,13 +13,13 @@ val _ = new_theory "MachineType"; val _ = temp_overload_on("abs",``real$abs``); val _ = Datatype ` - mType = M0 | M16 | M32 | M64(* | M128 | M256 *) + mType = REAL | M16 | M32 | M64(* | M128 | M256 *) |F num num (*first num is word length, second is fractional bits *)`; val mTypeToR_def = Define ` mTypeToR (m:mType) : real = case m of - | M0 => 0 + | REAL => 0 | M16 => 1 / (2 pow 11) | M32 => 1 / (2 pow 24) | M64 => 1 / (2 pow 53) @@ -29,14 +29,10 @@ val mTypeToR_def = Define ` (* | M128 => 1 / (2 pow 105) *) (* | M256 => 1 / (2 pow 211) *)`; -val _ = export_rewrites ["mTypeToR_def"]; - -(* val meps_def = Define `meps = mTypeToR`; *) - val computeError_def = Define ` computeError v m = case m of - | M0 => 0 + | REAL => 0 | F w f => mTypeToR m | _ => abs v * mTypeToR m`; @@ -50,7 +46,7 @@ val computeError_up = store_thm ( ``!v a b m. abs v <= maxAbs (a,b) ==> computeError v m <= computeError (maxAbs (a,b)) m``, - rpt strip_tac \\ Cases_on `m` \\ fs[computeError_def] \\ TRY RealArith.REAL_ASM_ARITH_TAC + rpt strip_tac \\ Cases_on `m` \\ fs[mTypeToR_def, computeError_def] \\ TRY RealArith.REAL_ASM_ARITH_TAC \\ irule REAL_LE_RMUL_IMP \\ fs[] \\ fs[maxAbs_def] \\ `abs (real$max (abs a) (abs b)) = real$max (abs a) (abs b)` @@ -62,28 +58,28 @@ val computeError_up = store_thm ( (** Check if machine precision m1 is more precise than machine precision m2. - M0 is real-valued evaluation, hence the most precise. + REAL is real-valued evaluation, hence the most precise. All others are compared by mTypeToR m1 <= mTypeToR m2 **) val isMorePrecise_def = Define ` isMorePrecise (m1:mType) (m2:mType) = case m1, m2 of - | M0, _ => T + | REAL, _ => T | F w1 f1, F w2 f2 => w1 <= w2 | F w f, _ => F | _, F w f => F | _, _ => (mTypeToR (m1) <= mTypeToR (m2))`; val morePrecise_def = Define ` - (morePrecise M0 _ = T) /\ + (morePrecise REAL _ = T) /\ (morePrecise (F w1 f1) (F w2 f2) = (w1 <= w2)) /\ (morePrecise (F w f) _ = F) /\ (morePrecise _ (F w f) = F) /\ (morePrecise M16 M16 = T) /\ (morePrecise M32 M32 = T) /\ (morePrecise M32 M16 = T) /\ - (morePrecise M64 M0 = F) /\ + (morePrecise M64 REAL = F) /\ (morePrecise M64 _ = T) /\ (morePrecise _ _ = F) `; @@ -114,18 +110,18 @@ val isMorePrecise_morePrecise = store_thm ( \\ once_rewrite_tac [morePrecise_def, isMorePrecise_def] \\ fs[morePrecise_def, isMorePrecise_def, mTypeToR_def]); -val M0_least_precision = store_thm ("M0_least_precision", +val REAL_least_precision = store_thm ("REAL_least_precision", ``!(m:mType). - isMorePrecise m M0 ==> - m = M0``, + isMorePrecise m REAL ==> + m = REAL``, fs [isMorePrecise_def, mTypeToR_def] \\ rpt strip_tac \\ Cases_on `m` \\ fs []); -val M0_lower_bound = store_thm ("M0_lower_bound", +val REAL_lower_bound = store_thm ("REAL_lower_bound", ``! (m:mType). - isMorePrecise M0 m``, + isMorePrecise REAL m``, Cases_on `m` \\ EVAL_TAC); (** @@ -140,24 +136,24 @@ val join_def = Define ` 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", *) +(* val REAL_join_is_REAL = store_thm ("REAL_join_is_REAL", *) (* ``!m1 m2. *) -(* join m1 m2 = M0 ==> *) -(* (m1 = M0 /\ m2 = M0)``, *) +(* join m1 m2 = REAL ==> *) +(* (m1 = REAL /\ m2 = REAL)``, *) (* fs [join_def, isMorePrecise_def] *) (* \\ rpt strip_tac *) -(* \\ Cases_on `m1 = M0` \\ Cases_on `m2 = M0` \\ fs[] *) -(* >- (m1 = M0 by (Cases_on `mTypeToR m1 <= mTypeToR M0` \\ fs[] *) -(* \\ fs [ONCE_REWRITE_RULE [isMorePrecise_def] M0_least_precision] *) +(* \\ Cases_on `m1 = REAL` \\ Cases_on `m2 = REAL` \\ fs[] *) +(* >- (m1 = REAL by (Cases_on `mTypeToR m1 <= mTypeToR REAL` \\ fs[] *) +(* \\ fs [ONCE_REWRITE_RULE [isMorePrecise_def] REAL_least_precision] *) (* \\ Cases_on `m1` \\ fs[mTypeToR_def] *) (* \\ Cases_on `m2` \\ fs[mTypeToR_def] *) -(* qpat_x_assum `_ = M0` *) +(* qpat_x_assum `_ = REAL` *) (* (fn thm => fs [thm]) *) (* >- (Cases_on `m1` \\ fs [mTypeToR_def]) *) (* >- (Cases_on `m2` \\ fs [mTypeToR_def])); *) val maxExponent_def = Define ` - (maxExponent (M0) = 0n) /\ + (maxExponent (REAL) = 0n) /\ (maxExponent (M16) = 15) /\ (maxExponent (M32) = 127) /\ (maxExponent (M64) = 1023) /\ @@ -166,7 +162,7 @@ val maxExponent_def = Define ` (* | M256 => 1023 *)`; val minExponentPos_def = Define ` - (minExponentPos (M0) = 0n) /\ + (minExponentPos (REAL) = 0n) /\ (minExponentPos (M16) = 14) /\ (minExponentPos (M32) = 126) /\ (minExponentPos (M64) = 1022) /\ @@ -210,7 +206,7 @@ val normal_def = Define ` val denormal_def = Define ` denormal (v:real) (m:mType) = case m of - | M0 => F + | REAL => F | _ => ((abs v) < (minValue_pos m) /\ v <> 0)`; (** @@ -222,13 +218,13 @@ val denormal_def = Define ` val validFloatValue_def = Define ` validFloatValue (v:real) (m:mType) = case m of - | M0 => T + | REAL => T | _ => normal v m \/ denormal v m \/ v = 0` val validValue_def = Define ` validValue (v:real) (m:mType) = case m of - | M0 => T + | REAL => T | _ => abs v <= maxValue m`; val no_underflow_fixed_point = store_thm ( diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml index f6097787e600e037348c7663ba0411e2fbc52509..441f602c2506131776ac8d25fcb92751e8865409 100644 --- a/hol4/IntervalValidationScript.sml +++ b/hol4/IntervalValidationScript.sml @@ -142,7 +142,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", vars_typed ((domain fVars) UNION (domain dVars)) Gamma ==> ? iv err vR. FloverMapTree_find f A = SOME(iv, err) /\ - eval_exp E (toRMap Gamma) (toREval f) vR M0 /\ + eval_exp E (toRMap Gamma) (toREval f) vR REAL /\ (FST iv) <= vR /\ vR <= (SND iv)``, Induct_on `f` \\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac @@ -173,9 +173,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[] \\ rveq \\ fs[]) (* Const case *) >- (qexists_tac `v` \\ fs[] - \\ irule Const_dist' \\ fs[] - \\ qexists_tac `0` \\ fs[perturb_def] - \\ irule mTypeToR_pos) + \\ irule Const_dist' \\ fs[perturb_def, mTypeToR_def]) (* Unary operator case *) >- (first_x_assum (qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct) \\ fs[] @@ -185,12 +183,12 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", >- (qexists_tac `- vR` \\ fs[negateInterval_def, isSupersetInterval_def] \\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def] \\ rpt conj_tac \\ TRY REAL_ASM_ARITH_TAC - \\ irule Unop_neg' \\ qexistsl_tac [`M0`, `vR`] \\ fs[evalUnop_def]) + \\ irule Unop_neg' \\ qexistsl_tac [`REAL`, `vR`] \\ fs[evalUnop_def]) (* Inversion case *) \\ qexists_tac `1 / vR` \\ conj_tac - >- (irule Unop_inv' \\ fs[] \\ qexistsl_tac [`0`, `vR`] - \\ fs[evalUnop_def, perturb_def, REAL_INV_1OVER, mTypeToR_pos, IVhi_def, IVlo_def] + >- (irule Unop_inv' \\ fs[mTypeToR_def] \\ qexistsl_tac [`vR`] + \\ fs[evalUnop_def, mTypeToR_def, perturb_def, REAL_INV_1OVER, mTypeToR_pos, IVhi_def, IVlo_def] \\ CCONTR_TAC \\ fs[] \\ rveq \\ `0 < 0:real` by (REAL_ASM_ARITH_TAC) \\ fs[]) @@ -216,12 +214,12 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", (qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct) \\ fs[domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]) \\ rveq - \\ rename1 `eval_exp E (toRMap Gamma) (toREval f1) vR1 M0` - \\ rename1 `eval_exp E (toRMap Gamma) (toREval f2) vR2 M0` + \\ rename1 `eval_exp E (toRMap Gamma) (toREval f1) vR1 REAL` + \\ rename1 `eval_exp E (toRMap Gamma) (toREval f2) vR2 REAL` \\ qexists_tac `evalBinop b vR1 vR2` \\ conj_tac - >- (irule Binop_dist' - \\ qexistsl_tac [`0:real`, `M0`, `M0`, `vR1`, `vR2`] + >- (irule Binop_dist' \\ fs[mTypeToR_def] + \\ qexistsl_tac [`REAL`, `REAL`, `vR1`, `vR2`] \\ fs[join_def, mTypeToR_pos, perturb_def] \\ strip_tac \\ rveq \\ fs[IVlo_def, IVhi_def] \\ CCONTR_TAC \\ fs[] \\ rveq @@ -282,7 +280,6 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", GSYM REAL_INV_1OVER] interval_division_valid) \\ qpat_x_assum `!x. _` kall_tac \\ REAL_ASM_ARITH_TAC) - (** MARKER **) (* FMA case *) >- (rename1 `Fma (toREval f1) (toREval f2) (toREval f3)` \\ rpt ( @@ -290,13 +287,13 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", (qspecl_then [`A`, `P`, `fVars`, `dVars`, `E`, `Gamma`] destruct) \\ fs[domain_union, UNION_DEF, DIFF_DEF, SUBSET_DEF]) \\ rveq - \\ rename1 `eval_exp E (toRMap Gamma) (toREval f1) vR1 M0` - \\ rename1 `eval_exp E (toRMap Gamma) (toREval f2) vR2 M0` - \\ rename1 `eval_exp E (toRMap Gamma) (toREval f3) vR3 M0` + \\ rename1 `eval_exp E (toRMap Gamma) (toREval f1) vR1 REAL` + \\ rename1 `eval_exp E (toRMap Gamma) (toREval f2) vR2 REAL` + \\ rename1 `eval_exp E (toRMap Gamma) (toREval f3) vR3 REAL` \\ qexists_tac `evalFma vR1 vR2 vR3` \\ conj_tac >- (irule Fma_dist' - \\ qexistsl_tac [`0:real`, `M0`, `M0`, `M0`, `vR1`, `vR2`, `vR3`] + \\ qexistsl_tac [`0:real`, `REAL`, `REAL`, `REAL`, `vR1`, `vR2`, `vR3`] \\ fs [mTypeToR_def, perturb_def, evalFma_def, evalBinop_def, join3_def, join_def]) \\ rename1 `FloverMapTree_find f1 A = SOME (iv_f1, err1)` \\ rename1 `FloverMapTree_find f2 A = SOME (iv_f2, err2)` @@ -331,7 +328,8 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound", \\ qexists_tac `vR` \\ fs[Downcast_dist', isSupersetInterval_def, IVlo_def, IVhi_def] \\ `FST iv = FST intv` by (metis_tac [REAL_LE_ANTISYM]) \\ `SND iv = SND intv` by (metis_tac [REAL_LE_ANTISYM]) - \\ fs[])); + \\ fs[] + )); val getRetExp_def = Define ` (getRetExp (Let m x e g) = getRetExp g) /\ @@ -340,7 +338,7 @@ val getRetExp_def = Define ` val Rmap_updVars_comm = store_thm ( "Rmap_updVars_comm", ``!Gamma n m x. - updDefVars n M0 (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x``, + updDefVars n REAL (toRMap Gamma) x = toRMap (updDefVars n m Gamma) x``, fs [updDefVars_def, toRMap_def] \\ rpt strip_tac \\ Cases_on `x = n` \\ fs[]); @@ -388,7 +386,7 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound", validIntervalboundsCmd f A P dVars ==> ?iv err vR. FloverMapTree_find (getRetExp f) A = SOME (iv, err) /\ - (bstep (toREvalCmd f) E (toRMap Gamma) vR M0 /\ + (bstep (toREvalCmd f) E (toRMap Gamma) vR REAL /\ FST iv <= vR /\ vR <= SND iv)``, Induct_on `f` \\ rpt gen_tac @@ -404,7 +402,7 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound", \\ rename1 `FloverMapTree_find e A = SOME (iv_e, err_e)` \\ first_x_assum (qspecl_then [`A`, `updEnv n vR E`, `fVars`, `insert n () dVars`, - `outVars`, `P`, `updDefVars n M0 Gamma`] + `outVars`, `P`, `updDefVars n REAL Gamma`] destruct) >- (fs [domain_insert] \\ rpt conj_tac @@ -436,7 +434,7 @@ val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound", \\ fs[] \\ irule let_b \\ qexists_tac `vR` \\ fs[] \\ irule swap_Gamma_bstep - \\ qexists_tac `(toRMap (updDefVars n M0 Gamma))` + \\ qexists_tac `(toRMap (updDefVars n REAL Gamma))` \\ fs[Rmap_updVars_comm]) >- (inversion `ssa _ _ _` ssa_cases \\ drule validIntervalbounds_sound diff --git a/hol4/configure_hol.sh b/hol4/configure_hol.sh index 92ba42da8c89d9316e49926e6903f4986024268a..18dbb5236fd63cfd40351632f2b8fec8118cbaef 100755 --- a/hol4/configure_hol.sh +++ b/hol4/configure_hol.sh @@ -23,7 +23,7 @@ then exit 1 fi -DIR=pwd +DIR="$(pwd)" HOLCOMMIT="$(cat ./.HOLCOMMIT)" if [[ "$INIT" = "yes" ]]; diff --git a/hol4/ssaPrgsScript.sml b/hol4/ssaPrgsScript.sml index 6b7c661cbd9061566dd7e2025433fa0ea8f67273..d5fc94d45731a7952064d9b51861bffc0866ad45 100644 --- a/hol4/ssaPrgsScript.sml +++ b/hol4/ssaPrgsScript.sml @@ -156,7 +156,7 @@ val ssa_shadowing_free = store_thm ("ssa_shadowing_free", ``!m x y v v' e f inVars outVars E defVars. ssa (Let m x (toREval e) (toREvalCmd f)) inVars outVars /\ (y IN (domain inVars)) /\ - eval_exp E defVars (toREval e) v M0 ==> + eval_exp E defVars (toREval e) v REAL ==> !E n. updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n``, rpt strip_tac \\ inversion `ssa (Let m x (toREval e) (toREvalCmd f)) _ _` ssa_cases @@ -170,23 +170,23 @@ val ssa_shadowing_free = store_thm ("ssa_shadowing_free", (* val shadowing_free_rewriting_exp = store_thm ("shadowing_free_rewriting_exp", *) (* ``!e v E1 E2 defVars. *) (* (!n. E1 n = E2 n) ==> *) -(* (eval_exp E1 defVars (toREval e) v M0 <=> *) -(* eval_exp E2 defVars (toREval e) v M0)``, *) +(* (eval_exp E1 defVars (toREval e) v REAL <=> *) +(* eval_exp E2 defVars (toREval e) v REAL)``, *) (* Induct \\ rpt strip_tac \\ fs[eval_exp_cases, EQ_IMP_THM] \\ metis_tac[]); *) (* val shadowing_free_rewriting_cmd = store_thm ("shadowing_free_rewriting_cmd", *) (* ``!f E1 E2 vR defVars. *) (* (!n. E1 n = E2 n) ==> *) -(* (bstep (toREvalCmd f) E1 defVars vR M0 <=> *) -(* bstep (toREvalCmd f) E2 defVars vR M0)``, *) +(* (bstep (toREvalCmd f) E1 defVars vR REAL <=> *) +(* bstep (toREvalCmd f) E2 defVars vR REAL)``, *) (* Induct \\ rpt strip_tac \\ fs[EQ_IMP_THM] \\ metis_tac[]); *) (* val dummy_bind_ok = store_thm ("dummy_bind_ok", *) (* ``!e v x v' (inVars:num_set) E defVars. *) (* (domain (usedVars e)) SUBSET (domain inVars) /\ *) (* (~ (x IN (domain inVars))) /\ *) -(* eval_exp E defVars (toREval e) v M0 ==> *) -(* eval_exp (updEnv x v' E) defVars (toREval e) v M0``, *) +(* eval_exp E defVars (toREval e) v REAL ==> *) +(* eval_exp (updEnv x v' E) defVars (toREval e) v REAL``, *) (* Induct \\ rpt strip_tac \\ once_rewrite_tac [toREval_def] \\ qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm)) \\ fs [] \\ rveq \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *) (* >- (match_mp_tac Var_load *) (* \\ fs[usedVars_def, updEnv_def] *) @@ -204,9 +204,9 @@ val ssa_shadowing_free = store_thm ("ssa_shadowing_free", (* \\ qexists_tac `inVars` *) (* \\ qpat_x_assum `domain _ SUBSET _` (fn thm => assume_tac (ONCE_REWRITE_RULE [usedVars_def] thm)) *) (* \\ fs[])) *) -(* >- (`(m1 = M0) /\ (m2 = M0)` by (match_mp_tac ifJoinIs0 \\ fs[]) *) +(* >- (`(m1 = REAL) /\ (m2 = REAL)` by (match_mp_tac ifJoinIs0 \\ fs[]) *) (* \\ rveq *) -(* \\ qpat_assum `M0 = _` (fn thm => once_rewrite_tac [thm]) *) +(* \\ qpat_assum `REAL = _` (fn thm => once_rewrite_tac [thm]) *) (* \\ match_mp_tac Binop_dist \\ fs[] *) (* \\ qpat_x_assum `domain _ SUBSET _` (fn thm => assume_tac (ONCE_REWRITE_RULE [usedVars_def] thm)) *) (* \\ conj_tac \\ first_x_assum match_mp_tac \\ qexists_tac `inVars` \\ fs[domain_union]) *) diff --git a/hol4/transScript.sml b/hol4/transScript.sml index 830a9274f209eca87183426c8ebdead6bb83a98f..ac247a93499d75fb74f16407def99371f01db572 100644 --- a/hol4/transScript.sml +++ b/hol4/transScript.sml @@ -1,6 +1,7 @@ open simpLib realTheory realLib RealArith stringTheory; open ml_translatorTheory ml_translatorLib cfTacticsLib basis basisProgTheory; open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory + MachineTypeTheory ErrorBoundsTheory IntervalArithTheory FloverTactics IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory ErrorValidationTheory CertificateCheckerTheory floverParserTheory; @@ -130,16 +131,16 @@ val _ = translate (MachineTypeTheory.mTypeToR_def GSYM const_1_over_2_pow_24_def, GSYM const_1_over_2_pow_53_def]); -val isMorePrecise_eq = prove( - ``isMorePrecise m1 m2 = - case m1 of - | M0 => T - | M64 => (case m2 of M0 => F | _ => T) - | M32 => (case m2 of M0 => F | M64 => F | _ => T) - | M16 => (case m2 of M16 => T | _ => F)``, - Cases_on `m1` \\ Cases_on `m2` \\ EVAL_TAC); +(* val isMorePrecise_eq = prove( *) +(* ``isMorePrecise m1 m2 = *) +(* case m1 of *) +(* | REAL => T *) +(* | M64 => (case m2 of REAL => F | _ => T) *) +(* | M32 => (case m2 of REAL => F | M64 => F | _ => T) *) +(* | M16 => (case m2 of M16 => T | _ => F)``, *) +(* Cases_on `m1` \\ Cases_on `m2` \\ EVAL_TAC); *) -val _ = translate isMorePrecise_eq; +(* val _ = translate isMorePrecise_eq; *) fun LET_CONV var_name body = (UNBETA_CONV body THENC @@ -164,9 +165,9 @@ val multInterval_eq = |> REWRITE_RULE [absIntvUpd_eq] val _ = translate multInterval_eq -val maxValueM0_def = - let val tm = EVAL ``maxValue M0`` |> concl |> rand in - Define `maxValueM0 = ^tm` end |> translate; +val maxValueREAL_def = + let val tm = EVAL ``maxValue REAL`` |> concl |> rand in + Define `maxValueREAL = ^tm` end |> translate; val maxValueM16_def = let val tm = EVAL ``maxValue M16`` |> concl |> rand in @@ -183,36 +184,38 @@ val maxValueM64_def = val maxValue_eq = prove( ``maxValue m = case m of - | M0 => maxValueM0 + | REAL => maxValueREAL | M16 => maxValueM16 | M32 => maxValueM32 - | M64 => maxValueM64``, + | M64 => maxValueM64 + | F w f => &(2 ** (w − 1) − 1) * &(2 ** maxExponent m)``, Cases_on `m` \\ EVAL_TAC) |> translate; -val minValueM0_def = - let val tm = EVAL ``minValue M0`` |> concl |> rand in - Define `minValueM0 = ^tm` end |> translate; +val minValue_posREAL_def = + let val tm = EVAL ``minValue_pos REAL`` |> concl |> rand in + Define `minValue_posREAL = ^tm` end |> translate; -val minValueM16_def = - let val tm = EVAL ``minValue M16`` |> concl |> rand in - Define `minValueM16 = ^tm` end |> translate; +val minValue_posM16_def = + let val tm = EVAL ``minValue_pos M16`` |> concl |> rand in + Define `minValue_posM16 = ^tm` end |> translate; -val minValueM32_def = - let val tm = EVAL ``minValue M32`` |> concl |> rand in - Define `minValueM32 = ^tm` end |> translate; +val minValue_posM32_def = + let val tm = EVAL ``minValue_pos M32`` |> concl |> rand in + Define `minValue_posM32 = ^tm` end |> translate; -val minValueM64_def = - let val tm = EVAL ``minValue M64`` |> concl |> rand in - Define `minValueM64 = ^tm` end |> translate; +val minValue_posM64_def = + let val tm = EVAL ``minValue_pos M64`` |> concl |> rand in + Define `minValue_posM64 = ^tm` end |> translate; -val minValue_eq = prove( - ``minValue m = +val minValue_pos_eq = prove( + ``minValue_pos m = case m of - | M0 => minValueM0 - | M16 => minValueM16 - | M32 => minValueM32 - | M64 => minValueM64``, + | REAL => minValue_posREAL + | M16 => minValue_posM16 + | M32 => minValue_posM32 + | M64 => minValue_posM64 + | F w f => 0``, Cases_on `m` \\ EVAL_TAC) |> translate;