# HG changeset patch # User nipkow # Date 1527616910 -7200 # Node ID 56c57e91edf915fd7d4c5929521b79348ee5a840 # Parent e9b5f25f6712aaa9016cc85e43d2fbbbd6e98932 slicker proof diff -r e9b5f25f6712 -r 56c57e91edf9 src/HOL/Data_Structures/AVL_Set.thy --- a/src/HOL/Data_Structures/AVL_Set.thy Tue May 29 14:05:59 2018 +0200 +++ b/src/HOL/Data_Structures/AVL_Set.thy Tue May 29 20:01:50 2018 +0200 @@ -455,80 +455,93 @@ subsection \Height-Size Relation\ -text \By Daniel St\"uwe\ - -fun fib_tree :: "nat \ unit avl_tree" where -"fib_tree 0 = Leaf" | -"fib_tree (Suc 0) = Node 1 Leaf () Leaf" | -"fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)" - -lemma [simp]: "ht (fib_tree h) = h" -by (induction h rule: "fib_tree.induct") auto +text \By Daniel St\"uwe, Manuel Eberl and Peter Lammich.\ -lemma [simp]: "height (fib_tree h) = h" -by (induction h rule: "fib_tree.induct") auto - -lemma "avl(fib_tree h)" -by (induction h rule: "fib_tree.induct") auto - -lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)" -by (induction h rule: fib_tree.induct) auto - -lemma height_invers[simp]: +lemma height_invers: "(height t = 0) = (t = Leaf)" "avl t \ (height t = Suc h) = (\ l a r . t = Node (Suc h) l a r)" by (induction t) auto -lemma fib_Suc_lt: "fib n \ fib (Suc n)" -by (induction n rule: fib.induct) auto +text \Any AVL tree of height \h\ has at least \fib (h+2)\ leaves:\ -lemma fib_mono: "n \ m \ fib n \ fib m" -proof (induction n arbitrary: m rule: fib.induct ) - case (2 m) - thus ?case using fib_neq_0_nat[of m] by auto +lemma avl_fib_bound: "avl t \ height t = h \ fib (h+2) \ size1 t" +proof (induction h arbitrary: t rule: fib.induct) + case 1 thus ?case by (simp add: height_invers) next - case (3 n m) - from 3 obtain m' where "m = Suc (Suc m')" - by (metis le_Suc_ex plus_nat.simps(2)) - thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto -qed simp - -lemma size1_fib_tree_mono: - assumes "n \ m" - shows "size1 (fib_tree n) \ size1 (fib_tree m)" -using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce - -lemma fib_tree_minimal: "avl t \ size1 (fib_tree (ht t)) \ size1 t" -proof (induction "ht t" arbitrary: t rule: fib_tree.induct) - case (2 t) - from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto - with 2 show ?case by auto + case 2 thus ?case by (cases t) (auto simp: height_invers) next - case (3 h t) - note [simp] = 3(3)[symmetric] - from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto - show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"]) - case equal - with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto - with 3 have "size1 (fib_tree (ht l)) \ size1 l" by auto moreover - from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \ size1 r" by auto ultimately - show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto - next - case greater - with 3(3,4) have ht: "ht l = Suc h" "ht r = h" by auto - from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \ size1 l" by auto moreover - from ht 3(1,2,4) have "size1 (fib_tree h) \ size1 r" by auto ultimately - show ?thesis by auto - next - case less (* analogously *) - with 3 have ht: "ht l = h" "Suc h = ht r" by auto - from ht 3 have "size1 (fib_tree h) \ size1 l" by auto moreover - from ht 3 have "size1 (fib_tree (Suc h)) \ size1 r" by auto ultimately - show ?thesis by auto - qed -qed auto + case (3 h) + from "3.prems" obtain l a r where + [simp]: "t = Node (Suc(Suc h)) l a r" "avl l" "avl r" + and C: " + height r = Suc h \ height l = Suc h + \ height r = Suc h \ height l = h + \ height r = h \ height l = Suc h" (is "?C1 \ ?C2 \ ?C3") + by (cases t) (simp, fastforce) + { + assume ?C1 + with "3.IH"(1) + have "fib (h + 3) \ size1 l" "fib (h + 3) \ size1 r" + by (simp_all add: eval_nat_numeral) + hence ?case by (auto simp: eval_nat_numeral) + } moreover { + assume ?C2 + hence ?case using "3.IH"(1)[of r] "3.IH"(2)[of l] by auto + } moreover { + assume ?C3 + hence ?case using "3.IH"(1)[of l] "3.IH"(2)[of r] by auto + } ultimately show ?case using C by blast +qed + +lemma fib_alt_induct [consumes 1, case_names 1 2 rec]: + assumes "n > 0" "P 1" "P 2" "\n. n > 0 \ P n \ P (Suc n) \ P (Suc (Suc n))" + shows "P n" + using assms(1) +proof (induction n rule: fib.induct) + case (3 n) + thus ?case using assms by (cases n) (auto simp: eval_nat_numeral) +qed (insert assms, auto) + +text \An exponential lower bound for @{const fib}:\ -theorem avl_size_bound: "avl t \ fib(height t + 2) \ size1 t" -using fib_tree_minimal fib_tree_size1 by fastforce +lemma fib_lowerbound: + defines "\ \ (1 + sqrt 5) / 2" + defines "c \ 1 / \ ^ 2" + assumes "n > 0" + shows "real (fib n) \ c * \ ^ n" +proof - + have "\ > 1" by (simp add: \_def) + hence "c > 0" by (simp add: c_def) + from \n > 0\ show ?thesis + proof (induction n rule: fib_alt_induct) + case (rec n) + have "c * \ ^ Suc (Suc n) = \ ^ 2 * (c * \ ^ n)" + by (simp add: field_simps power2_eq_square) + also have "\ \ (\ + 1) * (c * \ ^ n)" + by (rule mult_right_mono) (insert \c > 0\, simp_all add: \_def power2_eq_square field_simps) + also have "\ = c * \ ^ Suc n + c * \ ^ n" + by (simp add: field_simps) + also have "\ \ real (fib (Suc n)) + real (fib n)" + by (intro add_mono rec.IH) + finally show ?case by simp + qed (insert \\ > 1\, simp_all add: c_def power2_eq_square eval_nat_numeral) +qed + +text \The size of an AVL tree is (at least) exponential in its height:\ + +lemma avl_lowerbound: + defines "\ \ (1 + sqrt 5) / 2" + assumes "avl t" + shows "real (size1 t) \ \ ^ (height t)" +proof - + have "\ > 0" by(simp add: \_def add_pos_nonneg) + hence "\ ^ height t = (1 / \ ^ 2) * \ ^ (height t + 2)" + by(simp add: field_simps power2_eq_square) + also have "\ \ real (fib (height t + 2))" + using fib_lowerbound[of "height t + 2"] by(simp add: \_def) + also have "\ \ real (size1 t)" + using avl_fib_bound[of t "height t"] assms by simp + finally show ?thesis . +qed end