48 subsection "Functional Correctness Proofs" |
48 subsection "Functional Correctness Proofs" |
49 |
49 |
50 lemma inorder_paint: "inorder(paint c t) = inorder t" |
50 lemma inorder_paint: "inorder(paint c t) = inorder t" |
51 by(cases t) (auto) |
51 by(cases t) (auto) |
52 |
52 |
53 lemma inorder_bal: |
53 lemma inorder_baliL: |
54 "inorder(bal l a r) = inorder l @ a # inorder r" |
54 "inorder(baliL l a r) = inorder l @ a # inorder r" |
55 by(cases "(l,a,r)" rule: bal.cases) (auto) |
55 by(cases "(l,a,r)" rule: baliL.cases) (auto) |
|
56 |
|
57 lemma inorder_baliR: |
|
58 "inorder(baliR l a r) = inorder l @ a # inorder r" |
|
59 by(cases "(l,a,r)" rule: baliR.cases) (auto) |
56 |
60 |
57 lemma inorder_ins: |
61 lemma inorder_ins: |
58 "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)" |
62 "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)" |
59 by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal) |
63 by(induction x t rule: ins.induct) |
|
64 (auto simp: ins_list_simps inorder_baliL inorder_baliR) |
60 |
65 |
61 lemma inorder_insert: |
66 lemma inorder_insert: |
62 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
67 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
63 by (simp add: insert_def inorder_ins inorder_paint) |
68 by (simp add: insert_def inorder_ins inorder_paint) |
64 |
69 |
65 lemma inorder_balL: |
70 lemma inorder_baldL: |
66 "inorder(balL l a r) = inorder l @ a # inorder r" |
71 "inorder(baldL l a r) = inorder l @ a # inorder r" |
67 by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint) |
72 by(cases "(l,a,r)" rule: baldL.cases) |
68 |
73 (auto simp: inorder_baliL inorder_baliR inorder_paint) |
69 lemma inorder_balR: |
74 |
70 "inorder(balR l a r) = inorder l @ a # inorder r" |
75 lemma inorder_baldR: |
71 by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint) |
76 "inorder(baldR l a r) = inorder l @ a # inorder r" |
|
77 by(cases "(l,a,r)" rule: baldR.cases) |
|
78 (auto simp: inorder_baliL inorder_baliR inorder_paint) |
72 |
79 |
73 lemma inorder_combine: |
80 lemma inorder_combine: |
74 "inorder(combine l r) = inorder l @ inorder r" |
81 "inorder(combine l r) = inorder l @ inorder r" |
75 by(induction l r rule: combine.induct) |
82 by(induction l r rule: combine.induct) |
76 (auto simp: inorder_balL inorder_balR split: tree.split color.split) |
83 (auto simp: inorder_baldL inorder_baldR split: tree.split color.split) |
77 |
84 |
78 lemma inorder_del: |
85 lemma inorder_del: |
79 "sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)" |
86 "sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)" |
80 "sorted(inorder l) \<Longrightarrow> inorder(delL x l a r) = |
87 "sorted(inorder l) \<Longrightarrow> inorder(delL x l a r) = |
81 del_list x (inorder l) @ a # inorder r" |
88 del_list x (inorder l) @ a # inorder r" |
82 "sorted(inorder r) \<Longrightarrow> inorder(delR x l a r) = |
89 "sorted(inorder r) \<Longrightarrow> inorder(delR x l a r) = |
83 inorder l @ a # del_list x (inorder r)" |
90 inorder l @ a # del_list x (inorder r)" |
84 by(induction x t and x l a r and x l a r rule: del_delL_delR.induct) |
91 by(induction x t and x l a r and x l a r rule: del_delL_delR.induct) |
85 (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR) |
92 (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) |
86 |
93 |
87 lemma inorder_delete: |
94 lemma inorder_delete: |
88 "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
95 "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
89 by (auto simp: delete_def inorder_del inorder_paint) |
96 by (auto simp: delete_def inorder_del inorder_paint) |
90 |
97 |
133 by (cases t) auto |
140 by (cases t) auto |
134 |
141 |
135 lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)" |
142 lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)" |
136 by (cases t) auto |
143 by (cases t) auto |
137 |
144 |
138 lemma invc_bal: |
145 lemma invc_baliL: |
139 "\<lbrakk>invc l \<and> invc2 r \<or> invc2 l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)" |
146 "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" |
140 by (induct l a r rule: bal.induct) auto |
147 by (induct l a r rule: baliL.induct) auto |
141 |
148 |
142 lemma bheight_bal: |
149 lemma invc_baliR: |
143 "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)" |
150 "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" |
144 by (induct l a r rule: bal.induct) auto |
151 by (induct l a r rule: baliR.induct) auto |
145 |
152 |
146 lemma invh_bal: |
153 lemma bheight_baliL: |
147 "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)" |
154 "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)" |
148 by (induct l a r rule: bal.induct) auto |
155 by (induct l a r rule: baliL.induct) auto |
|
156 |
|
157 lemma bheight_baliR: |
|
158 "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)" |
|
159 by (induct l a r rule: baliR.induct) auto |
|
160 |
|
161 lemma invh_baliL: |
|
162 "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)" |
|
163 by (induct l a r rule: baliL.induct) auto |
|
164 |
|
165 lemma invh_baliR: |
|
166 "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)" |
|
167 by (induct l a r rule: baliR.induct) auto |
149 |
168 |
150 |
169 |
151 subsubsection \<open>Insertion\<close> |
170 subsubsection \<open>Insertion\<close> |
152 |
171 |
153 lemma invc_ins: assumes "invc t" |
172 lemma invc_ins: assumes "invc t" |
154 shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)" |
173 shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)" |
155 using assms |
174 using assms |
156 by (induct x t rule: ins.induct) (auto simp: invc_bal invc2I) |
175 by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I) |
157 |
176 |
158 lemma invh_ins: assumes "invh t" |
177 lemma invh_ins: assumes "invh t" |
159 shows "invh (ins x t)" "bheight (ins x t) = bheight t" |
178 shows "invh (ins x t)" "bheight (ins x t) = bheight t" |
160 using assms |
179 using assms |
161 by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal) |
180 by(induct x t rule: ins.induct) |
|
181 (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR) |
162 |
182 |
163 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)" |
183 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)" |
164 by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint |
184 by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint |
165 rbt_def insert_def) |
185 rbt_def insert_def) |
166 |
186 |
169 |
189 |
170 lemma bheight_paint_Red: |
190 lemma bheight_paint_Red: |
171 "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1" |
191 "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1" |
172 by (cases t) auto |
192 by (cases t) auto |
173 |
193 |
174 lemma balL_invh_with_invc: |
194 lemma baldL_invh_with_invc: |
175 assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt" |
195 assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r" |
176 shows "bheight (balL lt a rt) = bheight lt + 1" "invh (balL lt a rt)" |
196 shows "bheight (baldL l a r) = bheight l + 1" "invh (baldL l a r)" |
177 using assms |
197 using assms |
178 by (induct lt a rt rule: balL.induct) |
198 by (induct l a r rule: baldL.induct) |
179 (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red) |
199 (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red) |
180 |
200 |
181 lemma balL_invh_app: |
201 lemma baldL_invh_app: |
182 assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black" |
202 assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black" |
183 shows "invh (balL lt a rt)" |
203 shows "invh (baldL l a r)" |
184 "bheight (balL lt a rt) = bheight rt" |
204 "bheight (baldL l a r) = bheight r" |
185 using assms |
205 using assms |
186 by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) |
206 by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) |
187 |
207 |
188 lemma balL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)" |
208 lemma baldL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)" |
189 by (induct l a r rule: balL.induct) (simp_all add: invc_bal) |
209 by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR) |
190 |
210 |
191 lemma balL_invc2: "\<lbrakk> invc2 lt; invc rt \<rbrakk> \<Longrightarrow> invc2 (balL lt a rt)" |
211 lemma baldL_invc2: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)" |
192 by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc2 invc2I) |
212 by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I) |
193 |
213 |
194 lemma balR_invh_with_invc: |
214 lemma baldR_invh_with_invc: |
195 assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt" |
215 assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l" |
196 shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt" |
216 shows "invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l" |
197 using assms |
217 using assms |
198 by(induct lt a rt rule: balR.induct) |
218 by(induct l a r rule: baldR.induct) |
199 (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red) |
219 (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red) |
200 |
220 |
201 lemma invc_balR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)" |
221 lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)" |
202 by (induct a x b rule: balR.induct) (simp_all add: invc_bal) |
222 by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL) |
203 |
223 |
204 lemma invc2_balR: "\<lbrakk> invc lt; invc2 rt \<rbrakk> \<Longrightarrow>invc2 (balR lt x rt)" |
224 lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)" |
205 by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc2 invc2I) |
225 by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I) |
206 |
226 |
207 lemma invh_combine: |
227 lemma invh_combine: |
208 assumes "invh lt" "invh rt" "bheight lt = bheight rt" |
228 assumes "invh l" "invh r" "bheight l = bheight r" |
209 shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)" |
229 shows "bheight (combine l r) = bheight l" "invh (combine l r)" |
210 using assms |
230 using assms |
211 by (induct lt rt rule: combine.induct) |
231 by (induct l r rule: combine.induct) |
212 (auto simp: balL_invh_app split: tree.splits color.splits) |
232 (auto simp: baldL_invh_app split: tree.splits color.splits) |
213 |
233 |
214 lemma invc_combine: |
234 lemma invc_combine: |
215 assumes "invc lt" "invc rt" |
235 assumes "invc l" "invc r" |
216 shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)" |
236 shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)" |
217 "invc2 (combine lt rt)" |
237 "invc2 (combine l r)" |
218 using assms |
238 using assms |
219 by (induct lt rt rule: combine.induct) |
239 by (induct l r rule: combine.induct) |
220 (auto simp: balL_invc invc2I split: tree.splits color.splits) |
240 (auto simp: baldL_invc invc2I split: tree.splits color.splits) |
221 |
241 |
222 |
242 |
223 lemma assumes "invh lt" "invc lt" |
243 lemma assumes "invh l" "invc l" |
224 shows |
244 shows del_invc_invh: |
225 del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt) |
245 "invh (del x l) \<and> |
226 \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc2 (del x lt))" |
246 (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or> |
227 and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow> |
247 color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))" |
228 invh (delL x lt k rt) \<and> |
248 and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow> |
229 bheight (delL x lt k rt) = bheight lt \<and> |
249 invh (delL x l k r) \<and> |
230 (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or> |
250 bheight (delL x l k r) = bheight l \<and> |
231 (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delL x lt k rt))" |
251 (color l = Black \<and> color r = Black \<and> invc (delL x l k r) \<or> |
232 and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow> |
252 (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delL x l k r))" |
233 invh (delR x lt k rt) \<and> |
253 and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow> |
234 bheight (delR x lt k rt) = bheight lt \<and> |
254 invh (delR x l k r) \<and> |
235 (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or> |
255 bheight (delR x l k r) = bheight l \<and> |
236 (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delR x lt k rt))" |
256 (color l = Black \<and> color r = Black \<and> invc (delR x l k r) \<or> |
|
257 (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delR x l k r))" |
237 using assms |
258 using assms |
238 proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct) |
259 proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct) |
239 case (2 y c _ y') |
260 case (2 y c _ y') |
240 have "y = y' \<or> y < y' \<or> y > y'" by auto |
261 have "y = y' \<or> y < y' \<or> y > y'" by auto |
241 thus ?case proof (elim disjE) |
262 thus ?case proof (elim disjE) |
242 assume "y = y'" |
263 assume "y = y'" |
243 with 2 show ?thesis |
264 with 2 show ?thesis |