# HG changeset patch
# User nipkow
# Date 1485534490 -3600
# Node ID f11e974b47e062276dfdbc684e4fb986465ad448
# Parent  140addd19343010186e4c0708871aff5c7d160f9
removed unclear clause; slower but clearer

diff -r 140addd19343 -r f11e974b47e0 src/HOL/Data_Structures/RBT.thy
--- 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" |
diff -r 140addd19343 -r f11e974b47e0 src/HOL/Data_Structures/RBT_Set.thy
--- 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