(* Theoretical results for the floating-point arithmetic *)

(* Dependencies *)
needs "../formal_lp/arith/nat.hl";;
needs "../formal_lp/arith/num_exp_theory.hl";;

module Float_theory = struct

open Num_exp_theory;;
open Arith_nat;;
open Arith_options;;

(* The main definition *)
let min_exp_num_const = rand (mk_small_numeral_array min_exp);;
let min_exp_const = mk_small_numeral min_exp;;

let min_exp_def = new_definition (mk_eq(`min_exp:num`, min_exp_const));;


let float_tm = `float s n e = (if s then (-- &1) else &1) * &(num_exp n e) / &(num_exp 1 min_exp)`;;
let float = new_definition float_tm;;

let FLOAT_OF_NUM = (GEN_ALL o prove)(`&n = float F n min_exp`,
                         REWRITE_TAC[float; num_exp; REAL_MUL_LID] THEN
                           REWRITE_TAC[GSYM REAL_OF_NUM_MUL; REAL_MUL_LID; real_div] THEN
                           SUBGOAL_THEN (mk_comb(`(~)`, mk_eq(mk_comb(`&`, mk_binop `EXP` base_const `min_exp`), `&0`))) ASSUME_TAC THENL
                           [
                             REWRITE_TAC[REAL_OF_NUM_EQ; EXP_EQ_0] THEN ARITH_TAC;
                             ALL_TAC
                           ] THEN
                           ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_RID]);;



let FLOAT_NEG = 
prove(`!s n e. --float s n e = float (~s) n e`,

   REWRITE_TAC[float] THEN REAL_ARITH_TAC);;


let FLOAT_NEG_F = (GSYM o REWRITE_RULE[] o SPEC `T`) FLOAT_NEG;;
let FLOAT_NEG_T = (GSYM o REWRITE_RULE[] o SPEC `F`) FLOAT_NEG;;




let FLOAT_F_POS = 
prove(`!n e. &0 <= float F n e`,

   REPEAT GEN_TAC THEN REWRITE_TAC[float; REAL_MUL_LID; real_div] THEN
     MATCH_MP_TAC REAL_LE_MUL THEN
     REWRITE_TAC[REAL_POS; REAL_LE_INV_EQ]);;


let FLOAT_T_NEG = 
prove(`!n e. float T n e <= &0`,

                        REPEAT GEN_TAC THEN REWRITE_TAC[float; real_div] THEN
                          REWRITE_TAC[REAL_ARITH `-- &1 * a * b <= &0 <=> &0 <= a * b`] THEN
                          MATCH_MP_TAC REAL_LE_MUL THEN
                          REWRITE_TAC[REAL_POS; REAL_LE_INV_EQ]);;



let FLOAT_EQ_0 = 
prove(`!s n e. float s n e = &0 <=> n = 0`,

                       REPEAT GEN_TAC THEN REWRITE_TAC[float; real_div] THEN
                         REWRITE_TAC[REAL_ENTIRE] THEN
                         EQ_TAC THENL
                         [
                           STRIP_TAC THEN POP_ASSUM MP_TAC THENL
                             [
                               COND_CASES_TAC THEN REAL_ARITH_TAC;
                               REWRITE_TAC[REAL_OF_NUM_EQ; NUM_EXP_EQ_0];
                               REWRITE_TAC[REAL_INV_EQ_0; REAL_OF_NUM_EQ; NUM_EXP_EQ_0] THEN
                                 ARITH_TAC
                             ];

                           DISCH_TAC THEN
			     DISJ2_TAC THEN DISJ1_TAC THEN
                             ASM_REWRITE_TAC[REAL_OF_NUM_EQ; NUM_EXP_EQ_0]
                         ]);;


let FLOAT_F_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2
                                      ==> float F n1 e1 <= float F n2 e2`,
   DISCH_TAC THEN
     REWRITE_TAC[float; REAL_MUL_LID; real_div] THEN
     MATCH_MP_TAC REAL_LE_RMUL THEN
     ASM_REWRITE_TAC[REAL_OF_NUM_LE; REAL_LE_INV_EQ; REAL_POS]);;


let FLOAT_T_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2
                                        ==> float T n2 e2 <= float T n1 e1`,
                      REWRITE_TAC[FLOAT_NEG_T; REAL_LE_NEG; FLOAT_F_bound]);;

					  

end;;