Commit 2dea97d6 authored by Heiko Becker's avatar Heiko Becker

Port ErrorBoundsScript to new semantics

parent 2e3a7e7e
......@@ -4,8 +4,8 @@ This shortens soundness proofs later.
Bounds are exprlained in section 5, Deriving Computable Error Bounds
**)
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics
MachineTypeTheory ExpressionAbbrevsTheory EnvironmentsTheory;
open AbbrevsTheory ExpressionsTheory ExpressionSemanticsTheory RealSimpsTheory
FloverTactics MachineTypeTheory ExpressionAbbrevsTheory EnvironmentsTheory;
open preamble
val _ = new_theory "ErrorBounds";
......@@ -26,10 +26,9 @@ 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) fBits.
eval_expr E1 (toRMap defVars) fBits (Const REAL n) nR REAL /\
eval_expr E2 defVars fBits (Const m n) nF m ==>
``!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) Gamma.
eval_expr E1 (toRTMap Gamma) (Const REAL n) nR REAL /\
eval_expr E2 Gamma (Const m n) nF m ==>
abs (nR - nF) <= computeError n m``,
rpt strip_tac
\\ fs[eval_expr_cases]
......@@ -58,35 +57,34 @@ val float_add_tac =
val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
``!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
(err1:real) (err2:real) (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType)
(defVars: num -> mType option) fBits.
eval_expr E1 (toRMap defVars) fBits (toREval e1) e1R REAL /\
eval_expr E2 defVars fBits e1 e1F m1 /\
eval_expr E1 (toRMap defVars) fBits (toREval e2) e2R REAL /\
eval_expr E2 defVars fBits e2 e2F m2 /\
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Plus e1 e2)) vR REAL /\
(Gamma: real expr -> mType option).
eval_expr E1 (toRTMap Gamma) (toREval e1) e1R REAL /\
eval_expr E2 Gamma e1 e1F m1 /\
eval_expr E1 (toRTMap Gamma) (toREval e2) e2R REAL /\
eval_expr E2 Gamma e2 e2F m2 /\
eval_expr E1 (toRTMap Gamma) (toREval (Binop Plus e1 e2)) vR REAL /\
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(\e. if e = Binop Plus (Var 1) (Var 2)
then fBits (Binop Plus e1 e2)
else fBits e)
(updDefVars (Binop Plus (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 Gamma)))
(Binop Plus (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (computeError (e1F + e2F) m)``,
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ (Binop Plus _ _) _ _` eval_expr_cases
\\ inversion `eval_expr E1 _ (Binop Plus _ _) _ _` eval_expr_cases
\\ rename1 `vR = perturb (evalBinop Plus v1R v2R) REAL deltaR`
\\ rename1 `join m1R m2R fBit = SOME REAL`
\\ inversion `eval_expr _ _ _ (Binop Plus (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `isJoin m1R m2R REAL`
\\ inversion `eval_expr _ _ (Binop Plus (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `vF = perturb (evalBinop Plus v1F v2F) mF 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]
by (conj_tac \\ irule toRTMap_eval_REAL \\ qexistsl_tac [`E1`, `Gamma`]
THENL [qexistsl_tac [`e1`, `v1R`], qexistsl_tac [`e2`, `v2R`]]
\\ fs[])
\\ `v1R = e1R` by metis_tac [meps_0_deterministic]
\\ `v2R = e2R` by metis_tac [meps_0_deterministic]
\\ rveq
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _ _` eval_expr_cases)
\\ rveq \\ fs [perturb_def]
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _`
eval_expr_cases)
\\ fs [updEnv_def] \\ rveq
\\ once_rewrite_tac[real_sub]
\\ Cases_on `mF` \\ fs[perturb_def, evalBinop_def]
......@@ -131,39 +129,37 @@ val float_sub_tac =
val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
``!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
(err1:real) (err2:real) (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType)
(defVars: num -> mType option) fBits.
eval_expr E1 (toRMap defVars) fBits (toREval e1) e1R REAL /\
eval_expr E2 defVars fBits e1 e1F m1 /\
eval_expr E1 (toRMap defVars) fBits (toREval e2) e2R REAL /\
eval_expr E2 defVars fBits e2 e2F m2 /\
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Sub e1 e2)) vR REAL /\
(Gamma: real expr -> mType option).
eval_expr E1 (toRTMap Gamma) (toREval e1) e1R REAL /\
eval_expr E2 Gamma e1 e1F m1 /\
eval_expr E1 (toRTMap Gamma) (toREval e2) e2R REAL /\
eval_expr E2 Gamma e2 e2F m2 /\
eval_expr E1 (toRTMap Gamma) (toREval (Binop Sub e1 e2)) vR REAL /\
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(\e. if e = Binop Sub (Var 1) (Var 2)
then fBits (Binop Sub e1 e2)
else fBits e)
(updDefVars (Binop Sub (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 Gamma)))
(Binop Sub (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + computeError (e1F - e2F) m``,
rpt strip_tac
\\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ (Binop Sub _ _) _ _` eval_expr_cases
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ (Binop Sub _ _) _ _` eval_expr_cases
\\ rename1 `vR = perturb (evalBinop Sub v1R v2R) REAL deltaR`
\\ rename1 `join m1R m2R fBit = SOME REAL`
\\ inversion `eval_expr _ _ _ (Binop Sub (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `isJoin m1R m2R REAL`
\\ inversion `eval_expr _ _ (Binop Sub (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `vF = perturb (evalBinop Sub v1F v2F) mF deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL)`
by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[])
\\ rveq
by (conj_tac \\ irule toRTMap_eval_REAL \\ qexistsl_tac [`E1`, `Gamma`]
THENL [qexistsl_tac [`e1`, `v1R`], qexistsl_tac [`e2`, `v2R`]]
\\ fs[])
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ rveq
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _ _`
\\ rveq \\ fs[perturb_def]
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _`
eval_expr_cases)
\\ fs [updEnv_def] \\ rveq
\\ Cases_on `mF`
\\ fs[perturb_def, join_def, evalBinop_def, computeError_def]
\\ fs[perturb_def, evalBinop_def, computeError_def]
\\ rewrite_tac[real_sub]
>- (`e1R - e2R + - (e1F - e2F) = e1R + - e1F + (- e2R + e2F)`
by REAL_ASM_ARITH_TAC
......@@ -203,40 +199,37 @@ val float_mul_tac =
val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
``!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
(err1:real) (err2:real) (vR:real) (vF:real) (E1 E2 :env) (m m1 m2:mType)
(defVars: num -> mType option) fBits.
eval_expr E1 (toRMap defVars) fBits (toREval e1) e1R REAL /\
eval_expr E2 defVars fBits e1 e1F m1 /\
eval_expr E1 (toRMap defVars) fBits (toREval e2) e2R REAL /\
eval_expr E2 defVars fBits e2 e2F m2 /\
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Mult e1 e2)) vR REAL /\
(Gamma: real expr -> mType option).
eval_expr E1 (toRTMap Gamma) (toREval e1) e1R REAL /\
eval_expr E2 Gamma e1 e1F m1 /\
eval_expr E1 (toRTMap Gamma) (toREval e2) e2R REAL /\
eval_expr E2 Gamma e2 e2F m2 /\
eval_expr E1 (toRTMap Gamma) (toREval (Binop Mult e1 e2)) vR REAL /\
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(\e. if e = Binop Mult (Var 1) (Var 2)
then fBits (Binop Mult e1 e2)
else fBits e)
(updDefVars (Binop Mult (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 Gamma)))
(Binop Mult (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + computeError (e1F * e2F) m``,
rpt strip_tac
\\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ (Binop Mult _ _) _ _` eval_expr_cases
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ (Binop Mult _ _) _ _` eval_expr_cases
\\ rename1 `vR = perturb (evalBinop Mult v1R v2R) REAL deltaR`
\\ rename1 `join m1R m2R fBit = SOME REAL`
\\ inversion `eval_expr _ _ _ (Binop Mult (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `isJoin m1R m2R REAL`
\\ inversion `eval_expr _ _ (Binop Mult (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `vF = perturb (evalBinop Mult v1F v2F) mF deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL)`
by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[])
\\ rveq
\\ fs[perturb_def, evalBinop_def]
by (conj_tac \\ irule toRTMap_eval_REAL \\ qexistsl_tac [`E1`, `Gamma`]
THENL [qexistsl_tac [`e1`, `v1R`], qexistsl_tac [`e2`, `v2R`]]
\\ fs[])
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ rveq
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _ _`
\\ rveq \\ fs[perturb_def, evalBinop_def]
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _`
eval_expr_cases)
\\ fs [updEnv_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ Cases_on `mF` \\ fs[join_def, perturb_def]
\\ Cases_on `mF` \\ fs[perturb_def]
>- (rewrite_tac [REAL_LE_ADDR] \\ fs[computeError_def])
>- (float_mul_tac)
>- (float_mul_tac)
......@@ -264,39 +257,37 @@ val float_div_tac =
val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
``!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
(err1:real) (err2:real) (vR:real) (vF:real) (E1 E2 :env) (m m1 m2:mType)
(defVars: num -> mType option) fBits.
eval_expr E1 (toRMap defVars) fBits (toREval e1) e1R REAL /\
eval_expr E2 defVars fBits e1 e1F m1 /\
eval_expr E1 (toRMap defVars) fBits (toREval e2) e2R REAL /\
eval_expr E2 defVars fBits e2 e2F m2 /\
eval_expr E1 (toRMap defVars) fBits (toREval (Binop Div e1 e2)) vR REAL /\
(Gamma: real expr -> mType option).
eval_expr E1 (toRTMap Gamma) (toREval e1) e1R REAL /\
eval_expr E2 Gamma e1 e1F m1 /\
eval_expr E1 (toRTMap Gamma) (toREval e2) e2R REAL /\
eval_expr E2 Gamma e2 e2F m2 /\
eval_expr E1 (toRTMap Gamma) (toREval (Binop Div e1 e2)) vR REAL /\
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(\e. if e = Binop Div (Var 1) (Var 2)
then fBits (Binop Div e1 e2)
else fBits e)
(updDefVars (Binop Div (Var 1) (Var 2)) m
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 Gamma)))
(Binop Div (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + computeError (e1F / e2F) m``,
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ (Binop Div _ _) _ _` eval_expr_cases
\\ inversion `eval_expr E1 _ (Binop Div _ _) _ _` eval_expr_cases
\\ rename1 `vR = perturb (evalBinop Div v1R v2R) REAL deltaR`
\\ rename1 `join m1R m2R fBit = SOME REAL`
\\ inversion `eval_expr _ _ _ (Binop Div (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `isJoin m1R m2R REAL`
\\ inversion `eval_expr _ _ (Binop Div (Var 1) (Var 2)) _ _` eval_expr_cases
\\ rename1 `vF = perturb (evalBinop Div v1F v2F) mF deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL)`
by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[])
\\ rveq
\\ fs[perturb_def, evalBinop_def]
by (conj_tac \\ irule toRTMap_eval_REAL \\ qexistsl_tac [`E1`, `Gamma`]
THENL [qexistsl_tac [`e1`, `v1R`], qexistsl_tac [`e2`, `v2R`]]
\\ fs[])
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ rveq
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _ _`
\\ rveq \\ fs[perturb_def, evalBinop_def]
\\ rpt (inversion `eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _`
eval_expr_cases)
\\ fs [updEnv_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ Cases_on `mF` \\ fs[join_def, perturb_def]
\\ Cases_on `mF` \\ fs[perturb_def]
>- (rewrite_tac [REAL_LE_ADDR] \\ fs[computeError_def])
>- (float_div_tac)
>- (float_div_tac)
......@@ -325,19 +316,18 @@ val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded",
``!(e1:real expr) (e1R:real) (e1F:real) (e2:real expr) (e2R:real) (e2F:real)
(e3:real expr) (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) fBits.
eval_expr E1 (toRMap defVars) fBits (toREval e1) e1R REAL /\
eval_expr E2 defVars fBits e1 e1F m1 /\
eval_expr E1 (toRMap defVars) fBits (toREval e2) e2R REAL /\
eval_expr E2 defVars fBits e2 e2F m2 /\
eval_expr E1 (toRMap defVars) fBits (toREval e3) e3R REAL /\
eval_expr E2 defVars fBits e3 e3F m3 /\
eval_expr E1 (toRMap defVars) fBits (toREval (Fma e1 e2 e3)) vR REAL /\
(Gamma: real expr -> mType option).
eval_expr E1 (toRTMap Gamma) (toREval e1) e1R REAL /\
eval_expr E2 Gamma e1 e1F m1 /\
eval_expr E1 (toRTMap Gamma) (toREval e2) e2R REAL /\
eval_expr E2 Gamma e2 e2F m2 /\
eval_expr E1 (toRTMap Gamma) (toREval e3) e3R REAL /\
eval_expr E2 Gamma e3 e3F m3 /\
eval_expr E1 (toRTMap Gamma) (toREval (Fma e1 e2 e3)) vR REAL /\
eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(\e. if e = Fma (Var 1) (Var 2) (Var 3)
then fBits (Fma e1 e2 e3)
else fBits e)
(updDefVars (Fma (Var 1) (Var 2) (Var 3)) m
(updDefVars (Var 3) m3
(updDefVars (Var 2) m2 (updDefVars (Var 1) m1 Gamma))))
(Fma (Var 1) (Var 2) (Var 3)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 /\
......@@ -346,25 +336,27 @@ val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded",
abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) +
computeError (e1F + e2F * e3F) m``,
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ _ (Fma _ _ _) _ _` eval_expr_cases
\\ inversion `eval_expr E1 _ (Fma _ _ _) _ _` eval_expr_cases
\\ rename1 `vR = perturb (evalFma v1R v2R v3R) REAL deltaR`
\\ rename1 `join3 m1R m2R m3R fBit = SOME REAL`
\\ inversion `eval_expr _ _ _ (Fma (Var 1) (Var 2) (Var 3)) _ _` eval_expr_cases
\\ rename1 `isJoin3 m1R m2R m3R REAL`
\\ inversion `eval_expr _ _ (Fma (Var 1) (Var 2) (Var 3)) _ _` eval_expr_cases
\\ rename1 `vF = perturb (evalFma v1F v2F v3F) mF 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]
by (rpt conj_tac \\ irule toRTMap_eval_REAL \\ qexistsl_tac [`E1`, `Gamma`]
THENL [qexistsl_tac [`e1`, `v1R`],
qexistsl_tac [`e2`, `v2R`],
qexistsl_tac [`e3`, `v3R`]]
\\ fs[])
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ `v3R = e3R` by metis_tac[meps_0_deterministic]
\\ rveq
\\ rveq \\ fs[evalFma_def, evalBinop_def]
\\ rpt (inversion `eval_expr
(updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) _ _ _ _ _`
(updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) _ _ _ _`
eval_expr_cases)
\\ fs [updEnv_def] \\ rveq
\\ Cases_on `mF`
\\ fs[computeError_def, join3_def, join_def, perturb_def]
\\ fs[computeError_def, perturb_def]
\\ rewrite_tac[real_sub]
>- (`e1R + e2R * e3R + - (e1F + e2F * e3F) =
e1R + - e1F + (e2R * e3R + - (e2F * e3F))`
......@@ -383,14 +375,13 @@ val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded",
val round_abs_err_bounded = store_thm ("round_abs_err_bounded",
``!(e:real expr) (nR:real) (nF1:real) (nF:real) (E1:env) (E2:env) (err:real)
(m1:mType) (m:mType) (defVars: num -> mType option) fBits.
eval_expr E1 (toRMap defVars) fBits (toREval e) nR REAL /\
eval_expr E2 defVars fBits e nF1 m /\
eval_expr (updEnv 1 nF1 emptyEnv) (updDefVars 1 m defVars)
(\e. if e = Downcast m1 (Var 1)
then fBits (Downcast m1 e)
else fBits e)
(Downcast m1 (Var 1)) nF m1 /\
(m1:mType) (m:mType) (Gamma: real expr -> mType option).
eval_expr E1 (toRTMap Gamma) (toREval e) nR REAL /\
eval_expr E2 Gamma e nF1 m /\
eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars (Downcast m1 (Var 1)) m1
(updDefVars (Var 1) m Gamma))
(Downcast m1 (Var 1)) nF m1 /\
abs (nR - nF1) <= err ==>
abs (nR - nF) <= err + computeError nF1 m1``,
rpt strip_tac
......@@ -398,8 +389,8 @@ val round_abs_err_bounded = store_thm ("round_abs_err_bounded",
\\ fs []
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ fs[]
\\ inversion `eval_expr (updEnv _ _ _) _ _ _ _ _` eval_expr_cases
\\ inversion `eval_expr (updEnv _ _ _) _ _ _ _ _` eval_expr_cases
\\ inversion `eval_expr (updEnv _ _ _) _ _ _ _` eval_expr_cases
\\ inversion `eval_expr (updEnv _ _ _) _ _ _ _` eval_expr_cases
\\ fs [updEnv_def] \\ rveq \\ fs[]
\\ Cases_on `m1` \\ fs[perturb_def, computeError_def]
\\ once_rewrite_tac [REAL_LDISTRIB]
......
......@@ -18,7 +18,8 @@ val _ = type_abbrev ("typeMap", ``:mType fMap``);
val _ = type_abbrev ("analysisResult", ``:((real # real) # real) fMap``);
val updDefVars_def = Define `
updDefVars (x:real expr) (m:mType) (defVars:real expr -> mType option) (y:real expr) :mType option =
updDefVars (x:real expr) (m:mType) (defVars:real expr -> mType option)
(y:real expr) :mType option =
if y = x then SOME m else defVars y`;
val toRExpMap_def = Define `
......@@ -26,7 +27,7 @@ val toRExpMap_def = Define `
\e. FloverMapTree_find e tMap`;
val toRTMap_def = Define `
toRTMap Gamma (Var v) =
toRTMap (Gamma: real expr -> mType option) (Var v) =
(case Gamma (Var v) of
|SOME m => SOME REAL
|_ => NONE) /\
......
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