removed unclear clause; slower but clearer
authornipkow
Fri Jan 27 17:28:10 2017 +0100 (2017-01-27)
changeset 64952f11e974b47e0
parent 64951 140addd19343
child 64953 f9cfb10761ff
removed unclear clause; slower but clearer
src/HOL/Data_Structures/RBT.thy
src/HOL/Data_Structures/RBT_Set.thy
     1.1 --- a/src/HOL/Data_Structures/RBT.thy	Fri Jan 27 12:32:49 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT.thy	Fri Jan 27 17:28:10 2017 +0100
     1.3 @@ -14,13 +14,18 @@
     1.4  abbreviation B where "B l a r \<equiv> Node Black l a r"
     1.5  
     1.6  fun bal :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
     1.7 -(* The first line is superfluous; it merely speeds up pattern compilation *)
     1.8 -"bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
     1.9  "bal (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.10  "bal (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.11 +"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.12  "bal t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.13 -"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.14  "bal t1 a t2 = B t1 a t2"
    1.15 +(* Warning: takes 30 secs to compile (2017) *)
    1.16 +text\<open>Markus Reiter and Alexander Krauss added a first line not found in Okasaki:
    1.17 +@{prop "bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)"}
    1.18 +The motivation is unclear. However: it speeds up pattern compilation
    1.19 +and lemma \<open>invc_bal\<close> below can be simplified to
    1.20 +  @{prop "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)"}
    1.21 +All other proofs are unaffected.\<close>
    1.22  
    1.23  fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.24  "paint c Leaf = Leaf" |
     2.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 12:32:49 2017 +0100
     2.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 17:28:10 2017 +0100
     2.3 @@ -91,7 +91,7 @@
     2.4  
     2.5  subsection \<open>Structural invariants\<close>
     2.6  
     2.7 -text\<open>The proofs are due to Markus Reiter and Alexander Krauss,\<close>
     2.8 +text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
     2.9  
    2.10  fun color :: "'a rbt \<Rightarrow> color" where
    2.11  "color Leaf = Black" |
    2.12 @@ -135,7 +135,8 @@
    2.13  lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
    2.14  by (cases t) auto
    2.15  
    2.16 -lemma invc_bal: "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    2.17 +lemma invc_bal:
    2.18 +  "\<lbrakk>invc l \<and> invc_sons r \<or> invc_sons l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    2.19  by (induct l a r rule: bal.induct) auto
    2.20  
    2.21  lemma bheight_bal:
    2.22 @@ -314,224 +315,4 @@
    2.23    thus ?thesis by simp
    2.24  qed
    2.25  
    2.26 -text \<open>By Daniel St\"uwe\<close>
    2.27 -
    2.28 -lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
    2.29 - (\<exists> l a r . t = R l a r \<and> color l = Black \<and> color r = Black \<and> invc l \<and> invc r)"
    2.30 -by (cases t) auto
    2.31 -
    2.32 -lemma rbt_induct[consumes 1]:
    2.33 -  assumes "rbt t"
    2.34 -  assumes [simp]: "P Leaf"
    2.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"
    2.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"
    2.37 -  assumes "\<And> t . P(t) \<Longrightarrow> Q(t)"
    2.38 -  shows "P t"
    2.39 -using assms(1) unfolding rbt_def apply safe
    2.40 -proof (induction t rule: measure_induct[of size])
    2.41 -case (1 t)
    2.42 -  note * = 1 assms
    2.43 -  show ?case proof (cases t)
    2.44 -    case [simp]: (Node c l a r)
    2.45 -    show ?thesis proof (cases c)
    2.46 -      case Red thus ?thesis using 1 by simp
    2.47 -    next
    2.48 -      case [simp]: Black
    2.49 -      show ?thesis
    2.50 -      proof (cases "color l")
    2.51 -        case Red
    2.52 -        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
    2.53 -      next
    2.54 -        case Black
    2.55 -        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
    2.56 -      qed
    2.57 -    qed
    2.58 -  qed simp
    2.59 -qed
    2.60 -
    2.61 -lemma rbt_b_height: "rbt t \<Longrightarrow> bheight t * 2 \<ge> height t"
    2.62 -by (induction t rule: rbt_induct[where Q="\<lambda> t. bheight t * 2 + 1 \<ge> height t"]) auto
    2.63 -
    2.64 -lemma red_b_height: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t * 2 + 1 \<ge> height t"
    2.65 -apply (cases t) apply simp
    2.66 -  using rbt_b_height unfolding rbt_def
    2.67 -  by (cases "color t") fastforce+
    2.68 -
    2.69 -lemma red_b_height2: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t \<ge> height t div 2"
    2.70 -using red_b_height by fastforce
    2.71 -
    2.72 -lemma rbt_b_height2: "bheight t \<le> height t"
    2.73 -by (induction t) auto
    2.74 -
    2.75 -lemma "rbt t \<Longrightarrow> size1 t \<le>  4 ^ (bheight t)"
    2.76 -by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le>  2 * 4 ^ (bheight t)"]) auto
    2.77 -
    2.78 -text \<open>Balanced red-balck tree with all black nodes:\<close>
    2.79 -inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool"  where
    2.80 -"balB 0 Leaf" |
    2.81 -"balB h t \<Longrightarrow> balB (Suc h) (B t () t)"
    2.82 -
    2.83 -inductive_cases [elim!]: "balB 0 t"
    2.84 -inductive_cases [elim]: "balB (Suc h) t"
    2.85 -
    2.86 -lemma balB_hs: "balB h t \<Longrightarrow> bheight t = height t"
    2.87 -by (induction h t rule: "balB.induct") auto
    2.88 -
    2.89 -lemma balB_h: "balB h t \<Longrightarrow> h = height t"
    2.90 -by (induction h t rule: "balB.induct") auto
    2.91 -
    2.92 -lemma "rbt t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
    2.93 -by (induction t arbitrary: t' 
    2.94 - rule: rbt_induct[where Q="\<lambda> t . \<forall> h t'. balB (bheight t) t' \<longrightarrow> size t' \<le> size t"])
    2.95 - fastforce+
    2.96 -
    2.97 -lemma balB_bh: "invc t \<Longrightarrow> invh t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
    2.98 -by (induction t arbitrary: t') (fastforce split: if_split_asm)+
    2.99 -
   2.100 -lemma balB_bh3:"\<lbrakk> balB h t; balB (h' + h) t' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   2.101 -by (induction h t arbitrary: t' h' rule: balB.induct)  fastforce+
   2.102 -
   2.103 -corollary balB_bh3': "\<lbrakk> balB h t; balB h' t'; h \<le> h' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   2.104 -using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps)
   2.105 -
   2.106 -lemma exist_pt: "\<exists> t . balB h t"
   2.107 -by (induction h) (auto intro: balB.intros)
   2.108 -
   2.109 -corollary compact_pt:
   2.110 -  assumes "invc t" "invh t" "h \<le> bheight t" "balB h t'"
   2.111 -  shows   "size t' \<le> size t"
   2.112 -proof -
   2.113 -  obtain t'' where "balB (bheight t) t''" using exist_pt by blast
   2.114 -  thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto
   2.115 -qed
   2.116 -
   2.117 -lemma balB_bh2: "balB (bheight t) t'\<Longrightarrow> invc t \<Longrightarrow> invh t \<Longrightarrow> height t' \<le> height t"
   2.118 -apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct)
   2.119 -using balB_h rbt_b_height2 by auto
   2.120 -
   2.121 -lemma balB_rbt: "balB h t \<Longrightarrow> rbt t"
   2.122 -unfolding rbt_def
   2.123 -by (induction h t rule: balB.induct) auto
   2.124 -
   2.125 -lemma balB_size[simp]: "balB h t \<Longrightarrow> size1 t = 2^h"
   2.126 -by (induction h t rule: balB.induct) auto
   2.127 -
   2.128 -text \<open>Red-black tree (except that the root may be red) of minimal size
   2.129 -for a given height:\<close>
   2.130 -
   2.131 -inductive RB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
   2.132 -"RB 0 Leaf" |
   2.133 -"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Red \<Longrightarrow> RB (Suc h) (B t' () t)" |
   2.134 -"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Black \<Longrightarrow> RB (Suc h) (R t' () t)" 
   2.135 -
   2.136 -lemmas RB.intros[intro]
   2.137 -
   2.138 -lemma RB_invc: "RB h t \<Longrightarrow> invc t"
   2.139 -apply (induction h t rule: RB.induct)
   2.140 -using balB_rbt unfolding rbt_def by auto
   2.141 -
   2.142 -lemma RB_h: "RB h t \<Longrightarrow> h = height t"
   2.143 -apply (induction h t rule: RB.induct)
   2.144 -using balB_h by auto
   2.145 -
   2.146 -lemma RB_mod: "RB h t \<Longrightarrow> (color t = Black \<longleftrightarrow> h mod 2 = 0)"
   2.147 -apply (induction h t rule: RB.induct)
   2.148 -apply auto
   2.149 -by presburger
   2.150 -
   2.151 -lemma RB_b_height: "RB h t \<Longrightarrow> height t div 2 = bheight t"
   2.152 -proof  (induction h t rule: RB.induct)
   2.153 -  case 1 
   2.154 -  thus ?case by auto 
   2.155 -next
   2.156 -  case (2 h t t')
   2.157 -  with RB_mod obtain n where "2*n + 1 = h" 
   2.158 -    by (metis color.distinct(1) mult_div_mod_eq parity) 
   2.159 -  with 2 balB_h RB_h show ?case by auto
   2.160 -next
   2.161 -  case (3 h t t')
   2.162 -  with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast
   2.163 -  with 3 balB_h RB_h show ?case by auto
   2.164 -qed
   2.165 -
   2.166 -lemma weak_RB_induct[consumes 1]: 
   2.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>
   2.168 -    P h t' \<Longrightarrow> P (Suc h) (Node c t' () t)) \<Longrightarrow> P h t"
   2.169 -using RB.induct by metis
   2.170 -
   2.171 -lemma RB_invh: "RB h t \<Longrightarrow> invh t"
   2.172 -apply (induction h t rule: weak_RB_induct)
   2.173 -  using balB_h balB_hs RB_h balB_rbt RB_b_height
   2.174 -  unfolding rbt_def
   2.175 -by auto
   2.176 -
   2.177 -lemma RB_bheight_minimal:
   2.178 -  "\<lbrakk>RB (height t') t; invc t'; invh t'\<rbrakk> \<Longrightarrow> bheight t \<le> bheight t'"
   2.179 -using RB_b_height RB_h red_b_height2 by fastforce
   2.180 -
   2.181 -lemma RB_minimal: "RB (height t') t \<Longrightarrow> invh t \<Longrightarrow> invc t' \<Longrightarrow> invh t' \<Longrightarrow> size t \<le> size t'"
   2.182 -proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct)
   2.183 -  case 1 thus ?case by auto 
   2.184 -next
   2.185 -  case (2 h t t'')
   2.186 -  have ***: "size (Node c t'' () t) \<le> size t'"
   2.187 -    if assms:
   2.188 -      "\<And> (t' :: 'a rbt) . \<lbrakk> h = height t'; invh t''; invc t'; invh t' \<rbrakk>
   2.189 -                            \<Longrightarrow> size t'' \<le> size t'"
   2.190 -      "Suc h = height t'" "balB (h div 2) t" "RB h t''"
   2.191 -      "invc t'" "invh t'" "height l \<ge> height r"
   2.192 -      and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)"
   2.193 -  for t' :: "'a rbt" and c l a r
   2.194 -  proof -
   2.195 -    from assms have inv: "invc r" "invh r" by auto
   2.196 -    from assms have "height l = h" using max_def by auto
   2.197 -    with RB_bheight_minimal[of l t''] have
   2.198 -      "bheight t \<le> bheight r" using assms last by auto
   2.199 -    with compact_pt[OF inv] balB_h balB_hs have 
   2.200 -      "size t \<le> size r" using assms(3) by auto moreover
   2.201 -    have "size t'' \<le> size l" using assms last by auto ultimately
   2.202 -    show ?thesis by simp
   2.203 -  qed
   2.204 -  
   2.205 -  from 2 obtain c l a r where 
   2.206 -    t': "t' = Node c l a r" by (cases t') auto
   2.207 -  with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto
   2.208 -  show ?case proof (cases "height r \<le> height l")
   2.209 -    case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto
   2.210 -  next
   2.211 -    case False 
   2.212 -    obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto
   2.213 -    have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto
   2.214 -    thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto
   2.215 -  qed
   2.216 -qed
   2.217 -
   2.218 -lemma RB_size: "RB h t \<Longrightarrow> size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)"
   2.219 -by (induction h t rule: "RB.induct" ) auto
   2.220 -
   2.221 -lemma RB_exist: "\<exists> t . RB h t"
   2.222 -proof (induction h) 
   2.223 -  case (Suc n)
   2.224 -  obtain r where r: "balB (n div 2) r"  using  exist_pt by blast
   2.225 -  obtain l where l: "RB n l"  using  Suc by blast
   2.226 -  obtain t where 
   2.227 -    "color l = Red   \<Longrightarrow> t = B l () r"
   2.228 -    "color l = Black \<Longrightarrow> t = R l () r" by auto
   2.229 -  with l and r have "RB (Suc n) t" by (cases "color l") auto
   2.230 -  thus ?case by auto
   2.231 -qed auto
   2.232 -
   2.233 -lemma bound:
   2.234 -  assumes "invc t"  "invh t" and [simp]:"height t = h"
   2.235 -  shows "size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   2.236 -proof -
   2.237 -  obtain t' where t': "RB h t'" using RB_exist by auto
   2.238 -  show ?thesis using RB_size[OF t'] 
   2.239 -  RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t' 
   2.240 -  unfolding  size1_def by auto
   2.241 -qed
   2.242 -
   2.243 -corollary "rbt t \<Longrightarrow> h = height t \<Longrightarrow> size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   2.244 -using bound unfolding rbt_def by blast
   2.245 -
   2.246  end