# HG changeset patch # User haftmann # Date 1509369524 0 # Node ID c78ff0aeba4c2bdbc72c24f4e39b59f728006b64 # Parent a1a4a5e2933a76b0c585f0c2d4583e89dbb6387b generalized some lemmas on multisets diff -r a1a4a5e2933a -r c78ff0aeba4c src/HOL/Computational_Algebra/Factorial_Ring.thy --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Oct 30 13:18:44 2017 +0000 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Oct 30 13:18:44 2017 +0000 @@ -1424,7 +1424,7 @@ define A where "A = Abs_multiset f" from \finite S\ S(1) have "(\p\S. p ^ f p) \ 0" by auto with S(2) have nz: "n \ 0" by auto - from S_eq \finite S\ have count_A: "count A x = f x" for x + from S_eq \finite S\ have count_A: "count A = f" unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def) from S_eq count_A have set_mset_A: "set_mset A = S" by (simp only: set_mset_def) @@ -1452,7 +1452,8 @@ also from S(1) p have "image_mset (multiplicity p) A = image_mset (\q. if p = q then 1 else 0) A" by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other) - also have "sum_mset \ = f p" by (simp add: sum_mset_delta' count_A) + also have "sum_mset \ = f p" + by (simp add: semiring_1_class.sum_mset_delta' count_A) finally show "f p = multiplicity p n" .. qed qed diff -r a1a4a5e2933a -r c78ff0aeba4c src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Oct 30 13:18:44 2017 +0000 +++ b/src/HOL/Library/Multiset.thy Mon Oct 30 13:18:44 2017 +0000 @@ -2247,52 +2247,12 @@ sublocale sum_mset: comm_monoid_mset plus 0 defines sum_mset = sum_mset.F .. -lemma (in semiring_1) sum_mset_replicate_mset [simp]: - "sum_mset (replicate_mset n a) = of_nat n * a" - by (induct n) (simp_all add: algebra_simps) - lemma sum_unfold_sum_mset: "sum f A = sum_mset (image_mset f (mset_set A))" by (cases "finite A") (induct A rule: finite_induct, simp_all) -lemma sum_mset_delta: "sum_mset (image_mset (\x. if x = y then c else 0) A) = c * count A y" - by (induction A) simp_all - -lemma sum_mset_delta': "sum_mset (image_mset (\x. if y = x then c else 0) A) = c * count A y" - by (induction A) simp_all - end -lemma of_nat_sum_mset [simp]: - "of_nat (sum_mset M) = sum_mset (image_mset of_nat M)" -by (induction M) auto - -lemma sum_mset_0_iff [simp]: - "sum_mset M = (0::'a::canonically_ordered_monoid_add) - \ (\x \ set_mset M. x = 0)" -by(induction M) auto - -lemma sum_mset_diff: - fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset" - shows "N \# M \ sum_mset (M - N) = sum_mset M - sum_mset N" - by (metis add_diff_cancel_right' sum_mset.union subset_mset.diff_add) - -lemma size_eq_sum_mset: "size M = sum_mset (image_mset (\_. 1) M)" -proof (induct M) - case empty then show ?case by simp -next - case (add x M) then show ?case - by (cases "x \ set_mset M") - (simp_all add: size_multiset_overloaded_eq not_in_iff sum.If_cases Diff_eq[symmetric] - sum.remove) -qed - -lemma size_mset_set [simp]: "size (mset_set A) = card A" -by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset) - -lemma sum_mset_sum_list: "sum_mset (mset xs) = sum_list xs" - by (induction xs) auto - syntax (ASCII) "_sum_mset_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10) syntax @@ -2300,31 +2260,95 @@ translations "\i \# A. b" \ "CONST sum_mset (CONST image_mset (\i. b) A)" +context comm_monoid_add +begin + +lemma sum_mset_sum_list: + "sum_mset (mset xs) = sum_list xs" + by (induction xs) auto + +end + +context canonically_ordered_monoid_add +begin + +lemma sum_mset_0_iff [simp]: + "sum_mset M = 0 \ (\x \ set_mset M. x = 0)" + by (induction M) auto + +end + +context ordered_comm_monoid_add +begin + +lemma sum_mset_mono: + "sum_mset (image_mset f K) \ sum_mset (image_mset g K)" + if "\i. i \# K \ f i \ g i" + using that by (induction K) (simp_all add: add_mono) + +end + +context ordered_cancel_comm_monoid_diff +begin + +lemma sum_mset_diff: + "sum_mset (M - N) = sum_mset M - sum_mset N" if "N \# M" for M N :: "'a multiset" + using that by (auto simp add: subset_mset.le_iff_add) + +end + +context semiring_0 +begin + lemma sum_mset_distrib_left: - fixes f :: "'a \ 'b::semiring_0" - shows "c * (\x \# M. f x) = (\x \# M. c * f(x))" -by (induction M) (simp_all add: distrib_left) + "c * (\x \# M. f x) = (\x \# M. c * f(x))" + by (induction M) (simp_all add: algebra_simps) lemma sum_mset_distrib_right: - fixes f :: "'a \ 'b::semiring_0" - shows "(\b \# B. f b) * a = (\b \# B. f b * a)" - by (induction B) (auto simp: distrib_right) + "(\x \# M. f x) * c = (\x \# M. f x * c)" + by (induction M) (simp_all add: algebra_simps) + +end + +lemma sum_mset_product: + fixes f :: "'a::{comm_monoid_add,times} \ 'b::semiring_0" + shows "(\i \# A. f i) * (\i \# B. g i) = (\i\#A. \j\#B. f i * g j)" + by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right) + +context semiring_1 +begin + +lemma sum_mset_replicate_mset [simp]: + "sum_mset (replicate_mset n a) = of_nat n * a" + by (induction n) (simp_all add: algebra_simps) + +lemma sum_mset_delta: + "sum_mset (image_mset (\x. if x = y then c else 0) A) = c * of_nat (count A y)" + by (induction A) (simp_all add: algebra_simps) + +lemma sum_mset_delta': + "sum_mset (image_mset (\x. if y = x then c else 0) A) = c * of_nat (count A y)" + by (induction A) (simp_all add: algebra_simps) + +end + +lemma of_nat_sum_mset [simp]: + "of_nat (sum_mset A) = sum_mset (image_mset of_nat A)" + by (induction A) auto + +lemma size_eq_sum_mset: + "size M = (\a\#M. 1)" + using image_mset_const_eq [of "1::nat" M] by simp + +lemma size_mset_set [simp]: + "size (mset_set A) = card A" + by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset) lemma sum_mset_constant [simp]: fixes y :: "'b::semiring_1" shows \(\x\#A. y) = of_nat (size A) * y\ by (induction A) (auto simp: algebra_simps) -lemma (in ordered_comm_monoid_add) sum_mset_mono: - assumes "\i. i \# K \ f i \ g i" - shows "sum_mset (image_mset f K) \ sum_mset (image_mset g K)" - using assms by (induction K) (simp_all add: local.add_mono) - -lemma sum_mset_product: - fixes f :: "'a::{comm_monoid_add,times} \ 'b::semiring_0" - shows "(\i \# A. f i) * (\i \# B. g i) = (\i\#A. \j\#B. f i * g j)" - by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right) - abbreviation Union_mset :: "'a multiset multiset \ 'a multiset" ("\#_" [900] 900) where "\# MM \ sum_mset MM" \ \FIXME ambiguous notation -- could likewise refer to \\#\\ @@ -2347,6 +2371,7 @@ lemma Union_mset_empty_conv[simp]: "\# M = {#} \ (\i\#M. i = {#})" by (induction M) auto + context comm_monoid_mult begin @@ -2365,6 +2390,10 @@ "prod_mset (A + B) = prod_mset A * prod_mset B" by (fact prod_mset.union) +lemma prod_mset_prod_list: + "prod_mset (mset xs) = prod_list xs" + by (induct xs) auto + lemma prod_mset_replicate_mset [simp]: "prod_mset (replicate_mset n a) = a ^ n" by (induct n) simp_all @@ -2383,6 +2412,21 @@ lemma prod_mset_delta': "prod_mset (image_mset (\x. if y = x then c else 1) A) = c ^ count A y" by (induction A) simp_all +lemma prod_mset_subset_imp_dvd: + assumes "A \# B" + shows "prod_mset A dvd prod_mset B" +proof - + from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add) + also have "prod_mset \ = prod_mset (B - A) * prod_mset A" by simp + also have "prod_mset A dvd \" by simp + finally show ?thesis . +qed + +lemma dvd_prod_mset: + assumes "x \# A" + shows "x dvd prod_mset A" + using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp + end syntax (ASCII) @@ -2395,21 +2439,6 @@ lemma prod_mset_constant [simp]: "(\_\#A. c) = c ^ size A" by (simp add: image_mset_const_eq) -lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd: - assumes "A \# B" - shows "prod_mset A dvd prod_mset B" -proof - - from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add) - also have "prod_mset \ = prod_mset (B - A) * prod_mset A" by simp - also have "prod_mset A dvd \" by simp - finally show ?thesis . -qed - -lemma (in comm_monoid_mult) dvd_prod_mset: - assumes "x \# A" - shows "x dvd prod_mset A" - using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp - lemma (in semidom) prod_mset_zero_iff [iff]: "prod_mset A = 0 \ 0 \# A" by (induct A) auto @@ -2445,9 +2474,6 @@ then show ?thesis by (simp add: normalize_prod_mset) qed -lemma prod_mset_prod_list: "prod_mset (mset xs) = prod_list xs" - by (induct xs) auto - subsection \Alternative representations\