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

Intermediate state of division in HOL4, does not compile

parent 112d9e19
......@@ -891,24 +891,93 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
(divideInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon` \\
conj_tac \\
>- (match_mp_tac REAL_LE_ADD2 \\ conj_tac \\
>- (cheat)
>- (simp[maxAbsFun_def] \\
once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\
conj_tac \\ simp[mEps_geq_zero] \\
match_mp_tac maxAbs \\
`contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv \\
>- (`contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv \\
qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\
`contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv \\
by (match_mp_tac distance_gives_iv \\
qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\
`contained (nF1 / nF2) (divideInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac interval_division_valid \\
conj_tac \\ fs[]) \\
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[]))
>- (fs[]) \\
));
match_mp_tac REAL_LE_ADD2 \\ conj_tac
>- (rpt (qpat_x_assum `eval_exp _ _ _ _ _` kall_tac) \\
`contained (inv nR2) (invertInterval (e2lo, e2hi))`
by (match_mp_tac interval_inversion_valid \\ conj_tac \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`contained (inv nF2) (invertInterval (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac interval_inversion_valid \\ conj_tac \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR1 <= maxAbsFun (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`inv nR2 <= maxAbsFun (invertInterval(e2lo, e2hi))`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR1 <= maxAbsFun (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`- inv nR2 <= maxAbsFun (invertInterval (e2lo, e2hi))`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR1 * err2 <= maxAbsFun (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-nR1 * err2 <= maxAbsFun (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`inv nR2 * err1 <= maxAbsFun (invertInterval(e2lo, e2hi)) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`- inv nR2 * err1 <= maxAbsFun (invertInterval(e2lo, e2hi)) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`- (err1 * err2) <= err1 * err2`
by (fs[REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC) \\
`0 <= maxAbsFun (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC \\
`0 <= maxAbsFun (invertInterval (e2lo, e2hi)) * err1` by REAL_ASM_ARITH_TAC \\
`maxAbsFun (e1lo, e1hi) * err2 <= maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (invertInterval (e2lo, e2hi)) * err1`
by (REAL_ASM_ARITH_TAC) \\
`maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (invertInterval (e2lo, e2hi)) * err1 <=
maxAbsFun (e1lo, e1hi) * err2 + maxAbsFun (invertInterval (e2lo, e2hi)) * err1 + err1 * err2`
by REAL_ASM_ARITH_TAC \\
(* Case distinction for divisor positive or negative in float and real valued execution *)
fs[] \\
rpt (qpat_x_assum `validIntervalbounds _ _ _` kall_tac) \\
rpt (qpat_x_assum `validErrorbound _ _ ` kall_tac) \\
rpt (qpat_x_assum `absenv _ = _` kall_tac) \\
rpt (qpat_x_assum `isSupersetInterval _ _` kall_tac) \\
rpt (qpat_x_assum `maxAbsFun (e1lo,e1hi) *
(1 /
(minAbsFun (widenInterval (e2lo,e2hi) err2) *
minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
maxAbsFun (invertInterval (e2lo,e2hi)) * err1 +
err1 *
(1 /
(minAbsFun (widenInterval (e2lo,e2hi) err2) *
minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
maxAbsFun
(divideInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon <= e` kall_tac) \\
(* Negative case *)
>- (rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\
cheat)
>- (CCONTR_TAC \\
rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\
`e2lo <= e2hi` by REAL_ASM_ARITH_TAC \\
`e2lo <= e2hi + err2` by REAL_ASM_ARITH_TAC \\
`e2lo <= e2hi + err2` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC
)
>- (CCONTR_TAC \\
rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\
`e2lo <= e2hi` by REAL_ASM_ARITH_TAC \\
`e2lo - err2 <= e2hi` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC)
>- (rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def] thm) \\
`abs (inv nR2 - inv nF2) <= err2 * (inv ((e2lo - err2) * (e2lo -err2)))`
by (match_mp_tac err_prop_inversion_pos \\
qexists_tac `e2hi` \\ rpt(conj_tac) \\
fs[contained_def, IVlo_def, IVhi_def]) \\
cheat
)
)
>- (simp[maxAbsFun_def] \\
once_rewrite_tac [REAL_MUL_COMM] \\ match_mp_tac REAL_LE_LMUL_IMP \\
conj_tac \\ simp[mEps_geq_zero] \\
match_mp_tac maxAbs \\
`contained (nF1 / nF2) (divideInterval (widenInterval (e1lo, e1hi) err1) (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac interval_division_valid \\
conj_tac \\ fs[]) \\
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[]))
>- (fs[])));
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