src/HOL/Data_Structures/AVL_Set.thy
changeset 63411 e051eea34990
parent 62526 347150095fd2
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Jul 07 09:24:03 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Jul 07 18:08:02 2016 +0200
     1.3 @@ -1,12 +1,15 @@
     1.4  (*
     1.5 -Author:     Tobias Nipkow
     1.6 -Derived from AFP entry AVL.
     1.7 +Author:     Tobias Nipkow, Daniel Stüwe
     1.8 +Largely derived from AFP entry AVL.
     1.9  *)
    1.10  
    1.11  section "AVL Tree Implementation of Sets"
    1.12  
    1.13  theory AVL_Set
    1.14 -imports Cmp Isin2
    1.15 +imports
    1.16 + Cmp
    1.17 + Isin2
    1.18 +  "~~/src/HOL/Number_Theory/Fib"
    1.19  begin
    1.20  
    1.21  type_synonym 'a avl_tree = "('a,nat) tree"
    1.22 @@ -48,7 +51,7 @@
    1.23            else node (node l a bl) b br
    1.24    else node l a r)"
    1.25  
    1.26 -fun insert :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.27 +fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.28  "insert x Leaf = Node 1 Leaf x Leaf" |
    1.29  "insert x (Node h l a r) = (case cmp x a of
    1.30     EQ \<Rightarrow> Node h l a r |
    1.31 @@ -68,7 +71,7 @@
    1.32  
    1.33  lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node]
    1.34  
    1.35 -fun delete :: "'a::cmp \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.36 +fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
    1.37  "delete _ Leaf = Leaf" |
    1.38  "delete x (Node h l a r) =
    1.39    (case cmp x a of
    1.40 @@ -449,4 +452,83 @@
    1.41    qed
    1.42  qed simp_all
    1.43  
    1.44 +
    1.45 +subsection \<open>Height-Size Relation\<close>
    1.46 +
    1.47 +text \<open>By Daniel St\"uwe\<close>
    1.48 +
    1.49 +fun fib_tree :: "nat \<Rightarrow> unit avl_tree" where
    1.50 +"fib_tree 0 = Leaf" |
    1.51 +"fib_tree (Suc 0) = Node 1 Leaf () Leaf" |
    1.52 +"fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)"
    1.53 +
    1.54 +lemma [simp]: "ht (fib_tree h) = h"
    1.55 +by (induction h rule: "fib_tree.induct") auto
    1.56 +
    1.57 +lemma [simp]: "height (fib_tree h) = h"
    1.58 +by (induction h rule: "fib_tree.induct") auto
    1.59 +
    1.60 +lemma "avl(fib_tree h)"          
    1.61 +by (induction h rule: "fib_tree.induct") auto
    1.62 +
    1.63 +lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)"
    1.64 +by (induction h rule: fib_tree.induct) auto
    1.65 +
    1.66 +lemma height_invers[simp]: 
    1.67 +  "(height t = 0) = (t = Leaf)"
    1.68 +  "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
    1.69 +by (induction t) auto
    1.70 +
    1.71 +lemma fib_Suc_lt: "fib n \<le> fib (Suc n)"
    1.72 +by (induction n rule: fib.induct) auto
    1.73 +
    1.74 +lemma fib_mono: "n \<le> m \<Longrightarrow> fib n \<le> fib m"
    1.75 +proof (induction n arbitrary: m rule: fib.induct )
    1.76 +  case (2 m)
    1.77 +  thus ?case using fib_neq_0_nat[of m] by auto
    1.78 +next
    1.79 +  case (3 n m)
    1.80 +  from 3 obtain m' where "m = Suc (Suc m')"
    1.81 +    by (metis le_Suc_ex plus_nat.simps(2)) 
    1.82 +  thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto
    1.83 +qed simp
    1.84 +
    1.85 +lemma size1_fib_tree_mono:
    1.86 +  assumes "n \<le> m"
    1.87 +  shows   "size1 (fib_tree n) \<le> size1 (fib_tree m)"
    1.88 +using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce 
    1.89 +
    1.90 +lemma fib_tree_minimal: "avl t \<Longrightarrow> size1 (fib_tree (ht t)) \<le> size1 t"
    1.91 +proof (induction "ht t" arbitrary: t rule: fib_tree.induct)
    1.92 +  case (2 t)
    1.93 +  from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto
    1.94 +  with 2 show ?case by auto
    1.95 +next
    1.96 +  case (3 h t)
    1.97 +  note [simp] = 3(3)[symmetric] 
    1.98 +  from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto
    1.99 +  show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"]) 
   1.100 +    case equal
   1.101 +    with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto
   1.102 +    with 3 have "size1 (fib_tree (ht l)) \<le> size1 l" by auto moreover
   1.103 +    from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \<le> size1 r" by auto ultimately
   1.104 +    show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto
   1.105 +  next
   1.106 +    case greater
   1.107 +    with 3(3,4) have ht: "ht l = Suc h"  "ht r = h" by auto
   1.108 +    from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \<le> size1 l" by auto moreover
   1.109 +    from ht 3(1,2,4) have "size1 (fib_tree h) \<le> size1 r" by auto ultimately
   1.110 +    show ?thesis by auto
   1.111 +  next
   1.112 +    case less (* analogously *)
   1.113 +    with 3 have ht: "ht l = h"  "Suc h = ht r" by auto
   1.114 +    from ht 3 have "size1 (fib_tree h) \<le> size1 l" by auto moreover
   1.115 +    from ht 3 have "size1 (fib_tree (Suc h)) \<le> size1 r" by auto ultimately
   1.116 +    show ?thesis by auto
   1.117 +  qed
   1.118 +qed auto
   1.119 +
   1.120 +theorem avl_size_bound: "avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t" 
   1.121 +using fib_tree_minimal fib_tree_size1 by fastforce
   1.122 +
   1.123  end