Commit d09f63e5 authored by Heiko Becker's avatar Heiko Becker

Preliminary lemmas for Multiplication

parent d313ddeb
......@@ -406,6 +406,12 @@ 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 []);
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);
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 \\
......
......@@ -43,4 +43,16 @@ val real_le_trans2 = store_thm ("real_le_trans2",
val mEps_geq_zero = store_thm ("mEps_geq_zero",
``0 <= machineEpsilon``, once_rewrite_tac[machineEpsilon_def] \\ EVAL_TAC);
val err_up = store_thm ("err_up",
``!a b (c:real).
0 <= c /\
a - b <= c /\
0 < a - b ==>
b <= a + c``,
rpt (strip_tac) \\
`b < a` by REAL_ASM_ARITH_TAC \\
`a <= b + c` by REAL_ASM_ARITH_TAC \\
`b + c <= a + c` by REAL_ASM_ARITH_TAC \\
REAL_ASM_ARITH_TAC);
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