src/HOL/Library/Float.thy
 author wenzelm Tue Feb 21 16:28:18 2012 +0100 (2012-02-21) changeset 46573 8c4c5c8dcf7a parent 46028 9f113cdf3d66 child 46670 e9aa6d151329 permissions -rw-r--r--
misc tuning;
more indentation;
1 (*  Title:      HOL/Library/Float.thy
2     Author:     Steven Obua 2008
3     Author:     Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
4 *)
6 header {* Floating-Point Numbers *}
8 theory Float
9 imports Complex_Main Lattice_Algebras
10 begin
12 definition pow2 :: "int \<Rightarrow> real" where
13   [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
15 datatype float = Float int int
17 primrec of_float :: "float \<Rightarrow> real" where
18   "of_float (Float a b) = real a * pow2 b"
21   real_of_float_def [code_unfold]: "real == of_float"
23 declare [[coercion "% x . Float x 0"]]
24 declare [[coercion "real::float\<Rightarrow>real"]]
26 primrec mantissa :: "float \<Rightarrow> int" where
27   "mantissa (Float a b) = a"
29 primrec scale :: "float \<Rightarrow> int" where
30   "scale (Float a b) = b"
32 instantiation float :: zero
33 begin
34 definition zero_float where "0 = Float 0 0"
35 instance ..
36 end
38 instantiation float :: one
39 begin
40 definition one_float where "1 = Float 1 0"
41 instance ..
42 end
44 instantiation float :: number
45 begin
46 definition number_of_float where "number_of n = Float n 0"
47 instance ..
48 end
50 lemma number_of_float_Float:
51   "number_of k = Float (number_of k) 0"
52   by (simp add: number_of_float_def number_of_is_id)
54 declare number_of_float_Float [symmetric, code_abbrev]
56 lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
57   unfolding real_of_float_def using of_float.simps .
59 lemma real_of_float_neg_exp: "e < 0 \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
60 lemma real_of_float_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
61 lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto
63 lemma Float_num[simp]: shows
64    "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
65    "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
66    "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
67   by auto
69 lemma float_number_of[simp]: "real (number_of x :: float) = number_of x"
70   by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
72 lemma float_number_of_int[simp]: "real (Float n 0) = real n"
73   by simp
75 lemma pow2_0[simp]: "pow2 0 = 1" by simp
76 lemma pow2_1[simp]: "pow2 1 = 2" by simp
77 lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp
79 lemma pow2_powr: "pow2 a = 2 powr a"
80   by (simp add: powr_realpow[symmetric] powr_minus)
82 declare pow2_def[simp del]
84 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
87 lemma pow2_diff: "pow2 (a - b) = pow2 a / pow2 b"
88   by (simp add: pow2_powr powr_divide2)
90 lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
93 lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto
95 lemma float_split: "\<exists> a b. x = Float a b" by (cases x) auto
97 lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split)
99 lemma float_zero[simp]: "real (Float 0 e) = 0" by simp
101 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
102 by arith
104 function normfloat :: "float \<Rightarrow> float" where
105   "normfloat (Float a b) =
106     (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1))
107      else if a=0 then Float 0 0 else Float a b)"
108 by pat_completeness auto
109 termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less)
110 declare normfloat.simps[simp del]
112 theorem normfloat[symmetric, simp]: "real f = real (normfloat f)"
113 proof (induct f rule: normfloat.induct)
114   case (1 a b)
115   have real2: "2 = real (2::int)"
116     by auto
117   show ?case
118     apply (subst normfloat.simps)
119     apply auto
120     apply (subst 1[symmetric])
121     apply (auto simp add: pow2_add even_def)
122     done
123 qed
125 lemma pow2_neq_zero[simp]: "pow2 x \<noteq> 0"
126   by (auto simp add: pow2_def)
128 lemma pow2_int: "pow2 (int c) = 2^c"
129   by (simp add: pow2_def)
131 lemma zero_less_pow2[simp]: "0 < pow2 x"
132   by (simp add: pow2_powr)
134 lemma normfloat_imp_odd_or_zero:
135   "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
136 proof (induct f rule: normfloat.induct)
137   case (1 u v)
138   from 1 have ab: "normfloat (Float u v) = Float a b" by auto
139   {
140     assume eu: "even u"
141     assume z: "u \<noteq> 0"
142     have "normfloat (Float u v) = normfloat (Float (u div 2) (v + 1))"
143       apply (subst normfloat.simps)
144       by (simp add: eu z)
145     with ab have "normfloat (Float (u div 2) (v + 1)) = Float a b" by simp
146     with 1 eu z have ?case by auto
147   }
148   note case1 = this
149   {
150     assume "odd u \<or> u = 0"
151     then have ou: "\<not> (u \<noteq> 0 \<and> even u)" by auto
152     have "normfloat (Float u v) = (if u = 0 then Float 0 0 else Float u v)"
153       apply (subst normfloat.simps)
154       apply (simp add: ou)
155       done
156     with ab have "Float a b = (if u = 0 then Float 0 0 else Float u v)" by auto
157     then have ?case
158       apply (case_tac "u=0")
159       apply (auto)
160       by (insert ou, auto)
161   }
162   note case2 = this
163   show ?case
164     apply (case_tac "odd u \<or> u = 0")
165     apply (rule case2)
166     apply simp
167     apply (rule case1)
168     apply auto
169     done
170 qed
172 lemma float_eq_odd_helper:
173   assumes odd: "odd a'"
174     and floateq: "real (Float a b) = real (Float a' b')"
175   shows "b \<le> b'"
176 proof -
177   from odd have "a' \<noteq> 0" by auto
178   with floateq have a': "real a' = real a * pow2 (b - b')"
179     by (simp add: pow2_diff field_simps)
181   {
182     assume bcmp: "b > b'"
183     then have "\<exists>c::nat. b - b' = int c + 1"
184       by arith
185     then guess c ..
186     with a' have "real a' = real (a * 2^c * 2)"
188     with odd have False
189       unfolding real_of_int_inject by simp
190   }
191   then show ?thesis by arith
192 qed
194 lemma float_eq_odd:
195   assumes odd1: "odd a"
196     and odd2: "odd a'"
197     and floateq: "real (Float a b) = real (Float a' b')"
198   shows "a = a' \<and> b = b'"
199 proof -
200   from
201      float_eq_odd_helper[OF odd2 floateq]
202      float_eq_odd_helper[OF odd1 floateq[symmetric]]
203   have beq: "b = b'" by arith
204   with floateq show ?thesis by auto
205 qed
207 theorem normfloat_unique:
208   assumes real_of_float_eq: "real f = real g"
209   shows "normfloat f = normfloat g"
210 proof -
211   from float_split[of "normfloat f"] obtain a b where normf:"normfloat f = Float a b" by auto
212   from float_split[of "normfloat g"] obtain a' b' where normg:"normfloat g = Float a' b'" by auto
213   have "real (normfloat f) = real (normfloat g)"
214     by (simp add: real_of_float_eq)
215   then have float_eq: "real (Float a b) = real (Float a' b')"
216     by (simp add: normf normg)
217   have ab: "odd a \<or> (a = 0 \<and> b = 0)" by (rule normfloat_imp_odd_or_zero[OF normf])
218   have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg])
219   {
220     assume odd: "odd a"
221     then have "a \<noteq> 0" by (simp add: even_def) arith
222     with float_eq have "a' \<noteq> 0" by auto
223     with ab' have "odd a'" by simp
224     from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd)
225   }
226   note odd_case = this
227   {
228     assume even: "even a"
229     with ab have a0: "a = 0" by simp
230     with float_eq have a0': "a' = 0" by auto
231     from a0 a0' ab ab' have "a = a' \<and> b = b'" by auto
232   }
233   note even_case = this
234   from odd_case even_case show ?thesis
235     apply (simp add: normf normg)
236     apply (case_tac "even a")
237     apply auto
238     done
239 qed
241 instantiation float :: plus
242 begin
243 fun plus_float where
244 [simp del]: "(Float a_m a_e) + (Float b_m b_e) =
245      (if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e - a_e))) a_e
246                    else Float (a_m * 2^(nat (a_e - b_e)) + b_m) b_e)"
247 instance ..
248 end
250 instantiation float :: uminus
251 begin
252 primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
253 instance ..
254 end
256 instantiation float :: minus
257 begin
258 definition minus_float where "(z::float) - w = z + (- w)"
259 instance ..
260 end
262 instantiation float :: times
263 begin
264 fun times_float where [simp del]: "(Float a_m a_e) * (Float b_m b_e) = Float (a_m * b_m) (a_e + b_e)"
265 instance ..
266 end
268 primrec float_pprt :: "float \<Rightarrow> float" where
269   "float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
271 primrec float_nprt :: "float \<Rightarrow> float" where
272   "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))"
274 instantiation float :: ord
275 begin
276 definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w"
277 definition less_float_def: "z < (w :: float) \<equiv> real z < real w"
278 instance ..
279 end
281 lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)"
282   by (cases a, cases b) (simp add: algebra_simps plus_float.simps,
285 lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
286   by (cases a) simp
288 lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
289   by (cases a, cases b) (simp add: minus_float_def)
291 lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)"
292   by (cases a, cases b) (simp add: times_float.simps pow2_add)
294 lemma real_of_float_0[simp]: "real (0 :: float) = 0"
295   by (auto simp add: zero_float_def)
297 lemma real_of_float_1[simp]: "real (1 :: float) = 1"
298   by (auto simp add: one_float_def)
300 lemma zero_le_float:
301   "(0 <= real (Float a b)) = (0 <= a)"
302   apply auto
303   apply (auto simp add: zero_le_mult_iff)
304   apply (insert zero_less_pow2[of b])
305   apply (simp_all)
306   done
308 lemma float_le_zero:
309   "(real (Float a b) <= 0) = (a <= 0)"
310   apply auto
311   apply (auto simp add: mult_le_0_iff)
312   apply (insert zero_less_pow2[of b])
313   apply auto
314   done
316 lemma zero_less_float:
317   "(0 < real (Float a b)) = (0 < a)"
318   apply auto
319   apply (auto simp add: zero_less_mult_iff)
320   apply (insert zero_less_pow2[of b])
321   apply (simp_all)
322   done
324 lemma float_less_zero:
325   "(real (Float a b) < 0) = (a < 0)"
326   apply auto
327   apply (auto simp add: mult_less_0_iff)
328   apply (insert zero_less_pow2[of b])
329   apply (simp_all)
330   done
332 declare real_of_float_simp[simp del]
334 lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
335   by (cases a) (auto simp add: zero_le_float float_le_zero)
337 lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)"
338   by (cases a) (auto simp add: zero_le_float float_le_zero)
340 instance float :: ab_semigroup_add
341 proof (intro_classes)
342   fix a b c :: float
343   show "a + b + c = a + (b + c)"
344     by (cases a, cases b, cases c)
345       (auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
346 next
347   fix a b :: float
348   show "a + b = b + a"
349     by (cases a, cases b) (simp add: plus_float.simps)
350 qed
352 instance float :: comm_monoid_mult
353 proof (intro_classes)
354   fix a b c :: float
355   show "a * b * c = a * (b * c)"
356     by (cases a, cases b, cases c) (simp add: times_float.simps)
357 next
358   fix a b :: float
359   show "a * b = b * a"
360     by (cases a, cases b) (simp add: times_float.simps)
361 next
362   fix a :: float
363   show "1 * a = a"
364     by (cases a) (simp add: times_float.simps one_float_def)
365 qed
367 (* Floats do NOT form a cancel_semigroup_add: *)
368 lemma "0 + Float 0 1 = 0 + Float 0 2"
369   by (simp add: plus_float.simps zero_float_def)
371 instance float :: comm_semiring
372 proof (intro_classes)
373   fix a b c :: float
374   show "(a + b) * c = a * c + b * c"
375     by (cases a, cases b, cases c) (simp add: plus_float.simps times_float.simps algebra_simps)
376 qed
378 (* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *)
380 instance float :: zero_neq_one
381 proof (intro_classes)
382   show "(0::float) \<noteq> 1"
383     by (simp add: zero_float_def one_float_def)
384 qed
386 lemma float_le_simp: "((x::float) \<le> y) = (0 \<le> y - x)"
387   by (auto simp add: le_float_def)
389 lemma float_less_simp: "((x::float) < y) = (0 < y - x)"
390   by (auto simp add: less_float_def)
392 lemma real_of_float_min: "real (min x y :: float) = min (real x) (real y)" unfolding min_def le_float_def by auto
393 lemma real_of_float_max: "real (max a b :: float) = max (real a) (real b)" unfolding max_def le_float_def by auto
395 lemma float_power: "real (x ^ n :: float) = real x ^ n"
396   by (induct n) simp_all
398 lemma zero_le_pow2[simp]: "0 \<le> pow2 s"
399   apply (subgoal_tac "0 < pow2 s")
400   apply (auto simp only:)
401   apply auto
402   done
404 lemma pow2_less_0_eq_False[simp]: "(pow2 s < 0) = False"
405   apply auto
406   apply (subgoal_tac "0 \<le> pow2 s")
407   apply simp
408   apply simp
409   done
411 lemma pow2_le_0_eq_False[simp]: "(pow2 s \<le> 0) = False"
412   apply auto
413   apply (subgoal_tac "0 < pow2 s")
414   apply simp
415   apply simp
416   done
418 lemma float_pos_m_pos: "0 < Float m e \<Longrightarrow> 0 < m"
419   unfolding less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff
420   by auto
422 lemma float_pos_less1_e_neg: assumes "0 < Float m e" and "Float m e < 1" shows "e < 0"
423 proof -
424   have "0 < m" using float_pos_m_pos `0 < Float m e` by auto
425   hence "0 \<le> real m" and "1 \<le> real m" by auto
427   show "e < 0"
428   proof (rule ccontr)
429     assume "\<not> e < 0" hence "0 \<le> e" by auto
430     hence "1 \<le> pow2 e" unfolding pow2_def by auto
431     from mult_mono[OF `1 \<le> real m` this `0 \<le> real m`]
432     have "1 \<le> Float m e" by (simp add: le_float_def real_of_float_simp)
433     thus False using `Float m e < 1` unfolding less_float_def le_float_def by auto
434   qed
435 qed
437 lemma float_less1_mantissa_bound: assumes "0 < Float m e" "Float m e < 1" shows "m < 2^(nat (-e))"
438 proof -
439   have "e < 0" using float_pos_less1_e_neg assms by auto
440   have "\<And>x. (0::real) < 2^x" by auto
441   have "real m < 2^(nat (-e))" using `Float m e < 1`
442     unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1
443           real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric]
444           mult_assoc by auto
445   thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto
446 qed
448 function bitlen :: "int \<Rightarrow> int" where
449 "bitlen 0 = 0" |
450 "bitlen -1 = 1" |
451 "0 < x \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))" |
452 "x < -1 \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))"
453   apply (case_tac "x = 0 \<or> x = -1 \<or> x < -1 \<or> x > 0")
454   apply auto
455   done
456 termination by (relation "measure (nat o abs)", auto)
458 lemma bitlen_ge0: "0 \<le> bitlen x" by (induct x rule: bitlen.induct, auto)
459 lemma bitlen_ge1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> bitlen x" by (induct x rule: bitlen.induct, auto simp add: bitlen_ge0)
461 lemma bitlen_bounds': assumes "0 < x" shows "2^nat (bitlen x - 1) \<le> x \<and> x + 1 \<le> 2^nat (bitlen x)" (is "?P x")
462   using `0 < x`
463 proof (induct x rule: bitlen.induct)
464   fix x
465   assume "0 < x" and hyp: "0 < x div 2 \<Longrightarrow> ?P (x div 2)" hence "0 \<le> x" and "x \<noteq> 0" by auto
466   { fix x have "0 \<le> 1 + bitlen x" using bitlen_ge0[of x] by auto } note gt0_pls1 = this
468   have "0 < (2::int)" by auto
470   show "?P x"
471   proof (cases "x = 1")
472     case True show "?P x" unfolding True by auto
473   next
474     case False hence "2 \<le> x" using `0 < x` `x \<noteq> 1` by auto
475     hence "2 div 2 \<le> x div 2" by (rule zdiv_mono1, auto)
476     hence "0 < x div 2" and "x div 2 \<noteq> 0" by auto
477     hence bitlen_s1_ge0: "0 \<le> bitlen (x div 2) - 1" using bitlen_ge1[OF `x div 2 \<noteq> 0`] by auto
479     { from hyp[OF `0 < x div 2`]
480       have "2 ^ nat (bitlen (x div 2) - 1) \<le> x div 2" by auto
481       hence "2 ^ nat (bitlen (x div 2) - 1) * 2 \<le> x div 2 * 2" by (rule mult_right_mono, auto)
482       also have "\<dots> \<le> x" using `0 < x` by auto
483       finally have "2^nat (1 + bitlen (x div 2) - 1) \<le> x" unfolding power_Suc2[symmetric] Suc_nat_eq_nat_zadd1[OF bitlen_s1_ge0] by auto
484     } moreover
485     { have "x + 1 \<le> x - x mod 2 + 2"
486       proof -
487         have "x mod 2 < 2" using `0 < x` by auto
488         hence "x < x - x mod 2 +  2" unfolding algebra_simps by auto
489         thus ?thesis by auto
490       qed
491       also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` zdiv_zmod_equality2[of x 2 0] by auto
492       also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto)
493       also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto
494       finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" .
495     }
496     ultimately show ?thesis
497       unfolding bitlen.simps(3)[OF `0 < x`] nat_add_distrib[OF zero_le_one bitlen_ge0]
499       by auto
500   qed
501 next
502   fix x :: int assume "x < -1" and "0 < x" hence False by auto
503   thus "?P x" by auto
504 qed auto
506 lemma bitlen_bounds: assumes "0 < x" shows "2^nat (bitlen x - 1) \<le> x \<and> x < 2^nat (bitlen x)"
507   using bitlen_bounds'[OF `0<x`] by auto
509 lemma bitlen_div: assumes "0 < m" shows "1 \<le> real m / 2^nat (bitlen m - 1)" and "real m / 2^nat (bitlen m - 1) < 2"
510 proof -
511   let ?B = "2^nat(bitlen m - 1)"
513   have "?B \<le> m" using bitlen_bounds[OF `0 <m`] ..
514   hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto
515   thus "1 \<le> real m / ?B" by auto
517   have "m \<noteq> 0" using assms by auto
518   have "0 \<le> bitlen m - 1" using bitlen_ge1[OF `m \<noteq> 0`] by auto
520   have "m < 2^nat(bitlen m)" using bitlen_bounds[OF `0 <m`] ..
521   also have "\<dots> = 2^nat(bitlen m - 1 + 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
522   also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF `0 \<le> bitlen m - 1` zero_le_one] by auto
523   finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto
524   hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto)
525   thus "real m / ?B < 2" by auto
526 qed
528 lemma float_gt1_scale: assumes "1 \<le> Float m e"
529   shows "0 \<le> e + (bitlen m - 1)"
530 proof (cases "0 \<le> e")
531   have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto
532   hence "0 < m" using float_pos_m_pos by auto
533   hence "m \<noteq> 0" by auto
534   case True with bitlen_ge1[OF `m \<noteq> 0`] show ?thesis by auto
535 next
536   have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto
537   hence "0 < m" using float_pos_m_pos by auto
538   hence "m \<noteq> 0" and "1 < (2::int)" by auto
539   case False let ?S = "2^(nat (-e))"
540   have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def real_of_float_nge0_exp[OF False] by auto
541   hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
542   hence "?S \<le> real m" unfolding mult_assoc by auto
543   hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto
544   from this bitlen_bounds[OF `0 < m`, THEN conjunct2]
545   have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans)
546   hence "-e < bitlen m" using False bitlen_ge0 by auto
547   thus ?thesis by auto
548 qed
550 lemma normalized_float: assumes "m \<noteq> 0" shows "real (Float m (- (bitlen m - 1))) = real m / 2^nat (bitlen m - 1)"
551 proof (cases "- (bitlen m - 1) = 0")
552   case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto
553 next
554   case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
555   show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto
556 qed
558 lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
560 lemma bitlen_Min: "bitlen (Int.Min) = Int.Bit1 Int.Pls" by (subst Min_def, simp add: Bit1_def)
562 lemma bitlen_B0: "bitlen (Int.Bit0 b) = (if iszero b then Int.Pls else Int.succ (bitlen b))"
563   apply (auto simp add: iszero_def succ_def)
564   apply (simp add: Bit0_def Pls_def)
565   apply (subst Bit0_def)
566   apply simp
567   apply (subgoal_tac "0 < 2 * b \<or> 2 * b < -1")
568   apply auto
569   done
571 lemma bitlen_B1: "bitlen (Int.Bit1 b) = (if iszero (Int.succ b) then Int.Bit1 Int.Pls else Int.succ (bitlen b))"
572 proof -
573   have h: "! x. (2*x + 1) div 2 = (x::int)"
574     by arith
575   show ?thesis
576     apply (auto simp add: iszero_def succ_def)
577     apply (subst Bit1_def)+
578     apply simp
579     apply (subgoal_tac "2 * b + 1 = -1")
580     apply (simp only:)
581     apply simp_all
582     apply (subst Bit1_def)
583     apply simp
584     apply (subgoal_tac "0 < 2 * b + 1 \<or> 2 * b + 1 < -1")
585     apply (auto simp add: h)
586     done
587 qed
589 lemma bitlen_number_of: "bitlen (number_of w) = number_of (bitlen w)"
590   by (simp add: number_of_is_id)
592 lemma [code]: "bitlen x =
593      (if x = 0  then 0
594  else if x = -1 then 1
595                 else (1 + (bitlen (x div 2))))"
596   by (cases "x = 0 \<or> x = -1 \<or> 0 < x") auto
598 definition lapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
599 where
600   "lapprox_posrat prec x y =
601    (let
602        l = nat (int prec + bitlen y - bitlen x) ;
603        d = (x * 2^l) div y
604     in normfloat (Float d (- (int l))))"
606 lemma pow2_minus: "pow2 (-x) = inverse (pow2 x)"
607   unfolding pow2_neg[of "-x"] by auto
609 lemma lapprox_posrat:
610   assumes x: "0 \<le> x"
611   and y: "0 < y"
612   shows "real (lapprox_posrat prec x y) \<le> real x / real y"
613 proof -
614   let ?l = "nat (int prec + bitlen y - bitlen x)"
616   have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)"
617     by (rule mult_right_mono, fact real_of_int_div4, simp)
618   also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto
619   finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding mult_assoc by auto
620   thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp
621     unfolding pow2_minus pow2_int minus_minus .
622 qed
624 lemma real_of_int_div_mult:
625   fixes x y c :: int assumes "0 < y" and "0 < c"
626   shows "real (x div y) \<le> real (x * c div y) * inverse (real c)"
627 proof -
628   have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y]
629     by (rule add_left_mono,
630         auto intro!: mult_nonneg_nonneg
631              simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`])
632   hence "real (x div y) * real c \<le> real (x * c div y)"
633     unfolding real_of_int_mult[symmetric] real_of_int_le_iff mult_commute by auto
634   hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
635     using `0 < c` by auto
636   thus ?thesis unfolding mult_assoc using `0 < c` by auto
637 qed
639 lemma lapprox_posrat_bottom: assumes "0 < y"
640   shows "real (x div y) \<le> real (lapprox_posrat n x y)"
641 proof -
642   have pow: "\<And>x. (0::int) < 2^x" by auto
643   show ?thesis
644     unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
645     using real_of_int_div_mult[OF `0 < y` pow] by auto
646 qed
648 lemma lapprox_posrat_nonneg: assumes "0 \<le> x" and "0 < y"
649   shows "0 \<le> real (lapprox_posrat n x y)"
650 proof -
651   show ?thesis
652     unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
653     using pos_imp_zdiv_nonneg_iff[OF `0 < y`] assms by (auto intro!: mult_nonneg_nonneg)
654 qed
656 definition rapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
657 where
658   "rapprox_posrat prec x y = (let
659      l = nat (int prec + bitlen y - bitlen x) ;
660      X = x * 2^l ;
661      d = X div y ;
662      m = X mod y
663    in normfloat (Float (d + (if m = 0 then 0 else 1)) (- (int l))))"
665 lemma rapprox_posrat:
666   assumes x: "0 \<le> x"
667   and y: "0 < y"
668   shows "real x / real y \<le> real (rapprox_posrat prec x y)"
669 proof -
670   let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l"
671   show ?thesis
672   proof (cases "?X mod y = 0")
673     case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
674     from real_of_int_div[OF this]
675     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
676     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
677     finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
678     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True]
679       unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
680   next
681     case False
682     have "0 \<le> real y" and "real y \<noteq> 0" using `0 < y` by auto
683     have "0 \<le> real y * 2^?l" by (rule mult_nonneg_nonneg, rule `0 \<le> real y`, auto)
685     have "?X = y * (?X div y) + ?X mod y" by auto
686     also have "\<dots> \<le> y * (?X div y) + y" by (rule add_mono, auto simp add: pos_mod_bound[OF `0 < y`, THEN less_imp_le])
687     also have "\<dots> = y * (?X div y + 1)" unfolding right_distrib by auto
688     finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] .
689     hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)"
690       by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
691     also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto
692     also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`]
693       unfolding divide_inverse ..
694     finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
695       unfolding pow2_minus pow2_int minus_minus by auto
696   qed
697 qed
699 lemma rapprox_posrat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
700   shows "real (rapprox_posrat n x y) \<le> 1"
701 proof -
702   let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
703   show ?thesis
704   proof (cases "?X mod y = 0")
705     case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
706     from real_of_int_div[OF this]
707     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
708     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
709     finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
710     also have "real x / real y \<le> 1" using `0 \<le> x` and `0 < y` and `x \<le> y` by auto
711     finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True]
712       unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
713   next
714     case False
715     have "x \<noteq> y"
716     proof (rule ccontr)
717       assume "\<not> x \<noteq> y" hence "x = y" by auto
718       have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto
719       thus False using False by auto
720     qed
721     hence "x < y" using `x \<le> y` by auto
722     hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
724     from real_of_int_div4[of "?X" y]
725     have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
726     also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto)
727     finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
728     hence "?X div y + 1 \<le> 2^?l" by auto
729     hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)"
730       unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
731       by (rule mult_right_mono, auto)
732     hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
733     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
734       unfolding pow2_minus pow2_int minus_minus by auto
735   qed
736 qed
738 lemma zdiv_greater_zero: fixes a b :: int assumes "0 < a" and "a \<le> b"
739   shows "0 < b div a"
740 proof (rule ccontr)
741   have "0 \<le> b" using assms by auto
742   assume "\<not> 0 < b div a" hence "b div a = 0" using `0 \<le> b`[unfolded pos_imp_zdiv_nonneg_iff[OF `0<a`, of b, symmetric]] by auto
743   have "b = a * (b div a) + b mod a" by auto
744   hence "b = b mod a" unfolding `b div a = 0` by auto
745   hence "b < a" using `0 < a`[THEN pos_mod_bound, of b] by auto
746   thus False using `a \<le> b` by auto
747 qed
749 lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
750   shows "real (rapprox_posrat n x y) < 1"
751 proof (cases "x = 0")
752   case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat real_of_float_simp by auto
753 next
754   case False hence "0 < x" using `0 \<le> x` by auto
755   hence "x < y" using assms by auto
757   let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
758   show ?thesis
759   proof (cases "?X mod y = 0")
760     case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
761     from real_of_int_div[OF this]
762     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
763     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
764     finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
765     also have "real x / real y < 1" using `0 \<le> x` and `0 < y` and `x < y` by auto
766     finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_P[OF True]
767       unfolding pow2_minus pow2_int minus_minus by auto
768   next
769     case False
770     hence "(real x / real y) < 1 / 2" using `0 < y` and `0 \<le> x` `2 * x < y` by auto
772     have "0 < ?X div y"
773     proof -
774       have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)"
775         using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto
776       hence "(2::int)^nat (bitlen x - 1) < 2^nat (bitlen y)" by (rule order_le_less_trans)
777       hence "bitlen x \<le> bitlen y" by auto
778       hence len_less: "nat (bitlen x - 1) \<le> nat (int (n - 1) + bitlen y)" by auto
780       have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto
782       have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l"
783         using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto
785       have "y * 2^nat (bitlen x - 1) \<le> y * x"
786         using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono)
787       also have "\<dots> \<le> 2^nat (bitlen y) * x" using bitlen_bounds[OF `0 < y`, THEN conjunct2, THEN less_imp_le] `0 \<le> x` by (rule mult_right_mono)
788       also have "\<dots> \<le> x * 2^nat (int (n - 1) + bitlen y)" unfolding mult_commute[of x] by (rule mult_right_mono, auto simp add: `0 \<le> x`)
789       finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))"
790         unfolding real_of_int_le_iff[symmetric] by auto
791       hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))"
792         unfolding mult_assoc divide_inverse by auto
793       also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto
794       finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto
795       thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto
796     qed
798     from real_of_int_div4[of "?X" y]
799     have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
800     also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto)
801     finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
802     hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto
803     hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)"
804       unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
805       by (rule mult_strict_right_mono, auto)
806     hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
807     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
808       unfolding pow2_minus pow2_int minus_minus by auto
809   qed
810 qed
812 lemma approx_rat_pattern: fixes P and ps :: "nat * int * int"
813   assumes Y: "\<And>y prec x. \<lbrakk>y = 0; ps = (prec, x, 0)\<rbrakk> \<Longrightarrow> P"
814   and A: "\<And>x y prec. \<lbrakk>0 \<le> x; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
815   and B: "\<And>x y prec. \<lbrakk>x < 0; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
816   and C: "\<And>x y prec. \<lbrakk>x < 0; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
817   and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
818   shows P
819 proof -
820   obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps) auto
821   from Y have "y = 0 \<Longrightarrow> P" by auto
822   moreover {
823     assume "0 < y"
824     have P
825     proof (cases "0 \<le> x")
826       case True
827       with A and `0 < y` show P by auto
828     next
829       case False
830       with B and `0 < y` show P by auto
831     qed
832   }
833   moreover {
834     assume "y < 0"
835     have P
836     proof (cases "0 \<le> x")
837       case True
838       with D and `y < 0` show P by auto
839     next
840       case False
841       with C and `y < 0` show P by auto
842     qed
843   }
844   ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0") auto
845 qed
847 function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
848 where
849   "y = 0 \<Longrightarrow> lapprox_rat prec x y = 0"
850 | "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec x y"
851 | "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec (-x) y)"
852 | "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec (-x) (-y)"
853 | "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec x (-y))"
854 apply simp_all by (rule approx_rat_pattern)
855 termination by lexicographic_order
857 lemma compute_lapprox_rat[code]:
858       "lapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then lapprox_posrat prec x y else - (rapprox_posrat prec x (-y)))
859                                                              else (if 0 < y then - (rapprox_posrat prec (-x) y) else lapprox_posrat prec (-x) (-y)))"
860   by auto
862 lemma lapprox_rat: "real (lapprox_rat prec x y) \<le> real x / real y"
863 proof -
864   have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
865   show ?thesis
866     apply (case_tac "y = 0")
867     apply simp
868     apply (case_tac "0 \<le> x \<and> 0 < y")
869     apply (simp add: lapprox_posrat)
870     apply (case_tac "x < 0 \<and> 0 < y")
871     apply simp
872     apply (subst minus_le_iff)
873     apply (rule h[OF rapprox_posrat])
874     apply (simp_all)
875     apply (case_tac "x < 0 \<and> y < 0")
876     apply simp
877     apply (rule h[OF _ lapprox_posrat])
878     apply (simp_all)
879     apply (case_tac "0 \<le> x \<and> y < 0")
880     apply (simp)
881     apply (subst minus_le_iff)
882     apply (rule h[OF rapprox_posrat])
883     apply simp_all
884     apply arith
885     done
886 qed
888 lemma lapprox_rat_bottom: assumes "0 \<le> x" and "0 < y"
889   shows "real (x div y) \<le> real (lapprox_rat n x y)"
890   unfolding lapprox_rat.simps(2)[OF assms]  using lapprox_posrat_bottom[OF `0<y`] .
892 function rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
893 where
894   "y = 0 \<Longrightarrow> rapprox_rat prec x y = 0"
895 | "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec x y"
896 | "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec (-x) y)"
897 | "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec (-x) (-y)"
898 | "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec x (-y))"
899 apply simp_all by (rule approx_rat_pattern)
900 termination by lexicographic_order
902 lemma compute_rapprox_rat[code]:
903       "rapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then rapprox_posrat prec x y else - (lapprox_posrat prec x (-y))) else
904                                                                   (if 0 < y then - (lapprox_posrat prec (-x) y) else rapprox_posrat prec (-x) (-y)))"
905   by auto
907 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
908 proof -
909   have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
910   show ?thesis
911     apply (case_tac "y = 0")
912     apply simp
913     apply (case_tac "0 \<le> x \<and> 0 < y")
914     apply (simp add: rapprox_posrat)
915     apply (case_tac "x < 0 \<and> 0 < y")
916     apply simp
917     apply (subst le_minus_iff)
918     apply (rule h[OF _ lapprox_posrat])
919     apply (simp_all)
920     apply (case_tac "x < 0 \<and> y < 0")
921     apply simp
922     apply (rule h[OF rapprox_posrat])
923     apply (simp_all)
924     apply (case_tac "0 \<le> x \<and> y < 0")
925     apply (simp)
926     apply (subst le_minus_iff)
927     apply (rule h[OF _ lapprox_posrat])
928     apply simp_all
929     apply arith
930     done
931 qed
933 lemma rapprox_rat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
934   shows "real (rapprox_rat n x y) \<le> 1"
935   unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] using rapprox_posrat_le1[OF assms] .
937 lemma rapprox_rat_neg: assumes "x < 0" and "0 < y"
938   shows "real (rapprox_rat n x y) \<le> 0"
939   unfolding rapprox_rat.simps(3)[OF assms] using lapprox_posrat_nonneg[of "-x" y n] assms by auto
941 lemma rapprox_rat_nonneg_neg: assumes "0 \<le> x" and "y < 0"
942   shows "real (rapprox_rat n x y) \<le> 0"
943   unfolding rapprox_rat.simps(5)[OF assms] using lapprox_posrat_nonneg[of x "-y" n] assms by auto
945 lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y"
946   shows "real (rapprox_rat n x y) \<le> 0"
947 proof (cases "x = 0")
948   case True
949   hence "0 \<le> x" by auto show ?thesis
950     unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
951     unfolding True rapprox_posrat_def Let_def
952     by auto
953 next
954   case False
955   hence "x < 0" using assms by auto
956   show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] .
957 qed
959 fun float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
960 where
961   "float_divl prec (Float m1 s1) (Float m2 s2) =
962     (let
963        l = lapprox_rat prec m1 m2;
964        f = Float 1 (s1 - s2)
965      in
966        f * l)"
968 lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
969   using lapprox_rat[of prec "mantissa x" "mantissa y"]
970   by (cases x y rule: float.exhaust[case_product float.exhaust])
971      (simp split: split_if_asm
972            add: real_of_float_simp pow2_diff field_simps le_divide_eq mult_less_0_iff zero_less_mult_iff)
974 lemma float_divl_lower_bound: assumes "0 \<le> x" and "0 < y" shows "0 \<le> float_divl prec x y"
975 proof (cases x, cases y)
976   fix xm xe ym ye :: int
977   assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
978   have "0 \<le> xm"
979     using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff]
980     by auto
981   have "0 < ym"
982     using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff]
983     by auto
985   have "\<And>n. 0 \<le> real (Float 1 n)"
986     unfolding real_of_float_simp using zero_le_pow2 by auto
987   moreover have "0 \<le> real (lapprox_rat prec xm ym)"
988     apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]])
989     apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
990     done
991   ultimately show "0 \<le> float_divl prec x y"
992     unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0
993     by (auto intro!: mult_nonneg_nonneg)
994 qed
996 lemma float_divl_pos_less1_bound:
997   assumes "0 < x" and "x < 1" and "0 < prec"
998   shows "1 \<le> float_divl prec 1 x"
999 proof (cases x)
1000   case (Float m e)
1001   from `0 < x` `x < 1` have "0 < m" "e < 0"
1002     using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
1003   let ?b = "nat (bitlen m)" and ?e = "nat (-e)"
1004   have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto
1005   with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto
1006   hence "1 \<le> bitlen m" using power_le_imp_le_exp[of "2::int" 1 ?b] by auto
1007   hence pow_split: "nat (int prec + bitlen m - 1) = (prec - 1) + ?b" using `0 < prec` by auto
1009   have pow_not0: "\<And>x. (2::real)^x \<noteq> 0" by auto
1011   from float_less1_mantissa_bound `0 < x` `x < 1` Float
1012   have "m < 2^?e" by auto
1013   with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m - 1) < 2^?e"
1014     by (rule order_le_less_trans)
1015   from power_less_imp_less_exp[OF _ this]
1016   have "bitlen m \<le> - e" by auto
1017   hence "(2::real)^?b \<le> 2^?e" by auto
1018   hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)"
1019     by (rule mult_right_mono) auto
1020   hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto
1021   also
1022   let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))"
1023   {
1024     have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
1025       using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
1026     also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
1027       unfolding pow_split power_add by auto
1028     finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
1029       using `0 < m` by (rule zdiv_mono1)
1030     hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
1031       unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
1032     hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
1033       unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto
1034   }
1035   from mult_left_mono[OF this [unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
1036   have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
1037   finally have "1 \<le> 2^?e * ?d" .
1039   have e_nat: "0 - e = int (nat (-e))" using `e < 0` by auto
1040   have "bitlen 1 = 1" using bitlen.simps by auto
1042   show ?thesis
1043     unfolding one_float_def Float float_divl.simps Let_def
1044       lapprox_rat.simps(2)[OF zero_le_one `0 < m`]
1045       lapprox_posrat_def `bitlen 1 = 1`
1046     unfolding le_float_def real_of_float_mult normfloat real_of_float_simp
1047       pow2_minus pow2_int e_nat
1048     using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def)
1049 qed
1051 fun float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
1052 where
1053   "float_divr prec (Float m1 s1) (Float m2 s2) =
1054     (let
1055        r = rapprox_rat prec m1 m2;
1056        f = Float 1 (s1 - s2)
1057      in
1058        f * r)"
1060 lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
1061   using rapprox_rat[of "mantissa x" "mantissa y" prec]
1062   by (cases x y rule: float.exhaust[case_product float.exhaust])
1063      (simp split: split_if_asm
1064            add: real_of_float_simp pow2_diff field_simps divide_le_eq mult_less_0_iff zero_less_mult_iff)
1066 lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
1067 proof -
1068   have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto
1069   also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
1070   finally show ?thesis unfolding le_float_def by auto
1071 qed
1073 lemma float_divr_nonpos_pos_upper_bound: assumes "x \<le> 0" and "0 < y" shows "float_divr prec x y \<le> 0"
1074 proof (cases x, cases y)
1075   fix xm xe ym ye :: int
1076   assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
1077   have "xm \<le> 0" using `x \<le> 0`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 mult_le_0_iff] by auto
1078   have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto
1080   have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
1081   moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] .
1082   ultimately show "float_divr prec x y \<le> 0"
1083     unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos)
1084 qed
1086 lemma float_divr_nonneg_neg_upper_bound: assumes "0 \<le> x" and "y < 0" shows "float_divr prec x y \<le> 0"
1087 proof (cases x, cases y)
1088   fix xm xe ym ye :: int
1089   assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
1090   have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto
1091   have "ym < 0" using `y < 0`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 mult_less_0_iff] by auto
1092   hence "0 < - ym" by auto
1094   have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
1095   moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] .
1096   ultimately show "float_divr prec x y \<le> 0"
1097     unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos)
1098 qed
1100 primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
1101 "round_down prec (Float m e) = (let d = bitlen m - int prec in
1102      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
1103               else Float m e)"
1105 primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
1106 "round_up prec (Float m e) = (let d = bitlen m - int prec in
1107   if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d)
1108            else Float m e)"
1110 lemma round_up: "real x \<le> real (round_up prec x)"
1111 proof (cases x)
1112   case (Float m e)
1113   let ?d = "bitlen m - int prec"
1114   let ?p = "(2::int)^nat ?d"
1115   have "0 < ?p" by auto
1116   show "?thesis"
1117   proof (cases "0 < ?d")
1118     case True
1119     hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
1120     show ?thesis
1121     proof (cases "m mod ?p = 0")
1122       case True
1123       have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] .
1124       have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
1125         by (auto simp add: pow2_add `0 < ?d` pow_d)
1126       thus ?thesis
1127         unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`]
1128         by auto
1129     next
1130       case False
1131       have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
1132       also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
1133       finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
1134         unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
1135         by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
1136       thus ?thesis
1137         unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] .
1138     qed
1139   next
1140     case False
1141     show ?thesis
1142       unfolding Float round_up.simps Let_def if_not_P[OF False] ..
1143   qed
1144 qed
1146 lemma round_down: "real (round_down prec x) \<le> real x"
1147 proof (cases x)
1148   case (Float m e)
1149   let ?d = "bitlen m - int prec"
1150   let ?p = "(2::int)^nat ?d"
1151   have "0 < ?p" by auto
1152   show "?thesis"
1153   proof (cases "0 < ?d")
1154     case True
1155     hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
1156     have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
1157     also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
1158     finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
1159       unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric]
1160       by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
1161     thus ?thesis
1162       unfolding Float round_down.simps Let_def if_P[OF `0 < ?d`] .
1163   next
1164     case False
1165     show ?thesis
1166       unfolding Float round_down.simps Let_def if_not_P[OF False] ..
1167   qed
1168 qed
1170 definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1171   "lb_mult prec x y =
1172     (case normfloat (x * y) of Float m e \<Rightarrow>
1173       let
1174         l = bitlen m - int prec
1175       in if l > 0 then Float (m div (2^nat l)) (e + l)
1176                   else Float m e)"
1178 definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1179   "ub_mult prec x y =
1180     (case normfloat (x * y) of Float m e \<Rightarrow>
1181       let
1182         l = bitlen m - int prec
1183       in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
1184                   else Float m e)"
1186 lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)"
1187 proof (cases "normfloat (x * y)")
1188   case (Float m e)
1189   hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero)
1190   let ?l = "bitlen m - int prec"
1191   have "real (lb_mult prec x y) \<le> real (normfloat (x * y))"
1192   proof (cases "?l > 0")
1193     case False thus ?thesis unfolding lb_mult_def Float Let_def float.cases by auto
1194   next
1195     case True
1196     have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
1197     proof -
1198       have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_number_of unfolding pow2_int[symmetric]
1199         using `?l > 0` by auto
1200       also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto
1201       also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
1202       finally show ?thesis by auto
1203     qed
1204     thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto
1205   qed
1206   also have "\<dots> = real (x * y)" unfolding normfloat ..
1207   finally show ?thesis .
1208 qed
1210 lemma ub_mult: "real (x * y) \<le> real (ub_mult prec x y)"
1211 proof (cases "normfloat (x * y)")
1212   case (Float m e)
1213   hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero)
1214   let ?l = "bitlen m - int prec"
1215   have "real (x * y) = real (normfloat (x * y))" unfolding normfloat ..
1216   also have "\<dots> \<le> real (ub_mult prec x y)"
1217   proof (cases "?l > 0")
1218     case False thus ?thesis unfolding ub_mult_def Float Let_def float.cases by auto
1219   next
1220     case True
1221     have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l"
1222     proof -
1223       have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto
1224       hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding mult_1 real_of_int_less_iff[symmetric] by auto
1226       have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
1227       also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto
1228       also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding left_distrib using mod_uneq by auto
1229       finally show ?thesis unfolding pow2_int[symmetric] using True by auto
1230     qed
1231     thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto
1232   qed
1233   finally show ?thesis .
1234 qed
1236 primrec float_abs :: "float \<Rightarrow> float" where
1237   "float_abs (Float m e) = Float \<bar>m\<bar> e"
1239 instantiation float :: abs
1240 begin
1241 definition abs_float_def: "\<bar>x\<bar> = float_abs x"
1242 instance ..
1243 end
1245 lemma real_of_float_abs: "real \<bar>x :: float\<bar> = \<bar>real x\<bar>"
1246 proof (cases x)
1247   case (Float m e)
1248   have "\<bar>real m\<bar> * pow2 e = \<bar>real m * pow2 e\<bar>" unfolding abs_mult by auto
1249   thus ?thesis unfolding Float abs_float_def float_abs.simps real_of_float_simp by auto
1250 qed
1252 primrec floor_fl :: "float \<Rightarrow> float" where
1253   "floor_fl (Float m e) = (if 0 \<le> e then Float m e
1254                                   else Float (m div (2 ^ (nat (-e)))) 0)"
1256 lemma floor_fl: "real (floor_fl x) \<le> real x"
1257 proof (cases x)
1258   case (Float m e)
1259   show ?thesis
1260   proof (cases "0 \<le> e")
1261     case False
1262     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
1263     have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
1264     also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
1265     also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
1266     also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
1267     finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
1268   next
1269     case True thus ?thesis unfolding Float by auto
1270   qed
1271 qed
1273 lemma floor_pos_exp: assumes floor: "Float m e = floor_fl x" shows "0 \<le> e"
1274 proof (cases x)
1275   case (Float mx me)
1276   from floor[unfolded Float floor_fl.simps] show ?thesis by (cases "0 \<le> me", auto)
1277 qed
1279 declare floor_fl.simps[simp del]
1281 primrec ceiling_fl :: "float \<Rightarrow> float" where
1282   "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
1283                                     else Float (m div (2 ^ (nat (-e))) + 1) 0)"
1285 lemma ceiling_fl: "real x \<le> real (ceiling_fl x)"
1286 proof (cases x)
1287   case (Float m e)
1288   show ?thesis
1289   proof (cases "0 \<le> e")
1290     case False
1291     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
1292     have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
1293     also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
1294     also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
1295     also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
1296     finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
1297   next
1298     case True thus ?thesis unfolding Float by auto
1299   qed
1300 qed
1302 declare ceiling_fl.simps[simp del]
1304 definition lb_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1305   "lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
1307 definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1308   "ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
1310 lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x")
1311   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
1312   shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y"
1313 proof -
1314   have "?lb \<le> ?ub" using assms by auto
1315   have "0 \<le> ?lb" and "?lb \<noteq> 0" using assms by auto
1316   have "?k * y \<le> ?x" using assms by auto
1317   also have "\<dots> \<le> ?x / ?lb * ?ub" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?lb` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?lb \<noteq> 0`])
1318   also have "\<dots> \<le> real (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl)
1319   finally show ?thesis unfolding lb_mod_def real_of_float_sub real_of_float_mult by auto
1320 qed
1322 lemma ub_mod:
1323   fixes k :: int and x :: float
1324   assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
1325   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
1326   shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
1327 proof -
1328   have "?lb \<le> ?ub" using assms by auto
1329   hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" using assms by auto
1330   have "real (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl)
1331   also have "\<dots> \<le> ?x" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?ub` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?ub \<noteq> 0`])
1332   also have "\<dots> \<le> ?k * y" using assms by auto
1333   finally show ?thesis unfolding ub_mod_def real_of_float_sub real_of_float_mult by auto
1334 qed
1336 lemma le_float_def'[code]: "f \<le> g = (case f - g of Float a b \<Rightarrow> a \<le> 0)"
1337 proof -
1338   have le_transfer: "(f \<le> g) = (real (f - g) \<le> 0)" by (auto simp add: le_float_def)
1339   from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
1340   with le_transfer have le_transfer': "f \<le> g = (real (Float a b) \<le> 0)" by simp
1341   show ?thesis by (simp add: le_transfer' f_diff_g float_le_zero)
1342 qed
1344 lemma less_float_def'[code]: "f < g = (case f - g of Float a b \<Rightarrow> a < 0)"
1345 proof -
1346   have less_transfer: "(f < g) = (real (f - g) < 0)" by (auto simp add: less_float_def)
1347   from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
1348   with less_transfer have less_transfer': "f < g = (real (Float a b) < 0)" by simp
1349   show ?thesis by (simp add: less_transfer' f_diff_g float_less_zero)
1350 qed
1352 end