summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 02 Sep 2016 16:10:23 +0200 | |

changeset 63771 | 81e4d4f42f65 |

parent 63769 | 511d5ffd56ac (current diff) |

parent 63770 | a67397b13eb5 (diff) |

child 63775 | fd6caec306fc |

merged

--- a/src/HOL/Library/Tree.thy Fri Sep 02 11:26:52 2016 +0200 +++ b/src/HOL/Library/Tree.thy Fri Sep 02 16:10:23 2016 +0200 @@ -1,7 +1,7 @@ (* Author: Tobias Nipkow *) (* Todo: - size t = 2^h - 1 \<Longrightarrow> complete t (min_)height of balanced trees via floorlog + minimal path_len of balanced trees *) section \<open>Binary Tree\<close> @@ -125,11 +125,55 @@ apply (simp add: min_def max_def) by (metis le_antisym le_trans min_hight_le_height) -lemma complete_size1: "complete t \<Longrightarrow> size1 t = 2 ^ height t" +lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t" by (induction t) auto lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1" -using complete_size1[simplified size1_def] by fastforce +using size1_if_complete[simplified size1_def] by fastforce + +lemma complete_if_size: "size t = 2 ^ height t - 1 \<Longrightarrow> complete t" +proof (induct "height t" arbitrary: t) + case 0 thus ?case by (simp add: size_0_iff_Leaf) +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: "~ height l < h" + proof + assume 0: "height l < h" + have "size t = size l + (size r + 1)" by simp + also note size_height[of l] + also note size1_height[of r] + also have "(2::nat) ^ height l - 1 < 2 ^ h - 1" + using 0 by (simp add: diff_less_mono) + also have "(2::nat) ^ height r \<le> 2 ^ h" using 2 by simp + also have "(2::nat) ^ h - 1 + 2 ^ h = 2 ^ (Suc h) - 1" by (simp) + also have "\<dots> = size t" using Suc(2,3) by simp + finally show False by (simp add: diff_le_mono) + qed + have 4: "~ height r < h" + proof + assume 0: "height r < h" + have "size t = (size l + 1) + size r" by simp + also note size_height[of r] + also note size1_height[of l] + also have "(2::nat) ^ height r - 1 < 2 ^ h - 1" + using 0 by (simp add: diff_less_mono) + also have "(2::nat) ^ height l \<le> 2 ^ h" using 1 by simp + also have "(2::nat) ^ h + (2 ^ h - 1) = 2 ^ (Suc h) - 1" by (simp) + also have "\<dots> = size t" using Suc(2,3) by simp + finally show False by (simp add: diff_le_mono) + qed + from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+ + hence "size l = 2 ^ height l - 1" "size r = 2 ^ height r - 1" + using Suc(3) size_height[of l] size_height[of r] by (auto) + with * Suc(1) show ?case by simp +qed + +lemma complete_iff_size: "complete t \<longleftrightarrow> size t = 2 ^ height t - 1" +using complete_if_size size_if_complete by blast text\<open>A better lower bound for incomplete trees:\<close>