# HG changeset patch
# User nipkow
# Date 1475690465 -7200
# Node ID c6eb691770d84a47de8dbe5ba71cda718d980a1c
# Parent  5c2c559f01ebb78ccace859fb07551a925421743
replaced floorlog by floor/ceiling(log .)

diff -r 5c2c559f01eb -r c6eb691770d8 src/HOL/Data_Structures/Balance.thy
--- a/src/HOL/Data_Structures/Balance.thy	Wed Oct 05 14:28:22 2016 +0200
+++ b/src/HOL/Data_Structures/Balance.thy	Wed Oct 05 20:01:05 2016 +0200
@@ -4,10 +4,138 @@
 
 theory Balance
 imports
+  Complex_Main
   "~~/src/HOL/Library/Tree"
-  "~~/src/HOL/Library/Log_Nat"
 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. \<close>
+
+lemma floor_log_nat: 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: 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 ex_power_ivl1: fixes b k :: nat assumes "b \<ge> 2"
+shows "k \<ge> 1 \<Longrightarrow> \<exists>n. b^n \<le> k \<and> k < b^(n+1)" (is "_ \<Longrightarrow> \<exists>n. ?P k n")
+proof(induction k)
+  case 0 thus ?case by simp
+next
+  case (Suc k)
+  show ?case
+  proof cases
+    assume "k=0"
+    hence "?P (Suc k) 0"
+      using assms by simp
+    thus ?case ..
+  next
+    assume "k\<noteq>0"
+    with Suc obtain n where IH: "?P k n" by auto
+    show ?case
+    proof (cases "k = b^(n+1) - 1")
+      case True
+      hence "?P (Suc k) (n+1)" using assms
+        by (simp add: not_less_eq_eq[symmetric])
+      thus ?thesis ..
+    next
+      case False
+      hence "?P (Suc k) n" using IH by auto
+      thus ?thesis ..
+    qed
+  qed
+qed
+
+lemma ex_power_ivl2: fixes b k :: nat assumes "b \<ge> 2" "(k::nat) \<ge> 2"
+shows "\<exists>n. b^n < k \<and> k \<le> b^(n+1)"
+proof -
+  have "1 \<le> k - 1"
+    using assms(2) by arith
+  from ex_power_ivl1[OF assms(1) this]
+  obtain n where "b ^ n \<le> k - 1 \<and> k - 1 < b ^ (n + 1)" ..
+  hence "b^n < k \<and> k \<le> b^(n+1)"
+    using assms by auto
+  thus ?thesis ..
+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[OF _ this *] ceil_log_nat[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[OF _ * this] floor_log_nat[OF _ i]
+  show ?thesis by simp
+qed
+
+(* end of mv *)
+
 fun bal :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree * 'a list" where
 "bal xs n = (if n=0 then (Leaf,xs) else
  (let m = n div 2;
@@ -28,8 +156,8 @@
   "n > 0 \<Longrightarrow>
    bal xs n =
   (let m = n div 2;
-      (l, ys) = Balance.bal xs m;
-      (r, zs) = Balance.bal (tl ys) (n-1-m)
+      (l, ys) = bal xs m;
+      (r, zs) = bal (tl ys) (n-1-m)
   in (Node l (hd ys) r, zs))"
 by(simp_all add: bal.simps)
 
@@ -78,39 +206,22 @@
 using bal_inorder[of xs "length xs"]
 by (metis balance_list_def order_refl prod.collapse take_all)
 
-lemma bal_height: "bal xs n = (t,ys) \<Longrightarrow> height t = floorlog 2 n"
+corollary inorder_balance_tree[simp]: "inorder(balance_tree t) = inorder t"
+by(simp add: balance_tree_def inorder_balance_list)
+
+corollary size_balance_list[simp]: "size(balance_list xs) = length xs"
+by (metis inorder_balance_list length_inorder)
+
+corollary size_balance_tree[simp]: "size(balance_tree t) = size t"
+by(simp add: balance_tree_def inorder_balance_list)
+
+lemma min_height_bal:
+  "bal xs n = (t,ys) \<Longrightarrow> min_height t = nat(floor(log 2 (n + 1)))"
 proof(induction xs n arbitrary: t ys rule: bal.induct)
   case (1 xs n) show ?case
   proof cases
     assume "n = 0" thus ?thesis
-      using "1.prems" by (simp add: floorlog_def bal_simps)
-  next
-    assume [arith]: "n \<noteq> 0"
-    from "1.prems" obtain l r xs' where
-      b1: "bal xs (n div 2) = (l,xs')" and
-      b2: "bal (tl xs') (n - 1 - n div 2) = (r,ys)" and
-      t: "t = \<langle>l, hd xs', r\<rangle>"
-      by(auto simp: bal_simps Let_def split: prod.splits)
-    let ?log1 = "floorlog 2 (n div 2)"
-    let ?log2 = "floorlog 2 (n - 1 - n div 2)"
-    have IH1: "height l = ?log1" using "1.IH"(1) b1 by simp
-    have IH2: "height r = ?log2" using "1.IH"(2) b1 b2 by simp
-    have "n div 2 \<ge> n - 1 - n div 2" by arith
-    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: compute_floorlog)
-    finally show ?thesis .
-  qed
-qed
-
-lemma bal_min_height:
-  "bal xs n = (t,ys) \<Longrightarrow> min_height t = floorlog 2 (n + 1) - 1"
-proof(induction xs n arbitrary: t ys rule: bal.induct)
-  case (1 xs n) show ?case
-  proof cases
-    assume "n = 0" thus ?thesis
-      using "1.prems" by (simp add: floorlog_def bal_simps)
+      using "1.prems" by (simp add: bal_simps)
   next
     assume [arith]: "n \<noteq> 0"
     from "1.prems" obtain l r xs' where
@@ -118,54 +229,78 @@
       b2: "bal (tl xs') (n - 1 - n div 2) = (r,ys)" and
       t: "t = \<langle>l, hd xs', r\<rangle>"
       by(auto simp: bal_simps Let_def split: prod.splits)
-    let ?log1 = "floorlog 2 (n div 2 + 1) - 1"
-    let ?log2 = "floorlog 2 (n - 1 - n div 2 + 1) - 1"
-    let ?log2' = "floorlog 2 (n - n div 2) - 1"
-    have "n - 1 - n div 2 + 1 = n - n div 2" by arith
-    hence IH2: "min_height r = ?log2'" using "1.IH"(2) b1 b2 by simp
+    let ?log1 = "nat (floor(log 2 (n div 2 + 1)))"
+    let ?log2 = "nat (floor(log 2 (n - 1 - n div 2 + 1)))"
     have IH1: "min_height l = ?log1" using "1.IH"(1) b1 by simp
-    have *: "floorlog 2 (n - n div 2) \<ge> 1" by (simp add: floorlog_def)
-    have "n div 2 + 1 \<ge> n - n div 2" by arith
-    with * have le: "?log2' \<le> ?log1" by(simp add: floorlog_mono diff_le_mono)
-    have "min_height t = min ?log1 ?log2' + 1" by (simp add: t IH1 IH2)
-    also have "\<dots> = ?log2' + 1" using le by (simp add: min_absorb2)
-    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: compute_floorlog)
+    have IH2: "min_height r = ?log2" using "1.IH"(2) b1 b2 by simp
+    have "(n+1) div 2 \<ge> 1" by arith
+    hence 0: "log 2 ((n+1) div 2) \<ge> 0" by simp
+    have "n - 1 - n div 2 + 1 \<le> n div 2 + 1" by arith
+    hence le: "?log2 \<le> ?log1"
+      by(simp add: nat_mono floor_mono)
+    have "min_height t = min ?log1 ?log2 + 1" by (simp add: t IH1 IH2)
+    also have "\<dots> = ?log2 + 1" using le by (simp add: min_absorb2)
+    also have "n - 1 - n div 2 + 1 = (n+1) div 2" by linarith
+    also have "nat (floor(log 2 ((n+1) div 2))) + 1
+       = nat (floor(log 2 ((n+1) div 2) + 1))"
+      using 0 by linarith
+    also have "\<dots> = nat (floor(log 2 (n + 1)))"
+      using floor_log2_div2[of "n+1"] by (simp add: log_mult)
+    finally show ?thesis .
+  qed
+qed
+
+lemma height_bal:
+  "bal xs n = (t,ys) \<Longrightarrow> height t = nat \<lceil>log 2 (n + 1)\<rceil>"
+proof(induction xs n arbitrary: t ys rule: bal.induct)
+  case (1 xs n) show ?case
+  proof cases
+    assume "n = 0" thus ?thesis
+      using "1.prems" by (simp add: bal_simps)
+  next
+    assume [arith]: "n \<noteq> 0"
+    from "1.prems" obtain l r xs' where
+      b1: "bal xs (n div 2) = (l,xs')" and
+      b2: "bal (tl xs') (n - 1 - n div 2) = (r,ys)" and
+      t: "t = \<langle>l, hd xs', r\<rangle>"
+      by(auto simp: bal_simps Let_def split: prod.splits)
+    let ?log1 = "nat \<lceil>log 2 (n div 2 + 1)\<rceil>"
+    let ?log2 = "nat \<lceil>log 2 (n - 1 - n div 2 + 1)\<rceil>"
+    have IH1: "height l = ?log1" using "1.IH"(1) b1 by simp
+    have IH2: "height r = ?log2" using "1.IH"(2) b1 b2 by simp
+    have 0: "log 2 (n div 2 + 1) \<ge> 0" by auto
+    have "n - 1 - n div 2 + 1 \<le> n div 2 + 1" by arith
+    hence le: "?log2 \<le> ?log1"
+      by(simp add: nat_mono ceiling_mono del: nat_ceiling_le_eq)
+    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> = 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)
     finally show ?thesis .
   qed
 qed
 
 lemma balanced_bal:
   assumes "bal xs n = (t,ys)" shows "balanced t"
-proof -
-  have "floorlog 2 n \<le> floorlog 2 (n+1)" by (rule floorlog_mono) auto
-  thus ?thesis unfolding balanced_def
-    using bal_height[OF assms] bal_min_height[OF assms] by linarith
-qed
+unfolding balanced_def
+using height_bal[OF assms] min_height_bal[OF assms]
+by linarith
 
-corollary size_balance_list[simp]: "size(balance_list xs) = length xs"
-by (metis inorder_balance_list length_inorder)
+lemma height_balance_list:
+  "height (balance_list xs) = nat \<lceil>log 2 (length xs + 1)\<rceil>"
+by (metis balance_list_def height_bal prod.collapse)
+
+corollary height_balance_tree:
+  "height (balance_tree t) = nat(ceiling(log 2 (size t + 1)))"
+by(simp add: balance_tree_def height_balance_list)
 
 corollary balanced_balance_list[simp]: "balanced (balance_list xs)"
 by (metis balance_list_def balanced_bal prod.collapse)
 
-lemma height_balance_list: "height(balance_list xs) = floorlog 2 (length xs)"
-by (metis bal_height balance_list_def prod.collapse)
-
-lemma inorder_balance_tree[simp]: "inorder(balance_tree t) = inorder t"
-by(simp add: balance_tree_def inorder_balance_list)
-
-lemma size_balance_tree[simp]: "size(balance_tree t) = size t"
-by(simp add: balance_tree_def inorder_balance_list)
-
 corollary balanced_balance_tree[simp]: "balanced (balance_tree t)"
 by (simp add: balance_tree_def)
 
-lemma height_balance_tree: "height(balance_tree t) = floorlog 2 (size t)"
-by(simp add: balance_tree_def height_balance_list)
-
 lemma wbalanced_bal: "bal xs n = (t,ys) \<Longrightarrow> wbalanced t"
 proof(induction xs n arbitrary: t ys rule: bal.induct)
   case (1 xs n)