diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Library/Float.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -41,18 +41,6 @@
 instance ..
 end
 
-instantiation float :: number
-begin
-definition number_of_float where "number_of n = Float n 0"
-instance ..
-end
-
-lemma number_of_float_Float:
-  "number_of k = Float (number_of k) 0"
-  by (simp add: number_of_float_def number_of_is_id)
-
-declare number_of_float_Float [symmetric, code_abbrev]
-
 lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
   unfolding real_of_float_def using of_float.simps .
 
@@ -63,12 +51,9 @@
 lemma Float_num[simp]: shows
    "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
    "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
-   "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
+   "real (Float -1 0) = -1" and "real (Float (numeral n) 0) = numeral n"
   by auto
 
-lemma float_number_of[simp]: "real (number_of x :: float) = number_of x"
-  by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
-
 lemma float_number_of_int[simp]: "real (Float n 0) = real n"
   by simp
 
@@ -349,6 +334,21 @@
     by (cases a, cases b) (simp add: plus_float.simps)
 qed
 
+instance float :: numeral ..
+
+lemma Float_add_same_scale: "Float x e + Float y e = Float (x + y) e"
+  by (simp add: plus_float.simps)
+
+(* FIXME: define other constant for code_unfold_post *)
+lemma numeral_float_Float (*[code_unfold_post]*):
+  "numeral k = Float (numeral k) 0"
+  by (induct k, simp_all only: numeral.simps one_float_def
+    Float_add_same_scale)
+
+lemma float_number_of[simp]: "real (numeral x :: float) = numeral x"
+  by (simp only: numeral_float_Float Float_num)
+
+
 instance float :: comm_monoid_mult
 proof (intro_classes)
   fix a b c :: float
@@ -555,6 +555,7 @@
   show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto
 qed
 
+(* BROKEN
 lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
 
 lemma bitlen_Min: "bitlen (Int.Min) = Int.Bit1 Int.Pls" by (subst Min_def, simp add: Bit1_def) 
@@ -588,6 +589,7 @@
 
 lemma bitlen_number_of: "bitlen (number_of w) = number_of (bitlen w)"
   by (simp add: number_of_is_id)
+BH *)
 
 lemma [code]: "bitlen x = 
      (if x = 0  then 0 
@@ -722,12 +724,12 @@
     hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
 
     from real_of_int_div4[of "?X" y]
-    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
+    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_numeral .
     also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto)
     finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
     hence "?X div y + 1 \<le> 2^?l" by auto
     hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)"
-      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
+      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_numeral
       by (rule mult_right_mono, auto)
     hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
@@ -796,12 +798,12 @@
     qed
 
     from real_of_int_div4[of "?X" y]
-    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
+    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_numeral .
     also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto)
     finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
     hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto
     hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)"
-      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
+      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_numeral
       by (rule mult_strict_right_mono, auto)
     hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
     thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
@@ -1195,7 +1197,7 @@
     case True
     have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
     proof -
-      have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_number_of unfolding pow2_int[symmetric] 
+      have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_numeral unfolding pow2_int[symmetric] 
         using `?l > 0` by auto
       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
       also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
@@ -1262,7 +1264,7 @@
     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
     have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
     also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
-    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
+    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_numeral divide_inverse ..
     also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
     finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
   next
@@ -1290,7 +1292,7 @@
     case False
     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
     have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
-    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
+    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_numeral divide_inverse ..
     also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
     also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
     finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .