tuned
authornipkow
Thu Jun 15 11:11:36 2017 +0200 (23 months ago)
changeset 66088c9c9438cfc0f
parent 66087 6e0c330f4051
child 66089 def95e0bc529
tuned
src/HOL/Data_Structures/RBT_Set.thy
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Wed Jun 14 19:39:12 2017 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Jun 15 11:11:36 2017 +0200
     1.3 @@ -228,23 +228,23 @@
     1.4  lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>c l x r. t = Node c l x r"
     1.5  by(cases t) auto
     1.6  
     1.7 -lemma del_invc_invh: "invh l \<Longrightarrow> invc l \<Longrightarrow> invh (del x l) \<and>
     1.8 -   (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or>
     1.9 -    color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))"
    1.10 -proof (induct x l rule: del.induct)
    1.11 -case (2 y c _ y' W)
    1.12 -  have "y = y' \<or> y < y' \<or> y > y'" by auto
    1.13 +lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and>
    1.14 +   (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
    1.15 +    color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
    1.16 +proof (induct x t rule: del.induct)
    1.17 +case (2 x c _ y)
    1.18 +  have "x = y \<or> x < y \<or> x > y" by auto
    1.19    thus ?case proof (elim disjE)
    1.20 -    assume "y = y'"
    1.21 +    assume "x = y"
    1.22      with 2 show ?thesis
    1.23      by (cases c) (simp_all add: invh_combine invc_combine)
    1.24    next
    1.25 -    assume "y < y'"
    1.26 +    assume "x < y"
    1.27      with 2 show ?thesis
    1.28        by(cases c)
    1.29          (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
    1.30    next
    1.31 -    assume "y' < y"
    1.32 +    assume "y < x"
    1.33      with 2 show ?thesis
    1.34        by(cases c)
    1.35          (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)