263 lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>l x c r. t = Node l (x,c) r" |
263 lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>l x c r. t = Node l (x,c) r" |
264 by(cases t rule: tree2_cases) auto |
264 by(cases t rule: tree2_cases) auto |
265 |
265 |
266 lemma inv_del: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow> |
266 lemma inv_del: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow> |
267 invh (del x t) \<and> |
267 invh (del x t) \<and> |
268 (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or> |
268 (color t = Red \<longrightarrow> bheight (del x t) = bheight t \<and> invc (del x t)) \<and> |
269 color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))" |
269 (color t = Black \<longrightarrow> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))" |
270 by(induct x t rule: del.induct) |
270 by(induct x t rule: del.induct) |
271 (auto simp: inv_baldL inv_baldR inv_join dest!: neq_LeafD) |
271 (auto simp: inv_baldL inv_baldR inv_join dest!: neq_LeafD) |
272 |
272 |
273 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)" |
273 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)" |
274 by (metis delete_def rbt_def color_paint_Black inv_del invc2I invh_paint) |
274 by (metis delete_def rbt_def color_paint_Black inv_del invh_paint) |
275 |
275 |
276 text \<open>Overall correctness:\<close> |
276 text \<open>Overall correctness:\<close> |
277 |
277 |
278 interpretation S: Set_by_Ordered |
278 interpretation S: Set_by_Ordered |
279 where empty = empty and isin = isin and insert = insert and delete = delete |
279 where empty = empty and isin = isin and insert = insert and delete = delete |