ex/Tree23.thy: simplify proof of bal_del0
authorhuffman
Fri Nov 04 08:00:48 2011 +0100 (2011-11-04)
changeset 45335a68ce51de69a
parent 45334 3f74e041e05c
child 45336 f502f4393054
ex/Tree23.thy: simplify proof of bal_del0
src/HOL/ex/Tree23.thy
     1.1 --- a/src/HOL/ex/Tree23.thy	Fri Nov 04 07:37:37 2011 +0100
     1.2 +++ b/src/HOL/ex/Tree23.thy	Fri Nov 04 08:00:48 2011 +0100
     1.3 @@ -345,82 +345,77 @@
     1.4  apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
     1.5  done
     1.6  
     1.7 -definition
     1.8 -  "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')"
     1.9 +fun dfull where
    1.10 +"dfull n None \<longleftrightarrow> True" |
    1.11 +"dfull n (Some (p, (True, t'))) \<longleftrightarrow> full n t'" |
    1.12 +"dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
    1.13  
    1.14 -lemmas ord_case = ord.exhaust [where y=y and P="ord_case a b c y", standard]
    1.15 -lemmas option_ord_case = ord.exhaust [where y=y and P="option_case a b (ord_case d e f y)", standard]
    1.16 -lemmas option_option_case = option.exhaust [where y=y and P="option_case a b (option_case d e y)", standard]
    1.17 -lemmas option_prod_case = prod.exhaust [where y=y and P="option_case a b (prod_case c y)", standard]
    1.18 -lemmas option_bool_case = bool.exhaust [where y=y and P="option_case a b (bool_case c d y)", standard]
    1.19 -lemmas prod_tree23_case = tree23.exhaust [where y=y and P="prod_case a (tree23_case b c d y)", standard]
    1.20 -lemmas option_case = option.exhaust [where y=y and P="option_case a b y", standard]
    1.21 -lemmas full_tree23_case = tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
    1.22 +lemmas dfull_case_intros =
    1.23 +  ord.exhaust [where y=y and P="dfull a (ord_case b c d y)", standard]
    1.24 +  option.exhaust [where y=y and P="dfull a (option_case b c y)", standard]
    1.25 +  prod.exhaust [where y=y and P="dfull a (prod_case b y)", standard]
    1.26 +  bool.exhaust [where y=y and P="dfull a (bool_case b c y)", standard]
    1.27 +  tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))", standard]
    1.28 +  tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
    1.29  
    1.30 -lemmas case_intros =
    1.31 -  option_ord_case option_option_case option_prod_case option_bool_case prod_tree23_case option_case
    1.32 -  full_tree23_case
    1.33 -
    1.34 -lemma full_del: "full (Suc n) t \<Longrightarrow> full_del n k t"
    1.35 +lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
    1.36  proof -
    1.37    { fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k
    1.38 -    assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
    1.39 -    and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
    1.40 -    and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
    1.41 +    assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
    1.42 +    and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
    1.43 +    and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
    1.44      and "full (Suc n) (Branch2 l p r)"
    1.45 -    hence "full_del n k (Branch2 l p r)"
    1.46 +    hence "dfull n (del k (Branch2 l p r))"
    1.47       apply clarsimp
    1.48       apply (cases n)
    1.49        apply (cases k)
    1.50 -       apply (simp add: full_del_def)
    1.51 -      apply (simp add: full_del_def split: ord.split)
    1.52 -     apply (simp add: full_del_def)
    1.53 +       apply simp
    1.54 +      apply (simp split: ord.split)
    1.55 +     apply simp
    1.56       apply (subst del_extra_simps, force)
    1.57 -     apply (simp | rule case_intros)+
    1.58 +     apply (simp | rule dfull_case_intros)+
    1.59       done
    1.60    } note A = this
    1.61    { fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k
    1.62 -    assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
    1.63 -    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"
    1.64 -    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"
    1.65 -    and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
    1.66 -    and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
    1.67 +    assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
    1.68 +    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)"
    1.69 +    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)"
    1.70 +    and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
    1.71 +    and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
    1.72      and "full (Suc n) (Branch3 l p m q r)"
    1.73 -    hence "full_del n k (Branch3 l p m q r)"
    1.74 +    hence "dfull n (del k (Branch3 l p m q r))"
    1.75       apply clarsimp
    1.76       apply (cases n)
    1.77        apply (cases k)
    1.78 -       apply (simp add: full_del_def)
    1.79 -      apply (simp add: full_del_def split: ord.split)
    1.80 -     apply (simp add: full_del_def)
    1.81 +       apply simp
    1.82 +      apply (simp split: ord.split)
    1.83 +     apply simp
    1.84       apply (subst del_extra_simps, force)
    1.85 -     apply (simp | rule case_intros)+
    1.86 +     apply (simp | rule dfull_case_intros)+
    1.87       done
    1.88    } note B = this
    1.89 -  show "full (Suc n) t \<Longrightarrow> full_del n k t"
    1.90 +  show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
    1.91    proof (induct k t arbitrary: n rule: del.induct)
    1.92 -    { case goal1 thus "full_del n (Some k) Empty"
    1.93 +    { case goal1 thus "dfull n (del (Some k) Empty)" by simp }
    1.94 +    { case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp }
    1.95 +    { case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))"
    1.96          by simp }
    1.97 -    { case goal2 thus "full_del n None (Branch2 Empty p Empty)"
    1.98 -        unfolding full_del_def by auto }
    1.99 -    { case goal3 thus "full_del n None (Branch3 Empty p Empty q Empty)"
   1.100 -        unfolding full_del_def by auto }
   1.101 -    { case goal4 thus "full_del n (Some v) (Branch2 Empty p Empty)"
   1.102 -        unfolding full_del_def by (auto split: ord.split) }
   1.103 -    { case goal5 thus "full_del n (Some v) (Branch3 Empty p Empty q Empty)"
   1.104 -        unfolding full_del_def by (auto split: ord.split) }
   1.105 +    { case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
   1.106 +        by (simp split: ord.split) }
   1.107 +    { case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
   1.108 +        by (simp split: ord.split) }
   1.109      { case goal26 thus ?case by simp }
   1.110    qed (fact A | fact B)+
   1.111  qed
   1.112  
   1.113  lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
   1.114 -  unfolding del0_def
   1.115 -  apply (drule bal_imp_full)
   1.116 -  apply (case_tac "height t", simp, simp)
   1.117 -  apply (frule full_del [where k="Some k"])
   1.118 -  apply (simp add: full_del_def)
   1.119 -  apply (auto split: option.split elim: full_imp_bal)
   1.120 -  done
   1.121 +unfolding bal_iff_full del0_def
   1.122 +apply (erule exE)
   1.123 +apply (case_tac n, simp, simp)
   1.124 +apply (frule dfull_del [where k="Some k"])
   1.125 +apply (cases "del (Some k) t", force)
   1.126 +apply (case_tac "a", rename_tac p b t', case_tac "b", auto)
   1.127 +done
   1.128  
   1.129  text{* This is a little test harness and should be commented out once the
   1.130  above functions have been proved correct. *}