Commit 91790db5 authored by Heiko Becker's avatar Heiko Becker

Make FloVer compile with HOL4 master

parent 16846e80
570cfc9afd5e6ac1fd5a51e50c0780453c975124
4f67f38e1314dcb1488b3925ddbbc4bbd80795bf
......@@ -13,15 +13,6 @@ val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val triangle_trans = store_thm (
"triangle_trans",
``!a b c.
abs (a + b) <= abs a + abs b /\
abs a + abs b <= c ==>
abs (a + b) <= c``,
rpt strip_tac
\\ REAL_ASM_ARITH_TAC);
val triangle_tac =
irule triangle_trans \\ fs[REAL_ABS_TRIANGLE];
......@@ -418,7 +409,7 @@ val err_prop_inversion_pos = store_thm ("err_prop_inversion_pos",
\\ `inv nR - inv nF <= 0` by REAL_ASM_ARITH_TAC
\\ `0 <= - (inv nR - inv nF) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv nR - inv nF)) = - (inv nR - inv nF)` by fs [ABS_REFL]
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[ABS_NEG]
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by metis_tac[ABS_NEG]
\\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
\\ `- (1 / nR) = 1 / - nR` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
......@@ -497,7 +488,7 @@ val err_prop_inversion_neg = store_thm ("err_prop_inversion_neg",
\\ `inv (- nF) - inv (- nR) <= 0` by REAL_ASM_ARITH_TAC
\\ `0 <= - (inv (- nF) - inv (-nR)) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv (- nF) - inv (- nR))) = - (inv (- nF) - inv (- nR))` by fs [ABS_REFL]
\\ `abs (inv (- nF) - inv (- nR)) = - (inv (- nF) - inv (- nR))` by fs [ABS_NEG]
\\ `abs (inv (- nF) - inv (- nR)) = - (inv (- nF) - inv (- nR))` by metis_tac[ABS_NEG]
\\ `inv (- nF) - inv (- nR) = inv nR - inv nF` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[]
\\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
......@@ -549,7 +540,7 @@ val err_prop_inversion_neg = store_thm ("err_prop_inversion_neg",
\\ `inv (- nR) - inv (- nF) <= 0` by REAL_ASM_ARITH_TAC
\\ `0 <= - (inv (- nR) - inv (-nR)) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv (- nR) - inv (- nF))) = - (inv (- nR) - inv (- nF))` by fs [ABS_REFL]
\\ `abs (inv (- nR) - inv (- nF)) = - (inv (- nR) - inv (- nF))` by fs [ABS_NEG]
\\ `abs (inv (- nR) - inv (- nF)) = - (inv (- nR) - inv (- nF))` by metis_tac[ABS_NEG]
\\ `inv (- nR) - inv (- nF) = inv nF - inv nR` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC)
\\ `abs (inv nF - inv nR) = - (inv (- nR) - inv (- nF))` by fs[]
\\ `abs (inv nR - inv nF) = - (inv (- nR) - inv (- nF))` by fs[ABS_SUB]
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -8,7 +8,7 @@
value according to IEEE 754.
**)
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory;
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory RealArith;
open AbbrevsTheory MachineTypeTheory TypeValidatorTheory RealSimpsTheory
RealRangeArithTheory IntervalArithTheory ExpressionsTheory
ExpressionAbbrevsTheory ExpressionSemanticsTheory FloverTactics
......@@ -81,16 +81,16 @@ val enclosure_to_abs = store_thm (
(abs a <= abs b /\ abs b <= abs c) \/
(abs c <= abs b /\ abs b <= abs a)``,
rpt strip_tac \\ fs[]
>- (`0 < b` by RealArith.REAL_ASM_ARITH_TAC
\\ `0 <= a /\ 0 <= b` by RealArith.REAL_ASM_ARITH_TAC
>- (`0 < b` by REAL_ASM_ARITH_TAC
\\ `0 <= a /\ 0 <= b` by REAL_ASM_ARITH_TAC
\\ `abs a = a` by (fs[ABS_REFL])
\\ `abs b = b` by (fs[ABS_REFL])
\\ `0 <= c` by RealArith.REAL_ASM_ARITH_TAC
\\ `0 <= c` by REAL_ASM_ARITH_TAC
\\ `abs c = c` by (fs[ABS_REFL])
\\ fs[])
>- (`~ (0 <= b)` by RealArith.REAL_ASM_ARITH_TAC
\\ `~ (0 <= a)` by RealArith.REAL_ASM_ARITH_TAC
\\ `~ (0 <= c)` by RealArith.REAL_ASM_ARITH_TAC
\\ fs[realTheory.abs])
>- (`~ (0 <= b)` by REAL_ASM_ARITH_TAC
\\ `~ (0 <= a)` by REAL_ASM_ARITH_TAC
\\ `~ (0 <= c)` by REAL_ASM_ARITH_TAC
\\ fs[realTheory.abs]));
fun assume_all l =
......
......@@ -247,6 +247,7 @@ val normal_value_is_float_value = store_thm (
\\ `abs (1 + &w2n ff.Significand / 2 pow 52) = 1 + &w2n ff.Significand / 2 pow 52`
by (rewrite_tac [ABS_REFL]
\\ irule REAL_LE_ADD \\ fs[])
\\ qpat_x_assum `abs (1 + _) = _` (fn thm => fs[thm])
\\ `2 pow 1024 <= 2 pow 1023`
by (irule REAL_LE_TRANS \\ find_exists_tac \\ fs[]
\\ rewrite_tac [REAL_LDISTRIB, REAL_MUL_RID]
......
......@@ -14,52 +14,51 @@ val _ = temp_overload_on("abs",``real$abs``);
val _ = monadsyntax.enable_monadsyntax();
val _ = List.app monadsyntax.enable_monad ["option"];
val _ = Datatype `
mType = REAL
| M16 | M32 | M64
|F num num (*first num is word length, second is fractional bits *)`;
Datatype:
mType = REAL | M16 | M32 | M64 | F num num (* first num is word length, second is fractional bits *)
End
val isFixedPoint_def = Define `
Definition isFixedPoint_def :
isFixedPoint (F w f) = T /\
isFixedPoint _ = F`;
isFixedPoint _ = F
End
val mTypeToR_def = Define `
Definition mTypeToR_def:
mTypeToR (m:mType) : real =
case m of
| REAL => 0
| M16 => 1 / (2 pow 11)
| M32 => 1 / (2 pow 24)
| M64 => 1 / (2 pow 53)
| F w f => 1 / (2 pow f)`;
| F w f => 1 / (2 pow f)
End
val computeError_def = Define `
Definition computeError_def:
computeError v m =
case m of
| REAL => 0
| F w f => mTypeToR m
| _ => abs v * mTypeToR m`;
val mTypeToR_pos = store_thm("mTypeToR_pos",
``! e. 0 <= mTypeToR e``,
Cases_on `e` \\ TRY EVAL_TAC
\\ fs[]);
val computeError_up = store_thm (
"computeError_up",
``! v a b m.
abs v <= maxAbs (a,b) ==>
computeError v m <= computeError (maxAbs (a,b)) m``,
| _ => abs v * mTypeToR m
End
Theorem mTypeToR_pos:
! e. 0 <= mTypeToR e
Proof
Cases_on `e` \\ EVAL_TAC \\ fs[]
QED
Theorem computeError_up:
! v a b m.
abs v <= maxAbs (a,b) ==>
computeError v m <= computeError (maxAbs (a,b)) m
Proof
rpt strip_tac \\ Cases_on `m`
\\ fs[mTypeToR_def, computeError_def]
\\ TRY RealArith.REAL_ASM_ARITH_TAC
\\ irule REAL_LE_RMUL_IMP \\ fs[]
\\ fs[maxAbs_def]
\\ `abs (real$max (abs a) (abs b)) = real$max (abs a) (abs b)`
by (once_rewrite_tac[ABS_REFL]
\\ fs[max_def]
\\ Cases_on `abs a <= abs b`\\ fs[]
\\ irule REAL_ABS_POS)
\\ fs[]);
\\ irule REAL_LE_TRANS \\ asm_exists_tac
\\ fs[ABS_LE]
QED
(**
Check if machine precision m1 is more precise than machine precision m2.
......@@ -71,20 +70,21 @@ val computeError_up = store_thm (
fixed-point number, no matter what the fractional bits may be.
For the moment, fixed-point and floating-point formats are incomparable.
**)
val isMorePrecise_def = Define `
Definition isMorePrecise_def:
isMorePrecise (m1:mType) (m2:mType) =
case m1, m2 of
| REAL, _ => T
| F w1 f1, F w2 f2 => w2 <= w1
| F w f, _ => F
| _, F w f => F
| _, _ => (mTypeToR (m1) <= mTypeToR (m2))`;
| _, _ => (mTypeToR (m1) <= mTypeToR (m2))
End
(**
More efficient version for performance, unfortunately we cannot do better
for fixed-points
**)
val morePrecise_def = Define `
Definition morePrecise_def:
(morePrecise REAL _ = T) /\
(morePrecise (F w1 f1) (F w2 f2) = (w2 <= w1)) /\
(morePrecise (F w f) _ = F) /\
......@@ -94,17 +94,19 @@ val morePrecise_def = Define `
(morePrecise M32 M16 = T) /\
(morePrecise M64 REAL = F) /\
(morePrecise M64 _ = T) /\
(morePrecise _ _ = F) `;
val morePrecise_trans = store_thm (
"morePrecise_trans",
``!m1 m2 m3.
morePrecise m1 m2 /\
morePrecise m2 m3 ==>
morePrecise m1 m3``,
(morePrecise _ _ = F)
End
Theorem morePrecise_trans:
!m1 m2 m3.
morePrecise m1 m2 /\
morePrecise m2 m3 ==>
morePrecise m1 m3
Proof
rpt strip_tac
\\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3`
\\ fs[morePrecise_def]);
\\ fs[morePrecise_def]
QED
val isMorePrecise_morePrecise = store_thm (
"isMorePrecise_morePrecise",
......
open RealArith
open realTheory realLib
open preamble
open RealArith;
open realTheory realLib;
open FloverTactics;
open preamble;
(*
val _ = ParseExtras.temp_tight_equality() *)
......@@ -83,4 +84,22 @@ val REAL_LE_ADD_FLIP = store_thm ("REAL_LE_ADD_FLIP",
a - c <= b``,
REAL_ASM_ARITH_TAC);
val triangle_trans = store_thm (
"triangle_trans",
``!a b c.
abs (a + b) <= abs a + abs b /\
abs a + abs b <= c ==>
abs (a + b) <= c``,
rpt strip_tac
\\ REAL_ASM_ARITH_TAC);
Theorem REAL_LE_ABS_TRANS:
! a b.
abs a <= b ==>
a <= b
Proof
rpt strip_tac \\ irule REAL_LE_TRANS
\\ find_exists_tac \\ fs[ABS_LE]
QED
val _ = export_theory();
......@@ -517,7 +517,7 @@ val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo",
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]);
metis_tac[REAL_MIN_ALT]);
val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
``!(a b:real).
......@@ -528,6 +528,8 @@ val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi",
fs[minAbsFun_def] \\
`abs a = - a` by REAL_ASM_ARITH_TAC \\
`abs b = - b` by REAL_ASM_ARITH_TAC \\
fs[REAL_MIN_ALT]);
ntac 2 (pop_assum (fn thm => rewrite_tac [thm])) \\
`-b <= -a` by fs[] \\
metis_tac[REAL_MIN_ALT]);
val _ = export_theory();
Subproject commit 52270c049337b1915a61c946c535e43a0d2084b5
Subproject commit dc73bd8f21601e06bdc92eb303865a3992673970
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