src/HOL/Data_Structures/AVL_Set.thy
 author nipkow Sun Apr 08 09:46:33 2018 +0200 (13 months ago) changeset 67964 08cc5ab18c84 parent 67406 23307fd33906 child 67967 5a4280946a25 permissions -rw-r--r--
better name; added binary operations
```     1 (*
```
```     2 Author:     Tobias Nipkow, Daniel Stüwe
```
```     3 Largely derived from AFP entry AVL.
```
```     4 *)
```
```     5
```
```     6 section "AVL Tree Implementation of Sets"
```
```     7
```
```     8 theory AVL_Set
```
```     9 imports
```
```    10   Cmp
```
```    11   Isin2
```
```    12   "HOL-Number_Theory.Fib"
```
```    13 begin
```
```    14
```
```    15 type_synonym 'a avl_tree = "('a,nat) tree"
```
```    16
```
```    17 text \<open>Invariant:\<close>
```
```    18
```
```    19 fun avl :: "'a avl_tree \<Rightarrow> bool" where
```
```    20 "avl Leaf = True" |
```
```    21 "avl (Node h l a r) =
```
```    22  ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and>
```
```    23   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
```
```    24
```
```    25 fun ht :: "'a avl_tree \<Rightarrow> nat" where
```
```    26 "ht Leaf = 0" |
```
```    27 "ht (Node h l a r) = h"
```
```    28
```
```    29 definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
```
```    30 "node l a r = Node (max (ht l) (ht r) + 1) l a r"
```
```    31
```
```    32 definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
```
```    33 "balL l a r =
```
```    34   (if ht l = ht r + 2 then
```
```    35      case l of
```
```    36        Node _ bl b br \<Rightarrow>
```
```    37          if ht bl < ht br then
```
```    38            case br of
```
```    39              Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r)
```
```    40          else node bl b (node br a r)
```
```    41    else node l a r)"
```
```    42
```
```    43 definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
```
```    44 "balR l a r =
```
```    45    (if ht r = ht l + 2 then
```
```    46       case r of
```
```    47         Node _ bl b br \<Rightarrow>
```
```    48           if ht bl > ht br then
```
```    49             case bl of
```
```    50               Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br)
```
```    51           else node (node l a bl) b br
```
```    52   else node l a r)"
```
```    53
```
```    54 fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
```
```    55 "insert x Leaf = Node 1 Leaf x Leaf" |
```
```    56 "insert x (Node h l a r) = (case cmp x a of
```
```    57    EQ \<Rightarrow> Node h l a r |
```
```    58    LT \<Rightarrow> balL (insert x l) a r |
```
```    59    GT \<Rightarrow> balR l a (insert x r))"
```
```    60
```
```    61 fun del_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
```
```    62 "del_max (Node _ l a r) =
```
```    63   (if r = Leaf then (l,a) else let (r',a') = del_max r in (balL l a r', a'))"
```
```    64
```
```    65 lemmas del_max_induct = del_max.induct[case_names Node Leaf]
```
```    66
```
```    67 fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
```
```    68 "del_root (Node h Leaf a r) = r" |
```
```    69 "del_root (Node h l a Leaf) = l" |
```
```    70 "del_root (Node h l a r) = (let (l', a') = del_max l in balR l' a' r)"
```
```    71
```
```    72 lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node]
```
```    73
```
```    74 fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where
```
```    75 "delete _ Leaf = Leaf" |
```
```    76 "delete x (Node h l a r) =
```
```    77   (case cmp x a of
```
```    78      EQ \<Rightarrow> del_root (Node h l a r) |
```
```    79      LT \<Rightarrow> balR (delete x l) a r |
```
```    80      GT \<Rightarrow> balL l a (delete x r))"
```
```    81
```
```    82
```
```    83 subsection \<open>Functional Correctness Proofs\<close>
```
```    84
```
```    85 text\<open>Very different from the AFP/AVL proofs\<close>
```
```    86
```
```    87
```
```    88 subsubsection "Proofs for insert"
```
```    89
```
```    90 lemma inorder_balL:
```
```    91   "inorder (balL l a r) = inorder l @ a # inorder r"
```
```    92 by (auto simp: node_def balL_def split:tree.splits)
```
```    93
```
```    94 lemma inorder_balR:
```
```    95   "inorder (balR l a r) = inorder l @ a # inorder r"
```
```    96 by (auto simp: node_def balR_def split:tree.splits)
```
```    97
```
```    98 theorem inorder_insert:
```
```    99   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
```
```   100 by (induct t)
```
```   101    (auto simp: ins_list_simps inorder_balL inorder_balR)
```
```   102
```
```   103
```
```   104 subsubsection "Proofs for delete"
```
```   105
```
```   106 lemma inorder_del_maxD:
```
```   107   "\<lbrakk> del_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
```
```   108    inorder t' @ [a] = inorder t"
```
```   109 by(induction t arbitrary: t' rule: del_max.induct)
```
```   110   (auto simp: inorder_balL split: if_splits prod.splits tree.split)
```
```   111
```
```   112 lemma inorder_del_root:
```
```   113   "inorder (del_root (Node h l a r)) = inorder l @ inorder r"
```
```   114 by(cases "Node h l a r" rule: del_root.cases)
```
```   115   (auto simp: inorder_balL inorder_balR inorder_del_maxD split: if_splits prod.splits)
```
```   116
```
```   117 theorem inorder_delete:
```
```   118   "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
```
```   119 by(induction t)
```
```   120   (auto simp: del_list_simps inorder_balL inorder_balR
```
```   121     inorder_del_root inorder_del_maxD split: prod.splits)
```
```   122
```
```   123
```
```   124 subsubsection "Overall functional correctness"
```
```   125
```
```   126 interpretation Set_by_Ordered
```
```   127 where empty = Leaf and isin = isin and insert = insert and delete = delete
```
```   128 and inorder = inorder and inv = "\<lambda>_. True"
```
```   129 proof (standard, goal_cases)
```
```   130   case 1 show ?case by simp
```
```   131 next
```
```   132   case 2 thus ?case by(simp add: isin_set)
```
```   133 next
```
```   134   case 3 thus ?case by(simp add: inorder_insert)
```
```   135 next
```
```   136   case 4 thus ?case by(simp add: inorder_delete)
```
```   137 qed (rule TrueI)+
```
```   138
```
```   139
```
```   140 subsection \<open>AVL invariants\<close>
```
```   141
```
```   142 text\<open>Essentially the AFP/AVL proofs\<close>
```
```   143
```
```   144
```
```   145 subsubsection \<open>Insertion maintains AVL balance\<close>
```
```   146
```
```   147 declare Let_def [simp]
```
```   148
```
```   149 lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
```
```   150 by (induct t) simp_all
```
```   151
```
```   152 lemma height_balL:
```
```   153   "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
```
```   154    height (balL l a r) = height r + 2 \<or>
```
```   155    height (balL l a r) = height r + 3"
```
```   156 by (cases l) (auto simp:node_def balL_def split:tree.split)
```
```   157
```
```   158 lemma height_balR:
```
```   159   "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
```
```   160    height (balR l a r) = height l + 2 \<or>
```
```   161    height (balR l a r) = height l + 3"
```
```   162 by (cases r) (auto simp add:node_def balR_def split:tree.split)
```
```   163
```
```   164 lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
```
```   165 by (simp add: node_def)
```
```   166
```
```   167 lemma avl_node:
```
```   168   "\<lbrakk> avl l; avl r;
```
```   169      height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
```
```   170    \<rbrakk> \<Longrightarrow> avl(node l a r)"
```
```   171 by (auto simp add:max_def node_def)
```
```   172
```
```   173 lemma height_balL2:
```
```   174   "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
```
```   175    height (balL l a r) = (1 + max (height l) (height r))"
```
```   176 by (cases l, cases r) (simp_all add: balL_def)
```
```   177
```
```   178 lemma height_balR2:
```
```   179   "\<lbrakk> avl l;  avl r;  height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
```
```   180    height (balR l a r) = (1 + max (height l) (height r))"
```
```   181 by (cases l, cases r) (simp_all add: balR_def)
```
```   182
```
```   183 lemma avl_balL:
```
```   184   assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
```
```   185     \<or> height r = height l + 1 \<or> height l = height r + 2"
```
```   186   shows "avl(balL l a r)"
```
```   187 proof(cases l)
```
```   188   case Leaf
```
```   189   with assms show ?thesis by (simp add: node_def balL_def)
```
```   190 next
```
```   191   case (Node ln ll lr lh)
```
```   192   with assms show ?thesis
```
```   193   proof(cases "height l = height r + 2")
```
```   194     case True
```
```   195     from True Node assms show ?thesis
```
```   196       by (auto simp: balL_def intro!: avl_node split: tree.split) arith+
```
```   197   next
```
```   198     case False
```
```   199     with assms show ?thesis by (simp add: avl_node balL_def)
```
```   200   qed
```
```   201 qed
```
```   202
```
```   203 lemma avl_balR:
```
```   204   assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
```
```   205     \<or> height r = height l + 1 \<or> height r = height l + 2"
```
```   206   shows "avl(balR l a r)"
```
```   207 proof(cases r)
```
```   208   case Leaf
```
```   209   with assms show ?thesis by (simp add: node_def balR_def)
```
```   210 next
```
```   211   case (Node rn rl rr rh)
```
```   212   with assms show ?thesis
```
```   213   proof(cases "height r = height l + 2")
```
```   214     case True
```
```   215       from True Node assms show ?thesis
```
```   216         by (auto simp: balR_def intro!: avl_node split: tree.split) arith+
```
```   217   next
```
```   218     case False
```
```   219     with assms show ?thesis by (simp add: balR_def avl_node)
```
```   220   qed
```
```   221 qed
```
```   222
```
```   223 (* It appears that these two properties need to be proved simultaneously: *)
```
```   224
```
```   225 text\<open>Insertion maintains the AVL property:\<close>
```
```   226
```
```   227 theorem avl_insert_aux:
```
```   228   assumes "avl t"
```
```   229   shows "avl(insert x t)"
```
```   230         "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
```
```   231 using assms
```
```   232 proof (induction t)
```
```   233   case (Node h l a r)
```
```   234   case 1
```
```   235   with Node show ?case
```
```   236   proof(cases "x = a")
```
```   237     case True
```
```   238     with Node 1 show ?thesis by simp
```
```   239   next
```
```   240     case False
```
```   241     with Node 1 show ?thesis
```
```   242     proof(cases "x<a")
```
```   243       case True
```
```   244       with Node 1 show ?thesis by (auto simp add:avl_balL)
```
```   245     next
```
```   246       case False
```
```   247       with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
```
```   248     qed
```
```   249   qed
```
```   250   case 2
```
```   251   from 2 Node show ?case
```
```   252   proof(cases "x = a")
```
```   253     case True
```
```   254     with Node 1 show ?thesis by simp
```
```   255   next
```
```   256     case False
```
```   257     with Node 1 show ?thesis
```
```   258      proof(cases "x<a")
```
```   259       case True
```
```   260       with Node 2 show ?thesis
```
```   261       proof(cases "height (insert x l) = height r + 2")
```
```   262         case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
```
```   263       next
```
```   264         case True
```
```   265         hence "(height (balL (insert x l) a r) = height r + 2) \<or>
```
```   266           (height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
```
```   267           using Node 2 by (intro height_balL) simp_all
```
```   268         thus ?thesis
```
```   269         proof
```
```   270           assume ?A
```
```   271           with 2 \<open>x < a\<close> show ?thesis by (auto)
```
```   272         next
```
```   273           assume ?B
```
```   274           with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
```
```   275         qed
```
```   276       qed
```
```   277     next
```
```   278       case False
```
```   279       with Node 2 show ?thesis
```
```   280       proof(cases "height (insert x r) = height l + 2")
```
```   281         case False
```
```   282         with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
```
```   283       next
```
```   284         case True
```
```   285         hence "(height (balR l a (insert x r)) = height l + 2) \<or>
```
```   286           (height (balR l a (insert x r)) = height l + 3)"  (is "?A \<or> ?B")
```
```   287           using Node 2 by (intro height_balR) simp_all
```
```   288         thus ?thesis
```
```   289         proof
```
```   290           assume ?A
```
```   291           with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
```
```   292         next
```
```   293           assume ?B
```
```   294           with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
```
```   295         qed
```
```   296       qed
```
```   297     qed
```
```   298   qed
```
```   299 qed simp_all
```
```   300
```
```   301
```
```   302 subsubsection \<open>Deletion maintains AVL balance\<close>
```
```   303
```
```   304 lemma avl_del_max:
```
```   305   assumes "avl x" and "x \<noteq> Leaf"
```
```   306   shows "avl (fst (del_max x))" "height x = height(fst (del_max x)) \<or>
```
```   307          height x = height(fst (del_max x)) + 1"
```
```   308 using assms
```
```   309 proof (induct x rule: del_max_induct)
```
```   310   case (Node h l a r)
```
```   311   case 1
```
```   312   thus ?case using Node
```
```   313     by (auto simp: height_balL height_balL2 avl_balL
```
```   314       linorder_class.max.absorb1 linorder_class.max.absorb2
```
```   315       split:prod.split)
```
```   316 next
```
```   317   case (Node h l a r)
```
```   318   case 2
```
```   319   let ?r' = "fst (del_max r)"
```
```   320   from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all
```
```   321   thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a]
```
```   322     apply (auto split:prod.splits simp del:avl.simps) by arith+
```
```   323 qed auto
```
```   324
```
```   325 lemma avl_del_root:
```
```   326   assumes "avl t" and "t \<noteq> Leaf"
```
```   327   shows "avl(del_root t)"
```
```   328 using assms
```
```   329 proof (cases t rule:del_root_cases)
```
```   330   case (Node_Node h lh ll ln lr n rh rl rn rr)
```
```   331   let ?l = "Node lh ll ln lr"
```
```   332   let ?r = "Node rh rl rn rr"
```
```   333   let ?l' = "fst (del_max ?l)"
```
```   334   from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
```
```   335   from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
```
```   336   hence "avl(?l')" "height ?l = height(?l') \<or>
```
```   337          height ?l = height(?l') + 1" by (rule avl_del_max,simp)+
```
```   338   with \<open>avl t\<close> Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
```
```   339             \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
```
```   340   with \<open>avl ?l'\<close> \<open>avl ?r\<close> have "avl(balR ?l' (snd(del_max ?l)) ?r)"
```
```   341     by (rule avl_balR)
```
```   342   with Node_Node show ?thesis by (auto split:prod.splits)
```
```   343 qed simp_all
```
```   344
```
```   345 lemma height_del_root:
```
```   346   assumes "avl t" and "t \<noteq> Leaf"
```
```   347   shows "height t = height(del_root t) \<or> height t = height(del_root t) + 1"
```
```   348 using assms
```
```   349 proof (cases t rule: del_root_cases)
```
```   350   case (Node_Node h lh ll ln lr n rh rl rn rr)
```
```   351   let ?l = "Node lh ll ln lr"
```
```   352   let ?r = "Node rh rl rn rr"
```
```   353   let ?l' = "fst (del_max ?l)"
```
```   354   let ?t' = "balR ?l' (snd(del_max ?l)) ?r"
```
```   355   from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
```
```   356   from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
```
```   357   hence "avl(?l')"  by (rule avl_del_max,simp)
```
```   358   have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using \<open>avl ?l\<close> by (intro avl_del_max) auto
```
```   359   have t_height: "height t = 1 + max (height ?l) (height ?r)" using \<open>avl t\<close> Node_Node by simp
```
```   360   have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
```
```   361   proof(cases "height ?r = height ?l' + 2")
```
```   362     case False
```
```   363     show ?thesis using l'_height t_height False by (subst  height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
```
```   364   next
```
```   365     case True
```
```   366     show ?thesis
```
```   367     proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (del_max ?l)"]])
```
```   368       case 1
```
```   369       thus ?thesis using l'_height t_height True by arith
```
```   370     next
```
```   371       case 2
```
```   372       thus ?thesis using l'_height t_height True by arith
```
```   373     qed
```
```   374   qed
```
```   375   thus ?thesis using Node_Node by (auto split:prod.splits)
```
```   376 qed simp_all
```
```   377
```
```   378 text\<open>Deletion maintains the AVL property:\<close>
```
```   379
```
```   380 theorem avl_delete_aux:
```
```   381   assumes "avl t"
```
```   382   shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
```
```   383 using assms
```
```   384 proof (induct t)
```
```   385   case (Node h l n r)
```
```   386   case 1
```
```   387   with Node show ?case
```
```   388   proof(cases "x = n")
```
```   389     case True
```
```   390     with Node 1 show ?thesis by (auto simp:avl_del_root)
```
```   391   next
```
```   392     case False
```
```   393     with Node 1 show ?thesis
```
```   394     proof(cases "x<n")
```
```   395       case True
```
```   396       with Node 1 show ?thesis by (auto simp add:avl_balR)
```
```   397     next
```
```   398       case False
```
```   399       with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
```
```   400     qed
```
```   401   qed
```
```   402   case 2
```
```   403   with Node show ?case
```
```   404   proof(cases "x = n")
```
```   405     case True
```
```   406     with 1 have "height (Node h l n r) = height(del_root (Node h l n r))
```
```   407       \<or> height (Node h l n r) = height(del_root (Node h l n r)) + 1"
```
```   408       by (subst height_del_root,simp_all)
```
```   409     with True show ?thesis by simp
```
```   410   next
```
```   411     case False
```
```   412     with Node 1 show ?thesis
```
```   413      proof(cases "x<n")
```
```   414       case True
```
```   415       show ?thesis
```
```   416       proof(cases "height r = height (delete x l) + 2")
```
```   417         case False with Node 1 \<open>x < n\<close> show ?thesis by(auto simp: balR_def)
```
```   418       next
```
```   419         case True
```
```   420         hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
```
```   421           height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
```
```   422           using Node 2 by (intro height_balR) auto
```
```   423         thus ?thesis
```
```   424         proof
```
```   425           assume ?A
```
```   426           with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
```
```   427         next
```
```   428           assume ?B
```
```   429           with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
```
```   430         qed
```
```   431       qed
```
```   432     next
```
```   433       case False
```
```   434       show ?thesis
```
```   435       proof(cases "height l = height (delete x r) + 2")
```
```   436         case False with Node 1 \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> show ?thesis by(auto simp: balL_def)
```
```   437       next
```
```   438         case True
```
```   439         hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
```
```   440           height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
```
```   441           using Node 2 by (intro height_balL) auto
```
```   442         thus ?thesis
```
```   443         proof
```
```   444           assume ?A
```
```   445           with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
```
```   446         next
```
```   447           assume ?B
```
```   448           with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
```
```   449         qed
```
```   450       qed
```
```   451     qed
```
```   452   qed
```
```   453 qed simp_all
```
```   454
```
```   455
```
```   456 subsection \<open>Height-Size Relation\<close>
```
```   457
```
```   458 text \<open>By Daniel St\"uwe\<close>
```
```   459
```
```   460 fun fib_tree :: "nat \<Rightarrow> unit avl_tree" where
```
```   461 "fib_tree 0 = Leaf" |
```
```   462 "fib_tree (Suc 0) = Node 1 Leaf () Leaf" |
```
```   463 "fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)"
```
```   464
```
```   465 lemma [simp]: "ht (fib_tree h) = h"
```
```   466 by (induction h rule: "fib_tree.induct") auto
```
```   467
```
```   468 lemma [simp]: "height (fib_tree h) = h"
```
```   469 by (induction h rule: "fib_tree.induct") auto
```
```   470
```
```   471 lemma "avl(fib_tree h)"
```
```   472 by (induction h rule: "fib_tree.induct") auto
```
```   473
```
```   474 lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)"
```
```   475 by (induction h rule: fib_tree.induct) auto
```
```   476
```
```   477 lemma height_invers[simp]:
```
```   478   "(height t = 0) = (t = Leaf)"
```
```   479   "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
```
```   480 by (induction t) auto
```
```   481
```
```   482 lemma fib_Suc_lt: "fib n \<le> fib (Suc n)"
```
```   483 by (induction n rule: fib.induct) auto
```
```   484
```
```   485 lemma fib_mono: "n \<le> m \<Longrightarrow> fib n \<le> fib m"
```
```   486 proof (induction n arbitrary: m rule: fib.induct )
```
```   487   case (2 m)
```
```   488   thus ?case using fib_neq_0_nat[of m] by auto
```
```   489 next
```
```   490   case (3 n m)
```
```   491   from 3 obtain m' where "m = Suc (Suc m')"
```
```   492     by (metis le_Suc_ex plus_nat.simps(2))
```
```   493   thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto
```
```   494 qed simp
```
```   495
```
```   496 lemma size1_fib_tree_mono:
```
```   497   assumes "n \<le> m"
```
```   498   shows   "size1 (fib_tree n) \<le> size1 (fib_tree m)"
```
```   499 using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce
```
```   500
```
```   501 lemma fib_tree_minimal: "avl t \<Longrightarrow> size1 (fib_tree (ht t)) \<le> size1 t"
```
```   502 proof (induction "ht t" arbitrary: t rule: fib_tree.induct)
```
```   503   case (2 t)
```
```   504   from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto
```
```   505   with 2 show ?case by auto
```
```   506 next
```
```   507   case (3 h t)
```
```   508   note [simp] = 3(3)[symmetric]
```
```   509   from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto
```
```   510   show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"])
```
```   511     case equal
```
```   512     with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto
```
```   513     with 3 have "size1 (fib_tree (ht l)) \<le> size1 l" by auto moreover
```
```   514     from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \<le> size1 r" by auto ultimately
```
```   515     show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto
```
```   516   next
```
```   517     case greater
```
```   518     with 3(3,4) have ht: "ht l = Suc h"  "ht r = h" by auto
```
```   519     from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \<le> size1 l" by auto moreover
```
```   520     from ht 3(1,2,4) have "size1 (fib_tree h) \<le> size1 r" by auto ultimately
```
```   521     show ?thesis by auto
```
```   522   next
```
```   523     case less (* analogously *)
```
```   524     with 3 have ht: "ht l = h"  "Suc h = ht r" by auto
```
```   525     from ht 3 have "size1 (fib_tree h) \<le> size1 l" by auto moreover
```
```   526     from ht 3 have "size1 (fib_tree (Suc h)) \<le> size1 r" by auto ultimately
```
```   527     show ?thesis by auto
```
```   528   qed
```
```   529 qed auto
```
```   530
```
```   531 theorem avl_size_bound: "avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t"
```
```   532 using fib_tree_minimal fib_tree_size1 by fastforce
```
```   533
```
```   534 end
```