Commit c7ff0b5e authored by Heiko Becker's avatar Heiko Becker

WIP: Start working on HOL4 fixed-point checking

parent 8a64fbf4
......@@ -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 * (mTypeToQ m)) /\
(abs (v1 - v2) <= abs v1 * (mTypeToR 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) * (mTypeToQ m)``,
abs (v - v2) <= (abs v) * (mTypeToR 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) * (mTypeToQ m)`
abs (v - v2) <= (abs v) * (mTypeToR m)`
(fn thm => irule (SIMP_RULE std_ss [] thm))
approxEnv_ind
\\ rpt strip_tac
......
......@@ -17,10 +17,10 @@ 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 E2 defVars (Const m n) nF m ==>
abs (nR - nF) <= abs n * (mTypeToQ m)``,
abs (nR - nF) <= abs n * (mTypeToR m)``,
rpt strip_tac
\\ fs[eval_exp_cases]
\\ `perturb n delta = n` by (irule delta_0_deterministic \\ fs[mTypeToQ_def])
\\ `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);
......@@ -35,7 +35,7 @@ val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
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) * (mTypeToQ m))``,
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 []
......@@ -80,7 +80,7 @@ val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
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) * (mTypeToQ m))``,
abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F) * (mTypeToR 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 []
......@@ -129,7 +129,7 @@ val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
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) * (mTypeToQ m))``,
abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + (abs (e1F * e2F) * (mTypeToR 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 []
......@@ -171,7 +171,7 @@ val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
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) * (mTypeToQ m))``,
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 []
......@@ -215,7 +215,7 @@ val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded",
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 /\
abs (e3R - e3F) <= err3 ==>
abs (vR - vF) <= abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + abs (e1F + e2F * e3F) * (mTypeToQ m)``,
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 []
......@@ -254,7 +254,7 @@ val round_abs_err_bounded = store_thm ("round_abs_err_bounded",
eval_exp (updEnv 1 nF1 emptyEnv) (updDefVars 1 m defVars)
(Downcast machineEpsilon (Var 1)) nF machineEpsilon /\
abs (nR - nF1) <= err ==>
abs (nR - nF) <= err + (abs nF1) * (mTypeToQ machineEpsilon)``,
abs (nR - nF) <= err + (abs nF1) * (mTypeToR machineEpsilon)``,
rpt strip_tac
\\ `nR - nF = (nR - nF1) + (nF1 - nF)` by REAL_ASM_ARITH_TAC
\\ fs []
......
......@@ -24,8 +24,8 @@ val validErrorbound_def = Define `
| SOME (intv, err), SOME m =>
(if (0 <= err) then
case e of
| Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * (mTypeToQ m) <= err)
| Const _ n => (maxAbs intv * (mTypeToQ m) <= err)
| 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
......@@ -44,16 +44,16 @@ val validErrorbound_def = Define `
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
(case op of
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| 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) * (mTypeToQ m)) <= err)
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToR m)) <= err)
else F))
| _, _ => F
else F)
......@@ -73,7 +73,7 @@ val validErrorbound_def = Define `
let upperBoundE3 = maxAbs ive3 in
let errIntv_prod = multInterval errIve2 errIve3 in
let mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3) in
(err1 + mult_error_bound + (maxAbs (addInterval errIve1 errIntv_prod)) * (mTypeToQ m)) <= err
(err1 + mult_error_bound + (maxAbs (addInterval errIve1 errIntv_prod)) * (mTypeToR m)) <= err
|_, _, _ => F
else F)
| Downcast m1 e1 =>
......@@ -81,7 +81,7 @@ val validErrorbound_def = Define `
| SOME (ive1, err1) =>
let rec_res = validErrorbound e1 typeMap A dVars in
let errIve1 = widenInterval ive1 err1 in
rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToQ m1)) <= err)
rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToR m1)) <= err)
else F)
| _, _ => F`;
......@@ -168,17 +168,17 @@ val validErrorboundCorrectVariable = store_thm (
\\ fs[domain_lookup])
\\ fs[usedVars_def,domain_lookup]
\\ irule REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo,nhi) * mTypeToQ m` \\ fs[]
\\ qexists_tac `maxAbs (nlo,nhi) * mTypeToR m` \\ fs[]
\\ drule approxEnv_fVar_bounded
\\ rpt (disch_then drule)
\\ disch_then (qspec_then `m` assume_tac)
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs nR * mTypeToQ m`
\\ qexists_tac `abs nR * mTypeToR 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 mTypeToQ_pos);
\\ irule mTypeToR_pos);
val validErrorboundCorrectConstant_eval = store_thm (
"validErrorboundCorrectConstant_eval",
......@@ -187,10 +187,10 @@ val validErrorboundCorrectConstant_eval = store_thm (
?nF m1.
eval_exp E2 Gamma (Const m n) nF m1``,
rpt strip_tac
\\ qexistsl_tac [`perturb n (mTypeToQ m)`,`m`] \\ irule Const_dist'
\\ qexistsl_tac [`perturb n (mTypeToR m)`,`m`] \\ irule Const_dist'
\\ fs[]
\\ qexists_tac `mTypeToQ m`
\\ fs[realTheory.abs, mTypeToQ_pos]);
\\ qexists_tac `mTypeToR m`
\\ fs[realTheory.abs, mTypeToR_pos]);
val validErrorboundCorrectConstant = store_thm (
"validErrorboundCorrectConstant",
......@@ -209,10 +209,10 @@ val validErrorboundCorrectConstant = store_thm (
\\ `nR = n` by (metis_tac [delta_M0_deterministic]) \\ rveq
\\ inversion `eval_exp _ _ _ _ m` eval_exp_cases
\\ simp[perturb_def]
\\ rename1 `abs deltaF <= (mTypeToQ m)`
\\ rename1 `abs deltaF <= (mTypeToR m)`
\\ simp [Rabs_err_simpl, ABS_MUL]
\\ irule REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo, nhi) * (mTypeToQ m)` \\ conj_tac \\ simp[]
\\ 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[]);
......@@ -250,7 +250,7 @@ val validErrorboundCorrectAddition = store_thm (
by (irule typingSoundnessExp \\ metis_tac [])
\\ fs [] \\ rveq
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + (abs (nF1 + nF2) * (mTypeToQ (join m1 m2)))`
\\ qexists_tac `err1 + err2 + (abs (nF1 + nF2) * (mTypeToR (join m1 m2)))`
\\ conj_tac
>- (irule add_abs_err_bounded
\\ qexistsl_tac [`E1`, `E2`, `Gamma`, `e1`, `nR1`, `e2`, `nR2`, `m1`, `m2`]
......@@ -259,10 +259,10 @@ val validErrorboundCorrectAddition = store_thm (
\\ qexists_tac
`err1 + err2 + maxAbs (
addInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * (mTypeToQ (join m1 m2))`
(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[mTypeToQ_def,mTypeToQ_pos]
\\ simp[mTypeToR_def,mTypeToR_pos]
\\ match_mp_tac maxAbs
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv
......@@ -309,7 +309,7 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra
by (irule typingSoundnessExp \\ metis_tac [])
\\ fs [] \\ rveq
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + err2 + (abs (nF1 - nF2) * (mTypeToQ (join m1 m2)))`
\\ qexists_tac `err1 + err2 + (abs (nF1 - nF2) * (mTypeToR (join m1 m2)))`
\\ conj_tac
>- (irule subtract_abs_err_bounded
\\ qexistsl_tac [`E1`, `E2`, `Gamma`, `e1`, `nR1`, `e2`, `nR2`, `m1`, `m2`]
......@@ -318,10 +318,10 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra
\\ qexists_tac
`err1 + err2 + maxAbs (
subtractInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * (mTypeToQ (join m1 m2))`
(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[mTypeToQ_def,mTypeToQ_pos]
\\ simp[mTypeToR_def,mTypeToR_pos]
\\ match_mp_tac maxAbs
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv
......@@ -968,7 +968,7 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
\\ rpt (disch_then drule)
\\ fs[])
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * (mTypeToQ (join m1 m2))`
\\ qexists_tac `abs (nR1 * nR2 - nF1 * nF2) + abs (nF1 * nF2) * (mTypeToR (join m1 m2))`
\\ conj_tac
>- (irule mult_abs_err_bounded \\ TRY asm_exists_tac \\ fs[]
\\ qexistsl_tac [`E2`, `e2`, `m1`, `m2`]
......@@ -977,13 +977,13 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
\\ qexists_tac `maxAbs (e1lo,e1hi) * err2 + maxAbs (e2lo,e2hi) * err1 +
err1 * err2 +
maxAbs (multInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * (mTypeToQ (join m1 m2))`
(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[mTypeToQ_def,mTypeToQ_pos]
\\ simp[mTypeToR_def,mTypeToR_pos]
\\ match_mp_tac maxAbs
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (irule distance_gives_iv
......@@ -2090,7 +2090,7 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
\\ rpt (disch_then drule)
\\ fs[])
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + abs (nF1 / nF2) * (mTypeToQ (join m1 m2))`
\\ qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + abs (nF1 / nF2) * (mTypeToR (join m1 m2))`
\\ conj_tac
>- (irule div_abs_err_bounded \\ asm_exists_tac \\ fs[]
\\ qexistsl_tac [`E2`, `e2`, `m1`, `m2`] \\ fs [])
......@@ -2110,7 +2110,7 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
>- (simp[maxAbs_def]
\\ once_rewrite_tac [REAL_MUL_COMM]
\\ fs[join_def] \\ irule REAL_LE_LMUL_IMP
\\ simp[mTypeToQ_def,mTypeToQ_pos]
\\ 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
......@@ -2166,7 +2166,7 @@ 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) * (mTypeToQ (join3 m1 m2 m3))`
\\ qexists_tac `abs ((nR1 - nF1) + (nR2 * nR3 - nF2 * nF3)) + abs (nF1 + nF2 * nF3) * (mTypeToR (join3 m1 m2 m3))`
\\ conj_tac
>- (irule fma_abs_err_bounded \\ TRY (asm_exists_tac \\ fs[])
\\ rpt (asm_exists_tac \\ fs[toREval_def]))
......@@ -2207,7 +2207,7 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
\\ once_rewrite_tac [REAL_MUL_COMM] \\ fs[join3_def]
\\ ntac 2 (once_rewrite_tac [join_def])
\\ irule REAL_LE_LMUL_IMP
\\ simp[mTypeToQ_def,mTypeToQ_pos]
\\ 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)
......@@ -2236,14 +2236,14 @@ val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding"
by (irule typingSoundnessExp \\ metis_tac [])
\\ fs[] \\ rveq
\\ irule REAL_LE_TRANS
\\ qexists_tac `err1 + (abs nF1) * mTypeToQ mEps` \\ fs []
\\ qexists_tac `err1 + (abs nF1) * mTypeToR 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 [mTypeToQ_pos]
\\ fs [mTypeToR_pos]
\\ fs [maxAbs_def]
\\ match_mp_tac maxAbs
\\ fs [widenInterval_def,IVlo_def,IVhi_def]
......@@ -2403,13 +2403,13 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ conj_tac \\ rpt strip_tac
>- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) 0`, `join m1 m2`]
\\ irule Binop_dist'
\\ qexistsl_tac [`0`, `m1`, `m2`, `nF1`, `nF2`] \\ fs[mTypeToQ_pos])
\\ qexistsl_tac [`0`, `m1`, `m2`, `nF1`, `nF2`] \\ fs[mTypeToR_pos])
\\ rpt strip_tac
\\ `perturb (evalBinop op nR1 nR2) delta = evalBinop op nR1 nR2`
by (irule delta_0_deterministic \\ fs[mTypeToQ_def, join_def])
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 <= mTypeToQ (join mF1 mF2)`
\\ 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)
......@@ -2434,7 +2434,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ TRY (once_rewrite_tac [validErrorbound_def] \\ fs[] \\ FAIL_TAC "")
\\ irule Binop_dist'
\\ qexistsl_tac [`0`, `M0`, `M0`, `nR1`, `nR2`]
\\ fs[perturb_def, mTypeToQ_pos, join_def])
\\ fs[perturb_def, mTypeToR_pos, join_def])
>- (rename1 `Fma e1 e2 e3`
\\ Flover_compute ``validErrorbound``
\\ Flover_compute ``validIntervalbounds``
......@@ -2536,13 +2536,13 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
>- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) 0`, `join3 m1 m2 m3`]
\\ irule Fma_dist'
\\ qexistsl_tac [`0`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`]
\\ fs[mTypeToQ_pos])
\\ fs[mTypeToR_pos])
\\ rpt strip_tac
\\ `perturb (evalFma nR1 nR2 nR3) delta = evalFma nR1 nR2 nR3`
by (irule delta_0_deterministic \\ fs[mTypeToQ_def, join3_def, join_def])
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 <= mTypeToQ (join3 mF1 mF2 mF3)`
\\ 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)
......@@ -2565,7 +2565,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
>- (simp [Once toREval_def]
\\ irule Fma_dist'
\\ qexistsl_tac [`0`, `M0`, `M0`, `M0`, `nR1`, `nR2`, `nR3`]
\\ fs[perturb_def, mTypeToQ_pos]))
\\ fs[perturb_def, mTypeToR_pos]))
>- (rename1 `Downcast m1 e1`
\\ Flover_compute ``validErrorbound``
\\ Flover_compute ``typeCheck``
......@@ -2606,7 +2606,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
>- (qexistsl_tac [`perturb nF 0`, `m1`]
\\ irule Downcast_dist' \\ fs[]
\\ qexistsl_tac [`0`, `m`, `nF`]
\\ fs[mTypeToQ_pos, isMorePrecise_morePrecise])
\\ fs[mTypeToR_pos, isMorePrecise_morePrecise])
\\ irule validErrorboundCorrectRounding
\\ qpat_x_assum `eval_exp E2 _ e1 _ _` kall_tac
\\ inversion `eval_exp E2 _ (Downcast m1 e1) _ _` eval_exp_cases
......
......@@ -85,29 +85,29 @@ val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
E x = SOME v ==>
eval_exp E defVars (Var x) v m) /\
(!E defVars m n delta.
abs delta <= (mTypeToQ m) ==>
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.
abs delta <= (mTypeToQ m) /\
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.
isMorePrecise m1 m /\
abs delta <= (mTypeToQ 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.
abs delta <= (mTypeToQ (join m1 m2)) /\
abs delta <= (mTypeToR (join m1 m2)) /\
eval_exp E defVars f1 v1 m1 /\
eval_exp E defVars f2 v2 m2 /\
((b = Div) ==> (v2 <> 0)) ==>
eval_exp E defVars (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2)) /\
(!E defVars m1 m2 m3 f1 f2 f3 v1 v2 v3 delta.
abs delta <= (mTypeToQ (join3 m1 m2 m3)) /\
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 ==>
......@@ -144,7 +144,7 @@ save_thm ("Downcast_dist", Downcast_dist);
val Const_dist' = store_thm (
"Const_dist'",
``!m n delta v m' E Gamma.
(abs delta) <= (mTypeToQ m) /\
(abs delta) <= (mTypeToR m) /\
v = perturb n delta /\
m' = m ==>
eval_exp E Gamma (Const m n) v m'``,
......@@ -162,7 +162,7 @@ val Unop_neg' = store_thm (
val Unop_inv' = store_thm (
"Unop_inv'",
``!m f1 v1 delta v m' E Gamma.
(abs delta) <= (mTypeToQ m) /\
(abs delta) <= (mTypeToR m) /\
eval_exp E Gamma f1 v1 m /\
(v1 <> 0) /\
v = perturb (evalUnop Inv v1) delta /\
......@@ -173,7 +173,7 @@ val Unop_inv' = store_thm (
val Downcast_dist' = store_thm ("Downcast_dist'",
``!m m1 f1 v1 delta v m' E Gamma.
isMorePrecise m1 m /\
(abs delta) <= (mTypeToQ m) /\
(abs delta) <= (mTypeToR m) /\
eval_exp E Gamma f1 v1 m1 /\
v = perturb v1 delta /\
m' = m ==>
......@@ -185,7 +185,7 @@ val Downcast_dist' = store_thm ("Downcast_dist'",
val Binop_dist' = store_thm ("Binop_dist'",
``!m1 m2 op f1 f2 v1 v2 delta v m' E Gamma.
(abs delta) <= (mTypeToQ m') /\
(abs delta) <= (mTypeToR m') /\
eval_exp E Gamma f1 v1 m1 /\
eval_exp E Gamma f2 v2 m2 /\
((op = Div) ==> (v2 <> 0)) /\
......@@ -196,7 +196,7 @@ val Binop_dist' = store_thm ("Binop_dist'",
val Fma_dist' = store_thm ("Fma_dist'",
``!m1 m2 m3 f1 f2 f3 v1 v2 v3 delta v m' E Gamma.
(abs delta) <= (mTypeToQ m') /\
(abs delta) <= (mTypeToR m') /\
eval_exp E Gamma f1 v1 m1 /\
eval_exp E Gamma f2 v2 m2 /\
eval_exp E Gamma f3 v3 m3 /\
......@@ -227,8 +227,8 @@ val delta_0_deterministic = store_thm("delta_0_deterministic",
fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
val delta_M0_deterministic = store_thm("delta_M0_deterministic",
``!(v:real) (delta:real). abs delta <= mTypeToQ M0 ==> perturb v delta = v``,
fs [mTypeToQ_def,perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
``!(v:real) (delta:real). abs delta <= mTypeToR M0 ==> perturb v delta = v``,
fs [mTypeToR_def,perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
val toRMap_def = Define `
toRMap (d:num -> mType option) (n:num) : mType option =
......@@ -264,7 +264,7 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
Induct_on `f`
>- (rw [toREval_def] \\ fs [eval_exp_cases])
>- (rw [toREval_def]
\\ fs [eval_exp_cases, mTypeToQ_def, delta_0_deterministic])
\\ fs [eval_exp_cases, mTypeToR_def, delta_0_deterministic])
>- (rw []
\\ rpt (
qpat_x_assum `eval_exp _ _ (toREval _) _ _`
......@@ -272,7 +272,7 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ Cases_on `u` \\ fs [eval_exp_cases] \\ rw []
\\ fs [eval_exp_cases]
>- (res_tac \\ fs [REAL_NEG_EQ])
>- (res_tac \\ fs [mTypeToQ_def, delta_0_deterministic]))
>- (res_tac \\ fs [mTypeToR_def, delta_0_deterministic]))
>- (rw[]
\\ rename1 `Binop b f1 f2`
\\ rpt (
......@@ -287,7 +287,7 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ rename1 `eval_exp _ _ (toREval f2) vf22 m2`
\\ `m1 = M0 /\ m2 = M0` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs [])
\\ rw []
\\ fs [join_def, mTypeToQ_def, delta_0_deterministic]
\\ 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)
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`vf11`,`vf12`] ASSUME_TAC thm)
\\ res_tac
......@@ -305,7 +305,7 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v3`,`v3'`, `E`, `defVars`] ASSUME_TAC thm)
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v2'`,`v2''`, `E`, `defVars`] ASSUME_TAC thm)
\\ qpat_x_assum `!v1 v2 E defVars. _ /\ _ ==> v1 = v2` (fn thm =>qspecl_then [`v1'`,`v1''`, `E`, `defVars`] ASSUME_TAC thm)
\\ fs [join3_def, join_def, mTypeToQ_def, delta_0_deterministic])
\\ fs [join3_def, join_def, mTypeToR_def, delta_0_deterministic])
>- (rw[]
\\ rpt (
qpat_x_assum `eval_exp _ _ (toREval (Downcast _ _)) _ _`
......@@ -322,7 +322,7 @@ variables in the Environment.
val binary_unfolding = store_thm("binary_unfolding",
``!(b:binop) (f1:(real)exp) (f2:(real)exp) E Gamma (v:real) v1 v2 m1 m2 delta.
(b = Div ==> (v2 <> 0)) /\
(abs delta) <= (mTypeToQ (join m1 m2)) /\
(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) ==>
......@@ -334,7 +334,7 @@ val binary_unfolding = store_thm("binary_unfolding",
val fma_unfolding = store_thm("fma_unfolding",
``!(f1:(real)exp) (f2:(real)exp) (f3:(real)exp) E Gamma (v:real) v1 v2 v3 m1 m2 m3 delta.
(abs delta) <= (mTypeToQ (join3 m1 m2 m3)) /\
(abs delta) <= (mTypeToR (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 /\
......
......@@ -641,7 +641,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE",
\\ fs[optionLift_def, normal_or_zero_def, minValue_def,
minExponentPos_def, REAL_LT_INV_EQ]
\\ qexists_tac `0:real`
\\ fs[mTypeToQ_pos, perturb_def, fp64_to_float_float_to_fp64,
\\ fs[mTypeToR_pos, perturb_def, fp64_to_float_float_to_fp64,
zero_to_real])
>- (fs[eval_exp_float_def, optionLift_def]
\\ first_x_assum (qspecl_then [`E1`, `E2`, `E2_real`, `Gamma`, `tMap`, `v1`, `A`, `P`, `fVars`, `dVars`] destruct)
......@@ -786,7 +786,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE",
\\ asm_exists_tac \\ fs[])
\\ qexists_tac ` 0:real`
\\ Cases_on `b`
\\ fs[perturb_def, evalBinop_def, mTypeToQ_pos, join_def])
\\ 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,14 +862,14 @@ 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[mTypeToQ_def, join_def])
\\ fs[mTypeToR_def, join_def])
(* result = 0 *)
>- (fs[REAL_LNEG_UNIQ, evalBinop_def]
\\ fs[fp64_add_def, dmode_def, fp64_to_float_float_to_fp64]
\\ fs[float_add_def]
\\ fs[join_def]
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, mTypeToQ_pos, evalBinop_def]
\\ 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])
......@@ -905,18 +905,18 @@ 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[mTypeToQ_def, join_def])
\\ fs[mTypeToR_def, join_def])
>- (fs[evalBinop_def]
\\ qpat_x_assum `float_to_real (fp64_to_float _) = _` MP_TAC
\\ simp[real_sub, REAL_LNEG_UNIQ, evalBinop_def]
\\ fs[fp64_sub_def, dmode_def, fp64_to_float_float_to_fp64]
\\ fs[float_sub_def]
\\ fs[join_def]
\\ fs[perturb_def, mTypeToQ_pos, evalBinop_def]
\\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
\\ fs[validValue_gives_float_value, float_round_with_flags_def]
\\ strip_tac
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`, `float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, mTypeToQ_pos, evalBinop_def]
\\ 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])
......@@ -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[mTypeToQ_def, join_def])
\\ fs[mTypeToR_def, join_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, mTypeToQ_pos])
\\ fs[GSYM float_is_zero_to_real, float_is_zero_def, join_def, mTypeToR_pos])
(* 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[mTypeToQ_def, join_def])
\\ fs[mTypeToR_def, join_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`
......@@ -1022,7 +1022,7 @@ val eval_exp_gives_IEEE = store_thm ("eval_exp_gives_IEEE",
by (fs[GSYM float_is_zero_to_real, float_is_zero_def])
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, join_def, mTypeToQ_pos]))
\\ fs[perturb_def, join_def, mTypeToR_pos]))
>- (rename1 `Fma (toRExp e1) (toRExp e2) (toRExp e3)`
\\ qpat_x_assum `M64 = _` (fn thm => fs [GSYM thm])
\\ `FloverMapTree_find (toRExp e1) tMap = SOME M64 /\
......
......@@ -208,4 +208,5 @@ fun Flover_compute t =
(* Flover_compute_steps terms_to_eval g *)