src/HOL/Groups_Big.thy
 changeset 57418 6ab1c7cb0b8d parent 57275 0ddb5b755cdc child 57512 cc97b347b301
```     1.1 --- a/src/HOL/Groups_Big.thy	Fri Jun 27 22:08:55 2014 +0200
1.2 +++ b/src/HOL/Groups_Big.thy	Sat Jun 28 09:16:42 2014 +0200
1.3 @@ -87,6 +87,15 @@
1.4    shows "F g (A \<union> B) = F g A * F g B"
1.5    using assms by (simp add: union_inter_neutral)
1.6
1.7 +lemma union_diff2:
1.8 +  assumes "finite A" and "finite B"
1.9 +  shows "F g (A \<union> B) = F g (A - B) * F g (B - A) * F g (A \<inter> B)"
1.10 +proof -
1.11 +  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
1.12 +    by auto
1.13 +  with assms show ?thesis by simp (subst union_disjoint, auto)+
1.14 +qed
1.15 +
1.16  lemma subset_diff:
1.17    assumes "B \<subseteq> A" and "finite A"
1.18    shows "F g A = F g (A - B) * F g B"
1.19 @@ -139,6 +148,13 @@
1.20    shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
1.21    by (rule cong) (insert assms, simp_all add: simp_implies_def)
1.22
1.23 +lemma reindex_cong:
1.24 +  assumes "inj_on l B"
1.25 +  assumes "A = l ` B"
1.26 +  assumes "\<And>x. x \<in> B \<Longrightarrow> g (l x) = h x"
1.27 +  shows "F g A = F h B"
1.28 +  using assms by (simp add: reindex)
1.29 +
1.30  lemma UNION_disjoint:
1.31    assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
1.32    and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
1.33 @@ -156,7 +172,7 @@
1.34
1.35  lemma Union_disjoint:
1.36    assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
1.37 -  shows "F g (Union C) = F (F g) C"
1.38 +  shows "F g (Union C) = (F \<circ> F) g C"
1.39  proof cases
1.40    assume "finite C"
1.41    from UNION_disjoint [OF this assms]
1.42 @@ -257,6 +273,15 @@
1.43    qed simp
1.44  qed
1.45
1.46 +lemma reindex_nontrivial:
1.47 +  assumes "finite A"
1.48 +  and nz: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> h x = h y \<Longrightarrow> g (h x) = 1"
1.49 +  shows "F g (h ` A) = F (g \<circ> h) A"
1.50 +proof (subst reindex_bij_betw_not_neutral [symmetric])
1.51 +  show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = 1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = 1})"
1.52 +    using nz by (auto intro!: inj_onI simp: bij_betw_def)
1.53 +qed (insert `finite A`, auto)
1.54 +
1.55  lemma reindex_bij_witness_not_neutral:
1.56    assumes fin: "finite S'" "finite T'"
1.57    assumes witness:
1.58 @@ -336,6 +361,69 @@
1.59  apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
1.60  done
1.61
1.62 +lemma inter_restrict:
1.63 +  assumes "finite A"
1.64 +  shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else 1) A"
1.65 +proof -
1.66 +  let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else 1"
1.67 +  have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else 1) = 1"
1.68 +   by simp
1.69 +  moreover have "A \<inter> B \<subseteq> A" by blast
1.70 +  ultimately have "F ?g (A \<inter> B) = F ?g A" using `finite A`
1.71 +    by (intro mono_neutral_left) auto
1.72 +  then show ?thesis by simp
1.73 +qed
1.74 +
1.75 +lemma inter_filter:
1.76 +  "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else 1) A"
1.77 +  by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)
1.78 +
1.79 +lemma Union_comp:
1.80 +  assumes "\<forall>A \<in> B. finite A"
1.81 +    and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B  \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = 1"
1.82 +  shows "F g (\<Union>B) = (F \<circ> F) g B"
1.83 +using assms proof (induct B rule: infinite_finite_induct)
1.84 +  case (infinite A)
1.85 +  then have "\<not> finite (\<Union>A)" by (blast dest: finite_UnionD)
1.86 +  with infinite show ?case by simp
1.87 +next
1.88 +  case empty then show ?case by simp
1.89 +next
1.90 +  case (insert A B)
1.91 +  then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B"
1.92 +    and "\<forall>x\<in>A \<inter> \<Union>B. g x = 1"
1.93 +    and H: "F g (\<Union>B) = (F o F) g B" by auto
1.94 +  then have "F g (A \<union> \<Union>B) = F g A * F g (\<Union>B)"
1.95 +    by (simp add: union_inter_neutral)
1.96 +  with `finite B` `A \<notin> B` show ?case
1.97 +    by (simp add: H)
1.98 +qed
1.99 +
1.100 +lemma commute:
1.101 +  "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
1.102 +  unfolding cartesian_product
1.103 +  by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto
1.104 +
1.105 +lemma commute_restrict:
1.106 +  "finite A \<Longrightarrow> finite B \<Longrightarrow>
1.107 +    F (\<lambda>x. F (g x) {y. y \<in> B \<and> R x y}) A = F (\<lambda>y. F (\<lambda>x. g x y) {x. x \<in> A \<and> R x y}) B"
1.108 +  by (simp add: inter_filter) (rule commute)
1.109 +
1.110 +lemma Plus:
1.111 +  fixes A :: "'b set" and B :: "'c set"
1.112 +  assumes fin: "finite A" "finite B"
1.113 +  shows "F g (A <+> B) = F (g \<circ> Inl) A * F (g \<circ> Inr) B"
1.114 +proof -
1.115 +  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
1.116 +  moreover from fin have "finite (Inl ` A :: ('b + 'c) set)" "finite (Inr ` B :: ('b + 'c) set)"
1.117 +    by auto
1.118 +  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('b + 'c) set)" by auto
1.119 +  moreover have "inj_on (Inl :: 'b \<Rightarrow> 'b + 'c) A" "inj_on (Inr :: 'c \<Rightarrow> 'b + 'c) B"
1.120 +    by (auto intro: inj_onI)
1.121 +  ultimately show ?thesis using fin
1.122 +    by (simp add: union_disjoint reindex)
1.123 +qed
1.124 +
1.125  end
1.126
1.127  notation times (infixl "*" 70)
1.128 @@ -410,191 +498,27 @@
1.129  in [(@{const_syntax setsum}, K setsum_tr')] end
1.130  *}
1.131
1.132 -text {* TODO These are candidates for generalization *}
1.133 -
1.135 -begin
1.136 -
1.137 -lemma setsum_reindex_id:
1.138 -  "inj_on f B \<Longrightarrow> setsum f B = setsum id (f ` B)"
1.139 -  by (simp add: setsum.reindex)
1.140 -
1.141 -lemma setsum_reindex_nonzero:
1.142 -  assumes fS: "finite S"
1.143 -  and nz: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
1.144 -  shows "setsum h (f ` S) = setsum (h \<circ> f) S"
1.145 -proof (subst setsum.reindex_bij_betw_not_neutral[symmetric])
1.146 -  show "bij_betw f (S - {x\<in>S. h (f x) = 0}) (f`S - f`{x\<in>S. h (f x) = 0})"
1.147 -    using nz by (auto intro!: inj_onI simp: bij_betw_def)
1.148 -qed (insert fS, auto)
1.149 -
1.150 -lemma setsum_cong2:
1.151 -  "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
1.152 -  by (auto intro: setsum.cong)
1.153 -
1.154 -lemma setsum_reindex_cong:
1.155 -   "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|]
1.156 -    ==> setsum h B = setsum g A"
1.157 -  by (simp add: setsum.reindex)
1.158 -
1.159 -lemma setsum_restrict_set:
1.160 -  assumes fA: "finite A"
1.161 -  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
1.162 -proof-
1.163 -  from fA have fab: "finite (A \<inter> B)" by auto
1.164 -  have aba: "A \<inter> B \<subseteq> A" by blast
1.165 -  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
1.166 -  from setsum.mono_neutral_left [OF fA aba, of ?g]
1.167 -  show ?thesis by simp
1.168 -qed
1.169 +text {* TODO generalization candidates *}
1.170
1.171 -lemma setsum_Union_disjoint:
1.172 -  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
1.173 -  shows "setsum f (Union C) = setsum (setsum f) C"
1.174 -  using assms by (fact setsum.Union_disjoint)
1.175 -
1.176 -lemma setsum_cartesian_product:
1.177 -  "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
1.178 -  by (fact setsum.cartesian_product)
1.179 -
1.180 -lemma setsum_UNION_zero:
1.181 -  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
1.182 -  and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
1.183 -  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
1.184 -  using fSS f0
1.185 -proof(induct rule: finite_induct[OF fS])
1.186 -  case 1 thus ?case by simp
1.187 -next
1.188 -  case (2 T F)
1.189 -  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F"
1.190 -    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
1.191 -  from fTF have fUF: "finite (\<Union>F)" by auto
1.192 -  from "2.prems" TF fTF
1.193 -  show ?case
1.194 -    by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f])
1.195 -qed
1.196 -
1.197 -text {* Commuting outer and inner summation *}
1.198 -
1.199 -lemma setsum_commute:
1.200 -  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
1.201 -  unfolding setsum_cartesian_product
1.202 -  by (rule setsum.reindex_bij_witness[where i="\<lambda>(i, j). (j, i)" and j="\<lambda>(i, j). (j, i)"]) auto
1.203 -
1.204 -lemma setsum_Plus:
1.205 -  fixes A :: "'a set" and B :: "'b set"
1.206 -  assumes fin: "finite A" "finite B"
1.207 -  shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
1.208 -proof -
1.209 -  have "A <+> B = Inl ` A \<union> Inr ` B" by auto
1.210 -  moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
1.211 -    by auto
1.212 -  moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
1.213 -  moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
1.214 -  ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex)
1.215 +lemma setsum_image_gen:
1.216 +  assumes fS: "finite S"
1.217 +  shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
1.218 +proof-
1.219 +  { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto }
1.220 +  hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
1.221 +    by simp
1.222 +  also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
1.223 +    by (rule setsum.commute_restrict [OF fS finite_imageI [OF fS]])
1.224 +  finally show ?thesis .
1.225  qed
1.226
1.227 -end
1.228 -
1.229 -text {* TODO These are legacy *}
1.230 -
1.231 -lemma setsum_empty:
1.232 -  "setsum f {} = 0"
1.233 -  by (fact setsum.empty)
1.234 -
1.235 -lemma setsum_insert:
1.236 -  "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
1.237 -  by (fact setsum.insert)
1.238 -
1.239 -lemma setsum_infinite:
1.240 -  "~ finite A ==> setsum f A = 0"
1.241 -  by (fact setsum.infinite)
1.242 -
1.243 -lemma setsum_reindex:
1.244 -  "inj_on f B \<Longrightarrow> setsum h (f ` B) = setsum (h \<circ> f) B"
1.245 -  by (fact setsum.reindex)
1.246 -
1.247 -lemma setsum_cong:
1.248 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
1.249 -  by (fact setsum.cong)
1.250 -
1.251 -lemma strong_setsum_cong:
1.252 -  "A = B ==> (!!x. x:B =simp=> f x = g x)
1.253 -   ==> setsum (%x. f x) A = setsum (%x. g x) B"
1.254 -  by (fact setsum.strong_cong)
1.255 -
1.256 -lemmas setsum_0 = setsum.neutral_const
1.257 -lemmas setsum_0' = setsum.neutral
1.258 -
1.259 -lemma setsum_Un_Int: "finite A ==> finite B ==>
1.260 -  setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
1.261 -  -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
1.262 -  by (fact setsum.union_inter)
1.263 -
1.264 -lemma setsum_Un_disjoint: "finite A ==> finite B
1.265 -  ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
1.266 -  by (fact setsum.union_disjoint)
1.267 -
1.268 -lemma setsum_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
1.269 -    setsum f A = setsum f (A - B) + setsum f B"
1.270 -  by (fact setsum.subset_diff)
1.271 -
1.272 -lemma setsum_mono_zero_left:
1.273 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 0 \<rbrakk> \<Longrightarrow> setsum f S = setsum f T"
1.274 -  by (fact setsum.mono_neutral_left)
1.275 -
1.276 -lemmas setsum_mono_zero_right = setsum.mono_neutral_right
1.277 -
1.278 -lemma setsum_mono_zero_cong_left:
1.279 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
1.280 -  \<Longrightarrow> setsum f S = setsum g T"
1.281 -  by (fact setsum.mono_neutral_cong_left)
1.282 -
1.283 -lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right
1.284 -
1.285 -lemma setsum_delta: "finite S \<Longrightarrow>
1.286 -  setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
1.287 -  by (fact setsum.delta)
1.288 -
1.289 -lemma setsum_delta': "finite S \<Longrightarrow>
1.290 -  setsum (\<lambda>k. if a = k then b k else 0) S = (if a\<in> S then b a else 0)"
1.291 -  by (fact setsum.delta')
1.292 -
1.293 -lemma setsum_cases:
1.294 -  assumes "finite A"
1.295 -  shows "setsum (\<lambda>x. if P x then f x else g x) A =
1.296 -         setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
1.297 -  using assms by (fact setsum.If_cases)
1.298 -
1.299 -(*But we can't get rid of finite I. If infinite, although the rhs is 0,
1.300 -  the lhs need not be, since UNION I A could still be finite.*)
1.301 -lemma setsum_UN_disjoint:
1.302 -  assumes "finite I" and "ALL i:I. finite (A i)"
1.303 -    and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
1.304 -  shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
1.305 -  using assms by (fact setsum.UNION_disjoint)
1.306 -
1.307 -(*But we can't get rid of finite A. If infinite, although the lhs is 0,
1.308 -  the rhs need not be, since SIGMA A B could still be finite.*)
1.309 -lemma setsum_Sigma:
1.310 -  assumes "finite A" and  "ALL x:A. finite (B x)"
1.311 -  shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1.312 -  using assms by (fact setsum.Sigma)
1.313 -
1.314 -lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
1.315 -  by (fact setsum.distrib)
1.316 -
1.317 -lemma setsum_Un_zero:
1.318 -  "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 0 \<rbrakk> \<Longrightarrow>
1.319 -  setsum f (S \<union> T) = setsum f S + setsum f T"
1.320 -  by (fact setsum.union_inter_neutral)
1.321
1.322  subsubsection {* Properties in more restricted classes of structures *}
1.323
1.324  lemma setsum_Un: "finite A ==> finite B ==>
1.325    (setsum f (A Un B) :: 'a :: ab_group_add) =
1.326     setsum f A + setsum f B - setsum f (A Int B)"
1.327 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
1.328 +by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
1.329
1.330  lemma setsum_Un2:
1.331    assumes "finite (A \<union> B)"
1.332 @@ -602,7 +526,7 @@
1.333  proof -
1.334    have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
1.335      by auto
1.336 -  with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
1.337 +  with assms show ?thesis by simp (subst setsum.union_disjoint, auto)+
1.338  qed
1.339
1.340  lemma setsum_diff1: "finite A \<Longrightarrow>
1.341 @@ -664,12 +588,12 @@
1.342    have "setsum f A = setsum f ((A-{a}) \<union> {a})"
1.344    also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
1.345 -    using `finite A` by(subst setsum_Un_disjoint) auto
1.346 +    using `finite A` by(subst setsum.union_disjoint) auto
1.347    also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
1.349    also have "setsum f {a} < setsum g {a}" using a by simp
1.350    also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
1.351 -    using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
1.352 +    using `finite A` by(subst setsum.union_disjoint[symmetric]) auto
1.353    also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
1.355  qed
1.356 @@ -685,7 +609,7 @@
1.357  lemma setsum_subtractf:
1.358    "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
1.359      setsum f A - setsum g A"
1.360 -  using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
1.361 +  using setsum.distrib [of f "- g" A] by (simp add: setsum_negf)
1.362
1.363  lemma setsum_nonneg:
1.365 @@ -747,11 +671,32 @@
1.366    have "setsum f A \<le> setsum f A + setsum f (B-A)"
1.368    also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
1.369 -    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
1.370 +    by (simp add: setsum.union_disjoint del:Un_Diff_cancel)
1.371    also have "A \<union> (B-A) = B" using sub by blast
1.372    finally show ?thesis .
1.373  qed
1.374
1.375 +lemma setsum_le_included:
1.376 +  fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
1.377 +  assumes "finite s" "finite t"
1.378 +  and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
1.379 +  shows "setsum f s \<le> setsum g t"
1.380 +proof -
1.381 +  have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
1.382 +  proof (rule setsum_mono)
1.383 +    fix y assume "y \<in> s"
1.384 +    with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
1.385 +    with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
1.386 +      using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
1.387 +      by (auto intro!: setsum_mono2)
1.388 +  qed
1.389 +  also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
1.390 +    using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
1.391 +  also have "... \<le> setsum g t"
1.392 +    using assms by (auto simp: setsum_image_gen[symmetric])
1.393 +  finally show ?thesis .
1.394 +qed
1.395 +
1.396  lemma setsum_mono3: "finite B ==> A <= B ==>
1.397      ALL x: B - A.
1.399 @@ -762,7 +707,7 @@
1.400    apply simp
1.402    apply (erule setsum_nonneg)
1.403 -  apply (subst setsum_Un_disjoint [THEN sym])
1.404 +  apply (subst setsum.union_disjoint [THEN sym])
1.405    apply (erule finite_subset, assumption)
1.406    apply (rule finite_subset)
1.407    prefer 2
1.408 @@ -865,27 +810,21 @@
1.409    case False thus ?thesis by simp
1.410  qed
1.411
1.412 -lemma setsum_diff1'[rule_format]:
1.413 -  "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
1.414 -apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
1.416 -done
1.417 -
1.418  lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
1.419    shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
1.420 -unfolding setsum_diff1'[OF assms] by auto
1.421 +  unfolding setsum.remove [OF assms] by auto
1.422
1.423  lemma setsum_product:
1.424    fixes f :: "'a => ('b::semiring_0)"
1.425    shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
1.426 -  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
1.427 +  by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute)
1.428
1.429  lemma setsum_mult_setsum_if_inj:
1.430  fixes f :: "'a => ('b::semiring_0)"
1.431  shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
1.432    setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
1.433 -by(auto simp: setsum_product setsum_cartesian_product
1.434 -        intro!:  setsum_reindex_cong[symmetric])
1.435 +by(auto simp: setsum_product setsum.cartesian_product
1.436 +        intro!:  setsum.reindex_cong[symmetric])
1.437
1.438  lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
1.439  apply (case_tac "finite A")
1.440 @@ -909,7 +848,7 @@
1.441  lemma setsum_Un_nat: "finite A ==> finite B ==>
1.442    (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
1.443    -- {* For the natural numbers, we have subtraction. *}
1.444 -by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
1.445 +by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
1.446
1.447  lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
1.448    (if a:A then setsum f A - f a else setsum f A)"
1.449 @@ -993,7 +932,7 @@
1.450    shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
1.451  proof -
1.452    have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
1.453 -  with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
1.454 +  with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant)
1.455  qed
1.456
1.457  lemma card_Union_disjoint:
1.458 @@ -1004,13 +943,32 @@
1.459  apply simp_all
1.460  done
1.461
1.462 +lemma setsum_multicount_gen:
1.463 +  assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
1.464 +  shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
1.465 +proof-
1.466 +  have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
1.467 +  also have "\<dots> = ?r" unfolding setsum.commute_restrict [OF assms(1-2)]
1.468 +    using assms(3) by auto
1.469 +  finally show ?thesis .
1.470 +qed
1.471 +
1.472 +lemma setsum_multicount:
1.473 +  assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
1.474 +  shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
1.475 +proof-
1.476 +  have "?l = setsum (\<lambda>i. k) T" by (rule setsum_multicount_gen) (auto simp: assms)
1.477 +  also have "\<dots> = ?r" by (simp add: mult_commute)
1.478 +  finally show ?thesis by auto
1.479 +qed
1.480 +
1.481
1.482  subsubsection {* Cardinality of products *}
1.483
1.484  lemma card_SigmaI [simp]:
1.485    "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
1.486    \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
1.487 -by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
1.488 +by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant)
1.489
1.490  (*
1.491  lemma SigmaI_insert: "y \<notin> A ==>
1.492 @@ -1075,124 +1033,6 @@
1.493    "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
1.494    "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
1.495
1.496 -text {* TODO These are candidates for generalization *}
1.497 -
1.498 -context comm_monoid_mult
1.499 -begin
1.500 -
1.501 -lemma setprod_reindex_id:
1.502 -  "inj_on f B ==> setprod f B = setprod id (f ` B)"
1.503 -  by (auto simp add: setprod.reindex)
1.504 -
1.505 -lemma setprod_reindex_cong:
1.506 -  "inj_on f A ==> B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
1.507 -  by (frule setprod.reindex, simp)
1.508 -
1.509 -lemma strong_setprod_reindex_cong:
1.510 -  "inj_on f A \<Longrightarrow> B = f ` A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x) \<Longrightarrow> setprod h B = setprod g A"
1.511 -  by (subst setprod.reindex_bij_betw[symmetric, where h=f])
1.512 -     (auto simp: bij_betw_def)
1.513 -
1.514 -lemma setprod_Union_disjoint:
1.515 -  assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
1.516 -  shows "setprod f (Union C) = setprod (setprod f) C"
1.517 -  using assms by (fact setprod.Union_disjoint)
1.518 -
1.519 -text{*Here we can eliminate the finiteness assumptions, by cases.*}
1.520 -lemma setprod_cartesian_product:
1.521 -  "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
1.522 -  by (fact setprod.cartesian_product)
1.523 -
1.524 -lemma setprod_Un2:
1.525 -  assumes "finite (A \<union> B)"
1.526 -  shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
1.527 -proof -
1.528 -  have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
1.529 -    by auto
1.530 -  with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+
1.531 -qed
1.532 -
1.533 -end
1.534 -
1.535 -text {* TODO These are legacy *}
1.536 -
1.537 -lemma setprod_empty: "setprod f {} = 1"
1.538 -  by (fact setprod.empty)
1.539 -
1.540 -lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
1.541 -    setprod f (insert a A) = f a * setprod f A"
1.542 -  by (fact setprod.insert)
1.543 -
1.544 -lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
1.545 -  by (fact setprod.infinite)
1.546 -
1.547 -lemma setprod_reindex:
1.548 -  "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
1.549 -  by (fact setprod.reindex)
1.550 -
1.551 -lemma setprod_cong:
1.552 -  "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
1.553 -  by (fact setprod.cong)
1.554 -
1.555 -lemma strong_setprod_cong:
1.556 -  "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
1.557 -  by (fact setprod.strong_cong)
1.558 -
1.559 -lemma setprod_Un_one:
1.560 -  "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
1.561 -  \<Longrightarrow> setprod f (S \<union> T) = setprod f S  * setprod f T"
1.562 -  by (fact setprod.union_inter_neutral)
1.563 -
1.564 -lemmas setprod_1 = setprod.neutral_const
1.565 -lemmas setprod_1' = setprod.neutral
1.566 -
1.567 -lemma setprod_Un_Int: "finite A ==> finite B
1.568 -    ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
1.569 -  by (fact setprod.union_inter)
1.570 -
1.571 -lemma setprod_Un_disjoint: "finite A ==> finite B
1.572 -  ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
1.573 -  by (fact setprod.union_disjoint)
1.574 -
1.575 -lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
1.576 -    setprod f A = setprod f (A - B) * setprod f B"
1.577 -  by (fact setprod.subset_diff)
1.578 -
1.579 -lemma setprod_mono_one_left:
1.580 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
1.581 -  by (fact setprod.mono_neutral_left)
1.582 -
1.583 -lemmas setprod_mono_one_right = setprod.mono_neutral_right
1.584 -
1.585 -lemma setprod_mono_one_cong_left:
1.586 -  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
1.587 -  \<Longrightarrow> setprod f S = setprod g T"
1.588 -  by (fact setprod.mono_neutral_cong_left)
1.589 -
1.590 -lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right
1.591 -
1.592 -lemma setprod_delta: "finite S \<Longrightarrow>
1.593 -  setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
1.594 -  by (fact setprod.delta)
1.595 -
1.596 -lemma setprod_delta': "finite S \<Longrightarrow>
1.597 -  setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
1.598 -  by (fact setprod.delta')
1.599 -
1.600 -lemma setprod_UN_disjoint:
1.601 -    "finite I ==> (ALL i:I. finite (A i)) ==>
1.602 -        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.603 -      setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1.604 -  by (fact setprod.UNION_disjoint)
1.605 -
1.606 -lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1.607 -    (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
1.608 -    (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
1.609 -  by (fact setprod.Sigma)
1.610 -
1.611 -lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A = setprod f A * setprod g A"
1.612 -  by (fact setprod.distrib)
1.613 -
1.614
1.615  subsubsection {* Properties in more restricted classes of structures *}
1.616
1.617 @@ -1210,7 +1050,7 @@
1.618  lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
1.619    (setprod f (A Un B) :: 'a ::{field})
1.620     = setprod f A * setprod f B / setprod f (A Int B)"
1.621 -by (subst setprod_Un_Int [symmetric], auto)
1.622 +by (subst setprod.union_inter [symmetric], auto)
1.623
1.624  lemma setprod_nonneg [rule_format]:
1.625     "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
1.626 @@ -1238,9 +1078,9 @@
1.627           "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
1.628  apply (erule ssubst)
1.629  apply (subst divide_inverse)
1.630 -apply (subst setprod_timesf)
1.631 +apply (subst setprod.distrib)
1.632  apply (subst setprod_inversef, assumption+, rule refl)
1.633 -apply (rule setprod_cong, rule refl)
1.634 +apply (rule setprod.cong, rule refl)
1.635  apply (subst divide_inverse, auto)
1.636  done
1.637
1.638 @@ -1257,8 +1097,8 @@
1.639    "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
1.640    apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
1.641    apply (unfold dvd_def, blast)
1.642 -  apply (subst setprod_Un_disjoint [symmetric])
1.643 -  apply (auto elim: finite_subset intro: setprod_cong)
1.644 +  apply (subst setprod.union_disjoint [symmetric])
1.645 +  apply (auto elim: finite_subset intro: setprod.cong)
1.646  done
1.647
1.648  lemma setprod_dvd_setprod_subset2:
1.649 @@ -1290,7 +1130,7 @@
1.650    proof (induct A rule: finite_subset_induct)
1.651      case (insert a F)
1.652      thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
1.653 -      unfolding setprod_insert[OF insert(1,3)]
1.654 +      unfolding setprod.insert[OF insert(1,3)]
1.655        using assms[rule_format,OF insert(2)] insert
1.656        by (auto intro: mult_mono)
1.657    qed auto
```