diff -r 9789ccc2a477 -r def97df48390 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Jul 07 17:34:39 2016 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Jul 07 18:08:10 2016 +0200
@@ -1,12 +1,15 @@
 (*
-Author:     Tobias Nipkow
-Derived from AFP entry AVL.
+Author:     Tobias Nipkow, Daniel Stüwe
+Largely derived from AFP entry AVL.
 *)
 
 section "AVL Tree Implementation of Sets"
 
 theory AVL_Set
-imports Cmp Isin2
+imports
+ Cmp
+ Isin2
+  "~~/src/HOL/Number_Theory/Fib"
 begin
 
 type_synonym 'a avl_tree = "('a,nat) tree"
@@ -48,7 +51,7 @@
           else node (node l a bl) b br
   else node l a r)"
 
-fun insert :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
 "insert x Leaf = Node 1 Leaf x Leaf" |
 "insert x (Node h l a r) = (case cmp x a of
    EQ \<Rightarrow> Node h l a r |
@@ -68,7 +71,7 @@
 
 lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node]
 
-fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
+fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
 "delete _ Leaf = Leaf" |
 "delete x (Node h l a r) =
   (case cmp x a of
@@ -449,4 +452,83 @@
   qed
 qed simp_all
 
+
+subsection \<open>Height-Size Relation\<close>
+
+text \<open>By Daniel St\"uwe\<close>
+
+fun fib_tree :: "nat \<Rightarrow> 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
+
+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]: 
+  "(height t = 0) = (t = Leaf)"
+  "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
+by (induction t) auto
+
+lemma fib_Suc_lt: "fib n \<le> fib (Suc n)"
+by (induction n rule: fib.induct) auto
+
+lemma fib_mono: "n \<le> m \<Longrightarrow> fib n \<le> fib m"
+proof (induction n arbitrary: m rule: fib.induct )
+  case (2 m)
+  thus ?case using fib_neq_0_nat[of m] by auto
+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 \<le> m"
+  shows   "size1 (fib_tree n) \<le> 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 \<Longrightarrow> size1 (fib_tree (ht t)) \<le> 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
+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)) \<le> size1 l" by auto moreover
+    from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \<le> 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)) \<le> size1 l" by auto moreover
+    from ht 3(1,2,4) have "size1 (fib_tree h) \<le> 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) \<le> size1 l" by auto moreover
+    from ht 3 have "size1 (fib_tree (Suc h)) \<le> size1 r" by auto ultimately
+    show ?thesis by auto
+  qed
+qed auto
+
+theorem avl_size_bound: "avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t" 
+using fib_tree_minimal fib_tree_size1 by fastforce
+
 end