# HG changeset patch
# User nipkow
# Date 1481094880 -3600
# Node ID 3d4331b658613805a57bd86fbdd7de33f6ef296b
# Parent  f1f4ba6d02c93ab77820290e6d9c4d816c6d0919
more lemmas

diff -r f1f4ba6d02c9 -r 3d4331b65861 src/HOL/Data_Structures/Balance.thy
--- a/src/HOL/Data_Structures/Balance.thy	Mon Dec 05 18:14:41 2016 +0100
+++ b/src/HOL/Data_Structures/Balance.thy	Wed Dec 07 08:14:40 2016 +0100
@@ -151,6 +151,59 @@
   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
@@ -374,6 +427,10 @@
   qed
 qed
 
+text\<open>An alternative proof via @{thm balanced_if_wbalanced}:\<close>
+lemma "bal n xs = (t,ys) \<Longrightarrow> balanced t"
+by(rule balanced_if_wbalanced[OF wbalanced_bal])
+
 lemma wbalanced_bal_list[simp]: "wbalanced (bal_list n xs)"
 by(simp add: bal_list_def) (metis prod.collapse wbalanced_bal)