Commit a5076909 authored by Heiko Becker's avatar Heiko Becker
Browse files

Finish Error Validation

parent dac0edc4
......@@ -98,6 +98,7 @@ val validErrorbound_def = Define `
if (validErrorbound e1 typeMap A dVars)
then
case FloverMapTree_find e1 A of
| NONE => F
| SOME (ive1, err1) =>
let errIve1 = widenInterval ive1 err1;
mAbs = maxAbs errIve1 in
......@@ -2119,7 +2120,6 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
(e1lo <= nR1 /\ nR1 <= e1hi) /\
(e2lo <= nR2 /\ nR2 <= e2hi) /\
(e3lo <= nR3 /\ nR3 <= e3hi) /\
noDivzero e2hi e2lo /\
FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
FloverMapTree_find e3 A = SOME ((e3lo, e3hi), err3) /\
......@@ -2190,7 +2190,7 @@ val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding"
validErrorbound (Downcast mEps e) Gamma A dVars /\
elo <= nR /\ nR <= ehi /\
FloverMapTree_find e A = SOME ((elo, ehi), err1) /\
FloverMapTree_find (Downcast mEps e) A = SOME ((elo, ehi), err) /\
FloverMapTree_find (Downcast mEps e) A = SOME ((alo, ahi), err) /\
FloverMapTree_find (Downcast mEps e) Gamma = SOME mEps /\
abs (nR - nF1) <= err1 ==>
abs (nR - nF) <= err``,
......@@ -2304,11 +2304,13 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
>- (fs[DIFF_DEF, SUBSET_DEF, Once validTypes_def, Once validRanges_def]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ fs[Once validRanges_def] \\ IMP_RES_TAC validRanges_single
\\ fs[Once validRanges_def, Once validTypes_def]
\\ IMP_RES_TAC validRanges_single
\\ IMP_RES_TAC meps_0_deterministic \\ rveq
\\ fs[] \\ rveq \\ fs[]
\\ rename1 `FloverMapTree_find e1 A = SOME (iv1, err1)`
\\ rename1 `FloverMapTree_find e2 A = SOME (iv2, err2)`
\\ IMP_RES_TAC validTypes_exec \\ rveq
\\ rename1 `eval_expr E2 _ e1 nF1 m1`
\\ rename1 `eval_expr E2 _ e2 nF2 m2`
\\ `contained nF1 (widenInterval iv1 err1)`
......@@ -2319,145 +2321,118 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ qexists_tac `m1` \\ fs[])
\\ `contained nF2 (widenInterval iv2 err2)`
by (irule distance_gives_iv
\\ qexists_tac `v2` \\ fs [contained_def, IVlo_def, IVhi_def]
\\ qexists_tac `v2` \\ fs [contained_def]
\\ first_x_assum irule
\\ qexists_tac `m2` \\ fs[])
\\ `op = Div ==> nF2 <> 0`
by (strip_tac
\\ rveq
\\ fs[IVhi_def, IVlo_def, widenInterval_def, contained_def]
\\ fs[widenInterval_def, contained_def]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ fs[noDivzero_def] \\ TRY REAL_ASM_ARITH_TAC
\\ `0 < 0:real` suffices_by (fs[])
\\ TRY (irule REAL_LET_TRANS \\ qexists_tac `SND iv2 + err2`
\\ fs[] \\ FAIL_TAC "")
\\ irule REAL_LTE_TRANS \\ qexists_tac `FST iv2 - err2` \\ fs[])
(* MARKER *)
\\ conj_tac \\ rpt strip_tac
>- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) m 0`, `m`]
>- (qexistsl_tac [`perturb (evalBinop op nF1 nF2) x' 0`, `x'`]
\\ irule Binop_dist'
\\ qexistsl_tac [`0`, `x'`, `m1`, `m2`, `nF1`, `nF2`]
\\ fs[ABS_0, mTypeToR_pos, toRExpMap_def, Once validTypes_def])
\\ rpt strip_tac
\\ fs[ABS_0, mTypeToR_pos, toRExpMap_def])
\\ `m = x'`
by (first_x_assum irule \\ simp[Once validTypes_def]
\\ conj_tac
>- (rpt strip_tac \\ first_x_assum irule
\\ rpt (find_exists_tac \\ fs[]))
\\ find_exists_tac \\ fs[])
\\ rveq
\\ `perturb (evalBinop op nR1 nR2) REAL delta = evalBinop op nR1 nR2`
by (irule delta_0_deterministic \\ fs[mTypeToR_def, join_def])
by (irule delta_0_deterministic \\ fs[mTypeToR_def])
\\ fs[]
\\ qpat_assum `eval_expr E2 _ _ (Binop op e1 e2) _ _` assume_tac
\\ inversion `eval_expr E2 _ _ (Binop op e1 e2) _ _` eval_expr_cases
\\ rename1 `join m1F m2F fBit2 = SOME mF`
\\ qpat_assum `eval_expr E2 _ (Binop op e1 e2) _ _` assume_tac
\\ inversion `eval_expr E2 _ (Binop op e1 e2) _ _` eval_expr_cases
\\ rename1 `abs delta2 <= mTypeToR mF`
\\ rveq
\\ `eval_expr (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
(updDefVars 2 m2F (updDefVars 1 m1F Gamma))
(\e. if e = Binop op (Var 1) (Var 2)
then toRBMap (Binop op e1 e2)
else toRBMap e)
(Binop op (Var 1) (Var 2)) (perturb (evalBinop op v1 v2) mF delta2) mF`
\\ `m2' = m2`
by (irule validTypes_exec
\\ qexistsl_tac [`E2`, `Gamma`, `e2`, `v2'`] \\ fs[])
\\ `m1' = m1`
by (irule validTypes_exec
\\ qexistsl_tac [`E2`, `Gamma`, `e1`, `v1'`] \\ fs[])
\\ rveq
\\ `eval_expr (updEnv 2 v2' (updEnv 1 v1' emptyEnv))
(updDefVars (Binop op (Var 1) (Var 2)) mF
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma))))
(Binop op (Var 1) (Var 2)) (perturb (evalBinop op v1' v2') mF delta2) mF`
by (irule binary_unfolding \\ fs[] \\ rpt conj_tac
>- (find_exists_tac \\ fs[])
\\ find_exists_tac \\ fs[])
\\ rpt (find_exists_tac \\ fs[]))
\\ Cases_on `op` \\ rveq
THENL [irule validErrorboundCorrectAddition,
irule validErrorboundCorrectSubtraction,
irule validErrorboundCorrectMult,
irule validErrorboundCorrectDiv]
\\ fs [GSYM noDivzero_def]
\\ qexistsl_tac [`A`, `E1`, `E2`, `Gamma`, `ehi`, `elo`, `dVars`, `e1`,
`SND iv1`, `FST iv1`, `e2`, `SND iv2`, `FST iv2`, `err1`,
`err2`, `Gamma`, `fBit2`, `fBits`, `mF`, `m1F`,
`m2F`, `v1`, `v2`, `nR1`, `nR2` ]
\\ fs[toREval_def, toRBMap_def]
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`A`, `E1`, `E2`, `ehi`, `elo`, `dVars`, `SND iv1`,
`FST iv1`, `SND iv2`, `FST iv2`, `err1`, `err2`, `m1`,
`m2`, `v1'`, `v2'`, `v1`, `v2`]
\\ fs[toREval_def]
\\ rpt conj_tac \\ TRY (first_x_assum irule \\ asm_exists_tac \\ fs[])
\\ 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`, `fBit`, `REAL`, `REAL`, `nR1`, `nR2`]
\\ fs[perturb_def, mTypeToR_pos, join_def])
>- (rename1 `Fma e1 e2 e3`
\\ TRY (irule Binop_dist'
\\ qexistsl_tac [`0`, `REAL`, `REAL`, `REAL`, `v1`, `v2`]
\\ fs[perturb_def, mTypeToR_pos])
\\ simp[Once validErrorbound_def])
>- (rename1 `Fma e1 e2 e3` \\ fs[]
\\ Flover_compute ``validErrorbound``
\\ Flover_compute ``validIntervalbounds``
\\ Flover_compute ``typeCheck``
\\ rveq \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ _ _ _` eval_expr_cases
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases
\\ `m1 = REAL /\ m2 = REAL /\ m3 = REAL`
by (rpt (conj_tac) \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs[])
by (rpt conj_tac \\ irule toRTMap_eval_REAL \\ find_exists_tac \\ fs[])
\\ rveq
\\ first_x_assum
(fn thm =>
qspecl_then
[`E1`, `E2`, `A`, `v3`, `err3`, `P`, `FST iv3`, `SND iv3`,
`fVars`, `dVars`, `Gamma`, `Gamma`, `fBits`]
destruct thm)
(qspecl_then
[`E1`, `E2`, `A`, `v3`, `err3`, `FST ive3`, `SND ive3`,
`fVars`, `dVars`, `Gamma`]
destruct)
\\ fs[]
>- (fs[DIFF_DEF, SUBSET_DEF]
>- (fs[DIFF_DEF, SUBSET_DEF, Once validTypes_def, Once validRanges_def]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ first_x_assum
(fn thm =>
qspecl_then
[`E1`, `E2`, `A`, `v2`, `err2`, `P`, `FST iv2`, `SND iv2`,
`fVars`, `dVars`, `Gamma`, `Gamma`, `fBits`]
destruct thm)
(qspecl_then
[`E1`, `E2`, `A`, `v2`, `err2`, `FST ive2`, `SND ive2`,
`fVars`, `dVars`, `Gamma`]
destruct)
\\ fs[]
>- (fs[DIFF_DEF, SUBSET_DEF]
>- (fs[DIFF_DEF, SUBSET_DEF, Once validTypes_def, Once validRanges_def]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ first_x_assum
(fn thm =>
qspecl_then
[`E1`, `E2`, `A`, `v1`, `err1`, `P`, `FST iv1`, `SND iv1`,
`fVars`, `dVars`, `Gamma`, `Gamma`, `fBits`]
destruct thm)
(qspecl_then
[`E1`, `E2`, `A`, `v1`, `err1`, `FST ive1`, `SND ive1`,
`fVars`, `dVars`, `Gamma`]
destruct)
\\ fs[]
>- (fs[DIFF_DEF, SUBSET_DEF]
>- (fs[DIFF_DEF, SUBSET_DEF, Once validTypes_def, Once validRanges_def]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ rename1 `eval_expr E2 _ _ e3 nF3 m3`
\\ rename1 `eval_expr E2 _ _ e2 nF2 m2`
\\ rename1 `eval_expr E2 _ _ e1 nF1 m1`
\\ `FloverMapTree_find e1 Gamma = SOME m1`
by (irule typingSoundnessExp \\ metis_tac [])
\\ `FloverMapTree_find e2 Gamma = SOME m2`
by (irule typingSoundnessExp \\ metis_tac [])
\\ `FloverMapTree_find e3 Gamma = SOME m3`
by (irule typingSoundnessExp \\ metis_tac [])
\\ rveq \\ fs[]
\\ `?iv err nR1.
FloverMapTree_find e1 A = SOME (iv, err) /\
eval_expr E1 (toRMap Gamma) (toRBMap) (toREval e1) nR1 REAL /\
FST iv <= nR1 /\ nR1 <= SND iv`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `?iv err nR2.
FloverMapTree_find e2 A = SOME (iv, err) /\
eval_expr E1 (toRMap Gamma) (toRBMap) (toREval e2) nR2 REAL /\
FST iv <= nR2 /\ nR2 <= SND iv`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `?iv err nR3.
FloverMapTree_find e3 A = SOME (iv, err) /\
eval_expr E1 (toRMap Gamma) (toRBMap) (toREval e3) nR3 REAL /\
FST iv <= nR3 /\ nR3 <= SND iv`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ fs [] \\ rveq \\ fs[]
\\ fs[Once validTypes_def, Once validRanges_def]
\\ IMP_RES_TAC validTypes_exec \\ rveq
\\ rename1 `eval_expr E2 _ e3 nF3 m3`
\\ rename1 `eval_expr E2 _ e2 nF2 m2`
\\ rename1 `eval_expr E2 _ e1 nF1 m1`
\\ IMP_RES_TAC validRanges_single
\\ IMP_RES_TAC meps_0_deterministic \\ rveq
\\ rename1 `eval_expr E1 _ (toREval e3) nR3 _`
\\ rename1 `eval_expr E1 _ (toREval e2) nR2 _`
\\ rename1 `eval_expr E1 _ (toREval e1) nR1 _`
\\ fs[] \\ rveq \\ fs[] \\ rpt (qpat_x_assum `T` kall_tac)
\\ rename1 `FloverMapTree_find e1 A = SOME (iv1, err1)`
\\ rename1 `FloverMapTree_find e2 A = SOME (iv2, err2)`
\\ rename1 `FloverMapTree_find e3 A = SOME (iv3, err3)`
\\ `nR1 = v1 /\ nR2 = v2 /\ nR3 = v3` by (metis_tac[meps_0_deterministic])
\\ rveq
\\ `contained nF1 (widenInterval iv1 err1)`
by (irule distance_gives_iv
\\ qexists_tac `nR1` \\ fs[contained_def, IVlo_def, IVhi_def]
\\ qexists_tac `nR1` \\ fs[contained_def]
\\ first_x_assum irule
\\ qexists_tac `m1` \\ fs[])
\\ `contained nF2 (widenInterval iv2 err2)`
......@@ -2470,112 +2445,98 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ qexists_tac `nR3` \\ fs [contained_def, IVlo_def, IVhi_def]
\\ first_x_assum irule
\\ qexists_tac `m3` \\ fs[])
\\ qspecl_then [`e1`, `e2`, `e3`, `m1`, `m2`, `m3`, `Gamma`, `Gamma`, `fBits`]
destruct typingFixedPoint_fma_defined
>- (simp [Once typeCheck_def])
\\ fs[] \\ rename1 `FloverMapTree_find (Fma e1 e2 e3) = SOME fBitF`
\\ `?m. join3 m1 m2 m3 fBitF = SOME m`
by (irule typingFma_join_defined
\\ rpt (find_exists_tac \\ fs[])
\\ qexistsl_tac [`Gamma`]
\\ simp [Once typeCheck_def])
\\ conj_tac
>- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) m 0`, `m`]
>- (qexistsl_tac [`perturb (evalFma nF1 nF2 nF3) x' 0`, `x'`]
\\ irule Fma_dist'
\\ qexistsl_tac [`0`, `fBitF`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`]
\\ fs[mTypeToR_pos, toRBMap_def])
\\ qexistsl_tac [`0`, `x'`, `m1`, `m2`, `m3`, `nF1`, `nF2`, `nF3`]
\\ fs[mTypeToR_pos,toRExpMap_def])
\\ rpt strip_tac
\\ `perturb (evalFma nR1 nR2 nR3) REAL delta = evalFma nR1 nR2 nR3`
by (irule delta_0_deterministic \\ fs[mTypeToR_def, join3_def, join_def])
by (irule delta_0_deterministic \\ fs[mTypeToR_def])
\\ fs[]
\\ qpat_assum `eval_expr E2 _ _ (Fma e1 e2 e3) _ _` assume_tac
\\ inversion `eval_expr E2 _ _ (Fma e1 e2 e3) _ _` eval_expr_cases
\\ rename1 `join3 mF1 mF2 mF3 fBit2 = SOME mF`
\\ qpat_assum `eval_expr E2 _ (Fma e1 e2 e3) _ _` assume_tac
\\ inversion `eval_expr E2 _ (Fma e1 e2 e3) _ _` eval_expr_cases
\\ `m1' = m1`
by (irule validTypes_exec
\\ qexistsl_tac [`E2`, `Gamma`, `e1`, `v1`] \\ fs[])
\\ `m2' = m2`
by (irule validTypes_exec
\\ qexistsl_tac [`E2`, `Gamma`, `e2`, `v2`] \\ fs[])
\\ `m3' = m3`
by (irule validTypes_exec
\\ qexistsl_tac [`E2`, `Gamma`, `e3`, `v3`] \\ fs[])
\\ rveq
\\ rename1 `abs delta2 <= mTypeToR mF`
\\ `mF = x'`
by (irule validTypes_exec
\\ qexistsl_tac [`E2`, `Gamma`, `Fma e1 e2 e3`,
`perturb (evalFma v1 v2 v3) mF delta2`]
\\ simp[Once validTypes_def]
\\ first_x_assum MATCH_ACCEPT_TAC)
\\ rveq
\\ `eval_expr (updEnv 3 v3 (updEnv 2 v2 (updEnv 1 v1 emptyEnv)))
(updDefVars 3 mF3 (updDefVars 2 mF2 (updDefVars 1 mF1 Gamma)))
(\e. if e = Fma (Var 1) (Var 2) (Var 3)
then toRBMap (Fma e1 e2 e3)
else toRBMap e)
(updDefVars (Fma (Var 1) (Var 2) (Var 3)) mF
(updDefVars (Var 3) m3
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma)))))
(Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) mF delta2) mF`
by (irule fma_unfolding \\ conj_tac \\ fs[]
>- (find_exists_tac \\ fs[])
\\ find_exists_tac \\ fs[])
\\ rveq
\\ rpt (find_exists_tac \\ fs[]))
\\ irule validErrorboundCorrectFma
\\ rewrite_tac [CONJ_ASSOC]
\\ rpt (once_rewrite_tac [CONJ_COMM]
\\ asm_exists_tac \\ fs[])
\\ qexistsl_tac [`A`, `E1`, `ehi`, `elo`, `dVars`, `SND iv1`, `FST iv1`,
`SND iv2`, `FST iv2`, `SND iv3`, `FST iv3`, `err1`,
`err2`, `err3`, `Gamma`, `fBit2`, `nR1`, `nR2`, `nR3`]
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`A`, `E1`, `E2`, `ehi`, `elo`, `dVars`, `SND iv1`,
`FST iv1`, `SND iv2`, `FST iv2`, `SND iv3`, `FST iv3`,
`err1`, `err2`, `err3`, `m1`, `m2`, `m3`, `v1`, `v2`,
`v3`, `nR1`, `nR2`, `nR3`]
\\ fs[]
\\ rpt conj_tac \\ TRY (first_x_assum irule \\ asm_exists_tac \\ fs[])
>- (fs[toRBMap_def])
>- (once_rewrite_tac [typeCheck_def] \\ fs[join3_def, join_def])
>- (once_rewrite_tac [validErrorbound_def] \\ fs[])
\\ simp [Once toREval_def]
\\ irule Fma_dist'
\\ qexistsl_tac [`0`, `fBit`, `REAL`, `REAL`, `REAL`, `nR1`, `nR2`, `nR3`]
\\ fs[perturb_def, mTypeToR_pos])
>- (rename1 `Downcast m1 e1`
>- (simp [Once toREval_def]
\\ irule Fma_dist'
\\ qexistsl_tac [`0`, `REAL`, `REAL`, `REAL`, `REAL`, `nR1`, `nR2`, `nR3`]
\\ fs[perturb_def, mTypeToR_pos])
\\ once_rewrite_tac [validErrorbound_def] \\ fs[])
>- (rename1 `Downcast m1 e1` \\ fs[]
\\ Flover_compute ``validErrorbound``
\\ Flover_compute ``typeCheck``
\\ Flover_compute ``validIntervalbounds`` \\ rveq
\\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ _ _ _` eval_expr_cases \\ fs[]
\\ rveq \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ _ _` eval_expr_cases \\ fs[]
\\ first_x_assum
(fn thm =>
qspecl_then
[`E1`, `E2`, `A`, `nR`, `err1`, `P`, `FST iv1`, `SND iv1`,
`fVars`, `dVars`, `Gamma`, `Gamma`, `fBits`]
destruct thm)
(qspecl_then
[`E1`, `E2`, `A`, `nR`, `err1`, `FST ive1`, `SND ive1`,
`fVars`, `dVars`, `Gamma`]
destruct)
\\ fs[]
>- (fs[DIFF_DEF, SUBSET_DEF]
>- (fs[DIFF_DEF, SUBSET_DEF, Once validTypes_def, Once validRanges_def]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `?iv err nR1.
FloverMapTree_find e1 A = SOME (iv, err) /\
eval_expr E1 (toRMap Gamma) (toRBMap) (toREval e1) nR1 REAL /\
FST iv <= nR1 /\ nR1 <= SND iv`
by (irule validIntervalbounds_sound
\\ qexistsl_tac [`P`, `dVars`, `fVars`]
\\ fs [DIFF_DEF, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ once_rewrite_tac [usedVars_def] \\ fs[domain_union])
\\ `nR1 = nR` by (metis_tac[meps_0_deterministic]) \\ rveq
\\ fs[] \\ rveq
\\ fs[Once validRanges_def, Once validTypes_def]
\\ IMP_RES_TAC validTypes_exec \\ rveq
\\ IMP_RES_TAC validRanges_single
\\ IMP_RES_TAC meps_0_deterministic \\ rveq
\\ rename1 `eval_expr E1 _ (toREval e1) nR1 _`
\\ fs[] \\ rveq \\ fs[] \\ rpt (qpat_x_assum `T` kall_tac)
\\ rename1 `FloverMapTree_find e1 A = SOME (iv1, err1)`
\\ `FloverMapTree_find e1 Gamma = SOME m`
by (irule typingSoundnessExp \\ metis_tac [])
\\ fs[] \\ rveq
\\ `contained nF (widenInterval iv1 err1)`
by (irule distance_gives_iv
\\ qexists_tac `nR` \\ fs[contained_def, IVlo_def, IVhi_def]
\\ qexists_tac `nR1` \\ fs[contained_def]
\\ first_x_assum irule
\\ qexists_tac `m` \\ fs[])
\\ conj_tac \\ rpt strip_tac
>- (qexistsl_tac [`perturb nF m1 0`, `m1`]
\\ irule Downcast_dist' \\ fs[]
\\ irule Downcast_dist' \\ fs[toRExpMap_def]
\\ qexistsl_tac [`0`, `m`, `nF`]
\\ fs[mTypeToR_pos, isMorePrecise_morePrecise])
\\ inversion `eval_expr E2 _ (Downcast m1 e1) _ _` eval_expr_cases
\\ rveq
\\ irule validErrorboundCorrectRounding
\\ qpat_x_assum `eval_expr E2 _ _ e1 _ _` kall_tac
\\ inversion `eval_expr E2 _ _ (Downcast m1 e1) _ _` eval_expr_cases
\\ rename1 `eval_expr E2 Gamma (toRBMap) e1 v1 me1`
\\ rveq \\ fs[]
\\ rename1 `FloverMapTree_find (Downcast md e1) Gamma = SOME md`
\\ qexistsl_tac [`A`, `E1`, `E2`, `Gamma`, `dVars`, `e1`, `SND iv1`, `FST iv1`,
`err1`, `Gamma`, `fBits`, `me1`, `md`, `v1`]
\\ fs[isSupersetInterval_def]
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`A`, `E1`, `E2`, `ehi`, `elo`, `dVars`, `SND iv1`,
`FST iv1`, `err1`, `m1'`, `v1`]
\\ fs[]
\\ rpt conj_tac
>- (Cases_on `iv1` \\ fs[]
\\ qpat_x_assum `!x. _` kall_tac \\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (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`]
\\ irule Downcast_dist' \\ fs[updDefVars_def]
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`delta`, `v1`]
\\ fs[]
\\ irule Var_load
\\ fs[updDefVars_def, updEnv_def]));
......@@ -2583,82 +2544,67 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
val validErrorboundCmd_gives_eval = store_thm (
"validErrorboundCmd_gives_eval",
``!(f:real cmd) (A:analysisResult) (E1 E2:env)
(outVars fVars dVars:num_set) (vR elo ehi err:real) (P:precond)
(m:mType) Gamma Gamma.
typeCheckCmd f Gamma Gamma /\
approxEnv E1 Gamma A fVars dVars E2 /\
(outVars fVars dVars:num_set) (vR elo ehi err:real)
(m:mType) Gamma.
validTypesCmd f Gamma /\
approxEnv E1 (toRExpMap 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) (toRBMap) vR REAL /\
bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
validErrorboundCmd f Gamma A dVars /\
validIntervalboundsCmd f A P dVars /\
dVars_range_valid dVars E1 A /\
fVars_P_sound fVars E1 P /\
vars_typed ((domain fVars) UNION (domain dVars)) Gamma /\
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
?vF m.
bstep f E2 Gamma (toRBMap) vF m``,
bstep f E2 (toRExpMap Gamma) vF m``,
Induct_on `f` \\ rpt strip_tac
\\ Flover_compute ``validErrorboundCmd``
\\ Flover_compute ``validIntervalboundsCmd``
\\ Flover_compute ``typeCheckCmd``
\\ rveq \\ fs[Once toREvalCmd_def]
>- (inversion `bstep _ _ _ _ _ _` bstep_cases
>- (inversion `bstep _ _ _ _ _` bstep_cases
\\ inversion `ssa _ _ _` ssa_cases
\\ drule validErrorbound_sound
\\ disch_then drule
\\ disch_then (qspecl_then [`v`, `err_e`, `P`, `FST iv_e`, `SND iv_e`] destruct)
\\ fs[Once validTypesCmd_def, Once validRangesCmd_def, getRetExp_def]
\\ `validRangesCmd f A (updEnv n v E1) (toRTMap (toRExpMap Gamma))`
by (first_x_assum irule \\ fs[])
\\ IMP_RES_TAC validRangesCmd_single
\\ fs[] \\ rveq \\ fs[]
\\ qspecl_then
[`e`, `E1`, `E2`, `A`, `v`, `err_e`, `FST iv_e`, `SND iv_e`, `fVars`,
`dVars`, `Gamma`] destruct validErrorbound_sound
\\ fs[]
>- (rw_thm_asm `domain (freeVars _) DIFF _ SUBSET _` freeVars_def
\\ fs[]
\\ fs[SUBSET_DEF, domain_union]
\\ rpt strip_tac \\ first_x_assum irule \\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[]))
\\ rename1 `eval_expr E2 Gamma (toRBMap) e vF mF`
\\ `approxEnv (updEnv n v E1) (updDefVars n m Gamma) A fVars
\\ rename1 `eval_expr E2 (toRExpMap Gamma) e vF mF`
\\ `approxEnv (updEnv n v E1) (toRExpMap Gamma) A fVars
(insert n () dVars) (updEnv n vF E2)`
by (irule approxUpdBound \\ fs[lookup_NONE_domain]
\\ first_x_assum irule \\ qexists_tac `mF` \\ fs[])
\\ `FloverMapTree_find e Gamma = SOME mF`
by (irule typingSoundnessExp
\\ qexistsl_tac [`E2`, `Gamma`, `fBits`, `vF`] \\ fs[])
\\ conj_tac
>- (qexists_tac `m` \\ fs[toRExpMap_def])
\\ first_x_assum irule \\ find_exists_tac \\ fs[])
\\ `m = mF`
by (irule (GSYM validTypes_exec)
\\ qexistsl_tac [`E2`, `Gamma`, `e`, `vF`] \\ fs[])
\\ fs[] \\ rveq \\ fs[]
\\ `?vF_res m_res. bstep f (updEnv n vF E2) (updDefVars n m Gamma) (toRBMap) vF_res m_res`
\\ `?vF_res m_res.
bstep f (updEnv n vF E2) (toRExpMap Gamma) vF_res m_res`
by (first_x_assum irule
\\ qexistsl_tac [`A`, `updEnv n v E1`, `P`,
`insert n () dVars`, `ehi`, `elo`, `err`,
`Gamma`, `fVars`, `outVars`, `vR`]
\\ rpt conj_tac
>- (fs[getRetExp_def] \\ res_tac
\\ IMP_RES_TAC validTypesCmd_single
\\ fs[] \\ rveq \\ fs[])
>- (fs[Once validTypesCmd_def])
\\ qexistsl_tac [`A`, `updEnv n v E1`, `insert n () dVars`,
`ehi`, `elo`, `err`, `fVars`, `outVars`, `vR''`]
\\ fs[getRetExp_def]
\\ rpt conj_tac
>- (find_exists_tac \\ fs[])
>- (fs[Once validRangesCmd_def])
>- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule
\\ fs[Once freeVars_def]
\\ simp[Once freeVars_def, domain_union])
>- (fs [vars_typed_def]
\\ rpt strip_tac \\ fs[]
\\ TOP_CASE_TAC \\ first_x_assum irule \\ fs[])
>- (drule validIntervalbounds_sound
\\ disch_then (qspecl_then [`fVars`, `E1`, `Gamma`, `toRBMap`] destruct)
>- (fs[Once freeVars_def, domain_union, DIFF_DEF,
dVars_range_valid_def, SUBSET_DEF]
\\ rpt strip_tac \\ first_x_assum irule \\ fs[]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ fs[SUBSET_DEF, domain_union]
\\ `n IN domain fVars \/ n IN domain dVars` by (first_x_assum irule \\ fs[]))
\\ rename1 `eval_expr E1 _ _ (toREval e) vR2 REAL`
\\ `v = vR2` by (metis_tac[meps_0_deterministic])
\\ rveq
\\ fs [dVars_range_valid_def]
\\ rpt strip_tac \\ fs[] \\ rveq \\ fs[]
\\ rename1 `FloverMapTree_find e A = SOME (iv_e , err_e)`
\\ IF_CASES_TAC \\ rveq
>- (qexistsl_tac [`v`, `iv_e`, `err_e`] \\ fs[])
\\ first_x_assum irule \\ fs[])
>- (fs [fVars_P_sound_def]
\\ rpt strip_tac
\\ IF_CASES_TAC \\ fs[]
\\ rveq
\\ fs[domain_union])
>- (irule ssa_equal_set
\\ qexists_tac `insert n () (union fVars dVars)`
\\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
......@@ -2667,121 +2613,79 @@ val validErrorboundCmd_gives_eval = store_thm (
\\ fs[EXTENSION]
\\ rpt strip_tac
\\ metis_tac[])
>- (irule swap_Gamma_bstep
\\ 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
\\ fs[]))
\\ fs[Once toREvalCmd_def])
\\ qexistsl_tac [`vF_res`, `m_res`]
\\ fs[bstep_cases]
\\ qexists_tac `vF` \\ rveq \\ fs[])
>- (fs[getRetExp_def]
\\ inversion `ssa _ _ _` ssa_cases
\\ inversion `bstep _ _ _ _ _ _` bstep_cases
\\ inversion `bstep _ _ _ _ _` bstep_cases
\\ once_rewrite_tac [bstep_cases]
\\ `(?vF m. eval_expr E2 Gamma (toRBMap) e vF m) /\
(!vF m. eval_expr E2 Gamma (toRBMap) e vF m ==> abs (vR - vF) <= err)`
by (irule validErrorbound_sound
\\ qexistsl_tac [`A`, `E1`, `P`, `dVars`, `ehi`, `elo`, `Gamma`, `fVars`]
\\ fs[typeCheckCmd_def, freeVars_def])
\\ `(?vF m. eval_expr E2 (toRExpMap Gamma