1 (* Theoretical results for the floating-point arithmetic *)
\r
4 needs "../formal_lp/arith/nat.hl";;
\r
5 needs "../formal_lp/arith/num_exp_theory.hl";;
\r
7 module Float_theory = struct
\r
9 open Num_exp_theory;;
\r
11 open Arith_options;;
\r
13 (* The main definition *)
\r
14 let min_exp_num_const = rand (mk_small_numeral_array min_exp);;
\r
15 let min_exp_const = mk_small_numeral min_exp;;
\r
17 let min_exp_def = new_definition (mk_eq(`min_exp:num`, min_exp_const));;
\r
20 let float_tm = `float s n e = (if s then (-- &1) else &1) * &(num_exp n e) / &(num_exp 1 min_exp)`;;
\r
21 let float = new_definition float_tm;;
\r
23 let FLOAT_OF_NUM = (GEN_ALL o prove)(`&n = float F n min_exp`,
\r
24 REWRITE_TAC[float; num_exp; REAL_MUL_LID] THEN
\r
25 REWRITE_TAC[GSYM REAL_OF_NUM_MUL; REAL_MUL_LID; real_div] THEN
\r
26 SUBGOAL_THEN (mk_comb(`(~)`, mk_eq(mk_comb(`&`, mk_binop `EXP` base_const `min_exp`), `&0`))) ASSUME_TAC THENL
\r
28 REWRITE_TAC[REAL_OF_NUM_EQ; EXP_EQ_0] THEN ARITH_TAC;
\r
31 ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_RID]);;
\r
35 let FLOAT_NEG = prove(`!s n e. --float s n e = float (~s) n e`,
\r
36 REWRITE_TAC[float] THEN REAL_ARITH_TAC);;
\r
39 let FLOAT_NEG_F = (GSYM o REWRITE_RULE[] o SPEC `T`) FLOAT_NEG;;
\r
40 let FLOAT_NEG_T = (GSYM o REWRITE_RULE[] o SPEC `F`) FLOAT_NEG;;
\r
45 let FLOAT_F_POS = prove(`!n e. &0 <= float F n e`,
\r
46 REPEAT GEN_TAC THEN REWRITE_TAC[float; REAL_MUL_LID; real_div] THEN
\r
47 MATCH_MP_TAC REAL_LE_MUL THEN
\r
48 REWRITE_TAC[REAL_POS; REAL_LE_INV_EQ]);;
\r
51 let FLOAT_T_NEG = prove(`!n e. float T n e <= &0`,
\r
52 REPEAT GEN_TAC THEN REWRITE_TAC[float; real_div] THEN
\r
53 REWRITE_TAC[REAL_ARITH `-- &1 * a * b <= &0 <=> &0 <= a * b`] THEN
\r
54 MATCH_MP_TAC REAL_LE_MUL THEN
\r
55 REWRITE_TAC[REAL_POS; REAL_LE_INV_EQ]);;
\r
59 let FLOAT_EQ_0 = prove(`!s n e. float s n e = &0 <=> n = 0`,
\r
60 REPEAT GEN_TAC THEN REWRITE_TAC[float; real_div] THEN
\r
61 REWRITE_TAC[REAL_ENTIRE] THEN
\r
64 STRIP_TAC THEN POP_ASSUM MP_TAC THENL
\r
66 COND_CASES_TAC THEN REAL_ARITH_TAC;
\r
67 REWRITE_TAC[REAL_OF_NUM_EQ; NUM_EXP_EQ_0];
\r
68 REWRITE_TAC[REAL_INV_EQ_0; REAL_OF_NUM_EQ; NUM_EXP_EQ_0] THEN
\r
73 DISJ2_TAC THEN DISJ1_TAC THEN
\r
74 ASM_REWRITE_TAC[REAL_OF_NUM_EQ; NUM_EXP_EQ_0]
\r
78 let FLOAT_F_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2
\r
79 ==> float F n1 e1 <= float F n2 e2`,
\r
81 REWRITE_TAC[float; REAL_MUL_LID; real_div] THEN
\r
82 MATCH_MP_TAC REAL_LE_RMUL THEN
\r
83 ASM_REWRITE_TAC[REAL_OF_NUM_LE; REAL_LE_INV_EQ; REAL_POS]);;
\r
86 let FLOAT_T_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2
\r
87 ==> float T n2 e2 <= float T n1 e1`,
\r
88 REWRITE_TAC[FLOAT_NEG_T; REAL_LE_NEG; FLOAT_F_bound]);;
\r