# 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' \ rbt_join l' a (f a b b') r'))" + 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_inter_rec.simps[simp del] + +function rbt_inter_swap_rec :: "('a \ 'b \ 'b \ 'b) \ bool \ ('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_inter_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 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_swap_rec f \ l1 l2; r' = rbt_inter_swap_rec f \ r1 r2 in + (case \ of None \ rbt_join2 l' r' | Some b' \ rbt_join l' a (f' a b b') r'))" + 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_inter_swap_rec.simps[simp del] + +lemma rbt_inter_swap_rec: "rbt_inter_swap_rec f \ t1 t2 = + rbt_inter_rec (if \ then (\k v v'. f k v' v) else f) t1 t2" +proof (induction f \ t1 t2 rule: rbt_inter_swap_rec.induct) + case (1 f \ t1 t2) + show ?case + using 1[OF refl _ refl refl _ refl _ refl] + unfolding rbt_inter_swap_rec.simps[of _ _ t1] rbt_inter_rec.simps[of _ t1] + by (auto simp add: Let_def split: rbt.splits prod.splits option.splits) +qed + +lemma rbt_rbtreeify[simp]: "inv_12 (rbtreeify kvs)" + by (simp add: inv_12_def rbtreeify_def inv1_rbtreeify_g inv2_rbtreeify_g) + +lemma rbt_inter_rec: "inv_12 t1 \ inv_12 t2 \ inv_12 (rbt_inter_rec f t1 t2)" +proof(induction f t1 t2 rule: rbt_inter_rec.induct) + case (1 t1 t2) + thus ?case + by (auto simp: rbt_inter_rec.simps[of t1 t2] inv_rbt_join inv_rbt_join2 rbt_split Let_def + split!: RBT_Impl.rbt.splits RBT_Impl.color.splits prod.split if_splits + option.splits dest!: rbt_Node) +qed + +definition "filter_minus t1 t2 = filter (\(k, _). rbt_lookup t2 k = None) (RBT_Impl.entries t1)" + +fun rbt_minus_rec :: "('a, 'b) rbt \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "rbt_minus_rec t1 t2 = (if small_rbt t2 then RBT_Impl.fold (\k _ t. rbt_delete k t) t2 t1 + else if small_rbt t1 then rbtreeify (filter_minus t1 t2) + else case t2 of RBT_Impl.Empty \ t1 + | RBT_Impl.Branch _ l2 a b r2 \ + case rbt_split t1 a of (l1, _, r1) \ rbt_join2 (rbt_minus_rec l1 l2) (rbt_minus_rec r1 r2))" + +declare rbt_minus_rec.simps[simp del] end @@ -1921,6 +2392,173 @@ by(induct xs rule: rev_induct)(auto simp add: rbt_insertwk_is_rbt) qed +lemma rbt_delete: "inv_12 t \ inv_12 (rbt_delete x t)" + using rbt_del_inv1_inv2[of t x] + by (auto simp: inv_12_def rbt_delete_def rbt_del_inv1_inv2) + +lemma rbt_sorted_delete: "rbt_sorted t \ rbt_sorted (rbt_delete x t)" + by (auto simp: rbt_delete_def rbt_del_rbt_sorted) + +lemma rbt_fold_rbt_delete: + assumes "inv_12 t2" + shows "inv_12 (RBT_Impl.fold (\k _ t. rbt_delete k t) 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: rbt_delete) +qed + +lemma rbt_minus_rec: "inv_12 t1 \ inv_12 t2 \ inv_12 (rbt_minus_rec t1 t2)" +proof(induction t1 t2 rule: rbt_minus_rec.induct) + case (1 t1 t2) + thus ?case + by (auto simp: rbt_minus_rec.simps[of t1 t2] inv_rbt_join inv_rbt_join2 rbt_split + rbt_fold_rbt_delete split!: RBT_Impl.rbt.splits RBT_Impl.color.splits prod.split if_splits + dest: rbt_Node) +qed + +end + +context linorder begin + +lemma rbt_sorted_rbt_baliL: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_sorted (rbt_baliL l a b r)" + using rbt_greater_trans rbt_less_trans + by (cases "(l,a,b,r)" rule: rbt_baliL.cases) fastforce+ + +lemma rbt_lookup_rbt_baliL: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_lookup (rbt_baliL l a b r) k = + (if k < a then rbt_lookup l k else if k = a then Some b else rbt_lookup r k)" + by (cases "(l,a,b,r)" rule: rbt_baliL.cases) (auto split!: if_splits) + +lemma rbt_sorted_rbt_baliR: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_sorted (rbt_baliR l a b r)" + using rbt_greater_trans rbt_less_trans + by (cases "(l,a,b,r)" rule: rbt_baliR.cases) fastforce+ + +lemma rbt_lookup_rbt_baliR: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_lookup (rbt_baliR l a b r) k = + (if k < a then rbt_lookup l k else if k = a then Some b else rbt_lookup r k)" + by (cases "(l,a,b,r)" rule: rbt_baliR.cases) (auto split!: if_splits) + +lemma rbt_sorted_rbt_joinL: "rbt_sorted (RBT_Impl.Branch c l a b r) \ bheight l \ bheight r \ + rbt_sorted (rbt_joinL l a b r)" +proof (induction l a b r arbitrary: c 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] set_rbt_joinL rbt_less_prop + intro!: rbt_sorted_rbt_baliL split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma rbt_lookup_rbt_joinL: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_lookup (rbt_joinL l a b r) k = + (if k < a then rbt_lookup l k else if k = a then Some b else rbt_lookup r k)" +proof (induction l a b r rule: rbt_joinL.induct) + case (1 l a b r) + have less_rbt_joinL: + "rbt_sorted r1 \ r1 |\ x \ a \| r1 \ a < x \ rbt_joinL l a b r1 |\ x" for x r1 + using 1(5) + by (auto simp: rbt_less_prop rbt_greater_prop set_rbt_joinL) + show ?case + using 1 less_rbt_joinL rbt_lookup_rbt_baliL[OF rbt_sorted_rbt_joinL[of _ l a b], where ?k=k] + by (auto simp: rbt_joinL.simps[of l a b r] split!: if_splits rbt.splits color.splits) +qed + +lemma rbt_sorted_rbt_joinR: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_sorted (rbt_joinR l a b r)" +proof (induction l a b r rule: rbt_joinR.induct) + case (1 l a b r) + thus ?case + by (auto simp: rbt_set_rbt_baliR rbt_joinR.simps[of l a b r] set_rbt_joinR rbt_greater_prop + intro!: rbt_sorted_rbt_baliR split!: RBT_Impl.rbt.splits RBT_Impl.color.splits) +qed + +lemma rbt_lookup_rbt_joinR: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_lookup (rbt_joinR l a b r) k = + (if k < a then rbt_lookup l k else if k = a then Some b else rbt_lookup r k)" +proof (induction l a b r rule: rbt_joinR.induct) + case (1 l a b r) + have less_rbt_joinR: + "rbt_sorted l1 \ x \| l1 \ l1 |\ a \ x < a \ x \| rbt_joinR l1 a b r" for x l1 + using 1(6) + by (auto simp: rbt_less_prop rbt_greater_prop set_rbt_joinR) + show ?case + using 1 less_rbt_joinR rbt_lookup_rbt_baliR[OF _ rbt_sorted_rbt_joinR[of _ r a b], where ?k=k] + by (auto simp: rbt_joinR.simps[of l a b r] split!: if_splits rbt.splits color.splits) +qed + +lemma rbt_sorted_paint: "rbt_sorted (paint c t) = rbt_sorted t" + by (cases t) auto + +lemma rbt_sorted_rbt_join: "rbt_sorted (RBT_Impl.Branch c l a b r) \ + rbt_sorted (rbt_join l a b r)" + by (auto simp: rbt_sorted_paint rbt_sorted_rbt_joinL rbt_sorted_rbt_joinR rbt_join_def Let_def) + +lemma rbt_lookup_rbt_join: "rbt_sorted l \ rbt_sorted r \ l |\ a \ a \| r \ + rbt_lookup (rbt_join l a b r) k = + (if k < a then rbt_lookup l k else if k = a then Some b else rbt_lookup r k)" + by (auto simp: rbt_join_def Let_def rbt_lookup_rbt_joinL rbt_lookup_rbt_joinR) + +lemma rbt_split_min_rbt_sorted: "rbt_split_min t = (a,b,t') \ rbt_sorted t \ t \ RBT_Impl.Empty \ + rbt_sorted t' \ (\x \ set (RBT_Impl.keys t'). a < x)" + by (induction t arbitrary: t') + (fastforce simp: rbt_split_min_set rbt_sorted_rbt_join set_rbt_join rbt_less_prop rbt_greater_prop + split: if_splits prod.splits)+ + +lemma rbt_split_min_rbt_lookup: "rbt_split_min t = (a,b,t') \ rbt_sorted t \ t \ RBT_Impl.Empty \ + rbt_lookup t k = (if k < a then None else if k = a then Some b else rbt_lookup t' k)" + by (induction t arbitrary: a b t') + (auto simp: rbt_less_trans antisym_conv3 rbt_less_prop rbt_split_min_set rbt_lookup_rbt_join + rbt_split_min_rbt_sorted split!: if_splits prod.splits) + +lemma rbt_sorted_rbt_join2: "rbt_sorted l \ rbt_sorted r \ + \x \ set (RBT_Impl.keys l). \y \ set (RBT_Impl.keys r). x < y \ rbt_sorted (rbt_join2 l r)" + by (simp add: rbt_join2_def rbt_sorted_rbt_join rbt_split_min_set rbt_split_min_rbt_sorted set_rbt_join + rbt_greater_prop rbt_less_prop split: prod.split) + +lemma rbt_lookup_rbt_join2: "rbt_sorted l \ rbt_sorted r \ + \x \ set (RBT_Impl.keys l). \y \ set (RBT_Impl.keys r). x < y \ + rbt_lookup (rbt_join2 l r) k = (case rbt_lookup l k of None \ rbt_lookup r k | Some v \ Some v)" + using rbt_lookup_keys + by (fastforce simp: rbt_join2_def rbt_greater_prop rbt_less_prop rbt_lookup_rbt_join + rbt_split_min_rbt_lookup rbt_split_min_rbt_sorted rbt_split_min_set split: option.splits prod.splits) + +lemma rbt_split_props: "rbt_split t x = (l,\,r) \ rbt_sorted t \ + set (RBT_Impl.keys l) = {a \ set (RBT_Impl.keys t). a < x} \ + set (RBT_Impl.keys r) = {a \ set (RBT_Impl.keys t). x < a} \ + rbt_sorted l \ rbt_sorted r" + by (induction t arbitrary: l r) + (force simp: Let_def set_rbt_join rbt_greater_prop rbt_less_prop + split: if_splits prod.splits intro!: rbt_sorted_rbt_join)+ + +lemma rbt_split_lookup: "rbt_split t x = (l,\,r) \ rbt_sorted t \ + rbt_lookup t k = (if k < x then rbt_lookup l k else if k = x then \ else rbt_lookup r k)" +proof (induction t arbitrary: x l \ r) + case (Branch c t1 a b t2) + have "rbt_sorted r1" "r1 |\ a" if "rbt_split t1 x = (l, \, r1)" for r1 + using rbt_split_props Branch(4) that + by (fastforce simp: rbt_less_prop)+ + moreover have "rbt_sorted l1" "a \| l1" if "rbt_split t2 x = (l1, \, r)" for l1 + using rbt_split_props Branch(4) that + by (fastforce simp: rbt_greater_prop)+ + ultimately show ?case + using Branch rbt_lookup_rbt_join[of t1 _ a b k] rbt_lookup_rbt_join[of _ t2 a b k] + by (auto split!: if_splits prod.splits) +qed simp + +lemma rbt_sorted_fold_insertwk: "rbt_sorted t \ + rbt_sorted (RBT_Impl.fold (rbt_insert_with_key f) t' t)" + by (induct t' arbitrary: t) + (simp_all add: rbt_insertwk_rbt_sorted) + +lemma rbt_lookup_iff_keys: + "rbt_sorted t \ set (RBT_Impl.keys t) = {k. \v. rbt_lookup t k = Some v}" + "rbt_sorted t \ rbt_lookup t k = None \ k \ set (RBT_Impl.keys t)" + "rbt_sorted t \ (\v. rbt_lookup t k = Some v) \ k \ set (RBT_Impl.keys t)" + using entry_in_tree_keys rbt_lookup_keys[of t] + by force+ + lemma rbt_lookup_fold_rbt_insertwk: assumes t1: "rbt_sorted t1" and t2: "rbt_sorted t2" shows "rbt_lookup (fold (rbt_insert_with_key f) t1 t2) k = @@ -1939,9 +2577,363 @@ done qed +lemma rbt_lookup_union_rec: "rbt_sorted t1 \ rbt_sorted t2 \ + rbt_sorted (rbt_union_rec f t1 t2) \ rbt_lookup (rbt_union_rec f t1 t2) k = + (case rbt_lookup t1 k of None \ rbt_lookup t2 k + | Some v \ (case rbt_lookup t2 k of None \ Some v + | Some w \ Some (f k v w)))" +proof(induction f t1 t2 arbitrary: k rule: rbt_union_rec.induct) + case (1 f t1 t2) + obtain f' t1' t2' where flip: "(f', t2', t1') = + (if flip_rbt t2 t1 then (\k v v'. f k v' v, t1, t2) else (f, t2, t1))" + by fastforce + have rbt_sorted': "rbt_sorted t1'" "rbt_sorted t2'" + using 1(3,4) flip + by (auto split: if_splits) + show ?case + proof (cases t1') + case Empty + show ?thesis + unfolding rbt_union_rec.simps[of _ t1] flip[symmetric] + using flip rbt_sorted' rbt_split_props[of t2] + by (auto simp: Empty rbt_lookup_fold_rbt_insertwk + intro!: rbt_sorted_fold_insertwk split: if_splits option.splits) + next + case (Branch c l1 a b r1) + { + assume not_small: "\small_rbt t2'" + obtain l2 \ r2 where rbt_split_t2': "rbt_split t2' a = (l2, \, r2)" + by (cases "rbt_split t2' a") auto + have rbt_sort: "rbt_sorted l1" "rbt_sorted r1" + using 1(3,4) flip + by (auto simp: Branch split: if_splits) + note rbt_split_t2'_props = rbt_split_props[OF rbt_split_t2' rbt_sorted'(2)] + have union_l1_l2: "rbt_sorted (rbt_union_rec f' l1 l2)" "rbt_lookup (rbt_union_rec f' l1 l2) k = + (case rbt_lookup l1 k of None \ rbt_lookup l2 k + | Some v \ (case rbt_lookup l2 k of None \ Some v | Some w \ Some (f' k v w)))" for k + using 1(1)[OF flip refl refl _ Branch rbt_split_t2'[symmetric]] rbt_sort rbt_split_t2'_props + by (auto simp: not_small) + have union_r1_r2: "rbt_sorted (rbt_union_rec f' r1 r2)" "rbt_lookup (rbt_union_rec f' r1 r2) k = + (case rbt_lookup r1 k of None \ rbt_lookup r2 k + | Some v \ (case rbt_lookup r2 k of None \ Some v | Some w \ Some (f' k v w)))" for k + using 1(2)[OF flip refl refl _ Branch rbt_split_t2'[symmetric]] rbt_sort rbt_split_t2'_props + by (auto simp: not_small) + have union_l1_l2_keys: "set (RBT_Impl.keys (rbt_union_rec f' l1 l2)) = + set (RBT_Impl.keys l1) \ set (RBT_Impl.keys l2)" + using rbt_sorted'(1) rbt_split_t2'_props + by (auto simp: Branch rbt_lookup_iff_keys(1) union_l1_l2 split: option.splits) + have union_r1_r2_keys: "set (RBT_Impl.keys (rbt_union_rec f' r1 r2)) = + set (RBT_Impl.keys r1) \ set (RBT_Impl.keys r2)" + using rbt_sorted'(1) rbt_split_t2'_props + by (auto simp: Branch rbt_lookup_iff_keys(1) union_r1_r2 split: option.splits) + have union_l1_l2_less: "rbt_union_rec f' l1 l2 |\ a" + using rbt_sorted'(1) rbt_split_t2'_props + by (auto simp: Branch rbt_less_prop union_l1_l2_keys) + have union_r1_r2_greater: "a \| rbt_union_rec f' r1 r2" + using rbt_sorted'(1) rbt_split_t2'_props + by (auto simp: Branch rbt_greater_prop union_r1_r2_keys) + have "rbt_lookup (rbt_union_rec f t1 t2) k = + (case rbt_lookup t1' k of None \ rbt_lookup t2' k + | Some v \ (case rbt_lookup t2' k of None \ Some v | Some w \ Some (f' k v w)))" + using rbt_sorted' union_l1_l2 union_r1_r2 rbt_split_t2'_props + union_l1_l2_less union_r1_r2_greater not_small + by (auto simp: rbt_union_rec.simps[of _ t1] flip[symmetric] Branch + rbt_split_t2' rbt_lookup_rbt_join rbt_split_lookup[OF rbt_split_t2'] split: option.splits) + moreover have "rbt_sorted (rbt_union_rec f t1 t2)" + using rbt_sorted' rbt_split_t2'_props not_small + by (auto simp: rbt_union_rec.simps[of _ t1] flip[symmetric] Branch rbt_split_t2' + union_l1_l2 union_r1_r2 union_l1_l2_keys union_r1_r2_keys rbt_less_prop + rbt_greater_prop intro!: rbt_sorted_rbt_join) + ultimately have ?thesis + using flip + by (auto split: if_splits option.splits) + } + then show ?thesis + unfolding rbt_union_rec.simps[of _ t1] flip[symmetric] + using rbt_sorted' flip + by (auto simp: rbt_sorted_fold_insertwk rbt_lookup_fold_rbt_insertwk split: option.splits) + qed +qed + +lemma rbtreeify_map_filter_inter: + fixes f :: "'a \ 'b \ 'b \ 'b" + assumes "rbt_sorted t2" + shows "rbt_sorted (rbtreeify (map_filter_inter f t1 t2))" + "rbt_lookup (rbtreeify (map_filter_inter f t1 t2)) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ None | Some w \ Some (f k v w)))" +proof - + have map_of_map_filter: "map_of (List.map_filter (\(k, v). + case rbt_lookup t1 k of None \ None | Some v' \ Some (k, f k v' v)) xs) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case map_of xs k of None \ None | Some w \ Some (f k v w)))" for xs k + by (induction xs) (auto simp: List.map_filter_def split: option.splits) (* slow *) + have map_fst_map_filter: "map fst (List.map_filter (\(k, v). + case rbt_lookup t1 k of None \ None | Some v' \ Some (k, f k v' v)) xs) = + filter (\k. rbt_lookup t1 k \ None) (map fst xs)" for xs + by (induction xs) (auto simp: List.map_filter_def split: option.splits) + have "sorted (map fst (map_filter_inter f t1 t2))" + using sorted_filter[of id] rbt_sorted_entries[OF assms] + by (auto simp: map_filter_inter_def map_fst_map_filter) + moreover have "distinct (map fst (map_filter_inter f t1 t2))" + using distinct_filter distinct_entries[OF assms] + by (auto simp: map_filter_inter_def map_fst_map_filter) + ultimately show + "rbt_sorted (rbtreeify (map_filter_inter f t1 t2))" + "rbt_lookup (rbtreeify (map_filter_inter f t1 t2)) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ None | Some w \ Some (f k v w)))" + using rbt_sorted_rbtreeify + by (auto simp: rbt_lookup_rbtreeify map_filter_inter_def map_of_map_filter + map_of_entries[OF assms] split: option.splits) +qed + +lemma rbt_lookup_inter_rec: "rbt_sorted t1 \ rbt_sorted t2 \ + rbt_sorted (rbt_inter_rec f t1 t2) \ rbt_lookup (rbt_inter_rec f t1 t2) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ None | Some w \ Some (f k v w)))" +proof(induction f t1 t2 arbitrary: k rule: rbt_inter_rec.induct) + case (1 f t1 t2) + obtain f' t1' t2' where flip: "(f', t2', t1') = + (if flip_rbt t2 t1 then (\k v v'. f k v' v, t1, t2) else (f, t2, t1))" + by fastforce + have rbt_sorted': "rbt_sorted t1'" "rbt_sorted t2'" + using 1(3,4) flip + by (auto split: if_splits) + show ?case + proof (cases t1') + case Empty + show ?thesis + unfolding rbt_inter_rec.simps[of _ t1] flip[symmetric] + using flip rbt_sorted' rbt_split_props[of t2] rbtreeify_map_filter_inter[OF rbt_sorted'(2)] + by (auto simp: Empty split: option.splits) + next + case (Branch c l1 a b r1) + { + assume not_small: "\small_rbt t2'" + obtain l2 \ r2 where rbt_split_t2': "rbt_split t2' a = (l2, \, r2)" + by (cases "rbt_split t2' a") auto + note rbt_split_t2'_props = rbt_split_props[OF rbt_split_t2' rbt_sorted'(2)] + have rbt_sort: "rbt_sorted l1" "rbt_sorted r1" "rbt_sorted l2" "rbt_sorted r2" + using 1(3,4) flip + by (auto simp: Branch rbt_split_t2'_props split: if_splits) + have inter_l1_l2: "rbt_sorted (rbt_inter_rec f' l1 l2)" "rbt_lookup (rbt_inter_rec f' l1 l2) k = + (case rbt_lookup l1 k of None \ None + | Some v \ (case rbt_lookup l2 k of None \ None | Some w \ Some (f' k v w)))" for k + using 1(1)[OF flip refl refl _ Branch rbt_split_t2'[symmetric]] rbt_sort rbt_split_t2'_props + by (auto simp: not_small) + have inter_r1_r2: "rbt_sorted (rbt_inter_rec f' r1 r2)" "rbt_lookup (rbt_inter_rec f' r1 r2) k = + (case rbt_lookup r1 k of None \ None + | Some v \ (case rbt_lookup r2 k of None \ None | Some w \ Some (f' k v w)))" for k + using 1(2)[OF flip refl refl _ Branch rbt_split_t2'[symmetric]] rbt_sort rbt_split_t2'_props + by (auto simp: not_small) + have inter_l1_l2_keys: "set (RBT_Impl.keys (rbt_inter_rec f' l1 l2)) = + set (RBT_Impl.keys l1) \ set (RBT_Impl.keys l2)" + using inter_l1_l2(1) + by (auto simp: rbt_lookup_iff_keys(1) inter_l1_l2(2) rbt_sort split: option.splits) + have inter_r1_r2_keys: "set (RBT_Impl.keys (rbt_inter_rec f' r1 r2)) = + set (RBT_Impl.keys r1) \ set (RBT_Impl.keys r2)" + using inter_r1_r2(1) + by (auto simp: rbt_lookup_iff_keys(1) inter_r1_r2(2) rbt_sort split: option.splits) + have inter_l1_l2_less: "rbt_inter_rec f' l1 l2 |\ a" + using rbt_sorted'(1) rbt_split_t2'_props + by (auto simp: Branch rbt_less_prop inter_l1_l2_keys) + have inter_r1_r2_greater: "a \| rbt_inter_rec f' r1 r2" + using rbt_sorted'(1) rbt_split_t2'_props + by (auto simp: Branch rbt_greater_prop inter_r1_r2_keys) + have rbt_lookup_join2: "rbt_lookup (rbt_join2 (rbt_inter_rec f' l1 l2) (rbt_inter_rec f' r1 r2)) k = + (case rbt_lookup (rbt_inter_rec f' l1 l2) k of None \ rbt_lookup (rbt_inter_rec f' r1 r2) k + | Some v \ Some v)" for k + using rbt_lookup_rbt_join2[OF inter_l1_l2(1) inter_r1_r2(1)] rbt_sorted'(1) + by (fastforce simp: Branch inter_l1_l2_keys inter_r1_r2_keys rbt_less_prop rbt_greater_prop) + have rbt_lookup_l1_k: "rbt_lookup l1 k = Some v \ k < a" for k v + using rbt_sorted'(1) rbt_lookup_iff_keys(3) + by (auto simp: Branch rbt_less_prop) + have rbt_lookup_r1_k: "rbt_lookup r1 k = Some v \ a < k" for k v + using rbt_sorted'(1) rbt_lookup_iff_keys(3) + by (auto simp: Branch rbt_greater_prop) + have "rbt_lookup (rbt_inter_rec f t1 t2) k = + (case rbt_lookup t1' k of None \ None + | Some v \ (case rbt_lookup t2' k of None \ None | Some w \ Some (f' k v w)))" + by (auto simp: Let_def rbt_inter_rec.simps[of _ t1] flip[symmetric] not_small Branch + rbt_split_t2' rbt_lookup_join2 rbt_lookup_rbt_join inter_l1_l2_less inter_r1_r2_greater + rbt_split_lookup[OF rbt_split_t2' rbt_sorted'(2)] inter_l1_l2 inter_r1_r2 + split!: if_splits option.splits dest: rbt_lookup_l1_k rbt_lookup_r1_k) + moreover have "rbt_sorted (rbt_inter_rec f t1 t2)" + using rbt_sorted' inter_l1_l2 inter_r1_r2 rbt_split_t2'_props not_small + by (auto simp: Let_def rbt_inter_rec.simps[of _ t1] flip[symmetric] Branch rbt_split_t2' + rbt_less_prop rbt_greater_prop inter_l1_l2_less inter_r1_r2_greater + inter_l1_l2_keys inter_r1_r2_keys intro!: rbt_sorted_rbt_join rbt_sorted_rbt_join2 + split: if_splits option.splits dest!: bspec) + ultimately have ?thesis + using flip + by (auto split: if_splits split: option.splits) + } + then show ?thesis + unfolding rbt_inter_rec.simps[of _ t1] flip[symmetric] + using rbt_sorted' flip rbtreeify_map_filter_inter[OF rbt_sorted'(2)] + by (auto split: option.splits) + qed +qed + +lemma rbt_lookup_delete: + assumes "inv_12 t" "rbt_sorted t" + shows "rbt_lookup (rbt_delete x t) k = (if x = k then None else rbt_lookup t k)" +proof - + note rbt_sorted_del = rbt_del_rbt_sorted[OF assms(2), of x] + show ?thesis + using assms rbt_sorted_del rbt_del_in_tree rbt_lookup_from_in_tree[OF assms(2) rbt_sorted_del] + by (fastforce simp: inv_12_def rbt_delete_def rbt_lookup_iff_keys(2) keys_entries) +qed + +lemma fold_rbt_delete: + assumes "inv_12 t1" "rbt_sorted t1" "rbt_sorted t2" + shows "inv_12 (RBT_Impl.fold (\k _ t. rbt_delete k t) t2 t1) \ + rbt_sorted (RBT_Impl.fold (\k _ t. rbt_delete k t) t2 t1) \ + rbt_lookup (RBT_Impl.fold (\k _ t. rbt_delete k t) t2 t1) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ Some v | _ \ None))" +proof - + define xs where "xs = RBT_Impl.entries t2" + show "inv_12 (RBT_Impl.fold (\k _ t. rbt_delete k t) t2 t1) \ + rbt_sorted (RBT_Impl.fold (\k _ t. rbt_delete k t) t2 t1) \ + rbt_lookup (RBT_Impl.fold (\k _ t. rbt_delete k t) t2 t1) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ Some v | _ \ None))" + using assms(1,2) + unfolding map_of_entries[OF assms(3), symmetric] RBT_Impl.fold_def xs_def[symmetric] + by (induction xs arbitrary: t1 rule: rev_induct) + (auto simp: rbt_delete rbt_sorted_delete rbt_lookup_delete split!: option.splits) +qed + +lemma rbtreeify_filter_minus: + assumes "rbt_sorted t1" + shows "rbt_sorted (rbtreeify (filter_minus t1 t2)) \ + rbt_lookup (rbtreeify (filter_minus t1 t2)) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ Some v | _ \ None))" +proof - + have map_of_filter: "map_of (filter (\(k, _). rbt_lookup t2 k = None) xs) k = + (case map_of xs k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ Some v | Some x \ Map.empty x))" + for xs :: "('a \ 'b) list" + by (induction xs) (auto split: option.splits) + have map_fst_filter_minus: "map fst (filter_minus t1 t2) = + filter (\k. rbt_lookup t2 k = None) (map fst (RBT_Impl.entries t1))" + by (auto simp: filter_minus_def filter_map comp_def case_prod_unfold) + have "sorted (map fst (filter_minus t1 t2))" "distinct (map fst (filter_minus t1 t2))" + using distinct_filter distinct_entries[OF assms] + sorted_filter[of id] rbt_sorted_entries[OF assms] + by (auto simp: map_fst_filter_minus intro!: rbt_sorted_rbtreeify) + then show ?thesis + by (auto simp: rbt_lookup_rbtreeify filter_minus_def map_of_filter map_of_entries[OF assms] + intro!: rbt_sorted_rbtreeify) +qed + +lemma rbt_lookup_minus_rec: "inv_12 t1 \ rbt_sorted t1 \ rbt_sorted t2 \ + rbt_sorted (rbt_minus_rec t1 t2) \ rbt_lookup (rbt_minus_rec t1 t2) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ Some v | _ \ None))" +proof(induction t1 t2 arbitrary: k rule: rbt_minus_rec.induct) + case (1 t1 t2) + show ?case + proof (cases t2) + case Empty + show ?thesis + using rbtreeify_filter_minus[OF 1(4)] 1(4) + by (auto simp: rbt_minus_rec.simps[of t1] Empty split: option.splits) + next + case (Branch c l2 a b r2) + { + assume not_small: "\small_rbt t2" "\small_rbt t1" + obtain l1 \ r1 where rbt_split_t1: "rbt_split t1 a = (l1, \, r1)" + by (cases "rbt_split t1 a") auto + note rbt_split_t1_props = rbt_split_props[OF rbt_split_t1 1(4)] + have minus_l1_l2: "rbt_sorted (rbt_minus_rec l1 l2)" + "rbt_lookup (rbt_minus_rec l1 l2) k = + (case rbt_lookup l1 k of None \ None + | Some v \ (case rbt_lookup l2 k of None \ Some v | Some x \ None))" for k + using 1(1)[OF not_small Branch rbt_split_t1[symmetric] refl] 1(5) rbt_split_t1_props + rbt_split[OF rbt_split_t1 1(3)] + by (auto simp: Branch) + have minus_r1_r2: "rbt_sorted (rbt_minus_rec r1 r2)" + "rbt_lookup (rbt_minus_rec r1 r2) k = + (case rbt_lookup r1 k of None \ None + | Some v \ (case rbt_lookup r2 k of None \ Some v | Some x \ None))" for k + using 1(2)[OF not_small Branch rbt_split_t1[symmetric] refl] 1(5) rbt_split_t1_props + rbt_split[OF rbt_split_t1 1(3)] + by (auto simp: Branch) + have minus_l1_l2_keys: "set (RBT_Impl.keys (rbt_minus_rec l1 l2)) = + set (RBT_Impl.keys l1) - set (RBT_Impl.keys l2)" + using minus_l1_l2(1) 1(5) rbt_lookup_iff_keys(3) rbt_split_t1_props + by (auto simp: Branch rbt_lookup_iff_keys(1) minus_l1_l2(2) split: option.splits) + have minus_r1_r2_keys: "set (RBT_Impl.keys (rbt_minus_rec r1 r2)) = + set (RBT_Impl.keys r1) - set (RBT_Impl.keys r2)" + using minus_r1_r2(1) 1(5) rbt_lookup_iff_keys(3) rbt_split_t1_props + by (auto simp: Branch rbt_lookup_iff_keys(1) minus_r1_r2(2) split: option.splits) + have rbt_lookup_join2: "rbt_lookup (rbt_join2 (rbt_minus_rec l1 l2) (rbt_minus_rec r1 r2)) k = + (case rbt_lookup (rbt_minus_rec l1 l2) k of None \ rbt_lookup (rbt_minus_rec r1 r2) k + | Some v \ Some v)" for k + using rbt_lookup_rbt_join2[OF minus_l1_l2(1) minus_r1_r2(1)] rbt_split_t1_props + by (fastforce simp: minus_l1_l2_keys minus_r1_r2_keys) + have lookup_l1_r1_a: "rbt_lookup l1 a = None" "rbt_lookup r1 a = None" + using rbt_split_t1_props + by (auto simp: rbt_lookup_iff_keys(2)) + have "rbt_lookup (rbt_minus_rec t1 t2) k = + (case rbt_lookup t1 k of None \ None + | Some v \ (case rbt_lookup t2 k of None \ Some v | _ \ None))" + using not_small rbt_lookup_iff_keys(2)[of l1] rbt_lookup_iff_keys(3)[of l1] + rbt_lookup_iff_keys(3)[of r1] rbt_split_t1_props + by (auto simp: rbt_minus_rec.simps[of t1] Branch rbt_split_t1 rbt_lookup_join2 + minus_l1_l2(2) minus_r1_r2(2) rbt_split_lookup[OF rbt_split_t1 1(4)] lookup_l1_r1_a + split: option.splits) + moreover have "rbt_sorted (rbt_minus_rec t1 t2)" + using not_small minus_l1_l2(1) minus_r1_r2(1) rbt_split_t1_props rbt_sorted_rbt_join2 + by (fastforce simp: rbt_minus_rec.simps[of t1] Branch rbt_split_t1 minus_l1_l2_keys minus_r1_r2_keys) + ultimately have ?thesis + by (auto split: if_splits split: option.splits) + } + then show ?thesis + using fold_rbt_delete[OF 1(3,4,5)] rbtreeify_filter_minus[OF 1(4)] + by (auto simp: rbt_minus_rec.simps[of t1]) + qed +qed + +end + +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 = paint B (rbt_union_swap_rec f False t1 t2)" + +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 = paint B (rbt_inter_swap_rec f False t1 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)" + +definition rbt_minus where + "rbt_minus t1 t2 = paint B (rbt_minus_rec t1 t2)" + +end + +context linorder begin + lemma is_rbt_rbt_unionwk [simp]: "\ is_rbt t1; is_rbt t2 \ \ is_rbt (rbt_union_with_key f t1 t2)" -by(simp add: rbt_union_with_key_def Let_def is_rbt_fold_rbt_insertwk is_rbt_rbtreeify rbt_sorted_entries distinct_entries split: compare.split) + using rbt_union_rec rbt_lookup_union_rec + by (fastforce simp: rbt_union_with_key_def rbt_union_swap_rec is_rbt_def inv_12_def) lemma rbt_lookup_rbt_unionwk: "\ rbt_sorted t1; rbt_sorted t2 \ @@ -1949,7 +2941,8 @@ (case rbt_lookup t1 k of None \ rbt_lookup t2 k | Some v \ case rbt_lookup t2 k of None \ Some v | Some w \ Some (f k v w))" -by(auto simp add: rbt_union_with_key_def Let_def rbt_lookup_fold_rbt_insertwk rbt_sorted_entries distinct_entries map_of_sunion_with map_of_entries rbt_lookup_rbtreeify split: option.split compare.split) + using rbt_lookup_union_rec + by (auto simp: rbt_union_with_key_def rbt_union_swap_rec) lemma rbt_unionw_is_rbt: "\ is_rbt lt; is_rbt rt \ \ is_rbt (rbt_union_with f lt rt)" by(simp add: rbt_union_with_def) @@ -1963,15 +2956,16 @@ by(rule ext)(simp add: rbt_lookup_rbt_unionwk rbt_union_def map_add_def split: option.split) lemma rbt_interwk_is_rbt [simp]: - "\ rbt_sorted t1; rbt_sorted t2 \ \ is_rbt (rbt_inter_with_key f t1 t2)" -by(auto simp add: rbt_inter_with_key_def Let_def map_map_filter split_def o_def option.map_comp map_filter_map_option_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries intro: is_rbt_rbtreeify split: compare.split) + "\ is_rbt t1; is_rbt t2 \ \ is_rbt (rbt_inter_with_key f t1 t2)" + using rbt_inter_rec rbt_lookup_inter_rec + by (fastforce simp: rbt_inter_with_key_def rbt_inter_swap_rec is_rbt_def inv_12_def rbt_sorted_paint) lemma rbt_interw_is_rbt: - "\ rbt_sorted t1; rbt_sorted t2 \ \ is_rbt (rbt_inter_with f t1 t2)" + "\ is_rbt t1; is_rbt t2 \ \ is_rbt (rbt_inter_with f t1 t2)" by(simp add: rbt_inter_with_def) lemma rbt_inter_is_rbt: - "\ rbt_sorted t1; rbt_sorted t2 \ \ is_rbt (rbt_inter t1 t2)" + "\ is_rbt t1; is_rbt t2 \ \ is_rbt (rbt_inter t1 t2)" by(simp add: rbt_inter_def) lemma rbt_lookup_rbt_interwk: @@ -1980,13 +2974,26 @@ (case rbt_lookup t1 k of None \ None | Some v \ case rbt_lookup t2 k of None \ None | Some w \ Some (f k v w))" -by(auto 4 3 simp add: rbt_inter_with_key_def Let_def map_of_entries[symmetric] rbt_lookup_rbtreeify map_map_filter split_def o_def option.map_comp map_filter_map_option_const sorted_filter[where f=id, simplified] rbt_sorted_entries distinct_entries map_of_sinter_with map_of_eq_None_iff set_map_filter split: option.split compare.split intro: rev_image_eqI dest: rbt_sorted_entries_right_unique) + using rbt_lookup_inter_rec + by (auto simp: rbt_inter_with_key_def rbt_inter_swap_rec) lemma rbt_lookup_rbt_inter: "\ rbt_sorted t1; rbt_sorted t2 \ \ rbt_lookup (rbt_inter t1 t2) = rbt_lookup t2 |` dom (rbt_lookup t1)" by(auto simp add: rbt_inter_def rbt_lookup_rbt_interwk restrict_map_def split: option.split) +lemma rbt_minus_is_rbt: + "\ is_rbt t1; is_rbt t2 \ \ is_rbt (rbt_minus t1 t2)" + using rbt_minus_rec[of t1 t2] rbt_lookup_minus_rec[of t1 t2] + by (auto simp: rbt_minus_def is_rbt_def inv_12_def) + +lemma rbt_lookup_rbt_minus: + "\ is_rbt t1; is_rbt t2 \ + \ rbt_lookup (rbt_minus t1 t2) = rbt_lookup t1 |` (- dom (rbt_lookup t2))" + by (rule ext) + (auto simp: rbt_minus_def is_rbt_def inv_12_def restrict_map_def rbt_lookup_minus_rec + split: option.splits) + end @@ -2006,14 +3013,19 @@ ord.rbt_del_from_right.simps ord.rbt_del.simps ord.rbt_delete_def - ord.sunion_with.simps - ord.sinter_with.simps + ord.rbt_split.simps + ord.rbt_union_swap_rec.simps + ord.map_filter_inter_def + ord.rbt_inter_swap_rec.simps + ord.filter_minus_def + ord.rbt_minus_rec.simps ord.rbt_union_with_key_def ord.rbt_union_with_def ord.rbt_union_def ord.rbt_inter_with_key_def ord.rbt_inter_with_def ord.rbt_inter_def + ord.rbt_minus_def ord.rbt_map_entry.simps ord.rbt_bulkload_def @@ -2070,6 +3082,6 @@ (\<^const_name>\rbt_bulkload\, SOME \<^typ>\('a \ 'b) list \ ('a::linorder,'b) rbt\)] \ -hide_const (open) R B Empty entries keys fold gen_keys gen_entries +hide_const (open) MR MB R B Empty entries keys fold gen_keys gen_entries end diff -r feaf43e23b3a -r 6974bca47856 src/HOL/Library/Sublist.thy --- a/src/HOL/Library/Sublist.thy Mon Feb 01 14:01:01 2021 +0100 +++ b/src/HOL/Library/Sublist.thy Mon Feb 01 16:03:07 2021 +0100 @@ -476,40 +476,19 @@ obtains "prefix xs ys" | "strict_prefix ys xs" | "xs \ ys" unfolding parallel_def strict_prefix_def by blast +lemma parallel_cancel: "a#xs \ a#ys \ xs \ ys" + by (simp add: parallel_def) + theorem parallel_decomp: "xs \ ys \ \as b bs c cs. b \ c \ xs = as @ b # bs \ ys = as @ c # cs" -proof (induct xs rule: rev_induct) - case Nil - then have False by auto - then show ?case .. -next - case (snoc x xs) - show ?case - proof (rule prefix_cases) - assume le: "prefix xs ys" - then obtain ys' where ys: "ys = xs @ ys'" .. - show ?thesis - proof (cases ys') - assume "ys' = []" - then show ?thesis by (metis append_Nil2 parallelE prefixI snoc.prems ys) - next - fix c cs assume ys': "ys' = c # cs" - have "x \ c" using snoc.prems ys ys' by fastforce - thus "\as b bs c cs. b \ c \ xs @ [x] = as @ b # bs \ ys = as @ c # cs" - using ys ys' by blast - qed - next - assume "strict_prefix ys xs" - then have "prefix ys (xs @ [x])" by (simp add: strict_prefix_def) - with snoc have False by blast - then show ?thesis .. - next - assume "xs \ ys" - with snoc obtain as b bs c cs where neq: "(b::'a) \ c" - and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" - by blast - from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp - with neq ys show ?thesis by blast +proof (induct rule: list_induct2', blast, force, force) + case (4 x xs y ys) + then show ?case + proof (cases "x \ y", blast) + assume "\ x \ y" hence "x = y" by blast + then show ?thesis + using "4.hyps"[OF parallel_cancel[OF "4.prems"[folded \x = y\]]] + by (meson Cons_eq_appendI) qed qed diff -r feaf43e23b3a -r 6974bca47856 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Mon Feb 01 14:01:01 2021 +0100 +++ b/src/HOL/Set_Interval.thy Mon Feb 01 16:03:07 2021 +0100 @@ -1545,6 +1545,18 @@ finally show ?thesis. qed +lemma card_le_Suc_Max: "finite S \ card S \ Suc (Max S)" +proof (rule classical) + assume "finite S" and "\ Suc (Max S) \ card S" + then have "Suc (Max S) < card S" + by simp + with `finite S` have "S \ {0..Max S}" + by auto + hence "card S \ card {0..Max S}" + by (intro card_mono; auto) + thus "card S \ Suc (Max S)" + by simp +qed subsection \Lemmas useful with the summation operator sum\ @@ -2057,6 +2069,30 @@ end +lemma card_sum_le_nat_sum: "\ {0.. \ S" +proof (cases "finite S") + case True + then show ?thesis + proof (induction "card S" arbitrary: S) + case (Suc x) + then have "Max S \ x" using card_le_Suc_Max by fastforce + let ?S' = "S - {Max S}" + from Suc have "Max S \ S" by (auto intro: Max_in) + hence cards: "card S = Suc (card ?S')" + using `finite S` by (intro card.remove; auto) + hence "\ {0.. \ ?S'" + using Suc by (intro Suc; auto) + + hence "\ {0.. \ ?S' + Max S" + using `Max S \ x` by simp + also have "... = \ S" + using sum.remove[OF `finite S` `Max S \ S`, where g="\x. x"] + by simp + finally show ?case + using cards Suc by auto + qed simp +qed simp + lemma sum_natinterval_diff: fixes f:: "nat \ ('a::ab_group_add)" shows "sum (\k. f k - f(k + 1)) {(m::nat) .. n} = diff -r feaf43e23b3a -r 6974bca47856 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Mon Feb 01 14:01:01 2021 +0100 +++ b/src/Pure/Admin/build_history.scala Mon Feb 01 16:03:07 2021 +0100 @@ -161,8 +161,12 @@ val (afp_build_args, afp_sessions) = if (afp_rev.isEmpty) (Nil, Nil) else { - val afp = AFP.init(options, afp_repos) - (List("-d", "~~/AFP/thys"), afp.partition(afp_partition)) + val (opt, sessions) = + try { + val afp = AFP.init(options, afp_repos) + ("-d", afp.partition(afp_partition)) + } catch { case ERROR(_) => ("-D", Nil) } + (List(opt, "~~/AFP/thys"), sessions) } @@ -570,7 +574,7 @@ else { val afp_repos = isabelle_repos_other + Path.explode("AFP") Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh) - " -A " + Bash.string(afp_rev.get) + " -A " + Bash.string(afp_rev.get) } @@ -580,11 +584,19 @@ { val output_file = tmp_dir + Path.explode("output") - execute("Admin/build_history", - "-o " + ssh.bash_path(output_file) + - (if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " + - options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args, - echo = true, strict = false) + val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id) + + try { + execute("Admin/build_history", + "-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " + + ssh.bash_path(isabelle_repos_other) + " " + args, + echo = true, strict = false) + } + catch { + case ERROR(msg) => + cat_error(msg, + "The error(s) above occurred for build_bistory " + rev_options + afp_options) + } for (line <- split_lines(ssh.read(output_file))) yield { diff -r feaf43e23b3a -r 6974bca47856 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Mon Feb 01 14:01:01 2021 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Mon Feb 01 16:03:07 2021 +0100 @@ -104,7 +104,7 @@ isabelle_identifier = "cronjob_build_history", self_update = true, rev = "build_history_base", - options = "-f", + options = "-C '$USER_HOME/.isabelle/contrib' -f", args = "HOL") for ((log_name, bytes) <- results) { @@ -326,6 +326,14 @@ options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false", self_update = true, args = "-a -d '~~/src/Benchmarks'")), List( + Remote_Build("macOS 11.1 Big Sur", "mini1", + options = "-m32 -B -M1x2,2,4 -p pide_session=false" + + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + + " -e ISABELLE_GHC_SETUP=true" + + " -e ISABELLE_MLTON=/usr/local/bin/mlton" + + " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" + + " -e ISABELLE_SWIPL=/usr/local/bin/swipl", + self_update = true, args = "-a -d '~~/src/Benchmarks'"), Remote_Build("macOS 10.14 Mojave", "mini2", options = "-m32 -B -M1x2,2,4 -p pide_session=false" + " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" + @@ -407,6 +415,7 @@ rev = rev, afp_rev = afp_rev, options = + " -C '$USER_HOME/.isabelle/contrib'" + " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) + " -f -h " + Bash.string(r.host) + " " + (r.java_heap match {