# HG changeset patch # User nipkow # Date 1448820114 -3600 # Node ID 862daa8144f337d264198c91fcd11f504791f474 # Parent 865bb718bdb986f8f3d9ca1623aeb7042f33087d RBT invariants for insert diff -r 865bb718bdb9 -r 862daa8144f3 src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Sat Nov 28 23:59:08 2015 +0100 +++ b/src/HOL/Data_Structures/RBT_Set.thy Sun Nov 29 19:01:54 2015 +0100 @@ -101,4 +101,178 @@ case 4 thus ?case by(simp add: inorder_delete) qed auto + +subsection \Structural invariants\ + +fun color :: "'a rbt \ color" where +"color Leaf = Black" | +"color (Node c _ _ _) = c" + +fun bheight :: "'a rbt \ nat" where +"bheight Leaf = 0" | +"bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)" + +fun inv1 :: "'a rbt \ bool" where +"inv1 Leaf = True" | +"inv1 (Node c l a r) = + (inv1 l \ inv1 r \ (c = Black \ color l = Black \ color r = Black))" + +fun inv1_root :: "'a rbt \ bool" \ \Weaker version\ where +"inv1_root Leaf = True" | +"inv1_root (Node c l a r) = (inv1 l \ inv1 r)" + +fun inv2 :: "'a rbt \ bool" where +"inv2 Leaf = True" | +"inv2 (Node c l x r) = (inv2 l \ inv2 r \ bheight l = bheight r)" + +lemma inv1_rootI[simp]: "inv1 t \ inv1_root t" +by (cases t) simp+ + +definition rbt :: "'a rbt \ bool" where +"rbt t = (inv1 t \ inv2 t \ color t = Black)" + +lemma color_paint_Black: "color (paint Black t) = Black" +by (cases t) auto + +theorem rbt_Leaf: "rbt Leaf" +by (simp add: rbt_def) + +lemma paint_inv1_root: "inv1_root t \ inv1_root (paint c t)" +by (cases t) auto + +lemma inv1_paint_Black: "inv1_root t \ inv1 (paint Black t)" +by (cases t) auto + +lemma inv2_paint: "inv2 t \ inv2 (paint c t)" +by (cases t) auto + +lemma inv1_bal: "\inv1_root l; inv1_root r\ \ inv1 (bal l a r)" +by (induct l a r rule: bal.induct) auto + +lemma bheight_bal: + "bheight l = bheight r \ bheight (bal l a r) = Suc (bheight l)" +by (induct l a r rule: bal.induct) auto + +lemma inv2_bal: + "\ inv2 l; inv2 r; bheight l = bheight r \ \ inv2 (bal l a r)" +by (induct l a r rule: bal.induct) auto + + +subsubsection \Insertion\ + +lemma inv1_ins: assumes "inv1 t" + shows "color t = Black \ inv1 (ins x t)" "inv1_root (ins x t)" +using assms +by (induct x t rule: ins.induct) (auto simp: inv1_bal) + +lemma inv2_ins: assumes "inv2 t" + shows "inv2 (ins x t)" "bheight (ins x t) = bheight t" +using assms +by (induct x t rule: ins.induct) (auto simp: inv2_bal bheight_bal) + +theorem rbt_ins: "rbt t \ rbt (insert x t)" +by (simp add: inv1_ins inv2_ins color_paint_Black inv1_paint_Black inv2_paint + rbt_def insert_def) + +(* +lemma bheight_paintR'[simp]: "color t = Black \ bheight (paint Red t) = bheight t - 1" +by (cases t) auto + +lemma balL_inv2_with_inv1: + assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt" + shows "bheight (balL lt a rt) = bheight lt + 1" "inv2 (balL lt a rt)" +using assms +by (induct lt a rt rule: balL.induct) (auto simp: inv2_bal inv2_paint bheight_bal) + +lemma balL_inv2_app: + assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color rt = Black" + shows "inv2 (balL lt a rt)" + "bheight (balL lt a rt) = bheight rt" +using assms +by (induct lt a rt rule: balL.induct) (auto simp add: inv2_bal bheight_bal) + +lemma balL_inv1: "\inv1_root l; inv1 r; color r = Black\ \ inv1 (balL l a r)" +by (induct l a r rule: balL.induct) (simp_all add: inv1_bal) + +lemma balL_inv1_root: "\ inv1_root lt; inv1 rt \ \ inv1_root (balL lt a rt)" +by (induct lt a rt rule: balL.induct) (auto simp: inv1_bal paint_inv1_root) + +lemma balR_inv2_with_inv1: + assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt" + shows "inv2 (balR lt a rt) \ bheight (balR lt a rt) = bheight lt" +using assms +by(induct lt a rt rule: balR.induct)(auto simp: inv2_bal bheight_bal inv2_paint) + +lemma balR_inv1: "\inv1 a; inv1_root b; color a = Black\ \ inv1 (balR a x b)" +by (induct a x b rule: balR.induct) (simp_all add: inv1_bal) + +lemma balR_inv1_root: "\ inv1 lt; inv1_root rt \ \inv1_root (balR lt x rt)" +by (induct lt x rt rule: balR.induct) (auto simp: inv1_bal paint_inv1_root) + +lemma combine_inv2: + assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt" + shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)" +using assms +by (induct lt rt rule: combine.induct) + (auto simp: balL_inv2_app split: tree.splits color.splits) + +lemma combine_inv1: + assumes "inv1 lt" "inv1 rt" + shows "color lt = Black \ color rt = Black \ inv1 (combine lt rt)" + "inv1_root (combine lt rt)" +using assms +by (induct lt rt rule: combine.induct) + (auto simp: balL_inv1 split: tree.splits color.splits) + + +lemma + assumes "inv2 lt" "inv1 lt" + shows + "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \ + inv2 (rbt_del_from_left x lt k v rt) \ + bheight (rbt_del_from_left x lt k v rt) = bheight lt \ + (color_of lt = B \ color_of rt = B \ inv1 (rbt_del_from_left x lt k v rt) \ + (color_of lt \ B \ color_of rt \ B) \ inv1l (rbt_del_from_left x lt k v rt))" + and "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \ + inv2 (rbt_del_from_right x lt k v rt) \ + bheight (rbt_del_from_right x lt k v rt) = bheight lt \ + (color_of lt = B \ color_of rt = B \ inv1 (rbt_del_from_right x lt k v rt) \ + (color_of lt \ B \ color_of rt \ B) \ inv1l (rbt_del_from_right x lt k v rt))" + and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \ (color_of lt = R \ bheight (rbt_del x lt) = bheight lt \ inv1 (rbt_del x lt) + \ color_of lt = B \ bheight (rbt_del x lt) = bheight lt - 1 \ inv1l (rbt_del x lt))" +using assms +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) +case (2 y c _ y') + have "y = y' \ y < y' \ y > y'" by auto + thus ?case proof (elim disjE) + assume "y = y'" + with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+ + next + assume "y < y'" + with 2 show ?thesis by (cases c) auto + next + assume "y' < y" + with 2 show ?thesis by (cases c) auto + qed +next + case (3 y lt z v rta y' ss bb) + thus ?case by (cases "color_of (Branch B lt z v rta) = B \ color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+ +next + case (5 y a y' ss lt z v rta) + thus ?case by (cases "color_of a = B \ color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+ +next + case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \ color_of Empty = B") simp+ +qed auto + +theorem rbt_delete_is_rbt [simp]: assumes "rbt t" shows "rbt (delete k t)" +proof - + from assms have "inv2 t" and "inv1 t" unfolding rbt_def by auto + hence "inv2 (del k t) \ (color t = Red \ bheight (del k t) = bheight t \ inv1 (del k t) \ color t = Black \ bheight (del k t) = bheight t - 1 \ inv1_root (del k t))" + by (rule rbt_del_inv1_inv2) + hence "inv2 (del k t) \ inv1l (rbt_del k t)" by (cases "color_of t") auto + with assms show ?thesis + unfolding is_rbt_def rbt_delete_def + by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted) +qed +*) end