Skip to content

GitLab

F
FloVer
Commit d78f37ce authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Merge branch 'HOL4_fix' into 'master' 

Fast-forward CakeML to latest state and port dev in HOL4 to fix irule semantics changes

Closes #8

See merge request AVA/FloVer!11
parents be900b25 5e41371e
Hide whitespace changes
Inline Side-by-side
Showing with 29 additions and 27 deletions
hol4/.HOLCOMMIT
View file @ d78f37ce
bb9eaf3448d2c44c84c5d06849d0dc73db23670c
7ed3f12092db2062b6fccb60e9735143ecd5c7e5
hol4/ErrorBoundsScript.sml
View file @ d78f37ce
......@@ -314,7 +314,7 @@ val float_fma_tac =
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ triangle_tac
\\ irule REAL_LE_ADD2
\\ irule REAL_LE_ADD2 \\ conj_tac
\\ TRY (REAL_ASM_ARITH_TAC)
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ irule REAL_LE_MUL2 \\ fs[REAL_ABS_POS]
......
hol4/ErrorValidationScript.sml
View file @ d78f37ce
......@@ -1046,11 +1046,11 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + computeError (nF1 * nF2) m`
\\ conj_tac
>- (irule mult_abs_err_bounded
>- (irule mult_abs_err_bounded \\ rpt conj_tac
\\ rpt (find_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS \\ find_exists_tac
\\ conj_tac \\ fs[join_def]
\\ irule REAL_LE_ADD2
\\ irule REAL_LE_ADD2 \\ conj_tac
>- (irule multiplicationErroBounded \\ fs[])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
......@@ -2186,7 +2186,7 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + computeError (nF1 / nF2) m`
\\ conj_tac
>- (irule div_abs_err_bounded
>- (irule div_abs_err_bounded \\ rpt conj_tac
\\ rpt (find_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS \\ find_exists_tac
\\ conj_tac \\ fs[join_def]
......@@ -2198,7 +2198,7 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ irule REAL_LE_ADD2
\\ irule REAL_LE_ADD2 \\ conj_tac
>- (irule divisionErrorBounded \\ fs[])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
......@@ -2283,10 +2283,11 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
\\ qexists_tac `abs ((nR1 - nF1) + (nR2 * nR3 - nF2 * nF3)) +
computeError (nF1 + nF2 * nF3) m`
\\ conj_tac
>- (irule fma_abs_err_bounded \\ rpt (find_exists_tac \\ fs[toREval_def]))
>- (irule fma_abs_err_bounded \\ rpt conj_tac
\\ rpt (find_exists_tac \\ fs[toREval_def]))
\\ irule REAL_LE_TRANS \\ find_exists_tac
\\ conj_tac \\ fs[join_def]
\\ irule REAL_LE_ADD2
\\ irule REAL_LE_ADD2 \\ rpt conj_tac
>- (irule triangle_trans \\ fs[REAL_ABS_TRIANGLE]
\\ irule REAL_LE_ADD2 \\ fs[]
\\ irule multiplicationErroBounded \\ fs[])
......@@ -2529,7 +2530,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
then toRBMap fBits (Binop op e1 e2)
else toRBMap fBits e)
(Binop op (Var 1) (Var 2)) (perturb (evalBinop op v1 v2) mF delta2) mF`
by (irule binary_unfolding \\ fs[]
by (irule binary_unfolding \\ fs[] \\ rpt conj_tac
>- (find_exists_tac \\ fs[])
\\ find_exists_tac \\ fs[])
\\ Cases_on `op` \\ rveq
......@@ -2674,7 +2675,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
then toRBMap fBits (Fma e1 e2 e3)
else toRBMap fBits e)
(Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) mF delta2) mF`
by (irule fma_unfolding \\ fs[]
by (irule fma_unfolding \\ conj_tac \\ fs[]
>- (find_exists_tac \\ fs[])
\\ find_exists_tac \\ fs[])
\\ rveq
......@@ -2892,13 +2893,14 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
\\ rename1 `eval_expr _ _ _ _ vf m`
\\ first_x_assum match_mp_tac
\\ `FloverMapTree_find e exprTypes = SOME m`
by (irule typingSoundnessExp \\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `vf`] \\ fs[])
by (irule typingSoundnessExp \\ rpt conj_tac
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `vf`] \\ fs[])
\\ qexistsl_tac [`A`, `updEnv n vr E1`, `updEnv n vf E2`, `outVars`,
`fVars`, `insert n () dVars`, `elo`, `ehi`, `P`, `m'`,
`exprTypes`, `updDefVars n m Gamma`, `fBits`]
\\ fs [Once getRetExp_def]
\\ rpt conj_tac
>- (irule approxUpdBound
>- (irule approxUpdBound \\ rpt conj_tac
\\ fs[]
>- (Cases_on `lookup n (union fVars dVars)` \\ fs [domain_lookup])
\\ qspecl_then
......
hol4/IEEE_connectionScript.sml
View file @ d78f37ce
......@@ -195,9 +195,9 @@ val normal_value_is_float_value = store_thm (
normal (float_to_real ((ff):(52,11) float)) M64 ==>
float_value ff = Float (float_to_real ff)``,
rpt strip_tac
\\rewrite_tac[float_value_def]
\\rw_thm_asm `normal _ _` normal_def
\\fs[float_to_real_def]
\\ 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_pos_def, minExponentPos_def]
>-( Cases_on `ff.Sign` \\ fs[]
\\ Cases_on `n` \\ fs[]
......@@ -212,7 +212,7 @@ val normal_value_is_float_value = store_thm (
\\ strip_tac
>- (`abs (cst1 * cst2) = cst1 * cst2`
by (once_rewrite_tac[ABS_REFL]
\\ irule REAL_LE_MUL
\\ irule REAL_LE_MUL \\ rpt conj_tac
\\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
\\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
\\ fs[]
......@@ -239,7 +239,7 @@ val normal_value_is_float_value = store_thm (
\\ fs[]
\\ qmatch_abbrev_tac `~ (cst1 * cst2 <= 0:real)`
\\ once_rewrite_tac [REAL_NOT_LE]
\\ irule REAL_LT_MUL
\\ irule REAL_LT_MUL \\ conj_tac
\\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
\\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
\\ irule REAL_LT_ADD \\ fs[]
......@@ -504,7 +504,7 @@ val typing_expr_64bit = store_thm("typing_expr_64bit",
>- (fs[] \\ rveq \\ fs[is64BitEval_def])
>- (fs[]
\\ `FloverMapTree_find e tMap = SOME M64`
by (first_x_assum irule
by (first_x_assum irule \\ conj_tac
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexistsl_tac [`Gamma`, `fBits`]
\\ rpt strip_tac
......@@ -514,13 +514,13 @@ val typing_expr_64bit = store_thm("typing_expr_64bit",
>- (rename1 `Binop b e1 e2`
\\ fs[]
\\ `FloverMapTree_find e2 tMap = SOME M64`
by (first_x_assum irule
by (first_x_assum irule \\ conj_tac
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexistsl_tac [`Gamma`, `fBits`] \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ fs[])
\\ `FloverMapTree_find e1 tMap = SOME M64`
by (first_x_assum irule
by (first_x_assum irule \\ conj_tac
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexistsl_tac [`Gamma`, `fBits`] \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
......@@ -530,19 +530,19 @@ val typing_expr_64bit = store_thm("typing_expr_64bit",
\\ rename1 `Fma e1 e2 e3`
\\ fs[]
\\ `FloverMapTree_find e3 tMap = SOME M64`
by (first_x_assum irule
by (first_x_assum irule \\ conj_tac
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexistsl_tac [`Gamma`, `fBits`] \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ fs[])
\\ `FloverMapTree_find e2 tMap = SOME M64`
by (first_x_assum irule
by (first_x_assum irule \\ conj_tac
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexistsl_tac [`Gamma`, `fBits`] \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
\\ fs[])
\\ `FloverMapTree_find e1 tMap = SOME M64`
by (first_x_assum irule
by (first_x_assum irule \\ conj_tac
>- (rw_thm_asm `is64BitEval _` is64BitEval_def \\ fs[])
\\ qexistsl_tac [`Gamma`, `fBits`] \\ rpt strip_tac
>- (first_x_assum irule \\ simp[Once usedVars_def, domain_union])
......@@ -562,7 +562,7 @@ val typing_cmd_64bit = store_thm (
\\ fs[]
>- (rveq \\ once_rewrite_tac [getRetExp_def]
\\ fs[]
\\ first_x_assum irule
\\ first_x_assum irule \\ conj_tac
\\ fs[Once is64BitBstep_def, Once noDowncastFun_def]
\\ qexistsl_tac [`updDefVars n m Gamma`, `fBits`]
\\ fs[]
......@@ -1143,7 +1143,7 @@ val bstep_gives_IEEE = store_thm (
>- (`?v_e. eval_expr_float e E2 = SOME v_e /\
eval_expr (toREnv E2) Gamma (toRBMap fBits) (toRExp e)
(float_to_real (fp64_to_float v_e)) M64`
by (irule eval_expr_gives_IEEE \\ fs[]
by (irule eval_expr_gives_IEEE \\ rpt conj_tac \\ fs[]
>- (rpt strip_tac \\ first_x_assum irule
\\ fs[Once freeVars_def, domain_union]
\\ CCONTR_TAC \\ fs[] \\ rveq \\ fs[]
......@@ -1373,7 +1373,7 @@ val bstep_gives_IEEE = store_thm (
\\ asm_exists_tac \\ fs[]
\\ strip_tac \\ fs[toREnv_def, updEnv_def, updFlEnv_def]
\\ IF_CASES_TAC \\ fs[])
>- (fs[bstep_cases] \\ irule eval_expr_gives_IEEE
>- (fs[bstep_cases] \\ irule eval_expr_gives_IEEE \\ rpt conj_tac
\\ fs[]
>- (rpt strip_tac \\ first_x_assum irule
\\ fs[freeVars_def] \\ fs[])
......
cakeml @ 645d4af0
Compare 7f486a5f...645d4af0
Subproject commit 7f486a5f00f273d5ba21cc8ea98aaddf822ec371
Subproject commit 645d4af010862abf8d2245a879b09d51e48d9afc
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment