src/HOL/Library/Float.thy
 author immler Wed Nov 12 17:37:43 2014 +0100 (2014-11-12) changeset 58987 119680ebf37c parent 58985 bf498e0af9e3 child 58989 99831590def5 permissions -rw-r--r--
quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}
1 (*  Title:      HOL/Library/Float.thy
2     Author:     Johannes Hölzl, Fabian Immler
3     Copyright   2012  TU München
4 *)
6 section {* Floating-Point Numbers *}
8 theory Float
9 imports Complex_Main Lattice_Algebras
10 begin
12 definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
14 typedef float = float
15   morphisms real_of_float float_of
16   unfolding float_def by auto
18 instantiation float :: real_of
19 begin
21 definition real_float :: "float \<Rightarrow> real" where
22   real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
24 instance ..
25 end
27 lemma type_definition_float': "type_definition real float_of float"
28   using type_definition_float unfolding real_of_float_def .
30 setup_lifting (no_code) type_definition_float'
32 lemmas float_of_inject[simp]
34 declare [[coercion "real :: float \<Rightarrow> real"]]
36 lemma real_of_float_eq:
37   fixes f1 f2 :: float shows "f1 = f2 \<longleftrightarrow> real f1 = real f2"
38   unfolding real_of_float_def real_of_float_inject ..
40 lemma float_of_real[simp]: "float_of (real x) = x"
41   unfolding real_of_float_def by (rule real_of_float_inverse)
43 lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x"
44   unfolding real_of_float_def by (rule float_of_inverse)
46 subsection {* Real operations preserving the representation as floating point number *}
48 lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
49   by (auto simp: float_def)
51 lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
52 lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
53 lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
54 lemma neg_numeral_float[simp]: "- numeral i \<in> float" by (intro floatI[of "- numeral i" 0]) simp
55 lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
56 lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
57 lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp
58 lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \<in> float" by (intro floatI[of 1 i]) simp
59 lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp
60 lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \<in> float" by (intro floatI[of 1 "-i"]) simp
61 lemma two_powr_numeral_float[simp]: "2 powr numeral i \<in> float" by (intro floatI[of 1 "numeral i"]) simp
62 lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \<in> float" by (intro floatI[of 1 "- numeral i"]) simp
63 lemma two_pow_float[simp]: "2 ^ n \<in> float" by (intro floatI[of 1 "n"]) (simp add: powr_realpow)
64 lemma real_of_float_float[simp]: "real (f::float) \<in> float" by (cases f) simp
66 lemma plus_float[simp]: "r \<in> float \<Longrightarrow> p \<in> float \<Longrightarrow> r + p \<in> float"
67   unfolding float_def
68 proof (safe, simp)
69   fix e1 m1 e2 m2 :: int
70   { fix e1 m1 e2 m2 :: int assume "e1 \<le> e2"
71     then have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
72       by (simp add: powr_realpow[symmetric] powr_divide2[symmetric] field_simps)
73     then have "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e"
74       by blast }
75   note * = this
76   show "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e"
77   proof (cases e1 e2 rule: linorder_le_cases)
78     assume "e2 \<le> e1" from *[OF this, of m2 m1] show ?thesis by (simp add: ac_simps)
79   qed (rule *)
80 qed
82 lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
83   apply (auto simp: float_def)
84   apply hypsubst_thin
85   apply (rule_tac x="-x" in exI)
86   apply (rule_tac x="xa" in exI)
87   apply (simp add: field_simps)
88   done
90 lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
91   apply (auto simp: float_def)
92   apply hypsubst_thin
93   apply (rule_tac x="x * xa" in exI)
94   apply (rule_tac x="xb + xc" in exI)
95   apply (simp add: powr_add)
96   done
98 lemma minus_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x - y \<in> float"
99   using plus_float [of x "- y"] by simp
101 lemma abs_float[simp]: "x \<in> float \<Longrightarrow> abs x \<in> float"
102   by (cases x rule: linorder_cases[of 0]) auto
104 lemma sgn_of_float[simp]: "x \<in> float \<Longrightarrow> sgn x \<in> float"
105   by (cases x rule: linorder_cases[of 0]) (auto intro!: uminus_float)
107 lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
108   apply (auto simp add: float_def)
109   apply hypsubst_thin
110   apply (rule_tac x="x" in exI)
111   apply (rule_tac x="xa - d" in exI)
112   apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
113   done
115 lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
116   apply (auto simp add: float_def)
117   apply hypsubst_thin
118   apply (rule_tac x="x" in exI)
119   apply (rule_tac x="xa - d" in exI)
120   apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
121   done
123 lemma div_numeral_Bit0_float[simp]:
124   assumes x: "x / numeral n \<in> float" shows "x / (numeral (Num.Bit0 n)) \<in> float"
125 proof -
126   have "(x / numeral n) / 2^1 \<in> float"
127     by (intro x div_power_2_float)
128   also have "(x / numeral n) / 2^1 = x / (numeral (Num.Bit0 n))"
129     by (induct n) auto
130   finally show ?thesis .
131 qed
133 lemma div_neg_numeral_Bit0_float[simp]:
134   assumes x: "x / numeral n \<in> float" shows "x / (- numeral (Num.Bit0 n)) \<in> float"
135 proof -
136   have "- (x / numeral (Num.Bit0 n)) \<in> float" using x by simp
137   also have "- (x / numeral (Num.Bit0 n)) = x / - numeral (Num.Bit0 n)"
138     by simp
139   finally show ?thesis .
140 qed
142 lemma power_float[simp]: assumes "a \<in> float" shows "a ^ b \<in> float"
143 proof -
144   from assms obtain m e::int where "a = m * 2 powr e"
145     by (auto simp: float_def)
146   thus ?thesis
147     by (auto intro!: floatI[where m="m^b" and e = "e*b"]
148       simp: power_mult_distrib powr_realpow[symmetric] powr_powr)
149 qed
151 lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
152 declare Float.rep_eq[simp]
154 lemma compute_real_of_float[code]:
155   "real_of_float (Float m e) = (if e \<ge> 0 then m * 2 ^ nat e else m / 2 ^ (nat (-e)))"
156 by (simp add: real_of_float_def[symmetric] powr_int)
158 code_datatype Float
160 subsection {* Arithmetic operations on floating point numbers *}
162 instantiation float :: "{ring_1, linorder, linordered_ring, linordered_idom, numeral, equal}"
163 begin
165 lift_definition zero_float :: float is 0 by simp
166 declare zero_float.rep_eq[simp]
167 lift_definition one_float :: float is 1 by simp
168 declare one_float.rep_eq[simp]
169 lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp
170 declare plus_float.rep_eq[simp]
171 lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp
172 declare times_float.rep_eq[simp]
173 lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp
174 declare minus_float.rep_eq[simp]
175 lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp
176 declare uminus_float.rep_eq[simp]
178 lift_definition abs_float :: "float \<Rightarrow> float" is abs by simp
179 declare abs_float.rep_eq[simp]
180 lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
181 declare sgn_float.rep_eq[simp]
183 lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" .
185 lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" .
186 declare less_eq_float.rep_eq[simp]
187 lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" .
188 declare less_float.rep_eq[simp]
190 instance
191   proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
192 end
194 lemma Float_0_eq_0[simp]: "Float 0 e = 0"
195   by transfer simp
197 lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
198   by (induct n) simp_all
200 lemma fixes x y::float
201   shows real_of_float_min: "real (min x y) = min (real x) (real y)"
202     and real_of_float_max: "real (max x y) = max (real x) (real y)"
203   by (simp_all add: min_def max_def)
205 instance float :: unbounded_dense_linorder
206 proof
207   fix a b :: float
208   show "\<exists>c. a < c"
209     apply (intro exI[of _ "a + 1"])
210     apply transfer
211     apply simp
212     done
213   show "\<exists>c. c < a"
214     apply (intro exI[of _ "a - 1"])
215     apply transfer
216     apply simp
217     done
218   assume "a < b"
219   then show "\<exists>c. a < c \<and> c < b"
220     apply (intro exI[of _ "(a + b) * Float 1 (- 1)"])
221     apply transfer
222     apply (simp add: powr_minus)
223     done
224 qed
226 instantiation float :: lattice_ab_group_add
227 begin
229 definition inf_float::"float\<Rightarrow>float\<Rightarrow>float"
230 where "inf_float a b = min a b"
232 definition sup_float::"float\<Rightarrow>float\<Rightarrow>float"
233 where "sup_float a b = max a b"
235 instance
236   by default
237      (transfer, simp_all add: inf_float_def sup_float_def real_of_float_min real_of_float_max)+
238 end
240 lemma float_numeral[simp]: "real (numeral x :: float) = numeral x"
241   apply (induct x)
242   apply simp
243   apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq real_float
244                   plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
245   done
247 lemma transfer_numeral [transfer_rule]:
248   "rel_fun (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
249   unfolding rel_fun_def float.pcr_cr_eq  cr_float_def by simp
251 lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
252   by simp
254 lemma transfer_neg_numeral [transfer_rule]:
255   "rel_fun (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
256   unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp
258 lemma
259   shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
260     and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
261   unfolding real_of_float_eq by simp_all
263 subsection {* Quickcheck *}
265 instantiation float :: exhaustive
266 begin
268 definition exhaustive_float where
269   "exhaustive_float f d =
270     Quickcheck_Exhaustive.exhaustive (%x. Quickcheck_Exhaustive.exhaustive (%y. f (Float x y)) d) d"
272 instance ..
274 end
276 definition (in term_syntax) [code_unfold]:
277   "valtermify_float x y = Code_Evaluation.valtermify Float {\<cdot>} x {\<cdot>} y"
279 instantiation float :: full_exhaustive
280 begin
282 definition full_exhaustive_float where
283   "full_exhaustive_float f d =
284     Quickcheck_Exhaustive.full_exhaustive
285       (\<lambda>x. Quickcheck_Exhaustive.full_exhaustive (\<lambda>y. f (valtermify_float x y)) d) d"
287 instance ..
289 end
291 instantiation float :: random
292 begin
294 definition "Quickcheck_Random.random i =
295   scomp (Quickcheck_Random.random (2 ^ nat_of_natural i))
296     (\<lambda>man. scomp (Quickcheck_Random.random i) (\<lambda>exp. Pair (valtermify_float man exp)))"
298 instance ..
300 end
303 subsection {* Represent floats as unique mantissa and exponent *}
305 lemma int_induct_abs[case_names less]:
306   fixes j :: int
307   assumes H: "\<And>n. (\<And>i. \<bar>i\<bar> < \<bar>n\<bar> \<Longrightarrow> P i) \<Longrightarrow> P n"
308   shows "P j"
309 proof (induct "nat \<bar>j\<bar>" arbitrary: j rule: less_induct)
310   case less show ?case by (rule H[OF less]) simp
311 qed
313 lemma int_cancel_factors:
314   fixes n :: int assumes "1 < r" shows "n = 0 \<or> (\<exists>k i. n = k * r ^ i \<and> \<not> r dvd k)"
315 proof (induct n rule: int_induct_abs)
316   case (less n)
317   { fix m assume n: "n \<noteq> 0" "n = m * r"
318     then have "\<bar>m \<bar> < \<bar>n\<bar>"
319       by (metis abs_dvd_iff abs_ge_self assms comm_semiring_1_class.normalizing_semiring_rules(7)
320                 dvd_imp_le_int dvd_refl dvd_triv_right linorder_neq_iff linorder_not_le
321                 mult_eq_0_iff zdvd_mult_cancel1)
322     from less[OF this] n have "\<exists>k i. n = k * r ^ Suc i \<and> \<not> r dvd k" by auto }
323   then show ?case
324     by (metis comm_semiring_1_class.normalizing_semiring_rules(12,7) dvdE power_0)
325 qed
327 lemma mult_powr_eq_mult_powr_iff_asym:
328   fixes m1 m2 e1 e2 :: int
329   assumes m1: "\<not> 2 dvd m1" and "e1 \<le> e2"
330   shows "m1 * 2 powr e1 = m2 * 2 powr e2 \<longleftrightarrow> m1 = m2 \<and> e1 = e2"
331 proof
332   have "m1 \<noteq> 0" using m1 unfolding dvd_def by auto
333   assume eq: "m1 * 2 powr e1 = m2 * 2 powr e2"
334   with `e1 \<le> e2` have "m1 = m2 * 2 powr nat (e2 - e1)"
335     by (simp add: powr_divide2[symmetric] field_simps)
336   also have "\<dots> = m2 * 2^nat (e2 - e1)"
337     by (simp add: powr_realpow)
338   finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)"
339     unfolding real_of_int_inject .
340   with m1 have "m1 = m2"
341     by (cases "nat (e2 - e1)") (auto simp add: dvd_def)
342   then show "m1 = m2 \<and> e1 = e2"
343     using eq `m1 \<noteq> 0` by (simp add: powr_inj)
344 qed simp
346 lemma mult_powr_eq_mult_powr_iff:
347   fixes m1 m2 e1 e2 :: int
348   shows "\<not> 2 dvd m1 \<Longrightarrow> \<not> 2 dvd m2 \<Longrightarrow> m1 * 2 powr e1 = m2 * 2 powr e2 \<longleftrightarrow> m1 = m2 \<and> e1 = e2"
349   using mult_powr_eq_mult_powr_iff_asym[of m1 e1 e2 m2]
350   using mult_powr_eq_mult_powr_iff_asym[of m2 e2 e1 m1]
351   by (cases e1 e2 rule: linorder_le_cases) auto
353 lemma floatE_normed:
354   assumes x: "x \<in> float"
355   obtains (zero) "x = 0"
356    | (powr) m e :: int where "x = m * 2 powr e" "\<not> 2 dvd m" "x \<noteq> 0"
357 proof atomize_elim
358   { assume "x \<noteq> 0"
359     from x obtain m e :: int where x: "x = m * 2 powr e" by (auto simp: float_def)
360     with `x \<noteq> 0` int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\<not> 2 dvd k"
361       by auto
362     with `\<not> 2 dvd k` x have "\<exists>(m::int) (e::int). x = m * 2 powr e \<and> \<not> (2::int) dvd m"
363       by (rule_tac exI[of _ "k"], rule_tac exI[of _ "e + int i"])
364          (simp add: powr_add powr_realpow) }
365   then show "x = 0 \<or> (\<exists>(m::int) (e::int). x = m * 2 powr e \<and> \<not> (2::int) dvd m \<and> x \<noteq> 0)"
366     by blast
367 qed
369 lemma float_normed_cases:
370   fixes f :: float
371   obtains (zero) "f = 0"
372    | (powr) m e :: int where "real f = m * 2 powr e" "\<not> 2 dvd m" "f \<noteq> 0"
373 proof (atomize_elim, induct f)
374   case (float_of y) then show ?case
375     by (cases rule: floatE_normed) (auto simp: zero_float_def)
376 qed
378 definition mantissa :: "float \<Rightarrow> int" where
379   "mantissa f = fst (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
380    \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))"
382 definition exponent :: "float \<Rightarrow> int" where
383   "exponent f = snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
384    \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p))"
386 lemma
387   shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
388     and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
389 proof -
390   have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)" by auto
391   then show ?E ?M
392     by (auto simp add: mantissa_def exponent_def zero_float_def)
393 qed
395 lemma
396   shows mantissa_exponent: "real f = mantissa f * 2 powr exponent f" (is ?E)
397     and mantissa_not_dvd: "f \<noteq> (float_of 0) \<Longrightarrow> \<not> 2 dvd mantissa f" (is "_ \<Longrightarrow> ?D")
398 proof cases
399   assume [simp]: "f \<noteq> (float_of 0)"
400   have "f = mantissa f * 2 powr exponent f \<and> \<not> 2 dvd mantissa f"
401   proof (cases f rule: float_normed_cases)
402     case (powr m e)
403     then have "\<exists>p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
404      \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p)"
405       by auto
406     then show ?thesis
407       unfolding exponent_def mantissa_def
408       by (rule someI2_ex) (simp add: zero_float_def)
409   qed (simp add: zero_float_def)
410   then show ?E ?D by auto
411 qed simp
413 lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
414   using mantissa_not_dvd[of f] by auto
416 lemma
417   fixes m e :: int
418   defines "f \<equiv> float_of (m * 2 powr e)"
419   assumes dvd: "\<not> 2 dvd m"
420   shows mantissa_float: "mantissa f = m" (is "?M")
421     and exponent_float: "m \<noteq> 0 \<Longrightarrow> exponent f = e" (is "_ \<Longrightarrow> ?E")
422 proof cases
423   assume "m = 0" with dvd show "mantissa f = m" by auto
424 next
425   assume "m \<noteq> 0"
426   then have f_not_0: "f \<noteq> float_of 0" by (simp add: f_def)
427   from mantissa_exponent[of f]
428   have "m * 2 powr e = mantissa f * 2 powr exponent f"
429     by (auto simp add: f_def)
430   then show "?M" "?E"
431     using mantissa_not_dvd[OF f_not_0] dvd
432     by (auto simp: mult_powr_eq_mult_powr_iff)
433 qed
435 subsection {* Compute arithmetic operations *}
437 lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
438   unfolding real_of_float_eq mantissa_exponent[of f] by simp
440 lemma Float_cases[case_names Float, cases type: float]:
441   fixes f :: float
442   obtains (Float) m e :: int where "f = Float m e"
443   using Float_mantissa_exponent[symmetric]
444   by (atomize_elim) auto
446 lemma denormalize_shift:
447   assumes f_def: "f \<equiv> Float m e" and not_0: "f \<noteq> float_of 0"
448   obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i"
449 proof
450   from mantissa_exponent[of f] f_def
451   have "m * 2 powr e = mantissa f * 2 powr exponent f"
452     by simp
453   then have eq: "m = mantissa f * 2 powr (exponent f - e)"
454     by (simp add: powr_divide2[symmetric] field_simps)
455   moreover
456   have "e \<le> exponent f"
457   proof (rule ccontr)
458     assume "\<not> e \<le> exponent f"
459     then have pos: "exponent f < e" by simp
460     then have "2 powr (exponent f - e) = 2 powr - real (e - exponent f)"
461       by simp
462     also have "\<dots> = 1 / 2^nat (e - exponent f)"
463       using pos by (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
464     finally have "m * 2^nat (e - exponent f) = real (mantissa f)"
465       using eq by simp
466     then have "mantissa f = m * 2^nat (e - exponent f)"
467       unfolding real_of_int_inject by simp
468     with `exponent f < e` have "2 dvd mantissa f"
469       apply (intro dvdI[where k="m * 2^(nat (e-exponent f)) div 2"])
470       apply (cases "nat (e - exponent f)")
471       apply auto
472       done
473     then show False using mantissa_not_dvd[OF not_0] by simp
474   qed
475   ultimately have "real m = mantissa f * 2^nat (exponent f - e)"
476     by (simp add: powr_realpow[symmetric])
477   with `e \<le> exponent f`
478   show "m = mantissa f * 2 ^ nat (exponent f - e)" "e = exponent f - nat (exponent f - e)"
479     unfolding real_of_int_inject by auto
480 qed
482 lemma compute_float_zero[code_unfold, code]: "0 = Float 0 0"
483   by transfer simp
484 hide_fact (open) compute_float_zero
486 lemma compute_float_one[code_unfold, code]: "1 = Float 1 0"
487   by transfer simp
488 hide_fact (open) compute_float_one
490 lift_definition normfloat :: "float \<Rightarrow> float" is "\<lambda>x. x" .
491 lemma normloat_id[simp]: "normfloat x = x" by transfer rule
493 lemma compute_normfloat[code]: "normfloat (Float m e) =
494   (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1))
495                            else if m = 0 then 0 else Float m e)"
496   by transfer (auto simp add: powr_add zmod_eq_0_iff)
497 hide_fact (open) compute_normfloat
499 lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k"
500   by transfer simp
501 hide_fact (open) compute_float_numeral
503 lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k"
504   by transfer simp
505 hide_fact (open) compute_float_neg_numeral
507 lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1"
508   by transfer simp
509 hide_fact (open) compute_float_uminus
511 lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)"
512   by transfer (simp add: field_simps powr_add)
513 hide_fact (open) compute_float_times
515 lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 =
516   (if m1 = 0 then Float m2 e2 else if m2 = 0 then Float m1 e1 else
517   if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
518               else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
519   by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
520 hide_fact (open) compute_float_plus
522 lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)"
523   by simp
524 hide_fact (open) compute_float_minus
526 lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
527   by transfer (simp add: sgn_times)
528 hide_fact (open) compute_float_sgn
530 lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
532 lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
533   by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
534 hide_fact (open) compute_is_float_pos
536 lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)"
537   by transfer (simp add: field_simps)
538 hide_fact (open) compute_float_less
540 lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" .
542 lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
543   by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
544 hide_fact (open) compute_is_float_nonneg
546 lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)"
547   by transfer (simp add: field_simps)
548 hide_fact (open) compute_float_le
550 lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" .
552 lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
553   by transfer (auto simp add: is_float_zero_def)
554 hide_fact (open) compute_is_float_zero
556 lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
557   by transfer (simp add: abs_mult)
558 hide_fact (open) compute_float_abs
560 lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
561   by transfer simp
562 hide_fact (open) compute_float_eq
565 subsection {* Lemmas for types @{typ real}, @{typ nat}, @{typ int}*}
567 lemmas real_of_ints =
568   real_of_int_zero
569   real_of_one
570   real_of_int_add
571   real_of_int_minus
572   real_of_int_diff
573   real_of_int_mult
574   real_of_int_power
575   real_numeral
576 lemmas real_of_nats =
577   real_of_nat_zero
578   real_of_nat_one
579   real_of_nat_1
580   real_of_nat_add
581   real_of_nat_mult
582   real_of_nat_power
584 lemmas int_of_reals = real_of_ints[symmetric]
585 lemmas nat_of_reals = real_of_nats[symmetric]
587 lemma two_real_int: "(2::real) = real (2::int)" by simp
588 lemma two_real_nat: "(2::real) = real (2::nat)" by simp
591 subsection {* Rounding Real Numbers *}
593 definition round_down :: "int \<Rightarrow> real \<Rightarrow> real" where
594   "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec"
596 definition round_up :: "int \<Rightarrow> real \<Rightarrow> real" where
597   "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec"
599 lemma round_down_float[simp]: "round_down prec x \<in> float"
600   unfolding round_down_def
601   by (auto intro!: times_float simp: real_of_int_minus[symmetric] simp del: real_of_int_minus)
603 lemma round_up_float[simp]: "round_up prec x \<in> float"
604   unfolding round_up_def
605   by (auto intro!: times_float simp: real_of_int_minus[symmetric] simp del: real_of_int_minus)
607 lemma round_up: "x \<le> round_up prec x"
608   by (simp add: powr_minus_divide le_divide_eq round_up_def)
610 lemma round_down: "round_down prec x \<le> x"
611   by (simp add: powr_minus_divide divide_le_eq round_down_def)
613 lemma round_up_0[simp]: "round_up p 0 = 0"
614   unfolding round_up_def by simp
616 lemma round_down_0[simp]: "round_down p 0 = 0"
617   unfolding round_down_def by simp
619 lemma round_up_diff_round_down:
620   "round_up prec x - round_down prec x \<le> 2 powr -prec"
621 proof -
622   have "round_up prec x - round_down prec x =
623     (ceiling (x * 2 powr prec) - floor (x * 2 powr prec)) * 2 powr -prec"
624     by (simp add: round_up_def round_down_def field_simps)
625   also have "\<dots> \<le> 1 * 2 powr -prec"
626     by (rule mult_mono)
627        (auto simp del: real_of_int_diff
628              simp: real_of_int_diff[symmetric] real_of_int_le_one_cancel_iff ceiling_diff_floor_le_1)
629   finally show ?thesis by simp
630 qed
632 lemma round_down_shift: "round_down p (x * 2 powr k) = 2 powr k * round_down (p + k) x"
633   unfolding round_down_def
634   by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric])
635     (simp add: powr_add[symmetric])
637 lemma round_up_shift: "round_up p (x * 2 powr k) = 2 powr k * round_up (p + k) x"
638   unfolding round_up_def
639   by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric])
640     (simp add: powr_add[symmetric])
642 lemma round_up_uminus_eq: "round_up p (-x) = - round_down p x"
643   and round_down_uminus_eq: "round_down p (-x) = - round_up p x"
644   by (auto simp: round_up_def round_down_def ceiling_def)
646 lemma round_up_mono: "x \<le> y \<Longrightarrow> round_up p x \<le> round_up p y"
647   by (auto intro!: ceiling_mono simp: round_up_def)
649 lemma round_up_le1:
650   assumes "x \<le> 1" "prec \<ge> 0"
651   shows "round_up prec x \<le> 1"
652 proof -
653   have "real \<lceil>x * 2 powr prec\<rceil> \<le> real \<lceil>2 powr real prec\<rceil>"
654     using assms by (auto intro!: ceiling_mono)
655   also have "\<dots> = 2 powr prec" using assms by (auto simp: powr_int intro!: exI[where x="2^nat prec"])
656   finally show ?thesis
657     by (simp add: round_up_def) (simp add: powr_minus inverse_eq_divide)
658 qed
660 lemma round_up_less1:
661   assumes "x < 1 / 2" "p > 0"
662   shows "round_up p x < 1"
663 proof -
664   have powr1: "2 powr p = 2 ^ nat p"
665     using `p > 0` by (simp add: powr_realpow[symmetric])
666   have "x * 2 powr p < 1 / 2 * 2 powr p"
667     using assms by simp
668   also have "\<dots> = 2 powr (p - 1)"
669     by (simp add: algebra_simps powr_mult_base)
670   also have "\<dots> = 2 ^ nat (p - 1)"
671     using `p > 0` by (simp add: powr_realpow[symmetric])
672   also have "\<dots> \<le> 2 ^ nat p - 1"
673     using `p > 0`
674     unfolding int_of_reals real_of_int_le_iff
675     by simp
676   finally show ?thesis
677     apply (simp add: round_up_def field_simps powr_minus powr1)
678     unfolding int_of_reals real_of_int_less_iff
679     apply (simp add: ceiling_less_eq)
680     done
681 qed
683 lemma round_down_ge1:
684   assumes x: "x \<ge> 1"
685   assumes prec: "p \<ge> - log 2 x"
686   shows "1 \<le> round_down p x"
687 proof cases
688   assume nonneg: "0 \<le> p"
689   have "2 powr p = real \<lfloor>2 powr real p\<rfloor>"
690     using nonneg by (auto simp: powr_int)
691   also have "\<dots> \<le> real \<lfloor>x * 2 powr p\<rfloor>"
692     using assms by (auto intro!: floor_mono)
693   finally show ?thesis
694     by (simp add: round_down_def) (simp add: powr_minus inverse_eq_divide)
695 next
696   assume neg: "\<not> 0 \<le> p"
697   have "x = 2 powr (log 2 x)"
698     using x by simp
699   also have "2 powr (log 2 x) \<ge> 2 powr - p"
700     using prec by auto
701   finally have x_le: "x \<ge> 2 powr -p" .
703   from neg have "2 powr real p \<le> 2 powr 0"
704     by (intro powr_mono) auto
705   also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
706   also have "\<dots> \<le> \<lfloor>x * 2 powr real p\<rfloor>" unfolding real_of_int_le_iff
707     using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
708   finally show ?thesis
709     using prec x
710     by (simp add: round_down_def powr_minus_divide pos_le_divide_eq)
711 qed
713 lemma round_up_le0: "x \<le> 0 \<Longrightarrow> round_up p x \<le> 0"
714   unfolding round_up_def
715   by (auto simp: field_simps mult_le_0_iff zero_le_mult_iff)
718 subsection {* Rounding Floats *}
720 definition div_twopow::"int \<Rightarrow> nat \<Rightarrow> int" where [simp]: "div_twopow x n = x div (2 ^ n)"
722 definition mod_twopow::"int \<Rightarrow> nat \<Rightarrow> int" where [simp]: "mod_twopow x n = x mod (2 ^ n)"
724 lemma compute_div_twopow[code]:
725   "div_twopow x n = (if x = 0 \<or> x = -1 \<or> n = 0 then x else div_twopow (x div 2) (n - 1))"
726   by (cases n) (auto simp: zdiv_zmult2_eq div_eq_minus1)
728 lemma compute_mod_twopow[code]:
729   "mod_twopow x n = (if n = 0 then 0 else x mod 2 + 2 * mod_twopow (x div 2) (n - 1))"
730   by (cases n) (auto simp: zmod_zmult2_eq)
732 lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
733 declare float_up.rep_eq[simp]
735 lemma round_up_correct:
736   shows "round_up e f - f \<in> {0..2 powr -e}"
737 unfolding atLeastAtMost_iff
738 proof
739   have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
740   also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
741   finally show "round_up e f - f \<le> 2 powr real (- e)"
742     by simp
743 qed (simp add: algebra_simps round_up)
745 lemma float_up_correct:
746   shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
747   by transfer (rule round_up_correct)
749 lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
750 declare float_down.rep_eq[simp]
752 lemma round_down_correct:
753   shows "f - (round_down e f) \<in> {0..2 powr -e}"
754 unfolding atLeastAtMost_iff
755 proof
756   have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
757   also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
758   finally show "f - round_down e f \<le> 2 powr real (- e)"
759     by simp
760 qed (simp add: algebra_simps round_down)
762 lemma float_down_correct:
763   shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
764   by transfer (rule round_down_correct)
766 lemma compute_float_down[code]:
767   "float_down p (Float m e) =
768     (if p + e < 0 then Float (div_twopow m (nat (-(p + e)))) (-p) else Float m e)"
769 proof cases
770   assume "p + e < 0"
771   hence "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))"
772     using powr_realpow[of 2 "nat (-(p + e))"] by simp
773   also have "... = 1 / 2 powr p / 2 powr e"
774     unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add)
775   finally show ?thesis
776     using `p + e < 0`
777     by transfer (simp add: ac_simps round_down_def floor_divide_eq_div[symmetric])
778 next
779   assume "\<not> p + e < 0"
780   then have r: "real e + real p = real (nat (e + p))" by simp
781   have r: "\<lfloor>(m * 2 powr e) * 2 powr real p\<rfloor> = (m * 2 powr e) * 2 powr real p"
782     by (auto intro: exI[where x="m*2^nat (e+p)"]
783              simp add: ac_simps powr_add[symmetric] r powr_realpow)
784   with `\<not> p + e < 0` show ?thesis
785     by transfer (auto simp add: round_down_def field_simps powr_add powr_minus)
786 qed
787 hide_fact (open) compute_float_down
789 lemma abs_round_down_le: "\<bar>f - (round_down e f)\<bar> \<le> 2 powr -e"
790   using round_down_correct[of f e] by simp
792 lemma abs_round_up_le: "\<bar>f - (round_up e f)\<bar> \<le> 2 powr -e"
793   using round_up_correct[of e f] by simp
795 lemma round_down_nonneg: "0 \<le> s \<Longrightarrow> 0 \<le> round_down p s"
796   by (auto simp: round_down_def)
798 lemma ceil_divide_floor_conv:
799 assumes "b \<noteq> 0"
800 shows "\<lceil>real a / real b\<rceil> = (if b dvd a then a div b else \<lfloor>real a / real b\<rfloor> + 1)"
801 proof cases
802   assume "\<not> b dvd a"
803   hence "a mod b \<noteq> 0" by auto
804   hence ne: "real (a mod b) / real b \<noteq> 0" using `b \<noteq> 0` by auto
805   have "\<lceil>real a / real b\<rceil> = \<lfloor>real a / real b\<rfloor> + 1"
806   apply (rule ceiling_eq) apply (auto simp: floor_divide_eq_div[symmetric])
807   proof -
808     have "real \<lfloor>real a / real b\<rfloor> \<le> real a / real b" by simp
809     moreover have "real \<lfloor>real a / real b\<rfloor> \<noteq> real a / real b"
810     apply (subst (2) real_of_int_div_aux) unfolding floor_divide_eq_div using ne `b \<noteq> 0` by auto
811     ultimately show "real \<lfloor>real a / real b\<rfloor> < real a / real b" by arith
812   qed
813   thus ?thesis using `\<not> b dvd a` by simp
814 qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
815   floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
817 lemma compute_float_up[code]:
818   "float_up p x = - float_down p (-x)"
819   by transfer (simp add: round_down_uminus_eq)
820 hide_fact (open) compute_float_up
823 subsection {* Compute bitlen of integers *}
825 definition bitlen :: "int \<Rightarrow> int" where
826   "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
828 lemma bitlen_nonneg: "0 \<le> bitlen x"
829 proof -
830   {
831     assume "0 > x"
832     have "-1 = log 2 (inverse 2)" by (subst log_inverse) simp_all
833     also have "... < log 2 (-x)" using `0 > x` by auto
834     finally have "-1 < log 2 (-x)" .
835   } thus "0 \<le> bitlen x" unfolding bitlen_def by (auto intro!: add_nonneg_nonneg)
836 qed
838 lemma bitlen_bounds:
839   assumes "x > 0"
840   shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)"
841 proof
842   have "(2::real) ^ nat \<lfloor>log 2 (real x)\<rfloor> = 2 powr real (floor (log 2 (real x)))"
843     using powr_realpow[symmetric, of 2 "nat \<lfloor>log 2 (real x)\<rfloor>"] `x > 0`
844     using real_nat_eq_real[of "floor (log 2 (real x))"]
845     by simp
846   also have "... \<le> 2 powr log 2 (real x)"
847     by simp
848   also have "... = real x"
849     using `0 < x` by simp
850   finally have "2 ^ nat \<lfloor>log 2 (real x)\<rfloor> \<le> real x" by simp
851   thus "2 ^ nat (bitlen x - 1) \<le> x" using `x > 0`
852     by (simp add: bitlen_def)
853 next
854   have "x \<le> 2 powr (log 2 x)" using `x > 0` by simp
855   also have "... < 2 ^ nat (\<lfloor>log 2 (real x)\<rfloor> + 1)"
856     apply (simp add: powr_realpow[symmetric])
857     using `x > 0` by simp
858   finally show "x < 2 ^ nat (bitlen x)" using `x > 0`
859     by (simp add: bitlen_def ac_simps int_of_reals del: real_of_ints)
860 qed
862 lemma bitlen_pow2[simp]:
863   assumes "b > 0"
864   shows "bitlen (b * 2 ^ c) = bitlen b + c"
865 proof -
866   from assms have "b * 2 ^ c > 0" by auto
867   thus ?thesis
868     using floor_add[of "log 2 b" c] assms
869     by (auto simp add: log_mult log_nat_power bitlen_def)
870 qed
872 lemma bitlen_Float:
873   fixes m e
874   defines "f \<equiv> Float m e"
875   shows "bitlen (\<bar>mantissa f\<bar>) + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
876 proof (cases "m = 0")
877   case True
878   then show ?thesis by (simp add: f_def bitlen_def Float_def)
879 next
880   case False
881   hence "f \<noteq> float_of 0"
882     unfolding real_of_float_eq by (simp add: f_def)
883   hence "mantissa f \<noteq> 0"
884     by (simp add: mantissa_noteq_0)
885   moreover
886   obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
887     by (rule f_def[THEN denormalize_shift, OF `f \<noteq> float_of 0`])
888   ultimately show ?thesis by (simp add: abs_mult)
889 qed
891 lemma compute_bitlen[code]:
892   shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
893 proof -
894   { assume "2 \<le> x"
895     then have "\<lfloor>log 2 (x div 2)\<rfloor> + 1 = \<lfloor>log 2 (x - x mod 2)\<rfloor>"
896       by (simp add: log_mult zmod_zdiv_equality')
897     also have "\<dots> = \<lfloor>log 2 (real x)\<rfloor>"
898     proof cases
899       assume "x mod 2 = 0" then show ?thesis by simp
900     next
901       def n \<equiv> "\<lfloor>log 2 (real x)\<rfloor>"
902       then have "0 \<le> n"
903         using `2 \<le> x` by simp
904       assume "x mod 2 \<noteq> 0"
905       with `2 \<le> x` have "x mod 2 = 1" "\<not> 2 dvd x" by (auto simp add: dvd_eq_mod_eq_0)
906       with `2 \<le> x` have "x \<noteq> 2^nat n" by (cases "nat n") auto
907       moreover
908       { have "real (2^nat n :: int) = 2 powr (nat n)"
909           by (simp add: powr_realpow)
910         also have "\<dots> \<le> 2 powr (log 2 x)"
911           using `2 \<le> x` by (simp add: n_def del: powr_log_cancel)
912         finally have "2^nat n \<le> x" using `2 \<le> x` by simp }
913       ultimately have "2^nat n \<le> x - 1" by simp
914       then have "2^nat n \<le> real (x - 1)"
915         unfolding real_of_int_le_iff[symmetric] by simp
916       { have "n = \<lfloor>log 2 (2^nat n)\<rfloor>"
917           using `0 \<le> n` by (simp add: log_nat_power)
918         also have "\<dots> \<le> \<lfloor>log 2 (x - 1)\<rfloor>"
919           using `2^nat n \<le> real (x - 1)` `0 \<le> n` `2 \<le> x` by (auto intro: floor_mono)
920         finally have "n \<le> \<lfloor>log 2 (x - 1)\<rfloor>" . }
921       moreover have "\<lfloor>log 2 (x - 1)\<rfloor> \<le> n"
922         using `2 \<le> x` by (auto simp add: n_def intro!: floor_mono)
923       ultimately show "\<lfloor>log 2 (x - x mod 2)\<rfloor> = \<lfloor>log 2 x\<rfloor>"
924         unfolding n_def `x mod 2 = 1` by auto
925     qed
926     finally have "\<lfloor>log 2 (x div 2)\<rfloor> + 1 = \<lfloor>log 2 x\<rfloor>" . }
927   moreover
928   { assume "x < 2" "0 < x"
929     then have "x = 1" by simp
930     then have "\<lfloor>log 2 (real x)\<rfloor> = 0" by simp }
931   ultimately show ?thesis
932     unfolding bitlen_def
933     by (auto simp: pos_imp_zdiv_pos_iff not_le)
934 qed
935 hide_fact (open) compute_bitlen
937 lemma float_gt1_scale: assumes "1 \<le> Float m e"
938   shows "0 \<le> e + (bitlen m - 1)"
939 proof -
940   have "0 < Float m e" using assms by auto
941   hence "0 < m" using powr_gt_zero[of 2 e]
942     by (auto simp: zero_less_mult_iff)
943   hence "m \<noteq> 0" by auto
944   show ?thesis
945   proof (cases "0 \<le> e")
946     case True thus ?thesis using `0 < m`  by (simp add: bitlen_def)
947   next
948     have "(1::int) < 2" by simp
949     case False let ?S = "2^(nat (-e))"
950     have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"]
951       by (auto simp: powr_minus field_simps)
952     hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
953       by (auto simp: powr_minus)
954     hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
955     hence "?S \<le> real m" unfolding mult.assoc by auto
956     hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto
957     from this bitlen_bounds[OF `0 < m`, THEN conjunct2]
958     have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric]
959       by (rule order_le_less_trans)
960     hence "-e < bitlen m" using False by auto
961     thus ?thesis by auto
962   qed
963 qed
965 lemma bitlen_div:
966   assumes "0 < m"
967   shows "1 \<le> real m / 2^nat (bitlen m - 1)" and "real m / 2^nat (bitlen m - 1) < 2"
968 proof -
969   let ?B = "2^nat(bitlen m - 1)"
971   have "?B \<le> m" using bitlen_bounds[OF `0 <m`] ..
972   hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto
973   thus "1 \<le> real m / ?B" by auto
975   have "m \<noteq> 0" using assms by auto
976   have "0 \<le> bitlen m - 1" using `0 < m` by (auto simp: bitlen_def)
978   have "m < 2^nat(bitlen m)" using bitlen_bounds[OF `0 <m`] ..
979   also have "\<dots> = 2^nat(bitlen m - 1 + 1)" using `0 < m` by (auto simp: bitlen_def)
980   also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF `0 \<le> bitlen m - 1` zero_le_one] by auto
981   finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto
982   hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto)
983   thus "real m / ?B < 2" by auto
984 qed
986 subsection {* Truncating Real Numbers*}
988 definition truncate_down::"nat \<Rightarrow> real \<Rightarrow> real" where
989   "truncate_down prec x = round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
991 lemma truncate_down: "truncate_down prec x \<le> x"
992   using round_down by (simp add: truncate_down_def)
994 lemma truncate_down_le: "x \<le> y \<Longrightarrow> truncate_down prec x \<le> y"
995   by (rule order_trans[OF truncate_down])
997 lemma truncate_down_zero[simp]: "truncate_down prec 0 = 0"
998   by (simp add: truncate_down_def)
1000 lemma truncate_down_float[simp]: "truncate_down p x \<in> float"
1001   by (auto simp: truncate_down_def)
1003 definition truncate_up::"nat \<Rightarrow> real \<Rightarrow> real" where
1004   "truncate_up prec x = round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
1006 lemma truncate_up: "x \<le> truncate_up prec x"
1007   using round_up by (simp add: truncate_up_def)
1009 lemma truncate_up_le: "x \<le> y \<Longrightarrow> x \<le> truncate_up prec y"
1010   by (rule order_trans[OF _ truncate_up])
1012 lemma truncate_up_zero[simp]: "truncate_up prec 0 = 0"
1013   by (simp add: truncate_up_def)
1015 lemma truncate_up_uminus_eq: "truncate_up prec (-x) = - truncate_down prec x"
1016   and truncate_down_uminus_eq: "truncate_down prec (-x) = - truncate_up prec x"
1017   by (auto simp: truncate_up_def round_up_def truncate_down_def round_down_def ceiling_def)
1019 lemma truncate_up_float[simp]: "truncate_up p x \<in> float"
1020   by (auto simp: truncate_up_def)
1022 lemma mult_powr_eq: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> x * b powr y = b powr (y + log b x)"
1023   by (simp_all add: powr_add)
1025 lemma truncate_down_pos:
1026   assumes "x > 0" "p > 0"
1027   shows "truncate_down p x > 0"
1028 proof -
1029   have "0 \<le> log 2 x - real \<lfloor>log 2 x\<rfloor>"
1030     by (simp add: algebra_simps)
1031   from this assms
1032   show ?thesis
1033     by (auto simp: truncate_down_def round_down_def mult_powr_eq
1034       intro!: ge_one_powr_ge_zero mult_pos_pos)
1035 qed
1037 lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
1038   by (auto simp: truncate_down_def round_down_def)
1040 lemma truncate_down_ge1: "1 \<le> x \<Longrightarrow> 1 \<le> p \<Longrightarrow> 1 \<le> truncate_down p x"
1041   by (auto simp: truncate_down_def algebra_simps intro!: round_down_ge1 add_mono)
1043 lemma truncate_up_nonpos: "x \<le> 0 \<Longrightarrow> truncate_up prec x \<le> 0"
1044   by (auto simp: truncate_up_def round_up_def intro!: mult_nonpos_nonneg)
1046 lemma truncate_up_le1:
1047   assumes "x \<le> 1" "1 \<le> p" shows "truncate_up p x \<le> 1"
1048 proof -
1049   {
1050     assume "x \<le> 0"
1051     with truncate_up_nonpos[OF this, of p] have ?thesis by simp
1052   } moreover {
1053     assume "x > 0"
1054     hence le: "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<le> 0"
1055       using assms by (auto simp: log_less_iff)
1056     from assms have "1 \<le> int p" by simp
1057     from add_mono[OF this le]
1058     have ?thesis using assms
1059       by (simp add: truncate_up_def round_up_le1 add_mono)
1060   } ultimately show ?thesis by arith
1061 qed
1063 subsection {* Truncating Floats*}
1065 lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_up
1066   by (simp add: truncate_up_def)
1068 lemma float_round_up: "real x \<le> real (float_round_up prec x)"
1069   using truncate_up by transfer simp
1071 lemma float_round_up_zero[simp]: "float_round_up prec 0 = 0"
1072   by transfer simp
1074 lift_definition float_round_down :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_down
1075   by (simp add: truncate_down_def)
1077 lemma float_round_down: "real (float_round_down prec x) \<le> real x"
1078   using truncate_down by transfer simp
1080 lemma float_round_down_zero[simp]: "float_round_down prec 0 = 0"
1081   by transfer simp
1083 lemmas float_round_up_le = order_trans[OF _ float_round_up]
1084   and float_round_down_le = order_trans[OF float_round_down]
1086 lemma minus_float_round_up_eq: "- float_round_up prec x = float_round_down prec (- x)"
1087   and minus_float_round_down_eq: "- float_round_down prec x = float_round_up prec (- x)"
1088   by (transfer, simp add: truncate_down_uminus_eq truncate_up_uminus_eq)+
1090 lemma compute_float_round_down[code]:
1091   "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
1092     if 0 < d then Float (div_twopow m (nat d)) (e + d)
1093              else Float m e)"
1094   using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
1095   by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_down_def
1096     cong del: if_weak_cong)
1097 hide_fact (open) compute_float_round_down
1099 lemma compute_float_round_up[code]:
1100   "float_round_up prec x = - float_round_down prec (-x)"
1101   by transfer (simp add: truncate_down_uminus_eq)
1102 hide_fact (open) compute_float_round_up
1105 subsection {* Approximation of positive rationals *}
1107 lemma div_mult_twopow_eq: fixes a b::nat shows "a div ((2::nat) ^ n) div b = a div (b * 2 ^ n)"
1108   by (cases "b=0") (simp_all add: div_mult2_eq[symmetric] ac_simps)
1110 lemma real_div_nat_eq_floor_of_divide:
1111   fixes a b::nat
1112   shows "a div b = real (floor (a/b))"
1113 by (metis floor_divide_eq_div real_of_int_of_nat_eq zdiv_int)
1115 definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)"
1117 lift_definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
1118   is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
1120 lemma compute_lapprox_posrat[code]:
1121   fixes prec x y
1122   shows "lapprox_posrat prec x y =
1123    (let
1124        l = rat_precision prec x y;
1125        d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
1126     in normfloat (Float d (- l)))"
1127     unfolding div_mult_twopow_eq
1128     by transfer
1129        (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def
1130              del: two_powr_minus_int_float)
1131 hide_fact (open) compute_lapprox_posrat
1133 lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
1134   is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
1136 lemma compute_rapprox_posrat[code]:
1137   fixes prec x y
1138   notes divmod_int_mod_div[simp]
1139   defines "l \<equiv> rat_precision prec x y"
1140   shows "rapprox_posrat prec x y = (let
1141      l = l ;
1142      X = if 0 \<le> l then (x * 2^nat l, y) else (x, y * 2^nat(-l)) ;
1143      (d, m) = divmod_int (fst X) (snd X)
1144    in normfloat (Float (d + (if m = 0 \<or> y = 0 then 0 else 1)) (- l)))"
1145 proof (cases "y = 0")
1146   assume "y = 0" thus ?thesis by transfer simp
1147 next
1148   assume "y \<noteq> 0"
1149   show ?thesis
1150   proof (cases "0 \<le> l")
1151     assume "0 \<le> l"
1152     def x' \<equiv> "x * 2 ^ nat l"
1153     have "int x * 2 ^ nat l = x'" by (simp add: x'_def int_mult int_power)
1154     moreover have "real x * 2 powr real l = real x'"
1155       by (simp add: powr_realpow[symmetric] `0 \<le> l` x'_def)
1156     ultimately show ?thesis
1157       using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \<le> l` `y \<noteq> 0`
1158         l_def[symmetric, THEN meta_eq_to_obj_eq]
1159       by transfer (auto simp add: floor_divide_eq_div [symmetric] round_up_def)
1160    next
1161     assume "\<not> 0 \<le> l"
1162     def y' \<equiv> "y * 2 ^ nat (- l)"
1163     from `y \<noteq> 0` have "y' \<noteq> 0" by (simp add: y'_def)
1164     have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
1165     moreover have "real x * real (2::int) powr real l / real y = x / real y'"
1166       using `\<not> 0 \<le> l`
1167       by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
1168     ultimately show ?thesis
1169       using ceil_divide_floor_conv[of y' x] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 0`
1170         l_def[symmetric, THEN meta_eq_to_obj_eq]
1171       by transfer
1172          (auto simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div [symmetric])
1173   qed
1174 qed
1175 hide_fact (open) compute_rapprox_posrat
1177 lemma rat_precision_pos:
1178   assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
1179   shows "rat_precision n (int x) (int y) > 0"
1180 proof -
1181   { assume "0 < x" hence "log 2 x + 1 = log 2 (2 * x)" by (simp add: log_mult) }
1182   hence "bitlen (int x) < bitlen (int y)" using assms
1183     by (simp add: bitlen_def del: floor_add_one)
1184       (auto intro!: floor_mono simp add: floor_add_one[symmetric] simp del: floor_add floor_add_one)
1185   thus ?thesis
1186     using assms by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
1187 qed
1189 lemma rapprox_posrat_less1:
1190   shows "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 2 * x < y \<Longrightarrow> 0 < n \<Longrightarrow> real (rapprox_posrat n x y) < 1"
1191   by transfer (simp add: rat_precision_pos round_up_less1)
1193 lift_definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
1194   "\<lambda>prec (x::int) (y::int). round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
1196 lemma compute_lapprox_rat[code]:
1197   "lapprox_rat prec x y =
1198     (if y = 0 then 0
1199     else if 0 \<le> x then
1200       (if 0 < y then lapprox_posrat prec (nat x) (nat y)
1201       else - (rapprox_posrat prec (nat x) (nat (-y))))
1202       else (if 0 < y
1203         then - (rapprox_posrat prec (nat (-x)) (nat y))
1204         else lapprox_posrat prec (nat (-x)) (nat (-y))))"
1205   by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
1206 hide_fact (open) compute_lapprox_rat
1208 lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
1209   "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
1211 lemma "rapprox_rat = rapprox_posrat"
1212   by transfer auto
1214 lemma "lapprox_rat = lapprox_posrat"
1215   by transfer auto
1217 lemma compute_rapprox_rat[code]:
1218   "rapprox_rat prec x y = - lapprox_rat prec (-x) y"
1219   by transfer (simp add: round_down_uminus_eq)
1220 hide_fact (open) compute_rapprox_rat
1222 subsection {* Division *}
1224 definition "real_divl prec a b = round_down (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)"
1226 definition "real_divr prec a b = round_up (int prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)"
1228 lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divl
1229   by (simp add: real_divl_def)
1231 lemma compute_float_divl[code]:
1232   "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
1233 proof cases
1234   let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
1235   let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
1236   assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
1237   then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
1238     by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
1239   have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
1240     by (simp add: field_simps powr_divide2[symmetric])
1242   show ?thesis
1243     using not_0
1244     by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift real_divl_def,
1245       simp add: field_simps)
1246 qed (transfer, auto simp: real_divl_def)
1247 hide_fact (open) compute_float_divl
1249 lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr
1250   by (simp add: real_divr_def)
1252 lemma compute_float_divr[code]:
1253   "float_divr prec x y = - float_divl prec (-x) y"
1254   by transfer (simp add: real_divr_def real_divl_def round_down_uminus_eq)
1255 hide_fact (open) compute_float_divr
1258 subsection {* Approximate Power *}
1260 lemma div2_less_self[termination_simp]: fixes n::nat shows "odd n \<Longrightarrow> n div 2 < n"
1261   by (simp add: odd_pos)
1263 fun power_down :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real" where
1264   "power_down p x 0 = 1"
1265 | "power_down p x (Suc n) =
1266     (if odd n then truncate_down (Suc p) ((power_down p x (Suc n div 2))\<^sup>2) else truncate_down (Suc p) (x * power_down p x n))"
1268 fun power_up :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real" where
1269   "power_up p x 0 = 1"
1270 | "power_up p x (Suc n) =
1271     (if odd n then truncate_up p ((power_up p x (Suc n div 2))\<^sup>2) else truncate_up p (x * power_up p x n))"
1273 lift_definition power_up_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_up
1274   by (induct_tac rule: power_up.induct) simp_all
1276 lift_definition power_down_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_down
1277   by (induct_tac rule: power_down.induct) simp_all
1279 lemma power_float_transfer[transfer_rule]:
1280   "(rel_fun pcr_float (rel_fun op = pcr_float)) op ^ op ^"
1281   unfolding power_def
1282   by transfer_prover
1284 lemma compute_power_up_fl[code]:
1285   "power_up_fl p x 0 = 1"
1286   "power_up_fl p x (Suc n) =
1287     (if odd n then float_round_up p ((power_up_fl p x (Suc n div 2))\<^sup>2) else float_round_up p (x * power_up_fl p x n))"
1288   and compute_power_down_fl[code]:
1289   "power_down_fl p x 0 = 1"
1290   "power_down_fl p x (Suc n) =
1291     (if odd n then float_round_down (Suc p) ((power_down_fl p x (Suc n div 2))\<^sup>2) else float_round_down (Suc p) (x * power_down_fl p x n))"
1292   unfolding atomize_conj
1293   by transfer simp
1295 lemma power_down_pos: "0 < x \<Longrightarrow> 0 < power_down p x n"
1296   by (induct p x n rule: power_down.induct)
1297     (auto simp del: odd_Suc_div_two intro!: truncate_down_pos)
1299 lemma power_down_nonneg: "0 \<le> x \<Longrightarrow> 0 \<le> power_down p x n"
1300   by (induct p x n rule: power_down.induct)
1301     (auto simp del: odd_Suc_div_two intro!: truncate_down_nonneg mult_nonneg_nonneg)
1303 lemma power_down: "0 \<le> x \<Longrightarrow> power_down p x n \<le> x ^ n"
1304 proof (induct p x n rule: power_down.induct)
1305   case (2 p x n)
1306   {
1307     assume "odd n"
1308     hence "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
1309       using 2
1310       by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
1311     also have "\<dots> = x ^ (Suc n div 2 * 2)"
1312       by (simp add: power_mult[symmetric])
1313     also have "Suc n div 2 * 2 = Suc n"
1314       using `odd n` by presburger
1315     finally have ?case
1316       using `odd n`
1317       by (auto intro!: truncate_down_le simp del: odd_Suc_div_two)
1318   } thus ?case
1319     by (auto intro!: truncate_down_le mult_left_mono 2 mult_nonneg_nonneg power_down_nonneg)
1320 qed simp
1322 lemma power_up: "0 \<le> x \<Longrightarrow> x ^ n \<le> power_up p x n"
1323 proof (induct p x n rule: power_up.induct)
1324   case (2 p x n)
1325   {
1326     assume "odd n"
1327     hence "Suc n = Suc n div 2 * 2"
1328       using `odd n` even_Suc by presburger
1329     hence "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
1330       by (simp add: power_mult[symmetric])
1331     also have "\<dots> \<le> (power_up p x (Suc n div 2))\<^sup>2"
1332       using 2 `odd n`
1333       by (auto intro: power_mono simp del: odd_Suc_div_two )
1334     finally have ?case
1335       using `odd n`
1336       by (auto intro!: truncate_up_le simp del: odd_Suc_div_two )
1337   } thus ?case
1338     by (auto intro!: truncate_up_le mult_left_mono 2)
1339 qed simp
1341 lemmas power_up_le = order_trans[OF _ power_up]
1342   and power_up_less = less_le_trans[OF _ power_up]
1343   and power_down_le = order_trans[OF power_down]
1345 lemma power_down_fl: "0 \<le> x \<Longrightarrow> power_down_fl p x n \<le> x ^ n"
1346   by transfer (rule power_down)
1348 lemma power_up_fl: "0 \<le> x \<Longrightarrow> x ^ n \<le> power_up_fl p x n"
1349   by transfer (rule power_up)
1351 lemma real_power_up_fl: "real (power_up_fl p x n) = power_up p x n"
1352   by transfer simp
1354 lemma real_power_down_fl: "real (power_down_fl p x n) = power_down p x n"
1355   by transfer simp
1358 subsection {* Approximate Addition *}
1360 definition "plus_down prec x y = truncate_down prec (x + y)"
1362 definition "plus_up prec x y = truncate_up prec (x + y)"
1364 lemma float_plus_down_float[intro, simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> plus_down p x y \<in> float"
1365   by (simp add: plus_down_def)
1367 lemma float_plus_up_float[intro, simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> plus_up p x y \<in> float"
1368   by (simp add: plus_up_def)
1370 lift_definition float_plus_down::"nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is plus_down ..
1372 lift_definition float_plus_up::"nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is plus_up ..
1374 lemma plus_down: "plus_down prec x y \<le> x + y"
1375   and plus_up: "x + y \<le> plus_up prec x y"
1376   by (auto simp: plus_down_def truncate_down plus_up_def truncate_up)
1378 lemma float_plus_down: "real (float_plus_down prec x y) \<le> x + y"
1379   and float_plus_up: "x + y \<le> real (float_plus_up prec x y)"
1380   by (transfer, rule plus_down plus_up)+
1382 lemmas plus_down_le = order_trans[OF plus_down]
1383   and plus_up_le = order_trans[OF _ plus_up]
1384   and float_plus_down_le = order_trans[OF float_plus_down]
1385   and float_plus_up_le = order_trans[OF _ float_plus_up]
1387 lemma compute_plus_up[code]: "plus_up p x y = - plus_down p (-x) (-y)"
1388   using truncate_down_uminus_eq[of p "x + y"]
1389   by (auto simp: plus_down_def plus_up_def)
1391 lemma
1392   truncate_down_log2_eqI:
1393   assumes "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
1394   assumes "\<lfloor>x * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)\<rfloor> = \<lfloor>y * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)\<rfloor>"
1395   shows "truncate_down p x = truncate_down p y"
1396   using assms by (auto simp: truncate_down_def round_down_def)
1398 lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0"
1399   by (clarsimp simp add: bitlen_def)
1400     (metis Float.compute_bitlen add.commute bitlen_def bitlen_nonneg less_add_same_cancel2 not_less
1401       zero_less_one)
1403 lemma
1404   sum_neq_zeroI:
1405   fixes a k::real
1406   shows "abs a \<ge> k \<Longrightarrow> abs b < k \<Longrightarrow> a + b \<noteq> 0"
1407     and "abs a > k \<Longrightarrow> abs b \<le> k \<Longrightarrow> a + b \<noteq> 0"
1408   by auto
1410 lemma
1411   abs_real_le_2_powr_bitlen[simp]:
1412   "\<bar>real m2\<bar> < 2 powr real (bitlen \<bar>m2\<bar>)"
1413 proof cases
1414   assume "m2 \<noteq> 0"
1415   hence "\<bar>m2\<bar> < 2 ^ nat (bitlen \<bar>m2\<bar>)"
1416     using bitlen_bounds[of "\<bar>m2\<bar>"]
1417     by (auto simp: powr_add bitlen_nonneg)
1418   thus ?thesis
1419     by (simp add: powr_int bitlen_nonneg real_of_int_less_iff[symmetric])
1420 qed simp
1422 lemma floor_sum_times_2_powr_sgn_eq:
1423   fixes ai p q::int
1424   and a b::real
1425   assumes "a * 2 powr p = ai"
1426   assumes b_le_1: "abs (b * 2 powr (p + 1)) \<le> 1"
1427   assumes leqp: "q \<le> p"
1428   shows "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2 * ai + sgn b) * 2 powr (q - p - 1)\<rfloor>"
1429 proof -
1430   {
1431     assume "b = 0"
1432     hence ?thesis
1433       by (simp add: assms(1)[symmetric] powr_add[symmetric] algebra_simps powr_mult_base)
1434   } moreover {
1435     assume "b > 0"
1436     hence "b * 2 powr p < abs (b * 2 powr (p + 1))" by simp
1437     also note b_le_1
1438     finally have b_less_1: "b * 2 powr real p < 1" .
1440     from b_less_1 `b > 0` have floor_eq: "\<lfloor>b * 2 powr real p\<rfloor> = 0" "\<lfloor>sgn b / 2\<rfloor> = 0"
1441       by (simp_all add: floor_eq_iff)
1443     have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(a + b) * 2 powr p * 2 powr (q - p)\<rfloor>"
1444       by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric])
1445     also have "\<dots> = \<lfloor>(ai + b * 2 powr p) * 2 powr (q - p)\<rfloor>"
1446       by (simp add: assms algebra_simps)
1447     also have "\<dots> = \<lfloor>(ai + b * 2 powr p) / real ((2::int) ^ nat (p - q))\<rfloor>"
1448       using assms
1449       by (simp add: algebra_simps powr_realpow[symmetric] divide_powr_uminus powr_add[symmetric])
1450     also have "\<dots> = \<lfloor>ai / real ((2::int) ^ nat (p - q))\<rfloor>"
1451       by (simp del: real_of_int_power add: floor_divide_real_eq_div floor_eq)
1452     finally have "\<lfloor>(a + b) * 2 powr real q\<rfloor> = \<lfloor>real ai / real ((2::int) ^ nat (p - q))\<rfloor>" .
1453     moreover
1454     {
1455       have "\<lfloor>(2 * ai + sgn b) * 2 powr (real (q - p) - 1)\<rfloor> = \<lfloor>(ai + sgn b / 2) * 2 powr (q - p)\<rfloor>"
1456         by (subst powr_divide2[symmetric]) (simp add: field_simps)
1457       also have "\<dots> = \<lfloor>(ai + sgn b / 2) / real ((2::int) ^ nat (p - q))\<rfloor>"
1458         using leqp by (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
1459       also have "\<dots> = \<lfloor>ai / real ((2::int) ^ nat (p - q))\<rfloor>"
1460         by (simp del: real_of_int_power add: floor_divide_real_eq_div floor_eq)
1461       finally
1462       have "\<lfloor>(2 * ai + (sgn b)) * 2 powr (real (q - p) - 1)\<rfloor> =
1463           \<lfloor>real ai / real ((2::int) ^ nat (p - q))\<rfloor>"
1464         .
1465     } ultimately have ?thesis by simp
1466   } moreover {
1467     assume "\<not> 0 \<le> b"
1468     hence "0 > b" by simp
1469     hence floor_eq: "\<lfloor>b * 2 powr (real p + 1)\<rfloor> = -1"
1470       using b_le_1
1471       by (auto simp: floor_eq_iff algebra_simps pos_divide_le_eq[symmetric] abs_if divide_powr_uminus
1472         intro!: mult_neg_pos split: split_if_asm)
1473     have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2*a + 2*b) * 2 powr p * 2 powr (q - p - 1)\<rfloor>"
1474       by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric] powr_mult_base)
1475     also have "\<dots> = \<lfloor>(2 * (a * 2 powr p) + 2 * b * 2 powr p) * 2 powr (q - p - 1)\<rfloor>"
1476       by (simp add: algebra_simps)
1477     also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / 2 powr (1 - q + p)\<rfloor>"
1478       using assms by (simp add: algebra_simps powr_mult_base divide_powr_uminus)
1479     also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / real ((2::int) ^ nat (p - q + 1))\<rfloor>"
1480       using assms by (simp add: algebra_simps powr_realpow[symmetric])
1481     also have "\<dots> = \<lfloor>(2 * ai - 1) / real ((2::int) ^ nat (p - q + 1))\<rfloor>"
1482       using `b < 0` assms
1483       by (simp add: floor_divide_eq_div floor_eq floor_divide_real_eq_div
1484         del: real_of_int_mult real_of_int_power real_of_int_diff)
1485     also have "\<dots> = \<lfloor>(2 * ai - 1) * 2 powr (q - p - 1)\<rfloor>"
1486       using assms by (simp add: algebra_simps divide_powr_uminus powr_realpow[symmetric])
1487     finally have ?thesis using `b < 0` by simp
1488   } ultimately show ?thesis by arith
1489 qed
1491 lemma
1492   log2_abs_int_add_less_half_sgn_eq:
1493   fixes ai::int and b::real
1494   assumes "abs b \<le> 1/2" "ai \<noteq> 0"
1495   shows "\<lfloor>log 2 \<bar>real ai + b\<bar>\<rfloor> = \<lfloor>log 2 \<bar>ai + sgn b / 2\<bar>\<rfloor>"
1496 proof cases
1497   assume "b = 0" thus ?thesis by simp
1498 next
1499   assume "b \<noteq> 0"
1500   def k \<equiv> "\<lfloor>log 2 \<bar>ai\<bar>\<rfloor>"
1501   hence "\<lfloor>log 2 \<bar>ai\<bar>\<rfloor> = k" by simp
1502   hence k: "2 powr k \<le> \<bar>ai\<bar>" "\<bar>ai\<bar> < 2 powr (k + 1)"
1503     by (simp_all add: floor_log_eq_powr_iff `ai \<noteq> 0`)
1504   have "k \<ge> 0"
1505     using assms by (auto simp: k_def)
1506   def r \<equiv> "\<bar>ai\<bar> - 2 ^ nat k"
1507   have r: "0 \<le> r" "r < 2 powr k"
1508     using `k \<ge> 0` k
1509     by (auto simp: r_def k_def algebra_simps powr_add abs_if powr_int)
1510   hence "r \<le> (2::int) ^ nat k - 1"
1511     using `k \<ge> 0` by (auto simp: powr_int)
1512   from this[simplified real_of_int_le_iff[symmetric]] `0 \<le> k`
1513   have r_le: "r \<le> 2 powr k - 1"
1514     by (auto simp: algebra_simps powr_int simp del: real_of_int_le_iff)
1516   have "\<bar>ai\<bar> = 2 powr k + r"
1517     using `k \<ge> 0` by (auto simp: k_def r_def powr_realpow[symmetric])
1519   have pos: "\<And>b::real. abs b < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)"
1520     using `0 \<le> k` `ai \<noteq> 0`
1521     by (auto simp add: r_def powr_realpow[symmetric] abs_if sgn_if algebra_simps
1522       split: split_if_asm)
1523   have less: "\<bar>sgn ai * b\<bar> < 1"
1524     and less': "\<bar>sgn (sgn ai * b) / 2\<bar> < 1"
1525     using `abs b \<le> _` by (auto simp: abs_if sgn_if split: split_if_asm)
1527   have floor_eq: "\<And>b::real. abs b \<le> 1 / 2 \<Longrightarrow>
1528       \<lfloor>log 2 (1 + (r + b) / 2 powr k)\<rfloor> = (if r = 0 \<and> b < 0 then -1 else 0)"
1529     using `k \<ge> 0` r r_le
1530     by (auto simp: floor_log_eq_powr_iff powr_minus_divide field_simps sgn_if)
1532   from `real \<bar>ai\<bar> = _` have "\<bar>ai + b\<bar> = 2 powr k + (r + sgn ai * b)"
1533     using `abs b <= _` `0 \<le> k` r
1534     by (auto simp add: sgn_if abs_if)
1535   also have "\<lfloor>log 2 \<dots>\<rfloor> = \<lfloor>log 2 (2 powr k + r + sgn (sgn ai * b) / 2)\<rfloor>"
1536   proof -
1537     have "2 powr k + (r + (sgn ai) * b) = 2 powr k * (1 + (r + sgn ai * b) / 2 powr k)"
1538       by (simp add: field_simps)
1539     also have "\<lfloor>log 2 \<dots>\<rfloor> = k + \<lfloor>log 2 (1 + (r + sgn ai * b) / 2 powr k)\<rfloor>"
1540       using pos[OF less]
1541       by (subst log_mult) (simp_all add: log_mult powr_mult field_simps)
1542     also
1543     let ?if = "if r = 0 \<and> sgn ai * b < 0 then -1 else 0"
1544     have "\<lfloor>log 2 (1 + (r + sgn ai * b) / 2 powr k)\<rfloor> = ?if"
1545       using `abs b <= _`
1546       by (intro floor_eq) (auto simp: abs_mult sgn_if)
1547     also
1548     have "\<dots> = \<lfloor>log 2 (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k)\<rfloor>"
1549       by (subst floor_eq) (auto simp: sgn_if)
1550     also have "k + \<dots> = \<lfloor>log 2 (2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k))\<rfloor>"
1551       unfolding floor_add2[symmetric]
1552       using pos[OF less'] `abs b \<le> _`
1553       by (simp add: field_simps add_log_eq_powr)
1554     also have "2 powr k * (1 + (r + sgn (sgn ai * b) / 2) / 2 powr k) =
1555         2 powr k + r + sgn (sgn ai * b) / 2"
1556       by (simp add: sgn_if field_simps)
1557     finally show ?thesis .
1558   qed
1559   also have "2 powr k + r + sgn (sgn ai * b) / 2 = \<bar>ai + sgn b / 2\<bar>"
1560     unfolding `real \<bar>ai\<bar> = _`[symmetric] using `ai \<noteq> 0`
1561     by (auto simp: abs_if sgn_if algebra_simps)
1562   finally show ?thesis .
1563 qed
1565 lemma compute_far_float_plus_down:
1566   fixes m1 e1 m2 e2::int and p::nat
1567   defines "k1 \<equiv> p - nat (bitlen \<bar>m1\<bar>)"
1568   assumes H: "bitlen \<bar>m2\<bar> \<le> e1 - e2 - k1 - 2" "m1 \<noteq> 0" "m2 \<noteq> 0" "e1 \<ge> e2"
1569   shows "float_plus_down p (Float m1 e1) (Float m2 e2) =
1570     float_round_down p (Float (m1 * 2 ^ (Suc (Suc k1)) + sgn m2) (e1 - int k1 - 2))"
1571 proof -
1572   let ?a = "real (Float m1 e1)"
1573   let ?b = "real (Float m2 e2)"
1574   let ?sum = "?a + ?b"
1575   let ?shift = "real e2 - real e1 + real k1 + 1"
1576   let ?m1 = "m1 * 2 ^ Suc k1"
1577   let ?m2 = "m2 * 2 powr ?shift"
1578   let ?m2' = "sgn m2 / 2"
1579   let ?e = "e1 - int k1 - 1"
1581   have sum_eq: "?sum = (?m1 + ?m2) * 2 powr ?e"
1582     by (auto simp: powr_add[symmetric] powr_mult[symmetric] algebra_simps
1583       powr_realpow[symmetric] powr_mult_base)
1585   have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
1586     by (auto simp: field_simps powr_add powr_mult_base powr_numeral powr_divide2[symmetric] abs_mult)
1587   also have "\<dots> \<le> 2 powr 0"
1588     using H by (intro powr_mono) auto
1589   finally have abs_m2_less_half: "\<bar>?m2\<bar> < 1 / 2"
1590     by simp
1592   hence "\<bar>real m2\<bar> < 2 powr -(?shift + 1)"
1593     unfolding powr_minus_divide by (auto simp: bitlen_def field_simps powr_mult_base abs_mult)
1594   also have "\<dots> \<le> 2 powr real (e1 - e2 - 2)"
1595     by simp
1596   finally have b_less_quarter: "\<bar>?b\<bar> < 1/4 * 2 powr real e1"
1597     by (simp add: powr_add field_simps powr_divide2[symmetric] powr_numeral abs_mult)
1598   also have "1/4 < \<bar>real m1\<bar> / 2" using `m1 \<noteq> 0` by simp
1599   finally have b_less_half_a: "\<bar>?b\<bar> < 1/2 * \<bar>?a\<bar>"
1600     by (simp add: algebra_simps powr_mult_base abs_mult)
1601   hence a_half_less_sum: "\<bar>?a\<bar> / 2 < \<bar>?sum\<bar>"
1602     by (auto simp: field_simps abs_if split: split_if_asm)
1604   from b_less_half_a have "\<bar>?b\<bar> < \<bar>?a\<bar>" "\<bar>?b\<bar> \<le> \<bar>?a\<bar>"
1605     by simp_all
1607   have "\<bar>real (Float m1 e1)\<bar> \<ge> 1/4 * 2 powr real e1"
1608     using `m1 \<noteq> 0`
1609     by (auto simp: powr_add powr_int bitlen_nonneg divide_right_mono abs_mult)
1610   hence "?sum \<noteq> 0" using b_less_quarter
1611     by (rule sum_neq_zeroI)
1612   hence "?m1 + ?m2 \<noteq> 0"
1613     unfolding sum_eq by (simp add: abs_mult zero_less_mult_iff)
1615   have "\<bar>real ?m1\<bar> \<ge> 2 ^ Suc k1" "\<bar>?m2'\<bar> < 2 ^ Suc k1"
1616     using `m1 \<noteq> 0` `m2 \<noteq> 0` by (auto simp: sgn_if less_1_mult abs_mult simp del: power.simps)
1617   hence sum'_nz: "?m1 + ?m2' \<noteq> 0"
1618     by (intro sum_neq_zeroI)
1620   have "\<lfloor>log 2 \<bar>real (Float m1 e1) + real (Float m2 e2)\<bar>\<rfloor> = \<lfloor>log 2 \<bar>?m1 + ?m2\<bar>\<rfloor> + ?e"
1621     using `?m1 + ?m2 \<noteq> 0`
1622     unfolding floor_add[symmetric] sum_eq
1623     by (simp add: abs_mult log_mult)
1624   also have "\<lfloor>log 2 \<bar>?m1 + ?m2\<bar>\<rfloor> = \<lfloor>log 2 \<bar>?m1 + sgn (real m2 * 2 powr ?shift) / 2\<bar>\<rfloor>"
1625     using abs_m2_less_half `m1 \<noteq> 0`
1626     by (intro log2_abs_int_add_less_half_sgn_eq) (auto simp: abs_mult)
1627   also have "sgn (real m2 * 2 powr ?shift) = sgn m2"
1628     by (auto simp: sgn_if zero_less_mult_iff less_not_sym)
1629   also
1630   have "\<bar>?m1 + ?m2'\<bar> * 2 powr ?e = \<bar>?m1 * 2 + sgn m2\<bar> * 2 powr (?e - 1)"
1631     by (auto simp: field_simps powr_minus[symmetric] powr_divide2[symmetric] powr_mult_base)
1632   hence "\<lfloor>log 2 \<bar>?m1 + ?m2'\<bar>\<rfloor> + ?e = \<lfloor>log 2 \<bar>real (Float (?m1 * 2 + sgn m2) (?e - 1))\<bar>\<rfloor>"
1633     using `?m1 + ?m2' \<noteq> 0`
1634     unfolding floor_add[symmetric]
1635     by (simp add: log_add_eq_powr abs_mult_pos)
1636   finally
1637   have "\<lfloor>log 2 \<bar>?sum\<bar>\<rfloor> = \<lfloor>log 2 \<bar>real (Float (?m1*2 + sgn m2) (?e - 1))\<bar>\<rfloor>" .
1638   hence "plus_down p (Float m1 e1) (Float m2 e2) =
1639       truncate_down p (Float (?m1*2 + sgn m2) (?e - 1))"
1640     unfolding plus_down_def
1641   proof (rule truncate_down_log2_eqI)
1642     let ?f = "(int p - \<lfloor>log 2 \<bar>real (Float m1 e1) + real (Float m2 e2)\<bar>\<rfloor> - 1)"
1643     let ?ai = "m1 * 2 ^ (Suc k1)"
1644     have "\<lfloor>(?a + ?b) * 2 powr real ?f\<rfloor> = \<lfloor>(real (2 * ?ai) + sgn ?b) * 2 powr real (?f - - ?e - 1)\<rfloor>"
1645     proof (rule floor_sum_times_2_powr_sgn_eq)
1646       show "?a * 2 powr real (-?e) = real ?ai"
1647         by (simp add: powr_add powr_realpow[symmetric] powr_divide2[symmetric])
1648       show "\<bar>?b * 2 powr real (-?e + 1)\<bar> \<le> 1"
1649         using abs_m2_less_half
1650         by (simp add: abs_mult powr_add[symmetric] algebra_simps powr_mult_base)
1651     next
1652       have "e1 + \<lfloor>log 2 \<bar>real m1\<bar>\<rfloor> - 1 = \<lfloor>log 2 \<bar>?a\<bar>\<rfloor> - 1"
1653         using `m1 \<noteq> 0`
1654         by (simp add: floor_add2[symmetric] algebra_simps log_mult abs_mult del: floor_add2)
1655       also have "\<dots> \<le> \<lfloor>log 2 \<bar>?a + ?b\<bar>\<rfloor>"
1656         using a_half_less_sum `m1 \<noteq> 0` `?sum \<noteq> 0`
1657         unfolding floor_subtract[symmetric]
1658         by (auto simp add: log_minus_eq_powr powr_minus_divide
1659           intro!: floor_mono)
1660       finally
1661       have "int p - \<lfloor>log 2 \<bar>?a + ?b\<bar>\<rfloor> \<le> p - (bitlen \<bar>m1\<bar>) - e1 + 2"
1662         by (auto simp: algebra_simps bitlen_def `m1 \<noteq> 0`)
1663       also have "\<dots> \<le> 1 - ?e"
1664         using bitlen_nonneg[of "\<bar>m1\<bar>"] by (simp add: k1_def)
1665       finally show "?f \<le> - ?e" by simp
1666     qed
1667     also have "sgn ?b = sgn m2"
1668       using powr_gt_zero[of 2 e2]
1669       by (auto simp add: sgn_if zero_less_mult_iff simp del: powr_gt_zero)
1670     also have "\<lfloor>(real (2 * ?m1) + real (sgn m2)) * 2 powr real (?f - - ?e - 1)\<rfloor> =
1671         \<lfloor>Float (?m1 * 2 + sgn m2) (?e - 1) * 2 powr ?f\<rfloor>"
1672       by (simp add: powr_add[symmetric] algebra_simps powr_realpow[symmetric])
1673     finally
1674     show "\<lfloor>(?a + ?b) * 2 powr ?f\<rfloor> = \<lfloor>real (Float (?m1 * 2 + sgn m2) (?e - 1)) * 2 powr ?f\<rfloor>" .
1675   qed
1676   thus ?thesis
1677     by transfer (simp add: plus_down_def ac_simps Let_def)
1678 qed
1680 lemma compute_float_plus_down_naive[code]: "float_plus_down p x y = float_round_down p (x + y)"
1681   by transfer (auto simp: plus_down_def)
1683 lemma compute_float_plus_down[code]:
1684   fixes p::nat and m1 e1 m2 e2::int
1685   shows "float_plus_down p (Float m1 e1) (Float m2 e2) =
1686     (if m1 = 0 then float_round_down p (Float m2 e2)
1687     else if m2 = 0 then float_round_down p (Float m1 e1)
1688     else (if e1 \<ge> e2 then
1689       (let
1690         k1 = p - nat (bitlen \<bar>m1\<bar>)
1691       in
1692         if bitlen \<bar>m2\<bar> > e1 - e2 - k1 - 2 then float_round_down p ((Float m1 e1) + (Float m2 e2))
1693         else float_round_down p (Float (m1 * 2 ^ (Suc (Suc k1)) + sgn m2) (e1 - int k1 - 2)))
1694     else float_plus_down p (Float m2 e2) (Float m1 e1)))"
1695 proof -
1696   {
1697     assume H: "bitlen \<bar>m2\<bar> \<le> e1 - e2 - (p - nat (bitlen \<bar>m1\<bar>)) - 2" "m1 \<noteq> 0" "m2 \<noteq> 0" "e1 \<ge> e2"
1698     note compute_far_float_plus_down[OF H]
1699   }
1700   thus ?thesis
1701     by transfer (simp add: Let_def plus_down_def ac_simps)
1702 qed
1703 hide_fact (open) compute_far_float_plus_down
1704 hide_fact (open) compute_float_plus_down
1706 lemma compute_float_plus_up[code]: "float_plus_up p x y = - float_plus_down p (-x) (-y)"
1707   using truncate_down_uminus_eq[of p "x + y"]
1708   by transfer (simp add: plus_down_def plus_up_def ac_simps)
1709 hide_fact (open) compute_float_plus_up
1711 lemma mantissa_zero[simp]: "mantissa 0 = 0"
1712 by (metis mantissa_0 zero_float.abs_eq)
1715 subsection {* Lemmas needed by Approximate *}
1717 lemma Float_num[simp]: shows
1718    "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
1719    "real (Float 1 (- 1)) = 1/2" and "real (Float 1 (- 2)) = 1/4" and "real (Float 1 (- 3)) = 1/8" and
1720    "real (Float (- 1) 0) = -1" and "real (Float (number_of n) 0) = number_of n"
1721 using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"] two_powr_int_float[of "-3"]
1722 using powr_realpow[of 2 2] powr_realpow[of 2 3]
1723 using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
1724 by auto
1726 lemma real_of_Float_int[simp]: "real (Float n 0) = real n" by simp
1728 lemma float_zero[simp]: "real (Float 0 e) = 0" by simp
1730 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
1731 by arith
1733 lemma lapprox_rat:
1734   shows "real (lapprox_rat prec x y) \<le> real x / real y"
1735   using round_down by (simp add: lapprox_rat_def)
1737 lemma mult_div_le: fixes a b:: int assumes "b > 0" shows "a \<ge> b * (a div b)"
1738 proof -
1739   from zmod_zdiv_equality'[of a b]
1740   have "a = b * (a div b) + a mod b" by simp
1741   also have "... \<ge> b * (a div b) + 0" apply (rule add_left_mono) apply (rule pos_mod_sign)
1742   using assms by simp
1743   finally show ?thesis by simp
1744 qed
1746 lemma lapprox_rat_nonneg:
1747   fixes n x y
1748   assumes "0 \<le> x" and "0 \<le> y"
1749   shows "0 \<le> real (lapprox_rat n x y)"
1750   using assms by (auto simp: lapprox_rat_def simp: round_down_nonneg)
1752 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
1753   using round_up by (simp add: rapprox_rat_def)
1755 lemma rapprox_rat_le1:
1756   fixes n x y
1757   assumes xy: "0 \<le> x" "0 < y" "x \<le> y"
1758   shows "real (rapprox_rat n x y) \<le> 1"
1759 proof -
1760   have "bitlen \<bar>x\<bar> \<le> bitlen \<bar>y\<bar>"
1761     using xy unfolding bitlen_def by (auto intro!: floor_mono)
1762   from this assms show ?thesis
1763     by transfer (auto intro!: round_up_le1 simp: rat_precision_def)
1764 qed
1766 lemma rapprox_rat_nonneg_nonpos:
1767   "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
1768   by transfer (simp add: round_up_le0 divide_nonneg_nonpos)
1770 lemma rapprox_rat_nonpos_nonneg:
1771   "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
1772   by transfer (simp add: round_up_le0 divide_nonpos_nonneg)
1774 lemma real_divl: "real_divl prec x y \<le> x / y"
1775   by (simp add: real_divl_def round_down)
1777 lemma real_divr: "x / y \<le> real_divr prec x y"
1778   using round_up by (simp add: real_divr_def)
1780 lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
1781   by transfer (rule real_divl)
1783 lemma real_divl_lower_bound:
1784   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real_divl prec x y"
1785   by (simp add: real_divl_def round_down_nonneg)
1787 lemma float_divl_lower_bound:
1788   "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> real (float_divl prec x y)"
1789   by transfer (rule real_divl_lower_bound)
1791 lemma exponent_1: "exponent 1 = 0"
1792   using exponent_float[of 1 0] by (simp add: one_float_def)
1794 lemma mantissa_1: "mantissa 1 = 1"
1795   using mantissa_float[of 1 0] by (simp add: one_float_def)
1797 lemma bitlen_1: "bitlen 1 = 1"
1798   by (simp add: bitlen_def)
1800 lemma mantissa_eq_zero_iff: "mantissa x = 0 \<longleftrightarrow> x = 0"
1801 proof
1802   assume "mantissa x = 0" hence z: "0 = real x" using mantissa_exponent by simp
1803   show "x = 0" by (simp add: zero_float_def z)
1804 qed (simp add: zero_float_def)
1806 lemma float_upper_bound: "x \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x)"
1807 proof (cases "x = 0", simp)
1808   assume "x \<noteq> 0" hence "mantissa x \<noteq> 0" using mantissa_eq_zero_iff by auto
1809   have "x = mantissa x * 2 powr (exponent x)" by (rule mantissa_exponent)
1810   also have "mantissa x \<le> \<bar>mantissa x\<bar>" by simp
1811   also have "... \<le> 2 powr (bitlen \<bar>mantissa x\<bar>)"
1812     using bitlen_bounds[of "\<bar>mantissa x\<bar>"] bitlen_nonneg `mantissa x \<noteq> 0`
1813     by (simp add: powr_int) (simp only: two_real_int int_of_reals real_of_int_abs[symmetric]
1814       real_of_int_le_iff less_imp_le)
1815   finally show ?thesis by (simp add: powr_add)
1816 qed
1818 lemma real_divl_pos_less1_bound:
1819   assumes "0 < x" "x \<le> 1" "prec \<ge> 1"
1820   shows "1 \<le> real_divl prec 1 x"
1821 proof -
1822   have "log 2 x \<le> real prec + real \<lfloor>log 2 x\<rfloor>" using `prec \<ge> 1` by arith
1823   from this assms show ?thesis
1824     by (simp add: real_divl_def log_divide round_down_ge1)
1825 qed
1827 lemma float_divl_pos_less1_bound:
1828   "0 < real x \<Longrightarrow> real x \<le> 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
1829   by (transfer, rule real_divl_pos_less1_bound)
1831 lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
1832   by transfer (rule real_divr)
1834 lemma real_divr_pos_less1_lower_bound: assumes "0 < x" and "x \<le> 1" shows "1 \<le> real_divr prec 1 x"
1835 proof -
1836   have "1 \<le> 1 / x" using `0 < x` and `x <= 1` by auto
1837   also have "\<dots> \<le> real_divr prec 1 x" using real_divr[where x=1 and y=x] by auto
1838   finally show ?thesis by auto
1839 qed
1841 lemma float_divr_pos_less1_lower_bound: "0 < x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 1 \<le> float_divr prec 1 x"
1842   by transfer (rule real_divr_pos_less1_lower_bound)
1844 lemma real_divr_nonpos_pos_upper_bound:
1845   "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real_divr prec x y \<le> 0"
1846   by (simp add: real_divr_def round_up_le0 divide_le_0_iff)
1848 lemma float_divr_nonpos_pos_upper_bound:
1849   "real x \<le> 0 \<Longrightarrow> 0 \<le> real y \<Longrightarrow> real (float_divr prec x y) \<le> 0"
1850   by transfer (rule real_divr_nonpos_pos_upper_bound)
1852 lemma real_divr_nonneg_neg_upper_bound:
1853   "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real_divr prec x y \<le> 0"
1854   by (simp add: real_divr_def round_up_le0 divide_le_0_iff)
1856 lemma float_divr_nonneg_neg_upper_bound:
1857   "0 \<le> real x \<Longrightarrow> real y \<le> 0 \<Longrightarrow> real (float_divr prec x y) \<le> 0"
1858   by transfer (rule real_divr_nonneg_neg_upper_bound)
1860 lemma truncate_up_nonneg_mono:
1861   assumes "0 \<le> x" "x \<le> y"
1862   shows "truncate_up prec x \<le> truncate_up prec y"
1863 proof -
1864   {
1865     assume "\<lfloor>log 2 x\<rfloor> = \<lfloor>log 2 y\<rfloor>"
1866     hence ?thesis
1867       using assms
1868       by (auto simp: truncate_up_def round_up_def intro!: ceiling_mono)
1869   } moreover {
1870     assume "0 < x"
1871     hence "log 2 x \<le> log 2 y" using assms by auto
1872     moreover
1873     assume "\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>"
1874     ultimately have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
1875       unfolding atomize_conj
1876       by (metis floor_less_cancel linorder_cases not_le)
1877     have "truncate_up prec x =
1878       real \<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> * 2 powr - real (int prec - \<lfloor>log 2 x\<rfloor> - 1)"
1879       using assms by (simp add: truncate_up_def round_up_def)
1880     also have "\<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> (2 ^ prec)"
1881     proof (unfold ceiling_le_eq)
1882       have "x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> x * (2 powr real prec / (2 powr log 2 x))"
1883         using real_of_int_floor_add_one_ge[of "log 2 x"] assms
1884         by (auto simp add: algebra_simps powr_divide2 intro!: mult_left_mono)
1885       thus "x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> real ((2::int) ^ prec)"
1886         using `0 < x` by (simp add: powr_realpow)
1887     qed
1888     hence "real \<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> 2 powr int prec"
1889       by (auto simp: powr_realpow)
1890     also
1891     have "2 powr - real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> 2 powr - real (int prec - \<lfloor>log 2 y\<rfloor>)"
1892       using logless flogless by (auto intro!: floor_mono)
1893     also have "2 powr real (int prec) \<le> 2 powr (log 2 y + real (int prec - \<lfloor>log 2 y\<rfloor>))"
1894       using assms `0 < x`
1895       by (auto simp: algebra_simps)
1896     finally have "truncate_up prec x \<le> 2 powr (log 2 y + real (int prec - \<lfloor>log 2 y\<rfloor>)) * 2 powr - real (int prec - \<lfloor>log 2 y\<rfloor>)"
1897       by simp
1898     also have "\<dots> = 2 powr (log 2 y + real (int prec - \<lfloor>log 2 y\<rfloor>) - real (int prec - \<lfloor>log 2 y\<rfloor>))"
1899       by (subst powr_add[symmetric]) simp
1900     also have "\<dots> = y"
1901       using `0 < x` assms
1902       by (simp add: powr_add)
1903     also have "\<dots> \<le> truncate_up prec y"
1904       by (rule truncate_up)
1905     finally have ?thesis .
1906   } moreover {
1907     assume "~ 0 < x"
1908     hence ?thesis
1909       using assms
1910       by (auto intro!: truncate_up_le)
1911   } ultimately show ?thesis
1912     by blast
1913 qed
1915 lemma truncate_up_switch_sign_mono:
1916   assumes "x \<le> 0" "0 \<le> y"
1917   shows "truncate_up prec x \<le> truncate_up prec y"
1918 proof -
1919   note truncate_up_nonpos[OF `x \<le> 0`]
1920   also note truncate_up_le[OF `0 \<le> y`]
1921   finally show ?thesis .
1922 qed
1924 lemma truncate_down_zeroprec_mono:
1925   assumes "0 < x" "x \<le> y"
1926   shows "truncate_down 0 x \<le> truncate_down 0 y"
1927 proof -
1928   have "x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1) = x * inverse (2 powr ((real \<lfloor>log 2 x\<rfloor> + 1)))"
1929     by (simp add: powr_divide2[symmetric] powr_add powr_minus inverse_eq_divide)
1930   also have "\<dots> = 2 powr (log 2 x - (real \<lfloor>log 2 x\<rfloor>) - 1)"
1931     using `0 < x`
1932     by (auto simp: field_simps powr_add powr_divide2[symmetric])
1933   also have "\<dots> < 2 powr 0"
1934     using real_of_int_floor_add_one_gt
1935     unfolding neg_less_iff_less
1936     by (intro powr_less_mono) (auto simp: algebra_simps)
1937   finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> < 1"
1938     unfolding less_ceiling_eq real_of_int_minus real_of_one
1939     by simp
1940   moreover
1941   have "0 \<le> \<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>"
1942     using `x > 0` by auto
1943   ultimately have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> \<in> {0 ..< 1}"
1944     by simp
1945   also have "\<dots> \<subseteq> {0}" by auto
1946   finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0" by simp
1947   with assms show ?thesis
1948     by (auto simp: truncate_down_def round_down_def)
1949 qed
1951 lemma truncate_down_switch_sign_mono:
1952   assumes "x \<le> 0" "0 \<le> y"
1953   assumes "x \<le> y"
1954   shows "truncate_down prec x \<le> truncate_down prec y"
1955 proof -
1956   note truncate_down_le[OF `x \<le> 0`]
1957   also note truncate_down_nonneg[OF `0 \<le> y`]
1958   finally show ?thesis .
1959 qed
1961 lemma truncate_down_nonneg_mono:
1962   assumes "0 \<le> x" "x \<le> y"
1963   shows "truncate_down prec x \<le> truncate_down prec y"
1964 proof -
1965   {
1966     assume "0 < x" "prec = 0"
1967     with assms have ?thesis
1968       by (simp add: truncate_down_zeroprec_mono)
1969   } moreover {
1970     assume "~ 0 < x"
1971     with assms have "x = 0" "0 \<le> y" by simp_all
1972     hence ?thesis
1973       by (auto intro!: truncate_down_nonneg)
1974   } moreover {
1975     assume "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
1976     hence ?thesis
1977       using assms
1978       by (auto simp: truncate_down_def round_down_def intro!: floor_mono)
1979   } moreover {
1980     assume "0 < x"
1981     hence "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y" using assms by auto
1982     moreover
1983     assume "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
1984     ultimately have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
1985       unfolding atomize_conj abs_of_pos[OF `0 < x`] abs_of_pos[OF `0 < y`]
1986       by (metis floor_less_cancel linorder_cases not_le)
1987     assume "prec \<noteq> 0" hence [simp]: "prec \<ge> Suc 0" by auto
1988     have "2 powr (prec - 1) \<le> y * 2 powr real (prec - 1) / (2 powr log 2 y)"
1989       using `0 < y`
1990       by simp
1991     also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
1992       using `0 \<le> y` `0 \<le> x` assms(2)
1993       by (auto intro!: powr_mono divide_left_mono
1994         simp: real_of_nat_diff powr_add
1995         powr_divide2[symmetric])
1996     also have "\<dots> = y * 2 powr real prec / (2 powr real \<lfloor>log 2 y\<rfloor> * 2)"
1997       by (auto simp: powr_add)
1998     finally have "(2 ^ (prec - 1)) \<le> \<lfloor>y * 2 powr real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>"
1999       using `0 \<le> y`
2000       by (auto simp: powr_divide2[symmetric] le_floor_eq powr_realpow)
2001     hence "(2 ^ (prec - 1)) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1) \<le> truncate_down prec y"
2002       by (auto simp: truncate_down_def round_down_def)
2003     moreover
2004     {
2005       have "x = 2 powr (log 2 \<bar>x\<bar>)" using `0 < x` by simp
2006       also have "\<dots> \<le> (2 ^ (prec )) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)"
2007         using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"]
2008         by (auto simp: powr_realpow[symmetric] powr_add[symmetric] algebra_simps)
2009       also
2010       have "2 powr - real (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) \<le> 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)"
2011         using logless flogless `x > 0` `y > 0`
2012         by (auto intro!: floor_mono)
2013       finally have "x \<le> (2 ^ (prec - 1)) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)"
2014         by (auto simp: powr_realpow[symmetric] powr_divide2[symmetric] assms real_of_nat_diff)
2015     } ultimately have ?thesis
2016       by (metis dual_order.trans truncate_down)
2017   } ultimately show ?thesis by blast
2018 qed
2020 lemma truncate_down_eq_truncate_up: "truncate_down p x = - truncate_up p (-x)"
2021   and truncate_up_eq_truncate_down: "truncate_up p x = - truncate_down p (-x)"
2022   by (auto simp: truncate_up_uminus_eq truncate_down_uminus_eq)
2024 lemma truncate_down_mono: "x \<le> y \<Longrightarrow> truncate_down p x \<le> truncate_down p y"
2025   apply (cases "0 \<le> x")
2026   apply (rule truncate_down_nonneg_mono, assumption+)
2027   apply (simp add: truncate_down_eq_truncate_up)
2028   apply (cases "0 \<le> y")
2029   apply (auto intro: truncate_up_nonneg_mono truncate_up_switch_sign_mono)
2030   done
2032 lemma truncate_up_mono: "x \<le> y \<Longrightarrow> truncate_up p x \<le> truncate_up p y"
2033   by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
2035 lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
2036  apply (auto simp: zero_float_def mult_le_0_iff)
2037  using powr_gt_zero[of 2 b] by simp
2039 lemma real_of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
2040   unfolding pprt_def sup_float_def max_def sup_real_def by auto
2042 lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
2043   unfolding nprt_def inf_float_def min_def inf_real_def by auto
2045 lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor .
2047 lemma compute_int_floor_fl[code]:
2048   "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
2049   by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
2050 hide_fact (open) compute_int_floor_fl
2052 lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
2054 lemma compute_floor_fl[code]:
2055   "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
2056   by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
2057 hide_fact (open) compute_floor_fl
2059 lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
2061 lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
2063 lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
2064 proof (cases "floor_fl x = float_of 0")
2065   case True
2066   then show ?thesis by (simp add: floor_fl_def)
2067 next
2068   case False
2069   have eq: "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
2070   obtain i where "\<lfloor>real x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
2071     by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
2072   then show ?thesis by simp
2073 qed
2075 lemma compute_mantissa[code]:
2076   "mantissa (Float m e) = (if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
2077   by (auto simp: mantissa_float Float.abs_eq)
2079 lemma compute_exponent[code]:
2080   "exponent (Float m e) = (if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
2081   by (auto simp: exponent_float Float.abs_eq)
2083 end