added 1-2 brother trees
authornipkow
Fri Dec 04 14:39:31 2015 +0100 (2015-12-04)
changeset 6178421b34a2269e5
parent 61781 e1e6bb36b27a
child 61785 7a461602a218
added 1-2 brother trees
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/document/root.bib
src/HOL/Data_Structures/document/root.tex
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Fri Dec 04 14:39:31 2015 +0100
     1.3 @@ -0,0 +1,491 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section \<open>A 1-2 Brother Tree Implementation of Sets\<close>
     1.7 +
     1.8 +theory Brother12_Set
     1.9 +imports
    1.10 +  Cmp
    1.11 +  Set_by_Ordered
    1.12 +begin
    1.13 +
    1.14 +subsection \<open>Data Type and Operations\<close>
    1.15 +
    1.16 +datatype 'a bro =
    1.17 +  N0 |
    1.18 +  N1 "'a bro" |
    1.19 +  N2 "'a bro" 'a "'a bro" |
    1.20 +  (* auxiliary constructors: *)
    1.21 +  L2 'a |
    1.22 +  N3 "'a bro" 'a "'a bro" 'a "'a bro"
    1.23 +
    1.24 +fun inorder :: "'a bro \<Rightarrow> 'a list" where
    1.25 +"inorder N0 = []" |
    1.26 +"inorder (N1 t) = inorder t" |
    1.27 +"inorder (N2 l a r) = inorder l @ a # inorder r" |
    1.28 +"inorder (L2 a) = [a]" |
    1.29 +"inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
    1.30 +
    1.31 +fun isin :: "'a bro \<Rightarrow> 'a::cmp \<Rightarrow> bool" where
    1.32 +"isin N0 x = False" |
    1.33 +"isin (N1 t) x = isin t x" |
    1.34 +"isin (N2 l a r) x =
    1.35 +  (case cmp x a of
    1.36 +     LT \<Rightarrow> isin l x |
    1.37 +     EQ \<Rightarrow> True |
    1.38 +     GT \<Rightarrow> isin r x)"
    1.39 +
    1.40 +fun n1 :: "'a bro \<Rightarrow> 'a bro" where
    1.41 +"n1 (L2 a) = N2 N0 a N0" |
    1.42 +"n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
    1.43 +"n1 t = N1 t"
    1.44 +
    1.45 +hide_const (open) insert
    1.46 +
    1.47 +locale insert
    1.48 +begin
    1.49 +
    1.50 +fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    1.51 +"n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
    1.52 +"n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
    1.53 +"n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
    1.54 +"n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
    1.55 +"n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
    1.56 +"n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
    1.57 +"n2 t1 a t2 = N2 t1 a t2"
    1.58 +
    1.59 +fun ins :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    1.60 +"ins a N0 = L2 a" |
    1.61 +"ins a (N1 t) = n1 (ins a t)" |
    1.62 +"ins a (N2 l b r) =
    1.63 +  (case cmp a b of
    1.64 +     LT \<Rightarrow> n2 (ins a l) b r |
    1.65 +     EQ \<Rightarrow> N2 l b r |
    1.66 +     GT \<Rightarrow> n2 l b (ins a r))"
    1.67 +
    1.68 +fun tree :: "'a bro \<Rightarrow> 'a bro" where
    1.69 +"tree (L2 a) = N2 N0 a N0" |
    1.70 +"tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
    1.71 +"tree t = t"
    1.72 +
    1.73 +definition insert :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    1.74 +"insert x t = tree(ins x t)"
    1.75 +
    1.76 +end
    1.77 +
    1.78 +locale delete
    1.79 +begin
    1.80 +
    1.81 +fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
    1.82 +"n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
    1.83 +"n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
    1.84 +  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
    1.85 +"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
    1.86 +  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
    1.87 +"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
    1.88 +  N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" |
    1.89 +"n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
    1.90 +  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
    1.91 +"n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
    1.92 +  N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
    1.93 +"n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
    1.94 +  N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
    1.95 +"n2 t1 a1 t2 = N2 t1 a1 t2"
    1.96 +
    1.97 +fun del_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where
    1.98 +"del_min N0 = None" |
    1.99 +"del_min (N1 t) =
   1.100 +  (case del_min t of
   1.101 +     None \<Rightarrow> None |
   1.102 +     Some (a, t') \<Rightarrow> Some (a, N1 t'))" |
   1.103 +"del_min (N2 t1 a t2) =
   1.104 +  (case del_min t1 of
   1.105 +     None \<Rightarrow> Some (a, N1 t2) |
   1.106 +     Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))"
   1.107 +
   1.108 +fun del :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
   1.109 +"del _ N0         = N0" |
   1.110 +"del x (N1 t)     = N1 (del x t)" |
   1.111 +"del x (N2 l a r) =
   1.112 +  (case cmp x a of
   1.113 +     LT \<Rightarrow> n2 (del x l) a r |
   1.114 +     GT \<Rightarrow> n2 l a (del x r) |
   1.115 +     EQ \<Rightarrow> (case del_min r of
   1.116 +              None \<Rightarrow> N1 l |
   1.117 +              Some (b, r') \<Rightarrow> n2 l b r'))"
   1.118 +
   1.119 +fun tree :: "'a bro \<Rightarrow> 'a bro" where
   1.120 +"tree (N1 t) = t" |
   1.121 +"tree t = t"
   1.122 +
   1.123 +definition delete :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
   1.124 +"delete a t = tree (del a t)"
   1.125 +
   1.126 +end
   1.127 +
   1.128 +subsection \<open>Invariants\<close>
   1.129 +
   1.130 +fun B :: "nat \<Rightarrow> 'a bro set"
   1.131 +and U :: "nat \<Rightarrow> 'a bro set" where
   1.132 +"B 0 = {N0}" |
   1.133 +"B (Suc h) = { N2 t1 a t2 | t1 a t2. 
   1.134 +  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}" |
   1.135 +"U 0 = {}" |
   1.136 +"U (Suc h) = N1 ` B h"
   1.137 +
   1.138 +abbreviation "T h \<equiv> B h \<union> U h"
   1.139 +
   1.140 +fun Bp :: "nat \<Rightarrow> 'a bro set" where
   1.141 +"Bp 0 = B 0 \<union> L2 ` UNIV" |
   1.142 +"Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" |
   1.143 +"Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union>
   1.144 +  {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)}"
   1.145 +
   1.146 +fun Um :: "nat \<Rightarrow> 'a bro set" where
   1.147 +"Um 0 = {}" |
   1.148 +"Um (Suc h) = N1 ` T h"
   1.149 +
   1.150 +
   1.151 +subsection "Functional Correctness Proofs"
   1.152 +
   1.153 +subsubsection "Proofs for isin"
   1.154 +
   1.155 +lemma
   1.156 +  "t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
   1.157 +by(induction h arbitrary: t) (fastforce simp: elems_simps1 split: if_splits)+
   1.158 +
   1.159 +lemma isin_set: "t \<in> T h \<Longrightarrow>
   1.160 +  sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems(inorder t))"
   1.161 +by(induction h arbitrary: t) (auto simp: elems_simps2 split: if_splits)
   1.162 +
   1.163 +subsubsection "Proofs for insertion"
   1.164 +
   1.165 +lemma inorder_n1: "inorder(n1 t) = inorder t"
   1.166 +by(induction t rule: n1.induct) (auto simp: sorted_lems)
   1.167 +
   1.168 +context insert
   1.169 +begin
   1.170 +
   1.171 +lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
   1.172 +by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
   1.173 +
   1.174 +lemma inorder_tree: "inorder(tree t) = inorder t"
   1.175 +by(cases t) auto
   1.176 +
   1.177 +lemma inorder_ins: "t \<in> T h \<Longrightarrow>
   1.178 +  sorted(inorder t) \<Longrightarrow> inorder(ins a t) = ins_list a (inorder t)"
   1.179 +by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
   1.180 +
   1.181 +lemma inorder_insert: "t \<in> T h \<Longrightarrow>
   1.182 +  sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
   1.183 +by(simp add: insert_def inorder_ins inorder_tree)
   1.184 +
   1.185 +end
   1.186 +
   1.187 +subsubsection \<open>Proofs for deletion\<close>
   1.188 +
   1.189 +context delete
   1.190 +begin
   1.191 +
   1.192 +lemma inorder_tree: "inorder(tree t) = inorder t"
   1.193 +by(cases t) auto
   1.194 +
   1.195 +lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
   1.196 +by(induction l a r rule: n2.induct) (auto)
   1.197 +
   1.198 +lemma inorder_del_min:
   1.199 +shows "t \<in> B h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
   1.200 +  (del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
   1.201 +and "t \<in> U h \<Longrightarrow> (del_min t = None \<longleftrightarrow> inorder t = []) \<and>
   1.202 +  (del_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')"
   1.203 +by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
   1.204 +
   1.205 +lemma inorder_del:
   1.206 +  "t \<in> B h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del a t) = del_list a (inorder t)"
   1.207 +  "t \<in> U h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del a t) = del_list a (inorder t)"
   1.208 +by(induction h arbitrary: t)
   1.209 +  (auto simp: del_list_simps inorder_n2 inorder_del_min split: option.splits)
   1.210 +
   1.211 +end
   1.212 +
   1.213 +
   1.214 +subsection \<open>Invariant Proofs\<close>
   1.215 +
   1.216 +subsection \<open>Proofs for insertion\<close>
   1.217 +
   1.218 +lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)"
   1.219 +by(cases h rule: Bp.cases) auto
   1.220 +
   1.221 +context insert
   1.222 +begin
   1.223 +
   1.224 +lemma tree_type1: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)"
   1.225 +by(cases h rule: Bp.cases) auto
   1.226 +
   1.227 +lemma tree_type2: "t \<in> T h \<Longrightarrow> tree t \<in> T h"
   1.228 +by(cases h) auto
   1.229 +
   1.230 +lemma n2_type:
   1.231 +  "(t1 \<in> Bp h \<and> t2 \<in> T h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h)) \<and>
   1.232 +   (t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))"
   1.233 +apply(cases h rule: Bp.cases)
   1.234 +apply (auto)[2]
   1.235 +apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
   1.236 +done
   1.237 +
   1.238 +lemma Bp_if_B: "t \<in> B h \<Longrightarrow> t \<in> Bp h"
   1.239 +by (cases h rule: Bp.cases) simp_all
   1.240 +
   1.241 +text{* An automatic proof: *}
   1.242 +
   1.243 +lemma
   1.244 +  "(t \<in> B h \<longrightarrow> ins x t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> ins x t \<in> T h)"
   1.245 +apply(induction h arbitrary: t)
   1.246 + apply (simp)
   1.247 +apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
   1.248 +done
   1.249 +
   1.250 +text{* A detailed proof: *}
   1.251 +
   1.252 +lemma ins_type:
   1.253 +shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h"
   1.254 +proof(induction h arbitrary: t)
   1.255 +  case 0
   1.256 +  { case 1 thus ?case by simp
   1.257 +  next
   1.258 +    case 2 thus ?case by simp }
   1.259 +next
   1.260 +  case (Suc h)
   1.261 +  { case 1
   1.262 +    then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
   1.263 +      t1: "t1 \<in> T h" and t2: "t2 \<in> T h" and t12: "t1 \<in> B h \<or> t2 \<in> B h"
   1.264 +      by auto
   1.265 +    { assume "x < a"
   1.266 +      hence "?case \<longleftrightarrow> n2 (ins x t1) a t2 \<in> Bp (Suc h)" by simp
   1.267 +      also have "\<dots>"
   1.268 +      proof cases
   1.269 +        assume "t1 \<in> B h"
   1.270 +        with t2 show ?thesis by (simp add: Suc.IH(1) n2_type)
   1.271 +      next
   1.272 +        assume "t1 \<notin> B h"
   1.273 +        hence 1: "t1 \<in> U h" and 2: "t2 \<in> B h" using t1 t12 by auto
   1.274 +        show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type)
   1.275 +      qed
   1.276 +      finally have ?case .
   1.277 +    }
   1.278 +    moreover
   1.279 +    { assume "a < x"
   1.280 +      hence "?case \<longleftrightarrow> n2 t1 a (ins x t2) \<in> Bp (Suc h)" by simp
   1.281 +      also have "\<dots>"
   1.282 +      proof cases
   1.283 +        assume "t2 \<in> B h"
   1.284 +        with t1 show ?thesis by (simp add: Suc.IH(1) n2_type)
   1.285 +      next
   1.286 +        assume "t2 \<notin> B h"
   1.287 +        hence 1: "t1 \<in> B h" and 2: "t2 \<in> U h" using t2 t12 by auto
   1.288 +        show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type)
   1.289 +      qed
   1.290 +    }
   1.291 +    moreover 
   1.292 +    { assume "x = a"
   1.293 +      from 1 have "t \<in> Bp (Suc h)" by(rule Bp_if_B)
   1.294 +      hence "?case" using `x = a` by simp
   1.295 +    }
   1.296 +    ultimately show ?case by auto
   1.297 +  next
   1.298 +    case 2 thus ?case using Suc(1) n1_type by fastforce }
   1.299 +qed
   1.300 +
   1.301 +lemma insert_type:
   1.302 +  "t \<in> T h \<Longrightarrow> insert x t \<in> T h \<union> T (Suc h)"
   1.303 +unfolding insert_def by (metis Un_iff ins_type tree_type1 tree_type2)
   1.304 +
   1.305 +end
   1.306 +
   1.307 +subsection "Proofs for deletion"
   1.308 +
   1.309 +lemma B_simps[simp]: 
   1.310 +  "N1 t \<in> B h = False"
   1.311 +  "L2 y \<in> B h = False"
   1.312 +  "(N3 t1 a1 t2 a2 t3) \<in> B h = False"
   1.313 +  "N0 \<in> B h \<longleftrightarrow> h = 0"
   1.314 +by (cases h, auto)+
   1.315 +
   1.316 +context delete
   1.317 +begin
   1.318 +
   1.319 +lemma n2_type1:
   1.320 +  "\<lbrakk>t1 \<in> Um h; t2 \<in> B h\<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
   1.321 +apply(cases h rule: Bp.cases)
   1.322 +apply auto[2]
   1.323 +apply(erule exE bexE conjE imageE | simp | erule disjE)+
   1.324 +done
   1.325 +
   1.326 +lemma n2_type2:
   1.327 +  "\<lbrakk>t1 \<in> B h ; t2 \<in> Um h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
   1.328 +apply(cases h rule: Bp.cases)
   1.329 +apply auto[2]
   1.330 +apply(erule exE bexE conjE imageE | simp | erule disjE)+
   1.331 +done
   1.332 +
   1.333 +lemma n2_type3:
   1.334 +  "\<lbrakk>t1 \<in> T h ; t2 \<in> T h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)"
   1.335 +apply(cases h rule: Bp.cases)
   1.336 +apply auto[2]
   1.337 +apply(erule exE bexE conjE imageE | simp | erule disjE)+
   1.338 +done
   1.339 +
   1.340 +lemma del_minNoneN0: "\<lbrakk>t \<in> B h; del_min t = None\<rbrakk> \<Longrightarrow>  t = N0"
   1.341 +by (cases t) (auto split: option.splits)
   1.342 +
   1.343 +lemma del_minNoneN1 : "\<lbrakk>t \<in> U h; del_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
   1.344 +by (cases h) (auto simp: del_minNoneN0  split: option.splits)
   1.345 +
   1.346 +lemma del_min_type:
   1.347 +  "t \<in> B h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> T h"
   1.348 +  "t \<in> U h \<Longrightarrow> del_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h"
   1.349 +proof (induction h arbitrary: t a t')
   1.350 +  case (Suc h)
   1.351 +  { case 1
   1.352 +    then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
   1.353 +      t12: "t1 \<in> T h" "t2 \<in> T h" "t1 \<in> B h \<or> t2 \<in> B h"
   1.354 +      by auto
   1.355 +    show ?case
   1.356 +    proof (cases "del_min t1")
   1.357 +      case None
   1.358 +      show ?thesis
   1.359 +      proof cases
   1.360 +        assume "t1 \<in> B h"
   1.361 +        with del_minNoneN0[OF this None] 1 show ?thesis by(auto)
   1.362 +      next
   1.363 +        assume "t1 \<notin> B h"
   1.364 +        thus ?thesis using 1 None by (auto)
   1.365 +      qed
   1.366 +    next
   1.367 +      case [simp]: (Some bt')
   1.368 +      obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
   1.369 +      show ?thesis
   1.370 +      proof cases
   1.371 +        assume "t1 \<in> B h"
   1.372 +        from Suc.IH(1)[OF this] 1 have "t1' \<in> T h" by simp
   1.373 +        from n2_type3[OF this t12(2)] 1 show ?thesis by auto
   1.374 +      next
   1.375 +        assume "t1 \<notin> B h"
   1.376 +        hence t1: "t1 \<in> U h" and t2: "t2 \<in> B h" using t12 by auto
   1.377 +        from Suc.IH(2)[OF t1] have "t1' \<in> Um h" by simp
   1.378 +        from n2_type1[OF this t2] 1 show ?thesis by auto
   1.379 +      qed
   1.380 +    qed
   1.381 +  }
   1.382 +  { case 2
   1.383 +    then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \<in> B h" by auto
   1.384 +    show ?case
   1.385 +    proof (cases "del_min t1")
   1.386 +      case None
   1.387 +      with del_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
   1.388 +    next
   1.389 +      case [simp]: (Some bt')
   1.390 +      obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
   1.391 +      from Suc.IH(1)[OF t1] have "t1' \<in> T h" by simp
   1.392 +      thus ?thesis using 2 by auto
   1.393 +    qed
   1.394 +  }
   1.395 +qed auto
   1.396 +
   1.397 +lemma del_type:
   1.398 +  "t \<in> B h \<Longrightarrow> del x t \<in> T h"
   1.399 +  "t \<in> U h \<Longrightarrow> del x t \<in> Um h"
   1.400 +proof (induction h arbitrary: x t)
   1.401 +  case (Suc h)
   1.402 +  { case 1
   1.403 +    then obtain l a r where [simp]: "t = N2 l a r" and
   1.404 +      lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
   1.405 +    { assume "x < a"
   1.406 +      have ?case
   1.407 +      proof cases
   1.408 +        assume "l \<in> B h"
   1.409 +        from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
   1.410 +        show ?thesis using `x<a` by(simp)
   1.411 +      next
   1.412 +        assume "l \<notin> B h"
   1.413 +        hence "l \<in> U h" "r \<in> B h" using lr by auto
   1.414 +        from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
   1.415 +        show ?thesis using `x<a` by(simp)
   1.416 +      qed
   1.417 +    } moreover
   1.418 +    { assume "x > a"
   1.419 +      have ?case
   1.420 +      proof cases
   1.421 +        assume "r \<in> B h"
   1.422 +        from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
   1.423 +        show ?thesis using `x>a` by(simp)
   1.424 +      next
   1.425 +        assume "r \<notin> B h"
   1.426 +        hence "l \<in> B h" "r \<in> U h" using lr by auto
   1.427 +        from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
   1.428 +        show ?thesis using `x>a` by(simp)
   1.429 +      qed
   1.430 +    } moreover
   1.431 +    { assume [simp]: "x=a"
   1.432 +      have ?case
   1.433 +      proof (cases "del_min r")
   1.434 +        case None
   1.435 +        show ?thesis
   1.436 +        proof cases
   1.437 +          assume "r \<in> B h"
   1.438 +          with del_minNoneN0[OF this None] lr show ?thesis by(simp)
   1.439 +        next
   1.440 +          assume "r \<notin> B h"
   1.441 +          hence "r \<in> U h" using lr by auto
   1.442 +          with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   1.443 +        qed
   1.444 +      next
   1.445 +        case [simp]: (Some br')
   1.446 +        obtain b r' where [simp]: "br' = (b,r')" by fastforce
   1.447 +        show ?thesis
   1.448 +        proof cases
   1.449 +          assume "r \<in> B h"
   1.450 +          from del_min_type(1)[OF this] n2_type3[OF lr(1)]
   1.451 +          show ?thesis by simp
   1.452 +        next
   1.453 +          assume "r \<notin> B h"
   1.454 +          hence "l \<in> B h" and "r \<in> U h" using lr by auto
   1.455 +          from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   1.456 +          show ?thesis by simp
   1.457 +        qed
   1.458 +      qed
   1.459 +    } ultimately show ?case by auto
   1.460 +  }
   1.461 +  { case 2 with Suc.IH(1) show ?case by auto }
   1.462 +qed auto
   1.463 +
   1.464 +lemma tree_type:
   1.465 +  "t \<in> Um (Suc h) \<Longrightarrow> tree t : T h"
   1.466 +  "t \<in> T (Suc h) \<Longrightarrow> tree t : T h \<union> T(h+1)"
   1.467 +by(auto)
   1.468 +
   1.469 +lemma delete_type:
   1.470 +  "t \<in> T h \<Longrightarrow> delete x t \<in> T h \<union> T(h-1)"
   1.471 +unfolding delete_def
   1.472 +by (cases h) (simp, metis del_type tree_type Un_iff Suc_eq_plus1 diff_Suc_1)
   1.473 +
   1.474 +end
   1.475 +
   1.476 +subsection "Overall correctness"
   1.477 +
   1.478 +interpretation Set_by_Ordered
   1.479 +where empty = N0 and isin = isin and insert = insert.insert and delete = delete.delete
   1.480 +and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
   1.481 +proof (standard, goal_cases)
   1.482 +  case 2 thus ?case by(auto intro!: isin_set)
   1.483 +next
   1.484 +  case 3 thus ?case by(auto intro!: insert.inorder_insert)
   1.485 +next
   1.486 +  case 4 thus ?case
   1.487 +    by(auto simp: delete.delete_def delete.inorder_tree delete.inorder_del)
   1.488 +next
   1.489 +  case 6 thus ?case using insert.insert_type by blast
   1.490 +next
   1.491 +  case 7 thus ?case using delete.delete_type by blast
   1.492 +qed auto
   1.493 +
   1.494 +end
     2.1 --- a/src/HOL/Data_Structures/document/root.bib	Thu Dec 03 15:33:01 2015 +0100
     2.2 +++ b/src/HOL/Data_Structures/document/root.bib	Fri Dec 04 14:39:31 2015 +0100
     2.3 @@ -1,3 +1,8 @@
     2.4 +@article{Hinze-bro12,author={Ralf Hinze},
     2.5 +title={Purely Functional 1-2 Brother Trees},
     2.6 +journal={J. Functional Programming},
     2.7 +volume=19,number={6},pages={633--644},year=2009}
     2.8 +
     2.9  @article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
    2.10  journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
    2.11  
    2.12 @@ -7,6 +12,14 @@
    2.13  @book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
    2.14  publisher="Cambridge University Press",year=1998}
    2.15  
    2.16 +@article{OttmannS76,author={Thomas Ottmann and Hans-Werner Six},
    2.17 +title={Eine neue {K}lasse von ausgeglichenen {B}in\"arb\"aumen},
    2.18 +journal={Angewandte Informatik},volume=18,number=9,pages={395--400},year=1976}
    2.19 +
    2.20 +@article{OttmannW-CJ80,author={Thomas Ottmann and Derick Wood},
    2.21 +title={1-2 Brother Trees or {AVL} Trees Revisited},journal={Comput. J.},
    2.22 +volume=23,number=3,pages={248--255},year=1980}
    2.23 +
    2.24  @article{Schoenmakers-IPL93,author="Berry Schoenmakers",
    2.25  title="A Systematic Analysis of Splaying",journal={Information Processing Letters},volume=45,pages={41-50},year=1993}
    2.26  
     3.1 --- a/src/HOL/Data_Structures/document/root.tex	Thu Dec 03 15:33:01 2015 +0100
     3.2 +++ b/src/HOL/Data_Structures/document/root.tex	Fri Dec 04 14:39:31 2015 +0100
     3.3 @@ -45,6 +45,10 @@
     3.4  The function definitions are based on the teaching material by
     3.5  Turbak~\cite{Turbak230}.
     3.6  
     3.7 +\paragraph{1-2 brother trees}
     3.8 +They were invented by Ottmann and Six~\cite{OttmannS76,OttmannW-CJ80}.
     3.9 +The functional version is due to Hinze~\cite{Hinze-bro12}.
    3.10 +
    3.11  \paragraph{Splay trees}
    3.12  They were invented by Sleator and Tarjan \cite{SleatorT-JACM85}.
    3.13  Our formalisation follows Schoenmakers \cite{Schoenmakers-IPL93}.
     4.1 --- a/src/HOL/ROOT	Thu Dec 03 15:33:01 2015 +0100
     4.2 +++ b/src/HOL/ROOT	Fri Dec 04 14:39:31 2015 +0100
     4.3 @@ -178,6 +178,7 @@
     4.4      RBT_Map
     4.5      Tree23_Map
     4.6      Tree234_Map
     4.7 +    Brother12_Set
     4.8      Splay_Map
     4.9    document_files "root.tex" "root.bib"
    4.10