simplified delete/proof
authornipkow
Wed Jun 14 19:39:12 2017 +0200 (23 months ago)
changeset 660876e0c330f4051
parent 66086 3f7067ba5df3
child 66088 c9c9438cfc0f
simplified delete/proof
src/HOL/Data_Structures/RBT_Set.thy
     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)"