# HG changeset patch
# User nipkow
# Date 1503763024 -7200
# Node ID 7c7977f6c4ceb459dce55793a7a0cc29965074e9
# Parent  70e3f446bfc7a2384c295f02b5ac1c4cdc0a6bfe# Parent  97c2d3846e10ac86fcb6deb22be9359fac2a57b8
merged

diff -r 70e3f446bfc7 -r 7c7977f6c4ce src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Sat Aug 26 12:56:17 2017 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Sat Aug 26 17:57:04 2017 +0200
@@ -2803,7 +2803,7 @@
     case 1
     let ?n = "of_int (floor (x/a)) + 1"
     have x: "x < ?n * a"
-      by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
+      by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
     have "?n * a \<le> a + x"
       apply (simp add: algebra_simps)
       by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
@@ -2816,7 +2816,7 @@
     case 2
     let ?n = "of_int (floor (y/a)) + 1"
     have y: "y < ?n * a"
-      by (meson \<open>0 < a\<close> divide_less_eq floor_unique_iff)
+      by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
     have "?n * a \<le> a + y"
       apply (simp add: algebra_simps)
       by (metis \<open>0 < a\<close> floor_correct less_irrefl nonzero_mult_div_cancel_left real_mult_le_cancel_iff2 times_divide_eq_right)
diff -r 70e3f446bfc7 -r 7c7977f6c4ce src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Sat Aug 26 12:56:17 2017 +0100
+++ b/src/HOL/Archimedean_Field.thy	Sat Aug 26 17:57:04 2017 +0200
@@ -224,9 +224,8 @@
 lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
   using floor_correct [of x] floor_exists1 [of x] by auto
 
-lemma floor_unique_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
-  for x :: "'a::floor_ceiling"
-  using floor_correct floor_unique by auto
+lemma floor_eq_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
+using floor_correct floor_unique by auto
 
 lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
   using floor_correct ..
@@ -467,6 +466,9 @@
 lemma ceiling_unique: "of_int z - 1 < x \<Longrightarrow> x \<le> of_int z \<Longrightarrow> \<lceil>x\<rceil> = z"
   unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
 
+lemma ceiling_eq_iff: "\<lceil>x\<rceil> = a \<longleftrightarrow> of_int a - 1 < x \<and> x \<le> of_int a"
+using ceiling_correct ceiling_unique by auto
+
 lemma le_of_int_ceiling [simp]: "x \<le> of_int \<lceil>x\<rceil>"
   using ceiling_correct ..
 
@@ -673,7 +675,7 @@
     by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
   moreover
   have "\<not> x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>) \<Longrightarrow> \<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
-    apply (simp add: floor_unique_iff)
+    apply (simp add: floor_eq_iff)
     apply (auto simp add: algebra_simps)
     apply linarith
     done
@@ -727,7 +729,7 @@
 qed
 
 lemma round_of_int [simp]: "round (of_int n) = n"
-  unfolding round_def by (subst floor_unique_iff) force
+  unfolding round_def by (subst floor_eq_iff) force
 
 lemma round_0 [simp]: "round 0 = 0"
   using round_of_int[of 0] by simp
diff -r 70e3f446bfc7 -r 7c7977f6c4ce src/HOL/Data_Structures/Balance.thy
--- a/src/HOL/Data_Structures/Balance.thy	Sat Aug 26 12:56:17 2017 +0100
+++ b/src/HOL/Data_Structures/Balance.thy	Sat Aug 26 17:57:04 2017 +0200
@@ -7,147 +7,6 @@
   "HOL-Library.Tree_Real"
 begin
 
-(* mv *)
-
-text \<open>The lemmas about \<open>floor\<close> and \<open>ceiling\<close> of \<open>log 2\<close> should be generalized
-from 2 to \<open>n\<close> and should be made executable. In the end they should be moved
-to theory \<open>Log_Nat\<close> and \<open>floorlog\<close> should be replaced.\<close>
-
-lemma floor_log_nat_ivl: fixes b n k :: nat
-assumes "b \<ge> 2" "b^n \<le> k" "k < b^(n+1)"
-shows "floor (log b (real k)) = int(n)"
-proof -
-  have "k \<ge> 1"
-    using assms(1,2) one_le_power[of b n] by linarith
-  show ?thesis
-  proof(rule floor_eq2)
-    show "int n \<le> log b k"
-      using assms(1,2) \<open>k \<ge> 1\<close>
-      by(simp add: powr_realpow le_log_iff of_nat_power[symmetric] del: of_nat_power)
-  next
-    have "real k < b powr (real(n + 1))" using assms(1,3)
-      by (simp only: powr_realpow) (metis of_nat_less_iff of_nat_power)
-    thus "log b k < real_of_int (int n) + 1"
-      using assms(1) \<open>k \<ge> 1\<close> by(simp add: log_less_iff add_ac)
-  qed
-qed
-
-lemma ceil_log_nat_ivl: fixes b n k :: nat
-assumes "b \<ge> 2" "b^n < k" "k \<le> b^(n+1)"
-shows "ceiling (log b (real k)) = int(n)+1"
-proof(rule ceiling_eq)
-  show "int n < log b k"
-    using assms(1,2)
-    by(simp add: powr_realpow less_log_iff of_nat_power[symmetric] del: of_nat_power)
-next
-  have "real k \<le> b powr (real(n + 1))"
-    using assms(1,3)
-    by (simp only: powr_realpow) (metis of_nat_le_iff of_nat_power)
-  thus "log b k \<le> real_of_int (int n) + 1"
-    using assms(1,2) by(simp add: log_le_iff add_ac)
-qed
-
-lemma ceil_log2_div2: assumes "n \<ge> 2"
-shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
-proof cases
-  assume "n=2"
-  thus ?thesis by simp
-next
-  let ?m = "(n-1) div 2 + 1"
-  assume "n\<noteq>2"
-  hence "2 \<le> ?m"
-    using assms by arith
-  then obtain i where i: "2 ^ i < ?m" "?m \<le> 2 ^ (i + 1)"
-    using ex_power_ivl2[of 2 ?m] by auto
-  have "n \<le> 2*?m"
-    by arith
-  also have "2*?m \<le> 2 ^ ((i+1)+1)"
-    using i(2) by simp
-  finally have *: "n \<le> \<dots>" .
-  have "2^(i+1) < n"
-    using i(1) by (auto simp add: less_Suc_eq_0_disj)
-  from ceil_log_nat_ivl[OF _ this *] ceil_log_nat_ivl[OF _ i]
-  show ?thesis by simp
-qed
-
-lemma floor_log2_div2: fixes n :: nat assumes "n \<ge> 2"
-shows "floor(log 2 n) = floor(log 2 (n div 2)) + 1"
-proof cases
-  assume "n=2"
-  thus ?thesis by simp
-next
-  let ?m = "n div 2"
-  assume "n\<noteq>2"
-  hence "1 \<le> ?m"
-    using assms by arith
-  then obtain i where i: "2 ^ i \<le> ?m" "?m < 2 ^ (i + 1)"
-    using ex_power_ivl1[of 2 ?m] by auto
-  have "2^(i+1) \<le> 2*?m"
-    using i(1) by simp
-  also have "2*?m \<le> n"
-    by arith
-  finally have *: "2^(i+1) \<le> \<dots>" .
-  have "n < 2^(i+1+1)"
-    using i(2) by simp
-  from floor_log_nat_ivl[OF _ * this] floor_log_nat_ivl[OF _ i]
-  show ?thesis by simp
-qed
-
-lemma balanced_Node_if_wbal1:
-assumes "balanced l" "balanced r" "size l = size r + 1"
-shows "balanced \<langle>l, x, r\<rangle>"
-proof -
-  from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_def)
-  have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
-    by(rule nat_mono[OF ceiling_mono]) simp
-  hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
-    using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
-    by (simp del: nat_ceiling_le_eq add: max_def)
-  have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
-    by(rule nat_mono[OF floor_mono]) simp
-  hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
-    using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
-    by (simp)
-  have "size1 r \<ge> 1" by(simp add: size1_def)
-  then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
-    using ex_power_ivl1[of 2 "size1 r"] by auto
-  hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
-  from 1 2 floor_log_nat_ivl[OF _ i] ceil_log_nat_ivl[OF _ i1]
-  show ?thesis by(simp add:balanced_def)
-qed
-
-lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
-by(auto simp: balanced_def)
-
-lemma balanced_Node_if_wbal2:
-assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
-shows "balanced \<langle>l, x, r\<rangle>"
-proof -
-  have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
-    using assms(3) by linarith
-  thus ?thesis
-  proof
-    assume "?A"
-    thus ?thesis using assms(1,2)
-      apply(simp add: balanced_def min_def max_def)
-      by (metis assms(1,2) balanced_optimal le_antisym le_less)
-  next
-    assume "?B"
-    thus ?thesis
-      by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
-  qed
-qed
-
-lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
-proof(induction t)
-  case Leaf show ?case by (simp add: balanced_def)
-next
-  case (Node l x r)
-  thus ?case by(simp add: balanced_Node_if_wbal2)
-qed
-
-(* end of mv *)
-
 fun bal :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree * 'a list" where
 "bal n xs = (if n=0 then (Leaf,xs) else
  (let m = n div 2;
@@ -247,7 +106,7 @@
 by(simp add: balance_tree_def)
 
 lemma min_height_bal:
-  "bal n xs = (t,ys) \<Longrightarrow> min_height t = nat(floor(log 2 (n + 1)))"
+  "bal n xs = (t,ys) \<Longrightarrow> min_height t = nat(\<lfloor>log 2 (n + 1)\<rfloor>)"
 proof(induction n xs arbitrary: t ys rule: bal.induct)
   case (1 n xs) show ?case
   proof cases
@@ -307,7 +166,7 @@
     also have "\<dots> = ?log1 + 1" using le by (simp add: max_absorb1)
     also have "\<dots> = nat \<lceil>log 2 (n div 2 + 1) + 1\<rceil>" using 0 by linarith
     also have "\<dots> = nat \<lceil>log 2 (n + 1)\<rceil>"
-      using ceil_log2_div2[of "n+1"] by (simp)
+      using ceiling_log2_div2[of "n+1"] by (simp)
     finally show ?thesis .
   qed
 qed
@@ -327,12 +186,12 @@
 by (simp add: balance_list_def height_bal_list)
 
 corollary height_bal_tree:
-  "n \<le> length xs \<Longrightarrow> height (bal_tree n t) = nat(ceiling(log 2 (n + 1)))"
+  "n \<le> length xs \<Longrightarrow> height (bal_tree n t) = nat\<lceil>log 2 (n + 1)\<rceil>"
 unfolding bal_list_def bal_tree_def
 using height_bal prod.exhaust_sel by blast
 
 corollary height_balance_tree:
-  "height (balance_tree t) = nat(ceiling(log 2 (size t + 1)))"
+  "height (balance_tree t) = nat\<lceil>log 2 (size t + 1)\<rceil>"
 by (simp add: bal_tree_def balance_tree_def height_bal_list)
 
 corollary balanced_bal_list[simp]: "balanced (bal_list n xs)"
diff -r 70e3f446bfc7 -r 7c7977f6c4ce src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sat Aug 26 12:56:17 2017 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Sat Aug 26 17:57:04 2017 +0200
@@ -3423,7 +3423,7 @@
           (((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
         by (simp add: fp_def np algebra_simps)
       also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
-        using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
+        using floor_eq_iff[where x="?N ?nxs" and a="?l"] by simp
       moreover
       have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))" by simp
       ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"
@@ -3449,7 +3449,7 @@
           (((?N ?nxs \<ge> real_of_int ?l) \<and> (?N ?nxs < real_of_int (?l + 1))) \<and> (?N a = ?N ?nxs ))"
         by (simp add: np fp_def algebra_simps)
       also have "\<dots> \<longrightarrow> \<lfloor>?N ?nxs\<rfloor> = ?l \<and> ?N a = ?N ?nxs"
-        using floor_unique_iff[where x="?N ?nxs" and a="?l"] by simp
+        using floor_eq_iff[where x="?N ?nxs" and a="?l"] by simp
       moreover
       have "\<dots> \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"  by simp
       ultimately have "?I (?p (p',n',s') j) \<longrightarrow> (?N (Floor a) = ?N ((Add (Floor s') (C j))))"
diff -r 70e3f446bfc7 -r 7c7977f6c4ce src/HOL/Library/Tree_Real.thy
--- a/src/HOL/Library/Tree_Real.thy	Sat Aug 26 12:56:17 2017 +0100
+++ b/src/HOL/Library/Tree_Real.thy	Sat Aug 26 17:57:04 2017 +0200
@@ -61,4 +61,57 @@
   show ?thesis by linarith
 qed
 
+lemma balanced_Node_if_wbal1:
+assumes "balanced l" "balanced r" "size l = size r + 1"
+shows "balanced \<langle>l, x, r\<rangle>"
+proof -
+  from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_def)
+  have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
+    by(rule nat_mono[OF ceiling_mono]) simp
+  hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
+    using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
+    by (simp del: nat_ceiling_le_eq add: max_def)
+  have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
+    by(rule nat_mono[OF floor_mono]) simp
+  hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
+    using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
+    by (simp)
+  have "size1 r \<ge> 1" by(simp add: size1_def)
+  then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
+    using ex_power_ivl1[of 2 "size1 r"] by auto
+  hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
+  from 1 2 floor_log_nat_eq_if[OF i] ceiling_log_nat_eq_if[OF i1]
+  show ?thesis by(simp add:balanced_def)
+qed
+
+lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
+by(auto simp: balanced_def)
+
+lemma balanced_Node_if_wbal2:
+assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
+shows "balanced \<langle>l, x, r\<rangle>"
+proof -
+  have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
+    using assms(3) by linarith
+  thus ?thesis
+  proof
+    assume "?A"
+    thus ?thesis using assms(1,2)
+      apply(simp add: balanced_def min_def max_def)
+      by (metis assms(1,2) balanced_optimal le_antisym le_less)
+  next
+    assume "?B"
+    thus ?thesis
+      by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
+  qed
+qed
+
+lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
+proof(induction t)
+  case Leaf show ?case by (simp add: balanced_def)
+next
+  case (Node l x r)
+  thus ?case by(simp add: balanced_Node_if_wbal2)
+qed
+
 end
\ No newline at end of file
diff -r 70e3f446bfc7 -r 7c7977f6c4ce src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sat Aug 26 12:56:17 2017 +0100
+++ b/src/HOL/Real.thy	Sat Aug 26 17:57:04 2017 +0200
@@ -1495,9 +1495,6 @@
 lemma real_of_int_floor_add_one_gt [simp]: "r < real_of_int \<lfloor>r\<rfloor> + 1"
   by linarith
 
-lemma floor_eq_iff: "\<lfloor>x\<rfloor> = b \<longleftrightarrow> of_int b \<le> x \<and> x < of_int (b + 1)"
-  by (simp add: floor_unique_iff)
-
 lemma floor_divide_real_eq_div:
   assumes "0 \<le> b"
   shows "\<lfloor>a / real_of_int b\<rfloor> = \<lfloor>a\<rfloor> div b"
diff -r 70e3f446bfc7 -r 7c7977f6c4ce src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sat Aug 26 12:56:17 2017 +0100
+++ b/src/HOL/Transcendental.thy	Sat Aug 26 17:57:04 2017 +0200
@@ -2694,7 +2694,7 @@
   by auto
 
 lemmas powr_le_iff = le_log_iff[symmetric]
-  and powr_less_iff = le_log_iff[symmetric]
+  and powr_less_iff = less_log_iff[symmetric]
   and less_powr_iff = log_less_iff[symmetric]
   and le_powr_iff = log_le_iff[symmetric]
 
@@ -2739,6 +2739,80 @@
 lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
   by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
 
+lemma floor_log_nat_eq_powr_iff: fixes b n k :: nat
+  shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
+  floor (log b (real k)) = n \<longleftrightarrow> b^n \<le> k \<and> k < b^(n+1)"
+by (auto simp: floor_log_eq_powr_iff powr_add powr_realpow
+               of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
+         simp del: of_nat_power of_nat_mult)
+
+lemma floor_log_nat_eq_if: fixes b n k :: nat
+  assumes "b^n \<le> k" "k < b^(n+1)" "b \<ge> 2"
+  shows "floor (log b (real k)) = n"
+proof -
+  have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
+  with assms show ?thesis by(simp add: floor_log_nat_eq_powr_iff)
+qed
+
+lemma ceiling_log_eq_powr_iff: "\<lbrakk> x > 0; b > 1 \<rbrakk>
+  \<Longrightarrow> \<lceil>log b x\<rceil> = int k + 1 \<longleftrightarrow> b powr k < x \<and> x \<le> b powr (k + 1)"
+by (auto simp add: ceiling_eq_iff powr_less_iff le_powr_iff)
+
+lemma ceiling_log_nat_eq_powr_iff: fixes b n k :: nat
+  shows "\<lbrakk> b \<ge> 2; k > 0 \<rbrakk> \<Longrightarrow>
+  ceiling (log b (real k)) = int n + 1 \<longleftrightarrow> (b^n < k \<and> k \<le> b^(n+1))"
+using ceiling_log_eq_powr_iff
+by (auto simp: powr_add powr_realpow of_nat_power[symmetric] of_nat_mult[symmetric] ac_simps
+         simp del: of_nat_power of_nat_mult)
+
+lemma ceiling_log_nat_eq_if: fixes b n k :: nat
+  assumes "b^n < k" "k \<le> b^(n+1)" "b \<ge> 2"
+  shows "ceiling (log b (real k)) = int n + 1"
+proof -
+  have "k \<ge> 1" using assms(1,3) one_le_power[of b n] by linarith
+  with assms show ?thesis by(simp add: ceiling_log_nat_eq_powr_iff)
+qed
+
+(* FIXME: a more appropriate place for these two lemmas
+   is a theory of discrete logarithms
+*)
+
+lemma floor_log2_div2: fixes n :: nat assumes "n \<ge> 2"
+shows "floor(log 2 n) = floor(log 2 (n div 2)) + 1"
+proof cases
+  assume "n=2" thus ?thesis by simp
+next
+  let ?m = "n div 2"
+  assume "n\<noteq>2"
+  hence "1 \<le> ?m" using assms by arith
+  then obtain i where i: "2 ^ i \<le> ?m" "?m < 2 ^ (i + 1)"
+    using ex_power_ivl1[of 2 ?m] by auto
+  have "2^(i+1) \<le> 2*?m" using i(1) by simp
+  also have "2*?m \<le> n" by arith
+  finally have *: "2^(i+1) \<le> \<dots>" .
+  have "n < 2^(i+1+1)" using i(2) by simp
+  from floor_log_nat_eq_if[OF * this] floor_log_nat_eq_if[OF i]
+  show ?thesis by simp
+qed
+
+lemma ceiling_log2_div2: assumes "n \<ge> 2"
+shows "ceiling(log 2 (real n)) = ceiling(log 2 ((n-1) div 2 + 1)) + 1"
+proof cases
+  assume "n=2" thus ?thesis by simp
+next
+  let ?m = "(n-1) div 2 + 1"
+  assume "n\<noteq>2"
+  hence "2 \<le> ?m" using assms by arith
+  then obtain i where i: "2 ^ i < ?m" "?m \<le> 2 ^ (i + 1)"
+    using ex_power_ivl2[of 2 ?m] by auto
+  have "n \<le> 2*?m" by arith
+  also have "2*?m \<le> 2 ^ ((i+1)+1)" using i(2) by simp
+  finally have *: "n \<le> \<dots>" .
+  have "2^(i+1) < n" using i(1) by (auto simp add: less_Suc_eq_0_disj)
+  from ceiling_log_nat_eq_if[OF this *] ceiling_log_nat_eq_if[OF i]
+  show ?thesis by simp
+qed
+
 lemma powr_real_of_int:
   "x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (- n)))"
   using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]