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