src/HOL/Data_Structures/Brother12_Set.thy
 author nipkow Sat Apr 21 08:41:42 2018 +0200 (14 months ago) changeset 68020 6aade817bee5 parent 67965 aaa31cd0caef child 68431 b294e095f64c permissions -rw-r--r--
del_min -> split_min
```     1 (* Author: Tobias Nipkow, Daniel StÃ¼we *)
```
```     2
```
```     3 section \<open>1-2 Brother Tree Implementation of Sets\<close>
```
```     4
```
```     5 theory Brother12_Set
```
```     6 imports
```
```     7   Cmp
```
```     8   Set_Specs
```
```     9   "HOL-Number_Theory.Fib"
```
```    10 begin
```
```    11
```
```    12 subsection \<open>Data Type and Operations\<close>
```
```    13
```
```    14 datatype 'a bro =
```
```    15   N0 |
```
```    16   N1 "'a bro" |
```
```    17   N2 "'a bro" 'a "'a bro" |
```
```    18   (* auxiliary constructors: *)
```
```    19   L2 'a |
```
```    20   N3 "'a bro" 'a "'a bro" 'a "'a bro"
```
```    21
```
```    22 fun inorder :: "'a bro \<Rightarrow> 'a list" where
```
```    23 "inorder N0 = []" |
```
```    24 "inorder (N1 t) = inorder t" |
```
```    25 "inorder (N2 l a r) = inorder l @ a # inorder r" |
```
```    26 "inorder (L2 a) = [a]" |
```
```    27 "inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
```
```    28
```
```    29 fun isin :: "'a bro \<Rightarrow> 'a::linorder \<Rightarrow> bool" where
```
```    30 "isin N0 x = False" |
```
```    31 "isin (N1 t) x = isin t x" |
```
```    32 "isin (N2 l a r) x =
```
```    33   (case cmp x a of
```
```    34      LT \<Rightarrow> isin l x |
```
```    35      EQ \<Rightarrow> True |
```
```    36      GT \<Rightarrow> isin r x)"
```
```    37
```
```    38 fun n1 :: "'a bro \<Rightarrow> 'a bro" where
```
```    39 "n1 (L2 a) = N2 N0 a N0" |
```
```    40 "n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
```
```    41 "n1 t = N1 t"
```
```    42
```
```    43 hide_const (open) insert
```
```    44
```
```    45 locale insert
```
```    46 begin
```
```    47
```
```    48 fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
```
```    49 "n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
```
```    50 "n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
```
```    51 "n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
```
```    52 "n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
```
```    53 "n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
```
```    54 "n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
```
```    55 "n2 t1 a t2 = N2 t1 a t2"
```
```    56
```
```    57 fun ins :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
```
```    58 "ins x N0 = L2 x" |
```
```    59 "ins x (N1 t) = n1 (ins x t)" |
```
```    60 "ins x (N2 l a r) =
```
```    61   (case cmp x a of
```
```    62      LT \<Rightarrow> n2 (ins x l) a r |
```
```    63      EQ \<Rightarrow> N2 l a r |
```
```    64      GT \<Rightarrow> n2 l a (ins x r))"
```
```    65
```
```    66 fun tree :: "'a bro \<Rightarrow> 'a bro" where
```
```    67 "tree (L2 a) = N2 N0 a N0" |
```
```    68 "tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
```
```    69 "tree t = t"
```
```    70
```
```    71 definition insert :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
```
```    72 "insert x t = tree(ins x t)"
```
```    73
```
```    74 end
```
```    75
```
```    76 locale delete
```
```    77 begin
```
```    78
```
```    79 fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
```
```    80 "n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
```
```    81 "n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
```
```    82   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
```
```    83 "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
```
```    84   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
```
```    85 "n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
```
```    86   N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" |
```
```    87 "n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
```
```    88   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
```
```    89 "n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
```
```    90   N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
```
```    91 "n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
```
```    92   N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
```
```    93 "n2 t1 a1 t2 = N2 t1 a1 t2"
```
```    94
```
```    95 fun split_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
```
```    96 "split_min N0 = None" |
```
```    97 "split_min (N1 t) =
```
```    98   (case split_min t of
```
```    99      None \<Rightarrow> None |
```
```   100      Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
```
```   101 "split_min (N2 t1 a t2) =
```
```   102   (case split_min t1 of
```
```   103      None \<Rightarrow> Some (a, N1 t2) |
```
```   104      Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
```
```   105
```
```   106 fun del :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
```
```   107 "del _ N0         = N0" |
```
```   108 "del x (N1 t)     = N1 (del x t)" |
```
```   109 "del x (N2 l a r) =
```
```   110   (case cmp x a of
```
```   111      LT \<Rightarrow> n2 (del x l) a r |
```
```   112      GT \<Rightarrow> n2 l a (del x r) |
```
```   113      EQ \<Rightarrow> (case split_min r of
```
```   114               None \<Rightarrow> N1 l |
```
```   115               Some (b, r') \<Rightarrow> n2 l b r'))"
```
```   116
```
```   117 fun tree :: "'a bro \<Rightarrow> 'a bro" where
```
```   118 "tree (N1 t) = t" |
```
```   119 "tree t = t"
```
```   120
```
```   121 definition delete :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
```
```   122 "delete a t = tree (del a t)"
```
```   123
```
```   124 end
```
```   125
```
```   126 subsection \<open>Invariants\<close>
```
```   127
```
```   128 fun B :: "nat \<Rightarrow> 'a bro set"
```
```   129 and U :: "nat \<Rightarrow> 'a bro set" where
```
```   130 "B 0 = {N0}" |
```
```   131 "B (Suc h) = { N2 t1 a t2 | t1 a t2.
```
```   132   t1 \<in> B h \<union> U h \<and> t2 \<in> B h \<or> t1 \<in> B h \<and> t2 \<in> B h \<union> U h}" |
```
```   133 "U 0 = {}" |
```
```   134 "U (Suc h) = N1 ` B h"
```
```   135
```
```   136 abbreviation "T h \<equiv> B h \<union> U h"
```
```   137
```
```   138 fun Bp :: "nat \<Rightarrow> 'a bro set" where
```
```   139 "Bp 0 = B 0 \<union> L2 ` UNIV" |
```
```   140 "Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" |
```
```   141 "Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union>
```
```   142   {N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \<in> B (Suc h) \<and> t2 \<in> U (Suc h) \<and> t3 \<in> B (Suc h)}"
```
```   143
```
```   144 fun Um :: "nat \<Rightarrow> 'a bro set" where
```
```   145 "Um 0 = {}" |
```
```   146 "Um (Suc h) = N1 ` T h"
```
```   147
```
```   148
```
```   149 subsection "Functional Correctness Proofs"
```
```   150
```
```   151 subsubsection "Proofs for isin"
```
```   152
```
```   153 lemma isin_set:
```
```   154   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))"
```
```   155 by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+
```
```   156
```
```   157 subsubsection "Proofs for insertion"
```
```   158
```
```   159 lemma inorder_n1: "inorder(n1 t) = inorder t"
```
```   160 by(cases t rule: n1.cases) (auto simp: sorted_lems)
```
```   161
```
```   162 context insert
```
```   163 begin
```
```   164
```
```   165 lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
```
```   166 by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
```
```   167
```
```   168 lemma inorder_tree: "inorder(tree t) = inorder t"
```
```   169 by(cases t) auto
```
```   170
```
```   171 lemma inorder_ins: "t \<in> T h \<Longrightarrow>
```
```   172   sorted(inorder t) \<Longrightarrow> inorder(ins a t) = ins_list a (inorder t)"
```
```   173 by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
```
```   174
```
```   175 lemma inorder_insert: "t \<in> T h \<Longrightarrow>
```
```   176   sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
```
```   177 by(simp add: insert_def inorder_ins inorder_tree)
```
```   178
```
```   179 end
```
```   180
```
```   181 subsubsection \<open>Proofs for deletion\<close>
```
```   182
```
```   183 context delete
```
```   184 begin
```
```   185
```
```   186 lemma inorder_tree: "inorder(tree t) = inorder t"
```
```   187 by(cases t) auto
```
```   188
```
```   189 lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
```
```   190 by(cases "(l,a,r)" rule: n2.cases) (auto)
```
```   191
```
```   192 lemma inorder_split_min:
```
```   193   "t \<in> T h \<Longrightarrow> (split_min t = None \<longleftrightarrow> inorder t = []) \<and>
```
```   194   (split_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
```
```   195 by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
```
```   196
```
```   197 lemma inorder_del:
```
```   198   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
```
```   199 by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
```
```   200      inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
```
```   201
```
```   202 lemma inorder_delete:
```
```   203   "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
```
```   204 by(simp add: delete_def inorder_del inorder_tree)
```
```   205
```
```   206 end
```
```   207
```
```   208
```
```   209 subsection \<open>Invariant Proofs\<close>
```
```   210
```
```   211 subsubsection \<open>Proofs for insertion\<close>
```
```   212
```
```   213 lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)"
```
```   214 by(cases h rule: Bp.cases) auto
```
```   215
```
```   216 context insert
```
```   217 begin
```
```   218
```
```   219 lemma tree_type: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)"
```
```   220 by(cases h rule: Bp.cases) auto
```
```   221
```
```   222 lemma n2_type:
```
```   223   "(t1 \<in> Bp h \<and> t2 \<in> T h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h)) \<and>
```
```   224    (t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))"
```
```   225 apply(cases h rule: Bp.cases)
```
```   226 apply (auto)[2]
```
```   227 apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
```
```   228 done
```
```   229
```
```   230 lemma Bp_if_B: "t \<in> B h \<Longrightarrow> t \<in> Bp h"
```
```   231 by (cases h rule: Bp.cases) simp_all
```
```   232
```
```   233 text\<open>An automatic proof:\<close>
```
```   234
```
```   235 lemma
```
```   236   "(t \<in> B h \<longrightarrow> ins x t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> ins x t \<in> T h)"
```
```   237 apply(induction h arbitrary: t)
```
```   238  apply (simp)
```
```   239 apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
```
```   240 done
```
```   241
```
```   242 text\<open>A detailed proof:\<close>
```
```   243
```
```   244 lemma ins_type:
```
```   245 shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h"
```
```   246 proof(induction h arbitrary: t)
```
```   247   case 0
```
```   248   { case 1 thus ?case by simp
```
```   249   next
```
```   250     case 2 thus ?case by simp }
```
```   251 next
```
```   252   case (Suc h)
```
```   253   { case 1
```
```   254     then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
```
```   255       t1: "t1 \<in> T h" and t2: "t2 \<in> T h" and t12: "t1 \<in> B h \<or> t2 \<in> B h"
```
```   256       by auto
```
```   257     have ?case if "x < a"
```
```   258     proof -
```
```   259       have "n2 (ins x t1) a t2 \<in> Bp (Suc h)"
```
```   260       proof cases
```
```   261         assume "t1 \<in> B h"
```
```   262         with t2 show ?thesis by (simp add: Suc.IH(1) n2_type)
```
```   263       next
```
```   264         assume "t1 \<notin> B h"
```
```   265         hence 1: "t1 \<in> U h" and 2: "t2 \<in> B h" using t1 t12 by auto
```
```   266         show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type)
```
```   267       qed
```
```   268       with \<open>x < a\<close> show ?case by simp
```
```   269     qed
```
```   270     moreover
```
```   271     have ?case if "a < x"
```
```   272     proof -
```
```   273       have "n2 t1 a (ins x t2) \<in> Bp (Suc h)"
```
```   274       proof cases
```
```   275         assume "t2 \<in> B h"
```
```   276         with t1 show ?thesis by (simp add: Suc.IH(1) n2_type)
```
```   277       next
```
```   278         assume "t2 \<notin> B h"
```
```   279         hence 1: "t1 \<in> B h" and 2: "t2 \<in> U h" using t2 t12 by auto
```
```   280         show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type)
```
```   281       qed
```
```   282       with \<open>a < x\<close> show ?case by simp
```
```   283     qed
```
```   284     moreover
```
```   285     have ?case if "x = a"
```
```   286     proof -
```
```   287       from 1 have "t \<in> Bp (Suc h)" by(rule Bp_if_B)
```
```   288       thus "?case" using \<open>x = a\<close> by simp
```
```   289     qed
```
```   290     ultimately show ?case by auto
```
```   291   next
```
```   292     case 2 thus ?case using Suc(1) n1_type by fastforce }
```
```   293 qed
```
```   294
```
```   295 lemma insert_type:
```
```   296   "t \<in> B h \<Longrightarrow> insert x t \<in> B h \<union> B (Suc h)"
```
```   297 unfolding insert_def by (metis ins_type(1) tree_type)
```
```   298
```
```   299 end
```
```   300
```
```   301 subsubsection "Proofs for deletion"
```
```   302
```
```   303 lemma B_simps[simp]:
```
```   304   "N1 t \<in> B h = False"
```
```   305   "L2 y \<in> B h = False"
```
```   306   "(N3 t1 a1 t2 a2 t3) \<in> B h = False"
```
```   307   "N0 \<in> B h \<longleftrightarrow> h = 0"
```
```   308 by (cases h, auto)+
```
```   309
```
```   310 context delete
```
```   311 begin
```
```   312
```
```   313 lemma n2_type1:
```
```   314   "\<lbrakk>t1 \<in> Um h; t2 \<in> B h\<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
```
```   315 apply(cases h rule: Bp.cases)
```
```   316 apply auto[2]
```
```   317 apply(erule exE bexE conjE imageE | simp | erule disjE)+
```
```   318 done
```
```   319
```
```   320 lemma n2_type2:
```
```   321   "\<lbrakk>t1 \<in> B h ; t2 \<in> Um h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
```
```   322 apply(cases h rule: Bp.cases)
```
```   323 apply auto[2]
```
```   324 apply(erule exE bexE conjE imageE | simp | erule disjE)+
```
```   325 done
```
```   326
```
```   327 lemma n2_type3:
```
```   328   "\<lbrakk>t1 \<in> T h ; t2 \<in> T h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
```
```   329 apply(cases h rule: Bp.cases)
```
```   330 apply auto[2]
```
```   331 apply(erule exE bexE conjE imageE | simp | erule disjE)+
```
```   332 done
```
```   333
```
```   334 lemma split_minNoneN0: "\<lbrakk>t \<in> B h; split_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
```
```   335 by (cases t) (auto split: option.splits)
```
```   336
```
```   337 lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
```
```   338 by (cases h) (auto simp: split_minNoneN0  split: option.splits)
```
```   339
```
```   340 lemma split_min_type:
```
```   341   "t \<in> B h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
```
```   342   "t \<in> U h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
```
```   343 proof (induction h arbitrary: t a t')
```
```   344   case (Suc h)
```
```   345   { case 1
```
```   346     then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
```
```   347       t12: "t1 \<in> T h" "t2 \<in> T h" "t1 \<in> B h \<or> t2 \<in> B h"
```
```   348       by auto
```
```   349     show ?case
```
```   350     proof (cases "split_min t1")
```
```   351       case None
```
```   352       show ?thesis
```
```   353       proof cases
```
```   354         assume "t1 \<in> B h"
```
```   355         with split_minNoneN0[OF this None] 1 show ?thesis by(auto)
```
```   356       next
```
```   357         assume "t1 \<notin> B h"
```
```   358         thus ?thesis using 1 None by (auto)
```
```   359       qed
```
```   360     next
```
```   361       case [simp]: (Some bt')
```
```   362       obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
```
```   363       show ?thesis
```
```   364       proof cases
```
```   365         assume "t1 \<in> B h"
```
```   366         from Suc.IH(1)[OF this] 1 have "t1' \<in> T h" by simp
```
```   367         from n2_type3[OF this t12(2)] 1 show ?thesis by auto
```
```   368       next
```
```   369         assume "t1 \<notin> B h"
```
```   370         hence t1: "t1 \<in> U h" and t2: "t2 \<in> B h" using t12 by auto
```
```   371         from Suc.IH(2)[OF t1] have "t1' \<in> Um h" by simp
```
```   372         from n2_type1[OF this t2] 1 show ?thesis by auto
```
```   373       qed
```
```   374     qed
```
```   375   }
```
```   376   { case 2
```
```   377     then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \<in> B h" by auto
```
```   378     show ?case
```
```   379     proof (cases "split_min t1")
```
```   380       case None
```
```   381       with split_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
```
```   382     next
```
```   383       case [simp]: (Some bt')
```
```   384       obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
```
```   385       from Suc.IH(1)[OF t1] have "t1' \<in> T h" by simp
```
```   386       thus ?thesis using 2 by auto
```
```   387     qed
```
```   388   }
```
```   389 qed auto
```
```   390
```
```   391 lemma del_type:
```
```   392   "t \<in> B h \<Longrightarrow> del x t \<in> T h"
```
```   393   "t \<in> U h \<Longrightarrow> del x t \<in> Um h"
```
```   394 proof (induction h arbitrary: x t)
```
```   395   case (Suc h)
```
```   396   { case 1
```
```   397     then obtain l a r where [simp]: "t = N2 l a r" and
```
```   398       lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
```
```   399     have ?case if "x < a"
```
```   400     proof cases
```
```   401       assume "l \<in> B h"
```
```   402       from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
```
```   403       show ?thesis using \<open>x<a\<close> by(simp)
```
```   404     next
```
```   405       assume "l \<notin> B h"
```
```   406       hence "l \<in> U h" "r \<in> B h" using lr by auto
```
```   407       from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
```
```   408       show ?thesis using \<open>x<a\<close> by(simp)
```
```   409     qed
```
```   410     moreover
```
```   411     have ?case if "x > a"
```
```   412     proof cases
```
```   413       assume "r \<in> B h"
```
```   414       from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
```
```   415       show ?thesis using \<open>x>a\<close> by(simp)
```
```   416     next
```
```   417       assume "r \<notin> B h"
```
```   418       hence "l \<in> B h" "r \<in> U h" using lr by auto
```
```   419       from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
```
```   420       show ?thesis using \<open>x>a\<close> by(simp)
```
```   421     qed
```
```   422     moreover
```
```   423     have ?case if [simp]: "x=a"
```
```   424     proof (cases "split_min r")
```
```   425       case None
```
```   426       show ?thesis
```
```   427       proof cases
```
```   428         assume "r \<in> B h"
```
```   429         with split_minNoneN0[OF this None] lr show ?thesis by(simp)
```
```   430       next
```
```   431         assume "r \<notin> B h"
```
```   432         hence "r \<in> U h" using lr by auto
```
```   433         with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
```
```   434       qed
```
```   435     next
```
```   436       case [simp]: (Some br')
```
```   437       obtain b r' where [simp]: "br' = (b,r')" by fastforce
```
```   438       show ?thesis
```
```   439       proof cases
```
```   440         assume "r \<in> B h"
```
```   441         from split_min_type(1)[OF this] n2_type3[OF lr(1)]
```
```   442         show ?thesis by simp
```
```   443       next
```
```   444         assume "r \<notin> B h"
```
```   445         hence "l \<in> B h" and "r \<in> U h" using lr by auto
```
```   446         from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
```
```   447         show ?thesis by simp
```
```   448       qed
```
```   449     qed
```
```   450     ultimately show ?case by auto
```
```   451   }
```
```   452   { case 2 with Suc.IH(1) show ?case by auto }
```
```   453 qed auto
```
```   454
```
```   455 lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t \<in> B (h+1) \<union> B h"
```
```   456 by(auto)
```
```   457
```
```   458 lemma delete_type: "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
```
```   459 unfolding delete_def
```
```   460 by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
```
```   461
```
```   462 end
```
```   463
```
```   464
```
```   465 subsection "Overall correctness"
```
```   466
```
```   467 interpretation Set_by_Ordered
```
```   468 where empty = N0 and isin = isin and insert = insert.insert
```
```   469 and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
```
```   470 proof (standard, goal_cases)
```
```   471   case 2 thus ?case by(auto intro!: isin_set)
```
```   472 next
```
```   473   case 3 thus ?case by(auto intro!: insert.inorder_insert)
```
```   474 next
```
```   475   case 4 thus ?case by(auto intro!: delete.inorder_delete)
```
```   476 next
```
```   477   case 6 thus ?case using insert.insert_type by blast
```
```   478 next
```
```   479   case 7 thus ?case using delete.delete_type by blast
```
```   480 qed auto
```
```   481
```
```   482
```
```   483 subsection \<open>Height-Size Relation\<close>
```
```   484
```
```   485 text \<open>By Daniel St\"uwe\<close>
```
```   486
```
```   487 fun fib_tree :: "nat \<Rightarrow> unit bro" where
```
```   488   "fib_tree 0 = N0"
```
```   489 | "fib_tree (Suc 0) = N2 N0 () N0"
```
```   490 | "fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))"
```
```   491
```
```   492 fun fib' :: "nat \<Rightarrow> nat" where
```
```   493   "fib' 0 = 0"
```
```   494 | "fib' (Suc 0) = 1"
```
```   495 | "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h"
```
```   496
```
```   497 fun size :: "'a bro \<Rightarrow> nat" where
```
```   498   "size N0 = 0"
```
```   499 | "size (N1 t) = size t"
```
```   500 | "size (N2 t1 _ t2) = 1 + size t1 + size t2"
```
```   501
```
```   502 lemma fib_tree_B: "fib_tree h \<in> B h"
```
```   503 by (induction h rule: fib_tree.induct) auto
```
```   504
```
```   505 declare [[names_short]]
```
```   506
```
```   507 lemma size_fib': "size (fib_tree h) = fib' h"
```
```   508 by (induction h rule: fib_tree.induct) auto
```
```   509
```
```   510 lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))"
```
```   511 by (induction h rule: fib_tree.induct) auto
```
```   512
```
```   513 lemma B_N2_cases[consumes 1]:
```
```   514 assumes "N2 t1 a t2 \<in> B (Suc n)"
```
```   515 obtains
```
```   516   (BB) "t1 \<in> B n" and "t2 \<in> B n" |
```
```   517   (UB) "t1 \<in> U n" and "t2 \<in> B n" |
```
```   518   (BU) "t1 \<in> B n" and "t2 \<in> U n"
```
```   519 using assms by auto
```
```   520
```
```   521 lemma size_bounded: "t \<in> B h \<Longrightarrow> size t \<ge> size (fib_tree h)"
```
```   522 unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct)
```
```   523 case (3 h t')
```
```   524   note main = 3
```
```   525   then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto
```
```   526   with main have "N2 t1 a t2 \<in> B (Suc (Suc h))" by auto
```
```   527   thus ?case proof (cases rule: B_N2_cases)
```
```   528     case BB
```
```   529     then obtain x y z where t2: "t2 = N2 x y z \<or> t2 = N2 z y x" "x \<in> B h" by auto
```
```   530     show ?thesis unfolding t' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto
```
```   531   next
```
```   532     case UB
```
```   533     then obtain t11 where t1: "t1 = N1 t11" "t11 \<in> B h" by auto
```
```   534     show ?thesis unfolding t' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp
```
```   535   next
```
```   536     case BU
```
```   537     then obtain t22 where t2: "t2 = N1 t22" "t22 \<in> B h" by auto
```
```   538     show ?thesis unfolding t' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp
```
```   539   qed
```
```   540 qed auto
```
```   541
```
```   542 theorem "t \<in> B h \<Longrightarrow> fib (h + 2) \<le> size t + 1"
```
```   543 using size_bounded
```
```   544 by (simp add: size_fib' fibfib[symmetric] del: fib.simps)
```
```   545
```
```   546 end
```