# Theory Float

theory Float
imports Log_Nat Lattice_Algebras

section

theory Float
imports Log_Nat Lattice_Algebras
begin

definition

typedef float = float
morphisms real_of_float float_of
unfolding float_def by auto

setup_lifting type_definition_float

declare real_of_float [code_unfold]

lemmas float_of_inject[simp]

declare [[coercion ]]

lemma real_of_float_eq:  for f1 f2 :: float
unfolding real_of_float_inject ..

declare real_of_float_inverse[simp] float_of_inverse [simp]
declare real_of_float [simp]

subsection

lemma floatI:  for m e :: int
by (auto simp: float_def)

lemma zero_float[simp]:
by (auto simp: float_def)

lemma one_float[simp]:
by (intro floatI[of 1 0]) simp

lemma numeral_float[simp]:
by (intro floatI[of  0]) simp

lemma neg_numeral_float[simp]:
by (intro floatI[of  0]) simp

lemma real_of_int_float[simp]:  for x :: int
by (intro floatI[of x 0]) simp

lemma real_of_nat_float[simp]:  for x :: nat
by (intro floatI[of x 0]) simp

lemma two_powr_int_float[simp]:  for i :: int
by (intro floatI[of 1 i]) simp

lemma two_powr_nat_float[simp]:  for i :: nat
by (intro floatI[of 1 i]) simp

lemma two_powr_minus_int_float[simp]:  for i :: int
by (intro floatI[of 1 ]) simp

lemma two_powr_minus_nat_float[simp]:  for i :: nat
by (intro floatI[of 1 ]) simp

lemma two_powr_numeral_float[simp]:
by (intro floatI[of 1 ]) simp

lemma two_powr_neg_numeral_float[simp]:
by (intro floatI[of 1 ]) simp

lemma two_pow_float[simp]:
by (intro floatI[of 1 n]) (simp add: powr_realpow)

lemma plus_float[simp]:
unfolding float_def
proof (safe, simp)
have *:
if  for e1 m1 e2 m2 :: int
proof -
from that have
by (simp add: powr_diff field_simps flip: powr_realpow)
then show ?thesis
by blast
qed
fix e1 m1 e2 m2 :: int
consider  |  by (rule linorder_le_cases)
then show
proof cases
case 1
from *[OF this, of m2 m1] show ?thesis
next
case 2
then show ?thesis by (rule *)
qed
qed

lemma uminus_float[simp]:
apply (auto simp: float_def)
apply hypsubst_thin
apply (rename_tac m e)
apply (rule_tac x= in exI)
apply (rule_tac x= in exI)
done

lemma times_float[simp]:
apply (auto simp: float_def)
apply hypsubst_thin
apply (rename_tac mx my ex ey)
apply (rule_tac x= in exI)
apply (rule_tac x= in exI)
done

lemma minus_float[simp]:
using plus_float [of x ] by simp

lemma abs_float[simp]:
by (cases x rule: linorder_cases[of 0]) auto

lemma sgn_of_float[simp]:
by (cases x rule: linorder_cases[of 0]) (auto intro!: uminus_float)

lemma div_power_2_float[simp]:
apply hypsubst_thin
apply (rename_tac m e)
apply (rule_tac x= in exI)
apply (rule_tac x= in exI)
done

lemma div_power_2_int_float[simp]:
apply hypsubst_thin
apply (rename_tac m e)
apply (rule_tac x= in exI)
apply (rule_tac x= in exI)
done

lemma div_numeral_Bit0_float[simp]:
assumes
shows
proof -
have
by (intro assms div_power_2_float)
also have
by (induct n) auto
finally show ?thesis .
qed

lemma div_neg_numeral_Bit0_float[simp]:
assumes
shows
proof -
have
using assms by simp
also have
by simp
finally show ?thesis .
qed

lemma power_float[simp]:
assumes
shows
proof -
from assms obtain m e :: int where
by (auto simp: float_def)
then show ?thesis
by (auto intro!: floatI[where m= and e = ]
simp: power_mult_distrib powr_realpow[symmetric] powr_powr)
qed

lift_definition Float ::  is
by simp
declare Float.rep_eq[simp]

code_datatype Float

lemma compute_real_of_float[code]:

subsection

instantiation float ::
begin

lift_definition zero_float :: float is 0 by simp
declare zero_float.rep_eq[simp]

lift_definition one_float :: float is 1 by simp
declare one_float.rep_eq[simp]

lift_definition plus_float ::  is  by simp
declare plus_float.rep_eq[simp]

lift_definition times_float ::  is  by simp
declare times_float.rep_eq[simp]

lift_definition minus_float ::  is  by simp
declare minus_float.rep_eq[simp]

lift_definition uminus_float ::  is  by simp
declare uminus_float.rep_eq[simp]

lift_definition abs_float ::  is abs by simp
declare abs_float.rep_eq[simp]

lift_definition sgn_float ::  is sgn by simp
declare sgn_float.rep_eq[simp]

lift_definition equal_float ::  is  .

lift_definition less_eq_float ::  is  .
declare less_eq_float.rep_eq[simp]

lift_definition less_float ::  is  .
declare less_float.rep_eq[simp]

instance
by standard (transfer; fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+

end

lemma real_of_float [simp]:
by (induct n) simp_all

lemma real_of_float_of_int_eq [simp]:
by (cases z rule: int_diff_cases) (simp_all add: of_rat_diff)

lemma Float_0_eq_0[simp]:
by transfer simp

lemma real_of_float_power[simp]:  for f :: float
by (induct n) simp_all

lemma real_of_float_min:
and real_of_float_max:
for x y :: float

instance float :: unbounded_dense_linorder
proof
fix a b :: float
show
apply (intro exI[of _ ])
apply transfer
apply simp
done
show
apply (intro exI[of _ ])
apply transfer
apply simp
done
show  if
apply (rule exI[of _ ])
using that
apply transfer
done
qed

begin

definition inf_float ::
where

definition sup_float ::
where

instance
by standard (transfer; simp add: inf_float_def sup_float_def real_of_float_min real_of_float_max)+

end

lemma float_numeral[simp]:
apply (induct x)
apply simp
apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq float_of_inverse
plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
done

lemma transfer_numeral [transfer_rule]:

by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def)

lemma float_neg_numeral[simp]:
by simp

lemma transfer_neg_numeral [transfer_rule]:

by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def)

lemma float_of_numeral:
and float_of_neg_numeral:
unfolding real_of_float_eq by simp_all

subsection

instantiation float :: exhaustive
begin

definition exhaustive_float where

instance ..

end

definition (in term_syntax) [code_unfold]:

instantiation float :: full_exhaustive
begin

definition

instance ..

end

instantiation float :: random
begin

definition

instance ..

end

subsection

lemma int_induct_abs[case_names less]:
fixes j :: int
assumes H:
shows
proof (induct  arbitrary: j rule: less_induct)
case less
show ?case by (rule H[OF less]) simp
qed

lemma int_cancel_factors:
fixes n :: int
assumes
shows
proof (induct n rule: int_induct_abs)
case (less n)
have  if   for m
proof -
from that have
from less[OF this] that show ?thesis by auto
qed
then show ?case
by (metis dvd_def monoid_mult_class.mult.right_neutral mult.commute power_0)
qed

lemma mult_powr_eq_mult_powr_iff_asym:
fixes m1 m2 e1 e2 :: int
assumes m1:
and
shows
(is )
proof
show ?rhs if eq: ?lhs
proof -
have
using m1 unfolding dvd_def by auto
from  eq have
also have
finally have m1_eq:
by linarith
with m1 have
by (cases ) (auto simp add: dvd_def)
then show ?thesis
using eq  by (simp add: powr_inj)
qed
show ?lhs if ?rhs
using that by simp
qed

lemma mult_powr_eq_mult_powr_iff:

for m1 m2 e1 e2 :: int
using mult_powr_eq_mult_powr_iff_asym[of m1 e1 e2 m2]
using mult_powr_eq_mult_powr_iff_asym[of m2 e2 e1 m1]
by (cases e1 e2 rule: linorder_le_cases) auto

lemma floatE_normed:
assumes x:
obtains (zero)
| (powr) m e :: int where
proof -
have  if
proof -
from x obtain m e :: int where x:
by (auto simp: float_def)
with  int_cancel_factors[of 2 m] obtain k i where
by auto
with  x show ?thesis
apply (rule_tac exI[of _ ])
apply (rule_tac exI[of _ ])
done
qed
with that show thesis by blast
qed

lemma float_normed_cases:
fixes f :: float
obtains (zero)
| (powr) m e :: int where
proof (atomize_elim, induct f)
case (float_of y)
then show ?case
by (cases rule: floatE_normed) (auto simp: zero_float_def)
qed

definition mantissa ::
where

definition exponent ::
where

lemma exponent_0[simp]:  (is ?E)
and mantissa_0[simp]:  (is ?M)
proof -
have
by auto
then show ?E ?M
by (auto simp add: mantissa_def exponent_def zero_float_def)
qed

lemma mantissa_exponent:  (is ?E)
and mantissa_not_dvd:  (is )
proof cases
assume [simp]:
have
proof (cases f rule: float_normed_cases)
case zero
then show ?thesis by simp
next
case (powr m e)
then have
by auto
then show ?thesis
unfolding exponent_def mantissa_def
by (rule someI2_ex) simp
qed
then show ?E ?D by auto
qed simp

lemma mantissa_noteq_0:
using mantissa_not_dvd[of f] by auto

lemma mantissa_eq_zero_iff:
(is )
proof
show ?rhs if ?lhs
proof -
from that have z:
using mantissa_exponent by simp
show ?thesis
qed
show ?lhs if ?rhs
using that by simp
qed

lemma mantissa_pos_iff:
by (auto simp: mantissa_exponent sign_simps)

lemma mantissa_nonneg_iff:
by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)

lemma mantissa_neg_iff:
by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)

lemma
fixes m e :: int
defines
assumes dvd:
shows mantissa_float:  (is )
and exponent_float:  (is )
proof cases
assume
with dvd show  by auto
next
assume
then have f_not_0:  by (simp add: f_def zero_float_def)
from mantissa_exponent[of f] have
then show ?M ?E
using mantissa_not_dvd[OF f_not_0] dvd
by (auto simp: mult_powr_eq_mult_powr_iff)
qed

subsection

lemma Float_mantissa_exponent:
unfolding real_of_float_eq mantissa_exponent[of f] by simp

lemma Float_cases [cases type: float]:
fixes f :: float
obtains (Float) m e :: int where
using Float_mantissa_exponent[symmetric]
by (atomize_elim) auto

lemma denormalize_shift:
assumes f_def:
and not_0:
obtains i where
proof
from mantissa_exponent[of f] f_def
have
by simp
then have eq:
moreover
have
proof (rule ccontr)
assume
then have pos:  by simp
then have
by simp
also have
using pos by (simp flip: powr_realpow add: powr_diff)
finally have
using eq by simp
then have
by linarith
with  have
apply (intro dvdI[where k=])
apply (cases )
apply auto
done
then show False using mantissa_not_dvd[OF not_0] by simp
qed
ultimately have
by (simp flip: powr_realpow)
with
show
by linarith
show
using  by auto
qed

context
begin

qualified lemma compute_float_zero[code_unfold, code]:
by transfer simp

qualified lemma compute_float_one[code_unfold, code]:
by transfer simp

lift_definition normfloat ::  is  .
lemma normloat_id[simp]:  by transfer rule

qualified lemma compute_normfloat[code]:

qualified lemma compute_float_numeral[code_abbrev]:
by transfer simp

qualified lemma compute_float_neg_numeral[code_abbrev]:
by transfer simp

qualified lemma compute_float_uminus[code]:
by transfer simp

qualified lemma compute_float_times[code]:

qualified lemma compute_float_plus[code]:

by transfer (simp add: field_simps powr_realpow[symmetric] powr_diff)

qualified lemma compute_float_minus[code]:  for f g :: float
by simp

qualified lemma compute_float_sgn[code]:

lift_definition is_float_pos ::  is  .

qualified lemma compute_is_float_pos[code]:
by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])

lift_definition is_float_nonneg ::  is  .

qualified lemma compute_is_float_nonneg[code]:
by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])

lift_definition is_float_zero ::   is  .

qualified lemma compute_is_float_zero[code]:
by transfer (auto simp add: is_float_zero_def)

qualified lemma compute_float_abs[code]:

qualified lemma compute_float_eq[code]:
by transfer simp

end

subsection

lemmas real_of_ints =
of_int_minus
of_int_diff
of_int_mult
of_int_power
of_int_numeral of_int_neg_numeral

lemmas int_of_reals = real_of_ints[symmetric]

subsection

definition round_down ::
where

definition round_up ::
where

lemma round_down_float[simp]:
unfolding round_down_def
by (auto intro!: times_float simp flip: of_int_minus)

lemma round_up_float[simp]:
unfolding round_up_def
by (auto intro!: times_float simp flip: of_int_minus)

lemma round_up:
by (simp add: powr_minus_divide le_divide_eq round_up_def ceiling_correct)

lemma round_down:
by (simp add: powr_minus_divide divide_le_eq round_down_def)

lemma round_up_0[simp]:
unfolding round_up_def by simp

lemma round_down_0[simp]:
unfolding round_down_def by simp

lemma round_up_diff_round_down:
proof -
have
by (simp add: round_up_def round_down_def field_simps)
also have
by (rule mult_mono)
(auto simp flip: of_int_diff simp: ceiling_diff_floor_le_1)
finally show ?thesis by simp
qed

lemma round_down_shift:
unfolding round_down_def

lemma round_up_shift:
unfolding round_up_def

lemma round_up_uminus_eq:
and round_down_uminus_eq:
by (auto simp: round_up_def round_down_def ceiling_def)

lemma round_up_mono:
by (auto intro!: ceiling_mono simp: round_up_def)

lemma round_up_le1:
assumes
shows
proof -
have
using assms by (auto intro!: ceiling_mono)
also have  using assms by (auto simp: powr_int intro!: exI[where x=])
finally show ?thesis
qed

lemma round_up_less1:
assumes
shows
proof -
have
using assms by simp
also have  using
by (auto simp: powr_diff powr_int field_simps self_le_power)
finally show ?thesis using
by (simp add: round_up_def field_simps powr_minus powr_int ceiling_less_iff)
qed

lemma round_down_ge1:
assumes x:
assumes prec:
shows
proof cases
assume nonneg:
have
using nonneg by (auto simp: powr_int)
also have
using assms by (auto intro!: floor_mono)
finally show ?thesis
next
assume neg:
have
using x by simp
also have
using prec by auto
finally have x_le:  .

from neg have
by (intro powr_mono) auto
also have  by simp
also have
unfolding of_int_le_iff
using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
finally show ?thesis
using prec x
by (simp add: round_down_def powr_minus_divide pos_le_divide_eq)
qed

lemma round_up_le0:
unfolding round_up_def
by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)

subsection

definition div_twopow ::
where [simp]:

definition mod_twopow ::
where [simp]:

lemma compute_div_twopow[code]:

by (cases n) (auto simp: zdiv_zmult2_eq div_eq_minus1)

lemma compute_mod_twopow[code]:

by (cases n) (auto simp: zmod_zmult2_eq)

lift_definition float_up ::  is round_up by simp
declare float_up.rep_eq[simp]

lemma round_up_correct:
unfolding atLeastAtMost_iff
proof
have
using round_down by simp
also have
using round_up_diff_round_down by simp
finally show
by simp

lemma float_up_correct:
by transfer (rule round_up_correct)

lift_definition float_down ::  is round_down by simp
declare float_down.rep_eq[simp]

lemma round_down_correct:
unfolding atLeastAtMost_iff
proof
have
using round_up by simp
also have
using round_up_diff_round_down by simp
finally show
by simp

lemma float_down_correct:
by transfer (rule round_down_correct)

context
begin

qualified lemma compute_float_down[code]:

proof (cases )
case True
then have
using powr_realpow[of 2 ] by simp
also have
finally show ?thesis
using
apply transfer
apply (simp add: ac_simps round_down_def flip: floor_divide_of_int_eq)
proof -
fix pa :: int and ea :: int and ma :: int
assume a1:
assume
have
then show
qed
next
case False
then have r:
by simp
have r:
by (auto intro: exI[where x=]
with  show ?thesis
qed

lemma abs_round_down_le:
using round_down_correct[of f e] by simp

lemma abs_round_up_le:
using round_up_correct[of e f] by simp

lemma round_down_nonneg:
by (auto simp: round_down_def)

lemma ceil_divide_floor_conv:
assumes
shows
proof (cases )
case True
then show ?thesis
by (simp add: ceiling_def floor_divide_of_int_eq dvd_neg_div
flip: of_int_minus divide_minus_left)
next
case False
then have
by auto
then have ne:
using  by auto
have
apply (rule ceiling_eq)
apply (auto simp flip: floor_divide_of_int_eq)
proof -
have
by simp
moreover have
apply (subst (2) real_of_int_div_aux)
unfolding floor_divide_of_int_eq
using ne  apply auto
done
ultimately show  by arith
qed
then show ?thesis
using  by simp
qed

qualified lemma compute_float_up[code]:

end

lemma bitlen_Float:
fixes m e
defines [THEN meta_eq_to_obj_eq]:
shows
proof (cases )
case True
then show ?thesis by (simp add: f_def bitlen_alt_def)
next
case False
then have
unfolding real_of_float_eq by (simp add: f_def)
then have
moreover
obtain i where
by (rule f_def[THEN denormalize_shift, OF ])
ultimately show ?thesis by (simp add: abs_mult)
qed

lemma float_gt1_scale:
assumes
shows
proof -
have  using assms by auto
then have  using powr_gt_zero[of 2 e]
by (auto simp: zero_less_mult_iff)
then have  by auto
show ?thesis
proof (cases )
case True
then show ?thesis
next
case False
have  by simp
let ?S =
have
using assms False powr_realpow[of 2 ]
by (auto simp: powr_minus field_simps)
then have
using assms False powr_realpow[of 2 ]
by (auto simp: powr_minus)
then have
by (rule mult_right_mono) auto
then have
unfolding mult.assoc by auto
then have
unfolding of_int_le_iff[symmetric] by auto
from this bitlen_bounds[OF , THEN conjunct2]
have
unfolding power_strict_increasing_iff[OF , symmetric]
by (rule order_le_less_trans)
then have
using False by auto
then show ?thesis
by auto
qed
qed

subsection

definition truncate_down::
where

lemma truncate_down:
using round_down by (simp add: truncate_down_def)

lemma truncate_down_le:
by (rule order_trans[OF truncate_down])

lemma truncate_down_zero[simp]:

lemma truncate_down_float[simp]:
by (auto simp: truncate_down_def)

definition truncate_up::
where

lemma truncate_up:
using round_up by (simp add: truncate_up_def)

lemma truncate_up_le:
by (rule order_trans[OF _ truncate_up])

lemma truncate_up_zero[simp]:

lemma truncate_up_uminus_eq:
and truncate_down_uminus_eq:
by (auto simp: truncate_up_def round_up_def truncate_down_def round_down_def ceiling_def)

lemma truncate_up_float[simp]:
by (auto simp: truncate_up_def)

lemma mult_powr_eq:

lemma truncate_down_pos:
assumes
shows
proof -
have
with assms
show ?thesis
apply (auto simp: truncate_down_def round_down_def mult_powr_eq
intro!: ge_one_powr_ge_zero mult_pos_pos)
by linarith
qed

lemma truncate_down_nonneg:
by (auto simp: truncate_down_def round_down_def)

lemma truncate_down_ge1:
apply (auto simp: truncate_down_def algebra_simps intro!: round_down_ge1)
apply linarith
done

lemma truncate_up_nonpos:
by (auto simp: truncate_up_def round_up_def intro!: mult_nonpos_nonneg)

lemma truncate_up_le1:
assumes
shows
proof -
consider  |
by arith
then show ?thesis
proof cases
case 1
with truncate_up_nonpos[OF this, of p] show ?thesis
by simp
next
case 2
then have le:
using assms by (auto simp: log_less_iff)
from assms have  by simp
show ?thesis
qed
qed

lemma truncate_down_shift_int:

by (cases )
(simp_all add: algebra_simps abs_mult log_mult truncate_down_def
round_down_shift[of _ _ k, simplified])

lemma truncate_down_shift_nat:
by (metis of_int_of_nat_eq truncate_down_shift_int)

lemma truncate_up_shift_int:
by (cases )
(simp_all add: algebra_simps abs_mult log_mult truncate_up_def
round_up_shift[of _ _ k, simplified])

lemma truncate_up_shift_nat:
by (metis of_int_of_nat_eq truncate_up_shift_int)

subsection

lift_definition float_round_up ::  is truncate_up

lemma float_round_up:
using truncate_up by transfer simp

lemma float_round_up_zero[simp]:
by transfer simp

lift_definition float_round_down ::  is truncate_down

lemma float_round_down:
using truncate_down by transfer simp

lemma float_round_down_zero[simp]:
by transfer simp

lemmas float_round_up_le = order_trans[OF _ float_round_up]
and float_round_down_le = order_trans[OF float_round_down]

lemma minus_float_round_up_eq:
and minus_float_round_down_eq:
by (transfer; simp add: truncate_down_uminus_eq truncate_up_uminus_eq)+

context
begin

qualified lemma compute_float_round_down[code]:

using Float.compute_float_down[of  m e, symmetric]
by transfer
(simp add: field_simps abs_mult log_mult bitlen_alt_def truncate_down_def
cong del: if_weak_cong)

qualified lemma compute_float_round_up[code]:

end

subsection

lemma div_mult_twopow_eq:  for a b :: nat
by (cases ) (simp_all add: div_mult2_eq[symmetric] ac_simps)

lemma real_div_nat_eq_floor_of_divide:  for a b :: nat
by (simp add: floor_divide_of_nat_eq [of a b])

definition

lemma floor_log_divide_eq:
assumes
shows
proof -
let ?l =
let ?fl =
have  using assms
by (auto simp: log_divide)
also have
(is )
also note
note powr = powr_le_cancel_iff[symmetric, OF , THEN iffD2]
note powr_strict = powr_less_cancel_iff[symmetric, OF , THEN iffD2]
have  (is )
using assms
by (linarith |
auto
intro!: floor_eq2
intro: powr_strict powr
finally
show ?thesis by simp
qed

lemma truncate_down_rat_precision:

and truncate_up_rat_precision:

unfolding truncate_down_def truncate_up_def rat_precision_def
by (cases x; cases y) (auto simp: floor_log_divide_eq algebra_simps bitlen_alt_def)

lift_definition lapprox_posrat ::
is
by simp

context
begin

qualified lemma compute_lapprox_posrat[code]:

unfolding div_mult_twopow_eq
by transfer
(simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def
truncate_down_rat_precision del: two_powr_minus_int_float)

end

lift_definition rapprox_posrat ::
is
by simp

context
begin

qualified lemma compute_rapprox_posrat[code]:
fixes prec x y
defines
shows
proof (cases )
assume
then show ?thesis by transfer simp
next
assume
show ?thesis
proof (cases )
case True
define x' where
have
moreover have
by (simp flip: powr_realpow add:  x'_def)
ultimately show ?thesis
using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 ]
l_def[symmetric, THEN meta_eq_to_obj_eq]
apply transfer
apply (auto simp add: round_up_def truncate_up_rat_precision)
apply (metis dvd_triv_left of_nat_dvd_iff)
apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
done
next
case False
define y' where
from  have  by (simp add: y'_def)
have
moreover have
using  by (simp flip: powr_realpow add: powr_minus y'_def field_simps)
ultimately show ?thesis
using ceil_divide_floor_conv[of y' x]
l_def[symmetric, THEN meta_eq_to_obj_eq]
apply transfer
apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision)
apply (metis dvd_triv_left of_nat_dvd_iff)
apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
done
qed
qed

end

lemma rat_precision_pos:
assumes
and
and
shows
proof -
have
then have
using assms
then show ?thesis
using assms
qed

lemma rapprox_posrat_less1:

by transfer (simp add: rat_precision_pos round_up_less1 truncate_up_rat_precision)

lift_definition lapprox_rat ::  is

by simp

context
begin

qualified lemma compute_lapprox_rat[code]:

lift_definition rapprox_rat ::  is

by simp

lemma
by transfer auto

lemma
by transfer auto

qualified lemma compute_rapprox_rat[code]:

qualified lemma compute_truncate_down[code]:

by transfer (auto split: prod.split simp: of_rat_divide dest!: quotient_of_div)

qualified lemma compute_truncate_up[code]:

by transfer (auto split: prod.split simp:  of_rat_divide dest!: quotient_of_div)

end

subsection

definition

definition

lift_definition float_divl ::  is real_divl

context
begin

qualified lemma compute_float_divl[code]:

apply transfer
unfolding real_divl_def of_int_1 mult_1 truncate_down_shift_int[symmetric]
done

lift_definition float_divr ::  is real_divr

qualified lemma compute_float_divr[code]:

by transfer (simp add: real_divr_def real_divl_def truncate_down_uminus_eq)

end

subsection

lemma div2_less_self[termination_simp]:  for n :: nat

fun power_down ::
where

|

fun power_up ::
where

|

lift_definition power_up_fl ::  is power_up
by (induct_tac rule: power_up.induct) simp_all

lift_definition power_down_fl ::  is power_down
by (induct_tac rule: power_down.induct) simp_all

lemma power_float_transfer[transfer_rule]:

unfolding power_def
by transfer_prover

lemma compute_power_up_fl[code]:

and compute_power_down_fl[code]:

unfolding atomize_conj by transfer simp

lemma power_down_pos:
by (induct p x n rule: power_down.induct)
(auto simp del: odd_Suc_div_two intro!: truncate_down_pos)

lemma power_down_nonneg:
by (induct p x n rule: power_down.induct)
(auto simp del: odd_Suc_div_two intro!: truncate_down_nonneg mult_nonneg_nonneg)

lemma power_down:
proof (induct p x n rule: power_down.induct)
case (2 p x n)
have ?case if
proof -
from that 2 have
by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
also have
by (simp flip: power_mult)
also have
using  by presburger
finally show ?thesis
using that by (auto intro!: truncate_down_le simp del: odd_Suc_div_two)
qed
then show ?case
by (auto intro!: truncate_down_le mult_left_mono 2 mult_nonneg_nonneg power_down_nonneg)
qed simp

lemma power_up:
proof (induct p x n rule: power_up.induct)
case (2 p x n)
have ?case if
proof -
from that even_Suc have
by presburger
then have
by (simp flip: power_mult)
also from that 2 have
by (auto intro: power_mono simp del: odd_Suc_div_two)
finally show ?thesis
using that by (auto intro!: truncate_up_le simp del: odd_Suc_div_two)
qed
then show ?case
by (auto intro!: truncate_up_le mult_left_mono 2)
qed simp

lemmas power_up_le = order_trans[OF _ power_up]
and power_up_less = less_le_trans[OF _ power_up]
and power_down_le = order_trans[OF power_down]

lemma power_down_fl:
by transfer (rule power_down)

lemma power_up_fl:
by transfer (rule power_up)

lemma real_power_up_fl:
by transfer simp

lemma real_power_down_fl:
by transfer simp

subsection

definition

definition

lemma float_plus_down_float[intro, simp]:

lemma float_plus_up_float[intro, simp]:

lift_definition float_plus_down ::  is plus_down ..

lift_definition float_plus_up ::  is plus_up ..

lemma plus_down:
and plus_up:
by (auto simp: plus_down_def truncate_down plus_up_def truncate_up)

lemma float_plus_down:
and float_plus_up:
by (transfer; rule plus_down plus_up)+

lemmas plus_down_le = order_trans[OF plus_down]
and plus_up_le = order_trans[OF _ plus_up]
and float_plus_down_le = order_trans[OF float_plus_down]
and float_plus_up_le = order_trans[OF _ float_plus_up]

lemma compute_plus_up[code]:
using truncate_down_uminus_eq[of p ]
by (auto simp: plus_down_def plus_up_def)

lemma truncate_down_log2_eqI:
assumes
assumes
shows
using assms by (auto simp: truncate_down_def round_down_def)

lemma sum_neq_zeroI:

for a k :: real
by auto

lemma abs_real_le_2_powr_bitlen[simp]:
proof (cases )
case True
then show ?thesis by simp
next
case False
then have
using bitlen_bounds[of ]
then show ?thesis
by (metis bitlen_nonneg powr_int of_int_abs of_int_less_numeral_power_cancel_iff
zero_less_numeral)
qed

lemma floor_sum_times_2_powr_sgn_eq:
fixes ai p q :: int
and a b :: real
assumes
and b_le_1:
and leqp:
shows
proof -
consider  |  |  by arith
then show ?thesis
proof cases
case 1
then show ?thesis
next
case 2
then have
by simp
also note b_le_1
finally have b_less_1:  .

from b_less_1  have floor_eq:

have
also have
also have
using assms
also have
by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
finally have  .
moreover
have
proof -
have
by (subst powr_diff) (simp add: field_simps)
also have
using leqp by (simp flip: powr_realpow add: powr_diff)
also have
by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
finally show ?thesis .
qed
ultimately show ?thesis by simp
next
case 3
then have floor_eq:
using b_le_1
by (auto simp: floor_eq_iff algebra_simps pos_divide_le_eq[symmetric] abs_if divide_powr_uminus
intro!: mult_neg_pos split: if_split_asm)
have
also have
also have
using assms by (simp add: algebra_simps powr_mult_base divide_powr_uminus)
also have
using assms by (simp add: algebra_simps flip: powr_realpow)
also have
using  assms
by (simp add: floor_divide_of_int_eq floor_eq floor_divide_real_eq_div
del: of_int_mult of_int_power of_int_diff)
also have
using assms by (simp add: algebra_simps divide_powr_uminus flip: powr_realpow)
finally show ?thesis
using  by simp
qed
qed

fixes ai :: int
and b :: real
assumes
and
shows
proof (cases )
case True
then show ?thesis by simp
next
case False
define k where
then have
by simp
then have k:
have
using assms by (auto simp: k_def)
define r where
have r:
using  k
by (auto simp: r_def k_def algebra_simps powr_add abs_if powr_int)
then have
using  by (auto simp: powr_int)
from this[simplified of_int_le_iff[symmetric]]
have r_le:
by (auto simp: algebra_simps powr_int)

have
using  by (auto simp: k_def r_def simp flip: powr_realpow)

have pos:  for b :: real
using
by (auto simp add: r_def powr_realpow[symmetric] abs_if sgn_if algebra_simps
split: if_split_asm)
have less:
and less':
using  by (auto simp: abs_if sgn_if split: if_split_asm)

have floor_eq:
using  r r_le
by (auto simp: floor_log_eq_powr_iff powr_minus_divide field_simps sgn_if)

from  have
using   r
by (auto simp add: sgn_if abs_if)
also have
proof -
have
also have
using pos[OF less]
by (subst log_mult) (simp_all add: log_mult powr_mult field_simps)
also
let ?if =
have
using
by (intro floor_eq) (auto simp: abs_mult sgn_if)
also
have
by (subst floor_eq) (auto simp: sgn_if)
also have
using pos[OF less']
also have
finally show ?thesis .
qed
also have
unfolding [symmetric] using
by (auto simp: abs_if sgn_if algebra_simps)
finally show ?thesis .
qed

context
begin

qualified lemma compute_far_float_plus_down:
fixes m1 e1 m2 e2 :: int
and p :: nat
defines
assumes H:
shows
proof -
let ?a =
let ?b =
let ?sum =
let ?shift =
let ?m1 =
let ?m2 =
let ?m2' =
let ?e =

have sum_eq:
by (auto simp flip: powr_add powr_mult powr_realpow simp: powr_mult_base algebra_simps)

have
by (auto simp: field_simps powr_add powr_mult_base powr_diff abs_mult)
also have
using H by (intro powr_mono) auto
finally have abs_m2_less_half:
by simp

then have
unfolding powr_minus_divide by (auto simp: bitlen_alt_def field_simps powr_mult_base abs_mult)
also have
by simp
finally have b_less_quarter:
also have  using  by simp
finally have b_less_half_a:
by (simp add: algebra_simps powr_mult_base abs_mult)
then have a_half_less_sum:
by (auto simp: field_simps abs_if split: if_split_asm)

from b_less_half_a have
by simp_all

have
using
by (auto simp: powr_add powr_int bitlen_nonneg divide_right_mono abs_mult)
then have  using b_less_quarter
by (rule sum_neq_zeroI)
then have
unfolding sum_eq by (simp add: abs_mult zero_less_mult_iff)

have
using   by (auto simp: sgn_if less_1_mult abs_mult simp del: power.simps)
then have sum'_nz:
by (intro sum_neq_zeroI)

have
using
by (simp add: abs_mult log_mult) linarith
also have
using abs_m2_less_half
by (intro log2_abs_int_add_less_half_sgn_eq) (auto simp: abs_mult)
also have
by (auto simp: sgn_if zero_less_mult_iff less_not_sym)
also
have
by (auto simp: field_simps powr_minus[symmetric] powr_diff powr_mult_base)
then have
using
finally
have  .
then have
unfolding plus_down_def
proof (rule truncate_down_log2_eqI)
let ?f =
let ?ai =
have
proof (rule floor_sum_times_2_powr_sgn_eq)
show
show
using abs_m2_less_half
next
have
using
also have
using a_half_less_sum
unfolding floor_diff_of_int[symmetric]
by (auto simp add: log_minus_eq_powr powr_minus_divide intro!: floor_mono)
finally
have
by (auto simp: algebra_simps bitlen_alt_def )
also have
using bitlen_nonneg[of ] by (simp add: k1_def)
finally show  by simp
qed
also have
using powr_gt_zero[of 2 e2]
by (auto simp add: sgn_if zero_less_mult_iff simp del: powr_gt_zero)
also have
finally
show  .
qed
then show ?thesis
by transfer (simp add: plus_down_def ac_simps Let_def)
qed

lemma compute_float_plus_down_naive[code]:
by transfer (auto simp: plus_down_def)

qualified lemma compute_float_plus_down[code]:
fixes p::nat and m1 e1 m2 e2::int
shows
proof -
{
assume
note compute_far_float_plus_down[OF this]
}
then show ?thesis
by transfer (simp add: Let_def plus_down_def ac_simps)
qed

qualified lemma compute_float_plus_up[code]:
using truncate_down_uminus_eq[of p ]
by transfer (simp add: plus_down_def plus_up_def ac_simps)

lemma mantissa_zero[simp]:
by (metis mantissa_0 zero_float.abs_eq)

qualified lemma compute_float_less[code]:
using truncate_down[of 0 ] truncate_down_pos[of  0]
by transfer (auto simp: plus_down_def)

qualified lemma compute_float_le[code]:
using truncate_down[of 0 ] truncate_down_nonneg[of  0]
by transfer (auto simp: plus_down_def)

end

subsection

lemma Float_num[simp]:

using two_powr_int_float[of 2] two_powr_int_float[of ] two_powr_int_float[of ]
two_powr_int_float[of ]
using powr_realpow[of 2 2] powr_realpow[of 2 3]
using powr_minus[of  1] powr_minus[of  2] powr_minus[of  3]
by auto

lemma real_of_Float_int[simp]:
by simp

lemma float_zero[simp]:
by simp

lemma abs_div_2_less:
by arith

lemma lapprox_rat:

lemma mult_div_le:
fixes a b :: int
assumes
shows
proof -
from minus_div_mult_eq_mod [symmetric, of a b] have
by simp
also have
apply (rule pos_mod_sign)
using assms
apply simp
done
finally show ?thesis
by simp
qed

lemma lapprox_rat_nonneg:
assumes  and
shows
using assms

lemma rapprox_rat:

lemma rapprox_rat_le1:
assumes
shows
using assms

lemma rapprox_rat_nonneg_nonpos:
by transfer (simp add: truncate_up_nonpos divide_nonneg_nonpos)

lemma rapprox_rat_nonpos_nonneg:
by transfer (simp add: truncate_up_nonpos divide_nonpos_nonneg)

lemma real_divl:

lemma real_divr:

lemma float_divl:
by transfer (rule real_divl)

lemma real_divl_lower_bound:

lemma float_divl_lower_bound:
by transfer (rule real_divl_lower_bound)

lemma exponent_1:
using exponent_float[of 1 0] by (simp add: one_float_def)

lemma mantissa_1:
using mantissa_float[of 1 0] by (simp add: one_float_def)

lemma bitlen_1:

lemma float_upper_bound:
proof (cases )
case True
then show ?thesis by simp
next
case False
then have
using mantissa_eq_zero_iff by auto
have
by (rule mantissa_exponent)
also have
by simp
also have
using bitlen_bounds[of ] bitlen_nonneg
by (auto simp del: of_int_abs simp add: powr_int)
qed

lemma real_divl_pos_less1_bound:
assumes
shows
using assms
by (auto intro!: truncate_down_ge1 simp: real_divl_def)

lemma float_divl_pos_less1_bound:

by transfer (rule real_divl_pos_less1_bound)

lemma float_divr:
by transfer (rule real_divr)

lemma real_divr_pos_less1_lower_bound:
assumes
and
shows
proof -
have
using  and  by auto
also have
using real_divr[where x = 1 and y = x] by auto
finally show ?thesis by auto
qed

lemma float_divr_pos_less1_lower_bound:
by transfer (rule real_divr_pos_less1_lower_bound)

lemma real_divr_nonpos_pos_upper_bound:
by (simp add: real_divr_def truncate_up_nonpos divide_le_0_iff)

lemma float_divr_nonpos_pos_upper_bound:

by transfer (rule real_divr_nonpos_pos_upper_bound)

lemma real_divr_nonneg_neg_upper_bound:
by (simp add: real_divr_def truncate_up_nonpos divide_le_0_iff)

lemma float_divr_nonneg_neg_upper_bound:

by transfer (rule real_divr_nonneg_neg_upper_bound)

lemma truncate_up_nonneg_mono:
assumes
shows
proof -
consider  |   |
by arith
then show ?thesis
proof cases
case 1
then show ?thesis
using assms
by (auto simp: truncate_up_def round_up_def intro!: ceiling_mono)
next
case 2
from assms  have
by auto
with
have logless:  and flogless:
by (metis floor_less_cancel linorder_cases not_le)+
have
using assms by (simp add: truncate_up_def round_up_def)
also have
proof (simp only: ceiling_le_iff)
have
by (auto simp: algebra_simps simp flip: powr_diff intro!: mult_left_mono)
then show
qed
then have
(metis power_Suc of_int_le_numeral_power_cancel_iff)
also
have
using logless flogless by (auto intro!: floor_mono)
also have
using assms
by (auto simp: algebra_simps)
finally have
by simp
also have
also have
using  assms
also have
by (rule truncate_up)
finally show ?thesis .
next
case 3
then show ?thesis
using assms
by (auto intro!: truncate_up_le)
qed
qed

lemma truncate_up_switch_sign_mono:
assumes
shows
proof -
note truncate_up_nonpos[OF ]
also note truncate_up_le[OF ]
finally show ?thesis .
qed

lemma truncate_down_switch_sign_mono:
assumes
and
and
shows
proof -
note truncate_down_le[OF ]
also note truncate_down_nonneg[OF ]
finally show ?thesis .
qed

lemma truncate_down_nonneg_mono:
assumes
shows
proof -
consider  |  |

by arith
then show ?thesis
proof cases
case 1
with assms have   by simp_all
then show ?thesis
by (auto intro!: truncate_down_nonneg)
next
case 2
then show ?thesis
using assms
by (auto simp: truncate_down_def round_down_def intro!: floor_mono)
next
case 3
from  have
using assms by auto
with
have logless:  and flogless:
unfolding atomize_conj abs_of_pos[OF ] abs_of_pos[OF ]
by (metis floor_less_cancel linorder_cases not_le)
have
using  by simp
also have
using   assms(2)
by (auto intro!: powr_mono divide_left_mono
also have
finally have
using
by (auto simp: powr_diff le_floor_iff powr_realpow powr_add)
then have
by (auto simp: truncate_down_def round_down_def)
moreover have
proof -
have  using  by simp
also have
by (auto simp flip: powr_realpow powr_add simp: algebra_simps powr_mult_base le_powr_iff)
also
have
using logless flogless
by (auto intro!: floor_mono)
finally show ?thesis
by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
qed
ultimately show ?thesis
by (metis dual_order.trans truncate_down)
qed
qed

lemma truncate_down_eq_truncate_up:
and truncate_up_eq_truncate_down:
by (auto simp: truncate_up_uminus_eq truncate_down_uminus_eq)

lemma truncate_down_mono:
apply (cases )
apply (rule truncate_down_nonneg_mono, assumption+)
apply (cases )
apply (auto intro: truncate_up_nonneg_mono truncate_up_switch_sign_mono)
done

lemma truncate_up_mono:

lemma Float_le_zero_iff:
by (auto simp: zero_float_def mult_le_0_iff)

lemma real_of_float_pprt[simp]:
fixes a :: float
shows
unfolding pprt_def sup_float_def max_def sup_real_def by auto

lemma real_of_float_nprt[simp]:
fixes a :: float
shows
unfolding nprt_def inf_float_def min_def inf_real_def by auto

context
begin

lift_definition int_floor_fl ::  is floor .

qualified lemma compute_int_floor_fl[code]:

apply transfer
apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power floor_of_int of_int_mult)
done

lift_definition floor_fl ::  is
by simp

qualified lemma compute_floor_fl[code]:

apply transfer
apply (metis (no_types, hide_lams)floor_divide_of_int_eq of_int_numeral of_int_power of_int_mult)
done

end

lemma floor_fl:
by transfer simp

lemma int_floor_fl:
by transfer simp

lemma floor_pos_exp:
proof (cases )
case True
then show ?thesis
next
case False
have eq:
by transfer simp
obtain i where
by (rule denormalize_shift[OF eq False])
then show ?thesis
by simp
qed

lemma compute_mantissa[code]:

by (auto simp: mantissa_float Float.abs_eq simp flip: zero_float_def)

lemma compute_exponent[code]:

by (auto simp: exponent_float Float.abs_eq simp flip: zero_float_def)

lifting_update Float.float.lifting
lifting_forget Float.float.lifting

end