# HG changeset patch
# User nipkow
# Date 1538644719 -7200
# Node ID 12dce58bcd3f970563c6465d6c52684cfb0771cb
# Parent  cbcc43a00cff300a6dab7a1692ac35eb2d9be028# Parent  3d3e87835ae8c04b3a0a1de9daf8e463edf32761
merged

diff -r cbcc43a00cff -r 12dce58bcd3f src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Oct 04 11:10:15 2018 +0200
+++ b/src/HOL/Library/Tree.thy	Thu Oct 04 11:18:39 2018 +0200
@@ -227,106 +227,57 @@
 lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
 using size1_if_complete[simplified size1_size] by fastforce
 
-lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
-proof (induct "height t" arbitrary: t)
-  case 0 thus ?case by (simp)
+lemma size1_height_if_incomplete:
+  "\<not> complete t \<Longrightarrow> size1 t < 2 ^ height t"
+proof(induction t)
+  case Leaf thus ?case by simp
 next
-  case (Suc h)
-  hence "t \<noteq> Leaf" by auto
-  then obtain l a r where [simp]: "t = Node l a r"
-    by (auto simp: neq_Leaf_iff)
-  have 1: "height l \<le> h" and 2: "height r \<le> h" using Suc(2) by(auto)
-  have 3: "\<not> height l < h"
-  proof
-    assume 0: "height l < h"
-    have "size1 t = size1 l + size1 r" by simp
-    also have "\<dots> \<le> 2 ^ height l + 2 ^ height r"
-      using size1_height[of l] size1_height[of r] by arith
-    also have " \<dots> < 2 ^ h + 2 ^ height r" using 0 by (simp)
-    also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 2 by (simp)
-    also have "\<dots> = 2 ^ (Suc h)" by (simp)
-    also have "\<dots> = size1 t" using Suc(2,3) by simp
-    finally have "size1 t < size1 t" .
-    thus False by (simp)
-  qed
-  have 4: "\<not> height r < h"
-  proof
-    assume 0: "height r < h"
-    have "size1 t = size1 l + size1 r" by simp
-    also have "\<dots> \<le> 2 ^ height l + 2 ^ height r"
-      using size1_height[of l] size1_height[of r] by arith
-    also have " \<dots> < 2 ^ height l + 2 ^ h" using 0 by (simp)
-    also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 1 by (simp)
-    also have "\<dots> = 2 ^ (Suc h)" by (simp)
-    also have "\<dots> = size1 t" using Suc(2,3) by simp
-    finally have "size1 t < size1 t" .
-    thus False by (simp)
-  qed
-  from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+
-  hence "size1 l = 2 ^ height l" "size1 r = 2 ^ height r"
-    using Suc(3) size1_height[of l] size1_height[of r] by (auto)
-  with * Suc(1) show ?case by simp
+  case (Node l x r)
+  have 1: ?case if h: "height l < height r"
+    using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of "2::nat"]
+    by(auto simp: max_def simp del: power_strict_increasing_iff)
+  have 2: ?case if h: "height l > height r"
+    using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of "2::nat"]
+    by(auto simp: max_def simp del: power_strict_increasing_iff)
+  have 3: ?case if h: "height l = height r" and c: "\<not> complete l"
+    using h size1_height[of r] Node.IH(1)[OF c] by(simp)
+  have 4: ?case if h: "height l = height r" and c: "\<not> complete r"
+    using h size1_height[of l] Node.IH(2)[OF c] by(simp)
+  from 1 2 3 4 Node.prems show ?case apply (simp add: max_def) by linarith
 qed
 
-text\<open>The following proof involves \<open>\<ge>\<close>/\<open>>\<close> chains rather than the standard
-\<open>\<le>\<close>/\<open><\<close> chains. To chain the elements together the transitivity rules \<open>xtrans\<close>
-are used.\<close>
+lemma complete_iff_min_height: "complete t \<longleftrightarrow> (height t = min_height t)"
+by(auto simp add: complete_iff_height)
+
+lemma min_height_size1_if_incomplete:
+  "\<not> complete t \<Longrightarrow> 2 ^ min_height t < size1 t"
+proof(induction t)
+  case Leaf thus ?case by simp
+next
+  case (Node l x r)
+  have 1: ?case if h: "min_height l < min_height r"
+    using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of "2::nat"]
+    by(auto simp: max_def simp del: power_strict_increasing_iff)
+  have 2: ?case if h: "min_height l > min_height r"
+    using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of "2::nat"]
+    by(auto simp: max_def simp del: power_strict_increasing_iff)
+  have 3: ?case if h: "min_height l = min_height r" and c: "\<not> complete l"
+    using h min_height_size1[of r] Node.IH(1)[OF c] by(simp add: complete_iff_min_height)
+  have 4: ?case if h: "min_height l = min_height r" and c: "\<not> complete r"
+    using h min_height_size1[of l] Node.IH(2)[OF c] by(simp add: complete_iff_min_height)
+  from 1 2 3 4 Node.prems show ?case
+    by (fastforce simp: complete_iff_min_height[THEN iffD1])
+qed
+
+lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
+using  size1_height_if_incomplete by fastforce
 
 lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
-proof (induct "min_height t" arbitrary: t)
-  case 0 thus ?case by (simp add: size1_size)
-next
-  case (Suc h)
-  hence "t \<noteq> Leaf" by auto
-  then obtain l a r where [simp]: "t = Node l a r"
-    by (auto simp: neq_Leaf_iff)
-  have 1: "h \<le> min_height l" and 2: "h \<le> min_height r" using Suc(2) by(auto)
-  have 3: "\<not> h < min_height l"
-  proof
-    assume 0: "h < min_height l"
-    have "size1 t = size1 l + size1 r" by simp
-    also note min_height_size1[of l]
-    also(xtrans) note min_height_size1[of r]
-    also(xtrans) have "(2::nat) ^ min_height l > 2 ^ h"
-        using 0 by (simp add: diff_less_mono)
-    also(xtrans) have "(2::nat) ^ min_height r \<ge> 2 ^ h" using 2 by simp
-    also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
-    also have "\<dots> = size1 t" using Suc(2,3) by simp
-    finally show False by (simp add: diff_le_mono)
-  qed
-  have 4: "\<not> h < min_height r"
-  proof
-    assume 0: "h < min_height r"
-    have "size1 t = size1 l + size1 r" by simp
-    also note min_height_size1[of l]
-    also(xtrans) note min_height_size1[of r]
-    also(xtrans) have "(2::nat) ^ min_height r > 2 ^ h"
-        using 0 by (simp add: diff_less_mono)
-    also(xtrans) have "(2::nat) ^ min_height l \<ge> 2 ^ h" using 1 by simp
-    also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
-    also have "\<dots> = size1 t" using Suc(2,3) by simp
-    finally show False by (simp add: diff_le_mono)
-  qed
-  from 1 2 3 4 have *: "min_height l = h" "min_height r = h" by linarith+
-  hence "size1 l = 2 ^ min_height l" "size1 r = 2 ^ min_height r"
-    using Suc(3) min_height_size1[of l] min_height_size1[of r] by (auto)
-  with * Suc(1) show ?case
-    by (simp add: complete_iff_height)
-qed
+using min_height_size1_if_incomplete by fastforce
 
 lemma complete_iff_size1: "complete t \<longleftrightarrow> size1 t = 2 ^ height t"
 using complete_if_size1_height size1_if_complete by blast
 
-text\<open>Better bounds for incomplete trees:\<close>
-
-lemma size1_height_if_incomplete:
-  "\<not> complete t \<Longrightarrow> size1 t < 2 ^ height t"
-by (meson antisym_conv complete_iff_size1 not_le size1_height)
-
-lemma min_height_size1_if_incomplete:
-  "\<not> complete t \<Longrightarrow> 2 ^ min_height t < size1 t"
-by (metis complete_if_size1_min_height le_less min_height_size1)
-
 
 subsection \<open>@{const balanced}\<close>
 
diff -r cbcc43a00cff -r 12dce58bcd3f src/HOL/Library/Tree_Real.thy
--- a/src/HOL/Library/Tree_Real.thy	Thu Oct 04 11:10:15 2018 +0200
+++ b/src/HOL/Library/Tree_Real.thy	Thu Oct 04 11:18:39 2018 +0200
@@ -37,29 +37,24 @@
   assume *: "\<not> complete t"
   hence "height t = min_height t + 1"
     using assms min_height_le_height[of t]
-    by(auto simp add: balanced_def complete_iff_height)
-  hence "size1 t < 2 ^ (min_height t + 1)"
-    by (metis * size1_height_if_incomplete)
-  hence "log 2 (size1 t) < min_height t + 1"
-    using log2_of_power_less size1_ge0 by blast
-  thus ?thesis using min_height_size1_log[of t] by linarith
+    by(auto simp: balanced_def complete_iff_height)
+  hence "size1 t < 2 ^ (min_height t + 1)" by (metis * size1_height_if_incomplete)
+  from floor_log_nat_eq_if[OF min_height_size1 this] show ?thesis by simp
 qed
 
 lemma height_balanced: assumes "balanced t"
 shows "height t = nat(ceiling(log 2 (size1 t)))"
 proof cases
   assume *: "complete t"
-  hence "size1 t = 2 ^ height t"
-    by (simp add: size1_if_complete)
-  from log2_of_power_eq[OF this] show ?thesis
-    by linarith
+  hence "size1 t = 2 ^ height t" by (simp add: size1_if_complete)
+  from log2_of_power_eq[OF this] show ?thesis by linarith
 next
   assume *: "\<not> complete t"
   hence **: "height t = min_height t + 1"
     using assms min_height_le_height[of t]
     by(auto simp add: balanced_def complete_iff_height)
   hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
-  from  log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
+  from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
   show ?thesis by linarith
 qed