Commit 1bc535ca authored by Heiko Becker's avatar Heiko Becker
Browse files

Division proof, next half done, compiles

parent 4e20a38b
This diff is collapsed.
......@@ -384,7 +384,7 @@ fs iv_ss \\ rpt strip_tac
max4_correct)))));
val interval_division_valid = store_thm ( "interval_division_valid",
``!(iv1:interval) (iv2:interval) (a:real) (b:real).
``!(iv1:interval) (iv2:interval) (a:real) (b:real).
(IVhi iv2 < 0 \/ 0 < IVlo iv2) /\
contained a iv1 /\
contained b iv2 ==>
......@@ -403,25 +403,48 @@ fs[]);
(** Properties of the maxAbs function **)
val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs",
``!a iv. contained a iv ==> abs a <= maxAbsFun iv``,
rpt strip_tac\\ fs iv_ss \\ match_mp_tac maxAbs \\ fs []);
``!a iv. contained a iv ==> abs a <= maxAbsFun iv``,
rpt strip_tac\\ fs iv_ss \\ match_mp_tac maxAbs \\ fs []);
val contained_leq_maxAbs_val = store_thm ("contained_leq_maxAbs_val",
``!a iv. contained a iv ==> a <= maxAbsFun iv``,
rpt strip_tac \\ fs iv_ss \\
`abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
REAL_ASM_ARITH_TAC);
``!a iv. contained a iv ==> a <= maxAbsFun iv``,
rpt strip_tac \\ fs iv_ss \\
`abs a <= max (abs (FST iv)) (abs (SND iv))`
by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
REAL_ASM_ARITH_TAC);
val contained_leq_maxAbs_neg_val = store_thm ("contained_leq_maxAbs_neg_val",
``!a iv. contained a iv ==> - a <= maxAbsFun iv``,
rpt strip_tac\\ fs iv_ss \\
`abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
REAL_ASM_ARITH_TAC);
``!a iv. contained a iv ==> - a <= maxAbsFun iv``,
rpt strip_tac\\ fs iv_ss \\
`abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
REAL_ASM_ARITH_TAC);
val distance_gives_iv = store_thm ("distance_gives_iv",
``!a b e iv. contained a iv /\ abs (a - b) <= e ==> contained b (widenInterval iv e)``,
fs iv_ss \\ rpt strip_tac \\
`(b:real) - e <= a /\ a <= b + e` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC);
``!a b e iv. contained a iv /\ abs (a - b) <= e ==> contained b (widenInterval iv e)``,
fs iv_ss \\ rpt strip_tac \\
`(b:real) - e <= a /\ a <= b + e` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC);
val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
``!(a b:real).
(0 < a) /\
(a <= b) ==>
(minAbsFun (a,b) = a)``,
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = a` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
`abs b = b` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\
fs[REAL_MIN_ALT]);
val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
``!(a b:real).
(b < 0) /\
(a <= b) ==>
(minAbsFun (a,b) = - b)``,
rpt (strip_tac) \\
fs[minAbsFun_def] \\
`abs a = - a` by REAL_ASM_ARITH_TAC \\
`abs b = - b` by REAL_ASM_ARITH_TAC \\
fs[REAL_MIN_ALT] );
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