src/HOL/ex/Tree23.thy
author huffman
Thu Nov 03 17:40:50 2011 +0100 (2011-11-03)
changeset 45332 ede9dc025150
parent 45325 26b6179b5a45
child 45333 04b21922ed68
permissions -rw-r--r--
ex/Tree23.thy: prove that deletion preserves balance
     1 (*  Title:      HOL/ex/Tree23.thy
     2     Author:     Tobias Nipkow, TU Muenchen
     3 *)
     4 
     5 header {* 2-3 Trees *}
     6 
     7 theory Tree23
     8 imports Main
     9 begin
    10 
    11 text{* This is a very direct translation of some of the functions in table.ML
    12 in the Isabelle source code. That source is due to Makarius Wenzel and Stefan
    13 Berghofer.
    14 
    15 So far this file contains only data types and functions, but no proofs. Feel
    16 free to have a go at the latter!
    17 
    18 Note that because of complicated patterns and mutual recursion, these
    19 function definitions take a few minutes and can also be seen as stress tests
    20 for the function definition facility.  *}
    21 
    22 type_synonym key = int -- {*for simplicity, should be a type class*}
    23 
    24 datatype ord = LESS | EQUAL | GREATER
    25 
    26 definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)"
    27 
    28 datatype 'a tree23 =
    29   Empty |
    30   Branch2 "'a tree23" "key * 'a" "'a tree23" |
    31   Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23"
    32 
    33 datatype 'a growth =
    34   Stay "'a tree23" |
    35   Sprout "'a tree23" "key * 'a" "'a tree23"
    36 
    37 fun add :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a growth" where
    38 "add key y Empty = Sprout Empty (key,y) Empty" |
    39 "add key y (Branch2 left (k,x) right) =
    40    (case ord key k of
    41       LESS =>
    42         (case add key y left of
    43            Stay left' => Stay (Branch2 left' (k,x) right)
    44          | Sprout left1 q left2
    45            => Stay (Branch3 left1 q left2 (k,x) right))
    46     | EQUAL => Stay (Branch2 left (k,y) right)
    47     | GREATER =>
    48         (case add key y right of
    49            Stay right' => Stay (Branch2 left (k,x) right')
    50          | Sprout right1 q right2
    51            => Stay (Branch3 left (k,x) right1 q right2)))" |
    52 "add key y (Branch3 left (k1,x1) mid (k2,x2) right) =
    53    (case ord key k1 of
    54       LESS =>
    55         (case add key y left of
    56            Stay left' => Stay (Branch3 left' (k1,x1) mid (k2,x2) right)
    57          | Sprout left1 q left2
    58            => Sprout (Branch2 left1 q left2) (k1,x1) (Branch2 mid (k2,x2) right))
    59     | EQUAL => Stay (Branch3 left (k1,y) mid (k2,x2) right)
    60     | GREATER =>
    61         (case ord key k2 of
    62            LESS =>
    63              (case add key y mid of
    64                 Stay mid' => Stay (Branch3 left (k1,x1) mid' (k2,x2) right)
    65               | Sprout mid1 q mid2
    66                 => Sprout (Branch2 left (k1,x1) mid1) q (Branch2 mid2 (k2,x2) right))
    67          | EQUAL => Stay (Branch3 left (k1,x1) mid (k2,y) right)
    68          | GREATER =>
    69              (case add key y right of
    70                 Stay right' => Stay (Branch3 left (k1,x1) mid (k2,x2) right')
    71               | Sprout right1 q right2
    72                 => Sprout (Branch2 left (k1,x1) mid) (k2,x2) (Branch2 right1 q right2))))"
    73 
    74 definition add0 :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    75 "add0 k y t =
    76   (case add k y t of Stay t' => t' | Sprout l p r => Branch2 l p r)"
    77 
    78 value "add0 5 e (add0 4 d (add0 3 c (add0 2 b (add0 1 a Empty))))"
    79 
    80 fun compare where
    81 "compare None (k2, _) = LESS" |
    82 "compare (Some k1) (k2, _) = ord k1 k2"
    83 
    84 fun if_eq where
    85 "if_eq EQUAL x y = x" |
    86 "if_eq _ x y = y"
    87 
    88 fun del :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> ((key * 'a) * bool * 'a tree23)option"
    89 where
    90 "del (Some k) Empty = None" |
    91 "del None (Branch2 Empty p Empty) = Some(p, (True, Empty))" |
    92 "del None (Branch3 Empty p Empty q Empty) = Some(p, (False, Branch2 Empty q Empty))" |
    93 "del k (Branch2 Empty p Empty) = (case compare k p of
    94       EQUAL => Some(p, (True, Empty)) | _ => None)" |
    95 "del k (Branch3 Empty p Empty q Empty) = (case compare k p of
    96       EQUAL => Some(p, (False, Branch2 Empty q Empty))
    97     | _ => (case compare k q of
    98         EQUAL => Some(q, (False, Branch2 Empty p Empty))
    99       | _ => None))" |
   100 "del k (Branch2 l p r) = (case compare k p of
   101       LESS => (case del k l of None \<Rightarrow> None |
   102         Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
   103       | Some(p', (True, l')) => Some(p', case r of
   104           Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
   105         | Branch3 rl rp rm rq rr => (False, Branch2
   106             (Branch2 l' p rl) rp (Branch2 rm rq rr))))
   107     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   108         Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
   109       | Some(p', (True, r')) => Some(p', case l of
   110           Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
   111         | Branch3 ll lp lm lq lr => (False, Branch2
   112             (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))" |
   113 "del k (Branch3 l p m q r) = (case compare k q of
   114       LESS => (case compare k p of
   115         LESS => (case del k l of None \<Rightarrow> None |
   116           Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
   117         | Some(p', (True, l')) => Some(p', (False, case (m, r) of
   118             (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
   119           | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
   120           | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
   121               Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
   122       | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
   123           Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
   124         | Some(p', (True, m')) => Some(p', (False, case (l, r) of
   125             (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
   126           | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
   127           | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
   128     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   129         Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
   130       | Some(q', (True, r')) => Some(q', (False, case (l, m) of
   131           (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
   132         | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
   133         | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
   134             Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
   135 
   136 definition del0 :: "key \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   137 "del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"
   138 
   139 
   140 (* yes, this is rather slow *)
   141 fun ord0 :: "'a tree23 \<Rightarrow> bool"
   142 and ordl :: "key \<Rightarrow> 'a tree23 \<Rightarrow> bool"
   143 and ordr :: "'a tree23 \<Rightarrow> key \<Rightarrow> bool"
   144 and ordlr :: "key \<Rightarrow> 'a tree23 \<Rightarrow> key \<Rightarrow> bool"
   145 where
   146 "ord0 Empty = True" |
   147 "ord0 (Branch2 l p r)  = (ordr l (fst p) & ordl (fst p) r)" |
   148 "ord0 (Branch3 l p m q r)  = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
   149 
   150 "ordl _ Empty = True" |
   151 "ordl x (Branch2 l p r)  = (ordlr x l (fst p) & ordl (fst p) r)" |
   152 "ordl x (Branch3 l p m q r)  = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
   153 
   154 "ordr Empty _ = True" |
   155 "ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" |
   156 "ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" |
   157 
   158 "ordlr x Empty y = (x < y)" |
   159 "ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" |
   160 "ordlr x (Branch3 l p m q r) y = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r y)"
   161 
   162 definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
   163   "opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))"
   164 
   165 lemma opt_less_simps [simp]:
   166   "opt_less None y = True"
   167   "opt_less x None = True"
   168   "opt_less (Some a) (Some b) = (a < b)"
   169 unfolding opt_less_def by (auto simp add: ord_def split: option.split)
   170 
   171 fun ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
   172 "ord' x Empty y = opt_less x y" |
   173 "ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" |
   174 "ord' x (Branch3 l p m q r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) m (Some (fst q)) & ord' (Some (fst q)) r y)"
   175 
   176 lemma ord':
   177   "ord' x t y = (case x of None \<Rightarrow> (case y of None \<Rightarrow> ord0 t | Some y' \<Rightarrow> ordr t y')
   178     | Some x' \<Rightarrow> (case y of None \<Rightarrow> ordl x' t | Some y' \<Rightarrow> ordlr x' t y'))"
   179 by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split)
   180 
   181 fun height :: "'a tree23 \<Rightarrow> nat" where
   182 "height Empty = 0" |
   183 "height (Branch2 l _ r) = Suc(max (height l) (height r))" |
   184 "height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
   185 
   186 text{* Is a tree balanced? *}
   187 fun bal :: "'a tree23 \<Rightarrow> bool" where
   188 "bal Empty = True" |
   189 "bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
   190 "bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
   191 
   192 text {* The @{term "add0"} function either preserves the height of the
   193 tree, or increases it by one. The constructor returned by the @{term
   194 "add"} function determines which: A return value of the form @{term
   195 "Stay t"} indicates that the height will be the same. A value of the
   196 form @{term "Sprout l p r"} indicates an increase in height. *}
   197 
   198 fun gheight :: "'a growth \<Rightarrow> nat" where
   199 "gheight (Stay t) = height t" |
   200 "gheight (Sprout l p r) = max (height l) (height r)"
   201 
   202 lemma gheight_add: "gheight (add k y t) = height t"
   203  apply (induct t)
   204    apply simp
   205   apply clarsimp
   206   apply (case_tac "ord k a")
   207     apply simp
   208     apply (case_tac "add k y t1", simp, simp)
   209    apply simp
   210   apply simp
   211   apply (case_tac "add k y t2", simp, simp)
   212  apply clarsimp
   213  apply (case_tac "ord k a")
   214    apply simp
   215    apply (case_tac "add k y t1", simp, simp)
   216   apply simp
   217  apply simp
   218  apply (case_tac "ord k aa")
   219    apply simp
   220    apply (case_tac "add k y t2", simp, simp)
   221   apply simp
   222  apply simp
   223  apply (case_tac "add k y t3", simp, simp)
   224 done
   225 
   226 lemma add_eq_Stay_dest: "add k y t = Stay t' \<Longrightarrow> height t = height t'"
   227   using gheight_add [of k y t] by simp
   228 
   229 lemma add_eq_Sprout_dest: "add k y t = Sprout l p r \<Longrightarrow> height t = max (height l) (height r)"
   230   using gheight_add [of k y t] by simp
   231 
   232 definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
   233   "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
   234 
   235 lemma gtree_simps [simp]:
   236   "gtree (Stay t) = t"
   237   "gtree (Sprout l p r) = Branch2 l p r"
   238 unfolding gtree_def by simp_all
   239 
   240 lemma add0: "add0 k y t = gtree (add k y t)"
   241   unfolding add0_def by (simp split: growth.split)
   242 
   243 text {* The @{term "add0"} operation preserves balance. *}
   244 
   245 lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
   246 unfolding add0
   247  apply (induct t)
   248    apply simp
   249   apply clarsimp
   250   apply (case_tac "ord k a")
   251     apply simp
   252     apply (case_tac "add k y t1")
   253      apply (simp, drule add_eq_Stay_dest, simp)
   254     apply (simp, drule add_eq_Sprout_dest, simp)
   255    apply simp
   256   apply simp
   257   apply (case_tac "add k y t2")
   258    apply (simp, drule add_eq_Stay_dest, simp)
   259   apply (simp, drule add_eq_Sprout_dest, simp)
   260  apply clarsimp
   261  apply (case_tac "ord k a")
   262    apply simp
   263    apply (case_tac "add k y t1")
   264     apply (simp, drule add_eq_Stay_dest, simp)
   265    apply (simp, drule add_eq_Sprout_dest, simp)
   266   apply simp
   267  apply simp
   268  apply (case_tac "ord k aa")
   269    apply simp
   270    apply (case_tac "add k y t2")
   271     apply (simp, drule add_eq_Stay_dest, simp)
   272    apply (simp, drule add_eq_Sprout_dest, simp)
   273   apply simp
   274  apply simp
   275  apply (case_tac "add k y t3")
   276   apply (simp, drule add_eq_Stay_dest, simp)
   277  apply (simp, drule add_eq_Sprout_dest, simp)
   278 done
   279 
   280 text {* The @{term "add0"} operation preserves order. *}
   281 
   282 lemma ord_cases:
   283   fixes a b :: int obtains
   284   "ord a b = LESS" and "a < b" |
   285   "ord a b = EQUAL" and "a = b" |
   286   "ord a b = GREATER" and "a > b"
   287 unfolding ord_def by (rule linorder_cases [of a b]) auto
   288 
   289 lemma ord'_add0:
   290   "\<lbrakk>ord' k1 t k2; opt_less k1 (Some k); opt_less (Some k) k2\<rbrakk> \<Longrightarrow> ord' k1 (add0 k y t) k2"
   291 unfolding add0
   292  apply (induct t arbitrary: k1 k2)
   293    apply simp
   294   apply clarsimp
   295   apply (rule_tac a=k and b=a in ord_cases)
   296     apply simp
   297     apply (case_tac "add k y t1", simp, simp)
   298    apply simp
   299   apply simp
   300   apply (case_tac "add k y t2", simp, simp)
   301  apply clarsimp
   302  apply (rule_tac a=k and b=a in ord_cases)
   303    apply simp
   304    apply (case_tac "add k y t1", simp, simp)
   305   apply simp
   306  apply simp
   307  apply (rule_tac a=k and b=aa in ord_cases)
   308    apply simp
   309    apply (case_tac "add k y t2", simp, simp)
   310   apply simp
   311  apply simp
   312  apply (case_tac "add k y t3", simp, simp)
   313 done
   314 
   315 lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
   316 using ord'_add0 [of None t None k y] by (simp add: ord')
   317 
   318 text {* The @{term "del"} function preserves balance. *}
   319 
   320 lemma del_extra_simps:
   321 "l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
   322  del k (Branch2 l p r) = (case compare k p of
   323       LESS => (case del k l of None \<Rightarrow> None |
   324         Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
   325       | Some(p', (True, l')) => Some(p', case r of
   326           Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
   327         | Branch3 rl rp rm rq rr => (False, Branch2
   328             (Branch2 l' p rl) rp (Branch2 rm rq rr))))
   329     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   330         Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
   331       | Some(p', (True, r')) => Some(p', case l of
   332           Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
   333         | Branch3 ll lp lm lq lr => (False, Branch2
   334             (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))"
   335 "l \<noteq> Empty \<or> m \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
   336  del k (Branch3 l p m q r) = (case compare k q of
   337       LESS => (case compare k p of
   338         LESS => (case del k l of None \<Rightarrow> None |
   339           Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
   340         | Some(p', (True, l')) => Some(p', (False, case (m, r) of
   341             (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
   342           | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
   343           | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
   344               Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
   345       | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
   346           Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
   347         | Some(p', (True, m')) => Some(p', (False, case (l, r) of
   348             (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
   349           | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
   350           | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
   351     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   352         Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
   353       | Some(q', (True, r')) => Some(q', (False, case (l, m) of
   354           (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
   355         | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
   356         | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
   357             Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
   358 apply -
   359 apply (cases l, cases r, simp_all only: del.simps, simp)
   360 apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
   361 done
   362 
   363 inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
   364 "full 0 Empty" |
   365 "\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" |
   366 "\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)"
   367 
   368 inductive_cases full_elims:
   369   "full n Empty"
   370   "full n (Branch2 l p r)"
   371   "full n (Branch3 l p m q r)"
   372 
   373 inductive_cases full_0_elim: "full 0 t"
   374 inductive_cases full_Suc_elim: "full (Suc n) t"
   375 
   376 lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty"
   377   by (auto elim: full_0_elim intro: full.intros)
   378 
   379 lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0"
   380   by (auto elim: full_elims intro: full.intros)
   381 
   382 lemma full_Suc_Branch2_iff [simp]:
   383   "full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r"
   384   by (auto elim: full_elims intro: full.intros)
   385 
   386 lemma full_Suc_Branch3_iff [simp]:
   387   "full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
   388   by (auto elim: full_elims intro: full.intros)
   389 
   390 definition
   391   "full_del n k t = (case del k t of None \<Rightarrow> True | Some (p, b, t') \<Rightarrow> full (if b then n else Suc n) t')"
   392 
   393 lemmas ord_case = ord.exhaust [where y=y and P="ord_case a b c y", standard]
   394 lemmas option_ord_case = ord.exhaust [where y=y and P="option_case a b (ord_case d e f y)", standard]
   395 lemmas option_option_case = option.exhaust [where y=y and P="option_case a b (option_case d e y)", standard]
   396 lemmas option_prod_case = prod.exhaust [where y=y and P="option_case a b (prod_case c y)", standard]
   397 lemmas option_bool_case = bool.exhaust [where y=y and P="option_case a b (bool_case c d y)", standard]
   398 lemmas prod_tree23_case = tree23.exhaust [where y=y and P="prod_case a (tree23_case b c d y)", standard]
   399 lemmas option_case = option.exhaust [where y=y and P="option_case a b y", standard]
   400 lemmas full_tree23_case = tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
   401 
   402 lemmas case_intros =
   403   option_ord_case option_option_case option_prod_case option_bool_case prod_tree23_case option_case
   404   full_tree23_case
   405 
   406 lemma full_del: "full (Suc n) t \<Longrightarrow> full_del n k t"
   407 proof -
   408   { fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k
   409     assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
   410     and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
   411     and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
   412     and "full (Suc n) (Branch2 l p r)"
   413     hence "full_del n k (Branch2 l p r)"
   414      apply clarsimp
   415      apply (cases n)
   416       apply (cases k)
   417        apply (simp add: full_del_def)
   418       apply (simp add: full_del_def split: ord.split)
   419      apply (simp add: full_del_def)
   420      apply (subst del_extra_simps, force)
   421      apply (simp | rule case_intros)+
   422      done
   423   } note A = this
   424   { fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k
   425     assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
   426     and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = EQUAL; full (Suc n) m\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) m"
   427     and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = GREATER; full (Suc n) m\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) m"
   428     and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
   429     and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
   430     and "full (Suc n) (Branch3 l p m q r)"
   431     hence "full_del n k (Branch3 l p m q r)"
   432      apply clarsimp
   433      apply (cases n)
   434       apply (cases k)
   435        apply (simp add: full_del_def)
   436       apply (simp add: full_del_def split: ord.split)
   437      apply (simp add: full_del_def)
   438      apply (subst del_extra_simps, force)
   439      apply (simp | rule case_intros)+
   440      done
   441   } note B = this
   442   show "full (Suc n) t \<Longrightarrow> full_del n k t"
   443   proof (induct k t arbitrary: n rule: del.induct)
   444     { case goal1 thus "full_del n (Some k) Empty"
   445         by simp }
   446     { case goal2 thus "full_del n None (Branch2 Empty p Empty)"
   447         unfolding full_del_def by auto }
   448     { case goal3 thus "full_del n None (Branch3 Empty p Empty q Empty)"
   449         unfolding full_del_def by auto }
   450     { case goal4 thus "full_del n (Some v) (Branch2 Empty p Empty)"
   451         unfolding full_del_def by (auto split: ord.split) }
   452     { case goal5 thus "full_del n (Some v) (Branch3 Empty p Empty q Empty)"
   453         unfolding full_del_def by (auto split: ord.split) }
   454     { case goal26 thus ?case by simp }
   455   qed (fact A | fact B)+
   456 qed
   457 
   458 lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   459   by (induct set: full, simp_all)
   460 
   461 lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
   462   by (induct set: full, auto dest: full_imp_height)
   463 
   464 lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
   465   by (induct t, simp_all)
   466 
   467 lemma bal_iff_full: "bal t \<longleftrightarrow> full (height t) t"
   468   using bal_imp_full full_imp_bal ..
   469 
   470 lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
   471   unfolding del0_def
   472   apply (drule bal_imp_full)
   473   apply (case_tac "height t", simp, simp)
   474   apply (frule full_del [where k="Some k"])
   475   apply (simp add: full_del_def)
   476   apply (auto split: option.split elim: full_imp_bal)
   477   done
   478 
   479 text{* This is a little test harness and should be commented out once the
   480 above functions have been proved correct. *}
   481 
   482 datatype 'a act = Add int 'a | Del int
   483 
   484 fun exec where
   485 "exec [] t = t" |
   486 "exec (Add k x # as) t = exec as (add0 k x t)" |
   487 "exec (Del k # as) t = exec as (del0 k t)"
   488 
   489 text{* Some quick checks: *}
   490 
   491 lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)"
   492   by (induct as t arbitrary: t rule: exec.induct,
   493     simp_all add: bal_add0 bal_del0)
   494 
   495 lemma "bal(exec as Empty)"
   496   by (simp add: bal_exec)
   497 
   498 lemma "ord0(exec as Empty)"
   499 quickcheck
   500 oops
   501 
   502 end