src/HOL/Data_Structures/Tree234_Set.thy
author nipkow
Wed Jun 13 15:24:20 2018 +0200 (10 months ago)
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 69597 ff784d5a5bfb
permissions -rw-r--r--
qualify interpretations to avoid clashes
     1 (* Author: Tobias Nipkow *)
     2 
     3 section \<open>2-3-4 Tree Implementation of Sets\<close>
     4 
     5 theory Tree234_Set
     6 imports
     7   Tree234
     8   Cmp
     9   Set_Specs
    10 begin
    11 
    12 declare sorted_wrt.simps(2)[simp del]
    13 
    14 subsection \<open>Set operations on 2-3-4 trees\<close>
    15 
    16 definition empty :: "'a tree234" where
    17 "empty = Leaf"
    18 
    19 fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
    20 "isin Leaf x = False" |
    21 "isin (Node2 l a r) x =
    22   (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
    23 "isin (Node3 l a m b r) x =
    24   (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
    25    LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))" |
    26 "isin (Node4 t1 a t2 b t3 c t4) x =
    27   (case cmp x b of
    28      LT \<Rightarrow>
    29        (case cmp x a of
    30           LT \<Rightarrow> isin t1 x |
    31           EQ \<Rightarrow> True |
    32           GT \<Rightarrow> isin t2 x) |
    33      EQ \<Rightarrow> True |
    34      GT \<Rightarrow>
    35        (case cmp x c of
    36           LT \<Rightarrow> isin t3 x |
    37           EQ \<Rightarrow> True |
    38           GT \<Rightarrow> isin t4 x))"
    39 
    40 datatype 'a up\<^sub>i = T\<^sub>i "'a tree234" | Up\<^sub>i "'a tree234" 'a "'a tree234"
    41 
    42 fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree234" where
    43 "tree\<^sub>i (T\<^sub>i t) = t" |
    44 "tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
    45 
    46 fun ins :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
    47 "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
    48 "ins x (Node2 l a r) =
    49    (case cmp x a of
    50       LT \<Rightarrow> (case ins x l of
    51               T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
    52             | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
    53       EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
    54       GT \<Rightarrow> (case ins x r of
    55               T\<^sub>i r' => T\<^sub>i (Node2 l a r')
    56             | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
    57 "ins x (Node3 l a m b r) =
    58    (case cmp x a of
    59       LT \<Rightarrow> (case ins x l of
    60               T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
    61             | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
    62       EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    63       GT \<Rightarrow> (case cmp x b of
    64                GT \<Rightarrow> (case ins x r of
    65                        T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
    66                      | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
    67                EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    68                LT \<Rightarrow> (case ins x m of
    69                        T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
    70                      | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))" |
    71 "ins x (Node4 t1 a t2 b t3 c t4) =
    72   (case cmp x b of
    73      LT \<Rightarrow>
    74        (case cmp x a of
    75           LT \<Rightarrow>
    76             (case ins x t1 of
    77                T\<^sub>i t => T\<^sub>i (Node4 t a t2 b t3 c t4) |
    78                Up\<^sub>i l y r => Up\<^sub>i (Node2 l y r) a (Node3 t2 b t3 c t4)) |
    79           EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) |
    80           GT \<Rightarrow>
    81             (case ins x t2 of
    82                T\<^sub>i t => T\<^sub>i (Node4 t1 a t b t3 c t4) |
    83                Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a l) y (Node3 r b t3 c t4))) |
    84      EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) |
    85      GT \<Rightarrow>
    86        (case cmp x c of
    87           LT \<Rightarrow>
    88             (case ins x t3 of
    89               T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t c t4) |
    90               Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 l y r c t4)) |
    91           EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) |
    92           GT \<Rightarrow>
    93             (case ins x t4 of
    94               T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t3 c t) |
    95               Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 t3 c l y r))))"
    96 
    97 hide_const insert
    98 
    99 definition insert :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
   100 "insert x t = tree\<^sub>i(ins x t)"
   101 
   102 datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
   103 
   104 fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree234" where
   105 "tree\<^sub>d (T\<^sub>d t) = t" |
   106 "tree\<^sub>d (Up\<^sub>d t) = t"
   107 
   108 fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   109 "node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" |
   110 "node21 (Up\<^sub>d l) a (Node2 lr b rr) = Up\<^sub>d(Node3 l a lr b rr)" |
   111 "node21 (Up\<^sub>d l) a (Node3 lr b mr c rr) = T\<^sub>d(Node2 (Node2 l a lr) b (Node2 mr c rr))" |
   112 "node21 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
   113 
   114 fun node22 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
   115 "node22 l a (T\<^sub>d r) = T\<^sub>d(Node2 l a r)" |
   116 "node22 (Node2 ll b rl) a (Up\<^sub>d r) = Up\<^sub>d(Node3 ll b rl a r)" |
   117 "node22 (Node3 ll b ml c rl) a (Up\<^sub>d r) = T\<^sub>d(Node2 (Node2 ll b ml) c (Node2 rl a r))" |
   118 "node22 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
   119 
   120 fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   121 "node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
   122 "node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
   123 "node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" |
   124 "node31 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6)"
   125 
   126 fun node32 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   127 "node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
   128 "node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   129 "node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
   130 "node32 t1 a (Up\<^sub>d t2) b (Node4 t3 c t4 d t5 e t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
   131 
   132 fun node33 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
   133 "node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
   134 "node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   135 "node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
   136 "node33 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
   137 
   138 fun node41 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   139 "node41 (T\<^sub>d t1) a t2 b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   140 "node41 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
   141 "node41 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
   142 "node41 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
   143 
   144 fun node42 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   145 "node42 t1 a (T\<^sub>d t2) b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   146 "node42 (Node2 t1 a t2) b (Up\<^sub>d t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
   147 "node42 (Node3 t1 a t2 b t3) c (Up\<^sub>d t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
   148 "node42 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
   149 
   150 fun node43 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   151 "node43 t1 a t2 b (T\<^sub>d t3) c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   152 "node43 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) d t5 = T\<^sub>d(Node3 t1 a (Node3 t2 b t3 c t4) d t5)" |
   153 "node43 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) e t6 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node2 t4 d t5) e t6)" |
   154 "node43 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) f t7 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6) f t7)"
   155 
   156 fun node44 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
   157 "node44 t1 a t2 b t3 c (T\<^sub>d t4) = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
   158 "node44 t1 a t2 b (Node2 t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a t2 b (Node3 t3 c t4 d t5))" |
   159 "node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" |
   160 "node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Up\<^sub>d t7) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))"
   161 
   162 fun split_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
   163 "split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
   164 "split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
   165 "split_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
   166 "split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
   167 "split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" |
   168 "split_min (Node4 l a m b n c r) = (let (x,l') = split_min l in (x, node41 l' a m b n c r))"
   169 
   170 fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
   171 "del k Leaf = T\<^sub>d Leaf" |
   172 "del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
   173 "del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
   174   else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
   175 "del k (Node4 Leaf a Leaf b Leaf c Leaf) =
   176   T\<^sub>d(if k=a then Node3 Leaf b Leaf c Leaf else
   177      if k=b then Node3 Leaf a Leaf c Leaf else
   178      if k=c then Node3 Leaf a Leaf b Leaf
   179      else Node4 Leaf a Leaf b Leaf c Leaf)" |
   180 "del k (Node2 l a r) = (case cmp k a of
   181   LT \<Rightarrow> node21 (del k l) a r |
   182   GT \<Rightarrow> node22 l a (del k r) |
   183   EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
   184 "del k (Node3 l a m b r) = (case cmp k a of
   185   LT \<Rightarrow> node31 (del k l) a m b r |
   186   EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
   187   GT \<Rightarrow> (case cmp k b of
   188            LT \<Rightarrow> node32 l a (del k m) b r |
   189            EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
   190            GT \<Rightarrow> node33 l a m b (del k r)))" |
   191 "del k (Node4 l a m b n c r) = (case cmp k b of
   192   LT \<Rightarrow> (case cmp k a of
   193           LT \<Rightarrow> node41 (del k l) a m b n c r |
   194           EQ \<Rightarrow> let (a',m') = split_min m in node42 l a' m' b n c r |
   195           GT \<Rightarrow> node42 l a (del k m) b n c r) |
   196   EQ \<Rightarrow> let (b',n') = split_min n in node43 l a m b' n' c r |
   197   GT \<Rightarrow> (case cmp k c of
   198            LT \<Rightarrow> node43 l a m b (del k n) c r |
   199            EQ \<Rightarrow> let (c',r') = split_min r in node44 l a m b n c' r' |
   200            GT \<Rightarrow> node44 l a m b n c (del k r)))"
   201 
   202 definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
   203 "delete x t = tree\<^sub>d(del x t)"
   204 
   205 
   206 subsection "Functional correctness"
   207 
   208 subsubsection \<open>Functional correctness of isin:\<close>
   209 
   210 lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))"
   211 by (induction t) (auto simp: isin_simps ball_Un)
   212 
   213 
   214 subsubsection \<open>Functional correctness of insert:\<close>
   215 
   216 lemma inorder_ins:
   217   "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
   218 by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits)
   219 
   220 lemma inorder_insert:
   221   "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
   222 by(simp add: insert_def inorder_ins)
   223 
   224 
   225 subsubsection \<open>Functional correctness of delete\<close>
   226 
   227 lemma inorder_node21: "height r > 0 \<Longrightarrow>
   228   inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
   229 by(induct l' a r rule: node21.induct) auto
   230 
   231 lemma inorder_node22: "height l > 0 \<Longrightarrow>
   232   inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
   233 by(induct l a r' rule: node22.induct) auto
   234 
   235 lemma inorder_node31: "height m > 0 \<Longrightarrow>
   236   inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
   237 by(induct l' a m b r rule: node31.induct) auto
   238 
   239 lemma inorder_node32: "height r > 0 \<Longrightarrow>
   240   inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
   241 by(induct l a m' b r rule: node32.induct) auto
   242 
   243 lemma inorder_node33: "height m > 0 \<Longrightarrow>
   244   inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
   245 by(induct l a m b r' rule: node33.induct) auto
   246 
   247 lemma inorder_node41: "height m > 0 \<Longrightarrow>
   248   inorder (tree\<^sub>d (node41 l' a m b n c r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder n @ c # inorder r"
   249 by(induct l' a m b n c r rule: node41.induct) auto
   250 
   251 lemma inorder_node42: "height l > 0 \<Longrightarrow>
   252   inorder (tree\<^sub>d (node42 l a m b n c r)) = inorder l @ a # inorder (tree\<^sub>d m) @ b # inorder n @ c # inorder r"
   253 by(induct l a m b n c r rule: node42.induct) auto
   254 
   255 lemma inorder_node43: "height m > 0 \<Longrightarrow>
   256   inorder (tree\<^sub>d (node43 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder(tree\<^sub>d n) @ c # inorder r"
   257 by(induct l a m b n c r rule: node43.induct) auto
   258 
   259 lemma inorder_node44: "height n > 0 \<Longrightarrow>
   260   inorder (tree\<^sub>d (node44 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder n @ c # inorder (tree\<^sub>d r)"
   261 by(induct l a m b n c r rule: node44.induct) auto
   262 
   263 lemmas inorder_nodes = inorder_node21 inorder_node22
   264   inorder_node31 inorder_node32 inorder_node33
   265   inorder_node41 inorder_node42 inorder_node43 inorder_node44
   266 
   267 lemma split_minD:
   268   "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
   269   x # inorder(tree\<^sub>d t') = inorder t"
   270 by(induction t arbitrary: t' rule: split_min.induct)
   271   (auto simp: inorder_nodes split: prod.splits)
   272 
   273 lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   274   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   275 by(induction t rule: del.induct)
   276   (auto simp: inorder_nodes del_list_simps split_minD split!: if_split prod.splits)
   277   (* 30 secs (2016) *)
   278 
   279 lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   280   inorder(delete x t) = del_list x (inorder t)"
   281 by(simp add: delete_def inorder_del)
   282 
   283 
   284 subsection \<open>Balancedness\<close>
   285 
   286 subsubsection "Proofs for insert"
   287 
   288 text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close>
   289 
   290 instantiation up\<^sub>i :: (type)height
   291 begin
   292 
   293 fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
   294 "height (T\<^sub>i t) = height t" |
   295 "height (Up\<^sub>i l a r) = height l"
   296 
   297 instance ..
   298 
   299 end
   300 
   301 lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
   302 by (induct t) (auto split!: if_split up\<^sub>i.split)
   303 
   304 
   305 text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
   306 two properties (balance and height) are combined in one predicate.\<close>
   307 
   308 inductive full :: "nat \<Rightarrow> 'a tree234 \<Rightarrow> bool" where
   309 "full 0 Leaf" |
   310 "\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
   311 "\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)" |
   312 "\<lbrakk>full n l; full n m; full n m'; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node4 l p m q m' q' r)"
   313 
   314 inductive_cases full_elims:
   315   "full n Leaf"
   316   "full n (Node2 l p r)"
   317   "full n (Node3 l p m q r)"
   318   "full n (Node4 l p m q m' q' r)"
   319 
   320 inductive_cases full_0_elim: "full 0 t"
   321 inductive_cases full_Suc_elim: "full (Suc n) t"
   322 
   323 lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
   324   by (auto elim: full_0_elim intro: full.intros)
   325 
   326 lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
   327   by (auto elim: full_elims intro: full.intros)
   328 
   329 lemma full_Suc_Node2_iff [simp]:
   330   "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
   331   by (auto elim: full_elims intro: full.intros)
   332 
   333 lemma full_Suc_Node3_iff [simp]:
   334   "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
   335   by (auto elim: full_elims intro: full.intros)
   336 
   337 lemma full_Suc_Node4_iff [simp]:
   338   "full (Suc n) (Node4 l p m q m' q' r) \<longleftrightarrow> full n l \<and> full n m \<and> full n m' \<and> full n r"
   339   by (auto elim: full_elims intro: full.intros)
   340 
   341 lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   342   by (induct set: full, simp_all)
   343 
   344 lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
   345   by (induct set: full, auto dest: full_imp_height)
   346 
   347 lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
   348   by (induct t, simp_all)
   349 
   350 lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
   351   by (auto elim!: bal_imp_full full_imp_bal)
   352 
   353 text \<open>The @{const "insert"} function either preserves the height of the
   354 tree, or increases it by one. The constructor returned by the @{term
   355 "insert"} function determines which: A return value of the form @{term
   356 "T\<^sub>i t"} indicates that the height will be the same. A value of the
   357 form @{term "Up\<^sub>i l p r"} indicates an increase in height.\<close>
   358 
   359 primrec full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
   360 "full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
   361 "full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
   362 
   363 lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
   364 by (induct rule: full.induct) (auto, auto split: up\<^sub>i.split)
   365 
   366 text \<open>The @{const insert} operation preserves balance.\<close>
   367 
   368 lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
   369 unfolding bal_iff_full insert_def
   370 apply (erule exE)
   371 apply (drule full\<^sub>i_ins [of _ _ a])
   372 apply (cases "ins a t")
   373 apply (auto intro: full.intros)
   374 done
   375 
   376 
   377 subsubsection "Proofs for delete"
   378 
   379 instantiation up\<^sub>d :: (type)height
   380 begin
   381 
   382 fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
   383 "height (T\<^sub>d t) = height t" |
   384 "height (Up\<^sub>d t) = height t + 1"
   385 
   386 instance ..
   387 
   388 end
   389 
   390 lemma bal_tree\<^sub>d_node21:
   391   "\<lbrakk>bal r; bal (tree\<^sub>d l); height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l a r))"
   392 by(induct l a r rule: node21.induct) auto
   393 
   394 lemma bal_tree\<^sub>d_node22:
   395   "\<lbrakk>bal(tree\<^sub>d r); bal l; height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r))"
   396 by(induct l a r rule: node22.induct) auto
   397 
   398 lemma bal_tree\<^sub>d_node31:
   399   "\<lbrakk> bal (tree\<^sub>d l); bal m; bal r; height l = height r; height m = height r \<rbrakk>
   400   \<Longrightarrow> bal (tree\<^sub>d (node31 l a m b r))"
   401 by(induct l a m b r rule: node31.induct) auto
   402 
   403 lemma bal_tree\<^sub>d_node32:
   404   "\<lbrakk> bal l; bal (tree\<^sub>d m); bal r; height l = height r; height m = height r \<rbrakk>
   405   \<Longrightarrow> bal (tree\<^sub>d (node32 l a m b r))"
   406 by(induct l a m b r rule: node32.induct) auto
   407 
   408 lemma bal_tree\<^sub>d_node33:
   409   "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r); height l = height r; height m = height r \<rbrakk>
   410   \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r))"
   411 by(induct l a m b r rule: node33.induct) auto
   412 
   413 lemma bal_tree\<^sub>d_node41:
   414   "\<lbrakk> bal (tree\<^sub>d l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
   415   \<Longrightarrow> bal (tree\<^sub>d (node41 l a m b n c r))"
   416 by(induct l a m b n c r rule: node41.induct) auto
   417 
   418 lemma bal_tree\<^sub>d_node42:
   419   "\<lbrakk> bal l; bal (tree\<^sub>d m); bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
   420   \<Longrightarrow> bal (tree\<^sub>d (node42 l a m b n c r))"
   421 by(induct l a m b n c r rule: node42.induct) auto
   422 
   423 lemma bal_tree\<^sub>d_node43:
   424   "\<lbrakk> bal l; bal m; bal (tree\<^sub>d n); bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
   425   \<Longrightarrow> bal (tree\<^sub>d (node43 l a m b n c r))"
   426 by(induct l a m b n c r rule: node43.induct) auto
   427 
   428 lemma bal_tree\<^sub>d_node44:
   429   "\<lbrakk> bal l; bal m; bal n; bal (tree\<^sub>d r); height l = height r; height m = height r; height n = height r \<rbrakk>
   430   \<Longrightarrow> bal (tree\<^sub>d (node44 l a m b n c r))"
   431 by(induct l a m b n c r rule: node44.induct) auto
   432 
   433 lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
   434   bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
   435   bal_tree\<^sub>d_node41 bal_tree\<^sub>d_node42 bal_tree\<^sub>d_node43 bal_tree\<^sub>d_node44
   436 
   437 lemma height_node21:
   438    "height r > 0 \<Longrightarrow> height(node21 l a r) = max (height l) (height r) + 1"
   439 by(induct l a r rule: node21.induct)(simp_all add: max.assoc)
   440 
   441 lemma height_node22:
   442    "height l > 0 \<Longrightarrow> height(node22 l a r) = max (height l) (height r) + 1"
   443 by(induct l a r rule: node22.induct)(simp_all add: max.assoc)
   444 
   445 lemma height_node31:
   446   "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
   447    max (height l) (max (height m) (height r)) + 1"
   448 by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
   449 
   450 lemma height_node32:
   451   "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
   452    max (height l) (max (height m) (height r)) + 1"
   453 by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
   454 
   455 lemma height_node33:
   456   "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
   457    max (height l) (max (height m) (height r)) + 1"
   458 by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
   459 
   460 lemma height_node41:
   461   "height m > 0 \<Longrightarrow> height(node41 l a m b n c r) =
   462    max (height l) (max (height m) (max (height n) (height r))) + 1"
   463 by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def)
   464 
   465 lemma height_node42:
   466   "height l > 0 \<Longrightarrow> height(node42 l a m b n c r) =
   467    max (height l) (max (height m) (max (height n) (height r))) + 1"
   468 by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def)
   469 
   470 lemma height_node43:
   471   "height m > 0 \<Longrightarrow> height(node43 l a m b n c r) =
   472    max (height l) (max (height m) (max (height n) (height r))) + 1"
   473 by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def)
   474 
   475 lemma height_node44:
   476   "height n > 0 \<Longrightarrow> height(node44 l a m b n c r) =
   477    max (height l) (max (height m) (max (height n) (height r))) + 1"
   478 by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def)
   479 
   480 lemmas heights = height_node21 height_node22
   481   height_node31 height_node32 height_node33
   482   height_node41 height_node42 height_node43 height_node44
   483 
   484 lemma height_split_min:
   485   "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
   486 by(induct t arbitrary: x t' rule: split_min.induct)
   487   (auto simp: heights split: prod.splits)
   488 
   489 lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   490 by(induction x t rule: del.induct)
   491   (auto simp add: heights height_split_min split!: if_split prod.split)
   492 
   493 lemma bal_split_min:
   494   "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
   495 by(induct t arbitrary: x t' rule: split_min.induct)
   496   (auto simp: heights height_split_min bals split: prod.splits)
   497 
   498 lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   499 by(induction x t rule: del.induct)
   500   (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split)
   501 
   502 corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   503 by(simp add: delete_def bal_tree\<^sub>d_del)
   504 
   505 subsection \<open>Overall Correctness\<close>
   506 
   507 interpretation S: Set_by_Ordered
   508 where empty = empty and isin = isin and insert = insert and delete = delete
   509 and inorder = inorder and inv = bal
   510 proof (standard, goal_cases)
   511   case 2 thus ?case by(simp add: isin_set)
   512 next
   513   case 3 thus ?case by(simp add: inorder_insert)
   514 next
   515   case 4 thus ?case by(simp add: inorder_delete)
   516 next
   517   case 6 thus ?case by(simp add: bal_insert)
   518 next
   519   case 7 thus ?case by(simp add: bal_delete)
   520 qed (simp add: empty_def)+
   521 
   522 end