generalized some lemmas on multisets
authorhaftmann
Mon Oct 30 13:18:44 2017 +0000 (18 months ago)
changeset 66938c78ff0aeba4c
parent 66937 a1a4a5e2933a
child 66940 e5776e8e152b
child 66942 91a21a5631ae
generalized some lemmas on multisets
src/HOL/Computational_Algebra/Factorial_Ring.thy
src/HOL/Library/Multiset.thy
     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.35 -  by (metis add_diff_cancel_right' sum_mset.union subset_mset.diff_add)
    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.43 -      (simp_all add: size_multiset_overloaded_eq not_in_iff sum.If_cases Diff_eq[symmetric]
    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.60 +context comm_monoid_add
    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.69 +context canonically_ordered_monoid_add
    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.78 +context ordered_comm_monoid_add
    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.84 +  using that by (induction K) (simp_all add: add_mono)
    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.93 +  using that by (auto simp add: subset_mset.le_iff_add)
    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.155 -lemma (in ordered_comm_monoid_add) sum_mset_mono:
   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.158 -  using assms by (induction K) (simp_all add: local.add_mono)
   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.211    by (simp add: image_mset_const_eq)
   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