src/HOL/Data_Structures/RBT_Set.thy
 changeset 66087 6e0c330f4051 parent 64960 8be78855ee7a child 66088 c9c9438cfc0f
```     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Jun 13 22:39:57 2017 +0200
1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 14 19:39:12 2017 +0200
1.3 @@ -26,20 +26,19 @@
1.4  definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
1.5  "insert x t = paint Black (ins x t)"
1.6
1.7 -fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
1.8 -and delL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
1.9 -and delR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
1.10 -where
1.11 +fun color :: "'a rbt \<Rightarrow> color" where
1.12 +"color Leaf = Black" |
1.13 +"color (Node c _ _ _) = c"
1.14 +
1.15 +fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
1.16  "del x Leaf = Leaf" |
1.17  "del x (Node _ l a r) =
1.18    (case cmp x a of
1.19 -     LT \<Rightarrow> delL x l a r |
1.20 -     GT \<Rightarrow> delR x l a r |
1.21 -     EQ \<Rightarrow> combine l r)" |
1.22 -"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
1.23 -"delL x l a r = R (del x l) a r" |
1.24 -"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" |
1.25 -"delR x l a r = R l a (del x r)"
1.26 +     LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
1.27 +           then baldL (del x l) a r else R (del x l) a r |
1.28 +     GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
1.29 +           then baldR l a (del x r) else R l a (del x r) |
1.30 +     EQ \<Rightarrow> combine l r)"
1.31
1.32  definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
1.33  "delete x t = paint Black (del x t)"
1.34 @@ -84,11 +83,7 @@
1.35
1.36  lemma inorder_del:
1.37   "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
1.38 - "sorted(inorder l) \<Longrightarrow>  inorder(delL x l a r) =
1.39 -    del_list x (inorder l) @ a # inorder r"
1.40 - "sorted(inorder r) \<Longrightarrow>  inorder(delR x l a r) =
1.41 -    inorder l @ a # del_list x (inorder r)"
1.42 -by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
1.43 +by(induction x t rule: del.induct)
1.44    (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
1.45
1.46  lemma inorder_delete:
1.47 @@ -100,10 +95,6 @@
1.48
1.49  text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
1.50
1.51 -fun color :: "'a rbt \<Rightarrow> color" where
1.52 -"color Leaf = Black" |
1.53 -"color (Node c _ _ _) = c"
1.54 -
1.55  fun bheight :: "'a rbt \<Rightarrow> nat" where
1.56  "bheight Leaf = 0" |
1.57  "bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
1.58 @@ -181,7 +172,7 @@
1.59    (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
1.60
1.61  theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
1.62 -by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
1.63 +by (simp add: invc_ins(2) invh_ins(1) color_paint_Black invc_paint_Black invh_paint
1.64    rbt_def insert_def)
1.65
1.66
1.67 @@ -191,30 +182,26 @@
1.68    "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
1.69  by (cases t) auto
1.70
1.71 -lemma baldL_invh_with_invc:
1.72 -  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r"
1.73 -  shows "bheight (baldL l a r) = bheight l + 1"  "invh (baldL l a r)"
1.74 -using assms
1.75 +lemma invh_baldL_invc:
1.76 +  "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  invc r \<rbrakk>
1.77 +   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1"
1.78  by (induct l a r rule: baldL.induct)
1.79     (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
1.80
1.81 -lemma baldL_invh_app:
1.82 -  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black"
1.83 -  shows "invh (baldL l a r)"
1.84 -        "bheight (baldL l a r) = bheight r"
1.85 -using assms
1.86 +lemma invh_baldL_Black:
1.87 +  "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  color r = Black \<rbrakk>
1.88 +   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
1.89  by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR)
1.90
1.91 -lemma baldL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
1.92 +lemma invc_baldL: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
1.93  by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
1.94
1.95 -lemma baldL_invc2: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
1.96 +lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
1.97  by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
1.98
1.99 -lemma baldR_invh_with_invc:
1.100 -  assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l"
1.101 -  shows "invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
1.102 -using assms
1.103 +lemma invh_baldR_invc:
1.104 +  "\<lbrakk> invh l;  invh r;  bheight l = bheight r + 1;  invc l \<rbrakk>
1.105 +  \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
1.106  by(induct l a r rule: baldR.induct)
1.107    (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
1.108
1.109 @@ -225,11 +212,10 @@
1.110  by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
1.111
1.112  lemma invh_combine:
1.113 -  assumes "invh l" "invh r" "bheight l = bheight r"
1.114 -  shows "bheight (combine l r) = bheight l" "invh (combine l r)"
1.115 -using assms
1.116 +  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk>
1.117 +  \<Longrightarrow> invh (combine l r) \<and> bheight (combine l r) = bheight l"
1.118  by (induct l r rule: combine.induct)
1.119 -   (auto simp: baldL_invh_app split: tree.splits color.splits)
1.120 +   (auto simp: invh_baldL_Black split: tree.splits color.splits)
1.121
1.122  lemma invc_combine:
1.123    assumes "invc l" "invc r"
1.124 @@ -237,27 +223,16 @@
1.125           "invc2 (combine l r)"
1.126  using assms
1.127  by (induct l r rule: combine.induct)
1.128 -   (auto simp: baldL_invc invc2I split: tree.splits color.splits)
1.129 -
1.130 +   (auto simp: invc_baldL invc2I split: tree.splits color.splits)
1.131
1.132 -lemma assumes "invh l" "invc l"
1.133 -  shows del_invc_invh:
1.134 -   "invh (del x l) \<and>
1.135 +lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>c l x r. t = Node c l x r"
1.136 +by(cases t) auto
1.137 +
1.138 +lemma del_invc_invh: "invh l \<Longrightarrow> invc l \<Longrightarrow> invh (del x l) \<and>
1.139     (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or>
1.140      color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))"
1.141 -and  "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
1.142 -   invh (delL x l k r) \<and>
1.143 -   bheight (delL x l k r) = bheight l \<and>
1.144 -   (color l = Black \<and> color r = Black \<and> invc (delL x l k r) \<or>
1.145 -    (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delL x l k r))"
1.146 -  and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
1.147 -  invh (delR x l k r) \<and>
1.148 -  bheight (delR x l k r) = bheight l \<and>
1.149 -  (color l = Black \<and> color r = Black \<and> invc (delR x l k r) \<or>
1.150 -   (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delR x l k r))"
1.151 -using assms
1.152 -proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct)
1.153 -case (2 y c _ y')
1.154 +proof (induct x l rule: del.induct)
1.155 +case (2 y c _ y' W)
1.156    have "y = y' \<or> y < y' \<or> y > y'" by auto
1.157    thus ?case proof (elim disjE)
1.158      assume "y = y'"
1.159 @@ -265,19 +240,15 @@
1.160      by (cases c) (simp_all add: invh_combine invc_combine)
1.161    next
1.162      assume "y < y'"
1.163 -    with 2 show ?thesis by (cases c) (auto simp: invc2I)
1.164 +    with 2 show ?thesis
1.165 +      by(cases c)
1.166 +        (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
1.167    next
1.168      assume "y' < y"
1.169 -    with 2 show ?thesis by (cases c) (auto simp: invc2I)
1.170 +    with 2 show ?thesis
1.171 +      by(cases c)
1.172 +        (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)
1.173    qed
1.174 -next
1.175 -  case (3 y l z ra y' bb)
1.176 -  thus ?case by (cases "color (Node Black l z ra) = Black \<and> color bb = Black") (simp add: baldL_invh_with_invc baldL_invc baldL_invc2)+
1.177 -next
1.178 -  case (5 y a y' l z ra)
1.179 -  thus ?case by (cases "color a = Black \<and> color (Node Black l z ra) = Black") (simp add: baldR_invh_with_invc invc_baldR invc2_baldR)+
1.180 -next
1.181 -  case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
1.182  qed auto
1.183
1.184  theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
```