src/HOL/Data_Structures/RBT_Set.thy
changeset 64952 f11e974b47e0
parent 64951 140addd19343
child 64953 f9cfb10761ff
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 12:32:49 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 17:28:10 2017 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4  
     1.5  subsection \<open>Structural invariants\<close>
     1.6  
     1.7 -text\<open>The proofs are due to Markus Reiter and Alexander Krauss,\<close>
     1.8 +text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
     1.9  
    1.10  fun color :: "'a rbt \<Rightarrow> color" where
    1.11  "color Leaf = Black" |
    1.12 @@ -135,7 +135,8 @@
    1.13  lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
    1.14  by (cases t) auto
    1.15  
    1.16 -lemma invc_bal: "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    1.17 +lemma invc_bal:
    1.18 +  "\<lbrakk>invc l \<and> invc_sons r \<or> invc_sons l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    1.19  by (induct l a r rule: bal.induct) auto
    1.20  
    1.21  lemma bheight_bal:
    1.22 @@ -314,224 +315,4 @@
    1.23    thus ?thesis by simp
    1.24  qed
    1.25  
    1.26 -text \<open>By Daniel St\"uwe\<close>
    1.27 -
    1.28 -lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
    1.29 - (\<exists> l a r . t = R l a r \<and> color l = Black \<and> color r = Black \<and> invc l \<and> invc r)"
    1.30 -by (cases t) auto
    1.31 -
    1.32 -lemma rbt_induct[consumes 1]:
    1.33 -  assumes "rbt t"
    1.34 -  assumes [simp]: "P Leaf"
    1.35 -  assumes "\<And> t l a r. \<lbrakk>t = B l a r; invc t; invh t; Q(l); Q(r)\<rbrakk> \<Longrightarrow> P t"
    1.36 -  assumes "\<And> t l a r. \<lbrakk>t = R l a r; invc t; invh t; P(l); P(r)\<rbrakk> \<Longrightarrow> Q t"
    1.37 -  assumes "\<And> t . P(t) \<Longrightarrow> Q(t)"
    1.38 -  shows "P t"
    1.39 -using assms(1) unfolding rbt_def apply safe
    1.40 -proof (induction t rule: measure_induct[of size])
    1.41 -case (1 t)
    1.42 -  note * = 1 assms
    1.43 -  show ?case proof (cases t)
    1.44 -    case [simp]: (Node c l a r)
    1.45 -    show ?thesis proof (cases c)
    1.46 -      case Red thus ?thesis using 1 by simp
    1.47 -    next
    1.48 -      case [simp]: Black
    1.49 -      show ?thesis
    1.50 -      proof (cases "color l")
    1.51 -        case Red
    1.52 -        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
    1.53 -      next
    1.54 -        case Black
    1.55 -        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
    1.56 -      qed
    1.57 -    qed
    1.58 -  qed simp
    1.59 -qed
    1.60 -
    1.61 -lemma rbt_b_height: "rbt t \<Longrightarrow> bheight t * 2 \<ge> height t"
    1.62 -by (induction t rule: rbt_induct[where Q="\<lambda> t. bheight t * 2 + 1 \<ge> height t"]) auto
    1.63 -
    1.64 -lemma red_b_height: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t * 2 + 1 \<ge> height t"
    1.65 -apply (cases t) apply simp
    1.66 -  using rbt_b_height unfolding rbt_def
    1.67 -  by (cases "color t") fastforce+
    1.68 -
    1.69 -lemma red_b_height2: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t \<ge> height t div 2"
    1.70 -using red_b_height by fastforce
    1.71 -
    1.72 -lemma rbt_b_height2: "bheight t \<le> height t"
    1.73 -by (induction t) auto
    1.74 -
    1.75 -lemma "rbt t \<Longrightarrow> size1 t \<le>  4 ^ (bheight t)"
    1.76 -by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le>  2 * 4 ^ (bheight t)"]) auto
    1.77 -
    1.78 -text \<open>Balanced red-balck tree with all black nodes:\<close>
    1.79 -inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool"  where
    1.80 -"balB 0 Leaf" |
    1.81 -"balB h t \<Longrightarrow> balB (Suc h) (B t () t)"
    1.82 -
    1.83 -inductive_cases [elim!]: "balB 0 t"
    1.84 -inductive_cases [elim]: "balB (Suc h) t"
    1.85 -
    1.86 -lemma balB_hs: "balB h t \<Longrightarrow> bheight t = height t"
    1.87 -by (induction h t rule: "balB.induct") auto
    1.88 -
    1.89 -lemma balB_h: "balB h t \<Longrightarrow> h = height t"
    1.90 -by (induction h t rule: "balB.induct") auto
    1.91 -
    1.92 -lemma "rbt t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
    1.93 -by (induction t arbitrary: t' 
    1.94 - rule: rbt_induct[where Q="\<lambda> t . \<forall> h t'. balB (bheight t) t' \<longrightarrow> size t' \<le> size t"])
    1.95 - fastforce+
    1.96 -
    1.97 -lemma balB_bh: "invc t \<Longrightarrow> invh t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
    1.98 -by (induction t arbitrary: t') (fastforce split: if_split_asm)+
    1.99 -
   1.100 -lemma balB_bh3:"\<lbrakk> balB h t; balB (h' + h) t' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   1.101 -by (induction h t arbitrary: t' h' rule: balB.induct)  fastforce+
   1.102 -
   1.103 -corollary balB_bh3': "\<lbrakk> balB h t; balB h' t'; h \<le> h' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   1.104 -using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps)
   1.105 -
   1.106 -lemma exist_pt: "\<exists> t . balB h t"
   1.107 -by (induction h) (auto intro: balB.intros)
   1.108 -
   1.109 -corollary compact_pt:
   1.110 -  assumes "invc t" "invh t" "h \<le> bheight t" "balB h t'"
   1.111 -  shows   "size t' \<le> size t"
   1.112 -proof -
   1.113 -  obtain t'' where "balB (bheight t) t''" using exist_pt by blast
   1.114 -  thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto
   1.115 -qed
   1.116 -
   1.117 -lemma balB_bh2: "balB (bheight t) t'\<Longrightarrow> invc t \<Longrightarrow> invh t \<Longrightarrow> height t' \<le> height t"
   1.118 -apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct)
   1.119 -using balB_h rbt_b_height2 by auto
   1.120 -
   1.121 -lemma balB_rbt: "balB h t \<Longrightarrow> rbt t"
   1.122 -unfolding rbt_def
   1.123 -by (induction h t rule: balB.induct) auto
   1.124 -
   1.125 -lemma balB_size[simp]: "balB h t \<Longrightarrow> size1 t = 2^h"
   1.126 -by (induction h t rule: balB.induct) auto
   1.127 -
   1.128 -text \<open>Red-black tree (except that the root may be red) of minimal size
   1.129 -for a given height:\<close>
   1.130 -
   1.131 -inductive RB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
   1.132 -"RB 0 Leaf" |
   1.133 -"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Red \<Longrightarrow> RB (Suc h) (B t' () t)" |
   1.134 -"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Black \<Longrightarrow> RB (Suc h) (R t' () t)" 
   1.135 -
   1.136 -lemmas RB.intros[intro]
   1.137 -
   1.138 -lemma RB_invc: "RB h t \<Longrightarrow> invc t"
   1.139 -apply (induction h t rule: RB.induct)
   1.140 -using balB_rbt unfolding rbt_def by auto
   1.141 -
   1.142 -lemma RB_h: "RB h t \<Longrightarrow> h = height t"
   1.143 -apply (induction h t rule: RB.induct)
   1.144 -using balB_h by auto
   1.145 -
   1.146 -lemma RB_mod: "RB h t \<Longrightarrow> (color t = Black \<longleftrightarrow> h mod 2 = 0)"
   1.147 -apply (induction h t rule: RB.induct)
   1.148 -apply auto
   1.149 -by presburger
   1.150 -
   1.151 -lemma RB_b_height: "RB h t \<Longrightarrow> height t div 2 = bheight t"
   1.152 -proof  (induction h t rule: RB.induct)
   1.153 -  case 1 
   1.154 -  thus ?case by auto 
   1.155 -next
   1.156 -  case (2 h t t')
   1.157 -  with RB_mod obtain n where "2*n + 1 = h" 
   1.158 -    by (metis color.distinct(1) mult_div_mod_eq parity) 
   1.159 -  with 2 balB_h RB_h show ?case by auto
   1.160 -next
   1.161 -  case (3 h t t')
   1.162 -  with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast
   1.163 -  with 3 balB_h RB_h show ?case by auto
   1.164 -qed
   1.165 -
   1.166 -lemma weak_RB_induct[consumes 1]: 
   1.167 -  "RB h t \<Longrightarrow> P 0 \<langle>\<rangle> \<Longrightarrow> (\<And>h t t' c . balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow>
   1.168 -    P h t' \<Longrightarrow> P (Suc h) (Node c t' () t)) \<Longrightarrow> P h t"
   1.169 -using RB.induct by metis
   1.170 -
   1.171 -lemma RB_invh: "RB h t \<Longrightarrow> invh t"
   1.172 -apply (induction h t rule: weak_RB_induct)
   1.173 -  using balB_h balB_hs RB_h balB_rbt RB_b_height
   1.174 -  unfolding rbt_def
   1.175 -by auto
   1.176 -
   1.177 -lemma RB_bheight_minimal:
   1.178 -  "\<lbrakk>RB (height t') t; invc t'; invh t'\<rbrakk> \<Longrightarrow> bheight t \<le> bheight t'"
   1.179 -using RB_b_height RB_h red_b_height2 by fastforce
   1.180 -
   1.181 -lemma RB_minimal: "RB (height t') t \<Longrightarrow> invh t \<Longrightarrow> invc t' \<Longrightarrow> invh t' \<Longrightarrow> size t \<le> size t'"
   1.182 -proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct)
   1.183 -  case 1 thus ?case by auto 
   1.184 -next
   1.185 -  case (2 h t t'')
   1.186 -  have ***: "size (Node c t'' () t) \<le> size t'"
   1.187 -    if assms:
   1.188 -      "\<And> (t' :: 'a rbt) . \<lbrakk> h = height t'; invh t''; invc t'; invh t' \<rbrakk>
   1.189 -                            \<Longrightarrow> size t'' \<le> size t'"
   1.190 -      "Suc h = height t'" "balB (h div 2) t" "RB h t''"
   1.191 -      "invc t'" "invh t'" "height l \<ge> height r"
   1.192 -      and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)"
   1.193 -  for t' :: "'a rbt" and c l a r
   1.194 -  proof -
   1.195 -    from assms have inv: "invc r" "invh r" by auto
   1.196 -    from assms have "height l = h" using max_def by auto
   1.197 -    with RB_bheight_minimal[of l t''] have
   1.198 -      "bheight t \<le> bheight r" using assms last by auto
   1.199 -    with compact_pt[OF inv] balB_h balB_hs have 
   1.200 -      "size t \<le> size r" using assms(3) by auto moreover
   1.201 -    have "size t'' \<le> size l" using assms last by auto ultimately
   1.202 -    show ?thesis by simp
   1.203 -  qed
   1.204 -  
   1.205 -  from 2 obtain c l a r where 
   1.206 -    t': "t' = Node c l a r" by (cases t') auto
   1.207 -  with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto
   1.208 -  show ?case proof (cases "height r \<le> height l")
   1.209 -    case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto
   1.210 -  next
   1.211 -    case False 
   1.212 -    obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto
   1.213 -    have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto
   1.214 -    thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto
   1.215 -  qed
   1.216 -qed
   1.217 -
   1.218 -lemma RB_size: "RB h t \<Longrightarrow> size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)"
   1.219 -by (induction h t rule: "RB.induct" ) auto
   1.220 -
   1.221 -lemma RB_exist: "\<exists> t . RB h t"
   1.222 -proof (induction h) 
   1.223 -  case (Suc n)
   1.224 -  obtain r where r: "balB (n div 2) r"  using  exist_pt by blast
   1.225 -  obtain l where l: "RB n l"  using  Suc by blast
   1.226 -  obtain t where 
   1.227 -    "color l = Red   \<Longrightarrow> t = B l () r"
   1.228 -    "color l = Black \<Longrightarrow> t = R l () r" by auto
   1.229 -  with l and r have "RB (Suc n) t" by (cases "color l") auto
   1.230 -  thus ?case by auto
   1.231 -qed auto
   1.232 -
   1.233 -lemma bound:
   1.234 -  assumes "invc t"  "invh t" and [simp]:"height t = h"
   1.235 -  shows "size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   1.236 -proof -
   1.237 -  obtain t' where t': "RB h t'" using RB_exist by auto
   1.238 -  show ?thesis using RB_size[OF t'] 
   1.239 -  RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t' 
   1.240 -  unfolding  size1_def by auto
   1.241 -qed
   1.242 -
   1.243 -corollary "rbt t \<Longrightarrow> h = height t \<Longrightarrow> size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   1.244 -using bound unfolding rbt_def by blast
   1.245 -
   1.246  end