# HG changeset patch
# User hoelzl
# Date 1334829330 -7200
# Node ID 050718fe6eeef15d5ed82f05aa567e616b2cfa8e
# Parent  e12289b5796bdc69aaea6877a52a1a45e603256e
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems

diff -r e12289b5796b -r 050718fe6eee src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Apr 18 14:29:22 2012 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 19 11:55:30 2012 +0200
@@ -634,7 +634,7 @@
 
         have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
 
-        have "arctan (1 / x) \<le> arctan ?invx" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divr)
+        have "arctan (1 / x) \<le> arctan ?invx" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divr)
         also have "\<dots> \<le> (?ub_horner ?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
         finally have "pi / 2 - (?ub_horner ?invx) \<le> arctan x"
           using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
@@ -726,7 +726,7 @@
       have "1 / x \<noteq> 0" and "0 < 1 / x" using `0 < real x` by auto
 
       have "(?lb_horner ?invx) \<le> arctan (?invx)" using arctan_0_1_bounds[OF `0 \<le> real ?invx` `real ?invx \<le> 1`] by auto
-      also have "\<dots> \<le> arctan (1 / x)" unfolding real_of_float_one[symmetric] by (rule arctan_monotone', rule float_divl)
+      also have "\<dots> \<le> arctan (1 / x)" unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone', rule float_divl)
       finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)"
         using `0 \<le> arctan x` arctan_inverse[OF `1 / x \<noteq> 0`]
         unfolding real_sgn_pos[OF `0 < 1 / x`] le_diff_eq by auto
@@ -749,8 +749,8 @@
   case False hence "x < 0" and "0 \<le> real ?mx" by auto
   hence bounds: "lb_arctan prec ?mx \<le> arctan ?mx \<and> arctan ?mx \<le> ub_arctan prec ?mx"
     using ub_arctan_bound'[OF `0 \<le> real ?mx`] lb_arctan_bound'[OF `0 \<le> real ?mx`] by auto
-  show ?thesis unfolding real_of_float_minus arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`]
-    unfolding atLeastAtMost_iff using bounds[unfolded real_of_float_minus arctan_minus]
+  show ?thesis unfolding minus_float.rep_eq arctan_minus lb_arctan.simps[where x=x] ub_arctan.simps[where x=x] Let_def if_P[OF `x < 0`]
+    unfolding atLeastAtMost_iff using bounds[unfolded minus_float.rep_eq arctan_minus]
     by (simp add: arctan_minus)
 qed
 
@@ -783,6 +783,7 @@
 | "lb_sin_cos_aux prec 0 i k x = 0"
 | "lb_sin_cos_aux prec (Suc n) i k x =
     (lapprox_rat prec 1 k) - x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)"
+
 lemma cos_aux:
   shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
   and "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
@@ -880,7 +881,7 @@
     hence "get_even n = 0" by auto
     have "- (pi / 2) \<le> x" by (rule order_trans[OF _ `0 < real x`[THEN less_imp_le]], auto)
     with `x \<le> pi / 2`
-    show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps real_of_float_minus real_of_float_zero using cos_ge_zero by auto
+    show ?thesis unfolding `get_even n = 0` lb_sin_cos_aux.simps minus_float.rep_eq zero_float.rep_eq using cos_ge_zero by auto
   qed
   ultimately show ?thesis by auto
 next
@@ -995,7 +996,7 @@
     case False
     hence "get_even n = 0" by auto
     with `x \<le> pi / 2` `0 \<le> real x`
-    show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps real_of_float_minus using sin_ge_zero by auto
+    show ?thesis unfolding `get_even n = 0` ub_sin_cos_aux.simps minus_float.rep_eq using sin_ge_zero by auto
   qed
   ultimately show ?thesis by auto
 next
@@ -1214,7 +1215,7 @@
       using lb_cos_minus[OF pi_lx lx_0] by simp
     also have "\<dots> \<le> cos (x + (-k) * (2 * pi))"
       using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
-      by (simp only: real_of_float_uminus real_of_int_minus
+      by (simp only: uminus_float.rep_eq real_of_int_minus
         cos_minus diff_minus mult_minus_left)
     finally have "(lb_cos prec (- ?lx)) \<le> cos x"
       unfolding cos_periodic_int . }
@@ -1242,7 +1243,7 @@
 
     have "cos (x + (-k) * (2 * pi)) \<le> cos (real (- ?ux))"
       using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
-      by (simp only: real_of_float_uminus real_of_int_minus
+      by (simp only: uminus_float.rep_eq real_of_int_minus
           cos_minus diff_minus mult_minus_left)
     also have "\<dots> \<le> (ub_cos prec (- ?ux))"
       using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
@@ -1334,10 +1335,10 @@
         unfolding cos_periodic_int ..
       also have "\<dots> \<le> cos ((?ux - 2 * ?lpi))"
         using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
-        by (simp only: real_of_float_minus real_of_int_minus real_of_one minus_one[symmetric]
+        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one minus_one[symmetric]
             diff_minus mult_minus_left mult_1_left)
       also have "\<dots> = cos ((- (?ux - 2 * ?lpi)))"
-        unfolding real_of_float_uminus cos_minus ..
+        unfolding uminus_float.rep_eq cos_minus ..
       also have "\<dots> \<le> (ub_cos prec (- (?ux - 2 * ?lpi)))"
         using lb_cos_minus[OF pi_ux ux_0] by simp
       finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -1378,7 +1379,7 @@
         unfolding cos_periodic_int ..
       also have "\<dots> \<le> cos ((?lx + 2 * ?lpi))"
         using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
-        by (simp only: real_of_float_minus real_of_int_minus real_of_one
+        by (simp only: minus_float.rep_eq real_of_int_minus real_of_one
           minus_one[symmetric] diff_minus mult_minus_left mult_1_left)
       also have "\<dots> \<le> (ub_cos prec (?lx + 2 * ?lpi))"
         using lb_cos[OF lx_0 pi_lx] by simp
@@ -1534,7 +1535,7 @@
     proof -
       have div_less_zero: "real (float_divr prec x (- floor_fl x)) \<le> 0"
         using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 < real (- floor_fl x)`]
-        unfolding less_eq_float_def real_of_float_zero .
+        unfolding less_eq_float_def zero_float.rep_eq .
 
       have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
       also have "\<dots> = exp (x / ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
@@ -1562,7 +1563,7 @@
           exp (float_divl prec x (- floor_fl x)) ^ ?num"
           using `0 \<le> real ?horner`[unfolded floor_fl_def[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
         also have "\<dots> \<le> exp (x / ?num) ^ ?num" unfolding num_eq fl_eq
-          using float_divl by (auto intro!: power_mono simp del: real_of_float_uminus)
+          using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
         also have "\<dots> = exp (?num * (x / ?num))" unfolding exp_real_of_nat_mult ..
         also have "\<dots> = exp x" using `real ?num \<noteq> 0` by auto
         finally show ?thesis
@@ -1571,7 +1572,7 @@
         case True
         have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
         from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
-        have "- 1 \<le> x / (- floor_fl x)" unfolding real_of_float_minus by auto
+        have "- 1 \<le> x / (- floor_fl x)" unfolding minus_float.rep_eq by auto
         from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
         have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
         hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
@@ -1597,7 +1598,7 @@
     have "lb_exp prec x \<le> exp x"
     proof -
       from exp_boundaries'[OF `-x \<le> 0`]
-      have ub_exp: "exp (- real x) \<le> ub_exp prec (-x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
+      have ub_exp: "exp (- real x) \<le> ub_exp prec (-x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
 
       have "float_divl prec 1 (ub_exp prec (-x)) \<le> 1 / ub_exp prec (-x)" using float_divl[where x=1] by auto
       also have "\<dots> \<le> exp x"
@@ -1611,7 +1612,7 @@
       have "\<not> 0 < -x" using `0 < x` by auto
 
       from exp_boundaries'[OF `-x \<le> 0`]
-      have lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff real_of_float_minus by auto
+      have lb_exp: "lb_exp prec (-x) \<le> exp (- real x)" unfolding atLeastAtMost_iff minus_float.rep_eq by auto
 
       have "exp x \<le> (1 :: float) / lb_exp prec (-x)"
         using lb_exp lb_exp_pos[OF `\<not> 0 < -x`, of prec]
@@ -1686,7 +1687,7 @@
 
   let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
 
-  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_times setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
+  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
     using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
       OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
     by (rule mult_right_mono)
@@ -1694,7 +1695,7 @@
   finally show "?lb \<le> ?ln" .
 
   have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
-  also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_times setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
+  also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] times_float.rep_eq setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
     using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
       OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
     by (rule mult_right_mono)
@@ -1743,14 +1744,14 @@
   have uthird_gt0: "0 < real ?uthird + 1" using ub3_lb by auto
   have lthird_gt0: "0 < real ?lthird + 1" using lb3_lb by auto
 
-  show ?ub_ln2 unfolding ub_ln2_def Let_def real_of_float_plus ln2_sum Float_num(4)[symmetric]
+  show ?ub_ln2 unfolding ub_ln2_def Let_def plus_float.rep_eq ln2_sum Float_num(4)[symmetric]
   proof (rule add_mono, fact ln_float_bounds(2)[OF lb2 ub2])
     have "ln (1 / 3 + 1) \<le> ln (real ?uthird + 1)" unfolding ln_le_cancel_iff[OF third_gt0 uthird_gt0] using ub3 by auto
     also have "\<dots> \<le> ?uthird * ub_ln_horner prec (get_odd prec) 1 ?uthird"
       using ln_float_bounds(2)[OF ub3_lb ub3_ub] .
     finally show "ln (1 / 3 + 1) \<le> ?uthird * ub_ln_horner prec (get_odd prec) 1 ?uthird" .
   qed
-  show ?lb_ln2 unfolding lb_ln2_def Let_def real_of_float_plus ln2_sum Float_num(4)[symmetric]
+  show ?lb_ln2 unfolding lb_ln2_def Let_def plus_float.rep_eq ln2_sum Float_num(4)[symmetric]
   proof (rule add_mono, fact ln_float_bounds(1)[OF lb2 ub2])
     have "?lthird * lb_ln_horner prec (get_even prec) 1 ?lthird \<le> ln (real ?lthird + 1)"
       using ln_float_bounds(1)[OF lb3_lb lb3_ub] .
@@ -1993,7 +1994,7 @@
 
     {
       have "lb_ln2 prec * ?s \<le> ln 2 * (e + (bitlen m - 1))" (is "?lb2 \<le> _")
-        unfolding nat_0 power_0 mult_1_right real_of_float_times
+        unfolding nat_0 power_0 mult_1_right times_float.rep_eq
         using lb_ln2[of prec]
       proof (rule mult_mono)
         from float_gt1_scale[OF `1 \<le> Float m e`]
@@ -2011,7 +2012,7 @@
       have "ln ?x \<le> (?x - 1) * ub_ln_horner prec (get_odd prec) 1 (?x - 1)" (is "_ \<le> ?ub_horner") by auto
       moreover
       have "ln 2 * (e + (bitlen m - 1)) \<le> ub_ln2 prec * ?s" (is "_ \<le> ?ub2")
-        unfolding nat_0 power_0 mult_1_right real_of_float_times
+        unfolding nat_0 power_0 mult_1_right times_float.rep_eq
         using ub_ln2[of prec]
       proof (rule mult_mono)
         from float_gt1_scale[OF `1 \<le> Float m e`]
@@ -2025,7 +2026,7 @@
     }
     ultimately show ?thesis unfolding lb_ln.simps unfolding ub_ln.simps
       unfolding if_not_P[OF `\<not> x \<le> 0`] if_not_P[OF `\<not> x < 1`] if_not_P[OF False] if_not_P[OF `\<not> x \<le> Float 3 -1`] Let_def
-      unfolding real_of_float_plus e_def[symmetric] m_def[symmetric] by simp
+      unfolding plus_float.rep_eq e_def[symmetric] m_def[symmetric] by simp
   qed
 qed
 
@@ -2049,7 +2050,7 @@
     have "ln ?divl \<le> ln (1 / x)" unfolding ln_le_cancel_iff[OF B A] using float_divl[of _ 1 x] by auto
     hence "ln x \<le> - ln ?divl" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
     from this ub_ln_lb_ln_bounds'[OF A', THEN conjunct1, THEN le_imp_neg_le]
-    have "?ln \<le> - the (lb_ln prec ?divl)" unfolding real_of_float_uminus by (rule order_trans)
+    have "?ln \<le> - the (lb_ln prec ?divl)" unfolding uminus_float.rep_eq by (rule order_trans)
   } moreover
   {
     let ?divr = "float_divr prec 1 x"
@@ -2059,7 +2060,7 @@
     have "ln (1 / x) \<le> ln ?divr" unfolding ln_le_cancel_iff[OF A B] using float_divr[of 1 x] by auto
     hence "- ln ?divr \<le> ln x" unfolding nonzero_inverse_eq_divide[OF `real x \<noteq> 0`, symmetric] ln_inverse[OF `0 < real x`] by auto
     from ub_ln_lb_ln_bounds'[OF A', THEN conjunct2, THEN le_imp_neg_le] this
-    have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding real_of_float_uminus by (rule order_trans)
+    have "- the (ub_ln prec ?divr) \<le> ?ln" unfolding uminus_float.rep_eq by (rule order_trans)
   }
   ultimately show ?thesis unfolding lb_ln.simps[where x=x]  ub_ln.simps[where x=x]
     unfolding if_not_P[OF `\<not> x \<le> 0`] if_P[OF True] by auto
@@ -2447,7 +2448,7 @@
   from lift_un'[OF Minus.prems[unfolded approx.simps]] Minus.hyps
   obtain l1 u1 where "l = -u1" and "u = -l1"
     "l1 \<le> interpret_floatarith a xs" and "interpret_floatarith a xs \<le> u1" unfolding fst_conv snd_conv by blast
-  thus ?case unfolding interpret_floatarith.simps using real_of_float_minus by auto
+  thus ?case unfolding interpret_floatarith.simps using minus_float.rep_eq by auto
 next
   case (Mult a b)
   from lift_bin'[OF Mult.prems[unfolded approx.simps]] Mult.hyps
diff -r e12289b5796b -r 050718fe6eee src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Apr 18 14:29:22 2012 +0200
+++ b/src/HOL/Library/Float.thy	Thu Apr 19 11:55:30 2012 +0200
@@ -8,13 +8,16 @@
   morphisms real_of_float float_of
   by auto
 
-setup_lifting type_definition_float
+defs (overloaded)
+  real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
+
+lemma type_definition_float': "type_definition real float_of float"
+  using type_definition_float unfolding real_of_float_def .
+
+setup_lifting (no_code) type_definition_float'
 
 lemmas float_of_inject[simp]
 
-defs (overloaded)
-  real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
-
 declare [[coercion "real :: float \<Rightarrow> real"]]
 
 lemma real_of_float_eq:
@@ -27,10 +30,6 @@
 lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x"
   unfolding real_of_float_def by (rule float_of_inverse)
 
-lemma transfer_real_of_float [transfer_rule]:
-  "(fun_rel cr_float op =) (\<lambda>x. x) real"
-  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def)
-
 subsection {* Real operations preserving the representation as floating point number *}
 
 lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
@@ -124,6 +123,9 @@
 qed
 
 lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
+declare Float.rep_eq[simp]
+
+code_datatype Float
 
 subsection {* Arithmetic operations on floating point numbers *}
 
@@ -131,41 +133,34 @@
 begin
 
 lift_definition zero_float :: float is 0 by simp
+declare zero_float.rep_eq[simp]
 lift_definition one_float :: float is 1 by simp
+declare one_float.rep_eq[simp]
 lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp
+declare plus_float.rep_eq[simp]
 lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp
+declare times_float.rep_eq[simp]
 lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp
+declare minus_float.rep_eq[simp]
 lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp
+declare uminus_float.rep_eq[simp]
 
 lift_definition abs_float :: "float \<Rightarrow> float" is abs by simp
+declare abs_float.rep_eq[simp]
 lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp
+declare sgn_float.rep_eq[simp]
 
 lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" ..
 
 lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" ..
+declare less_eq_float.rep_eq[simp]
 lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" ..
+declare less_float.rep_eq[simp]
 
 instance
   proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
 end
 
-lemma
-  fixes x y :: float
-  shows real_of_float_uminus[simp]: "real (- x) = - real x"
-    and real_of_float_plus[simp]: "real (y + x) = real y + real x"
-    and real_of_float_minus[simp]: "real (y - x) = real y - real x"
-    and real_of_float_times[simp]: "real (y * x) = real y * real x"
-    and real_of_float_zero[simp]: "real (0::float) = 0"
-    and real_of_float_one[simp]: "real (1::float) = 1"
-    and real_of_float_le[simp]: "x \<le> y \<longleftrightarrow> real x \<le> real y"
-    and real_of_float_less[simp]: "x < y \<longleftrightarrow> real x < real y"
-    and real_of_float_abs[simp]: "real (abs x) = abs (real x)"
-    and real_of_float_sgn[simp]: "real (sgn x) = sgn (real x)"
-  using uminus_float.rep_eq plus_float.rep_eq minus_float.rep_eq times_float.rep_eq
-    zero_float.rep_eq one_float.rep_eq less_eq_float.rep_eq less_float.rep_eq
-    abs_float.rep_eq sgn_float.rep_eq
-  by (simp_all add: real_of_float_def)
-
 lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
   by (induct n) simp_all
 
@@ -213,7 +208,7 @@
   apply (induct x)
   apply simp
   apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq real_float
-                  real_of_float_plus real_of_float_one plus_float numeral_float one_float)
+                  plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float)
   done
 
 lemma transfer_numeral [transfer_rule]: 
@@ -366,12 +361,9 @@
 
 subsection {* Compute arithmetic operations *}
 
-lemma real_Float[simp]: "real (Float m e) = m * 2 powr e"
-  using Float.rep_eq by (simp add: real_of_float_def)
-
 lemma real_of_float_Float[code]: "real_of_float (Float m e) =
   (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
-by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric] Float_def)
+by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric])
 
 lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
   unfolding real_of_float_eq mantissa_exponent[of f] by simp
@@ -537,9 +529,7 @@
 subsection {* Rounding Floats *}
 
 lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
-
-lemma real_of_float_float_up[simp]: "real (float_up e f) = round_up e (real f)"
-  using float_up.rep_eq by (simp add: real_of_float_def)
+declare float_up.rep_eq[simp]
 
 lemma float_up_correct:
   shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
@@ -552,9 +542,7 @@
 qed (simp add: algebra_simps round_up)
 
 lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
-
-lemma real_of_float_float_down[simp]: "real (float_down e f) = round_down e (real f)"
-  using float_down.rep_eq by (simp add: real_of_float_def)
+declare float_down.rep_eq[simp]
 
 lemma float_down_correct:
   shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
@@ -929,7 +917,8 @@
   ultimately show ?thesis using assms by simp
 qed
 
-lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
+lemma rapprox_posrat_less1:
+  assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   shows "real (rapprox_posrat n x y) < 1"
 proof -
   have powr1: "2 powr real (rat_precision n (int x) (int y)) = 
@@ -947,14 +936,10 @@
     unfolding int_of_reals real_of_int_le_iff
     using rat_precision_pos[OF assms] by (rule power_aux)
   finally show ?thesis
-    unfolding rapprox_posrat_def
-    apply (simp add: round_up_def)
-    apply (simp add: field_simps powr_minus inverse_eq_divide)
-    unfolding powr1
+    apply (transfer fixing: n x y)
+    apply (simp add: round_up_def field_simps powr_minus inverse_eq_divide powr1)
     unfolding int_of_reals real_of_int_less_iff
-    unfolding ceiling_less_eq
-    using rat_precision_pos[of x y n] assms
-    apply simp
+    apply (simp add: ceiling_less_eq)
     done
 qed
 
@@ -970,12 +955,7 @@
       else (if 0 < y
         then - (rapprox_posrat prec (nat (-x)) (nat y))
         else lapprox_posrat prec (nat (-x)) (nat (-y))))"
-  apply transfer
-  apply (cases "y = 0")
-  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
-                    int_of_reals simp del: real_of_ints)
-  apply (auto simp: ac_simps)
-  done
+  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
 
 lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
   "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
@@ -989,12 +969,7 @@
       else (if 0 < y
         then - (lapprox_posrat prec (nat (-x)) (nat y))
         else rapprox_posrat prec (nat (-x)) (nat (-y))))"
-  apply transfer
-  apply (cases "y = 0")
-  apply (auto simp: round_up_def round_down_def ceiling_def real_of_float_uminus[symmetric] ac_simps
-                    int_of_reals simp del: real_of_ints)
-  apply (auto simp: ac_simps)
-  done
+  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
 
 subsection {* Division *}
 
@@ -1004,23 +979,17 @@
 lemma compute_float_divl[code]:
   "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
 proof cases
-  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
-  then show ?thesis
-  proof transfer
-    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
-    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
-    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
+  let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
+  let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
+  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+  then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
+    by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
+  have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
+    by (simp add: field_simps powr_divide2[symmetric])
 
-    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
-      by (simp add: field_simps powr_divide2[symmetric])
-    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
-        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
-      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
-    
-    show "round_down (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
-      round_down (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
-      using not_0 unfolding eq1 eq2 round_down_shift by (simp add: field_simps)
-  qed
+  show ?thesis
+    using not_0 
+    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
 qed (transfer, auto)
 
 lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
@@ -1029,23 +998,17 @@
 lemma compute_float_divr[code]:
   "float_divr prec (Float m1 s1) (Float m2 s2) = rapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
 proof cases
-  assume "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
-  then show ?thesis
-  proof transfer
-    fix prec :: nat and m1 s1 m2 s2 :: int assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
-    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
-    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
+  let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
+  let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
+  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
+  then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
+    by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
+  have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
+    by (simp add: field_simps powr_divide2[symmetric])
 
-    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
-      by (simp add: field_simps powr_divide2[symmetric])
-    have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
-        rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
-      using not_0 by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
-    
-    show "round_up (int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) (?f1 / ?f2) =
-      round_up (rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar>) ?m * (real (1::int) * ?s)"
-      using not_0 unfolding eq1 eq2 round_up_shift by (simp add: field_simps)
-  qed
+  show ?thesis
+    using not_0 
+    by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
 qed (transfer, auto)
 
 subsection {* Lemmas needed by Approximate *}
@@ -1242,12 +1205,9 @@
   "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
     if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
              else Float m e)"
+  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   unfolding Let_def
-  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
-  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
-  apply (cases "m = 0")
-  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
-  done
+  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
 
 lemma compute_float_round_up[code]:
   "float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
@@ -1256,10 +1216,7 @@
               else Float m e)"
   using compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   unfolding Let_def
-  apply (simp add: field_simps split del: split_if cong del: if_weak_cong)
-  apply (cases "m = 0")
-  apply (transfer, auto simp add: field_simps abs_mult log_mult bitlen_def)+
-  done
+  by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
 
 lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
  apply (auto simp: zero_float_def mult_le_0_iff)
@@ -1282,15 +1239,13 @@
 lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
 
 lemma compute_int_floor_fl[code]:
-  shows "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e
-                                  else m div (2 ^ (nat (-e))))"
+  "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
   by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
 
 lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
 
 lemma compute_floor_fl[code]:
-  shows "floor_fl (Float m e) = (if 0 \<le> e then Float m e
-                                  else Float (m div (2 ^ (nat (-e)))) 0)"
+  "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
 
 lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
@@ -1305,7 +1260,5 @@
   thus ?thesis by simp
 qed (simp add: floor_fl_def)
 
-code_datatype Float
-
 end