# HG changeset patch # User nipkow # Date 1497461952 -7200 # Node ID 6e0c330f4051e13f2229261d307df657d7212440 # Parent 3f7067ba5df35931ba80b0a3733706ce43999dae simplified delete/proof diff -r 3f7067ba5df3 -r 6e0c330f4051 src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Tue Jun 13 22:39:57 2017 +0200 +++ b/src/HOL/Data_Structures/RBT_Set.thy Wed Jun 14 19:39:12 2017 +0200 @@ -26,20 +26,19 @@ definition insert :: "'a::linorder \ 'a rbt \ 'a rbt" where "insert x t = paint Black (ins x t)" -fun del :: "'a::linorder \ 'a rbt \ 'a rbt" -and delL :: "'a::linorder \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" -and delR :: "'a::linorder \ 'a rbt \ 'a \ 'a rbt \ 'a rbt" -where +fun color :: "'a rbt \ color" where +"color Leaf = Black" | +"color (Node c _ _ _) = c" + +fun del :: "'a::linorder \ 'a rbt \ 'a rbt" where "del x Leaf = Leaf" | "del x (Node _ l a r) = (case cmp x a of - LT \ delL x l a r | - GT \ delR x l a r | - EQ \ combine l r)" | -"delL x (B t1 a t2) b t3 = baldL (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) = baldR t1 a (del x (B t2 b t3))" | -"delR x l a r = R l a (del x r)" + LT \ if l \ Leaf \ color l = Black + then baldL (del x l) a r else R (del x l) a r | + GT \ if r \ Leaf\ color r = Black + then baldR l a (del x r) else R l a (del x r) | + EQ \ combine l r)" definition delete :: "'a::linorder \ 'a rbt \ 'a rbt" where "delete x t = paint Black (del x t)" @@ -84,11 +83,7 @@ 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(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: del_delL_delR.induct) +by(induction x t rule: del.induct) (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR) lemma inorder_delete: @@ -100,10 +95,6 @@ text\The proofs are due to Markus Reiter and Alexander Krauss.\ -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 bheight l + 1 else bheight l)" @@ -181,7 +172,7 @@ (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR) theorem rbt_insert: "rbt t \ rbt (insert x t)" -by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint +by (simp add: invc_ins(2) invh_ins(1) color_paint_Black invc_paint_Black invh_paint rbt_def insert_def) @@ -191,30 +182,26 @@ "color t = Black \ bheight (paint Red t) = bheight t - 1" by (cases t) auto -lemma baldL_invh_with_invc: - assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r" - shows "bheight (baldL l a r) = bheight l + 1" "invh (baldL l a r)" -using assms +lemma invh_baldL_invc: + "\ invh l; invh r; bheight l + 1 = bheight r; invc r \ + \ invh (baldL l a r) \ bheight (baldL l a r) = bheight l + 1" by (induct l a r rule: baldL.induct) (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red) -lemma baldL_invh_app: - assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black" - shows "invh (baldL l a r)" - "bheight (baldL l a r) = bheight r" -using assms +lemma invh_baldL_Black: + "\ invh l; invh r; bheight l + 1 = bheight r; color r = Black \ + \ invh (baldL l a r) \ bheight (baldL l a r) = bheight r" by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) -lemma baldL_invc: "\invc2 l; invc r; color r = Black\ \ invc (baldL l a r)" +lemma invc_baldL: "\invc2 l; invc r; color r = Black\ \ invc (baldL l a r)" by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR) -lemma baldL_invc2: "\ invc2 l; invc r \ \ invc2 (baldL l a r)" +lemma invc2_baldL: "\ invc2 l; invc r \ \ invc2 (baldL l a r)" by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I) -lemma baldR_invh_with_invc: - assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l" - shows "invh (baldR l a r) \ bheight (baldR l a r) = bheight l" -using assms +lemma invh_baldR_invc: + "\ invh l; invh r; bheight l = bheight r + 1; invc l \ + \ invh (baldR l a r) \ bheight (baldR l a r) = bheight l" by(induct l a r rule: baldR.induct) (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red) @@ -225,11 +212,10 @@ by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I) lemma invh_combine: - assumes "invh l" "invh r" "bheight l = bheight r" - shows "bheight (combine l r) = bheight l" "invh (combine l r)" -using assms + "\ invh l; invh r; bheight l = bheight r \ + \ invh (combine l r) \ bheight (combine l r) = bheight l" by (induct l r rule: combine.induct) - (auto simp: baldL_invh_app split: tree.splits color.splits) + (auto simp: invh_baldL_Black split: tree.splits color.splits) lemma invc_combine: assumes "invc l" "invc r" @@ -237,27 +223,16 @@ "invc2 (combine l r)" using assms by (induct l r rule: combine.induct) - (auto simp: baldL_invc invc2I split: tree.splits color.splits) - + (auto simp: invc_baldL invc2I split: tree.splits color.splits) -lemma assumes "invh l" "invc l" - shows del_invc_invh: - "invh (del x l) \ +lemma neq_LeafD: "t \ Leaf \ \c l x r. t = Node c l x r" +by(cases t) auto + +lemma del_invc_invh: "invh l \ invc l \ invh (del x l) \ (color l = Red \ bheight (del x l) = bheight l \ invc (del x l) \ color l = Black \ bheight (del x l) = bheight l - 1 \ invc2 (del x l))" -and "\invh r; bheight l = bheight r; invc r\ \ - invh (delL x l k r) \ - bheight (delL x l k r) = bheight l \ - (color l = Black \ color r = Black \ invc (delL x l k r) \ - (color l \ Black \ color r \ Black) \ invc2 (delL x l k r))" - and "\invh r; bheight l = bheight r; invc r\ \ - invh (delR x l k r) \ - bheight (delR x l k r) = bheight l \ - (color l = Black \ color r = Black \ invc (delR x l k r) \ - (color l \ Black \ color r \ Black) \ invc2 (delR x l k r))" -using assms -proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct) -case (2 y c _ y') +proof (induct x l rule: del.induct) +case (2 y c _ y' W) have "y = y' \ y < y' \ y > y'" by auto thus ?case proof (elim disjE) assume "y = y'" @@ -265,19 +240,15 @@ by (cases c) (simp_all add: invh_combine invc_combine) next assume "y < y'" - with 2 show ?thesis by (cases c) (auto simp: invc2I) + with 2 show ?thesis + by(cases c) + (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD) next assume "y' < y" - with 2 show ?thesis by (cases c) (auto simp: invc2I) + with 2 show ?thesis + by(cases c) + (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD) qed -next - case (3 y l z ra y' bb) - thus ?case by (cases "color (Node Black l z ra) = Black \ color bb = Black") (simp add: baldL_invh_with_invc baldL_invc baldL_invc2)+ -next - case (5 y a y' l z ra) - thus ?case by (cases "color a = Black \ color (Node Black l z ra) = Black") (simp add: baldR_invh_with_invc invc_baldR invc2_baldR)+ -next - case ("6_1" y a y') thus ?case by (cases "color a = Black \ color Leaf = Black") simp+ qed auto theorem rbt_delete: "rbt t \ rbt (delete k t)"