Commit 53adcf51 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove multiplication bound in HOL-Light'

parent 48c2792e
This diff is collapsed.
......@@ -87,3 +87,7 @@ let mEps_geq_zero =
`(&0) <= machineEpsilon`,
SIMP_TAC [machineEpsilon]
THEN REAL_ARITH_TAC);;
let REAL_ABS_CASES = prove (
`!(a:real) b. abs (a) <= b <=> (((a >= &0) /\ a <= b) \/ ((a < &0) /\ -- a <= b))`,
REAL_ARITH_TAC);;
......@@ -376,6 +376,50 @@ let contained_leq_maxAbs = prove (
THEN mp iv_le_maxAbs
THEN auto);;
let contained_leq_maxAbs_val = prove (
`! (a:real) ivlo ivhi.
contained a (ivlo, ivhi) ==>
(a <= maxAbsFun (ivlo, ivhi))`,
intros "!a ivlo ivhi; contained_a"
THEN rewrite contained "contained_a"
THEN rewrite IVlo "contained_a"
THEN rewrite IVhi "contained_a"
THEN rewrite SND "contained_a"
THEN SIMP_TAC[maxAbsFun]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `abs (a:real)`
THEN split
THENL [
SIMP_TAC[REAL_ABS_LE];
mp iv_le_maxAbs
THEN auto
]);;
let contained_leq_maxAbs_neg_val = prove (
`! (a:real) ivlo ivhi.
contained a (ivlo, ivhi) ==>
(-- a <= maxAbsFun (ivlo, ivhi))`,
intros "!a ivlo ivhi; contained_a"
THEN rewrite contained "contained_a"
THEN rewrite IVlo "contained_a"
THEN rewrite IVhi "contained_a"
THEN rewrite SND "contained_a"
THEN SIMP_TAC[maxAbsFun]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `abs (a:real)`
THEN split
THENL [
mp REAL_LE_TRANS
THEN EXISTS_TAC `abs (-- (a:real))`
THEN split
THENL [
SIMP_TAC[REAL_ABS_LE];
SIMP_TAC [REAL_ABS_NEG; REAL_LE_REFL]
];
mp iv_le_maxAbs
THEN auto
]);;
let Rabs_error_bounded_maxAbs = prove (
`!(a:real) b eps ivlo ivhi.
(abs (a - b) <= eps) /\
......
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