src/HOL/Data_Structures/RBT_Set.thy
changeset 61754 862daa8144f3
parent 61749 7f530d7e552d
child 62526 347150095fd2
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Nov 28 23:59:08 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sun Nov 29 19:01:54 2015 +0100
     1.3 @@ -101,4 +101,178 @@
     1.4    case 4 thus ?case by(simp add: inorder_delete)
     1.5  qed auto
     1.6  
     1.7 +
     1.8 +subsection \<open>Structural invariants\<close>
     1.9 +
    1.10 +fun color :: "'a rbt \<Rightarrow> color" where
    1.11 +"color Leaf = Black" |
    1.12 +"color (Node c _ _ _) = c"
    1.13 +
    1.14 +fun bheight :: "'a rbt \<Rightarrow> nat" where
    1.15 +"bheight Leaf = 0" |
    1.16 +"bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)"
    1.17 +
    1.18 +fun inv1 :: "'a rbt \<Rightarrow> bool" where
    1.19 +"inv1 Leaf = True" |
    1.20 +"inv1 (Node c l a r) =
    1.21 +  (inv1 l \<and> inv1 r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
    1.22 +
    1.23 +fun inv1_root :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
    1.24 +"inv1_root Leaf = True" |
    1.25 +"inv1_root (Node c l a r) = (inv1 l \<and> inv1 r)"
    1.26 +
    1.27 +fun inv2 :: "'a rbt \<Rightarrow> bool" where
    1.28 +"inv2 Leaf = True" |
    1.29 +"inv2 (Node c l x r) = (inv2 l \<and> inv2 r \<and> bheight l = bheight r)"
    1.30 +
    1.31 +lemma inv1_rootI[simp]: "inv1 t \<Longrightarrow> inv1_root t"
    1.32 +by (cases t) simp+
    1.33 +
    1.34 +definition rbt :: "'a rbt \<Rightarrow> bool" where
    1.35 +"rbt t = (inv1 t \<and> inv2 t \<and> color t = Black)"
    1.36 +
    1.37 +lemma color_paint_Black: "color (paint Black t) = Black"
    1.38 +by (cases t) auto
    1.39 +
    1.40 +theorem rbt_Leaf: "rbt Leaf"
    1.41 +by (simp add: rbt_def)
    1.42 +
    1.43 +lemma paint_inv1_root: "inv1_root t \<Longrightarrow> inv1_root (paint c t)"
    1.44 +by (cases t) auto
    1.45 +
    1.46 +lemma inv1_paint_Black: "inv1_root t \<Longrightarrow> inv1 (paint Black t)"
    1.47 +by (cases t) auto
    1.48 +
    1.49 +lemma inv2_paint: "inv2 t \<Longrightarrow> inv2 (paint c t)"
    1.50 +by (cases t) auto
    1.51 +
    1.52 +lemma inv1_bal: "\<lbrakk>inv1_root l; inv1_root r\<rbrakk> \<Longrightarrow> inv1 (bal l a r)" 
    1.53 +by (induct l a r rule: bal.induct) auto
    1.54 +
    1.55 +lemma bheight_bal:
    1.56 +  "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
    1.57 +by (induct l a r rule: bal.induct) auto
    1.58 +
    1.59 +lemma inv2_bal: 
    1.60 +  "\<lbrakk> inv2 l; inv2 r; bheight l = bheight r \<rbrakk> \<Longrightarrow> inv2 (bal l a r)"
    1.61 +by (induct l a r rule: bal.induct) auto
    1.62 +
    1.63 +
    1.64 +subsubsection \<open>Insertion\<close>
    1.65 +
    1.66 +lemma inv1_ins: assumes "inv1 t"
    1.67 +  shows "color t = Black \<Longrightarrow> inv1 (ins x t)" "inv1_root (ins x t)"
    1.68 +using assms
    1.69 +by (induct x t rule: ins.induct) (auto simp: inv1_bal)
    1.70 +
    1.71 +lemma inv2_ins: assumes "inv2 t"
    1.72 +  shows "inv2 (ins x t)" "bheight (ins x t) = bheight t"
    1.73 +using assms
    1.74 +by (induct x t rule: ins.induct) (auto simp: inv2_bal bheight_bal)
    1.75 +
    1.76 +theorem rbt_ins: "rbt t \<Longrightarrow> rbt (insert x t)"
    1.77 +by (simp add: inv1_ins inv2_ins color_paint_Black inv1_paint_Black inv2_paint
    1.78 +  rbt_def insert_def)
    1.79 +
    1.80 +(*
    1.81 +lemma bheight_paintR'[simp]: "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
    1.82 +by (cases t) auto
    1.83 +
    1.84 +lemma balL_inv2_with_inv1:
    1.85 +  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
    1.86 +  shows "bheight (balL lt a rt) = bheight lt + 1"  "inv2 (balL lt a rt)"
    1.87 +using assms 
    1.88 +by (induct lt a rt rule: balL.induct) (auto simp: inv2_bal inv2_paint bheight_bal)
    1.89 +
    1.90 +lemma balL_inv2_app: 
    1.91 +  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color rt = Black"
    1.92 +  shows "inv2 (balL lt a rt)" 
    1.93 +        "bheight (balL lt a rt) = bheight rt"
    1.94 +using assms 
    1.95 +by (induct lt a rt rule: balL.induct) (auto simp add: inv2_bal bheight_bal) 
    1.96 +
    1.97 +lemma balL_inv1: "\<lbrakk>inv1_root l; inv1 r; color r = Black\<rbrakk> \<Longrightarrow> inv1 (balL l a r)"
    1.98 +by (induct l a r rule: balL.induct) (simp_all add: inv1_bal)
    1.99 +
   1.100 +lemma balL_inv1_root: "\<lbrakk> inv1_root lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1_root (balL lt a rt)"
   1.101 +by (induct lt a rt rule: balL.induct) (auto simp: inv1_bal paint_inv1_root)
   1.102 +
   1.103 +lemma balR_inv2_with_inv1:
   1.104 +  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
   1.105 +  shows "inv2 (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
   1.106 +using assms
   1.107 +by(induct lt a rt rule: balR.induct)(auto simp: inv2_bal bheight_bal inv2_paint)
   1.108 +
   1.109 +lemma balR_inv1: "\<lbrakk>inv1 a; inv1_root b; color a = Black\<rbrakk> \<Longrightarrow> inv1 (balR a x b)"
   1.110 +by (induct a x b rule: balR.induct) (simp_all add: inv1_bal)
   1.111 +
   1.112 +lemma balR_inv1_root: "\<lbrakk> inv1 lt; inv1_root rt \<rbrakk> \<Longrightarrow>inv1_root (balR lt x rt)"
   1.113 +by (induct lt x rt rule: balR.induct) (auto simp: inv1_bal paint_inv1_root)
   1.114 +
   1.115 +lemma combine_inv2:
   1.116 +  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
   1.117 +  shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
   1.118 +using assms 
   1.119 +by (induct lt rt rule: combine.induct) 
   1.120 +   (auto simp: balL_inv2_app split: tree.splits color.splits)
   1.121 +
   1.122 +lemma combine_inv1: 
   1.123 +  assumes "inv1 lt" "inv1 rt"
   1.124 +  shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> inv1 (combine lt rt)"
   1.125 +         "inv1_root (combine lt rt)"
   1.126 +using assms 
   1.127 +by (induct lt rt rule: combine.induct)
   1.128 +   (auto simp: balL_inv1 split: tree.splits color.splits)
   1.129 +
   1.130 +
   1.131 +lemma 
   1.132 +  assumes "inv2 lt" "inv1 lt"
   1.133 +  shows
   1.134 +  "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   1.135 +   inv2 (rbt_del_from_left x lt k v rt) \<and> 
   1.136 +   bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and> 
   1.137 +   (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or> 
   1.138 +    (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))"
   1.139 +  and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   1.140 +  inv2 (rbt_del_from_right x lt k v rt) \<and> 
   1.141 +  bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and> 
   1.142 +  (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or> 
   1.143 +   (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))"
   1.144 +  and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \<and> (color_of lt = R \<and> bheight (rbt_del x lt) = bheight lt \<and> inv1 (rbt_del x lt) 
   1.145 +  \<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt - 1 \<and> inv1l (rbt_del x lt))"
   1.146 +using assms
   1.147 +proof (induct x lt k v rt and x lt k v rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   1.148 +case (2 y c _ y')
   1.149 +  have "y = y' \<or> y < y' \<or> y > y'" by auto
   1.150 +  thus ?case proof (elim disjE)
   1.151 +    assume "y = y'"
   1.152 +    with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
   1.153 +  next
   1.154 +    assume "y < y'"
   1.155 +    with 2 show ?thesis by (cases c) auto
   1.156 +  next
   1.157 +    assume "y' < y"
   1.158 +    with 2 show ?thesis by (cases c) auto
   1.159 +  qed
   1.160 +next
   1.161 +  case (3 y lt z v rta y' ss bb) 
   1.162 +  thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
   1.163 +next
   1.164 +  case (5 y a y' ss lt z v rta)
   1.165 +  thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
   1.166 +next
   1.167 +  case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
   1.168 +qed auto
   1.169 +
   1.170 +theorem rbt_delete_is_rbt [simp]: assumes "rbt t" shows "rbt (delete k t)"
   1.171 +proof -
   1.172 +  from assms have "inv2 t" and "inv1 t" unfolding rbt_def by auto 
   1.173 +  hence "inv2 (del k t) \<and> (color t = Red \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color t = Black \<and> bheight (del k t) = bheight t - 1 \<and> inv1_root (del k t))"
   1.174 +    by (rule rbt_del_inv1_inv2)
   1.175 +  hence "inv2 (del k t) \<and> inv1l (rbt_del k t)" by (cases "color_of t") auto
   1.176 +  with assms show ?thesis
   1.177 +    unfolding is_rbt_def rbt_delete_def
   1.178 +    by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted)
   1.179 +qed
   1.180 +*)
   1.181  end