ex/Tree23.thy: simplify proof of bal_add0
authorhuffman
Fri Nov 04 07:37:37 2011 +0100 (2011-11-04)
changeset 453343f74e041e05c
parent 45333 04b21922ed68
child 45335 a68ce51de69a
ex/Tree23.thy: simplify proof of bal_add0
src/HOL/ex/Tree23.thy
     1.1 --- a/src/HOL/ex/Tree23.thy	Fri Nov 04 07:04:34 2011 +0100
     1.2 +++ b/src/HOL/ex/Tree23.thy	Fri Nov 04 07:37:37 2011 +0100
     1.3 @@ -136,8 +136,7 @@
     1.4  definition del0 :: "key \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
     1.5  "del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"
     1.6  
     1.7 -
     1.8 -text {* Specifying correctness *}
     1.9 +text {* Ordered trees *}
    1.10  
    1.11  definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
    1.12    "opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))"
    1.13 @@ -156,6 +155,35 @@
    1.14  definition ord0 :: "'a tree23 \<Rightarrow> bool" where
    1.15    "ord0 t = ord' None t None"
    1.16  
    1.17 +text {* Balanced trees *}
    1.18 +
    1.19 +inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
    1.20 +"full 0 Empty" |
    1.21 +"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" |
    1.22 +"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)"
    1.23 +
    1.24 +inductive_cases full_elims:
    1.25 +  "full n Empty"
    1.26 +  "full n (Branch2 l p r)"
    1.27 +  "full n (Branch3 l p m q r)"
    1.28 +
    1.29 +inductive_cases full_0_elim: "full 0 t"
    1.30 +inductive_cases full_Suc_elim: "full (Suc n) t"
    1.31 +
    1.32 +lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty"
    1.33 +  by (auto elim: full_0_elim intro: full.intros)
    1.34 +
    1.35 +lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0"
    1.36 +  by (auto elim: full_elims intro: full.intros)
    1.37 +
    1.38 +lemma full_Suc_Branch2_iff [simp]:
    1.39 +  "full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r"
    1.40 +  by (auto elim: full_elims intro: full.intros)
    1.41 +
    1.42 +lemma full_Suc_Branch3_iff [simp]:
    1.43 +  "full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
    1.44 +  by (auto elim: full_elims intro: full.intros)
    1.45 +
    1.46  fun height :: "'a tree23 \<Rightarrow> nat" where
    1.47  "height Empty = 0" |
    1.48  "height (Branch2 l _ r) = Suc(max (height l) (height r))" |
    1.49 @@ -167,45 +195,70 @@
    1.50  "bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
    1.51  "bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
    1.52  
    1.53 +lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
    1.54 +  by (induct set: full, simp_all)
    1.55 +
    1.56 +lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
    1.57 +  by (induct set: full, auto dest: full_imp_height)
    1.58 +
    1.59 +lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
    1.60 +  by (induct t, simp_all)
    1.61 +
    1.62 +lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
    1.63 +  by (auto elim!: bal_imp_full full_imp_bal)
    1.64 +
    1.65  text {* The @{term "add0"} function either preserves the height of the
    1.66  tree, or increases it by one. The constructor returned by the @{term
    1.67  "add"} function determines which: A return value of the form @{term
    1.68  "Stay t"} indicates that the height will be the same. A value of the
    1.69  form @{term "Sprout l p r"} indicates an increase in height. *}
    1.70  
    1.71 -fun gheight :: "'a growth \<Rightarrow> nat" where
    1.72 -"gheight (Stay t) = height t" |
    1.73 -"gheight (Sprout l p r) = max (height l) (height r)"
    1.74 +primrec gfull :: "nat \<Rightarrow> 'a growth \<Rightarrow> bool" where
    1.75 +"gfull n (Stay t) \<longleftrightarrow> full n t" |
    1.76 +"gfull n (Sprout l p r) \<longleftrightarrow> full n l \<and> full n r"
    1.77  
    1.78 -lemma gheight_add: "gheight (add k y t) = height t"
    1.79 - apply (induct t)
    1.80 +lemma gfull_add: "full n t \<Longrightarrow> gfull n (add k y t)"
    1.81 + apply (induct set: full)
    1.82     apply simp
    1.83    apply clarsimp
    1.84    apply (case_tac "ord k a")
    1.85      apply simp
    1.86 -    apply (case_tac "add k y t1", simp, simp)
    1.87 +    apply (case_tac "add k y l", simp, simp)
    1.88     apply simp
    1.89    apply simp
    1.90 -  apply (case_tac "add k y t2", simp, simp)
    1.91 +  apply (case_tac "add k y r", simp, simp)
    1.92   apply clarsimp
    1.93   apply (case_tac "ord k a")
    1.94     apply simp
    1.95 -   apply (case_tac "add k y t1", simp, simp)
    1.96 +   apply (case_tac "add k y l", simp, simp)
    1.97    apply simp
    1.98   apply simp
    1.99   apply (case_tac "ord k aa")
   1.100     apply simp
   1.101 -   apply (case_tac "add k y t2", simp, simp)
   1.102 +   apply (case_tac "add k y m", simp, simp)
   1.103    apply simp
   1.104   apply simp
   1.105 - apply (case_tac "add k y t3", simp, simp)
   1.106 + apply (case_tac "add k y r", simp, simp)
   1.107  done
   1.108  
   1.109 -lemma add_eq_Stay_dest: "add k y t = Stay t' \<Longrightarrow> height t = height t'"
   1.110 -  using gheight_add [of k y t] by simp
   1.111 +text {* The @{term "add0"} operation preserves balance. *}
   1.112  
   1.113 -lemma add_eq_Sprout_dest: "add k y t = Sprout l p r \<Longrightarrow> height t = max (height l) (height r)"
   1.114 -  using gheight_add [of k y t] by simp
   1.115 +lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
   1.116 +unfolding bal_iff_full add0_def
   1.117 +apply (erule exE)
   1.118 +apply (drule gfull_add [of _ _ k y])
   1.119 +apply (cases "add k y t")
   1.120 +apply (auto intro: full.intros)
   1.121 +done
   1.122 +
   1.123 +text {* The @{term "add0"} operation preserves order. *}
   1.124 +
   1.125 +lemma ord_cases:
   1.126 +  fixes a b :: int obtains
   1.127 +  "ord a b = LESS" and "a < b" |
   1.128 +  "ord a b = EQUAL" and "a = b" |
   1.129 +  "ord a b = GREATER" and "a > b"
   1.130 +unfolding ord_def by (rule linorder_cases [of a b]) auto
   1.131  
   1.132  definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
   1.133    "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
   1.134 @@ -218,52 +271,6 @@
   1.135  lemma add0: "add0 k y t = gtree (add k y t)"
   1.136    unfolding add0_def by (simp split: growth.split)
   1.137  
   1.138 -text {* The @{term "add0"} operation preserves balance. *}
   1.139 -
   1.140 -lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
   1.141 -unfolding add0
   1.142 - apply (induct t)
   1.143 -   apply simp
   1.144 -  apply clarsimp
   1.145 -  apply (case_tac "ord k a")
   1.146 -    apply simp
   1.147 -    apply (case_tac "add k y t1")
   1.148 -     apply (simp, drule add_eq_Stay_dest, simp)
   1.149 -    apply (simp, drule add_eq_Sprout_dest, simp)
   1.150 -   apply simp
   1.151 -  apply simp
   1.152 -  apply (case_tac "add k y t2")
   1.153 -   apply (simp, drule add_eq_Stay_dest, simp)
   1.154 -  apply (simp, drule add_eq_Sprout_dest, simp)
   1.155 - apply clarsimp
   1.156 - apply (case_tac "ord k a")
   1.157 -   apply simp
   1.158 -   apply (case_tac "add k y t1")
   1.159 -    apply (simp, drule add_eq_Stay_dest, simp)
   1.160 -   apply (simp, drule add_eq_Sprout_dest, simp)
   1.161 -  apply simp
   1.162 - apply simp
   1.163 - apply (case_tac "ord k aa")
   1.164 -   apply simp
   1.165 -   apply (case_tac "add k y t2")
   1.166 -    apply (simp, drule add_eq_Stay_dest, simp)
   1.167 -   apply (simp, drule add_eq_Sprout_dest, simp)
   1.168 -  apply simp
   1.169 - apply simp
   1.170 - apply (case_tac "add k y t3")
   1.171 -  apply (simp, drule add_eq_Stay_dest, simp)
   1.172 - apply (simp, drule add_eq_Sprout_dest, simp)
   1.173 -done
   1.174 -
   1.175 -text {* The @{term "add0"} operation preserves order. *}
   1.176 -
   1.177 -lemma ord_cases:
   1.178 -  fixes a b :: int obtains
   1.179 -  "ord a b = LESS" and "a < b" |
   1.180 -  "ord a b = EQUAL" and "a = b" |
   1.181 -  "ord a b = GREATER" and "a > b"
   1.182 -unfolding ord_def by (rule linorder_cases [of a b]) auto
   1.183 -
   1.184  lemma ord'_add0:
   1.185    "\<lbrakk>ord' k1 t k2; opt_less k1 (Some k); opt_less (Some k) k2\<rbrakk> \<Longrightarrow> ord' k1 (add0 k y t) k2"
   1.186  unfolding add0
   1.187 @@ -338,33 +345,6 @@
   1.188  apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
   1.189  done
   1.190  
   1.191 -inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
   1.192 -"full 0 Empty" |
   1.193 -"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" |
   1.194 -"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)"
   1.195 -
   1.196 -inductive_cases full_elims:
   1.197 -  "full n Empty"
   1.198 -  "full n (Branch2 l p r)"
   1.199 -  "full n (Branch3 l p m q r)"
   1.200 -
   1.201 -inductive_cases full_0_elim: "full 0 t"
   1.202 -inductive_cases full_Suc_elim: "full (Suc n) t"
   1.203 -
   1.204 -lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty"
   1.205 -  by (auto elim: full_0_elim intro: full.intros)
   1.206 -
   1.207 -lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0"
   1.208 -  by (auto elim: full_elims intro: full.intros)
   1.209 -
   1.210 -lemma full_Suc_Branch2_iff [simp]:
   1.211 -  "full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r"
   1.212 -  by (auto elim: full_elims intro: full.intros)
   1.213 -
   1.214 -lemma full_Suc_Branch3_iff [simp]:
   1.215 -  "full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
   1.216 -  by (auto elim: full_elims intro: full.intros)
   1.217 -
   1.218  definition
   1.219    "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.220  
   1.221 @@ -433,18 +413,6 @@
   1.222    qed (fact A | fact B)+
   1.223  qed
   1.224  
   1.225 -lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   1.226 -  by (induct set: full, simp_all)
   1.227 -
   1.228 -lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
   1.229 -  by (induct set: full, auto dest: full_imp_height)
   1.230 -
   1.231 -lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
   1.232 -  by (induct t, simp_all)
   1.233 -
   1.234 -lemma bal_iff_full: "bal t \<longleftrightarrow> full (height t) t"
   1.235 -  using bal_imp_full full_imp_bal ..
   1.236 -
   1.237  lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
   1.238    unfolding del0_def
   1.239    apply (drule bal_imp_full)