# Theory Affine_Arithmetic.Float_Real

section ‹Dyadic Rational Representation of Real›
theory Float_Real
imports
"HOL-Library.Float"
Optimize_Float
begin
text ‹\label{sec:floatreal}›

code_datatype real_of_float

abbreviation
float_of_nat :: "nat ⇒ float"
where
"float_of_nat ≡ of_nat"

abbreviation
float_of_int :: "int ⇒ float"
where
"float_of_int ≡ of_int"

text‹Collapse nested embeddings›

text ‹Operations›

text ‹Undo code setup for @{term Ratreal}.›

lemma of_rat_numeral_eq [code_abbrev]:
"real_of_float (numeral w) = Ratreal (numeral w)"
by simp

lemma zero_real_code [code]:
"0 = real_of_float 0"
by simp

lemma one_real_code [code]:
"1 = real_of_float 1"
by simp

lemma [code_abbrev]:
"(real_of_float (of_int a) :: real) = (Ratreal (Rat.of_int a) :: real)"
by (auto simp: Rat.of_int_def )

lemma [code_abbrev]:
"real_of_float 0 ≡ Ratreal 0"
by simp

lemma [code_abbrev]:
"real_of_float 1 = Ratreal 1"
by simp

lemmas compute_real_of_float[code del]

lemmas [code del] =
real_equal_code
real_less_eq_code
real_less_code
real_plus_code
real_times_code
real_uminus_code
real_minus_code
real_inverse_code
real_divide_code
real_floor_code
Float.compute_truncate_down
Float.compute_truncate_up

lemma real_equal_code [code]:
"HOL.equal (real_of_float x) (real_of_float y) ⟷ HOL.equal x y"
by (metis (poly_guards_query) equal real_of_float_inverse)

abbreviation FloatR::"int⇒int⇒real" where
"FloatR a b ≡ real_of_float (Float a b)"

lemma real_less_eq_code' [code]: "real_of_float x ≤ real_of_float y ⟷ x ≤ y"
and real_less_code' [code]: "real_of_float x < real_of_float y ⟷ x < y"
and real_plus_code' [code]: "real_of_float x + real_of_float y = real_of_float (x + y)"
and real_times_code' [code]: "real_of_float x * real_of_float y = real_of_float (x * y)"
and real_uminus_code' [code]: "- real_of_float x = real_of_float (- x)"
and real_minus_code' [code]: "real_of_float x - real_of_float y = real_of_float (x - y)"
and real_inverse_code' [code]: "inverse (FloatR a b) =
(if FloatR a b = 2 then FloatR 1 (-1) else
if a = 1 then FloatR 1 (- b) else
Code.abort (STR ''inverse not of 2'') (λ_. inverse (FloatR a b)))"
and real_divide_code' [code]: "FloatR a b / FloatR c d =
(if FloatR c d = 2 then if a mod 2 = 0 then FloatR (a div 2) b else FloatR a (b - 1) else
if c = 1 then FloatR a (b - d) else
Code.abort (STR ''division not by 2'') (λ_. FloatR a b / FloatR c d))"
and real_floor_code' [code]: "floor (real_of_float x) = int_floor_fl x"
and real_abs_code' [code]: "abs (real_of_float x) = real_of_float (abs x)"
by (auto simp add: int_floor_fl.rep_eq powr_diff powr_minus inverse_eq_divide)

lemma compute_round_down[code]: "round_down prec (real_of_float f) = real_of_float (float_down prec f)"
by simp

lemma compute_round_up[code]: "round_up prec (real_of_float f) = real_of_float (float_up prec f)"
by simp

lemma compute_truncate_down[code]:
"truncate_down prec (real_of_float f) = real_of_float (float_round_down prec f)"

lemma compute_truncate_up[code]:
"truncate_up prec (real_of_float f) = real_of_float (float_round_up prec f)"