src/HOL/Library/Float.thy
 author haftmann Mon Feb 08 14:06:41 2010 +0100 (2010-02-08) changeset 35032 7efe662e41b4 parent 33555 a0a8a40385a2 child 35344 e0b46cd72414 permissions -rw-r--r--
separate library theory for type classes combining lattices with various algebraic structures
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
13   pow2 :: "int \<Rightarrow> real" where
14   [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
16 datatype float = Float int int
18 primrec of_float :: "float \<Rightarrow> real" where
19   "of_float (Float a b) = real a * pow2 b"
22   real_of_float_def [code_unfold]: "real == of_float"
24 primrec mantissa :: "float \<Rightarrow> int" where
25   "mantissa (Float a b) = a"
27 primrec scale :: "float \<Rightarrow> int" where
28   "scale (Float a b) = b"
30 instantiation float :: zero begin
31 definition zero_float where "0 = Float 0 0"
32 instance ..
33 end
35 instantiation float :: one begin
36 definition one_float where "1 = Float 1 0"
37 instance ..
38 end
40 instantiation float :: number begin
41 definition number_of_float where "number_of n = Float n 0"
42 instance ..
43 end
45 lemma number_of_float_Float [code_unfold_post]:
46   "number_of k = Float (number_of k) 0"
47   by (simp add: number_of_float_def number_of_is_id)
49 lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
50   unfolding real_of_float_def using of_float.simps .
52 lemma real_of_float_neg_exp: "e < 0 \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
53 lemma real_of_float_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
54 lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto
56 lemma Float_num[simp]: shows
57    "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
58    "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
59    "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
60   by auto
62 lemma float_number_of[simp]: "real (number_of x :: float) = number_of x"
63   by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
65 lemma float_number_of_int[simp]: "real (Float n 0) = real n"
66   by (simp add: Float_num[unfolded number_of_is_id] real_of_float_simp pow2_def)
68 lemma pow2_0[simp]: "pow2 0 = 1" by simp
69 lemma pow2_1[simp]: "pow2 1 = 2" by simp
70 lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp
72 declare pow2_def[simp del]
74 lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
75 proof -
76   have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
77   have g: "! a b. a - -1 = a + (1::int)" by arith
78   have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
79     apply (auto, induct_tac n)
81     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
82     by (auto simp add: h)
83   show ?thesis
84   proof (induct a)
85     case (1 n)
86     from pos show ?case by (simp add: algebra_simps)
87   next
88     case (2 n)
89     show ?case
90       apply (auto)
91       apply (subst pow2_neg[of "- int n"])
92       apply (subst pow2_neg[of "-1 - int n"])
93       apply (auto simp add: g pos)
94       done
95   qed
96 qed
98 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
99 proof (induct b)
100   case (1 n)
101   show ?case
102   proof (induct n)
103     case 0
104     show ?case by simp
105   next
106     case (Suc m)
108   qed
109 next
110   case (2 n)
111   show ?case
112   proof (induct n)
113     case 0
114     show ?case
115       apply (auto)
116       apply (subst pow2_neg[of "a + -1"])
117       apply (subst pow2_neg[of "-1"])
118       apply (simp)
121       apply (subst pow2_neg[of "-a"])
122       apply (simp)
123       done
124     case (Suc m)
125     have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
126     have b: "int m - -2 = 1 + (int m + 1)" by arith
127     show ?case
128       apply (auto)
129       apply (subst pow2_neg[of "a + (-2 - int m)"])
130       apply (subst pow2_neg[of "-2 - int m"])
131       apply (auto simp add: algebra_simps)
132       apply (subst a)
133       apply (subst b)
135       apply (subst pow2_neg[of "int m - a + 1"])
136       apply (subst pow2_neg[of "int m + 1"])
137       apply auto
138       apply (insert prems)
139       apply (auto simp add: algebra_simps)
140       done
141   qed
142 qed
144 lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f, auto)
146 lemma float_split: "\<exists> a b. x = Float a b" by (cases x, auto)
148 lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split)
150 lemma float_zero[simp]: "real (Float 0 e) = 0" by simp
152 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
153 by arith
155 function normfloat :: "float \<Rightarrow> float" where
156 "normfloat (Float a b) = (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1)) else if a=0 then Float 0 0 else Float a b)"
157 by pat_completeness auto
158 termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less)
159 declare normfloat.simps[simp del]
161 theorem normfloat[symmetric, simp]: "real f = real (normfloat f)"
162 proof (induct f rule: normfloat.induct)
163   case (1 a b)
164   have real2: "2 = real (2::int)"
165     by auto
166   show ?case
167     apply (subst normfloat.simps)
168     apply (auto simp add: float_zero)
169     apply (subst 1[symmetric])
171     done
172 qed
174 lemma pow2_neq_zero[simp]: "pow2 x \<noteq> 0"
175   by (auto simp add: pow2_def)
177 lemma pow2_int: "pow2 (int c) = 2^c"
180 lemma zero_less_pow2[simp]:
181   "0 < pow2 x"
182 proof -
183   {
184     fix y
185     have "0 <= y \<Longrightarrow> 0 < pow2 y"
187   }
188   note helper=this
189   show ?thesis
190     apply (case_tac "0 <= x")
192     apply (subst pow2_neg)
194     done
195 qed
197 lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
198 proof (induct f rule: normfloat.induct)
199   case (1 u v)
200   from 1 have ab: "normfloat (Float u v) = Float a b" by auto
201   {
202     assume eu: "even u"
203     assume z: "u \<noteq> 0"
204     have "normfloat (Float u v) = normfloat (Float (u div 2) (v + 1))"
205       apply (subst normfloat.simps)
206       by (simp add: eu z)
207     with ab have "normfloat (Float (u div 2) (v + 1)) = Float a b" by simp
208     with 1 eu z have ?case by auto
209   }
210   note case1 = this
211   {
212     assume "odd u \<or> u = 0"
213     then have ou: "\<not> (u \<noteq> 0 \<and> even u)" by auto
214     have "normfloat (Float u v) = (if u = 0 then Float 0 0 else Float u v)"
215       apply (subst normfloat.simps)
217       done
218     with ab have "Float a b = (if u = 0 then Float 0 0 else Float u v)" by auto
219     then have ?case
220       apply (case_tac "u=0")
221       apply (auto)
222       by (insert ou, auto)
223   }
224   note case2 = this
225   show ?case
226     apply (case_tac "odd u \<or> u = 0")
227     apply (rule case2)
228     apply simp
229     apply (rule case1)
230     apply auto
231     done
232 qed
234 lemma float_eq_odd_helper:
235   assumes odd: "odd a'"
236   and floateq: "real (Float a b) = real (Float a' b')"
237   shows "b \<le> b'"
238 proof -
239   {
240     assume bcmp: "b > b'"
241     from floateq have eq: "real a * pow2 b = real a' * pow2 b'" by simp
242     {
243       fix x y z :: real
244       assume "y \<noteq> 0"
245       then have "(x * inverse y = z) = (x = z * y)"
246         by auto
247     }
248     note inverse = this
249     have eq': "real a * (pow2 (b - b')) = real a'"
250       apply (subst diff_int_def)
252       apply (subst pow2_neg[where x = "-b'"])
253       apply simp
254       apply (subst mult_assoc[symmetric])
255       apply (subst inverse)
257       done
258     have "\<exists> z > 0. pow2 (b-b') = 2^z"
259       apply (rule exI[where x="nat (b - b')"])
260       apply (auto)
261       apply (insert bcmp)
262       apply simp
263       apply (subst pow2_int[symmetric])
264       apply auto
265       done
266     then obtain z where z: "z > 0 \<and> pow2 (b-b') = 2^z" by auto
267     with eq' have "real a * 2^z = real a'"
268       by auto
269     then have "real a * real ((2::int)^z) = real a'"
270       by auto
271     then have "real (a * 2^z) = real a'"
272       apply (subst real_of_int_mult)
273       apply simp
274       done
275     then have a'_rep: "a * 2^z = a'" by arith
276     then have "a' = a*2^z" by simp
277     with z have "even a'" by simp
278     with odd have False by auto
279   }
280   then show ?thesis by arith
281 qed
283 lemma float_eq_odd:
284   assumes odd1: "odd a"
285   and odd2: "odd a'"
286   and floateq: "real (Float a b) = real (Float a' b')"
287   shows "a = a' \<and> b = b'"
288 proof -
289   from
290      float_eq_odd_helper[OF odd2 floateq]
291      float_eq_odd_helper[OF odd1 floateq[symmetric]]
292   have beq: "b = b'"  by arith
293   with floateq show ?thesis by auto
294 qed
296 theorem normfloat_unique:
297   assumes real_of_float_eq: "real f = real g"
298   shows "normfloat f = normfloat g"
299 proof -
300   from float_split[of "normfloat f"] obtain a b where normf:"normfloat f = Float a b" by auto
301   from float_split[of "normfloat g"] obtain a' b' where normg:"normfloat g = Float a' b'" by auto
302   have "real (normfloat f) = real (normfloat g)"
304   then have float_eq: "real (Float a b) = real (Float a' b')"
305     by (simp add: normf normg)
306   have ab: "odd a \<or> (a = 0 \<and> b = 0)" by (rule normfloat_imp_odd_or_zero[OF normf])
307   have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg])
308   {
309     assume odd: "odd a"
310     then have "a \<noteq> 0" by (simp add: even_def, arith)
311     with float_eq have "a' \<noteq> 0" by auto
312     with ab' have "odd a'" by simp
313     from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd)
314   }
315   note odd_case = this
316   {
317     assume even: "even a"
318     with ab have a0: "a = 0" by simp
319     with float_eq have a0': "a' = 0" by auto
320     from a0 a0' ab ab' have "a = a' \<and> b = b'" by auto
321   }
322   note even_case = this
323   from odd_case even_case show ?thesis
324     apply (simp add: normf normg)
325     apply (case_tac "even a")
326     apply auto
327     done
328 qed
330 instantiation float :: plus begin
331 fun plus_float where
332 [simp del]: "(Float a_m a_e) + (Float b_m b_e) =
333      (if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e - a_e))) a_e
334                    else Float (a_m * 2^(nat (a_e - b_e)) + b_m) b_e)"
335 instance ..
336 end
338 instantiation float :: uminus begin
339 primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
340 instance ..
341 end
343 instantiation float :: minus begin
344 definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
345 instance ..
346 end
348 instantiation float :: times begin
349 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)"
350 instance ..
351 end
353 primrec float_pprt :: "float \<Rightarrow> float" where
354   "float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
356 primrec float_nprt :: "float \<Rightarrow> float" where
357   "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))"
359 instantiation float :: ord begin
360 definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w"
361 definition less_float_def: "z < (w :: float) \<equiv> real z < real w"
362 instance ..
363 end
365 lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)"
366   by (cases a, cases b, simp add: algebra_simps plus_float.simps,
369 lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
370   by (cases a, simp add: uminus_float.simps)
372 lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
373   by (cases a, cases b, simp add: minus_float_def)
375 lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)"
378 lemma real_of_float_0[simp]: "real (0 :: float) = 0"
379   by (auto simp add: zero_float_def float_zero)
381 lemma real_of_float_1[simp]: "real (1 :: float) = 1"
382   by (auto simp add: one_float_def)
384 lemma zero_le_float:
385   "(0 <= real (Float a b)) = (0 <= a)"
386   apply auto
387   apply (auto simp add: zero_le_mult_iff)
388   apply (insert zero_less_pow2[of b])
389   apply (simp_all)
390   done
392 lemma float_le_zero:
393   "(real (Float a b) <= 0) = (a <= 0)"
394   apply auto
395   apply (auto simp add: mult_le_0_iff)
396   apply (insert zero_less_pow2[of b])
397   apply auto
398   done
400 declare real_of_float_simp[simp del]
402 lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
403   by (cases a, auto simp add: float_pprt.simps zero_le_float float_le_zero float_zero)
405 lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)"
406   by (cases a,  auto simp add: float_nprt.simps zero_le_float float_le_zero float_zero)
409 proof (intro_classes)
410   fix a b c :: float
411   show "a + b + c = a + (b + c)"
412     by (cases a, cases b, cases c, auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
413 next
414   fix a b :: float
415   show "a + b = b + a"
416     by (cases a, cases b, simp add: plus_float.simps)
417 qed
419 instance float :: comm_monoid_mult
420 proof (intro_classes)
421   fix a b c :: float
422   show "a * b * c = a * (b * c)"
423     by (cases a, cases b, cases c, simp add: times_float.simps)
424 next
425   fix a b :: float
426   show "a * b = b * a"
427     by (cases a, cases b, simp add: times_float.simps)
428 next
429   fix a :: float
430   show "1 * a = a"
431     by (cases a, simp add: times_float.simps one_float_def)
432 qed
434 (* Floats do NOT form a cancel_semigroup_add: *)
435 lemma "0 + Float 0 1 = 0 + Float 0 2"
436   by (simp add: plus_float.simps zero_float_def)
438 instance float :: comm_semiring
439 proof (intro_classes)
440   fix a b c :: float
441   show "(a + b) * c = a * c + b * c"
442     by (cases a, cases b, cases c, simp, simp add: plus_float.simps times_float.simps algebra_simps)
443 qed
445 (* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *)
447 instance float :: zero_neq_one
448 proof (intro_classes)
449   show "(0::float) \<noteq> 1"
450     by (simp add: zero_float_def one_float_def)
451 qed
453 lemma float_le_simp: "((x::float) \<le> y) = (0 \<le> y - x)"
454   by (auto simp add: le_float_def)
456 lemma float_less_simp: "((x::float) < y) = (0 < y - x)"
457   by (auto simp add: less_float_def)
459 lemma real_of_float_min: "real (min x y :: float) = min (real x) (real y)" unfolding min_def le_float_def by auto
460 lemma real_of_float_max: "real (max a b :: float) = max (real a) (real b)" unfolding max_def le_float_def by auto
462 lemma float_power: "real (x ^ n :: float) = real x ^ n"
463   by (induct n) simp_all
465 lemma zero_le_pow2[simp]: "0 \<le> pow2 s"
466   apply (subgoal_tac "0 < pow2 s")
467   apply (auto simp only:)
468   apply auto
469   done
471 lemma pow2_less_0_eq_False[simp]: "(pow2 s < 0) = False"
472   apply auto
473   apply (subgoal_tac "0 \<le> pow2 s")
474   apply simp
475   apply simp
476   done
478 lemma pow2_le_0_eq_False[simp]: "(pow2 s \<le> 0) = False"
479   apply auto
480   apply (subgoal_tac "0 < pow2 s")
481   apply simp
482   apply simp
483   done
485 lemma float_pos_m_pos: "0 < Float m e \<Longrightarrow> 0 < m"
486   unfolding less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff
487   by auto
489 lemma float_pos_less1_e_neg: assumes "0 < Float m e" and "Float m e < 1" shows "e < 0"
490 proof -
491   have "0 < m" using float_pos_m_pos `0 < Float m e` by auto
492   hence "0 \<le> real m" and "1 \<le> real m" by auto
494   show "e < 0"
495   proof (rule ccontr)
496     assume "\<not> e < 0" hence "0 \<le> e" by auto
497     hence "1 \<le> pow2 e" unfolding pow2_def by auto
498     from mult_mono[OF `1 \<le> real m` this `0 \<le> real m`]
499     have "1 \<le> Float m e" by (simp add: le_float_def real_of_float_simp)
500     thus False using `Float m e < 1` unfolding less_float_def le_float_def by auto
501   qed
502 qed
504 lemma float_less1_mantissa_bound: assumes "0 < Float m e" "Float m e < 1" shows "m < 2^(nat (-e))"
505 proof -
506   have "e < 0" using float_pos_less1_e_neg assms by auto
507   have "\<And>x. (0::real) < 2^x" by auto
508   have "real m < 2^(nat (-e))" using `Float m e < 1`
509     unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1
510           real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric]
511           real_mult_assoc by auto
512   thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto
513 qed
515 function bitlen :: "int \<Rightarrow> int" where
516 "bitlen 0 = 0" |
517 "bitlen -1 = 1" |
518 "0 < x \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))" |
519 "x < -1 \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))"
520   apply (case_tac "x = 0 \<or> x = -1 \<or> x < -1 \<or> x > 0")
521   apply auto
522   done
523 termination by (relation "measure (nat o abs)", auto)
525 lemma bitlen_ge0: "0 \<le> bitlen x" by (induct x rule: bitlen.induct, auto)
526 lemma bitlen_ge1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> bitlen x" by (induct x rule: bitlen.induct, auto simp add: bitlen_ge0)
528 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")
529   using `0 < x`
530 proof (induct x rule: bitlen.induct)
531   fix x
532   assume "0 < x" and hyp: "0 < x div 2 \<Longrightarrow> ?P (x div 2)" hence "0 \<le> x" and "x \<noteq> 0" by auto
533   { fix x have "0 \<le> 1 + bitlen x" using bitlen_ge0[of x] by auto } note gt0_pls1 = this
535   have "0 < (2::int)" by auto
537   show "?P x"
538   proof (cases "x = 1")
539     case True show "?P x" unfolding True by auto
540   next
541     case False hence "2 \<le> x" using `0 < x` `x \<noteq> 1` by auto
542     hence "2 div 2 \<le> x div 2" by (rule zdiv_mono1, auto)
543     hence "0 < x div 2" and "x div 2 \<noteq> 0" by auto
544     hence bitlen_s1_ge0: "0 \<le> bitlen (x div 2) - 1" using bitlen_ge1[OF `x div 2 \<noteq> 0`] by auto
546     { from hyp[OF `0 < x div 2`]
547       have "2 ^ nat (bitlen (x div 2) - 1) \<le> x div 2" by auto
548       hence "2 ^ nat (bitlen (x div 2) - 1) * 2 \<le> x div 2 * 2" by (rule mult_right_mono, auto)
549       also have "\<dots> \<le> x" using `0 < x` by auto
550       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
551     } moreover
552     { have "x + 1 \<le> x - x mod 2 + 2"
553       proof -
554         have "x mod 2 < 2" using `0 < x` by auto
555         hence "x < x - x mod 2 +  2" unfolding algebra_simps by auto
556         thus ?thesis by auto
557       qed
558       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
559       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)
560       also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto
561       finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" .
562     }
563     ultimately show ?thesis
564       unfolding bitlen.simps(3)[OF `0 < x`] nat_add_distrib[OF zero_le_one bitlen_ge0]
566       by auto
567   qed
568 next
569   fix x :: int assume "x < -1" and "0 < x" hence False by auto
570   thus "?P x" by auto
571 qed auto
573 lemma bitlen_bounds: assumes "0 < x" shows "2^nat (bitlen x - 1) \<le> x \<and> x < 2^nat (bitlen x)"
574   using bitlen_bounds'[OF `0<x`] by auto
576 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"
577 proof -
578   let ?B = "2^nat(bitlen m - 1)"
580   have "?B \<le> m" using bitlen_bounds[OF `0 <m`] ..
581   hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto
582   thus "1 \<le> real m / ?B" by auto
584   have "m \<noteq> 0" using assms by auto
585   have "0 \<le> bitlen m - 1" using bitlen_ge1[OF `m \<noteq> 0`] by auto
587   have "m < 2^nat(bitlen m)" using bitlen_bounds[OF `0 <m`] ..
588   also have "\<dots> = 2^nat(bitlen m - 1 + 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
589   also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF `0 \<le> bitlen m - 1` zero_le_one] by auto
590   finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto
591   hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto)
592   thus "real m / ?B < 2" by auto
593 qed
595 lemma float_gt1_scale: assumes "1 \<le> Float m e"
596   shows "0 \<le> e + (bitlen m - 1)"
597 proof (cases "0 \<le> e")
598   have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto
599   hence "0 < m" using float_pos_m_pos by auto
600   hence "m \<noteq> 0" by auto
601   case True with bitlen_ge1[OF `m \<noteq> 0`] show ?thesis by auto
602 next
603   have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto
604   hence "0 < m" using float_pos_m_pos by auto
605   hence "m \<noteq> 0" and "1 < (2::int)" by auto
606   case False let ?S = "2^(nat (-e))"
607   have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def real_of_float_nge0_exp[OF False] by auto
608   hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
609   hence "?S \<le> real m" unfolding mult_assoc by auto
610   hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto
611   from this bitlen_bounds[OF `0 < m`, THEN conjunct2]
612   have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans)
613   hence "-e < bitlen m" using False bitlen_ge0 by auto
614   thus ?thesis by auto
615 qed
617 lemma normalized_float: assumes "m \<noteq> 0" shows "real (Float m (- (bitlen m - 1))) = real m / 2^nat (bitlen m - 1)"
618 proof (cases "- (bitlen m - 1) = 0")
619   case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto
620 next
621   case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
622   show ?thesis unfolding real_of_float_nge0_exp[OF P] real_divide_def by auto
623 qed
625 lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
627 lemma bitlen_Min: "bitlen (Int.Min) = Int.Bit1 Int.Pls" by (subst Min_def, simp add: Bit1_def)
629 lemma bitlen_B0: "bitlen (Int.Bit0 b) = (if iszero b then Int.Pls else Int.succ (bitlen b))"
630   apply (auto simp add: iszero_def succ_def)
631   apply (simp add: Bit0_def Pls_def)
632   apply (subst Bit0_def)
633   apply simp
634   apply (subgoal_tac "0 < 2 * b \<or> 2 * b < -1")
635   apply auto
636   done
638 lemma bitlen_B1: "bitlen (Int.Bit1 b) = (if iszero (Int.succ b) then Int.Bit1 Int.Pls else Int.succ (bitlen b))"
639 proof -
640   have h: "! x. (2*x + 1) div 2 = (x::int)"
641     by arith
642   show ?thesis
643     apply (auto simp add: iszero_def succ_def)
644     apply (subst Bit1_def)+
645     apply simp
646     apply (subgoal_tac "2 * b + 1 = -1")
647     apply (simp only:)
648     apply simp_all
649     apply (subst Bit1_def)
650     apply simp
651     apply (subgoal_tac "0 < 2 * b + 1 \<or> 2 * b + 1 < -1")
652     apply (auto simp add: h)
653     done
654 qed
656 lemma bitlen_number_of: "bitlen (number_of w) = number_of (bitlen w)"
659 lemma [code]: "bitlen x =
660      (if x = 0  then 0
661  else if x = -1 then 1
662                 else (1 + (bitlen (x div 2))))"
663   by (cases "x = 0 \<or> x = -1 \<or> 0 < x") auto
665 definition lapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
666 where
667   "lapprox_posrat prec x y =
668    (let
669        l = nat (int prec + bitlen y - bitlen x) ;
670        d = (x * 2^l) div y
671     in normfloat (Float d (- (int l))))"
673 lemma pow2_minus: "pow2 (-x) = inverse (pow2 x)"
674   unfolding pow2_neg[of "-x"] by auto
676 lemma lapprox_posrat:
677   assumes x: "0 \<le> x"
678   and y: "0 < y"
679   shows "real (lapprox_posrat prec x y) \<le> real x / real y"
680 proof -
681   let ?l = "nat (int prec + bitlen y - bitlen x)"
683   have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)"
684     by (rule mult_right_mono, fact real_of_int_div4, simp)
685   also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto
686   finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding real_mult_assoc by auto
687   thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp
688     unfolding pow2_minus pow2_int minus_minus .
689 qed
691 lemma real_of_int_div_mult:
692   fixes x y c :: int assumes "0 < y" and "0 < c"
693   shows "real (x div y) \<le> real (x * c div y) * inverse (real c)"
694 proof -
695   have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y]
697         auto intro!: mult_nonneg_nonneg
698              simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`])
699   hence "real (x div y) * real c \<le> real (x * c div y)"
700     unfolding real_of_int_mult[symmetric] real_of_int_le_iff zmult_commute by auto
701   hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
702     using `0 < c` by auto
703   thus ?thesis unfolding real_mult_assoc using `0 < c` by auto
704 qed
706 lemma lapprox_posrat_bottom: assumes "0 < y"
707   shows "real (x div y) \<le> real (lapprox_posrat n x y)"
708 proof -
709   have pow: "\<And>x. (0::int) < 2^x" by auto
710   show ?thesis
711     unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
712     using real_of_int_div_mult[OF `0 < y` pow] by auto
713 qed
715 lemma lapprox_posrat_nonneg: assumes "0 \<le> x" and "0 < y"
716   shows "0 \<le> real (lapprox_posrat n x y)"
717 proof -
718   show ?thesis
719     unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
720     using pos_imp_zdiv_nonneg_iff[OF `0 < y`] assms by (auto intro!: mult_nonneg_nonneg)
721 qed
723 definition rapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
724 where
725   "rapprox_posrat prec x y = (let
726      l = nat (int prec + bitlen y - bitlen x) ;
727      X = x * 2^l ;
728      d = X div y ;
729      m = X mod y
730    in normfloat (Float (d + (if m = 0 then 0 else 1)) (- (int l))))"
732 lemma rapprox_posrat:
733   assumes x: "0 \<le> x"
734   and y: "0 < y"
735   shows "real x / real y \<le> real (rapprox_posrat prec x y)"
736 proof -
737   let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l"
738   show ?thesis
739   proof (cases "?X mod y = 0")
740     case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
741     from real_of_int_div[OF this]
742     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
743     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
744     finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
745     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True]
746       unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
747   next
748     case False
749     have "0 \<le> real y" and "real y \<noteq> 0" using `0 < y` by auto
750     have "0 \<le> real y * 2^?l" by (rule mult_nonneg_nonneg, rule `0 \<le> real y`, auto)
752     have "?X = y * (?X div y) + ?X mod y" by auto
753     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])
754     also have "\<dots> = y * (?X div y + 1)" unfolding zadd_zmult_distrib2 by auto
755     finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] .
756     hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)"
757       by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
758     also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto
759     also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`]
760       unfolding real_divide_def ..
761     finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
762       unfolding pow2_minus pow2_int minus_minus by auto
763   qed
764 qed
766 lemma rapprox_posrat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
767   shows "real (rapprox_posrat n x y) \<le> 1"
768 proof -
769   let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
770   show ?thesis
771   proof (cases "?X mod y = 0")
772     case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
773     from real_of_int_div[OF this]
774     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
775     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
776     finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
777     also have "real x / real y \<le> 1" using `0 \<le> x` and `0 < y` and `x \<le> y` by auto
778     finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True]
779       unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
780   next
781     case False
782     have "x \<noteq> y"
783     proof (rule ccontr)
784       assume "\<not> x \<noteq> y" hence "x = y" by auto
785       have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto
786       thus False using False by auto
787     qed
788     hence "x < y" using `x \<le> y` by auto
789     hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
791     from real_of_int_div4[of "?X" y]
792     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[symmetric] real_number_of .
793     also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto)
794     finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
795     hence "?X div y + 1 \<le> 2^?l" by auto
796     hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)"
797       unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
798       by (rule mult_right_mono, auto)
799     hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
800     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
801       unfolding pow2_minus pow2_int minus_minus by auto
802   qed
803 qed
805 lemma zdiv_greater_zero: fixes a b :: int assumes "0 < a" and "a \<le> b"
806   shows "0 < b div a"
807 proof (rule ccontr)
808   have "0 \<le> b" using assms by auto
809   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
810   have "b = a * (b div a) + b mod a" by auto
811   hence "b = b mod a" unfolding `b div a = 0` by auto
812   hence "b < a" using `0 < a`[THEN pos_mod_bound, of b] by auto
813   thus False using `a \<le> b` by auto
814 qed
816 lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
817   shows "real (rapprox_posrat n x y) < 1"
818 proof (cases "x = 0")
819   case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat real_of_float_simp by auto
820 next
821   case False hence "0 < x" using `0 \<le> x` by auto
822   hence "x < y" using assms by auto
824   let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
825   show ?thesis
826   proof (cases "?X mod y = 0")
827     case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
828     from real_of_int_div[OF this]
829     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
830     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
831     finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
832     also have "real x / real y < 1" using `0 \<le> x` and `0 < y` and `x < y` by auto
833     finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_P[OF True]
834       unfolding pow2_minus pow2_int minus_minus by auto
835   next
836     case False
837     hence "(real x / real y) < 1 / 2" using `0 < y` and `0 \<le> x` `2 * x < y` by auto
839     have "0 < ?X div y"
840     proof -
841       have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)"
842         using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto
843       hence "(2::int)^nat (bitlen x - 1) < 2^nat (bitlen y)" by (rule order_le_less_trans)
844       hence "bitlen x \<le> bitlen y" by auto
845       hence len_less: "nat (bitlen x - 1) \<le> nat (int (n - 1) + bitlen y)" by auto
847       have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto
849       have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l"
850         using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto
852       have "y * 2^nat (bitlen x - 1) \<le> y * x"
853         using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono)
854       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)
855       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`)
856       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))"
857         unfolding real_of_int_le_iff[symmetric] by auto
858       hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))"
859         unfolding real_mult_assoc real_divide_def by auto
860       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
861       finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto
862       thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto
863     qed
865     from real_of_int_div4[of "?X" y]
866     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[symmetric] real_number_of .
867     also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto)
868     finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
869     hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto
870     hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)"
871       unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power[symmetric] real_number_of
872       by (rule mult_strict_right_mono, auto)
873     hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
874     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
875       unfolding pow2_minus pow2_int minus_minus by auto
876   qed
877 qed
879 lemma approx_rat_pattern: fixes P and ps :: "nat * int * int"
880   assumes Y: "\<And>y prec x. \<lbrakk>y = 0; ps = (prec, x, 0)\<rbrakk> \<Longrightarrow> P"
881   and A: "\<And>x y prec. \<lbrakk>0 \<le> x; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
882   and B: "\<And>x y prec. \<lbrakk>x < 0; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
883   and C: "\<And>x y prec. \<lbrakk>x < 0; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
884   and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
885   shows P
886 proof -
887   obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps, auto)
888   from Y have "y = 0 \<Longrightarrow> P" by auto
889   moreover { assume "0 < y" have P proof (cases "0 \<le> x") case True with A and `0 < y` show P by auto next case False with B and `0 < y` show P by auto qed }
890   moreover { assume "y < 0" have P proof (cases "0 \<le> x") case True with D and `y < 0` show P by auto next case False with C and `y < 0` show P by auto qed }
891   ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0", auto)
892 qed
894 function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
895 where
896   "y = 0 \<Longrightarrow> lapprox_rat prec x y = 0"
897 | "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec x y"
898 | "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec (-x) y)"
899 | "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec (-x) (-y)"
900 | "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec x (-y))"
901 apply simp_all by (rule approx_rat_pattern)
902 termination by lexicographic_order
904 lemma compute_lapprox_rat[code]:
905       "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)))
906                                                              else (if 0 < y then - (rapprox_posrat prec (-x) y) else lapprox_posrat prec (-x) (-y)))"
907   by auto
909 lemma lapprox_rat: "real (lapprox_rat prec x y) \<le> real x / real y"
910 proof -
911   have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
912   show ?thesis
913     apply (case_tac "y = 0")
914     apply simp
915     apply (case_tac "0 \<le> x \<and> 0 < y")
917     apply (case_tac "x < 0 \<and> 0 < y")
918     apply simp
919     apply (subst minus_le_iff)
920     apply (rule h[OF rapprox_posrat])
921     apply (simp_all)
922     apply (case_tac "x < 0 \<and> y < 0")
923     apply simp
924     apply (rule h[OF _ lapprox_posrat])
925     apply (simp_all)
926     apply (case_tac "0 \<le> x \<and> y < 0")
927     apply (simp)
928     apply (subst minus_le_iff)
929     apply (rule h[OF rapprox_posrat])
930     apply simp_all
931     apply arith
932     done
933 qed
935 lemma lapprox_rat_bottom: assumes "0 \<le> x" and "0 < y"
936   shows "real (x div y) \<le> real (lapprox_rat n x y)"
937   unfolding lapprox_rat.simps(2)[OF assms]  using lapprox_posrat_bottom[OF `0<y`] .
939 function rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
940 where
941   "y = 0 \<Longrightarrow> rapprox_rat prec x y = 0"
942 | "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec x y"
943 | "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec (-x) y)"
944 | "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec (-x) (-y)"
945 | "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec x (-y))"
946 apply simp_all by (rule approx_rat_pattern)
947 termination by lexicographic_order
949 lemma compute_rapprox_rat[code]:
950       "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
951                                                                   (if 0 < y then - (lapprox_posrat prec (-x) y) else rapprox_posrat prec (-x) (-y)))"
952   by auto
954 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
955 proof -
956   have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
957   show ?thesis
958     apply (case_tac "y = 0")
959     apply simp
960     apply (case_tac "0 \<le> x \<and> 0 < y")
962     apply (case_tac "x < 0 \<and> 0 < y")
963     apply simp
964     apply (subst le_minus_iff)
965     apply (rule h[OF _ lapprox_posrat])
966     apply (simp_all)
967     apply (case_tac "x < 0 \<and> y < 0")
968     apply simp
969     apply (rule h[OF rapprox_posrat])
970     apply (simp_all)
971     apply (case_tac "0 \<le> x \<and> y < 0")
972     apply (simp)
973     apply (subst le_minus_iff)
974     apply (rule h[OF _ lapprox_posrat])
975     apply simp_all
976     apply arith
977     done
978 qed
980 lemma rapprox_rat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
981   shows "real (rapprox_rat n x y) \<le> 1"
982   unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] using rapprox_posrat_le1[OF assms] .
984 lemma rapprox_rat_neg: assumes "x < 0" and "0 < y"
985   shows "real (rapprox_rat n x y) \<le> 0"
986   unfolding rapprox_rat.simps(3)[OF assms] using lapprox_posrat_nonneg[of "-x" y n] assms by auto
988 lemma rapprox_rat_nonneg_neg: assumes "0 \<le> x" and "y < 0"
989   shows "real (rapprox_rat n x y) \<le> 0"
990   unfolding rapprox_rat.simps(5)[OF assms] using lapprox_posrat_nonneg[of x "-y" n] assms by auto
992 lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y"
993   shows "real (rapprox_rat n x y) \<le> 0"
994 proof (cases "x = 0")
995   case True hence "0 \<le> x" by auto show ?thesis unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
996     unfolding True rapprox_posrat_def Let_def by auto
997 next
998   case False hence "x < 0" using assms by auto
999   show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] .
1000 qed
1002 fun float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
1003 where
1004   "float_divl prec (Float m1 s1) (Float m2 s2) =
1005     (let
1006        l = lapprox_rat prec m1 m2;
1007        f = Float 1 (s1 - s2)
1008      in
1009        f * l)"
1011 lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
1012 proof -
1013   from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
1014   from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
1015   have "real mx / real my \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
1016     apply (case_tac "my = 0")
1017     apply simp
1018     apply (case_tac "my > 0")
1019     apply (subst pos_le_divide_eq)
1020     apply simp
1021     apply (subst pos_le_divide_eq)
1023     apply simp
1025     apply simp
1026     apply (subgoal_tac "my < 0")
1027     apply auto
1031     done
1032   then have "real (lapprox_rat prec mx my) \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
1033     by (rule order_trans[OF lapprox_rat])
1034   then have "real (lapprox_rat prec mx my) * pow2 (sx - sy) \<le> real mx * pow2 sx / (real my * pow2 sy)"
1035     apply (subst pos_le_divide_eq[symmetric])
1036     apply simp_all
1037     done
1038   then have "pow2 (sx - sy) * real (lapprox_rat prec mx my) \<le> real mx * pow2 sx / (real my * pow2 sy)"
1040   then show ?thesis
1041     by (simp add: x y Let_def real_of_float_simp)
1042 qed
1044 lemma float_divl_lower_bound: assumes "0 \<le> x" and "0 < y" shows "0 \<le> float_divl prec x y"
1045 proof (cases x, cases y)
1046   fix xm xe ym ye :: int
1047   assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
1048   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
1049   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
1051   have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
1052   moreover have "0 \<le> real (lapprox_rat prec xm ym)" by (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]], auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
1053   ultimately show "0 \<le> float_divl prec x y"
1054     unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0 by (auto intro!: mult_nonneg_nonneg)
1055 qed
1057 lemma float_divl_pos_less1_bound: assumes "0 < x" and "x < 1" and "0 < prec" shows "1 \<le> float_divl prec 1 x"
1058 proof (cases x)
1059   case (Float m e)
1060   from `0 < x` `x < 1` have "0 < m" "e < 0" using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
1061   let ?b = "nat (bitlen m)" and ?e = "nat (-e)"
1062   have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto
1063   with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto
1064   hence "1 \<le> bitlen m" using power_le_imp_le_exp[of "2::int" 1 ?b] by auto
1065   hence pow_split: "nat (int prec + bitlen m - 1) = (prec - 1) + ?b" using `0 < prec` by auto
1067   have pow_not0: "\<And>x. (2::real)^x \<noteq> 0" by auto
1069   from float_less1_mantissa_bound `0 < x` `x < 1` Float
1070   have "m < 2^?e" by auto
1071   with bitlen_bounds[OF `0 < m`, THEN conjunct1]
1072   have "(2::int)^nat (bitlen m - 1) < 2^?e" by (rule order_le_less_trans)
1073   from power_less_imp_less_exp[OF _ this]
1074   have "bitlen m \<le> - e" by auto
1075   hence "(2::real)^?b \<le> 2^?e" by auto
1076   hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)" by (rule mult_right_mono, auto)
1077   hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto
1078   also
1079   let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))"
1080   { have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b" using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono, auto)
1081     also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)" unfolding pow_split zpower_zadd_distrib by auto
1082     finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m" using `0 < m` by (rule zdiv_mono1)
1083     hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
1084     hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
1085       unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
1086   from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"]
1087   have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
1088   finally have "1 \<le> 2^?e * ?d" .
1090   have e_nat: "0 - e = int (nat (-e))" using `e < 0` by auto
1091   have "bitlen 1 = 1" using bitlen.simps by auto
1093   show ?thesis
1094     unfolding one_float_def Float float_divl.simps Let_def lapprox_rat.simps(2)[OF zero_le_one `0 < m`] lapprox_posrat_def `bitlen 1 = 1`
1095     unfolding le_float_def real_of_float_mult normfloat real_of_float_simp pow2_minus pow2_int e_nat
1096     using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def)
1097 qed
1099 fun float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
1100 where
1101   "float_divr prec (Float m1 s1) (Float m2 s2) =
1102     (let
1103        r = rapprox_rat prec m1 m2;
1104        f = Float 1 (s1 - s2)
1105      in
1106        f * r)"
1108 lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
1109 proof -
1110   from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
1111   from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
1112   have "real mx / real my \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
1113     apply (case_tac "my = 0")
1114     apply simp
1115     apply (case_tac "my > 0")
1116     apply auto
1117     apply (subst pos_divide_le_eq)
1118     apply (rule mult_pos_pos)+
1119     apply simp_all
1121     apply simp
1122     apply (subgoal_tac "my < 0")
1123     apply auto
1127     done
1128   then have "real (rapprox_rat prec mx my) \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
1129     by (rule order_trans[OF _ rapprox_rat])
1130   then have "real (rapprox_rat prec mx my) * pow2 (sx - sy) \<ge> real mx * pow2 sx / (real my * pow2 sy)"
1131     apply (subst pos_divide_le_eq[symmetric])
1132     apply simp_all
1133     done
1134   then show ?thesis
1135     by (simp add: x y Let_def algebra_simps real_of_float_simp)
1136 qed
1138 lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
1139 proof -
1140   have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto
1141   also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
1142   finally show ?thesis unfolding le_float_def by auto
1143 qed
1145 lemma float_divr_nonpos_pos_upper_bound: assumes "x \<le> 0" and "0 < y" shows "float_divr prec x y \<le> 0"
1146 proof (cases x, cases y)
1147   fix xm xe ym ye :: int
1148   assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
1149   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
1150   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
1152   have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
1153   moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] .
1154   ultimately show "float_divr prec x y \<le> 0"
1155     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)
1156 qed
1158 lemma float_divr_nonneg_neg_upper_bound: assumes "0 \<le> x" and "y < 0" shows "float_divr prec x y \<le> 0"
1159 proof (cases x, cases y)
1160   fix xm xe ym ye :: int
1161   assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
1162   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
1163   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
1164   hence "0 < - ym" by auto
1166   have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
1167   moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] .
1168   ultimately show "float_divr prec x y \<le> 0"
1169     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)
1170 qed
1172 primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
1173 "round_down prec (Float m e) = (let d = bitlen m - int prec in
1174      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
1175               else Float m e)"
1177 primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
1178 "round_up prec (Float m e) = (let d = bitlen m - int prec in
1179   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)
1180            else Float m e)"
1182 lemma round_up: "real x \<le> real (round_up prec x)"
1183 proof (cases x)
1184   case (Float m e)
1185   let ?d = "bitlen m - int prec"
1186   let ?p = "(2::int)^nat ?d"
1187   have "0 < ?p" by auto
1188   show "?thesis"
1189   proof (cases "0 < ?d")
1190     case True
1191     hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
1192     show ?thesis
1193     proof (cases "m mod ?p = 0")
1194       case True
1195       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] .
1196       have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
1198       thus ?thesis
1199         unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`]
1200         by auto
1201     next
1202       case False
1203       have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
1204       also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib zmult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
1205       finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
1206         unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
1207         by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
1208       thus ?thesis
1209         unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] .
1210     qed
1211   next
1212     case False
1213     show ?thesis
1214       unfolding Float round_up.simps Let_def if_not_P[OF False] ..
1215   qed
1216 qed
1218 lemma round_down: "real (round_down prec x) \<le> real x"
1219 proof (cases x)
1220   case (Float m e)
1221   let ?d = "bitlen m - int prec"
1222   let ?p = "(2::int)^nat ?d"
1223   have "0 < ?p" by auto
1224   show "?thesis"
1225   proof (cases "0 < ?d")
1226     case True
1227     hence pow_d: "pow2 ?d = real ?p" unfolding pow2_int[symmetric] power_real_number_of[symmetric] by auto
1228     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])
1229     also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
1230     finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
1231       unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric]
1232       by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
1233     thus ?thesis
1234       unfolding Float round_down.simps Let_def if_P[OF `0 < ?d`] .
1235   next
1236     case False
1237     show ?thesis
1238       unfolding Float round_down.simps Let_def if_not_P[OF False] ..
1239   qed
1240 qed
1242 definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1243 "lb_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
1244     l = bitlen m - int prec
1245   in if l > 0 then Float (m div (2^nat l)) (e + l)
1246               else Float m e)"
1248 definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1249 "ub_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
1250     l = bitlen m - int prec
1251   in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
1252               else Float m e)"
1254 lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)"
1255 proof (cases "normfloat (x * y)")
1256   case (Float m e)
1257   hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero)
1258   let ?l = "bitlen m - int prec"
1259   have "real (lb_mult prec x y) \<le> real (normfloat (x * y))"
1260   proof (cases "?l > 0")
1261     case False thus ?thesis unfolding lb_mult_def Float Let_def float.cases by auto
1262   next
1263     case True
1264     have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
1265     proof -
1266       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[symmetric] real_number_of unfolding pow2_int[symmetric]
1267         using `?l > 0` by auto
1268       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
1269       also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
1270       finally show ?thesis by auto
1271     qed
1272     thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
1273   qed
1274   also have "\<dots> = real (x * y)" unfolding normfloat ..
1275   finally show ?thesis .
1276 qed
1278 lemma ub_mult: "real (x * y) \<le> real (ub_mult prec x y)"
1279 proof (cases "normfloat (x * y)")
1280   case (Float m e)
1281   hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero)
1282   let ?l = "bitlen m - int prec"
1283   have "real (x * y) = real (normfloat (x * y))" unfolding normfloat ..
1284   also have "\<dots> \<le> real (ub_mult prec x y)"
1285   proof (cases "?l > 0")
1286     case False thus ?thesis unfolding ub_mult_def Float Let_def float.cases by auto
1287   next
1288     case True
1289     have "real m \<le> real (m div 2^(nat ?l) + 1) * pow2 ?l"
1290     proof -
1291       have "m mod 2^(nat ?l) < 2^(nat ?l)" by (rule pos_mod_bound) auto
1292       hence mod_uneq: "real (m mod 2^(nat ?l)) \<le> 1 * 2^(nat ?l)" unfolding zmult_1 real_of_int_less_iff[symmetric] by auto
1294       have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
1295       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
1296       also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding real_add_mult_distrib using mod_uneq by auto
1297       finally show ?thesis unfolding pow2_int[symmetric] using True by auto
1298     qed
1299     thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
1300   qed
1301   finally show ?thesis .
1302 qed
1304 primrec float_abs :: "float \<Rightarrow> float" where
1305   "float_abs (Float m e) = Float \<bar>m\<bar> e"
1307 instantiation float :: abs begin
1308 definition abs_float_def: "\<bar>x\<bar> = float_abs x"
1309 instance ..
1310 end
1312 lemma real_of_float_abs: "real \<bar>x :: float\<bar> = \<bar>real x\<bar>"
1313 proof (cases x)
1314   case (Float m e)
1315   have "\<bar>real m\<bar> * pow2 e = \<bar>real m * pow2 e\<bar>" unfolding abs_mult by auto
1316   thus ?thesis unfolding Float abs_float_def float_abs.simps real_of_float_simp by auto
1317 qed
1319 primrec floor_fl :: "float \<Rightarrow> float" where
1320   "floor_fl (Float m e) = (if 0 \<le> e then Float m e
1321                                   else Float (m div (2 ^ (nat (-e)))) 0)"
1323 lemma floor_fl: "real (floor_fl x) \<le> real x"
1324 proof (cases x)
1325   case (Float m e)
1326   show ?thesis
1327   proof (cases "0 \<le> e")
1328     case False
1329     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
1330     have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
1331     also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
1332     also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
1333     also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
1334     finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
1335   next
1336     case True thus ?thesis unfolding Float by auto
1337   qed
1338 qed
1340 lemma floor_pos_exp: assumes floor: "Float m e = floor_fl x" shows "0 \<le> e"
1341 proof (cases x)
1342   case (Float mx me)
1343   from floor[unfolded Float floor_fl.simps] show ?thesis by (cases "0 \<le> me", auto)
1344 qed
1346 declare floor_fl.simps[simp del]
1348 primrec ceiling_fl :: "float \<Rightarrow> float" where
1349   "ceiling_fl (Float m e) = (if 0 \<le> e then Float m e
1350                                     else Float (m div (2 ^ (nat (-e))) + 1) 0)"
1352 lemma ceiling_fl: "real x \<le> real (ceiling_fl x)"
1353 proof (cases x)
1354   case (Float m e)
1355   show ?thesis
1356   proof (cases "0 \<le> e")
1357     case False
1358     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
1359     have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
1360     also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding power_real_number_of[symmetric] real_divide_def ..
1361     also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
1362     also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
1363     finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
1364   next
1365     case True thus ?thesis unfolding Float by auto
1366   qed
1367 qed
1369 declare ceiling_fl.simps[simp del]
1371 definition lb_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1372 "lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
1374 definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
1375 "ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
1377 lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x")
1378   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
1379   shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y"
1380 proof -
1381   have "?lb \<le> ?ub" using assms by auto
1382   have "0 \<le> ?lb" and "?lb \<noteq> 0" using assms by auto
1383   have "?k * y \<le> ?x" using assms by auto
1384   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`])
1385   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)
1386   finally show ?thesis unfolding lb_mod_def real_of_float_sub real_of_float_mult by auto
1387 qed
1389 lemma ub_mod: fixes k :: int and x :: float assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
1390   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
1391   shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
1392 proof -
1393   have "?lb \<le> ?ub" using assms by auto
1394   hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" using assms by auto
1395   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)
1396   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`])
1397   also have "\<dots> \<le> ?k * y" using assms by auto
1398   finally show ?thesis unfolding ub_mod_def real_of_float_sub real_of_float_mult by auto
1399 qed
1401 lemma le_float_def': "f \<le> g = (case f - g of Float a b \<Rightarrow> a \<le> 0)"
1402 proof -
1403   have le_transfer: "(f \<le> g) = (real (f - g) \<le> 0)" by (auto simp add: le_float_def)
1404   from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
1405   with le_transfer have le_transfer': "f \<le> g = (real (Float a b) \<le> 0)" by simp
1406   show ?thesis by (simp add: le_transfer' f_diff_g float_le_zero)
1407 qed
1409 lemma float_less_zero:
1410   "(real (Float a b) < 0) = (a < 0)"
1411   apply (auto simp add: mult_less_0_iff real_of_float_simp)
1412   done
1414 lemma less_float_def': "f < g = (case f - g of Float a b \<Rightarrow> a < 0)"
1415 proof -
1416   have less_transfer: "(f < g) = (real (f - g) < 0)" by (auto simp add: less_float_def)
1417   from float_split[of "f - g"] obtain a b where f_diff_g: "f - g = Float a b" by auto
1418   with less_transfer have less_transfer': "f < g = (real (Float a b) < 0)" by simp
1419   show ?thesis by (simp add: less_transfer' f_diff_g float_less_zero)
1420 qed
1422 end