Commit 6953a7de authored by Heiko Becker's avatar Heiko Becker
Browse files

alpha renmaing of maxAbsFun into maxAbs

parent 0a383995
......@@ -87,8 +87,8 @@ multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`;
val divideInterval_def = Define `
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`;
val maxAbsFun_def = Define `
maxAbsFun iv = max (abs (FST iv)) (abs (SND iv))`;
val maxAbs_def = Define `
maxAbs iv = max (abs (FST iv)) (abs (SND iv))`;
val minAbsFun_def = Define `
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
......@@ -103,7 +103,7 @@ val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_de
invertInterval_def,
addInterval_def, subtractInterval_def,
multInterval_def, divideInterval_def,
maxAbsFun_def, minAbsFun_def
maxAbs_def, minAbsFun_def
];
val contained_implies_valid = store_thm ("contained_implies_valid",
......@@ -403,18 +403,18 @@ fs[]);
(** Properties of the maxAbs function **)
val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs",
``!a iv. contained a iv ==> abs a <= maxAbsFun iv``,
``!a iv. contained a iv ==> abs a <= maxAbs 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``,
``!a iv. contained a iv ==> a <= maxAbs 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``,
``!a iv. contained a iv ==> - a <= maxAbs 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);
......
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