src/HOL/ex/Tree23.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     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 by (induct set: full, auto split: ord.split growth.split)
   222 
   223 text {* The @{term "add0"} operation preserves balance. *}
   224 
   225 lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
   226 unfolding bal_iff_full add0_def
   227 apply (erule exE)
   228 apply (drule gfull_add [of _ _ k y])
   229 apply (cases "add k y t")
   230 apply (auto intro: full.intros)
   231 done
   232 
   233 text {* The @{term "add0"} operation preserves order. *}
   234 
   235 lemma ord_cases:
   236   fixes a b :: int obtains
   237   "ord a b = LESS" and "a < b" |
   238   "ord a b = EQUAL" and "a = b" |
   239   "ord a b = GREATER" and "a > b"
   240 unfolding ord_def by (rule linorder_cases [of a b]) auto
   241 
   242 definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
   243   "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
   244 
   245 lemma gtree_simps [simp]:
   246   "gtree (Stay t) = t"
   247   "gtree (Sprout l p r) = Branch2 l p r"
   248 unfolding gtree_def by simp_all
   249 
   250 lemma add0: "add0 k y t = gtree (add k y t)"
   251   unfolding add0_def by (simp split: growth.split)
   252 
   253 lemma ord'_add0:
   254   "\<lbrakk>ord' k1 t k2; opt_less k1 (Some k); opt_less (Some k) k2\<rbrakk> \<Longrightarrow> ord' k1 (add0 k y t) k2"
   255 unfolding add0
   256  apply (induct t arbitrary: k1 k2)
   257    apply simp
   258   apply clarsimp
   259   apply (rule_tac a=k and b=a in ord_cases)
   260     apply simp
   261     apply (case_tac "add k y t1", simp, simp)
   262    apply simp
   263   apply simp
   264   apply (case_tac "add k y t2", simp, simp)
   265  apply clarsimp
   266  apply (rule_tac a=k and b=a in ord_cases)
   267    apply simp
   268    apply (case_tac "add k y t1", simp, simp)
   269   apply simp
   270  apply simp
   271  apply (rule_tac a=k and b=aa in ord_cases)
   272    apply simp
   273    apply (case_tac "add k y t2", simp, simp)
   274   apply simp
   275  apply simp
   276  apply (case_tac "add k y t3", simp, simp)
   277 done
   278 
   279 lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
   280   by (simp add: ord0_def ord'_add0)
   281 
   282 text {* The @{term "del"} function preserves balance. *}
   283 
   284 lemma del_extra_simps:
   285 "l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
   286  del k (Branch2 l p r) = (case compare k p of
   287       LESS => (case del k l of None \<Rightarrow> None |
   288         Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
   289       | Some(p', (True, l')) => Some(p', case r of
   290           Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
   291         | Branch3 rl rp rm rq rr => (False, Branch2
   292             (Branch2 l' p rl) rp (Branch2 rm rq rr))))
   293     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   294         Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
   295       | Some(p', (True, r')) => Some(p', case l of
   296           Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
   297         | Branch3 ll lp lm lq lr => (False, Branch2
   298             (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))"
   299 "l \<noteq> Empty \<or> m \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
   300  del k (Branch3 l p m q r) = (case compare k q of
   301       LESS => (case compare k p of
   302         LESS => (case del k l of None \<Rightarrow> None |
   303           Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
   304         | Some(p', (True, l')) => Some(p', (False, case (m, r) of
   305             (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
   306           | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
   307           | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
   308               Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
   309       | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
   310           Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
   311         | Some(p', (True, m')) => Some(p', (False, case (l, r) of
   312             (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
   313           | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
   314           | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
   315     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   316         Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
   317       | Some(q', (True, r')) => Some(q', (False, case (l, m) of
   318           (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
   319         | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
   320         | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
   321             Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
   322 apply -
   323 apply (cases l, cases r, simp_all only: del.simps, simp)
   324 apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
   325 done
   326 
   327 fun dfull where
   328 "dfull n None \<longleftrightarrow> True" |
   329 "dfull n (Some (p, (True, t'))) \<longleftrightarrow> full n t'" |
   330 "dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
   331 
   332 lemmas dfull_case_intros =
   333   ord.exhaust [of y "dfull a (case_ord b c d y)"]
   334   option.exhaust [of y "dfull a (case_option b c y)"]
   335   prod.exhaust [of y "dfull a (case_prod b y)"]
   336   bool.exhaust [of y "dfull a (case_bool b c y)"]
   337   tree23.exhaust [of y "dfull a (Some (b, case_tree23 c d e y))"]
   338   tree23.exhaust [of y "full a (case_tree23 b c d y)"]
   339   for a b c d e y
   340 
   341 lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
   342 proof -
   343   { fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k
   344     assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
   345     and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
   346     and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
   347     and "full (Suc n) (Branch2 l p r)"
   348     hence "dfull n (del k (Branch2 l p r))"
   349      apply clarsimp
   350      apply (cases n)
   351       apply (cases k)
   352        apply simp
   353       apply (simp split: ord.split)
   354      apply simp
   355      apply (subst del_extra_simps, force)
   356      (* This should work, but it is way too slow!
   357      apply (force split: ord.split option.split bool.split tree23.split) *)
   358      apply (simp | rule dfull_case_intros)+
   359      done
   360   } note A = this
   361   { fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k
   362     assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
   363     and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = EQUAL; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) m)"
   364     and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = GREATER; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) m)"
   365     and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
   366     and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
   367     and "full (Suc n) (Branch3 l p m q r)"
   368     hence "dfull n (del k (Branch3 l p m q r))"
   369      apply clarsimp
   370      apply (cases n)
   371       apply (cases k)
   372        apply simp
   373       apply (simp split: ord.split)
   374      apply simp
   375      apply (subst del_extra_simps, force)
   376      apply (simp | rule dfull_case_intros)+
   377      done
   378   } note B = this
   379   show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
   380   proof (induct k t arbitrary: n rule: del.induct)
   381     { case goal1 thus "dfull n (del (Some k) Empty)" by simp }
   382     { case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp }
   383     { case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))"
   384         by simp }
   385     { case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
   386         by (simp split: ord.split) }
   387     { case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
   388         by (simp split: ord.split) }
   389     { case goal26 thus ?case by simp }
   390   qed (fact A | fact B)+
   391 qed
   392 
   393 lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
   394 unfolding bal_iff_full del0_def
   395 apply (erule exE)
   396 apply (case_tac n, simp, simp)
   397 apply (frule dfull_del [where k="Some k"])
   398 apply (cases "del (Some k) t", force)
   399 apply (rename_tac a, case_tac "a", rename_tac b t', case_tac "b", auto)
   400 done
   401 
   402 text{* This is a little test harness and should be commented out once the
   403 above functions have been proved correct. *}
   404 
   405 datatype 'a act = Add int 'a | Del int
   406 
   407 fun exec where
   408 "exec [] t = t" |
   409 "exec (Add k x # as) t = exec as (add0 k x t)" |
   410 "exec (Del k # as) t = exec as (del0 k t)"
   411 
   412 text{* Some quick checks: *}
   413 
   414 lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)"
   415   by (induct as t arbitrary: t rule: exec.induct,
   416     simp_all add: bal_add0 bal_del0)
   417 
   418 lemma "bal(exec as Empty)"
   419   by (simp add: bal_exec)
   420 
   421 lemma "ord0(exec as Empty)"
   422 quickcheck
   423 oops
   424 
   425 end