tuned name
authornipkow
Fri Jan 27 17:35:08 2017 +0100 (2017-01-27)
changeset 64953f9cfb10761ff
parent 64952 f11e974b47e0
child 64954 e5f535f90d61
tuned name
src/HOL/Data_Structures/RBT_Set.thy
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 17:28:10 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 17:35:08 2017 +0100
     1.3 @@ -106,15 +106,15 @@
     1.4  "invc (Node c l a r) =
     1.5    (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
     1.6  
     1.7 -fun invc_sons :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
     1.8 -"invc_sons Leaf = True" |
     1.9 -"invc_sons (Node c l a r) = (invc l \<and> invc r)"
    1.10 +fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
    1.11 +"invc2 Leaf = True" |
    1.12 +"invc2 (Node c l a r) = (invc l \<and> invc r)"
    1.13  
    1.14  fun invh :: "'a rbt \<Rightarrow> bool" where
    1.15  "invh Leaf = True" |
    1.16  "invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
    1.17  
    1.18 -lemma invc_sonsI: "invc t \<Longrightarrow> invc_sons t"
    1.19 +lemma invc2I: "invc t \<Longrightarrow> invc2 t"
    1.20  by (cases t) simp+
    1.21  
    1.22  definition rbt :: "'a rbt \<Rightarrow> bool" where
    1.23 @@ -126,17 +126,17 @@
    1.24  theorem rbt_Leaf: "rbt Leaf"
    1.25  by (simp add: rbt_def)
    1.26  
    1.27 -lemma paint_invc_sons: "invc_sons t \<Longrightarrow> invc_sons (paint c t)"
    1.28 +lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)"
    1.29  by (cases t) auto
    1.30  
    1.31 -lemma invc_paint_Black: "invc_sons t \<Longrightarrow> invc (paint Black t)"
    1.32 +lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)"
    1.33  by (cases t) auto
    1.34  
    1.35  lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
    1.36  by (cases t) auto
    1.37  
    1.38  lemma invc_bal:
    1.39 -  "\<lbrakk>invc l \<and> invc_sons r \<or> invc_sons l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    1.40 +  "\<lbrakk>invc l \<and> invc2 r \<or> invc2 l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    1.41  by (induct l a r rule: bal.induct) auto
    1.42  
    1.43  lemma bheight_bal:
    1.44 @@ -151,9 +151,9 @@
    1.45  subsubsection \<open>Insertion\<close>
    1.46  
    1.47  lemma invc_ins: assumes "invc t"
    1.48 -  shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc_sons (ins x t)"
    1.49 +  shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
    1.50  using assms
    1.51 -by (induct x t rule: ins.induct) (auto simp: invc_bal invc_sonsI)
    1.52 +by (induct x t rule: ins.induct) (auto simp: invc_bal invc2I)
    1.53  
    1.54  lemma invh_ins: assumes "invh t"
    1.55    shows "invh (ins x t)" "bheight (ins x t) = bheight t"
    1.56 @@ -185,11 +185,11 @@
    1.57  using assms 
    1.58  by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) 
    1.59  
    1.60 -lemma balL_invc: "\<lbrakk>invc_sons l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
    1.61 +lemma balL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
    1.62  by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
    1.63  
    1.64 -lemma balL_invc_sons: "\<lbrakk> invc_sons lt; invc rt \<rbrakk> \<Longrightarrow> invc_sons (balL lt a rt)"
    1.65 -by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
    1.66 +lemma balL_invc2: "\<lbrakk> invc2 lt; invc rt \<rbrakk> \<Longrightarrow> invc2 (balL lt a rt)"
    1.67 +by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc2 invc2I)
    1.68  
    1.69  lemma balR_invh_with_invc:
    1.70    assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
    1.71 @@ -198,11 +198,11 @@
    1.72  by(induct lt a rt rule: balR.induct)
    1.73    (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
    1.74  
    1.75 -lemma invc_balR: "\<lbrakk>invc a; invc_sons b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
    1.76 +lemma invc_balR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
    1.77  by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
    1.78  
    1.79 -lemma invc_sons_balR: "\<lbrakk> invc lt; invc_sons rt \<rbrakk> \<Longrightarrow>invc_sons (balR lt x rt)"
    1.80 -by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
    1.81 +lemma invc2_balR: "\<lbrakk> invc lt; invc2 rt \<rbrakk> \<Longrightarrow>invc2 (balR lt x rt)"
    1.82 +by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc2 invc2I)
    1.83  
    1.84  lemma invh_combine:
    1.85    assumes "invh lt" "invh rt" "bheight lt = bheight rt"
    1.86 @@ -214,26 +214,26 @@
    1.87  lemma invc_combine: 
    1.88    assumes "invc lt" "invc rt"
    1.89    shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
    1.90 -         "invc_sons (combine lt rt)"
    1.91 +         "invc2 (combine lt rt)"
    1.92  using assms 
    1.93  by (induct lt rt rule: combine.induct)
    1.94 -   (auto simp: balL_invc invc_sonsI split: tree.splits color.splits)
    1.95 +   (auto simp: balL_invc invc2I split: tree.splits color.splits)
    1.96  
    1.97  
    1.98  lemma assumes "invh lt" "invc lt"
    1.99    shows
   1.100    del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt) 
   1.101 -  \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc_sons (del x lt))"
   1.102 +  \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc2 (del x lt))"
   1.103  and  "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   1.104     invh (delL x lt k rt) \<and> 
   1.105     bheight (delL x lt k rt) = bheight lt \<and> 
   1.106     (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or> 
   1.107 -    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delL x lt k rt))"
   1.108 +    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delL x lt k rt))"
   1.109    and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   1.110    invh (delR x lt k rt) \<and> 
   1.111    bheight (delR x lt k rt) = bheight lt \<and> 
   1.112    (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or> 
   1.113 -   (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delR x lt k rt))"
   1.114 +   (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delR x lt k rt))"
   1.115  using assms
   1.116  proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
   1.117  case (2 y c _ y')
   1.118 @@ -244,23 +244,23 @@
   1.119      by (cases c) (simp_all add: invh_combine invc_combine)
   1.120    next
   1.121      assume "y < y'"
   1.122 -    with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
   1.123 +    with 2 show ?thesis by (cases c) (auto simp: invc2I)
   1.124    next
   1.125      assume "y' < y"
   1.126 -    with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
   1.127 +    with 2 show ?thesis by (cases c) (auto simp: invc2I)
   1.128    qed
   1.129  next
   1.130    case (3 y lt z rta y' bb)
   1.131 -  thus ?case by (cases "color (Node Black lt z rta) = Black \<and> color bb = Black") (simp add: balL_invh_with_invc balL_invc balL_invc_sons)+
   1.132 +  thus ?case by (cases "color (Node Black lt z rta) = Black \<and> color bb = Black") (simp add: balL_invh_with_invc balL_invc balL_invc2)+
   1.133  next
   1.134    case (5 y a y' lt z rta)
   1.135 -  thus ?case by (cases "color a = Black \<and> color (Node Black lt z rta) = Black") (simp add: balR_invh_with_invc invc_balR invc_sons_balR)+
   1.136 +  thus ?case by (cases "color a = Black \<and> color (Node Black lt z rta) = Black") (simp add: balR_invh_with_invc invc_balR invc2_balR)+
   1.137  next
   1.138    case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
   1.139  qed auto
   1.140  
   1.141  theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
   1.142 -by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc_sonsI invh_paint)
   1.143 +by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
   1.144  
   1.145  text \<open>Overall correctness:\<close>
   1.146