--- a/src/HOL/Data_Structures/RBT.thy Fri Jan 27 12:32:49 2017 +0100
+++ b/src/HOL/Data_Structures/RBT.thy Fri Jan 27 17:28:10 2017 +0100
@@ -14,13 +14,18 @@
abbreviation B where "B l a r \<equiv> Node Black l a r"
fun bal :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-(* The first line is superfluous; it merely speeds up pattern compilation *)
-"bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
"bal (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
"bal (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
"bal t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
"bal t1 a t2 = B t1 a t2"
+(* Warning: takes 30 secs to compile (2017) *)
+text\<open>Markus Reiter and Alexander Krauss added a first line not found in Okasaki:
+@{prop "bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)"}
+The motivation is unclear. However: it speeds up pattern compilation
+and lemma \<open>invc_bal\<close> below can be simplified to
+ @{prop "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)"}
+All other proofs are unaffected.\<close>
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"paint c Leaf = Leaf" |
--- a/src/HOL/Data_Structures/RBT_Set.thy Fri Jan 27 12:32:49 2017 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy Fri Jan 27 17:28:10 2017 +0100
@@ -91,7 +91,7 @@
subsection \<open>Structural invariants\<close>
-text\<open>The proofs are due to Markus Reiter and Alexander Krauss,\<close>
+text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
fun color :: "'a rbt \<Rightarrow> color" where
"color Leaf = Black" |
@@ -135,7 +135,8 @@
lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
by (cases t) auto
-lemma invc_bal: "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)"
+lemma invc_bal:
+ "\<lbrakk>invc l \<and> invc_sons r \<or> invc_sons l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)"
by (induct l a r rule: bal.induct) auto
lemma bheight_bal:
@@ -314,224 +315,4 @@
thus ?thesis by simp
qed
-text \<open>By Daniel St\"uwe\<close>
-
-lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
- (\<exists> l a r . t = R l a r \<and> color l = Black \<and> color r = Black \<and> invc l \<and> invc r)"
-by (cases t) auto
-
-lemma rbt_induct[consumes 1]:
- assumes "rbt t"
- assumes [simp]: "P Leaf"
- assumes "\<And> t l a r. \<lbrakk>t = B l a r; invc t; invh t; Q(l); Q(r)\<rbrakk> \<Longrightarrow> P t"
- assumes "\<And> t l a r. \<lbrakk>t = R l a r; invc t; invh t; P(l); P(r)\<rbrakk> \<Longrightarrow> Q t"
- assumes "\<And> t . P(t) \<Longrightarrow> Q(t)"
- shows "P t"
-using assms(1) unfolding rbt_def apply safe
-proof (induction t rule: measure_induct[of size])
-case (1 t)
- note * = 1 assms
- show ?case proof (cases t)
- case [simp]: (Node c l a r)
- show ?thesis proof (cases c)
- case Red thus ?thesis using 1 by simp
- next
- case [simp]: Black
- show ?thesis
- proof (cases "color l")
- case Red
- thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
- next
- case Black
- thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
- qed
- qed
- qed simp
-qed
-
-lemma rbt_b_height: "rbt t \<Longrightarrow> bheight t * 2 \<ge> height t"
-by (induction t rule: rbt_induct[where Q="\<lambda> t. bheight t * 2 + 1 \<ge> height t"]) auto
-
-lemma red_b_height: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t * 2 + 1 \<ge> height t"
-apply (cases t) apply simp
- using rbt_b_height unfolding rbt_def
- by (cases "color t") fastforce+
-
-lemma red_b_height2: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t \<ge> height t div 2"
-using red_b_height by fastforce
-
-lemma rbt_b_height2: "bheight t \<le> height t"
-by (induction t) auto
-
-lemma "rbt t \<Longrightarrow> size1 t \<le> 4 ^ (bheight t)"
-by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le> 2 * 4 ^ (bheight t)"]) auto
-
-text \<open>Balanced red-balck tree with all black nodes:\<close>
-inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
-"balB 0 Leaf" |
-"balB h t \<Longrightarrow> balB (Suc h) (B t () t)"
-
-inductive_cases [elim!]: "balB 0 t"
-inductive_cases [elim]: "balB (Suc h) t"
-
-lemma balB_hs: "balB h t \<Longrightarrow> bheight t = height t"
-by (induction h t rule: "balB.induct") auto
-
-lemma balB_h: "balB h t \<Longrightarrow> h = height t"
-by (induction h t rule: "balB.induct") auto
-
-lemma "rbt t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
-by (induction t arbitrary: t'
- rule: rbt_induct[where Q="\<lambda> t . \<forall> h t'. balB (bheight t) t' \<longrightarrow> size t' \<le> size t"])
- fastforce+
-
-lemma balB_bh: "invc t \<Longrightarrow> invh t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
-by (induction t arbitrary: t') (fastforce split: if_split_asm)+
-
-lemma balB_bh3:"\<lbrakk> balB h t; balB (h' + h) t' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
-by (induction h t arbitrary: t' h' rule: balB.induct) fastforce+
-
-corollary balB_bh3': "\<lbrakk> balB h t; balB h' t'; h \<le> h' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
-using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps)
-
-lemma exist_pt: "\<exists> t . balB h t"
-by (induction h) (auto intro: balB.intros)
-
-corollary compact_pt:
- assumes "invc t" "invh t" "h \<le> bheight t" "balB h t'"
- shows "size t' \<le> size t"
-proof -
- obtain t'' where "balB (bheight t) t''" using exist_pt by blast
- thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto
-qed
-
-lemma balB_bh2: "balB (bheight t) t'\<Longrightarrow> invc t \<Longrightarrow> invh t \<Longrightarrow> height t' \<le> height t"
-apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct)
-using balB_h rbt_b_height2 by auto
-
-lemma balB_rbt: "balB h t \<Longrightarrow> rbt t"
-unfolding rbt_def
-by (induction h t rule: balB.induct) auto
-
-lemma balB_size[simp]: "balB h t \<Longrightarrow> size1 t = 2^h"
-by (induction h t rule: balB.induct) auto
-
-text \<open>Red-black tree (except that the root may be red) of minimal size
-for a given height:\<close>
-
-inductive RB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
-"RB 0 Leaf" |
-"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Red \<Longrightarrow> RB (Suc h) (B t' () t)" |
-"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Black \<Longrightarrow> RB (Suc h) (R t' () t)"
-
-lemmas RB.intros[intro]
-
-lemma RB_invc: "RB h t \<Longrightarrow> invc t"
-apply (induction h t rule: RB.induct)
-using balB_rbt unfolding rbt_def by auto
-
-lemma RB_h: "RB h t \<Longrightarrow> h = height t"
-apply (induction h t rule: RB.induct)
-using balB_h by auto
-
-lemma RB_mod: "RB h t \<Longrightarrow> (color t = Black \<longleftrightarrow> h mod 2 = 0)"
-apply (induction h t rule: RB.induct)
-apply auto
-by presburger
-
-lemma RB_b_height: "RB h t \<Longrightarrow> height t div 2 = bheight t"
-proof (induction h t rule: RB.induct)
- case 1
- thus ?case by auto
-next
- case (2 h t t')
- with RB_mod obtain n where "2*n + 1 = h"
- by (metis color.distinct(1) mult_div_mod_eq parity)
- with 2 balB_h RB_h show ?case by auto
-next
- case (3 h t t')
- with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast
- with 3 balB_h RB_h show ?case by auto
-qed
-
-lemma weak_RB_induct[consumes 1]:
- "RB h t \<Longrightarrow> P 0 \<langle>\<rangle> \<Longrightarrow> (\<And>h t t' c . balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow>
- P h t' \<Longrightarrow> P (Suc h) (Node c t' () t)) \<Longrightarrow> P h t"
-using RB.induct by metis
-
-lemma RB_invh: "RB h t \<Longrightarrow> invh t"
-apply (induction h t rule: weak_RB_induct)
- using balB_h balB_hs RB_h balB_rbt RB_b_height
- unfolding rbt_def
-by auto
-
-lemma RB_bheight_minimal:
- "\<lbrakk>RB (height t') t; invc t'; invh t'\<rbrakk> \<Longrightarrow> bheight t \<le> bheight t'"
-using RB_b_height RB_h red_b_height2 by fastforce
-
-lemma RB_minimal: "RB (height t') t \<Longrightarrow> invh t \<Longrightarrow> invc t' \<Longrightarrow> invh t' \<Longrightarrow> size t \<le> size t'"
-proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct)
- case 1 thus ?case by auto
-next
- case (2 h t t'')
- have ***: "size (Node c t'' () t) \<le> size t'"
- if assms:
- "\<And> (t' :: 'a rbt) . \<lbrakk> h = height t'; invh t''; invc t'; invh t' \<rbrakk>
- \<Longrightarrow> size t'' \<le> size t'"
- "Suc h = height t'" "balB (h div 2) t" "RB h t''"
- "invc t'" "invh t'" "height l \<ge> height r"
- and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)"
- for t' :: "'a rbt" and c l a r
- proof -
- from assms have inv: "invc r" "invh r" by auto
- from assms have "height l = h" using max_def by auto
- with RB_bheight_minimal[of l t''] have
- "bheight t \<le> bheight r" using assms last by auto
- with compact_pt[OF inv] balB_h balB_hs have
- "size t \<le> size r" using assms(3) by auto moreover
- have "size t'' \<le> size l" using assms last by auto ultimately
- show ?thesis by simp
- qed
-
- from 2 obtain c l a r where
- t': "t' = Node c l a r" by (cases t') auto
- with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto
- show ?case proof (cases "height r \<le> height l")
- case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto
- next
- case False
- obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto
- have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto
- thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto
- qed
-qed
-
-lemma RB_size: "RB h t \<Longrightarrow> size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)"
-by (induction h t rule: "RB.induct" ) auto
-
-lemma RB_exist: "\<exists> t . RB h t"
-proof (induction h)
- case (Suc n)
- obtain r where r: "balB (n div 2) r" using exist_pt by blast
- obtain l where l: "RB n l" using Suc by blast
- obtain t where
- "color l = Red \<Longrightarrow> t = B l () r"
- "color l = Black \<Longrightarrow> t = R l () r" by auto
- with l and r have "RB (Suc n) t" by (cases "color l") auto
- thus ?case by auto
-qed auto
-
-lemma bound:
- assumes "invc t" "invh t" and [simp]:"height t = h"
- shows "size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
-proof -
- obtain t' where t': "RB h t'" using RB_exist by auto
- show ?thesis using RB_size[OF t']
- RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t'
- unfolding size1_def by auto
-qed
-
-corollary "rbt t \<Longrightarrow> h = height t \<Longrightarrow> size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
-using bound unfolding rbt_def by blast
-
end