20 EQ \<Rightarrow> R l (x,y) r)" |
20 EQ \<Rightarrow> R l (x,y) r)" |
21 |
21 |
22 definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
22 definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
23 "update x y t = paint Black (upd x y t)" |
23 "update x y t = paint Black (upd x y t)" |
24 |
24 |
25 fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
25 fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" where |
26 and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
|
27 and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" |
|
28 where |
|
29 "del x Leaf = Leaf" | |
26 "del x Leaf = Leaf" | |
30 "del x (Node t1 (a,b) c t2) = (case cmp x a of |
27 "del x (Node l (a,b) c r) = (case cmp x a of |
31 LT \<Rightarrow> delL x t1 (a,b) t2 | |
28 LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black |
32 GT \<Rightarrow> delR x t1 (a,b) t2 | |
29 then baldL (del x l) (a,b) r else R (del x l) (a,b) r | |
33 EQ \<Rightarrow> combine t1 t2)" | |
30 GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black |
34 "delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" | |
31 then baldR l (a,b) (del x r) else R l (a,b) (del x r) | |
35 "delL x t1 a t2 = R (del x t1) a t2" | |
32 EQ \<Rightarrow> combine l r)" |
36 "delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" | |
|
37 "delR x t1 a t2 = R t1 a (del x t2)" |
|
38 |
33 |
39 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
34 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where |
40 "delete x t = paint Black (del x t)" |
35 "delete x t = paint Black (del x t)" |
41 |
36 |
42 |
37 |
50 lemma inorder_update: |
45 lemma inorder_update: |
51 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
46 "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
52 by(simp add: update_def inorder_upd inorder_paint) |
47 by(simp add: update_def inorder_upd inorder_paint) |
53 |
48 |
54 lemma inorder_del: |
49 lemma inorder_del: |
55 "sorted1(inorder t1) \<Longrightarrow> inorder(del x t1) = del_list x (inorder t1)" and |
50 "sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)" |
56 "sorted1(inorder t1) \<Longrightarrow> inorder(delL x t1 a t2) = |
51 by(induction x t rule: del.induct) |
57 del_list x (inorder t1) @ a # inorder t2" and |
|
58 "sorted1(inorder t2) \<Longrightarrow> inorder(delR x t1 a t2) = |
|
59 inorder t1 @ a # del_list x (inorder t2)" |
|
60 by(induction x t1 and x t1 a t2 and x t1 a t2 rule: del_delL_delR.induct) |
|
61 (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) |
52 (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) |
62 |
53 |
63 lemma inorder_delete: |
54 lemma inorder_delete: |
64 "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
55 "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
65 by(simp add: delete_def inorder_del inorder_paint) |
56 by(simp add: delete_def inorder_del inorder_paint) |
66 |
57 |
|
58 |
|
59 subsection \<open>Structural invariants\<close> |
|
60 |
|
61 subsubsection \<open>Update\<close> |
|
62 |
|
63 lemma invc_upd: assumes "invc t" |
|
64 shows "color t = Black \<Longrightarrow> invc (upd x y t)" "invc2 (upd x y t)" |
|
65 using assms |
|
66 by (induct x y t rule: upd.induct) (auto simp: invc_baliL invc_baliR invc2I) |
|
67 |
|
68 lemma invh_upd: assumes "invh t" |
|
69 shows "invh (upd x y t)" "bheight (upd x y t) = bheight t" |
|
70 using assms |
|
71 by(induct x y t rule: upd.induct) |
|
72 (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR) |
|
73 |
|
74 theorem rbt_update: "rbt t \<Longrightarrow> rbt (update x y t)" |
|
75 by (simp add: invc_upd(2) invh_upd(1) color_paint_Black invc_paint_Black invh_paint |
|
76 rbt_def update_def) |
|
77 |
|
78 |
|
79 subsubsection \<open>Deletion\<close> |
|
80 |
|
81 lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and> |
|
82 (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or> |
|
83 color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))" |
|
84 proof (induct x t rule: del.induct) |
|
85 case (2 x _ y _ c) |
|
86 have "x = y \<or> x < y \<or> x > y" by auto |
|
87 thus ?case proof (elim disjE) |
|
88 assume "x = y" |
|
89 with 2 show ?thesis |
|
90 by (cases c) (simp_all add: invh_combine invc_combine) |
|
91 next |
|
92 assume "x < y" |
|
93 with 2 show ?thesis |
|
94 by(cases c) |
|
95 (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD) |
|
96 next |
|
97 assume "y < x" |
|
98 with 2 show ?thesis |
|
99 by(cases c) |
|
100 (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD) |
|
101 qed |
|
102 qed auto |
|
103 |
|
104 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)" |
|
105 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint) |
|
106 |
67 interpretation Map_by_Ordered |
107 interpretation Map_by_Ordered |
68 where empty = Leaf and lookup = lookup and update = update and delete = delete |
108 where empty = Leaf and lookup = lookup and update = update and delete = delete |
69 and inorder = inorder and inv = "\<lambda>_. True" |
109 and inorder = inorder and inv = rbt |
70 proof (standard, goal_cases) |
110 proof (standard, goal_cases) |
71 case 1 show ?case by simp |
111 case 1 show ?case by simp |
72 next |
112 next |
73 case 2 thus ?case by(simp add: lookup_map_of) |
113 case 2 thus ?case by(simp add: lookup_map_of) |
74 next |
114 next |
75 case 3 thus ?case by(simp add: inorder_update) |
115 case 3 thus ?case by(simp add: inorder_update) |
76 next |
116 next |
77 case 4 thus ?case by(simp add: inorder_delete) |
117 case 4 thus ?case by(simp add: inorder_delete) |
78 qed auto |
118 next |
|
119 case 5 thus ?case by (simp add: rbt_Leaf) |
|
120 next |
|
121 case 6 thus ?case by (simp add: rbt_update) |
|
122 next |
|
123 case 7 thus ?case by (simp add: rbt_delete) |
|
124 qed |
79 |
125 |
80 end |
126 end |