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.134 -context comm_monoid_add
   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.343      by(simp add:insert_absorb[OF `a: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.348      by(rule setsum_mono)(simp add: assms(2))
   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.354    finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
   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.364    assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   1.365 @@ -747,11 +671,32 @@
   1.366    have "setsum f A \<le> setsum f A + setsum f (B-A)"
   1.367      by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   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.398        0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   1.399 @@ -762,7 +707,7 @@
   1.400    apply simp
   1.401    apply (rule add_left_mono)
   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.415 -apply (auto simp add: insert_Diff_if add_ac)
   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