src/HOL/ex/Tree23.thy
author huffman
Fri Nov 04 07:37:37 2011 +0100 (2011-11-04)
changeset 45334 3f74e041e05c
parent 45333 04b21922ed68
child 45335 a68ce51de69a
permissions -rw-r--r--
ex/Tree23.thy: simplify proof of bal_add0
     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 text {* Ordered trees *}
   140 
   141 definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
   142   "opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))"
   143 
   144 lemma opt_less_simps [simp]:
   145   "opt_less None y = True"
   146   "opt_less x None = True"
   147   "opt_less (Some a) (Some b) = (a < b)"
   148 unfolding opt_less_def by (auto simp add: ord_def split: option.split)
   149 
   150 primrec ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
   151 "ord' x Empty y = opt_less x y" |
   152 "ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" |
   153 "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)"
   154 
   155 definition ord0 :: "'a tree23 \<Rightarrow> bool" where
   156   "ord0 t = ord' None t None"
   157 
   158 text {* Balanced trees *}
   159 
   160 inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
   161 "full 0 Empty" |
   162 "\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" |
   163 "\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)"
   164 
   165 inductive_cases full_elims:
   166   "full n Empty"
   167   "full n (Branch2 l p r)"
   168   "full n (Branch3 l p m q r)"
   169 
   170 inductive_cases full_0_elim: "full 0 t"
   171 inductive_cases full_Suc_elim: "full (Suc n) t"
   172 
   173 lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty"
   174   by (auto elim: full_0_elim intro: full.intros)
   175 
   176 lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0"
   177   by (auto elim: full_elims intro: full.intros)
   178 
   179 lemma full_Suc_Branch2_iff [simp]:
   180   "full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r"
   181   by (auto elim: full_elims intro: full.intros)
   182 
   183 lemma full_Suc_Branch3_iff [simp]:
   184   "full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
   185   by (auto elim: full_elims intro: full.intros)
   186 
   187 fun height :: "'a tree23 \<Rightarrow> nat" where
   188 "height Empty = 0" |
   189 "height (Branch2 l _ r) = Suc(max (height l) (height r))" |
   190 "height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
   191 
   192 text{* Is a tree balanced? *}
   193 fun bal :: "'a tree23 \<Rightarrow> bool" where
   194 "bal Empty = True" |
   195 "bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
   196 "bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
   197 
   198 lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   199   by (induct set: full, simp_all)
   200 
   201 lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
   202   by (induct set: full, auto dest: full_imp_height)
   203 
   204 lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
   205   by (induct t, simp_all)
   206 
   207 lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
   208   by (auto elim!: bal_imp_full full_imp_bal)
   209 
   210 text {* The @{term "add0"} function either preserves the height of the
   211 tree, or increases it by one. The constructor returned by the @{term
   212 "add"} function determines which: A return value of the form @{term
   213 "Stay t"} indicates that the height will be the same. A value of the
   214 form @{term "Sprout l p r"} indicates an increase in height. *}
   215 
   216 primrec gfull :: "nat \<Rightarrow> 'a growth \<Rightarrow> bool" where
   217 "gfull n (Stay t) \<longleftrightarrow> full n t" |
   218 "gfull n (Sprout l p r) \<longleftrightarrow> full n l \<and> full n r"
   219 
   220 lemma gfull_add: "full n t \<Longrightarrow> gfull n (add k y t)"
   221  apply (induct set: full)
   222    apply simp
   223   apply clarsimp
   224   apply (case_tac "ord k a")
   225     apply simp
   226     apply (case_tac "add k y l", simp, simp)
   227    apply simp
   228   apply simp
   229   apply (case_tac "add k y r", simp, simp)
   230  apply clarsimp
   231  apply (case_tac "ord k a")
   232    apply simp
   233    apply (case_tac "add k y l", simp, simp)
   234   apply simp
   235  apply simp
   236  apply (case_tac "ord k aa")
   237    apply simp
   238    apply (case_tac "add k y m", simp, simp)
   239   apply simp
   240  apply simp
   241  apply (case_tac "add k y r", simp, simp)
   242 done
   243 
   244 text {* The @{term "add0"} operation preserves balance. *}
   245 
   246 lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
   247 unfolding bal_iff_full add0_def
   248 apply (erule exE)
   249 apply (drule gfull_add [of _ _ k y])
   250 apply (cases "add k y t")
   251 apply (auto intro: full.intros)
   252 done
   253 
   254 text {* The @{term "add0"} operation preserves order. *}
   255 
   256 lemma ord_cases:
   257   fixes a b :: int obtains
   258   "ord a b = LESS" and "a < b" |
   259   "ord a b = EQUAL" and "a = b" |
   260   "ord a b = GREATER" and "a > b"
   261 unfolding ord_def by (rule linorder_cases [of a b]) auto
   262 
   263 definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
   264   "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
   265 
   266 lemma gtree_simps [simp]:
   267   "gtree (Stay t) = t"
   268   "gtree (Sprout l p r) = Branch2 l p r"
   269 unfolding gtree_def by simp_all
   270 
   271 lemma add0: "add0 k y t = gtree (add k y t)"
   272   unfolding add0_def by (simp split: growth.split)
   273 
   274 lemma ord'_add0:
   275   "\<lbrakk>ord' k1 t k2; opt_less k1 (Some k); opt_less (Some k) k2\<rbrakk> \<Longrightarrow> ord' k1 (add0 k y t) k2"
   276 unfolding add0
   277  apply (induct t arbitrary: k1 k2)
   278    apply simp
   279   apply clarsimp
   280   apply (rule_tac a=k and b=a in ord_cases)
   281     apply simp
   282     apply (case_tac "add k y t1", simp, simp)
   283    apply simp
   284   apply simp
   285   apply (case_tac "add k y t2", simp, simp)
   286  apply clarsimp
   287  apply (rule_tac a=k and b=a in ord_cases)
   288    apply simp
   289    apply (case_tac "add k y t1", simp, simp)
   290   apply simp
   291  apply simp
   292  apply (rule_tac a=k and b=aa in ord_cases)
   293    apply simp
   294    apply (case_tac "add k y t2", simp, simp)
   295   apply simp
   296  apply simp
   297  apply (case_tac "add k y t3", simp, simp)
   298 done
   299 
   300 lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
   301   by (simp add: ord0_def ord'_add0)
   302 
   303 text {* The @{term "del"} function preserves balance. *}
   304 
   305 lemma del_extra_simps:
   306 "l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
   307  del k (Branch2 l p r) = (case compare k p of
   308       LESS => (case del k l of None \<Rightarrow> None |
   309         Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
   310       | Some(p', (True, l')) => Some(p', case r of
   311           Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
   312         | Branch3 rl rp rm rq rr => (False, Branch2
   313             (Branch2 l' p rl) rp (Branch2 rm rq rr))))
   314     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   315         Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
   316       | Some(p', (True, r')) => Some(p', case l of
   317           Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
   318         | Branch3 ll lp lm lq lr => (False, Branch2
   319             (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))"
   320 "l \<noteq> Empty \<or> m \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
   321  del k (Branch3 l p m q r) = (case compare k q of
   322       LESS => (case compare k p of
   323         LESS => (case del k l of None \<Rightarrow> None |
   324           Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
   325         | Some(p', (True, l')) => Some(p', (False, case (m, r) of
   326             (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
   327           | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
   328           | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
   329               Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
   330       | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
   331           Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
   332         | Some(p', (True, m')) => Some(p', (False, case (l, r) of
   333             (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
   334           | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
   335           | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
   336     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   337         Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
   338       | Some(q', (True, r')) => Some(q', (False, case (l, m) of
   339           (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
   340         | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
   341         | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
   342             Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
   343 apply -
   344 apply (cases l, cases r, simp_all only: del.simps, simp)
   345 apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
   346 done
   347 
   348 definition
   349   "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')"
   350 
   351 lemmas ord_case = ord.exhaust [where y=y and P="ord_case a b c y", standard]
   352 lemmas option_ord_case = ord.exhaust [where y=y and P="option_case a b (ord_case d e f y)", standard]
   353 lemmas option_option_case = option.exhaust [where y=y and P="option_case a b (option_case d e y)", standard]
   354 lemmas option_prod_case = prod.exhaust [where y=y and P="option_case a b (prod_case c y)", standard]
   355 lemmas option_bool_case = bool.exhaust [where y=y and P="option_case a b (bool_case c d y)", standard]
   356 lemmas prod_tree23_case = tree23.exhaust [where y=y and P="prod_case a (tree23_case b c d y)", standard]
   357 lemmas option_case = option.exhaust [where y=y and P="option_case a b y", standard]
   358 lemmas full_tree23_case = tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
   359 
   360 lemmas case_intros =
   361   option_ord_case option_option_case option_prod_case option_bool_case prod_tree23_case option_case
   362   full_tree23_case
   363 
   364 lemma full_del: "full (Suc n) t \<Longrightarrow> full_del n k t"
   365 proof -
   366   { fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k
   367     assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
   368     and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
   369     and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
   370     and "full (Suc n) (Branch2 l p r)"
   371     hence "full_del n k (Branch2 l p r)"
   372      apply clarsimp
   373      apply (cases n)
   374       apply (cases k)
   375        apply (simp add: full_del_def)
   376       apply (simp add: full_del_def split: ord.split)
   377      apply (simp add: full_del_def)
   378      apply (subst del_extra_simps, force)
   379      apply (simp | rule case_intros)+
   380      done
   381   } note A = this
   382   { fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k
   383     assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
   384     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"
   385     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"
   386     and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
   387     and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
   388     and "full (Suc n) (Branch3 l p m q r)"
   389     hence "full_del n k (Branch3 l p m q r)"
   390      apply clarsimp
   391      apply (cases n)
   392       apply (cases k)
   393        apply (simp add: full_del_def)
   394       apply (simp add: full_del_def split: ord.split)
   395      apply (simp add: full_del_def)
   396      apply (subst del_extra_simps, force)
   397      apply (simp | rule case_intros)+
   398      done
   399   } note B = this
   400   show "full (Suc n) t \<Longrightarrow> full_del n k t"
   401   proof (induct k t arbitrary: n rule: del.induct)
   402     { case goal1 thus "full_del n (Some k) Empty"
   403         by simp }
   404     { case goal2 thus "full_del n None (Branch2 Empty p Empty)"
   405         unfolding full_del_def by auto }
   406     { case goal3 thus "full_del n None (Branch3 Empty p Empty q Empty)"
   407         unfolding full_del_def by auto }
   408     { case goal4 thus "full_del n (Some v) (Branch2 Empty p Empty)"
   409         unfolding full_del_def by (auto split: ord.split) }
   410     { case goal5 thus "full_del n (Some v) (Branch3 Empty p Empty q Empty)"
   411         unfolding full_del_def by (auto split: ord.split) }
   412     { case goal26 thus ?case by simp }
   413   qed (fact A | fact B)+
   414 qed
   415 
   416 lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
   417   unfolding del0_def
   418   apply (drule bal_imp_full)
   419   apply (case_tac "height t", simp, simp)
   420   apply (frule full_del [where k="Some k"])
   421   apply (simp add: full_del_def)
   422   apply (auto split: option.split elim: full_imp_bal)
   423   done
   424 
   425 text{* This is a little test harness and should be commented out once the
   426 above functions have been proved correct. *}
   427 
   428 datatype 'a act = Add int 'a | Del int
   429 
   430 fun exec where
   431 "exec [] t = t" |
   432 "exec (Add k x # as) t = exec as (add0 k x t)" |
   433 "exec (Del k # as) t = exec as (del0 k t)"
   434 
   435 text{* Some quick checks: *}
   436 
   437 lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)"
   438   by (induct as t arbitrary: t rule: exec.induct,
   439     simp_all add: bal_add0 bal_del0)
   440 
   441 lemma "bal(exec as Empty)"
   442   by (simp add: bal_exec)
   443 
   444 lemma "ord0(exec as Empty)"
   445 quickcheck
   446 oops
   447 
   448 end