src/HOL/Matrix/ComputeFloat.thy
author wenzelm
Wed Sep 02 16:25:44 2009 +0200 (2009-09-02)
changeset 32491 d5d8bea0cd94
parent 29804 src/HOL/Tools/ComputeFloat.thy@e15b74577368
child 35032 7efe662e41b4
permissions -rw-r--r--
reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools;
     1 (*  Title:  HOL/Tools/ComputeFloat.thy
     2     Author: Steven Obua
     3 *)
     4 
     5 header {* Floating Point Representation of the Reals *}
     6 
     7 theory ComputeFloat
     8 imports Complex_Main
     9 uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
    10 begin
    11 
    12 definition
    13   pow2 :: "int \<Rightarrow> real" where
    14   "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
    15 
    16 definition
    17   float :: "int * int \<Rightarrow> real" where
    18   "float x = real (fst x) * pow2 (snd x)"
    19 
    20 lemma pow2_0[simp]: "pow2 0 = 1"
    21 by (simp add: pow2_def)
    22 
    23 lemma pow2_1[simp]: "pow2 1 = 2"
    24 by (simp add: pow2_def)
    25 
    26 lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
    27 by (simp add: pow2_def)
    28 
    29 lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
    30 proof -
    31   have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
    32   have g: "! a b. a - -1 = a + (1::int)" by arith
    33   have pos: "! n. pow2 (int n + 1) = 2 * pow2 (int n)"
    34     apply (auto, induct_tac n)
    35     apply (simp_all add: pow2_def)
    36     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
    37     by (auto simp add: h)
    38   show ?thesis
    39   proof (induct a)
    40     case (1 n)
    41     from pos show ?case by (simp add: algebra_simps)
    42   next
    43     case (2 n)
    44     show ?case
    45       apply (auto)
    46       apply (subst pow2_neg[of "- int n"])
    47       apply (subst pow2_neg[of "-1 - int n"])
    48       apply (auto simp add: g pos)
    49       done
    50   qed
    51 qed
    52 
    53 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
    54 proof (induct b)
    55   case (1 n)
    56   show ?case
    57   proof (induct n)
    58     case 0
    59     show ?case by simp
    60   next
    61     case (Suc m)
    62     show ?case by (auto simp add: algebra_simps pow2_add1 prems)
    63   qed
    64 next
    65   case (2 n)
    66   show ?case
    67   proof (induct n)
    68     case 0
    69     show ?case
    70       apply (auto)
    71       apply (subst pow2_neg[of "a + -1"])
    72       apply (subst pow2_neg[of "-1"])
    73       apply (simp)
    74       apply (insert pow2_add1[of "-a"])
    75       apply (simp add: algebra_simps)
    76       apply (subst pow2_neg[of "-a"])
    77       apply (simp)
    78       done
    79     case (Suc m)
    80     have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
    81     have b: "int m - -2 = 1 + (int m + 1)" by arith
    82     show ?case
    83       apply (auto)
    84       apply (subst pow2_neg[of "a + (-2 - int m)"])
    85       apply (subst pow2_neg[of "-2 - int m"])
    86       apply (auto simp add: algebra_simps)
    87       apply (subst a)
    88       apply (subst b)
    89       apply (simp only: pow2_add1)
    90       apply (subst pow2_neg[of "int m - a + 1"])
    91       apply (subst pow2_neg[of "int m + 1"])
    92       apply auto
    93       apply (insert prems)
    94       apply (auto simp add: algebra_simps)
    95       done
    96   qed
    97 qed
    98 
    99 lemma "float (a, e) + float (b, e) = float (a + b, e)"
   100 by (simp add: float_def algebra_simps)
   101 
   102 definition
   103   int_of_real :: "real \<Rightarrow> int" where
   104   "int_of_real x = (SOME y. real y = x)"
   105 
   106 definition
   107   real_is_int :: "real \<Rightarrow> bool" where
   108   "real_is_int x = (EX (u::int). x = real u)"
   109 
   110 lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
   111 by (auto simp add: real_is_int_def int_of_real_def)
   112 
   113 lemma float_transfer: "real_is_int ((real a)*(pow2 c)) \<Longrightarrow> float (a, b) = float (int_of_real ((real a)*(pow2 c)), b - c)"
   114 by (simp add: float_def real_is_int_def2 pow2_add[symmetric])
   115 
   116 lemma pow2_int: "pow2 (int c) = 2^c"
   117 by (simp add: pow2_def)
   118 
   119 lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
   120 by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric])
   121 
   122 lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
   123 by (auto simp add: real_is_int_def int_of_real_def)
   124 
   125 lemma int_of_real_real[simp]: "int_of_real (real x) = x"
   126 by (simp add: int_of_real_def)
   127 
   128 lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real (int_of_real x) = x"
   129 by (auto simp add: int_of_real_def real_is_int_def)
   130 
   131 lemma real_is_int_add_int_of_real: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)"
   132 by (auto simp add: int_of_real_def real_is_int_def)
   133 
   134 lemma real_is_int_add[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a+b)"
   135 apply (subst real_is_int_def2)
   136 apply (simp add: real_is_int_add_int_of_real real_int_of_real)
   137 done
   138 
   139 lemma int_of_real_sub: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)"
   140 by (auto simp add: int_of_real_def real_is_int_def)
   141 
   142 lemma real_is_int_sub[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a-b)"
   143 apply (subst real_is_int_def2)
   144 apply (simp add: int_of_real_sub real_int_of_real)
   145 done
   146 
   147 lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
   148 by (auto simp add: real_is_int_def)
   149 
   150 lemma int_of_real_mult:
   151   assumes "real_is_int a" "real_is_int b"
   152   shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
   153 proof -
   154   from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
   155   from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
   156   from a obtain a'::int where a':"a = real a'" by auto
   157   from b obtain b'::int where b':"b = real b'" by auto
   158   have r: "real a' * real b' = real (a' * b')" by auto
   159   show ?thesis
   160     apply (simp add: a' b')
   161     apply (subst r)
   162     apply (simp only: int_of_real_real)
   163     done
   164 qed
   165 
   166 lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)"
   167 apply (subst real_is_int_def2)
   168 apply (simp add: int_of_real_mult)
   169 done
   170 
   171 lemma real_is_int_0[simp]: "real_is_int (0::real)"
   172 by (simp add: real_is_int_def int_of_real_def)
   173 
   174 lemma real_is_int_1[simp]: "real_is_int (1::real)"
   175 proof -
   176   have "real_is_int (1::real) = real_is_int(real (1::int))" by auto
   177   also have "\<dots> = True" by (simp only: real_is_int_real)
   178   ultimately show ?thesis by auto
   179 qed
   180 
   181 lemma real_is_int_n1: "real_is_int (-1::real)"
   182 proof -
   183   have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
   184   also have "\<dots> = True" by (simp only: real_is_int_real)
   185   ultimately show ?thesis by auto
   186 qed
   187 
   188 lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
   189 proof -
   190   have neg1: "real_is_int (-1::real)"
   191   proof -
   192     have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
   193     also have "\<dots> = True" by (simp only: real_is_int_real)
   194     ultimately show ?thesis by auto
   195   qed
   196 
   197   {
   198     fix x :: int
   199     have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
   200       unfolding number_of_eq
   201       apply (induct x)
   202       apply (induct_tac n)
   203       apply (simp)
   204       apply (simp)
   205       apply (induct_tac n)
   206       apply (simp add: neg1)
   207     proof -
   208       fix n :: nat
   209       assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
   210       have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
   211       show "real_is_int (of_int (- (int (Suc (Suc n)))))"
   212         apply (simp only: s of_int_add)
   213         apply (rule real_is_int_add)
   214         apply (simp add: neg1)
   215         apply (simp only: rn)
   216         done
   217     qed
   218   }
   219   note Abs_Bin = this
   220   {
   221     fix x :: int
   222     have "? u. x = u"
   223       apply (rule exI[where x = "x"])
   224       apply (simp)
   225       done
   226   }
   227   then obtain u::int where "x = u" by auto
   228   with Abs_Bin show ?thesis by auto
   229 qed
   230 
   231 lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
   232 by (simp add: int_of_real_def)
   233 
   234 lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
   235 proof -
   236   have 1: "(1::real) = real (1::int)" by auto
   237   show ?thesis by (simp only: 1 int_of_real_real)
   238 qed
   239 
   240 lemma int_of_real_number_of[simp]: "int_of_real (number_of b) = number_of b"
   241 proof -
   242   have "real_is_int (number_of b)" by simp
   243   then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
   244   then obtain u::int where u:"number_of b = real u" by auto
   245   have "number_of b = real ((number_of b)::int)"
   246     by (simp add: number_of_eq real_of_int_def)
   247   have ub: "number_of b = real ((number_of b)::int)"
   248     by (simp add: number_of_eq real_of_int_def)
   249   from uu u ub have unb: "u = number_of b"
   250     by blast
   251   have "int_of_real (number_of b) = u" by (simp add: u)
   252   with unb show ?thesis by simp
   253 qed
   254 
   255 lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
   256   apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
   257   apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps)
   258   apply (auto)
   259 proof -
   260   fix q::int
   261   have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
   262   show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
   263     by (simp add: a)
   264 qed
   265 
   266 lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
   267 by (rule zdiv_int)
   268 
   269 lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
   270 by (rule zmod_int)
   271 
   272 lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
   273 by arith
   274 
   275 function norm_float :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
   276   "norm_float a b = (if a \<noteq> 0 \<and> even a then norm_float (a div 2) (b + 1)
   277     else if a = 0 then (0, 0) else (a, b))"
   278 by auto
   279 
   280 termination by (relation "measure (nat o abs o fst)")
   281   (auto intro: abs_div_2_less)
   282 
   283 lemma norm_float: "float x = float (split norm_float x)"
   284 proof -
   285   {
   286     fix a b :: int
   287     have norm_float_pair: "float (a, b) = float (norm_float a b)"
   288     proof (induct a b rule: norm_float.induct)
   289       case (1 u v)
   290       show ?case
   291       proof cases
   292         assume u: "u \<noteq> 0 \<and> even u"
   293         with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
   294         with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
   295         then show ?thesis
   296           apply (subst norm_float.simps)
   297           apply (simp add: ind)
   298           done
   299       next
   300         assume "~(u \<noteq> 0 \<and> even u)"
   301         then show ?thesis
   302           by (simp add: prems float_def)
   303       qed
   304     qed
   305   }
   306   note helper = this
   307   have "? a b. x = (a,b)" by auto
   308   then obtain a b where "x = (a, b)" by blast
   309   then show ?thesis by (simp add: helper)
   310 qed
   311 
   312 lemma float_add_l0: "float (0, e) + x = x"
   313   by (simp add: float_def)
   314 
   315 lemma float_add_r0: "x + float (0, e) = x"
   316   by (simp add: float_def)
   317 
   318 lemma float_add:
   319   "float (a1, e1) + float (a2, e2) =
   320   (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
   321   else float (a1*2^(nat (e1-e2))+a2, e2))"
   322   apply (simp add: float_def algebra_simps)
   323   apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
   324   done
   325 
   326 lemma float_add_assoc1:
   327   "(x + float (y1, e1)) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
   328   by simp
   329 
   330 lemma float_add_assoc2:
   331   "(float (y1, e1) + x) + float (y2, e2) = (float (y1, e1) + float (y2, e2)) + x"
   332   by simp
   333 
   334 lemma float_add_assoc3:
   335   "float (y1, e1) + (x + float (y2, e2)) = (float (y1, e1) + float (y2, e2)) + x"
   336   by simp
   337 
   338 lemma float_add_assoc4:
   339   "float (y1, e1) + (float (y2, e2) + x) = (float (y1, e1) + float (y2, e2)) + x"
   340   by simp
   341 
   342 lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
   343   by (simp add: float_def)
   344 
   345 lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
   346   by (simp add: float_def)
   347 
   348 definition 
   349   lbound :: "real \<Rightarrow> real"
   350 where
   351   "lbound x = min 0 x"
   352 
   353 definition
   354   ubound :: "real \<Rightarrow> real"
   355 where
   356   "ubound x = max 0 x"
   357 
   358 lemma lbound: "lbound x \<le> x"   
   359   by (simp add: lbound_def)
   360 
   361 lemma ubound: "x \<le> ubound x"
   362   by (simp add: ubound_def)
   363 
   364 lemma float_mult:
   365   "float (a1, e1) * float (a2, e2) =
   366   (float (a1 * a2, e1 + e2))"
   367   by (simp add: float_def pow2_add)
   368 
   369 lemma float_minus:
   370   "- (float (a,b)) = float (-a, b)"
   371   by (simp add: float_def)
   372 
   373 lemma zero_less_pow2:
   374   "0 < pow2 x"
   375 proof -
   376   {
   377     fix y
   378     have "0 <= y \<Longrightarrow> 0 < pow2 y"
   379       by (induct y, induct_tac n, simp_all add: pow2_add)
   380   }
   381   note helper=this
   382   show ?thesis
   383     apply (case_tac "0 <= x")
   384     apply (simp add: helper)
   385     apply (subst pow2_neg)
   386     apply (simp add: helper)
   387     done
   388 qed
   389 
   390 lemma zero_le_float:
   391   "(0 <= float (a,b)) = (0 <= a)"
   392   apply (auto simp add: float_def)
   393   apply (auto simp add: zero_le_mult_iff zero_less_pow2)
   394   apply (insert zero_less_pow2[of b])
   395   apply (simp_all)
   396   done
   397 
   398 lemma float_le_zero:
   399   "(float (a,b) <= 0) = (a <= 0)"
   400   apply (auto simp add: float_def)
   401   apply (auto simp add: mult_le_0_iff)
   402   apply (insert zero_less_pow2[of b])
   403   apply auto
   404   done
   405 
   406 lemma float_abs:
   407   "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
   408   apply (auto simp add: abs_if)
   409   apply (simp_all add: zero_le_float[symmetric, of a b] float_minus)
   410   done
   411 
   412 lemma float_zero:
   413   "float (0, b) = 0"
   414   by (simp add: float_def)
   415 
   416 lemma float_pprt:
   417   "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
   418   by (auto simp add: zero_le_float float_le_zero float_zero)
   419 
   420 lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
   421   apply (simp add: float_def)
   422   apply (rule pprt_eq_0)
   423   apply (simp add: lbound_def)
   424   done
   425 
   426 lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
   427   apply (simp add: float_def)
   428   apply (rule nprt_eq_0)
   429   apply (simp add: ubound_def)
   430   done
   431 
   432 lemma float_nprt:
   433   "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
   434   by (auto simp add: zero_le_float float_le_zero float_zero)
   435 
   436 lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
   437   by auto
   438 
   439 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
   440   by simp
   441 
   442 lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
   443   by simp
   444 
   445 lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
   446   by simp
   447 
   448 lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
   449   by simp
   450 
   451 lemma int_pow_0: "(a::int)^(Numeral0) = 1"
   452   by simp
   453 
   454 lemma int_pow_1: "(a::int)^(Numeral1) = a"
   455   by simp
   456 
   457 lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
   458   by simp
   459 
   460 lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
   461   by simp
   462 
   463 lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
   464   by simp
   465 
   466 lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
   467   by simp
   468 
   469 lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
   470   by simp
   471 
   472 lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
   473 proof -
   474   have 1:"((-1)::nat) = 0"
   475     by simp
   476   show ?thesis by (simp add: 1)
   477 qed
   478 
   479 lemma fst_cong: "a=a' \<Longrightarrow> fst (a,b) = fst (a',b)"
   480   by simp
   481 
   482 lemma snd_cong: "b=b' \<Longrightarrow> snd (a,b) = snd (a,b')"
   483   by simp
   484 
   485 lemma lift_bool: "x \<Longrightarrow> x=True"
   486   by simp
   487 
   488 lemma nlift_bool: "~x \<Longrightarrow> x=False"
   489   by simp
   490 
   491 lemma not_false_eq_true: "(~ False) = True" by simp
   492 
   493 lemma not_true_eq_false: "(~ True) = False" by simp
   494 
   495 lemmas binarith =
   496   normalize_bin_simps
   497   pred_bin_simps succ_bin_simps
   498   add_bin_simps minus_bin_simps mult_bin_simps
   499 
   500 lemma int_eq_number_of_eq:
   501   "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
   502   by (rule eq_number_of_eq)
   503 
   504 lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
   505   by (simp only: iszero_number_of_Pls)
   506 
   507 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
   508   by simp
   509 
   510 lemma int_iszero_number_of_Bit0: "iszero ((number_of (Int.Bit0 w))::int) = iszero ((number_of w)::int)"
   511   by simp
   512 
   513 lemma int_iszero_number_of_Bit1: "\<not> iszero ((number_of (Int.Bit1 w))::int)"
   514   by simp
   515 
   516 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   517   unfolding neg_def number_of_is_id by simp
   518 
   519 lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
   520   by simp
   521 
   522 lemma int_neg_number_of_Min: "neg (-1::int)"
   523   by simp
   524 
   525 lemma int_neg_number_of_Bit0: "neg ((number_of (Int.Bit0 w))::int) = neg ((number_of w)::int)"
   526   by simp
   527 
   528 lemma int_neg_number_of_Bit1: "neg ((number_of (Int.Bit1 w))::int) = neg ((number_of w)::int)"
   529   by simp
   530 
   531 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   532   unfolding neg_def number_of_is_id by (simp add: not_less)
   533 
   534 lemmas intarithrel =
   535   int_eq_number_of_eq
   536   lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_Bit0
   537   lift_bool[OF int_iszero_number_of_Bit1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
   538   int_neg_number_of_Bit0 int_neg_number_of_Bit1 int_le_number_of_eq
   539 
   540 lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   541   by simp
   542 
   543 lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   544   by simp
   545 
   546 lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
   547   by simp
   548 
   549 lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   550   by simp
   551 
   552 lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
   553 
   554 lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
   555 
   556 lemmas powerarith = nat_number_of zpower_number_of_even
   557   zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
   558   zpower_Pls zpower_Min
   559 
   560 lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 
   561           float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound
   562 
   563 (* for use with the compute oracle *)
   564 lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
   565 
   566 use "~~/src/HOL/Tools/float_arith.ML"
   567 
   568 end