# HG changeset patch # User wenzelm # Date 1612191787 -3600 # Node ID 6974bca47856ff64581b244ab710592ab4949ebd # Parent bb35f7f60d6ce596a6e3249d8627d9b91f820251# Parent feaf43e23b3ab90d237f28dea59af71a7e68b746 merged diff -r feaf43e23b3a -r 6974bca47856 Admin/PLATFORMS --- a/Admin/PLATFORMS Mon Feb 01 14:01:01 2021 +0100 +++ b/Admin/PLATFORMS Mon Feb 01 16:03:07 2021 +0100 @@ -38,7 +38,7 @@ x86_64-darwin macOS 10.13 High Sierra (lapbroy68 MacBookPro11,2) macOS 10.14 Mojave (mini2 Macmini8,1) macOS 10.15 Catalina (laramac01 Macmini8,1) - macOS 11.1 Big Sur + macOS 11.1 Big Sur (mini1 Macmini8,1) x86_64-windows Windows 10 x86_64-cygwin Cygwin 3.1.x https://isabelle.sketis.net/cygwin_2021 (x86_64/release) diff -r feaf43e23b3a -r 6974bca47856 CONTRIBUTORS --- a/CONTRIBUTORS Mon Feb 01 14:01:01 2021 +0100 +++ b/CONTRIBUTORS Mon Feb 01 16:03:07 2021 +0100 @@ -3,6 +3,15 @@ listed as an author in one of the source files of this Isabelle distribution. +Contributions to this Isabelle version +-------------------------------------- + +* January 2021: Jakub Kądziołka + Some lemmas for HOL-Computational_Algebra. + +* January 2021: Martin Rasyzk + Fast set operations for red-black trees. + Contributions to Isabelle2021 ----------------------------- diff -r feaf43e23b3a -r 6974bca47856 src/HOL/Computational_Algebra/Factorial_Ring.thy --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Feb 01 14:01:01 2021 +0100 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Feb 01 16:03:07 2021 +0100 @@ -898,6 +898,26 @@ ultimately show ?thesis by (rule finite_subset) qed +lemma infinite_unit_divisor_powers: + assumes "y \ 0" + assumes "is_unit x" + shows "infinite {n. x^n dvd y}" +proof - + from `is_unit x` have "is_unit (x^n)" for n + using is_unit_power_iff by auto + hence "x^n dvd y" for n + by auto + hence "{n. x^n dvd y} = UNIV" + by auto + thus ?thesis + by auto +qed + +corollary is_unit_iff_infinite_divisor_powers: + assumes "y \ 0" + shows "is_unit x \ infinite {n. x^n dvd y}" + using infinite_unit_divisor_powers finite_divisor_powers assms by auto + lemma prime_elem_iff_irreducible: "prime_elem x \ irreducible x" by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible) @@ -1606,8 +1626,8 @@ thus ?thesis by simp qed -lemma multiplicity_zero_1 [simp]: "multiplicity 0 x = 0" - by (metis (mono_tags) local.dvd_0_left multiplicity_zero not_dvd_imp_multiplicity_0) +lemma multiplicity_zero_left [simp]: "multiplicity 0 x = 0" + by (cases "x = 0") (auto intro: not_dvd_imp_multiplicity_0) lemma inj_on_Prod_primes: assumes "\P p. P \ A \ p \ P \ prime p" @@ -2129,6 +2149,91 @@ with assms show False by auto qed +text \Now a string of results due to Jakub Kądziołka\ + +lemma multiplicity_dvd_iff_dvd: + assumes "x \ 0" + shows "p^k dvd x \ p^k dvd p^multiplicity p x" +proof (cases "is_unit p") + case True + then have "is_unit (p^k)" + using is_unit_power_iff by simp + hence "p^k dvd x" + by auto + moreover from `is_unit p` have "p^k dvd p^multiplicity p x" + using multiplicity_unit_left is_unit_power_iff by simp + ultimately show ?thesis by simp +next + case False + show ?thesis + proof (cases "p = 0") + case True + then have "p^multiplicity p x = 1" + by simp + moreover have "p^k dvd x \ k = 0" + proof (rule ccontr) + assume "p^k dvd x" and "k \ 0" + with `p = 0` have "p^k = 0" by auto + with `p^k dvd x` have "0 dvd x" by auto + hence "x = 0" by auto + with `x \ 0` show False by auto + qed + ultimately show ?thesis + by (auto simp add: is_unit_power_iff `\ is_unit p`) + next + case False + with `x \ 0` `\ is_unit p` show ?thesis + by (simp add: power_dvd_iff_le_multiplicity dvd_power_iff multiplicity_same_power) + qed +qed + +lemma multiplicity_decomposeI: + assumes "x = p^k * x'" and "\ p dvd x'" and "p \ 0" + shows "multiplicity p x = k" + using assms local.multiplicity_eqI local.power_Suc2 by force + +lemma multiplicity_sum_lt: + assumes "multiplicity p a < multiplicity p b" "a \ 0" "b \ 0" + shows "multiplicity p (a + b) = multiplicity p a" +proof - + let ?vp = "multiplicity p" + have unit: "\ is_unit p" + proof + assume "is_unit p" + then have "?vp a = 0" and "?vp b = 0" using multiplicity_unit_left by auto + with assms show False by auto + qed + + from multiplicity_decompose' obtain a' where a': "a = p^?vp a * a'" "\ p dvd a'" + using unit assms by metis + from multiplicity_decompose' obtain b' where b': "b = p^?vp b * b'" + using unit assms by metis + + show "?vp (a + b) = ?vp a" + proof (rule multiplicity_decomposeI) + let ?k = "?vp b - ?vp a" + from assms have k: "?k > 0" by simp + with b' have "b = p^?vp a * p^?k * b'" + by (simp flip: power_add) + with a' show *: "a + b = p^?vp a * (a' + p^?k * b')" + by (simp add: ac_simps distrib_left) + moreover show "\ p dvd a' + p^?k * b'" + using a' k dvd_add_left_iff by auto + show "p \ 0" using assms by auto + qed +qed + +corollary multiplicity_sum_min: + assumes "multiplicity p a \ multiplicity p b" "a \ 0" "b \ 0" + shows "multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)" +proof - + let ?vp = "multiplicity p" + from assms have "?vp a < ?vp b \ ?vp a > ?vp b" + by auto + then show ?thesis + by (metis assms multiplicity_sum_lt min.commute add_commute min.strict_order_iff) +qed + end end diff -r feaf43e23b3a -r 6974bca47856 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Mon Feb 01 14:01:01 2021 +0100 +++ b/src/HOL/Equiv_Relations.thy Mon Feb 01 16:03:07 2021 +0100 @@ -355,6 +355,50 @@ by (simp add: quotient_def card_UN_disjoint) qed +text \By Jakub Kądziołka:\ + +lemma sum_fun_comp: + assumes "finite S" "finite R" "g ` S \ R" + shows "(\x \ S. f (g x)) = (\y \ R. of_nat (card {x \ S. g x = y}) * f y)" +proof - + let ?r = "relation_of (\p q. g p = g q) S" + have eqv: "equiv S ?r" + unfolding relation_of_def by (auto intro: comp_equivI) + have finite: "C \ S//?r \ finite C" for C + by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]]) + have disjoint: "A \ S//?r \ B \ S//?r \ A \ B \ A \ B = {}" for A B + using eqv quotient_disj by blast + + let ?cls = "\y. {x \ S. y = g x}" + have quot_as_img: "S//?r = ?cls ` g ` S" + by (auto simp add: relation_of_def quotient_def) + have cls_inj: "inj_on ?cls (g ` S)" + by (auto intro: inj_onI) + + have rest_0: "(\y \ R - g ` S. of_nat (card (?cls y)) * f y) = 0" + proof - + have "of_nat (card (?cls y)) * f y = 0" if asm: "y \ R - g ` S" for y + proof - + from asm have *: "?cls y = {}" by auto + show ?thesis unfolding * by simp + qed + thus ?thesis by simp + qed + + have "(\x \ S. f (g x)) = (\C \ S//?r. \x \ C. f (g x))" + using eqv finite disjoint + by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient) + also have "... = (\y \ g ` S. \x \ ?cls y. f (g x))" + unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj]) + also have "... = (\y \ g ` S. \x \ ?cls y. f y)" + by auto + also have "... = (\y \ g ` S. of_nat (card (?cls y)) * f y)" + by (simp flip: sum_constant) + also have "... = (\y \ R. of_nat (card (?cls y)) * f y)" + using rest_0 by (simp add: sum.subset_diff[OF \g ` S \ R\ \finite R\]) + finally show ?thesis + by (simp add: eq_commute) +qed subsection \Projection\ diff -r feaf43e23b3a -r 6974bca47856 src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Mon Feb 01 14:01:01 2021 +0100 +++ b/src/HOL/Library/RBT_Impl.thy Mon Feb 01 16:03:07 2021 +0100 @@ -1869,35 +1869,506 @@ lemma set_map_filter: "set (List.map_filter P xs) = the ` (P ` set xs - {None})" by(auto simp add: List.map_filter_def intro: rev_image_eqI) +(* Split and Join *) + +definition is_rbt_empty :: "('a, 'b) rbt \ bool" where + "is_rbt_empty t \ (case t of RBT_Impl.Empty \ True | _ \ False)" + +lemma is_rbt_empty_prop[simp]: "is_rbt_empty t \ t = RBT_Impl.Empty" + by (auto simp: is_rbt_empty_def split: RBT_Impl.rbt.splits) + +definition small_rbt :: "('a, 'b) rbt \ bool" where + "small_rbt t \ bheight t < 4" + +definition flip_rbt :: "('a, 'b) rbt \ ('a, 'b) rbt \ bool" where + "flip_rbt t1 t2 \ bheight t2 < bheight t1" + +abbreviation (input) MR where "MR l a b r \ Branch RBT_Impl.R l a b r" +abbreviation (input) MB where "MB l a b r \ Branch RBT_Impl.B l a b r" + +fun rbt_baliL :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_baliL (MR (MR t1 a b t2) a' b' t3) a'' b'' t4 = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)" +| "rbt_baliL (MR t1 a b (MR t2 a' b' t3)) a'' b'' t4 = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)" +| "rbt_baliL t1 a b t2 = MB t1 a b t2" + +fun rbt_baliR :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_baliR t1 a b (MR t2 a' b' (MR t3 a'' b'' t4)) = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)" +| "rbt_baliR t1 a b (MR (MR t2 a' b' t3) a'' b'' t4) = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)" +| "rbt_baliR t1 a b t2 = MB t1 a b t2" + +fun rbt_baldL :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_baldL (MR t1 a b t2) a' b' t3 = MR (MB t1 a b t2) a' b' t3" +| "rbt_baldL t1 a b (MB t2 a' b' t3) = rbt_baliR t1 a b (MR t2 a' b' t3)" +| "rbt_baldL t1 a b (MR (MB t2 a' b' t3) a'' b'' t4) = + MR (MB t1 a b t2) a' b' (rbt_baliR t3 a'' b'' (paint RBT_Impl.R t4))" +| "rbt_baldL t1 a b t2 = MR t1 a b t2" + +fun rbt_baldR :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_baldR t1 a b (MR t2 a' b' t3) = MR t1 a b (MB t2 a' b' t3)" +| "rbt_baldR (MB t1 a b t2) a' b' t3 = rbt_baliL (MR t1 a b t2) a' b' t3" +| "rbt_baldR (MR t1 a b (MB t2 a' b' t3)) a'' b'' t4 = + MR (rbt_baliL (paint RBT_Impl.R t1) a b t2) a' b' (MB t3 a'' b'' t4)" +| "rbt_baldR t1 a b t2 = MR t1 a b t2" + +fun rbt_app :: "('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_app RBT_Impl.Empty t = t" +| "rbt_app t RBT_Impl.Empty = t" +| "rbt_app (MR t1 a b t2) (MR t3 a'' b'' t4) = (case rbt_app t2 t3 of + MR u2 a' b' u3 \ (MR (MR t1 a b u2) a' b' (MR u3 a'' b'' t4)) + | t23 \ MR t1 a b (MR t23 a'' b'' t4))" +| "rbt_app (MB t1 a b t2) (MB t3 a'' b'' t4) = (case rbt_app t2 t3 of + MR u2 a' b' u3 \ MR (MB t1 a b u2) a' b' (MB u3 a'' b'' t4) + | t23 \ rbt_baldL t1 a b (MB t23 a'' b'' t4))" +| "rbt_app t1 (MR t2 a b t3) = MR (rbt_app t1 t2) a b t3" +| "rbt_app (MR t1 a b t2) t3 = MR t1 a b (rbt_app t2 t3)" + +fun rbt_joinL :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_joinL l a b r = (if bheight l \ bheight r then MR l a b r + else case r of MB l' a' b' r' \ rbt_baliL (rbt_joinL l a b l') a' b' r' + | MR l' a' b' r' \ MR (rbt_joinL l a b l') a' b' r')" + +declare rbt_joinL.simps[simp del] + +fun rbt_joinR :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_joinR l a b r = (if bheight l \ bheight r then MR l a b r + else case l of MB l' a' b' r' \ rbt_baliR l' a' b' (rbt_joinR r' a b r) + | MR l' a' b' r' \ MR l' a' b' (rbt_joinR r' a b r))" + +declare rbt_joinR.simps[simp del] + +definition rbt_join :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_join l a b r = + (let bhl = bheight l; bhr = bheight r + in if bhl > bhr + then paint RBT_Impl.B (rbt_joinR l a b r) + else if bhl < bhr + then paint RBT_Impl.B (rbt_joinL l a b r) + else MB l a b r)" + +lemma size_paint[simp]: "size (paint c t) = size t" + by (cases t) auto + +lemma size_baliL[simp]: "size (rbt_baliL t1 a b t2) = Suc (size t1 + size t2)" + by (induction t1 a b t2 rule: rbt_baliL.induct) auto + +lemma size_baliR[simp]: "size (rbt_baliR t1 a b t2) = Suc (size t1 + size t2)" + by (induction t1 a b t2 rule: rbt_baliR.induct) auto + +lemma size_baldL[simp]: "size (rbt_baldL t1 a b t2) = Suc (size t1 + size t2)" + by (induction t1 a b t2 rule: rbt_baldL.induct) auto + +lemma size_baldR[simp]: "size (rbt_baldR t1 a b t2) = Suc (size t1 + size t2)" + by (induction t1 a b t2 rule: rbt_baldR.induct) auto + +lemma size_rbt_app[simp]: "size (rbt_app t1 t2) = size t1 + size t2" + by (induction t1 t2 rule: rbt_app.induct) + (auto split: RBT_Impl.rbt.splits RBT_Impl.color.splits) + +lemma size_rbt_joinL[simp]: "size (rbt_joinL t1 a b t2) = Suc (size t1 + size t2)" + by (induction t1 a b t2 rule: rbt_joinL.induct) + (auto simp: rbt_joinL.simps split: RBT_Impl.rbt.splits RBT_Impl.color.splits) + +lemma size_rbt_joinR[simp]: "size (rbt_joinR t1 a b t2) = Suc (size t1 + size t2)" + by (induction t1 a b t2 rule: rbt_joinR.induct) + (auto simp: rbt_joinR.simps split: RBT_Impl.rbt.splits RBT_Impl.color.splits) + +lemma size_rbt_join[simp]: "size (rbt_join t1 a b t2) = Suc (size t1 + size t2)" + by (auto simp: rbt_join_def Let_def) + +definition "inv_12 t \ inv1 t \ inv2 t" + +lemma rbt_Node: "inv_12 (RBT_Impl.Branch c l a b r) \ inv_12 l \ inv_12 r" + by (auto simp: inv_12_def) + +lemma paint2: "paint c2 (paint c1 t) = paint c2 t" + by (cases t) auto + +lemma inv1_rbt_baliL: "inv1l l \ inv1 r \ inv1 (rbt_baliL l a b r)" + by (induct l a b r rule: rbt_baliL.induct) auto + +lemma inv1_rbt_baliR: "inv1 l \ inv1l r \ inv1 (rbt_baliR l a b r)" + by (induct l a b r rule: rbt_baliR.induct) auto + +lemma rbt_bheight_rbt_baliL: "bheight l = bheight r \ bheight (rbt_baliL l a b r) = Suc (bheight l)" + by (induct l a b r rule: rbt_baliL.induct) auto + +lemma rbt_bheight_rbt_baliR: "bheight l = bheight r \ bheight (rbt_baliR l a b r) = Suc (bheight l)" + by (induct l a b r rule: rbt_baliR.induct) auto + +lemma inv2_rbt_baliL: "inv2 l \ inv2 r \ bheight l = bheight r \ inv2 (rbt_baliL l a b r)" + by (induct l a b r rule: rbt_baliL.induct) auto + +lemma inv2_rbt_baliR: "inv2 l \ inv2 r \ bheight l = bheight r \ inv2 (rbt_baliR l a b r)" + by (induct l a b r rule: rbt_baliR.induct) auto + +lemma inv_rbt_baliR: "inv2 l \ inv2 r \ inv1 l \ inv1l r \ bheight l = bheight r \ + inv1 (rbt_baliR l a b r) \ inv2 (rbt_baliR l a b r) \ bheight (rbt_baliR l a b r) = Suc (bheight l)" + by (induct l a b r rule: rbt_baliR.induct) auto + +lemma inv_rbt_baliL: "inv2 l \ inv2 r \ inv1l l \ inv1 r \ bheight l = bheight r \ + inv1 (rbt_baliL l a b r) \ inv2 (rbt_baliL l a b r) \ bheight (rbt_baliL l a b r) = Suc (bheight l)" + by (induct l a b r rule: rbt_baliL.induct) auto + +lemma inv2_rbt_baldL_inv1: "inv2 l \ inv2 r \ bheight l + 1 = bheight r \ inv1 r \ + inv2 (rbt_baldL l a b r) \ bheight (rbt_baldL l a b r) = bheight r" + by (induct l a b r rule: rbt_baldL.induct) (auto simp: inv2_rbt_baliR rbt_bheight_rbt_baliR) + +lemma inv2_rbt_baldL_B: "inv2 l \ inv2 r \ bheight l + 1 = bheight r \ color_of r = RBT_Impl.B \ + inv2 (rbt_baldL l a b r) \ bheight (rbt_baldL l a b r) = bheight r" + by (induct l a b r rule: rbt_baldL.induct) (auto simp add: inv2_rbt_baliR rbt_bheight_rbt_baliR) + +lemma inv1_rbt_baldL: "inv1l l \ inv1 r \ color_of r = RBT_Impl.B \ inv1 (rbt_baldL l a b r)" + by (induct l a b r rule: rbt_baldL.induct) (simp_all add: inv1_rbt_baliR) + +lemma inv1lI: "inv1 t \ inv1l t" + by (cases t) auto + +lemma neq_Black[simp]: "(c \ RBT_Impl.B) = (c = RBT_Impl.R)" + by (cases c) auto + +lemma inv1l_rbt_baldL: "inv1l l \ inv1 r \ inv1l (rbt_baldL l a b r)" + by (induct l a b r rule: rbt_baldL.induct) (auto simp: inv1_rbt_baliR paint2) + +lemma inv2_rbt_baldR_inv1: "inv2 l \ inv2 r \ bheight l = bheight r + 1 \ inv1 l \ + inv2 (rbt_baldR l a b r) \ bheight (rbt_baldR l a b r) = bheight l" + by (induct l a b r rule: rbt_baldR.induct) (auto simp: inv2_rbt_baliL rbt_bheight_rbt_baliL) + +lemma inv1_rbt_baldR: "inv1 l \ inv1l r \ color_of l = RBT_Impl.B \ inv1 (rbt_baldR l a b r)" + by (induct l a b r rule: rbt_baldR.induct) (simp_all add: inv1_rbt_baliL) + +lemma inv1l_rbt_baldR: "inv1 l \ inv1l r \inv1l (rbt_baldR l a b r)" + by (induct l a b r rule: rbt_baldR.induct) (auto simp: inv1_rbt_baliL paint2) + +lemma inv2_rbt_app: "inv2 l \ inv2 r \ bheight l = bheight r \ + inv2 (rbt_app l r) \ bheight (rbt_app l r) = bheight l" + by (induct l r rule: rbt_app.induct) + (auto simp: inv2_rbt_baldL_B split: RBT_Impl.rbt.splits RBT_Impl.color.splits) + +lemma inv1_rbt_app: "inv1 l \ inv1 r \ (color_of l = RBT_Impl.B \ + color_of r = RBT_Impl.B \ inv1 (rbt_app l r)) \ inv1l (rbt_app l r)" + by (induct l r rule: rbt_app.induct) + (auto simp: inv1_rbt_baldL split: RBT_Impl.rbt.splits RBT_Impl.color.splits) + +lemma inv_rbt_baldL: "inv2 l \ inv2 r \ bheight l + 1 = bheight r \ inv1l l \ inv1 r \ + inv2 (rbt_baldL l a b r) \ bheight (rbt_baldL l a b r) = bheight r \ + inv1l (rbt_baldL l a b r) \ (color_of r = RBT_Impl.B \ inv1 (rbt_baldL l a b r))" + by (induct l a b r rule: rbt_baldL.induct) (auto simp: inv_rbt_baliR rbt_bheight_rbt_baliR paint2) + +lemma inv_rbt_baldR: "inv2 l \ inv2 r \ bheight l = bheight r + 1 \ inv1 l \ inv1l r \ + inv2 (rbt_baldR l a b r) \ bheight (rbt_baldR l a b r) = bheight l \ + inv1l (rbt_baldR l a b r) \ (color_of l = RBT_Impl.B \ inv1 (rbt_baldR l a b r))" + by (induct l a b r rule: rbt_baldR.induct) (auto simp: inv_rbt_baliL rbt_bheight_rbt_baliL paint2) + +lemma inv_rbt_app: "inv2 l \ inv2 r \ bheight l = bheight r \ inv1 l \ inv1 r \ + inv2 (rbt_app l r) \ bheight (rbt_app l r) = bheight l \ + inv1l (rbt_app l r) \ (color_of l = RBT_Impl.B \ color_of r = RBT_Impl.B \ inv1 (rbt_app l r))" + by (induct l r rule: rbt_app.induct) + (auto simp: inv2_rbt_baldL_B inv_rbt_baldL split: RBT_Impl.rbt.splits RBT_Impl.color.splits) + +lemma inv1l_rbt_joinL: "inv1 l \ inv1 r \ bheight l \ bheight r \ + inv1l (rbt_joinL l a b r) \ + (bheight l \ bheight r \ color_of r = RBT_Impl.B \ inv1 (rbt_joinL l a b r))" +proof (induct l a b r rule: rbt_joinL.induct) + case (1 l a b r) + then show ?case + by (auto simp: inv1_rbt_baliL rbt_joinL.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma inv1l_rbt_joinR: "inv1 l \ inv2 l \ inv1 r \ inv2 r \ bheight l \ bheight r \ + inv1l (rbt_joinR l a b r) \ + (bheight l \ bheight r \ color_of l = RBT_Impl.B \ inv1 (rbt_joinR l a b r))" +proof (induct l a b r rule: rbt_joinR.induct) + case (1 l a b r) + then show ?case + by (fastforce simp: inv1_rbt_baliR rbt_joinR.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma bheight_rbt_joinL: "inv2 l \ inv2 r \ bheight l \ bheight r \ + bheight (rbt_joinL l a b r) = bheight r" +proof (induct l a b r rule: rbt_joinL.induct) + case (1 l a b r) + then show ?case + by (auto simp: rbt_bheight_rbt_baliL rbt_joinL.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma inv2_rbt_joinL: "inv2 l \ inv2 r \ bheight l \ bheight r \ inv2 (rbt_joinL l a b r)" +proof (induct l a b r rule: rbt_joinL.induct) + case (1 l a b r) + then show ?case + by (auto simp: inv2_rbt_baliL bheight_rbt_joinL rbt_joinL.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma bheight_rbt_joinR: "inv2 l \ inv2 r \ bheight l \ bheight r \ + bheight (rbt_joinR l a b r) = bheight l" +proof (induct l a b r rule: rbt_joinR.induct) + case (1 l a b r) + then show ?case + by (fastforce simp: rbt_bheight_rbt_baliR rbt_joinR.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma inv2_rbt_joinR: "inv2 l \ inv2 r \ bheight l \ bheight r \ inv2 (rbt_joinR l a b r)" +proof (induct l a b r rule: rbt_joinR.induct) + case (1 l a b r) + then show ?case + by (fastforce simp: inv2_rbt_baliR bheight_rbt_joinR rbt_joinR.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma keys_paint[simp]: "RBT_Impl.keys (paint c t) = RBT_Impl.keys t" + by (cases t) auto + +lemma keys_rbt_baliL: "RBT_Impl.keys (rbt_baliL l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r" + by (cases "(l,a,b,r)" rule: rbt_baliL.cases) auto + +lemma keys_rbt_baliR: "RBT_Impl.keys (rbt_baliR l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r" + by (cases "(l,a,b,r)" rule: rbt_baliR.cases) auto + +lemma keys_rbt_baldL: "RBT_Impl.keys (rbt_baldL l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r" + by (cases "(l,a,b,r)" rule: rbt_baldL.cases) (auto simp: keys_rbt_baliL keys_rbt_baliR) + +lemma keys_rbt_baldR: "RBT_Impl.keys (rbt_baldR l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r" + by (cases "(l,a,b,r)" rule: rbt_baldR.cases) (auto simp: keys_rbt_baliL keys_rbt_baliR) + +lemma keys_rbt_app: "RBT_Impl.keys (rbt_app l r) = RBT_Impl.keys l @ RBT_Impl.keys r" + by (induction l r rule: rbt_app.induct) + (auto simp: keys_rbt_baldL keys_rbt_baldR split: RBT_Impl.rbt.splits RBT_Impl.color.splits) + +lemma keys_rbt_joinL: "bheight l \ bheight r \ + RBT_Impl.keys (rbt_joinL l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r" +proof (induction l a b r rule: rbt_joinL.induct) + case (1 l a b r) + thus ?case + by (auto simp: keys_rbt_baliL rbt_joinL.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma keys_rbt_joinR: "RBT_Impl.keys (rbt_joinR l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r" +proof (induction l a b r rule: rbt_joinR.induct) + case (1 l a b r) + thus ?case + by (force simp: keys_rbt_baliR rbt_joinR.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma rbt_set_rbt_baliL: "set (RBT_Impl.keys (rbt_baliL l a b r)) = + set (RBT_Impl.keys l) \ {a} \ set (RBT_Impl.keys r)" + by (cases "(l,a,b,r)" rule: rbt_baliL.cases) auto + +lemma set_rbt_joinL: "set (RBT_Impl.keys (rbt_joinL l a b r)) = + set (RBT_Impl.keys l) \ {a} \ set (RBT_Impl.keys r)" +proof (induction l a b r rule: rbt_joinL.induct) + case (1 l a b r) + thus ?case + by (auto simp: rbt_set_rbt_baliL rbt_joinL.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma rbt_set_rbt_baliR: "set (RBT_Impl.keys (rbt_baliR l a b r)) = + set (RBT_Impl.keys l) \ {a} \ set (RBT_Impl.keys r)" + by (cases "(l,a,b,r)" rule: rbt_baliR.cases) auto + +lemma set_rbt_joinR: "set (RBT_Impl.keys (rbt_joinR l a b r)) = + set (RBT_Impl.keys l) \ {a} \ set (RBT_Impl.keys r)" +proof (induction l a b r rule: rbt_joinR.induct) + case (1 l a b r) + thus ?case + by (force simp: rbt_set_rbt_baliR rbt_joinR.simps[of l a b r] + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma set_keys_paint: "set (RBT_Impl.keys (paint c t)) = set (RBT_Impl.keys t)" + by (cases t) auto + +lemma set_rbt_join: "set (RBT_Impl.keys (rbt_join l a b r)) = + set (RBT_Impl.keys l) \ {a} \ set (RBT_Impl.keys r)" + by (simp add: set_rbt_joinL set_rbt_joinR set_keys_paint rbt_join_def Let_def) + +lemma inv_rbt_join: "inv_12 l \ inv_12 r \ inv_12 (rbt_join l a b r)" + by (auto simp: rbt_join_def Let_def inv1l_rbt_joinL inv1l_rbt_joinR + inv2_rbt_joinL inv2_rbt_joinR inv_12_def) + +fun rbt_recolor :: "('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_recolor (Branch RBT_Impl.R t1 k v t2) = + (if color_of t1 = RBT_Impl.B \ color_of t2 = RBT_Impl.B then Branch RBT_Impl.B t1 k v t2 + else Branch RBT_Impl.R t1 k v t2)" +| "rbt_recolor t = t" + +lemma rbt_recolor: "inv_12 t \ inv_12 (rbt_recolor t)" + by (induction t rule: rbt_recolor.induct) (auto simp: inv_12_def) + +fun rbt_split_min :: "('a, 'b) rbt \ 'a \ 'b \ ('a, 'b) rbt" where + "rbt_split_min RBT_Impl.Empty = undefined" +| "rbt_split_min (RBT_Impl.Branch _ l a b r) = + (if is_rbt_empty l then (a,b,r) else let (a',b',l') = rbt_split_min l in (a',b',rbt_join l' a b r))" + +lemma rbt_split_min_set: + "rbt_split_min t = (a,b,t') \ t \ RBT_Impl.Empty \ + a \ set (RBT_Impl.keys t) \ set (RBT_Impl.keys t) = {a} \ set (RBT_Impl.keys t')" + by (induction t arbitrary: t') (auto simp: set_rbt_join split: prod.splits if_splits) + +lemma rbt_split_min_inv: "rbt_split_min t = (a,b,t') \ inv_12 t \ t \ RBT_Impl.Empty \ inv_12 t'" + by (induction t arbitrary: t') + (auto simp: inv_rbt_join split: if_splits prod.splits dest: rbt_Node) + +definition rbt_join2 :: "('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_join2 l r = (if is_rbt_empty r then l else let (a,b,r') = rbt_split_min r in rbt_join l a b r')" + +lemma set_rbt_join2[simp]: "set (RBT_Impl.keys (rbt_join2 l r)) = + set (RBT_Impl.keys l) \ set (RBT_Impl.keys r)" + by (simp add: rbt_join2_def rbt_split_min_set set_rbt_join split: prod.split) + +lemma inv_rbt_join2: "inv_12 l \ inv_12 r \ inv_12 (rbt_join2 l r)" + by (simp add: rbt_join2_def inv_rbt_join rbt_split_min_set rbt_split_min_inv split: prod.split) + context ord begin -definition rbt_union_with_key :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" -where - "rbt_union_with_key f t1 t2 = - (case RBT_Impl.compare_height t1 t1 t2 t2 - of compare.EQ \ rbtreeify (sunion_with f (entries t1) (entries t2)) - | compare.LT \ fold (rbt_insert_with_key (\k v w. f k w v)) t1 t2 - | compare.GT \ fold (rbt_insert_with_key f) t2 t1)" - -definition rbt_union_with where - "rbt_union_with f = rbt_union_with_key (\_. f)" - -definition rbt_union where - "rbt_union = rbt_union_with_key (%_ _ rv. rv)" - -definition rbt_inter_with_key :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" -where - "rbt_inter_with_key f t1 t2 = - (case RBT_Impl.compare_height t1 t1 t2 t2 - of compare.EQ \ rbtreeify (sinter_with f (entries t1) (entries t2)) - | compare.LT \ rbtreeify (List.map_filter (\(k, v). map_option (\w. (k, f k v w)) (rbt_lookup t2 k)) (entries t1)) - | compare.GT \ rbtreeify (List.map_filter (\(k, v). map_option (\w. (k, f k w v)) (rbt_lookup t1 k)) (entries t2)))" - -definition rbt_inter_with where - "rbt_inter_with f = rbt_inter_with_key (\_. f)" - -definition rbt_inter where - "rbt_inter = rbt_inter_with_key (\_ _ rv. rv)" +fun rbt_split :: "('a, 'b) rbt \ 'a \ ('a, 'b) rbt \ 'b option \ ('a, 'b) rbt" where + "rbt_split RBT_Impl.Empty k = (RBT_Impl.Empty, None, RBT_Impl.Empty)" +| "rbt_split (RBT_Impl.Branch _ l a b r) x = + (if x < a then (case rbt_split l x of (l1, \, l2) \ (l1, \, rbt_join l2 a b r)) + else if a < x then (case rbt_split r x of (r1, \, r2) \ (rbt_join l a b r1, \, r2)) + else (l, Some b, r))" + +lemma rbt_split: "rbt_split t x = (l,\,r) \ inv_12 t \ inv_12 l \ inv_12 r" + by (induction t arbitrary: l r) + (auto simp: set_rbt_join inv_rbt_join rbt_greater_prop rbt_less_prop + split: if_splits prod.splits dest!: rbt_Node) + +lemma rbt_split_size: "(l2,\,r2) = rbt_split t2 a \ size l2 + size r2 \ size t2" + by (induction t2 a arbitrary: l2 r2 rule: rbt_split.induct) (auto split: if_splits prod.splits) + +function rbt_union_rec :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_union_rec f t1 t2 = (let (f, t2, t1) = + if flip_rbt t2 t1 then (\k v v'. f k v' v, t1, t2) else (f, t2, t1) in + if small_rbt t2 then RBT_Impl.fold (rbt_insert_with_key f) t2 t1 + else (case t1 of RBT_Impl.Empty \ t2 + | RBT_Impl.Branch _ l1 a b r1 \ + case rbt_split t2 a of (l2, \, r2) \ + rbt_join (rbt_union_rec f l1 l2) a (case \ of None \ b | Some b' \ f a b b') (rbt_union_rec f r1 r2)))" + by pat_completeness auto +termination + using rbt_split_size + by (relation "measure (\(f,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+ + +declare rbt_union_rec.simps[simp del] + +function rbt_union_swap_rec :: "('a \ 'b \ 'b \ 'b) \ bool \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_union_swap_rec f \ t1 t2 = (let (\, t2, t1) = + if flip_rbt t2 t1 then (\\, t1, t2) else (\, t2, t1); + f' = (if \ then (\k v v'. f k v' v) else f) in + if small_rbt t2 then RBT_Impl.fold (rbt_insert_with_key f') t2 t1 + else (case t1 of RBT_Impl.Empty \ t2 + | RBT_Impl.Branch _ l1 a b r1 \ + case rbt_split t2 a of (l2, \, r2) \ + rbt_join (rbt_union_swap_rec f \ l1 l2) a (case \ of None \ b | Some b' \ f' a b b') (rbt_union_swap_rec f \ r1 r2)))" + by pat_completeness auto +termination + using rbt_split_size + by (relation "measure (\(f,\,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+ + +declare rbt_union_swap_rec.simps[simp del] + +lemma rbt_union_swap_rec: "rbt_union_swap_rec f \ t1 t2 = + rbt_union_rec (if \ then (\k v v'. f k v' v) else f) t1 t2" +proof (induction f \ t1 t2 rule: rbt_union_swap_rec.induct) + case (1 f \ t1 t2) + show ?case + using 1[OF refl _ refl refl _ refl _ refl] + unfolding rbt_union_swap_rec.simps[of _ _ t1] rbt_union_rec.simps[of _ t1] + by (auto simp: Let_def split: rbt.splits prod.splits option.splits) (* slow *) +qed + +lemma rbt_fold_rbt_insert: + assumes "inv_12 t2" + shows "inv_12 (RBT_Impl.fold (rbt_insert_with_key f) t1 t2)" +proof - + define xs where "xs = RBT_Impl.entries t1" + from assms show ?thesis + unfolding RBT_Impl.fold_def xs_def[symmetric] + by (induct xs rule: rev_induct) + (auto simp: inv_12_def rbt_insert_with_key_def ins_inv1_inv2) +qed + +lemma rbt_union_rec: "inv_12 t1 \ inv_12 t2 \ inv_12 (rbt_union_rec f t1 t2)" +proof (induction f t1 t2 rule: rbt_union_rec.induct) + case (1 t1 t2) + thus ?case + by (auto simp: rbt_union_rec.simps[of t1 t2] inv_rbt_join rbt_split rbt_fold_rbt_insert + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits prod.split if_splits dest: rbt_Node) +qed + +definition "map_filter_inter f t1 t2 = List.map_filter (\(k, v). + case rbt_lookup t1 k of None \ None + | Some v' \ Some (k, f k v' v)) (RBT_Impl.entries t2)" + +function rbt_inter_rec :: "('a \ 'b \ 'b \ 'b) \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_inter_rec f t1 t2 = (let (f, t2, t1) = + if flip_rbt t2 t1 then (\k v v'. f k v' v, t1, t2) else (f, t2, t1) in + if small_rbt t2 then rbtreeify (map_filter_inter f t1 t2) + else case t1 of RBT_Impl.Empty \ RBT_Impl.Empty + | RBT_Impl.Branch _ l1 a b r1 \ + case rbt_split t2 a of (l2, \, r2) \ let l' = rbt_inter_rec f l1 l2; r' = rbt_inter_rec f r1 r2 in + (case \ of None \ rbt_join2 l' r' | Some b' \