# HG changeset patch # User nipkow # Date 1448643673 -3600 # Node ID 7f530d7e552dd94efafa79097213701a319db5a3 # Parent fc53fbf9fe016f03aea3220add86e01ffda2066f paint root black after insert and delete diff -r fc53fbf9fe01 -r 7f530d7e552d src/HOL/Data_Structures/RBT.thy --- a/src/HOL/Data_Structures/RBT.thy Wed Nov 25 15:58:22 2015 +0100 +++ b/src/HOL/Data_Structures/RBT.thy Fri Nov 27 18:01:13 2015 +0100 @@ -22,20 +22,20 @@ "bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" | "bal t1 a t2 = B t1 a t2" -fun red :: "'a rbt \ 'a rbt" where -"red Leaf = Leaf" | -"red (Node _ l a r) = R l a r" +fun paint :: "color \ 'a rbt \ 'a rbt" where +"paint c Leaf = Leaf" | +"paint c (Node _ l a r) = Node c l a r" fun balL :: "'a rbt \ 'a \ 'a rbt \ 'a rbt" where "balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" | "balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" | -"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (red t3))" | +"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (paint Red t3))" | "balL t1 x t2 = R t1 x t2" fun balR :: "'a rbt \ 'a \ 'a rbt \ 'a rbt" where "balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" | "balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" | -"balR (R t1 x (B t2 y t3)) z t4 = R (bal (red t1) x t2) y (B t3 z t4)" | +"balR (R t1 x (B t2 y t3)) z t4 = R (bal (paint Red t1) x t2) y (B t3 z t4)" | "balR t1 x t2 = R t1 x t2" fun combine :: "'a rbt \ 'a rbt \ 'a rbt" where diff -r fc53fbf9fe01 -r 7f530d7e552d src/HOL/Data_Structures/RBT_Map.thy --- a/src/HOL/Data_Structures/RBT_Map.thy Wed Nov 25 15:58:22 2015 +0100 +++ b/src/HOL/Data_Structures/RBT_Map.thy Fri Nov 27 18:01:13 2015 +0100 @@ -8,48 +8,61 @@ Lookup2 begin -fun update :: "'a::cmp \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where -"update x y Leaf = R Leaf (x,y) Leaf" | -"update x y (B l (a,b) r) = (case cmp x a of - LT \ bal (update x y l) (a,b) r | - GT \ bal l (a,b) (update x y r) | +fun upd :: "'a::cmp \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where +"upd x y Leaf = R Leaf (x,y) Leaf" | +"upd x y (B l (a,b) r) = (case cmp x a of + LT \ bal (upd x y l) (a,b) r | + GT \ bal l (a,b) (upd x y r) | EQ \ B l (x,y) r)" | -"update x y (R l (a,b) r) = (case cmp x a of - LT \ R (update x y l) (a,b) r | - GT \ R l (a,b) (update x y r) | +"upd x y (R l (a,b) r) = (case cmp x a of + LT \ R (upd x y l) (a,b) r | + GT \ R l (a,b) (upd x y r) | EQ \ R l (x,y) r)" -fun delete :: "'a::cmp \ ('a*'b)rbt \ ('a*'b)rbt" -and deleteL :: "'a::cmp \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" -and deleteR :: "'a::cmp \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" +definition update :: "'a::cmp \ 'b \ ('a*'b) rbt \ ('a*'b) rbt" where +"update x y t = paint Black (upd x y t)" + +fun del :: "'a::cmp \ ('a*'b)rbt \ ('a*'b)rbt" +and delL :: "'a::cmp \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" +and delR :: "'a::cmp \ ('a*'b)rbt \ 'a*'b \ ('a*'b)rbt \ ('a*'b)rbt" where -"delete x Leaf = Leaf" | -"delete x (Node c t1 (a,b) t2) = (case cmp x a of - LT \ deleteL x t1 (a,b) t2 | - GT \ deleteR x t1 (a,b) t2 | +"del x Leaf = Leaf" | +"del x (Node c t1 (a,b) t2) = (case cmp x a of + LT \ delL x t1 (a,b) t2 | + GT \ delR x t1 (a,b) t2 | EQ \ combine t1 t2)" | -"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" | -"deleteL x t1 a t2 = R (delete x t1) a t2" | -"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | -"deleteR x t1 a t2 = R t1 a (delete x t2)" +"delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" | +"delL x t1 a t2 = R (del x t1) a t2" | +"delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | +"delR x t1 a t2 = R t1 a (del x t2)" + +definition delete :: "'a::cmp \ ('a*'b) rbt \ ('a*'b) rbt" where +"delete x t = paint Black (del x t)" subsection "Functional Correctness Proofs" +lemma inorder_upd: + "sorted1(inorder t) \ inorder(upd x y t) = upd_list x y (inorder t)" +by(induction x y t rule: upd.induct) + (auto simp: upd_list_simps inorder_bal) + lemma inorder_update: "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" -by(induction x y t rule: update.induct) - (auto simp: upd_list_simps inorder_bal) +by(simp add: update_def inorder_upd inorder_paint) +lemma inorder_del: + "sorted1(inorder t1) \ inorder(del x t1) = del_list x (inorder t1)" and + "sorted1(inorder t1) \ inorder(delL x t1 a t2) = + del_list x (inorder t1) @ a # inorder t2" and + "sorted1(inorder t2) \ inorder(delR x t1 a t2) = + inorder t1 @ a # del_list x (inorder t2)" +by(induction x t1 and x t1 a t2 and x t1 a t2 rule: del_delL_delR.induct) + (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR) lemma inorder_delete: - "sorted1(inorder t1) \ inorder(delete x t1) = del_list x (inorder t1)" and - "sorted1(inorder t1) \ inorder(deleteL x t1 a t2) = - del_list x (inorder t1) @ a # inorder t2" and - "sorted1(inorder t2) \ inorder(deleteR x t1 a t2) = - inorder t1 @ a # del_list x (inorder t2)" -by(induction x t1 and x t1 a t2 and x t1 a t2 rule: delete_deleteL_deleteR.induct) - (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR) + "sorted1(inorder t) \ inorder(delete x t) = del_list x (inorder t)" +by(simp add: delete_def inorder_del inorder_paint) interpretation Map_by_Ordered where empty = Leaf and lookup = lookup and update = update and delete = delete diff -r fc53fbf9fe01 -r 7f530d7e552d src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Wed Nov 25 15:58:22 2015 +0100 +++ b/src/HOL/Data_Structures/RBT_Set.thy Fri Nov 27 18:01:13 2015 +0100 @@ -9,70 +9,84 @@ Isin2 begin -fun insert :: "'a::cmp \ 'a rbt \ 'a rbt" where -"insert x Leaf = R Leaf x Leaf" | -"insert x (B l a r) = +fun ins :: "'a::cmp \ 'a rbt \ 'a rbt" where +"ins x Leaf = R Leaf x Leaf" | +"ins x (B l a r) = (case cmp x a of - LT \ bal (insert x l) a r | - GT \ bal l a (insert x r) | + LT \ bal (ins x l) a r | + GT \ bal l a (ins x r) | EQ \ B l a r)" | -"insert x (R l a r) = +"ins x (R l a r) = (case cmp x a of - LT \ R (insert x l) a r | - GT \ R l a (insert x r) | + LT \ R (ins x l) a r | + GT \ R l a (ins x r) | EQ \ R l a r)" -fun delete :: "'a::cmp \ 'a rbt \ 'a rbt" -and deleteL :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" -and deleteR :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" +definition insert :: "'a::cmp \ 'a rbt \ 'a rbt" where +"insert x t = paint Black (ins x t)" + +fun del :: "'a::cmp \ 'a rbt \ 'a rbt" +and delL :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" +and delR :: "'a::cmp \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" where -"delete x Leaf = Leaf" | -"delete x (Node _ l a r) = +"del x Leaf = Leaf" | +"del x (Node _ l a r) = (case cmp x a of - LT \ deleteL x l a r | - GT \ deleteR x l a r | + LT \ delL x l a r | + GT \ delR x l a r | EQ \ combine l r)" | -"deleteL x (B t1 a t2) b t3 = balL (delete x (B t1 a t2)) b t3" | -"deleteL x l a r = R (delete x l) a r" | -"deleteR x t1 a (B t2 b t3) = balR t1 a (delete x (B t2 b t3))" | -"deleteR x l a r = R l a (delete x r)" +"delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" | +"delL x l a r = R (del x l) a r" | +"delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | +"delR x l a r = R l a (del x r)" + +definition delete :: "'a::cmp \ 'a rbt \ 'a rbt" where +"delete x t = paint Black (del x t)" subsection "Functional Correctness Proofs" +lemma inorder_paint: "inorder(paint c t) = inorder t" +by(induction t) (auto) + lemma inorder_bal: "inorder(bal l a r) = inorder l @ a # inorder r" by(induction l a r rule: bal.induct) (auto) +lemma inorder_ins: + "sorted(inorder t) \ inorder(ins x t) = ins_list x (inorder t)" +by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal) + lemma inorder_insert: - "sorted(inorder t) \ inorder(insert a t) = ins_list a (inorder t)" -by(induction a t rule: insert.induct) (auto simp: ins_list_simps inorder_bal) - -lemma inorder_red: "inorder(red t) = inorder t" -by(induction t) (auto) + "sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" +by (simp add: insert_def inorder_ins inorder_paint) lemma inorder_balL: "inorder(balL l a r) = inorder l @ a # inorder r" -by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_red) +by(induction l a r rule: balL.induct)(auto simp: inorder_bal inorder_paint) lemma inorder_balR: "inorder(balR l a r) = inorder l @ a # inorder r" -by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_red) +by(induction l a r rule: balR.induct) (auto simp: inorder_bal inorder_paint) lemma inorder_combine: "inorder(combine l r) = inorder l @ inorder r" by(induction l r rule: combine.induct) (auto simp: inorder_balL inorder_balR split: tree.split color.split) -lemma inorder_delete: - "sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" - "sorted(inorder l) \ inorder(deleteL x l a r) = +lemma inorder_del: + "sorted(inorder t) \ inorder(del x t) = del_list x (inorder t)" + "sorted(inorder l) \ inorder(delL x l a r) = del_list x (inorder l) @ a # inorder r" - "sorted(inorder r) \ inorder(deleteR x l a r) = + "sorted(inorder r) \ inorder(delR x l a r) = inorder l @ a # del_list x (inorder r)" -by(induction x t and x l a r and x l a r rule: delete_deleteL_deleteR.induct) +by(induction x t and x l a r and x l a r rule: del_delL_delR.induct) (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR) +lemma inorder_delete: + "sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" +by (auto simp: delete_def inorder_del inorder_paint) + interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert and delete = delete @@ -84,7 +98,7 @@ next case 3 thus ?case by(simp add: inorder_insert) next - case 4 thus ?case by(simp add: inorder_delete(1)) -qed (rule TrueI)+ + case 4 thus ?case by(simp add: inorder_delete) +qed auto end