author haftmann Mon Oct 30 13:18:44 2017 +0000 (18 months ago) changeset 66938 c78ff0aeba4c parent 66937 a1a4a5e2933a child 66940 e5776e8e152b child 66942 91a21a5631ae
generalized some lemmas on multisets
```     1.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Oct 30 13:18:44 2017 +0000
1.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Oct 30 13:18:44 2017 +0000
1.3 @@ -1424,7 +1424,7 @@
1.4    define A where "A = Abs_multiset f"
1.5    from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
1.6    with S(2) have nz: "n \<noteq> 0" by auto
1.7 -  from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
1.8 +  from S_eq \<open>finite S\<close> have count_A: "count A = f"
1.9      unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
1.10    from S_eq count_A have set_mset_A: "set_mset A = S"
1.11      by (simp only: set_mset_def)
1.12 @@ -1452,7 +1452,8 @@
1.13      also from S(1) p
1.14      have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
1.15        by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
1.16 -    also have "sum_mset \<dots> = f p" by (simp add: sum_mset_delta' count_A)
1.17 +    also have "sum_mset \<dots> = f p"
1.18 +      by (simp add: semiring_1_class.sum_mset_delta' count_A)
1.19      finally show "f p = multiplicity p n" ..
1.20    qed
1.21  qed
```
```     2.1 --- a/src/HOL/Library/Multiset.thy	Mon Oct 30 13:18:44 2017 +0000
2.2 +++ b/src/HOL/Library/Multiset.thy	Mon Oct 30 13:18:44 2017 +0000
2.3 @@ -2247,52 +2247,12 @@
2.4  sublocale sum_mset: comm_monoid_mset plus 0
2.5    defines sum_mset = sum_mset.F ..
2.6
2.7 -lemma (in semiring_1) sum_mset_replicate_mset [simp]:
2.8 -  "sum_mset (replicate_mset n a) = of_nat n * a"
2.9 -  by (induct n) (simp_all add: algebra_simps)
2.10 -
2.11  lemma sum_unfold_sum_mset:
2.12    "sum f A = sum_mset (image_mset f (mset_set A))"
2.13    by (cases "finite A") (induct A rule: finite_induct, simp_all)
2.14
2.15 -lemma sum_mset_delta: "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
2.16 -  by (induction A) simp_all
2.17 -
2.18 -lemma sum_mset_delta': "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
2.19 -  by (induction A) simp_all
2.20 -
2.21  end
2.22
2.23 -lemma of_nat_sum_mset [simp]:
2.24 -  "of_nat (sum_mset M) = sum_mset (image_mset of_nat M)"
2.25 -by (induction M) auto
2.26 -
2.27 -lemma sum_mset_0_iff [simp]:
2.28 -  "sum_mset M = (0::'a::canonically_ordered_monoid_add)
2.29 -   \<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
2.30 -by(induction M) auto
2.31 -
2.32 -lemma sum_mset_diff:
2.33 -  fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
2.34 -  shows "N \<subseteq># M \<Longrightarrow> sum_mset (M - N) = sum_mset M - sum_mset N"
2.36 -
2.37 -lemma size_eq_sum_mset: "size M = sum_mset (image_mset (\<lambda>_. 1) M)"
2.38 -proof (induct M)
2.39 -  case empty then show ?case by simp
2.40 -next
2.41 -  case (add x M) then show ?case
2.42 -    by (cases "x \<in> set_mset M")
2.44 -        sum.remove)
2.45 -qed
2.46 -
2.47 -lemma size_mset_set [simp]: "size (mset_set A) = card A"
2.48 -by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
2.49 -
2.50 -lemma sum_mset_sum_list: "sum_mset (mset xs) = sum_list xs"
2.51 -  by (induction xs) auto
2.52 -
2.53  syntax (ASCII)
2.54    "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
2.55  syntax
2.56 @@ -2300,31 +2260,95 @@
2.57  translations
2.58    "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
2.59
2.61 +begin
2.62 +
2.63 +lemma sum_mset_sum_list:
2.64 +  "sum_mset (mset xs) = sum_list xs"
2.65 +  by (induction xs) auto
2.66 +
2.67 +end
2.68 +
2.70 +begin
2.71 +
2.72 +lemma sum_mset_0_iff [simp]:
2.73 +  "sum_mset M = 0  \<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
2.74 +  by (induction M) auto
2.75 +
2.76 +end
2.77 +
2.79 +begin
2.80 +
2.81 +lemma sum_mset_mono:
2.82 +  "sum_mset (image_mset f K) \<le> sum_mset (image_mset g K)"
2.83 +  if "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
2.85 +
2.86 +end
2.87 +
2.88 +context ordered_cancel_comm_monoid_diff
2.89 +begin
2.90 +
2.91 +lemma sum_mset_diff:
2.92 +  "sum_mset (M - N) = sum_mset M - sum_mset N" if "N \<subseteq># M" for M N :: "'a multiset"
2.94 +
2.95 +end
2.96 +
2.97 +context semiring_0
2.98 +begin
2.99 +
2.100  lemma sum_mset_distrib_left:
2.101 -  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
2.102 -  shows "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
2.103 -by (induction M) (simp_all add: distrib_left)
2.104 +  "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
2.105 +  by (induction M) (simp_all add: algebra_simps)
2.106
2.107  lemma sum_mset_distrib_right:
2.108 -  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
2.109 -  shows "(\<Sum>b \<in># B. f b) * a = (\<Sum>b \<in># B. f b * a)"
2.110 -  by (induction B) (auto simp: distrib_right)
2.111 +  "(\<Sum>x \<in># M. f x) * c = (\<Sum>x \<in># M. f x * c)"
2.112 +  by (induction M) (simp_all add: algebra_simps)
2.113 +
2.114 +end
2.115 +
2.116 +lemma sum_mset_product:
2.117 +  fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
2.118 +  shows "(\<Sum>i \<in># A. f i) * (\<Sum>i \<in># B. g i) = (\<Sum>i\<in>#A. \<Sum>j\<in>#B. f i * g j)"
2.119 +  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
2.120 +
2.121 +context semiring_1
2.122 +begin
2.123 +
2.124 +lemma sum_mset_replicate_mset [simp]:
2.125 +  "sum_mset (replicate_mset n a) = of_nat n * a"
2.126 +  by (induction n) (simp_all add: algebra_simps)
2.127 +
2.128 +lemma sum_mset_delta:
2.129 +  "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * of_nat (count A y)"
2.130 +  by (induction A) (simp_all add: algebra_simps)
2.131 +
2.132 +lemma sum_mset_delta':
2.133 +  "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * of_nat (count A y)"
2.134 +  by (induction A) (simp_all add: algebra_simps)
2.135 +
2.136 +end
2.137 +
2.138 +lemma of_nat_sum_mset [simp]:
2.139 +  "of_nat (sum_mset A) = sum_mset (image_mset of_nat A)"
2.140 +  by (induction A) auto
2.141 +
2.142 +lemma size_eq_sum_mset:
2.143 +  "size M = (\<Sum>a\<in>#M. 1)"
2.144 +  using image_mset_const_eq [of "1::nat" M] by simp
2.145 +
2.146 +lemma size_mset_set [simp]:
2.147 +  "size (mset_set A) = card A"
2.148 +  by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
2.149
2.150  lemma sum_mset_constant [simp]:
2.151    fixes y :: "'b::semiring_1"
2.152    shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
2.153    by (induction A) (auto simp: algebra_simps)
2.154
2.156 -  assumes "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
2.157 -  shows "sum_mset (image_mset f K) \<le> sum_mset (image_mset g K)"
2.159 -
2.160 -lemma sum_mset_product:
2.161 -  fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
2.162 -  shows "(\<Sum>i \<in># A. f i) * (\<Sum>i \<in># B. g i) = (\<Sum>i\<in>#A. \<Sum>j\<in>#B. f i * g j)"
2.163 -  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
2.164 -
2.165  abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
2.166    where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
2.167      could likewise refer to \<open>\<Squnion>#\<close>\<close>
2.168 @@ -2347,6 +2371,7 @@
2.169  lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
2.170    by (induction M) auto
2.171
2.172 +
2.173  context comm_monoid_mult
2.174  begin
2.175
2.176 @@ -2365,6 +2390,10 @@
2.177    "prod_mset (A + B) = prod_mset A * prod_mset B"
2.178    by (fact prod_mset.union)
2.179
2.180 +lemma prod_mset_prod_list:
2.181 +  "prod_mset (mset xs) = prod_list xs"
2.182 +  by (induct xs) auto
2.183 +
2.184  lemma prod_mset_replicate_mset [simp]:
2.185    "prod_mset (replicate_mset n a) = a ^ n"
2.186    by (induct n) simp_all
2.187 @@ -2383,6 +2412,21 @@
2.188  lemma prod_mset_delta': "prod_mset (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
2.189    by (induction A) simp_all
2.190
2.191 +lemma prod_mset_subset_imp_dvd:
2.192 +  assumes "A \<subseteq># B"
2.193 +  shows   "prod_mset A dvd prod_mset B"
2.194 +proof -
2.195 +  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
2.196 +  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
2.197 +  also have "prod_mset A dvd \<dots>" by simp
2.198 +  finally show ?thesis .
2.199 +qed
2.200 +
2.201 +lemma dvd_prod_mset:
2.202 +  assumes "x \<in># A"
2.203 +  shows "x dvd prod_mset A"
2.204 +  using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
2.205 +
2.206  end
2.207
2.208  syntax (ASCII)
2.209 @@ -2395,21 +2439,6 @@
2.210  lemma prod_mset_constant [simp]: "(\<Prod>_\<in>#A. c) = c ^ size A"
2.212
2.213 -lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
2.214 -  assumes "A \<subseteq># B"
2.215 -  shows   "prod_mset A dvd prod_mset B"
2.216 -proof -
2.217 -  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
2.218 -  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
2.219 -  also have "prod_mset A dvd \<dots>" by simp
2.220 -  finally show ?thesis .
2.221 -qed
2.222 -
2.223 -lemma (in comm_monoid_mult) dvd_prod_mset:
2.224 -  assumes "x \<in># A"
2.225 -  shows "x dvd prod_mset A"
2.226 -  using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
2.227 -
2.228  lemma (in semidom) prod_mset_zero_iff [iff]:
2.229    "prod_mset A = 0 \<longleftrightarrow> 0 \<in># A"
2.230    by (induct A) auto
2.231 @@ -2445,9 +2474,6 @@
2.232    then show ?thesis by (simp add: normalize_prod_mset)
2.233  qed
2.234
2.235 -lemma prod_mset_prod_list: "prod_mset (mset xs) = prod_list xs"
2.236 -  by (induct xs) auto
2.237 -
2.238
2.239  subsection \<open>Alternative representations\<close>
2.240
```