# HG changeset patch
# User nipkow
# Date 1470982817 -7200
# Node ID 28d1deca302e9204b2d2979424fc839bbff237f3
# Parent  5cdcd51a4dadf1c21abfece124bf07cf84efcaf6
Extracted floorlog and bitlen to separate theory Log_Nat

diff -r 5cdcd51a4dad -r 28d1deca302e src/HOL/Data_Structures/Balance_List.thy
--- a/src/HOL/Data_Structures/Balance_List.thy	Wed Aug 10 18:57:20 2016 +0200
+++ b/src/HOL/Data_Structures/Balance_List.thy	Fri Aug 12 08:20:17 2016 +0200
@@ -5,7 +5,7 @@
 theory Balance_List
 imports
   "~~/src/HOL/Library/Tree"
-  "~~/src/HOL/Library/Float"
+  "~~/src/HOL/Library/Log_Nat"
 begin
 
 fun bal :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree * 'a list" where
@@ -73,7 +73,7 @@
     hence le: "?log2 \<le> ?log1" by(simp add:floorlog_mono)
     have "height t = max ?log1 ?log2 + 1" by (simp add: t IH1 IH2)
     also have "\<dots> = ?log1 + 1" using le by (simp add: max_absorb1)
-    also have "\<dots> = floorlog 2 n" by (simp add: Float.compute_floorlog)
+    also have "\<dots> = floorlog 2 n" by (simp add: compute_floorlog)
     finally show ?thesis .
   qed
 qed
@@ -106,7 +106,7 @@
     also have "\<dots> = floorlog 2 (n - n div 2)" by(simp add: floorlog_def)
     also have "n - n div 2 = (n+1) div 2" by arith
     also have "floorlog 2 \<dots> = floorlog 2 (n+1) - 1"
-      by (simp add: Float.compute_floorlog)
+      by (simp add: compute_floorlog)
     finally show ?thesis .
   qed
 qed
diff -r 5cdcd51a4dad -r 28d1deca302e src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Aug 10 18:57:20 2016 +0200
+++ b/src/HOL/Library/Float.thy	Fri Aug 12 08:20:17 2016 +0200
@@ -6,7 +6,7 @@
 section \<open>Floating-Point Numbers\<close>
 
 theory Float
-imports Complex_Main Lattice_Algebras
+imports Log_Nat Lattice_Algebras
 begin
 
 definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
@@ -878,193 +878,6 @@
 
 end
 
-definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  where "floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)"
-
-lemma floorlog_mono: "x \<le> y \<Longrightarrow> floorlog b x \<le> floorlog b y"
-by(auto simp: floorlog_def floor_mono nat_mono)
-
-lemma floorlog_bounds:
-  assumes "x > 0" "b > 1"
-  shows "b ^ (floorlog b x - 1) \<le> x \<and> x < b ^ (floorlog b x)"
-proof
-  show "b ^ (floorlog b x - 1) \<le> x"
-  proof -
-    have "(b::real) ^ nat \<lfloor>log b (real_of_int x)\<rfloor> = b powr real_of_int \<lfloor>log b (real_of_int x)\<rfloor>"
-      using powr_realpow[symmetric, of b "nat \<lfloor>log b (real_of_int x)\<rfloor>"] \<open>x > 0\<close> \<open>b > 1\<close>
-      by simp
-    also have "\<dots> \<le> b powr log b (real_of_int x)"
-      using \<open>b > 1\<close>
-      by simp
-    also have "\<dots> = real_of_int x"
-      using \<open>0 < x\<close> \<open>b > 1\<close> by simp
-    finally have "b ^ nat \<lfloor>log b (real_of_int x)\<rfloor> \<le> real_of_int x"
-      by simp
-    then show ?thesis
-      using \<open>0 < x\<close> \<open>b > 1\<close> of_nat_le_iff
-      by (fastforce simp add: floorlog_def)
-  qed
-  show "x < b ^ (floorlog b x)"
-  proof -
-    have "x \<le> b powr (log b x)"
-      using \<open>x > 0\<close> \<open>b > 1\<close> by simp
-    also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
-      using assms
-      by (intro powr_less_mono) auto
-    also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
-      using assms
-      by (simp add: powr_realpow[symmetric])
-    finally
-    have "x < b ^ nat (\<lfloor>log (real b) (real_of_int (int x))\<rfloor> + 1)"
-      by (rule of_nat_less_imp_less)
-    then show ?thesis
-      using \<open>x > 0\<close> \<open>b > 1\<close>
-      by (simp add: floorlog_def nat_add_distrib)
-  qed
-qed
-
-lemma floorlog_power[simp]:
-  assumes "a > 0" "b > 1"
-  shows "floorlog b (a * b ^ c) = floorlog b a + c"
-proof -
-  have "\<lfloor>log (real b) (real a) + real c\<rfloor> = \<lfloor>log (real b) (real a)\<rfloor> + c"
-    by arith
-  then show ?thesis using assms
-    by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
-qed
-
-lemma floor_log_add_eqI:
-  fixes a::nat and b::nat and r::real
-  assumes "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1"
-  shows "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>"
-proof (rule floor_eq2)
-  have "log (real b) (real a) \<le> log (real b) (real a + r)"
-    using assms by force
-  then show "\<lfloor>log (real b) (real a)\<rfloor> \<le> log (real b) (real a + r)"
-    by arith
-next
-  define l::int where "l = int b ^ (nat \<lfloor>log b a\<rfloor> + 1)"
-  have l_def_real: "l = b powr (\<lfloor>log b a\<rfloor> + 1)"
-    using assms by (simp add: l_def powr_add powr_real_of_int)
-  have "a < l"
-  proof -
-    have "a = b powr (log b a)" using assms by simp
-    also have "\<dots> < b powr floor ((log b a) + 1)"
-      using assms(1) by auto
-    also have "\<dots> = l"
-      using assms
-      by (simp add: l_def powr_real_of_int powr_add)
-    finally show ?thesis by simp
-  qed
-  then have "a + r < l" using assms by simp
-  then have "log b (a + r) < log b l"
-    using assms by simp
-  also have "\<dots> = real_of_int \<lfloor>log b a\<rfloor> + 1"
-    using assms by (simp add: l_def_real)
-  finally show "log b (a + r) < real_of_int \<lfloor>log b a\<rfloor> + 1" .
-qed
-
-lemma divide_nat_diff_div_nat_less_one:
-  fixes x b::nat shows "x / b - x div b < 1"
-proof -
-  have "int 0 \<noteq> \<lfloor>1::real\<rfloor>" by simp
-  thus ?thesis
-    by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def
-        mod_div_trivial real_of_nat_div3 real_of_nat_div_aux)
-qed
-
-lemma floor_log_div:
-  fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0"
-  shows "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1"
-proof-
-  have "\<lfloor>log (real b) (real x)\<rfloor> = \<lfloor>log (real b) (x / b * b)\<rfloor>"
-    using assms by simp
-  also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>"
-    using assms by (subst log_mult) auto
-  also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using assms by simp
-  also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>"
-    by simp
-  also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>"
-    using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one
-    by (intro floor_log_add_eqI) auto
-  finally show ?thesis .
-qed
-
-lemma compute_floorlog[code]:
-  "floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)"
-by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
-    intro!: floor_eq2)
-
-lemma floor_log_eq_if:
-  fixes b x y :: nat
-  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
-  shows "floor(log b x) = floor(log b y)"
-proof -
-  have "y > 0" using assms by(auto intro: ccontr)
-  thus ?thesis using assms by (simp add: floor_log_div)
-qed
-
-lemma floorlog_eq_if:
-  fixes b x y :: nat
-  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
-  shows "floorlog b x = floorlog b y"
-proof -
-  have "y > 0" using assms by(auto intro: ccontr)
-  thus ?thesis using assms
-    by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
-qed
-
-
-definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)"
-
-lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
-  by (simp add: bitlen_def floorlog_def)
-
-lemma bitlen_nonneg: "0 \<le> bitlen x"
-by (simp add: bitlen_def)
-
-lemma bitlen_bounds:
-  assumes "x > 0"
-  shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)"
-proof -
-  from assms have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def)
-  with assms floorlog_bounds[of "nat x" 2] show ?thesis
-    by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib)
-qed
-
-lemma bitlen_pow2[simp]:
-  assumes "b > 0"
-  shows "bitlen (b * 2 ^ c) = bitlen b + c"
-  using assms
-  by (simp add: bitlen_def nat_mult_distrib nat_power_eq)
-
-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
-
-context
-begin
-
-qualified lemma compute_bitlen[code]: "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
-  unfolding bitlen_def
-  by (subst Float.compute_floorlog) (simp add: nat_div_distrib)
-
-end
 
 lemma float_gt1_scale:
   assumes "1 \<le> Float m e"
@@ -1653,7 +1466,7 @@
 
 lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0"
   by (auto simp add: bitlen_alt_def)
-    (metis Float.compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
+    (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
       not_less zero_less_one)
 
 lemma sum_neq_zeroI:
diff -r 5cdcd51a4dad -r 28d1deca302e src/HOL/Library/Log_Nat.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Log_Nat.thy	Fri Aug 12 08:20:17 2016 +0200
@@ -0,0 +1,161 @@
+(*  Title:      HOL/Library/Log_Nat.thy
+    Author:     Johannes Hölzl, Fabian Immler
+    Copyright   2012  TU München
+*)
+
+section \<open>Logarithm of Natural Numbers\<close>
+
+theory Log_Nat
+imports Complex_Main
+begin
+
+definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)"
+
+lemma floorlog_mono: "x \<le> y \<Longrightarrow> floorlog b x \<le> floorlog b y"
+by(auto simp: floorlog_def floor_mono nat_mono)
+
+lemma floorlog_bounds:
+  assumes "x > 0" "b > 1"
+  shows "b ^ (floorlog b x - 1) \<le> x \<and> x < b ^ (floorlog b x)"
+proof
+  show "b ^ (floorlog b x - 1) \<le> x"
+  proof -
+    have "b ^ nat \<lfloor>log b x\<rfloor> = b powr \<lfloor>log b x\<rfloor>"
+      using powr_realpow[symmetric, of b "nat \<lfloor>log b x\<rfloor>"] \<open>x > 0\<close> \<open>b > 1\<close>
+      by simp
+    also have "\<dots> \<le> b powr log b x" using \<open>b > 1\<close> by simp
+    also have "\<dots> = real_of_int x" using \<open>0 < x\<close> \<open>b > 1\<close> by simp
+    finally have "b ^ nat \<lfloor>log b x\<rfloor> \<le> real_of_int x" by simp
+    then show ?thesis
+      using \<open>0 < x\<close> \<open>b > 1\<close> of_nat_le_iff
+      by (fastforce simp add: floorlog_def)
+  qed
+  show "x < b ^ (floorlog b x)"
+  proof -
+    have "x \<le> b powr (log b x)" using \<open>x > 0\<close> \<open>b > 1\<close> by simp
+    also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
+      using assms by (intro powr_less_mono) auto
+    also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
+      using assms by (simp add: powr_realpow[symmetric])
+    finally
+    have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)"
+      by (rule of_nat_less_imp_less)
+    then show ?thesis
+      using \<open>x > 0\<close> \<open>b > 1\<close> by (simp add: floorlog_def nat_add_distrib)
+  qed
+qed
+
+lemma floorlog_power[simp]:
+  assumes "a > 0" "b > 1"
+  shows "floorlog b (a * b ^ c) = floorlog b a + c"
+proof -
+  have "\<lfloor>log b a + real c\<rfloor> = \<lfloor>log b a\<rfloor> + c" by arith
+  then show ?thesis using assms
+    by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
+qed
+
+lemma floor_log_add_eqI:
+  fixes a::nat and b::nat and r::real
+  assumes "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1"
+  shows "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>"
+proof (rule floor_eq2)
+  have "log b a \<le> log b (a + r)" using assms by force
+  then show "\<lfloor>log b a\<rfloor> \<le> log b (a + r)" by arith
+next
+  define l::int where "l = int b ^ (nat \<lfloor>log b a\<rfloor> + 1)"
+  have l_def_real: "l = b powr (\<lfloor>log b a\<rfloor> + 1)"
+    using assms by (simp add: l_def powr_add powr_real_of_int)
+  have "a < l"
+  proof -
+    have "a = b powr (log b a)" using assms by simp
+    also have "\<dots> < b powr floor ((log b a) + 1)"
+      using assms(1) by auto
+    also have "\<dots> = l"
+      using assms by (simp add: l_def powr_real_of_int powr_add)
+    finally show ?thesis by simp
+  qed
+  then have "a + r < l" using assms by simp
+  then have "log b (a + r) < log b l" using assms by simp
+  also have "\<dots> = real_of_int \<lfloor>log b a\<rfloor> + 1"
+    using assms by (simp add: l_def_real)
+  finally show "log b (a + r) < real_of_int \<lfloor>log b a\<rfloor> + 1" .
+qed
+
+lemma divide_nat_diff_div_nat_less_one:
+  fixes x b::nat shows "x / b - x div b < 1"
+proof -
+  have "int 0 \<noteq> \<lfloor>1::real\<rfloor>" by simp
+  thus ?thesis
+    by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def
+        mod_div_trivial real_of_nat_div3 real_of_nat_div_aux)
+qed
+
+lemma floor_log_div:
+  fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0"
+  shows "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1"
+proof-
+  have "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x / b * b)\<rfloor>" using assms by simp
+  also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>"
+    using assms by (subst log_mult) auto
+  also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using assms by simp
+  also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>" by simp
+  also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>"
+    using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one
+    by (intro floor_log_add_eqI) auto
+  finally show ?thesis .
+qed
+
+lemma compute_floorlog[code]:
+  "floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)"
+by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
+    intro!: floor_eq2)
+
+lemma floor_log_eq_if:
+  fixes b x y :: nat
+  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
+  shows "floor(log b x) = floor(log b y)"
+proof -
+  have "y > 0" using assms by(auto intro: ccontr)
+  thus ?thesis using assms by (simp add: floor_log_div)
+qed
+
+lemma floorlog_eq_if:
+  fixes b x y :: nat
+  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
+  shows "floorlog b x = floorlog b y"
+proof -
+  have "y > 0" using assms by(auto intro: ccontr)
+  thus ?thesis using assms
+    by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
+qed
+
+
+definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)"
+
+lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
+by (simp add: bitlen_def floorlog_def)
+
+lemma bitlen_nonneg: "0 \<le> bitlen x"
+by (simp add: bitlen_def)
+
+lemma bitlen_bounds:
+  assumes "x > 0"
+  shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)"
+proof -
+  from assms have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def)
+  with assms floorlog_bounds[of "nat x" 2] show ?thesis
+    by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib)
+qed
+
+lemma bitlen_pow2[simp]:
+  assumes "b > 0"
+  shows "bitlen (b * 2 ^ c) = bitlen b + c"
+  using assms
+  by (simp add: bitlen_def nat_mult_distrib nat_power_eq)
+
+lemma compute_bitlen[code]:
+  "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
+by (simp add: bitlen_def nat_div_distrib compute_floorlog)
+
+end