(* 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;;