src/HOL/Library/Tree.thy
changeset 69117 3d3e87835ae8
parent 69115 919a1b23c192
child 69218 59aefb3b9e95
equal deleted inserted replaced
69115:919a1b23c192 69117:3d3e87835ae8
   225 by (induction t) auto
   225 by (induction t) auto
   226 
   226 
   227 lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
   227 lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
   228 using size1_if_complete[simplified size1_size] by fastforce
   228 using size1_if_complete[simplified size1_size] by fastforce
   229 
   229 
       
   230 lemma size1_height_if_incomplete:
       
   231   "\<not> complete t \<Longrightarrow> size1 t < 2 ^ height t"
       
   232 proof(induction t)
       
   233   case Leaf thus ?case by simp
       
   234 next
       
   235   case (Node l x r)
       
   236   have 1: ?case if h: "height l < height r"
       
   237     using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of "2::nat"]
       
   238     by(auto simp: max_def simp del: power_strict_increasing_iff)
       
   239   have 2: ?case if h: "height l > height r"
       
   240     using h size1_height[of l] size1_height[of r] power_strict_increasing[OF h, of "2::nat"]
       
   241     by(auto simp: max_def simp del: power_strict_increasing_iff)
       
   242   have 3: ?case if h: "height l = height r" and c: "\<not> complete l"
       
   243     using h size1_height[of r] Node.IH(1)[OF c] by(simp)
       
   244   have 4: ?case if h: "height l = height r" and c: "\<not> complete r"
       
   245     using h size1_height[of l] Node.IH(2)[OF c] by(simp)
       
   246   from 1 2 3 4 Node.prems show ?case apply (simp add: max_def) by linarith
       
   247 qed
       
   248 
       
   249 lemma complete_iff_min_height: "complete t \<longleftrightarrow> (height t = min_height t)"
       
   250 by(auto simp add: complete_iff_height)
       
   251 
       
   252 lemma min_height_size1_if_incomplete:
       
   253   "\<not> complete t \<Longrightarrow> 2 ^ min_height t < size1 t"
       
   254 proof(induction t)
       
   255   case Leaf thus ?case by simp
       
   256 next
       
   257   case (Node l x r)
       
   258   have 1: ?case if h: "min_height l < min_height r"
       
   259     using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of "2::nat"]
       
   260     by(auto simp: max_def simp del: power_strict_increasing_iff)
       
   261   have 2: ?case if h: "min_height l > min_height r"
       
   262     using h min_height_size1[of l] min_height_size1[of r] power_strict_increasing[OF h, of "2::nat"]
       
   263     by(auto simp: max_def simp del: power_strict_increasing_iff)
       
   264   have 3: ?case if h: "min_height l = min_height r" and c: "\<not> complete l"
       
   265     using h min_height_size1[of r] Node.IH(1)[OF c] by(simp add: complete_iff_min_height)
       
   266   have 4: ?case if h: "min_height l = min_height r" and c: "\<not> complete r"
       
   267     using h min_height_size1[of l] Node.IH(2)[OF c] by(simp add: complete_iff_min_height)
       
   268   from 1 2 3 4 Node.prems show ?case
       
   269     by (fastforce simp: complete_iff_min_height[THEN iffD1])
       
   270 qed
       
   271 
   230 lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
   272 lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
   231 proof (induct "height t" arbitrary: t)
   273 using  size1_height_if_incomplete by fastforce
   232   case 0 thus ?case by (simp)
       
   233 next
       
   234   case (Suc h)
       
   235   hence "t \<noteq> Leaf" by auto
       
   236   then obtain l a r where [simp]: "t = Node l a r"
       
   237     by (auto simp: neq_Leaf_iff)
       
   238   have 1: "height l \<le> h" and 2: "height r \<le> h" using Suc(2) by(auto)
       
   239   have 3: "\<not> height l < h"
       
   240   proof
       
   241     assume 0: "height l < h"
       
   242     have "size1 t = size1 l + size1 r" by simp
       
   243     also have "\<dots> \<le> 2 ^ height l + 2 ^ height r"
       
   244       using size1_height[of l] size1_height[of r] by arith
       
   245     also have " \<dots> < 2 ^ h + 2 ^ height r" using 0 by (simp)
       
   246     also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 2 by (simp)
       
   247     also have "\<dots> = 2 ^ (Suc h)" by (simp)
       
   248     also have "\<dots> = size1 t" using Suc(2,3) by simp
       
   249     finally have "size1 t < size1 t" .
       
   250     thus False by (simp)
       
   251   qed
       
   252   have 4: "\<not> height r < h"
       
   253   proof
       
   254     assume 0: "height r < h"
       
   255     have "size1 t = size1 l + size1 r" by simp
       
   256     also have "\<dots> \<le> 2 ^ height l + 2 ^ height r"
       
   257       using size1_height[of l] size1_height[of r] by arith
       
   258     also have " \<dots> < 2 ^ height l + 2 ^ h" using 0 by (simp)
       
   259     also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 1 by (simp)
       
   260     also have "\<dots> = 2 ^ (Suc h)" by (simp)
       
   261     also have "\<dots> = size1 t" using Suc(2,3) by simp
       
   262     finally have "size1 t < size1 t" .
       
   263     thus False by (simp)
       
   264   qed
       
   265   from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+
       
   266   hence "size1 l = 2 ^ height l" "size1 r = 2 ^ height r"
       
   267     using Suc(3) size1_height[of l] size1_height[of r] by (auto)
       
   268   with * Suc(1) show ?case by simp
       
   269 qed
       
   270 
       
   271 text\<open>The following proof involves \<open>\<ge>\<close>/\<open>>\<close> chains rather than the standard
       
   272 \<open>\<le>\<close>/\<open><\<close> chains. To chain the elements together the transitivity rules \<open>xtrans\<close>
       
   273 are used.\<close>
       
   274 
   274 
   275 lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
   275 lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
   276 proof (induct "min_height t" arbitrary: t)
   276 using min_height_size1_if_incomplete by fastforce
   277   case 0 thus ?case by (simp add: size1_size)
       
   278 next
       
   279   case (Suc h)
       
   280   hence "t \<noteq> Leaf" by auto
       
   281   then obtain l a r where [simp]: "t = Node l a r"
       
   282     by (auto simp: neq_Leaf_iff)
       
   283   have 1: "h \<le> min_height l" and 2: "h \<le> min_height r" using Suc(2) by(auto)
       
   284   have 3: "\<not> h < min_height l"
       
   285   proof
       
   286     assume 0: "h < min_height l"
       
   287     have "size1 t = size1 l + size1 r" by simp
       
   288     also note min_height_size1[of l]
       
   289     also(xtrans) note min_height_size1[of r]
       
   290     also(xtrans) have "(2::nat) ^ min_height l > 2 ^ h"
       
   291         using 0 by (simp add: diff_less_mono)
       
   292     also(xtrans) have "(2::nat) ^ min_height r \<ge> 2 ^ h" using 2 by simp
       
   293     also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
       
   294     also have "\<dots> = size1 t" using Suc(2,3) by simp
       
   295     finally show False by (simp add: diff_le_mono)
       
   296   qed
       
   297   have 4: "\<not> h < min_height r"
       
   298   proof
       
   299     assume 0: "h < min_height r"
       
   300     have "size1 t = size1 l + size1 r" by simp
       
   301     also note min_height_size1[of l]
       
   302     also(xtrans) note min_height_size1[of r]
       
   303     also(xtrans) have "(2::nat) ^ min_height r > 2 ^ h"
       
   304         using 0 by (simp add: diff_less_mono)
       
   305     also(xtrans) have "(2::nat) ^ min_height l \<ge> 2 ^ h" using 1 by simp
       
   306     also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp)
       
   307     also have "\<dots> = size1 t" using Suc(2,3) by simp
       
   308     finally show False by (simp add: diff_le_mono)
       
   309   qed
       
   310   from 1 2 3 4 have *: "min_height l = h" "min_height r = h" by linarith+
       
   311   hence "size1 l = 2 ^ min_height l" "size1 r = 2 ^ min_height r"
       
   312     using Suc(3) min_height_size1[of l] min_height_size1[of r] by (auto)
       
   313   with * Suc(1) show ?case
       
   314     by (simp add: complete_iff_height)
       
   315 qed
       
   316 
   277 
   317 lemma complete_iff_size1: "complete t \<longleftrightarrow> size1 t = 2 ^ height t"
   278 lemma complete_iff_size1: "complete t \<longleftrightarrow> size1 t = 2 ^ height t"
   318 using complete_if_size1_height size1_if_complete by blast
   279 using complete_if_size1_height size1_if_complete by blast
   319 
       
   320 text\<open>Better bounds for incomplete trees:\<close>
       
   321 
       
   322 lemma size1_height_if_incomplete:
       
   323   "\<not> complete t \<Longrightarrow> size1 t < 2 ^ height t"
       
   324 by (meson antisym_conv complete_iff_size1 not_le size1_height)
       
   325 
       
   326 lemma min_height_size1_if_incomplete:
       
   327   "\<not> complete t \<Longrightarrow> 2 ^ min_height t < size1 t"
       
   328 by (metis complete_if_size1_min_height le_less min_height_size1)
       
   329 
   280 
   330 
   281 
   331 subsection \<open>@{const balanced}\<close>
   282 subsection \<open>@{const balanced}\<close>
   332 
   283 
   333 lemma balanced_subtreeL: "balanced (Node l x r) \<Longrightarrow> balanced l"
   284 lemma balanced_subtreeL: "balanced (Node l x r) \<Longrightarrow> balanced l"