formal_lp/old/arith/float_theory.hl

   1 (* Theoretical results for the floating-point arithmetic *)\r
   2 \r
   3 (* Dependencies *)\r
   4 needs "../formal_lp/arith/nat.hl";;\r
   5 needs "../formal_lp/arith/num_exp_theory.hl";;\r
   6 \r
   7 module Float_theory = struct\r
   8 \r
   9 open Num_exp_theory;;\r
  10 open Arith_nat;;\r
  11 open Arith_options;;\r
  12 \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
  16 \r
  17 let min_exp_def = new_definition (mk_eq(`min_exp:num`, min_exp_const));;\r
  18 \r
  19 \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
  22 \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
  27                            [\r
  28                              REWRITE_TAC[REAL_OF_NUM_EQ; EXP_EQ_0] THEN ARITH_TAC;\r
  29                              ALL_TAC\r
  30                            ] THEN\r
  31                            ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_RID]);;\r
  32 \r
  33 \r
  34 \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
  37 \r
  38 \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
  41 \r
  42 \r
  43 \r
  44 \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
  49 \r
  50 \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
  56 \r
  57 \r
  58 \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
  62                          EQ_TAC THENL\r
  63                          [\r
  64                            STRIP_TAC THEN POP_ASSUM MP_TAC THENL\r
  65                              [\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
  69                                  ARITH_TAC\r
  70                              ];\r
  71 \r
  72                            DISCH_TAC THEN\r
  73                              DISJ2_TAC THEN DISJ1_TAC THEN\r
  74                              ASM_REWRITE_TAC[REAL_OF_NUM_EQ; NUM_EXP_EQ_0]\r
  75                          ]);;\r
  76 \r
  77 \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
  80    DISCH_TAC THEN\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
  84 \r
  85 \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
  89 \r
  90                                           \r
  91 \r
  92 end;;\r