src/HOL/Library/Multiset.thy
changeset 66938 c78ff0aeba4c
parent 66494 8645dc296dca
child 67051 e7e54a0b9197
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Oct 30 13:18:44 2017 +0000
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Oct 30 13:18:44 2017 +0000
     1.3 @@ -2247,52 +2247,12 @@
     1.4  sublocale sum_mset: comm_monoid_mset plus 0
     1.5    defines sum_mset = sum_mset.F ..
     1.6  
     1.7 -lemma (in semiring_1) sum_mset_replicate_mset [simp]:
     1.8 -  "sum_mset (replicate_mset n a) = of_nat n * a"
     1.9 -  by (induct n) (simp_all add: algebra_simps)
    1.10 -
    1.11  lemma sum_unfold_sum_mset:
    1.12    "sum f A = sum_mset (image_mset f (mset_set A))"
    1.13    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    1.14  
    1.15 -lemma sum_mset_delta: "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * count A y"
    1.16 -  by (induction A) simp_all
    1.17 -
    1.18 -lemma sum_mset_delta': "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * count A y"
    1.19 -  by (induction A) simp_all
    1.20 -
    1.21  end
    1.22  
    1.23 -lemma of_nat_sum_mset [simp]:
    1.24 -  "of_nat (sum_mset M) = sum_mset (image_mset of_nat M)"
    1.25 -by (induction M) auto
    1.26 -
    1.27 -lemma sum_mset_0_iff [simp]:
    1.28 -  "sum_mset M = (0::'a::canonically_ordered_monoid_add)
    1.29 -   \<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
    1.30 -by(induction M) auto
    1.31 -
    1.32 -lemma sum_mset_diff:
    1.33 -  fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
    1.34 -  shows "N \<subseteq># M \<Longrightarrow> sum_mset (M - N) = sum_mset M - sum_mset N"
    1.35 -  by (metis add_diff_cancel_right' sum_mset.union subset_mset.diff_add)
    1.36 -
    1.37 -lemma size_eq_sum_mset: "size M = sum_mset (image_mset (\<lambda>_. 1) M)"
    1.38 -proof (induct M)
    1.39 -  case empty then show ?case by simp
    1.40 -next
    1.41 -  case (add x M) then show ?case
    1.42 -    by (cases "x \<in> set_mset M")
    1.43 -      (simp_all add: size_multiset_overloaded_eq not_in_iff sum.If_cases Diff_eq[symmetric]
    1.44 -        sum.remove)
    1.45 -qed
    1.46 -
    1.47 -lemma size_mset_set [simp]: "size (mset_set A) = card A"
    1.48 -by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
    1.49 -
    1.50 -lemma sum_mset_sum_list: "sum_mset (mset xs) = sum_list xs"
    1.51 -  by (induction xs) auto
    1.52 -
    1.53  syntax (ASCII)
    1.54    "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
    1.55  syntax
    1.56 @@ -2300,31 +2260,95 @@
    1.57  translations
    1.58    "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST sum_mset (CONST image_mset (\<lambda>i. b) A)"
    1.59  
    1.60 +context comm_monoid_add
    1.61 +begin
    1.62 +
    1.63 +lemma sum_mset_sum_list:
    1.64 +  "sum_mset (mset xs) = sum_list xs"
    1.65 +  by (induction xs) auto
    1.66 +
    1.67 +end
    1.68 +
    1.69 +context canonically_ordered_monoid_add
    1.70 +begin
    1.71 +
    1.72 +lemma sum_mset_0_iff [simp]:
    1.73 +  "sum_mset M = 0  \<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
    1.74 +  by (induction M) auto
    1.75 +
    1.76 +end
    1.77 +
    1.78 +context ordered_comm_monoid_add
    1.79 +begin
    1.80 +
    1.81 +lemma sum_mset_mono:
    1.82 +  "sum_mset (image_mset f K) \<le> sum_mset (image_mset g K)"
    1.83 +  if "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
    1.84 +  using that by (induction K) (simp_all add: add_mono)
    1.85 +
    1.86 +end
    1.87 +
    1.88 +context ordered_cancel_comm_monoid_diff
    1.89 +begin
    1.90 +
    1.91 +lemma sum_mset_diff:
    1.92 +  "sum_mset (M - N) = sum_mset M - sum_mset N" if "N \<subseteq># M" for M N :: "'a multiset"
    1.93 +  using that by (auto simp add: subset_mset.le_iff_add)
    1.94 +
    1.95 +end
    1.96 +
    1.97 +context semiring_0
    1.98 +begin
    1.99 +
   1.100  lemma sum_mset_distrib_left:
   1.101 -  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   1.102 -  shows "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
   1.103 -by (induction M) (simp_all add: distrib_left)
   1.104 +  "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
   1.105 +  by (induction M) (simp_all add: algebra_simps)
   1.106  
   1.107  lemma sum_mset_distrib_right:
   1.108 -  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   1.109 -  shows "(\<Sum>b \<in># B. f b) * a = (\<Sum>b \<in># B. f b * a)"
   1.110 -  by (induction B) (auto simp: distrib_right)
   1.111 +  "(\<Sum>x \<in># M. f x) * c = (\<Sum>x \<in># M. f x * c)"
   1.112 +  by (induction M) (simp_all add: algebra_simps)
   1.113 +
   1.114 +end
   1.115 +
   1.116 +lemma sum_mset_product:
   1.117 +  fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
   1.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)"
   1.119 +  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
   1.120 +
   1.121 +context semiring_1
   1.122 +begin
   1.123 +
   1.124 +lemma sum_mset_replicate_mset [simp]:
   1.125 +  "sum_mset (replicate_mset n a) = of_nat n * a"
   1.126 +  by (induction n) (simp_all add: algebra_simps)
   1.127 +
   1.128 +lemma sum_mset_delta:
   1.129 +  "sum_mset (image_mset (\<lambda>x. if x = y then c else 0) A) = c * of_nat (count A y)"
   1.130 +  by (induction A) (simp_all add: algebra_simps)
   1.131 +
   1.132 +lemma sum_mset_delta':
   1.133 +  "sum_mset (image_mset (\<lambda>x. if y = x then c else 0) A) = c * of_nat (count A y)"
   1.134 +  by (induction A) (simp_all add: algebra_simps)
   1.135 +
   1.136 +end
   1.137 +
   1.138 +lemma of_nat_sum_mset [simp]:
   1.139 +  "of_nat (sum_mset A) = sum_mset (image_mset of_nat A)"
   1.140 +  by (induction A) auto
   1.141 +
   1.142 +lemma size_eq_sum_mset:
   1.143 +  "size M = (\<Sum>a\<in>#M. 1)"
   1.144 +  using image_mset_const_eq [of "1::nat" M] by simp
   1.145 +
   1.146 +lemma size_mset_set [simp]:
   1.147 +  "size (mset_set A) = card A"
   1.148 +  by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
   1.149  
   1.150  lemma sum_mset_constant [simp]:
   1.151    fixes y :: "'b::semiring_1"
   1.152    shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
   1.153    by (induction A) (auto simp: algebra_simps)
   1.154  
   1.155 -lemma (in ordered_comm_monoid_add) sum_mset_mono:
   1.156 -  assumes "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
   1.157 -  shows "sum_mset (image_mset f K) \<le> sum_mset (image_mset g K)"
   1.158 -  using assms by (induction K) (simp_all add: local.add_mono)
   1.159 -
   1.160 -lemma sum_mset_product:
   1.161 -  fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
   1.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)"
   1.163 -  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
   1.164 -
   1.165  abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
   1.166    where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
   1.167      could likewise refer to \<open>\<Squnion>#\<close>\<close>
   1.168 @@ -2347,6 +2371,7 @@
   1.169  lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
   1.170    by (induction M) auto
   1.171  
   1.172 +
   1.173  context comm_monoid_mult
   1.174  begin
   1.175  
   1.176 @@ -2365,6 +2390,10 @@
   1.177    "prod_mset (A + B) = prod_mset A * prod_mset B"
   1.178    by (fact prod_mset.union)
   1.179  
   1.180 +lemma prod_mset_prod_list:
   1.181 +  "prod_mset (mset xs) = prod_list xs"
   1.182 +  by (induct xs) auto
   1.183 +
   1.184  lemma prod_mset_replicate_mset [simp]:
   1.185    "prod_mset (replicate_mset n a) = a ^ n"
   1.186    by (induct n) simp_all
   1.187 @@ -2383,6 +2412,21 @@
   1.188  lemma prod_mset_delta': "prod_mset (image_mset (\<lambda>x. if y = x then c else 1) A) = c ^ count A y"
   1.189    by (induction A) simp_all
   1.190  
   1.191 +lemma prod_mset_subset_imp_dvd:
   1.192 +  assumes "A \<subseteq># B"
   1.193 +  shows   "prod_mset A dvd prod_mset B"
   1.194 +proof -
   1.195 +  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
   1.196 +  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
   1.197 +  also have "prod_mset A dvd \<dots>" by simp
   1.198 +  finally show ?thesis .
   1.199 +qed
   1.200 +
   1.201 +lemma dvd_prod_mset:
   1.202 +  assumes "x \<in># A"
   1.203 +  shows "x dvd prod_mset A"
   1.204 +  using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
   1.205 +
   1.206  end
   1.207  
   1.208  syntax (ASCII)
   1.209 @@ -2395,21 +2439,6 @@
   1.210  lemma prod_mset_constant [simp]: "(\<Prod>_\<in>#A. c) = c ^ size A"
   1.211    by (simp add: image_mset_const_eq)
   1.212  
   1.213 -lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
   1.214 -  assumes "A \<subseteq># B"
   1.215 -  shows   "prod_mset A dvd prod_mset B"
   1.216 -proof -
   1.217 -  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
   1.218 -  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
   1.219 -  also have "prod_mset A dvd \<dots>" by simp
   1.220 -  finally show ?thesis .
   1.221 -qed
   1.222 -
   1.223 -lemma (in comm_monoid_mult) dvd_prod_mset:
   1.224 -  assumes "x \<in># A"
   1.225 -  shows "x dvd prod_mset A"
   1.226 -  using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
   1.227 -
   1.228  lemma (in semidom) prod_mset_zero_iff [iff]:
   1.229    "prod_mset A = 0 \<longleftrightarrow> 0 \<in># A"
   1.230    by (induct A) auto
   1.231 @@ -2445,9 +2474,6 @@
   1.232    then show ?thesis by (simp add: normalize_prod_mset)
   1.233  qed
   1.234  
   1.235 -lemma prod_mset_prod_list: "prod_mset (mset xs) = prod_list xs"
   1.236 -  by (induct xs) auto
   1.237 -
   1.238  
   1.239  subsection \<open>Alternative representations\<close>
   1.240