formal_ineqs/arith/float_theory.hl

   1 (* =========================================================== *)\r
   2 (* Theoretical results for floating point arithmetic           *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 \r
   8 (* Dependencies *)\r
   9 needs "arith/nat.hl";;\r
  10 needs "arith/num_exp_theory.hl";;\r
  11 \r
  12 module Float_theory = struct\r
  13 \r
  14 open Num_exp_theory;;\r
  15 open Arith_nat;;\r
  16 \r
  17 (* Fix the minimal exponent *)\r
  18 let min_exp = !Arith_options.min_exp;;\r
  19 \r
  20 (* The main definition *)\r
  21 let min_exp_num_const = rand (mk_small_numeral_array min_exp);;\r
  22 let min_exp_const = mk_small_numeral min_exp;;\r
  23 \r
  24 let min_exp_def = new_definition (mk_eq(`min_exp:num`, min_exp_const));;\r
  25 \r
  26 let float_tm = `float_num s n e = (if s then (-- &1) else &1) * &(num_exp n e) / &(num_exp 1 min_exp)`;;\r
  27 let float = new_definition float_tm;;\r
  28 \r
  29 let FLOAT_OF_NUM = (GEN_ALL o prove)(`&n = float_num F n min_exp`,\r
  30                          REWRITE_TAC[float; num_exp; REAL_MUL_LID] THEN\r
  31                            REWRITE_TAC[GSYM REAL_OF_NUM_MUL; REAL_MUL_LID; real_div] THEN\r
  32                            SUBGOAL_THEN (mk_comb(`(~)`, mk_eq(mk_comb(`&`, mk_binop `EXP` base_const `min_exp`), `&0`))) ASSUME_TAC THENL\r
  33                            [\r
  34                              REWRITE_TAC[REAL_OF_NUM_EQ; EXP_EQ_0] THEN ARITH_TAC;\r
  35                              ALL_TAC\r
  36                            ] THEN\r
  37                            ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_RID]);;\r
  38 \r
  39 let FLOAT_NEG = prove(`!s n e. --float_num s n e = float_num (~s) n e`,\r
  40    REWRITE_TAC[float] THEN REAL_ARITH_TAC);;\r
  41 \r
  42 let FLOAT_NEG_F = (GSYM o REWRITE_RULE[] o SPEC `T`) FLOAT_NEG;;\r
  43 let FLOAT_NEG_T = (GSYM o REWRITE_RULE[] o SPEC `F`) FLOAT_NEG;;\r
  44 \r
  45 let FLOAT_F_POS = prove(`!n e. &0 <= float_num 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
  49 \r
  50 let FLOAT_T_NEG = prove(`!n e. float_num T n e <= &0`,\r
  51                         REPEAT GEN_TAC THEN REWRITE_TAC[float; real_div] THEN\r
  52                           REWRITE_TAC[REAL_ARITH `-- &1 * a * b <= &0 <=> &0 <= a * b`] THEN\r
  53                           MATCH_MP_TAC REAL_LE_MUL THEN\r
  54                           REWRITE_TAC[REAL_POS; REAL_LE_INV_EQ]);;\r
  55 \r
  56 let FLOAT_EQ_0 = prove(`!s n e. float_num s n e = &0 <=> n = 0`,\r
  57                        REPEAT GEN_TAC THEN REWRITE_TAC[float; real_div] THEN\r
  58                          REWRITE_TAC[REAL_ENTIRE] THEN\r
  59                          EQ_TAC THENL\r
  60                          [\r
  61                            STRIP_TAC THEN POP_ASSUM MP_TAC THENL\r
  62                              [\r
  63                                COND_CASES_TAC THEN REAL_ARITH_TAC;\r
  64                                REWRITE_TAC[REAL_OF_NUM_EQ; NUM_EXP_EQ_0];\r
  65                                REWRITE_TAC[REAL_INV_EQ_0; REAL_OF_NUM_EQ; NUM_EXP_EQ_0] THEN\r
  66                                  ARITH_TAC\r
  67                              ];\r
  68 \r
  69                            DISCH_TAC THEN\r
  70                              DISJ2_TAC THEN DISJ1_TAC THEN\r
  71                              ASM_REWRITE_TAC[REAL_OF_NUM_EQ; NUM_EXP_EQ_0]\r
  72                          ]);;\r
  73 \r
  74 let FLOAT_F_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2\r
  75                                       ==> float_num F n1 e1 <= float_num F n2 e2`,\r
  76    DISCH_TAC THEN\r
  77      REWRITE_TAC[float; REAL_MUL_LID; real_div] THEN\r
  78      MATCH_MP_TAC REAL_LE_RMUL THEN\r
  79      ASM_REWRITE_TAC[REAL_OF_NUM_LE; REAL_LE_INV_EQ; REAL_POS]);;\r
  80 \r
  81 let FLOAT_T_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2\r
  82                                         ==> float_num T n2 e2 <= float_num T n1 e1`,\r
  83                       REWRITE_TAC[FLOAT_NEG_T; REAL_LE_NEG; FLOAT_F_bound]);;\r
  84 \r
  85                                   \r
  86 \r
  87 end;;\r