Commit 139aea84 authored by Heiko Becker's avatar Heiko Becker
Browse files

Minor modification to iv validation and translation file

parent 20c18685
......@@ -29,40 +29,38 @@ val validIntervalbounds_def = Define `
| Param v => isSupersetInterval (P v) intv
| Const n => isSupersetInterval (n,n) intv
| Unop op f =>
let rec = validIntervalbounds f absenv P validVars in
(let rec = validIntervalbounds f absenv P validVars in
let (iv, _) = absenv f in
let opres =
case op of
| Neg =>
let new_iv = negateInterval iv in
isSupersetInterval new_iv intv
| Inv =>
let nodiv0 = (IVhi iv < 0 \/ 0 < IVlo iv) in
let new_iv = invertInterval iv in
isSupersetInterval new_iv intv /\ nodiv0
in
rec /\ opres
case op of
| Neg =>
(let new_iv = negateInterval iv in
(isSupersetInterval new_iv intv /\ rec))
| Inv =>
(if (IVhi iv < 0 \/ 0 < IVlo iv)
then
let new_iv = invertInterval iv in
(isSupersetInterval new_iv intv /\ rec)
else F))
| Binop op f1 f2 =>
let rec = (validIntervalbounds f1 absenv P validVars /\ validIntervalbounds f2 absenv P validVars) in
let (iv1, _ ) = absenv f1 in
let (iv2, _) = absenv f2 in
let opres =
case op of
| Plus =>
let new_iv = addInterval iv1 iv2 in
isSupersetInterval new_iv intv
isSupersetInterval new_iv intv /\ rec
| Sub =>
let new_iv = subtractInterval iv1 iv2 in
isSupersetInterval new_iv intv
isSupersetInterval new_iv intv /\ rec
| Mult =>
let new_iv = multInterval iv1 iv2 in
isSupersetInterval new_iv intv
isSupersetInterval new_iv intv /\ rec
| Div =>
let nodiv0 = (IVhi iv2 < 0 \/ 0 < IVlo iv2) in
if (IVhi iv2 < 0 \/ 0 < IVlo iv2)
then
let new_iv = divideInterval iv1 iv2 in
isSupersetInterval new_iv intv /\ nodiv0
in
rec /\ opres `;
(isSupersetInterval new_iv intv /\ rec)
else F`;
val validIntervalboundsCmd_def = Define `
validIntervalboundsCmd (f:real cmd) (absenv:analysisResult) (P:precond) (validVars:num set) =
......@@ -163,68 +161,73 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
Cases_on `absenv f` \\
qmatch_assum_rename_tac `absenv f = (iv_f, err_f)` \\
fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, negateInterval_def] \\
rveq \\
fs [] \\
`FST iv_f <= v1 /\ v1 <= SND iv_f` by metis_tac []\\
qpat_x_assum `! _. Q ==> R` kall_tac \\
Cases_on `u`
>- (fs[] \\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `- SND iv_f` \\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (qexists_tac `- FST iv_f` \\ conj_tac \\ REAL_ASM_ARITH_TAC))
>- (CCONTR_TAC \\ fs[]))
fs[] \\ conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `- SND iv_f` \\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (qexists_tac `- FST iv_f` \\ conj_tac \\ REAL_ASM_ARITH_TAC))
(* Inversion case *)
>- (simp[evalUnop_def] \\
>- (rveq \\ simp[evalUnop_def] \\
`perturb (evalUnop Inv v1) delta = evalUnop Inv v1`
by (qspecl_then [`evalUnop Inv v1`, `delta`] match_mp_tac delta_0_deterministic \\ fs[]) \\
`perturb (inv v1) delta = inv v1` by (fs[evalUnop_def]) \\
simp[] \\
qpat_x_assum `validIntervalbounds a b c d`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm)) \\
qpat_x_assum `!absenv P V VarEnv ParamEnv vR. validIntervalbounds f absenv P V /\ Q /\ eval_exp 0 VarEnv ParamEnv P f vR ==> R`
(fn thm => qspecl_then [`absenv`,`P`, `V`, `VarEnv`, `ParamEnv`, `v1`] ASSUME_TAC thm) \\
Cases_on `absenv (Unop u f)` \\
qmatch_assum_rename_tac `absenv (Unop u f) = (iv_u, err_u)` \\
Cases_on `absenv (Unop Inv f)` \\
qmatch_assum_rename_tac `absenv (Unop Inv f) = (iv_u, err_u)` \\
Cases_on `absenv f` \\
qmatch_assum_rename_tac `absenv f = (iv_f, err_f)` \\
`absenv (Unop Inv f) = (iv_u,err_u)` by metis_tac [] \\
fs[evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER] \\
full_simp_tac std_ss [METIS_PROVE [] ``(b \/ c) <=> (~b ==> c)``] \\
fs [evalUnop_def, isSupersetInterval_def, IVlo_def, IVhi_def, invertInterval_def, GSYM REAL_INV_1OVER] \\
`FST iv_f <= v1 /\ v1 <= SND iv_f` by metis_tac [] \\
qpat_x_assum `!v. _ ==> _` kall_tac \\
Cases_on `u`
>- (CCONTR_TAC \\ fs[])
>- (conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `inv (SND iv_f)` \\ conj_tac \\ TRY(fs[])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC \\
`0 < -v1` by REAL_ASM_ARITH_TAC \\
`-SND iv_f <= -v1` by REAL_ASM_ARITH_TAC \\
`inv (-v1) <= inv (- SND iv_f)` by fs[REAL_INV_LE_ANTIMONO]\\
`inv(-v1) = - (inv v1)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`inv(-(SND iv_f)) = - (inv (SND iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`-(inv v1) <= - (inv (SND iv_f))` by fs [] \\
fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < SND iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))
>- (qexists_tac `inv (FST iv_f)` \\ conj_tac \\ TRY (fs[])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC \\
`0 < -v1` by REAL_ASM_ARITH_TAC \\
`0 < - (FST iv_f)` by REAL_ASM_ARITH_TAC \\
`- v1 <= - (FST iv_f)` by REAL_ASM_ARITH_TAC \\
`inv (- FST iv_f) <= inv (- v1)` by fs[REAL_INV_LE_ANTIMONO]\\
`inv(- FST iv_f) = - (inv (FST iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`inv(- v1) = - (inv v1)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`-(inv (FST iv_f)) <= - (inv v1)` by fs [] \\
fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < FST iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))))
qpat_x_assum `(~ A) ==> B`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [GSYM (METIS_PROVE [] ``(b \/ c) <=> (~b ==> c)``)] thm)) \\
conj_tac \\ match_mp_tac REAL_LE_TRANS
>- (qexists_tac `inv (SND iv_f)` \\ conj_tac \\ TRY(fs[])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC \\
`0 < -v1` by REAL_ASM_ARITH_TAC \\
`-SND iv_f <= -v1` by REAL_ASM_ARITH_TAC \\
`inv (-v1) <= inv (- SND iv_f)` by fs[REAL_INV_LE_ANTIMONO]\\
`inv(-v1) = - (inv v1)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`inv(-(SND iv_f)) = - (inv (SND iv_f))` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`-(inv v1) <= - (inv (SND iv_f))` by fs [] \\
fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < SND iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO]))
>- (qexists_tac `inv (FST iv_f)` \\ conj_tac \\ TRY (fs[])
>- (`0 < - SND iv_f` by REAL_ASM_ARITH_TAC \\
`0 < -v1` by REAL_ASM_ARITH_TAC \\
`0 < - (FST iv_f)` by REAL_ASM_ARITH_TAC \\
`- v1 <= - (FST iv_f)` by REAL_ASM_ARITH_TAC \\
`inv (- FST iv_f) <= inv (- v1)` by fs[REAL_INV_LE_ANTIMONO]\\
`inv(- FST iv_f) = - (inv (FST iv_f))`
by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`inv(- v1) = - (inv v1)`
by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`-(inv (FST iv_f)) <= - (inv v1)` by fs [] \\
fs[])
>- (`0 < v1` by REAL_ASM_ARITH_TAC \\
`0 < FST iv_f` by REAL_ASM_ARITH_TAC \\
fs[REAL_INV_LE_ANTIMONO])))
(* Binary operator case *)
>- (`perturb (evalBinop b v1 v2) delta = evalBinop b v1 v2`
by (qspecl_then [`evalBinop b v1 v2`, `delta`] match_mp_tac delta_0_deterministic) \\ fs[] \\
`vR = evalBinop b v1 v2` by fs[] \\
by (qspecl_then [`evalBinop b v1 v2`, `delta`] match_mp_tac delta_0_deterministic \\ fs[]) \\
fs[] \\
qpat_x_assum `validIntervalbounds (Binop b f f') absenv P V`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validIntervalbounds_def] thm)) \\
qpat_x_assum `!absenv P V VarEnv ParamEnv vR. validIntervalbounds f absenv P V /\ Q /\ eval_exp 0 VarEnv ParamEnv P f vR ==> R`
qpat_x_assum
`!absenv P V VarEnv ParamEnv vR.
validIntervalbounds f absenv P V /\ Q /\ eval_exp 0 VarEnv ParamEnv P f vR ==> R`
(fn thm => qspecl_then [`absenv`,`P`, `V`, `VarEnv`, `ParamEnv`, `v1`] ASSUME_TAC thm) \\
qpat_x_assum `!absenv P V VarEnv ParamEnv vR. validIntervalbounds f' absenv P V /\ Q /\ eval_exp 0 VarEnv ParamEnv P f' vR ==> R`
qpat_x_assum
`!absenv P V VarEnv ParamEnv vR.
validIntervalbounds f' absenv P V /\ Q /\ eval_exp 0 VarEnv ParamEnv P f' vR ==> R`
(fn thm => qspecl_then [`absenv`,`P`, `V`, `VarEnv`, `ParamEnv`, `v2`] ASSUME_TAC thm) \\
Cases_on `b` \\ simp[evalBinop_def]
(* Plus case *)
......
......@@ -324,12 +324,12 @@ val pair_div_v_thm =
val divideInterval_v_thm = translate divideInterval_def;
val precond_def = fetch_thm "divideinterval_side_def"
(show_assums:=true)
(show_assums:=true);
val supersetInterval_v_thm = translate isSupersetInterval_def;
val validIvbounds_v_thm = translate validIntervalbounds_def;
val validIvbounds_thm = fetch "-" "validintervalbounds_side_def";
val _ = export_theory();
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