Commit 665b39ac authored by Heiko Becker's avatar Heiko Becker

Fix proofs in transScript.sml

parent 57aed088
......@@ -36,4 +36,6 @@ val emptyEnv_def = Define `
val updEnv_def = Define `
updEnv (x:num) (v:real) (E:env) (y:num) :real option = if y = x then SOME v else E y`;
val - = export_theory();
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val _ = export_theory();
......@@ -61,8 +61,6 @@ val validErrorboundCmd_def = Define `
| Ret e =>
validErrorbound e env dVars`;
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val err_always_positive = store_thm ("err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars.
(validErrorbound (e:real exp) (absenv:analysisResult) dVars) /\
......
......@@ -434,13 +434,4 @@ val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates
>- (cheat) *)
);
val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv",
``!(f:real cmd) (absenv:analysisResult) (P:precond) (dVars:num_set).
(!v. v IN domain dVars ==>
valid (FST (absenv (Var v)))) /\
validIntervalboundsCmd f absenv P dVars ==>
valid (FST (absenv f))``,
cheat
);
val _ = export_theory();
......@@ -143,8 +143,10 @@ val precond_validErrorbound_true = prove (``
\\ rpt (disch_then ASSUME_TAC)
\\ rveq
\\ rename1 `absenv (Binop Div e1 e2) = (ivDiv, errDiv)`
\\ rename1 `absenv e1 = (ive1,err1)` \\ Cases_on `ive1` \\ rename1 `absenv e1 = ((e1lo,e1hi), err1)`
\\ rename1 `absenv e2 = (ive2,err2)` \\ Cases_on `ive2` \\ rename1 `absenv e2 = ((e2lo,e2hi), err2)`
\\ rename1 `absenv e1 = (ive1,err1)`
\\ Cases_on `ive1` \\ rename1 `absenv e1 = ((e1lo,e1hi), err1)`
\\ rename1 `absenv e2 = (ive2,err2)`
\\ Cases_on `ive2` \\ rename1 `absenv e2 = ((e2lo,e2hi), err2)`
\\ rewrite_tac [divideinterval_side_def, widenInterval_def, minAbsFun_def, invertinterval_side_def, IVlo_def, IVhi_def]
\\ `valid (FST(absenv e1)) /\ valid (FST(absenv e2))`
by (conj_tac \\ drule validIntervalbounds_validates_iv
......@@ -153,7 +155,7 @@ val precond_validErrorbound_true = prove (``
\\ fs [Once validIntervalbounds_def])
>- (disch_then match_mp_tac
\\ qexists_tac `P`
\\ fs [Once validIntervalbounds_def])
\\ fs [Once validIntervalbounds_def]))
\\ rw_asm `absenv e1 = _`
\\ rw_asm `absenv e2 = _`
\\ qpat_x_assum `!v. _` kall_tac
......@@ -161,13 +163,21 @@ val precond_validErrorbound_true = prove (``
by (drule err_always_positive
\\ disch_then (fn thm => qspecl_then [`e2lo,e2hi`, `err2`] match_mp_tac thm)
\\ fs [])
\\ `e2lo - err2 0 /\ e2hi + err2 0` by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def] \\ conj_tac \\ TRY REAL_ASM_ARITH_TAC)
\\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))` by (drule validIntervalbounds_noDivzero_real
\\ fs [])
\\ `abs (e2lo - err2) 0 /\ abs (e2hi + err2) 0` by (conj_tac \\ REAL_ASM_ARITH_TAC)
\\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) 0` by (fs [min_def] \\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)` \\ fs [] \\ TRY REAL_ASM_ARITH_TAC)
\\ `e2lo - err2 0 /\ e2hi + err2 0`
by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
\\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))`
by (drule validIntervalbounds_noDivzero_real
\\ fs [])
\\ `abs (e2lo - err2) 0 /\ abs (e2hi + err2) 0`
by (REAL_ASM_ARITH_TAC)
\\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) 0`
by (fs [min_def]
\\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)`
\\ fs [] \\ REAL_ASM_ARITH_TAC)
\\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
\\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def] \\ REAL_ASM_ARITH_TAC));
\\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
\\ REAL_ASM_ARITH_TAC));
val precond_errorbounds_true = prove (``
!P f absenv dVars.
......
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