ex/Tree23.thy: prove that insertion preserves tree balance and order
authorhuffman
Thu Nov 03 11:18:06 2011 +0100 (2011-11-03)
changeset 4532526b6179b5a45
parent 45324 4ef9220b886b
child 45326 8fa859aebc0d
child 45332 ede9dc025150
ex/Tree23.thy: prove that insertion preserves tree balance and order
src/HOL/ex/Tree23.thy
     1.1 --- a/src/HOL/ex/Tree23.thy	Thu Nov 03 18:10:47 2011 +1100
     1.2 +++ b/src/HOL/ex/Tree23.thy	Thu Nov 03 11:18:06 2011 +0100
     1.3 @@ -159,6 +159,25 @@
     1.4  "ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" |
     1.5  "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)"
     1.6  
     1.7 +definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
     1.8 +  "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.9 +
    1.10 +lemma opt_less_simps [simp]:
    1.11 +  "opt_less None y = True"
    1.12 +  "opt_less x None = True"
    1.13 +  "opt_less (Some a) (Some b) = (a < b)"
    1.14 +unfolding opt_less_def by (auto simp add: ord_def split: option.split)
    1.15 +
    1.16 +fun ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
    1.17 +"ord' x Empty y = opt_less x y" |
    1.18 +"ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" |
    1.19 +"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)"
    1.20 +
    1.21 +lemma ord':
    1.22 +  "ord' x t y = (case x of None \<Rightarrow> (case y of None \<Rightarrow> ord0 t | Some y' \<Rightarrow> ordr t y')
    1.23 +    | Some x' \<Rightarrow> (case y of None \<Rightarrow> ordl x' t | Some y' \<Rightarrow> ordlr x' t y'))"
    1.24 +by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split)
    1.25 +
    1.26  fun height :: "'a tree23 \<Rightarrow> nat" where
    1.27  "height Empty = 0" |
    1.28  "height (Branch2 l _ r) = Suc(max (height l) (height r))" |
    1.29 @@ -170,6 +189,132 @@
    1.30  "bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
    1.31  "bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
    1.32  
    1.33 +text {* The @{term "add0"} function either preserves the height of the
    1.34 +tree, or increases it by one. The constructor returned by the @{term
    1.35 +"add"} function determines which: A return value of the form @{term
    1.36 +"Stay t"} indicates that the height will be the same. A value of the
    1.37 +form @{term "Sprout l p r"} indicates an increase in height. *}
    1.38 +
    1.39 +fun gheight :: "'a growth \<Rightarrow> nat" where
    1.40 +"gheight (Stay t) = height t" |
    1.41 +"gheight (Sprout l p r) = max (height l) (height r)"
    1.42 +
    1.43 +lemma gheight_add: "gheight (add k y t) = height t"
    1.44 + apply (induct t)
    1.45 +   apply simp
    1.46 +  apply clarsimp
    1.47 +  apply (case_tac "ord k a")
    1.48 +    apply simp
    1.49 +    apply (case_tac "add k y t1", simp, simp)
    1.50 +   apply simp
    1.51 +  apply simp
    1.52 +  apply (case_tac "add k y t2", simp, simp)
    1.53 + apply clarsimp
    1.54 + apply (case_tac "ord k a")
    1.55 +   apply simp
    1.56 +   apply (case_tac "add k y t1", simp, simp)
    1.57 +  apply simp
    1.58 + apply simp
    1.59 + apply (case_tac "ord k aa")
    1.60 +   apply simp
    1.61 +   apply (case_tac "add k y t2", simp, simp)
    1.62 +  apply simp
    1.63 + apply simp
    1.64 + apply (case_tac "add k y t3", simp, simp)
    1.65 +done
    1.66 +
    1.67 +lemma add_eq_Stay_dest: "add k y t = Stay t' \<Longrightarrow> height t = height t'"
    1.68 +  using gheight_add [of k y t] by simp
    1.69 +
    1.70 +lemma add_eq_Sprout_dest: "add k y t = Sprout l p r \<Longrightarrow> height t = max (height l) (height r)"
    1.71 +  using gheight_add [of k y t] by simp
    1.72 +
    1.73 +definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
    1.74 +  "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
    1.75 +
    1.76 +lemma gtree_simps [simp]:
    1.77 +  "gtree (Stay t) = t"
    1.78 +  "gtree (Sprout l p r) = Branch2 l p r"
    1.79 +unfolding gtree_def by simp_all
    1.80 +
    1.81 +lemma add0: "add0 k y t = gtree (add k y t)"
    1.82 +  unfolding add0_def by (simp split: growth.split)
    1.83 +
    1.84 +text {* The @{term "add0"} operation preserves balance. *}
    1.85 +
    1.86 +lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
    1.87 +unfolding add0
    1.88 + apply (induct t)
    1.89 +   apply simp
    1.90 +  apply clarsimp
    1.91 +  apply (case_tac "ord k a")
    1.92 +    apply simp
    1.93 +    apply (case_tac "add k y t1")
    1.94 +     apply (simp, drule add_eq_Stay_dest, simp)
    1.95 +    apply (simp, drule add_eq_Sprout_dest, simp)
    1.96 +   apply simp
    1.97 +  apply simp
    1.98 +  apply (case_tac "add k y t2")
    1.99 +   apply (simp, drule add_eq_Stay_dest, simp)
   1.100 +  apply (simp, drule add_eq_Sprout_dest, simp)
   1.101 + apply clarsimp
   1.102 + apply (case_tac "ord k a")
   1.103 +   apply simp
   1.104 +   apply (case_tac "add k y t1")
   1.105 +    apply (simp, drule add_eq_Stay_dest, simp)
   1.106 +   apply (simp, drule add_eq_Sprout_dest, simp)
   1.107 +  apply simp
   1.108 + apply simp
   1.109 + apply (case_tac "ord k aa")
   1.110 +   apply simp
   1.111 +   apply (case_tac "add k y t2")
   1.112 +    apply (simp, drule add_eq_Stay_dest, simp)
   1.113 +   apply (simp, drule add_eq_Sprout_dest, simp)
   1.114 +  apply simp
   1.115 + apply simp
   1.116 + apply (case_tac "add k y t3")
   1.117 +  apply (simp, drule add_eq_Stay_dest, simp)
   1.118 + apply (simp, drule add_eq_Sprout_dest, simp)
   1.119 +done
   1.120 +
   1.121 +text {* The @{term "add0"} operation preserves order. *}
   1.122 +
   1.123 +lemma ord_cases:
   1.124 +  fixes a b :: int obtains
   1.125 +  "ord a b = LESS" and "a < b" |
   1.126 +  "ord a b = EQUAL" and "a = b" |
   1.127 +  "ord a b = GREATER" and "a > b"
   1.128 +unfolding ord_def by (rule linorder_cases [of a b]) auto
   1.129 +
   1.130 +lemma ord'_add0:
   1.131 +  "\<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.132 +unfolding add0
   1.133 + apply (induct t arbitrary: k1 k2)
   1.134 +   apply simp
   1.135 +  apply clarsimp
   1.136 +  apply (rule_tac a=k and b=a in ord_cases)
   1.137 +    apply simp
   1.138 +    apply (case_tac "add k y t1", simp, simp)
   1.139 +   apply simp
   1.140 +  apply simp
   1.141 +  apply (case_tac "add k y t2", simp, simp)
   1.142 + apply clarsimp
   1.143 + apply (rule_tac a=k and b=a in ord_cases)
   1.144 +   apply simp
   1.145 +   apply (case_tac "add k y t1", simp, simp)
   1.146 +  apply simp
   1.147 + apply simp
   1.148 + apply (rule_tac a=k and b=aa in ord_cases)
   1.149 +   apply simp
   1.150 +   apply (case_tac "add k y t2", simp, simp)
   1.151 +  apply simp
   1.152 + apply simp
   1.153 + apply (case_tac "add k y t3", simp, simp)
   1.154 +done
   1.155 +
   1.156 +lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
   1.157 +using ord'_add0 [of None t None k y] by (simp add: ord')
   1.158 +
   1.159  text{* This is a little test harness and should be commented out once the
   1.160  above functions have been proved correct. *}
   1.161