src/HOL/Data_Structures/AVL_Set.thy
 author nipkow Tue Jun 12 07:18:09 2018 +0200 (11 months ago) changeset 68422 0a3a36fa1d63 parent 68413 b56ed5010e69 child 68431 b294e095f64c permissions -rw-r--r--
proved avl for map (finally); tuned
```     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 l a h 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 l a h 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 l a (max (ht l) (ht r) + 1) 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 Leaf x 1 Leaf" |
```
```    56 "insert x (Node l a h r) = (case cmp x a of
```
```    57    EQ \<Rightarrow> Node l a h r |
```
```    58    LT \<Rightarrow> balL (insert x l) a r |
```
```    59    GT \<Rightarrow> balR l a (insert x r))"
```
```    60
```
```    61 fun split_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where
```
```    62 "split_max (Node l a _ r) =
```
```    63   (if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))"
```
```    64
```
```    65 lemmas split_max_induct = split_max.induct[case_names Node Leaf]
```
```    66
```
```    67 fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where
```
```    68 "del_root (Node Leaf a h r) = r" |
```
```    69 "del_root (Node l a h Leaf) = l" |
```
```    70 "del_root (Node l a h r) = (let (l', a') = split_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 l a h r) =
```
```    77   (case cmp x a of
```
```    78      EQ \<Rightarrow> del_root (Node l a h 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_split_maxD:
```
```   107   "\<lbrakk> split_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
```
```   108    inorder t' @ [a] = inorder t"
```
```   109 by(induction t arbitrary: t' rule: split_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 l a h r)) = inorder l @ inorder r"
```
```   114 by(cases "Node l a h r" rule: del_root.cases)
```
```   115   (auto simp: inorder_balL inorder_balR inorder_split_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_split_maxD split: prod.splits)
```
```   122
```
```   123
```
```   124 subsection \<open>AVL invariants\<close>
```
```   125
```
```   126 text\<open>Essentially the AFP/AVL proofs\<close>
```
```   127
```
```   128
```
```   129 subsubsection \<open>Insertion maintains AVL balance\<close>
```
```   130
```
```   131 declare Let_def [simp]
```
```   132
```
```   133 lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
```
```   134 by (induct t) simp_all
```
```   135
```
```   136 lemma height_balL:
```
```   137   "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
```
```   138    height (balL l a r) = height r + 2 \<or>
```
```   139    height (balL l a r) = height r + 3"
```
```   140 by (cases l) (auto simp:node_def balL_def split:tree.split)
```
```   141
```
```   142 lemma height_balR:
```
```   143   "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
```
```   144    height (balR l a r) = height l + 2 \<or>
```
```   145    height (balR l a r) = height l + 3"
```
```   146 by (cases r) (auto simp add:node_def balR_def split:tree.split)
```
```   147
```
```   148 lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
```
```   149 by (simp add: node_def)
```
```   150
```
```   151 lemma avl_node:
```
```   152   "\<lbrakk> avl l; avl r;
```
```   153      height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
```
```   154    \<rbrakk> \<Longrightarrow> avl(node l a r)"
```
```   155 by (auto simp add:max_def node_def)
```
```   156
```
```   157 lemma height_balL2:
```
```   158   "\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
```
```   159    height (balL l a r) = (1 + max (height l) (height r))"
```
```   160 by (cases l, cases r) (simp_all add: balL_def)
```
```   161
```
```   162 lemma height_balR2:
```
```   163   "\<lbrakk> avl l;  avl r;  height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
```
```   164    height (balR l a r) = (1 + max (height l) (height r))"
```
```   165 by (cases l, cases r) (simp_all add: balR_def)
```
```   166
```
```   167 lemma avl_balL:
```
```   168   assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
```
```   169     \<or> height r = height l + 1 \<or> height l = height r + 2"
```
```   170   shows "avl(balL l a r)"
```
```   171 proof(cases l)
```
```   172   case Leaf
```
```   173   with assms show ?thesis by (simp add: node_def balL_def)
```
```   174 next
```
```   175   case Node
```
```   176   with assms show ?thesis
```
```   177   proof(cases "height l = height r + 2")
```
```   178     case True
```
```   179     from True Node assms show ?thesis
```
```   180       by (auto simp: balL_def intro!: avl_node split: tree.split) arith+
```
```   181   next
```
```   182     case False
```
```   183     with assms show ?thesis by (simp add: avl_node balL_def)
```
```   184   qed
```
```   185 qed
```
```   186
```
```   187 lemma avl_balR:
```
```   188   assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
```
```   189     \<or> height r = height l + 1 \<or> height r = height l + 2"
```
```   190   shows "avl(balR l a r)"
```
```   191 proof(cases r)
```
```   192   case Leaf
```
```   193   with assms show ?thesis by (simp add: node_def balR_def)
```
```   194 next
```
```   195   case Node
```
```   196   with assms show ?thesis
```
```   197   proof(cases "height r = height l + 2")
```
```   198     case True
```
```   199       from True Node assms show ?thesis
```
```   200         by (auto simp: balR_def intro!: avl_node split: tree.split) arith+
```
```   201   next
```
```   202     case False
```
```   203     with assms show ?thesis by (simp add: balR_def avl_node)
```
```   204   qed
```
```   205 qed
```
```   206
```
```   207 (* It appears that these two properties need to be proved simultaneously: *)
```
```   208
```
```   209 text\<open>Insertion maintains the AVL property:\<close>
```
```   210
```
```   211 theorem avl_insert:
```
```   212   assumes "avl t"
```
```   213   shows "avl(insert x t)"
```
```   214         "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
```
```   215 using assms
```
```   216 proof (induction t)
```
```   217   case (Node l a h r)
```
```   218   case 1
```
```   219   show ?case
```
```   220   proof(cases "x = a")
```
```   221     case True with Node 1 show ?thesis by simp
```
```   222   next
```
```   223     case False
```
```   224     show ?thesis
```
```   225     proof(cases "x<a")
```
```   226       case True with Node 1 show ?thesis by (auto simp add:avl_balL)
```
```   227     next
```
```   228       case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
```
```   229     qed
```
```   230   qed
```
```   231   case 2
```
```   232   show ?case
```
```   233   proof(cases "x = a")
```
```   234     case True with Node 1 show ?thesis by simp
```
```   235   next
```
```   236     case False
```
```   237     show ?thesis
```
```   238     proof(cases "x<a")
```
```   239       case True
```
```   240       show ?thesis
```
```   241       proof(cases "height (insert x l) = height r + 2")
```
```   242         case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
```
```   243       next
```
```   244         case True
```
```   245         hence "(height (balL (insert x l) a r) = height r + 2) \<or>
```
```   246           (height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B")
```
```   247           using Node 2 by (intro height_balL) simp_all
```
```   248         thus ?thesis
```
```   249         proof
```
```   250           assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
```
```   251         next
```
```   252           assume ?B with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
```
```   253         qed
```
```   254       qed
```
```   255     next
```
```   256       case False
```
```   257       show ?thesis
```
```   258       proof(cases "height (insert x r) = height l + 2")
```
```   259         case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
```
```   260       next
```
```   261         case True
```
```   262         hence "(height (balR l a (insert x r)) = height l + 2) \<or>
```
```   263           (height (balR l a (insert x r)) = height l + 3)"  (is "?A \<or> ?B")
```
```   264           using Node 2 by (intro height_balR) simp_all
```
```   265         thus ?thesis
```
```   266         proof
```
```   267           assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
```
```   268         next
```
```   269           assume ?B with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
```
```   270         qed
```
```   271       qed
```
```   272     qed
```
```   273   qed
```
```   274 qed simp_all
```
```   275
```
```   276
```
```   277 subsubsection \<open>Deletion maintains AVL balance\<close>
```
```   278
```
```   279 lemma avl_split_max:
```
```   280   assumes "avl x" and "x \<noteq> Leaf"
```
```   281   shows "avl (fst (split_max x))" "height x = height(fst (split_max x)) \<or>
```
```   282          height x = height(fst (split_max x)) + 1"
```
```   283 using assms
```
```   284 proof (induct x rule: split_max_induct)
```
```   285   case (Node l a h r)
```
```   286   case 1
```
```   287   thus ?case using Node
```
```   288     by (auto simp: height_balL height_balL2 avl_balL split:prod.split)
```
```   289 next
```
```   290   case (Node l a h r)
```
```   291   case 2
```
```   292   let ?r' = "fst (split_max r)"
```
```   293   from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all
```
```   294   thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a]
```
```   295     apply (auto split:prod.splits simp del:avl.simps) by arith+
```
```   296 qed auto
```
```   297
```
```   298 lemma avl_del_root:
```
```   299   assumes "avl t" and "t \<noteq> Leaf"
```
```   300   shows "avl(del_root t)"
```
```   301 using assms
```
```   302 proof (cases t rule:del_root_cases)
```
```   303   case (Node_Node ll ln lh lr n h rl rn rh rr)
```
```   304   let ?l = "Node ll ln lh lr"
```
```   305   let ?r = "Node rl rn rh rr"
```
```   306   let ?l' = "fst (split_max ?l)"
```
```   307   from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
```
```   308   from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
```
```   309   hence "avl(?l')" "height ?l = height(?l') \<or>
```
```   310          height ?l = height(?l') + 1" by (rule avl_split_max,simp)+
```
```   311   with \<open>avl t\<close> Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1
```
```   312             \<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce
```
```   313   with \<open>avl ?l'\<close> \<open>avl ?r\<close> have "avl(balR ?l' (snd(split_max ?l)) ?r)"
```
```   314     by (rule avl_balR)
```
```   315   with Node_Node show ?thesis by (auto split:prod.splits)
```
```   316 qed simp_all
```
```   317
```
```   318 lemma height_del_root:
```
```   319   assumes "avl t" and "t \<noteq> Leaf"
```
```   320   shows "height t = height(del_root t) \<or> height t = height(del_root t) + 1"
```
```   321 using assms
```
```   322 proof (cases t rule: del_root_cases)
```
```   323   case (Node_Node ll ln lh lr n h rl rn rh rr)
```
```   324   let ?l = "Node ll ln lh lr"
```
```   325   let ?r = "Node rl rn rh rr"
```
```   326   let ?l' = "fst (split_max ?l)"
```
```   327   let ?t' = "balR ?l' (snd(split_max ?l)) ?r"
```
```   328   from \<open>avl t\<close> and Node_Node have "avl ?r" by simp
```
```   329   from \<open>avl t\<close> and Node_Node have "avl ?l" by simp
```
```   330   hence "avl(?l')"  by (rule avl_split_max,simp)
```
```   331   have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using \<open>avl ?l\<close> by (intro avl_split_max) auto
```
```   332   have t_height: "height t = 1 + max (height ?l) (height ?r)" using \<open>avl t\<close> Node_Node by simp
```
```   333   have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
```
```   334   proof(cases "height ?r = height ?l' + 2")
```
```   335     case False
```
```   336     show ?thesis using l'_height t_height False
```
```   337       by (subst height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
```
```   338   next
```
```   339     case True
```
```   340     show ?thesis
```
```   341     proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (split_max ?l)"]])
```
```   342       case 1 thus ?thesis using l'_height t_height True by arith
```
```   343     next
```
```   344       case 2 thus ?thesis using l'_height t_height True by arith
```
```   345     qed
```
```   346   qed
```
```   347   thus ?thesis using Node_Node by (auto split:prod.splits)
```
```   348 qed simp_all
```
```   349
```
```   350 text\<open>Deletion maintains the AVL property:\<close>
```
```   351
```
```   352 theorem avl_delete:
```
```   353   assumes "avl t"
```
```   354   shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
```
```   355 using assms
```
```   356 proof (induct t)
```
```   357   case (Node l n h r)
```
```   358   case 1
```
```   359   show ?case
```
```   360   proof(cases "x = n")
```
```   361     case True with Node 1 show ?thesis by (auto simp:avl_del_root)
```
```   362   next
```
```   363     case False
```
```   364     show ?thesis
```
```   365     proof(cases "x<n")
```
```   366       case True with Node 1 show ?thesis by (auto simp add:avl_balR)
```
```   367     next
```
```   368       case False with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
```
```   369     qed
```
```   370   qed
```
```   371   case 2
```
```   372   show ?case
```
```   373   proof(cases "x = n")
```
```   374     case True
```
```   375     with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
```
```   376       \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1"
```
```   377       by (subst height_del_root,simp_all)
```
```   378     with True show ?thesis by simp
```
```   379   next
```
```   380     case False
```
```   381     show ?thesis
```
```   382     proof(cases "x<n")
```
```   383       case True
```
```   384       show ?thesis
```
```   385       proof(cases "height r = height (delete x l) + 2")
```
```   386         case False with Node 1 \<open>x < n\<close> show ?thesis by(auto simp: balR_def)
```
```   387       next
```
```   388         case True
```
```   389         hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
```
```   390           height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
```
```   391           using Node 2 by (intro height_balR) auto
```
```   392         thus ?thesis
```
```   393         proof
```
```   394           assume ?A with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
```
```   395         next
```
```   396           assume ?B with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
```
```   397         qed
```
```   398       qed
```
```   399     next
```
```   400       case False
```
```   401       show ?thesis
```
```   402       proof(cases "height l = height (delete x r) + 2")
```
```   403         case False with Node 1 \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> show ?thesis by(auto simp: balL_def)
```
```   404       next
```
```   405         case True
```
```   406         hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
```
```   407           height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
```
```   408           using Node 2 by (intro height_balL) auto
```
```   409         thus ?thesis
```
```   410         proof
```
```   411           assume ?A with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
```
```   412         next
```
```   413           assume ?B with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
```
```   414         qed
```
```   415       qed
```
```   416     qed
```
```   417   qed
```
```   418 qed simp_all
```
```   419
```
```   420
```
```   421 subsection "Overall correctness"
```
```   422
```
```   423 interpretation Set_by_Ordered
```
```   424 where empty = Leaf and isin = isin and insert = insert and delete = delete
```
```   425 and inorder = inorder and inv = avl
```
```   426 proof (standard, goal_cases)
```
```   427   case 1 show ?case by simp
```
```   428 next
```
```   429   case 2 thus ?case by(simp add: isin_set_inorder)
```
```   430 next
```
```   431   case 3 thus ?case by(simp add: inorder_insert)
```
```   432 next
```
```   433   case 4 thus ?case by(simp add: inorder_delete)
```
```   434 next
```
```   435   case 5 thus ?case by simp
```
```   436 next
```
```   437   case 6 thus ?case by (simp add: avl_insert(1))
```
```   438 next
```
```   439   case 7 thus ?case by (simp add: avl_delete(1))
```
```   440 qed
```
```   441
```
```   442
```
```   443 subsection \<open>Height-Size Relation\<close>
```
```   444
```
```   445 text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
```
```   446
```
```   447 lemma height_invers:
```
```   448   "(height t = 0) = (t = Leaf)"
```
```   449   "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node l a (Suc h) r)"
```
```   450 by (induction t) auto
```
```   451
```
```   452 text \<open>Any AVL tree of height \<open>h\<close> has at least \<open>fib (h+2)\<close> leaves:\<close>
```
```   453
```
```   454 lemma avl_fib_bound: "avl t \<Longrightarrow> height t = h \<Longrightarrow> fib (h+2) \<le> size1 t"
```
```   455 proof (induction h arbitrary: t rule: fib.induct)
```
```   456   case 1 thus ?case by (simp add: height_invers)
```
```   457 next
```
```   458   case 2 thus ?case by (cases t) (auto simp: height_invers)
```
```   459 next
```
```   460   case (3 h)
```
```   461   from "3.prems" obtain l a r where
```
```   462     [simp]: "t = Node l a (Suc(Suc h)) r" "avl l" "avl r"
```
```   463     and C: "
```
```   464       height r = Suc h \<and> height l = Suc h
```
```   465     \<or> height r = Suc h \<and> height l = h
```
```   466     \<or> height r = h \<and> height l = Suc h" (is "?C1 \<or> ?C2 \<or> ?C3")
```
```   467     by (cases t) (simp, fastforce)
```
```   468   {
```
```   469     assume ?C1
```
```   470     with "3.IH"(1)
```
```   471     have "fib (h + 3) \<le> size1 l" "fib (h + 3) \<le> size1 r"
```
```   472       by (simp_all add: eval_nat_numeral)
```
```   473     hence ?case by (auto simp: eval_nat_numeral)
```
```   474   } moreover {
```
```   475     assume ?C2
```
```   476     hence ?case using "3.IH"(1)[of r] "3.IH"(2)[of l] by auto
```
```   477   } moreover {
```
```   478     assume ?C3
```
```   479     hence ?case using "3.IH"(1)[of l] "3.IH"(2)[of r] by auto
```
```   480   } ultimately show ?case using C by blast
```
```   481 qed
```
```   482
```
```   483 lemma fib_alt_induct [consumes 1, case_names 1 2 rec]:
```
```   484   assumes "n > 0" "P 1" "P 2" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))"
```
```   485   shows   "P n"
```
```   486   using assms(1)
```
```   487 proof (induction n rule: fib.induct)
```
```   488   case (3 n)
```
```   489   thus ?case using assms by (cases n) (auto simp: eval_nat_numeral)
```
```   490 qed (insert assms, auto)
```
```   491
```
```   492 text \<open>An exponential lower bound for @{const fib}:\<close>
```
```   493
```
```   494 lemma fib_lowerbound:
```
```   495   defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
```
```   496   defines "c \<equiv> 1 / \<phi> ^ 2"
```
```   497   assumes "n > 0"
```
```   498   shows   "real (fib n) \<ge> c * \<phi> ^ n"
```
```   499 proof -
```
```   500   have "\<phi> > 1" by (simp add: \<phi>_def)
```
```   501   hence "c > 0" by (simp add: c_def)
```
```   502   from \<open>n > 0\<close> show ?thesis
```
```   503   proof (induction n rule: fib_alt_induct)
```
```   504     case (rec n)
```
```   505     have "c * \<phi> ^ Suc (Suc n) = \<phi> ^ 2 * (c * \<phi> ^ n)"
```
```   506       by (simp add: field_simps power2_eq_square)
```
```   507     also have "\<dots> \<le> (\<phi> + 1) * (c * \<phi> ^ n)"
```
```   508       by (rule mult_right_mono) (insert \<open>c > 0\<close>, simp_all add: \<phi>_def power2_eq_square field_simps)
```
```   509     also have "\<dots> = c * \<phi> ^ Suc n + c * \<phi> ^ n"
```
```   510       by (simp add: field_simps)
```
```   511     also have "\<dots> \<le> real (fib (Suc n)) + real (fib n)"
```
```   512       by (intro add_mono rec.IH)
```
```   513     finally show ?case by simp
```
```   514   qed (insert \<open>\<phi> > 1\<close>, simp_all add: c_def power2_eq_square eval_nat_numeral)
```
```   515 qed
```
```   516
```
```   517 text \<open>The size of an AVL tree is (at least) exponential in its height:\<close>
```
```   518
```
```   519 lemma avl_size_lowerbound:
```
```   520   defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
```
```   521   assumes "avl t"
```
```   522   shows   "\<phi> ^ (height t) \<le> size1 t"
```
```   523 proof -
```
```   524   have "\<phi> > 0" by(simp add: \<phi>_def add_pos_nonneg)
```
```   525   hence "\<phi> ^ height t = (1 / \<phi> ^ 2) * \<phi> ^ (height t + 2)"
```
```   526     by(simp add: field_simps power2_eq_square)
```
```   527   also have "\<dots> \<le> fib (height t + 2)"
```
```   528     using fib_lowerbound[of "height t + 2"] by(simp add: \<phi>_def)
```
```   529   also have "\<dots> \<le> size1 t"
```
```   530     using avl_fib_bound[of t "height t"] assms by simp
```
```   531   finally show ?thesis .
```
```   532 qed
```
```   533
```
```   534 text \<open>The height of an AVL tree is most @{term "(1/log 2 \<phi>)"} \<open>\<approx> 1.44\<close> times worse
```
```   535 than @{term "log 2 (size1 t)"}:\<close>
```
```   536
```
```   537 lemma  avl_height_upperbound:
```
```   538   defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
```
```   539   assumes "avl t"
```
```   540   shows   "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)"
```
```   541 proof -
```
```   542   have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict)
```
```   543   hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power)
```
```   544   also have "\<dots> \<le> log \<phi> (size1 t)"
```
```   545     using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>  by simp
```
```   546   also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)"
```
```   547     by(simp add: log_base_change[of 2 \<phi>])
```
```   548   finally show ?thesis .
```
```   549 qed
```
```   550
```
```   551 end
```