tuned

--- a/src/HOL/Library/Float.thy	Fri Aug 12 08:20:17 2016 +0200
+++ b/src/HOL/Library/Float.thy	Fri Aug 12 09:57:09 2016 +0200
@@ -879,6 +879,25 @@
 end
 
 
+lemma bitlen_Float:
+  fixes m e
+  defines "f \<equiv> Float m e"
+  shows "bitlen \<bar>mantissa f\<bar> + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
+proof (cases "m = 0")
+  case True
+  then show ?thesis by (simp add: f_def bitlen_alt_def Float_def)
+next
+  case False
+  then have "f \<noteq> float_of 0"
+    unfolding real_of_float_eq by (simp add: f_def)
+  then have "mantissa f \<noteq> 0"
+    by (simp add: mantissa_noteq_0)
+  moreover
+  obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
+    by (rule f_def[THEN denormalize_shift, OF \<open>f \<noteq> float_of 0\<close>])
+  ultimately show ?thesis by (simp add: abs_mult)
+qed
+
 lemma float_gt1_scale:
   assumes "1 \<le> Float m e"
   shows "0 \<le> e + (bitlen m - 1)"
@@ -922,38 +941,6 @@
   qed
 qed
 
-lemma bitlen_div:
-  assumes "0 < m"
-  shows "1 \<le> real_of_int m / 2^nat (bitlen m - 1)"
-    and "real_of_int m / 2^nat (bitlen m - 1) < 2"
-proof -
-  let ?B = "2^nat (bitlen m - 1)"
-
-  have "?B \<le> m" using bitlen_bounds[OF \<open>0 <m\<close>] ..
-  then have "1 * ?B \<le> real_of_int m"
-    unfolding of_int_le_iff[symmetric] by auto
-  then show "1 \<le> real_of_int m / ?B"
-    by auto
-
-  from assms have "m \<noteq> 0"
-    by auto
-  from assms have "0 \<le> bitlen m - 1"
-    by (auto simp: bitlen_alt_def)
-
-  have "m < 2^nat(bitlen m)"
-    using bitlen_bounds[OF assms] ..
-  also from assms have "\<dots> = 2^nat(bitlen m - 1 + 1)"
-    by (auto simp: bitlen_def)
-  also have "\<dots> = ?B * 2"
-    unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
-  finally have "real_of_int m < 2 * ?B"
-    by (metis (full_types) mult.commute power.simps(2) real_of_int_less_numeral_power_cancel_iff)
-  then have "real_of_int m / ?B < 2 * ?B / ?B"
-    by (rule divide_strict_right_mono) auto
-  then show "real_of_int m / ?B < 2"
-    by auto
-qed
-
 
 subsection \<open>Truncating Real Numbers\<close>
 
@@ -1464,11 +1451,6 @@
   shows "truncate_down p x = truncate_down p y"
   using assms by (auto simp: truncate_down_def round_down_def)
 
-lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0"
-  by (auto simp add: bitlen_alt_def)
-    (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
-      not_less zero_less_one)
-
 lemma sum_neq_zeroI:
   "\<bar>a\<bar> \<ge> k \<Longrightarrow> \<bar>b\<bar> < k \<Longrightarrow> a + b \<noteq> 0"
   "\<bar>a\<bar> > k \<Longrightarrow> \<bar>b\<bar> \<le> k \<Longrightarrow> a + b \<noteq> 0"

--- a/src/HOL/Library/Log_Nat.thy	Fri Aug 12 08:20:17 2016 +0200
+++ b/src/HOL/Library/Log_Nat.thy	Fri Aug 12 09:57:09 2016 +0200
@@ -158,4 +158,36 @@
   "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
 by (simp add: bitlen_def nat_div_distrib compute_floorlog)
 
+lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0"
+by (auto simp add: bitlen_alt_def)
+   (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
+      not_less zero_less_one)
+
+lemma bitlen_div:
+  assumes "0 < m"
+  shows "1 \<le> real_of_int m / 2^nat (bitlen m - 1)"
+    and "real_of_int m / 2^nat (bitlen m - 1) < 2"
+proof -
+  let ?B = "2^nat (bitlen m - 1)"
+
+  have "?B \<le> m" using bitlen_bounds[OF \<open>0 <m\<close>] ..
+  then have "1 * ?B \<le> real_of_int m"
+    unfolding of_int_le_iff[symmetric] by auto
+  then show "1 \<le> real_of_int m / ?B" by auto
+
+  from assms have "m \<noteq> 0" by auto
+  from assms have "0 \<le> bitlen m - 1" by (auto simp: bitlen_alt_def)
+
+  have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] ..
+  also from assms have "\<dots> = 2^nat(bitlen m - 1 + 1)"
+    by (auto simp: bitlen_def)
+  also have "\<dots> = ?B * 2"
+    unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
+  finally have "real_of_int m < 2 * ?B"
+    by (metis (full_types) mult.commute power.simps(2) real_of_int_less_numeral_power_cancel_iff)
+  then have "real_of_int m / ?B < 2 * ?B / ?B"
+    by (rule divide_strict_right_mono) auto
+  then show "real_of_int m / ?B < 2" by auto
+qed
+
 end