src/HOL/Groups_Big.thy
author haftmann
Mon Nov 17 14:55:34 2014 +0100 (2014-11-17)
changeset 59010 ec2b4270a502
parent 58889 5b7a9633cfa8
child 59416 fde2659085e1
permissions -rw-r--r--
generalized lemmas and tuned proofs
     1 (*  Title:      HOL/Groups_Big.thy
     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3                 with contributions by Jeremy Avigad
     4 *)
     5 
     6 section {* Big sum and product over finite (non-empty) sets *}
     7 
     8 theory Groups_Big
     9 imports Finite_Set
    10 begin
    11 
    12 subsection {* Generic monoid operation over a set *}
    13 
    14 no_notation times (infixl "*" 70)
    15 no_notation Groups.one ("1")
    16 
    17 locale comm_monoid_set = comm_monoid
    18 begin
    19 
    20 interpretation comp_fun_commute f
    21   by default (simp add: fun_eq_iff left_commute)
    22 
    23 interpretation comp?: comp_fun_commute "f \<circ> g"
    24   by (fact comp_comp_fun_commute)
    25 
    26 definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    27 where
    28   eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
    29 
    30 lemma infinite [simp]:
    31   "\<not> finite A \<Longrightarrow> F g A = 1"
    32   by (simp add: eq_fold)
    33 
    34 lemma empty [simp]:
    35   "F g {} = 1"
    36   by (simp add: eq_fold)
    37 
    38 lemma insert [simp]:
    39   assumes "finite A" and "x \<notin> A"
    40   shows "F g (insert x A) = g x * F g A"
    41   using assms by (simp add: eq_fold)
    42 
    43 lemma remove:
    44   assumes "finite A" and "x \<in> A"
    45   shows "F g A = g x * F g (A - {x})"
    46 proof -
    47   from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
    48     by (auto dest: mk_disjoint_insert)
    49   moreover from `finite A` A have "finite B" by simp
    50   ultimately show ?thesis by simp
    51 qed
    52 
    53 lemma insert_remove:
    54   assumes "finite A"
    55   shows "F g (insert x A) = g x * F g (A - {x})"
    56   using assms by (cases "x \<in> A") (simp_all add: remove insert_absorb)
    57 
    58 lemma neutral:
    59   assumes "\<forall>x\<in>A. g x = 1"
    60   shows "F g A = 1"
    61   using assms by (induct A rule: infinite_finite_induct) simp_all
    62 
    63 lemma neutral_const [simp]:
    64   "F (\<lambda>_. 1) A = 1"
    65   by (simp add: neutral)
    66 
    67 lemma union_inter:
    68   assumes "finite A" and "finite B"
    69   shows "F g (A \<union> B) * F g (A \<inter> B) = F g A * F g B"
    70   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    71 using assms proof (induct A)
    72   case empty then show ?case by simp
    73 next
    74   case (insert x A) then show ?case
    75     by (auto simp add: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
    76 qed
    77 
    78 corollary union_inter_neutral:
    79   assumes "finite A" and "finite B"
    80   and I0: "\<forall>x \<in> A \<inter> B. g x = 1"
    81   shows "F g (A \<union> B) = F g A * F g B"
    82   using assms by (simp add: union_inter [symmetric] neutral)
    83 
    84 corollary union_disjoint:
    85   assumes "finite A" and "finite B"
    86   assumes "A \<inter> B = {}"
    87   shows "F g (A \<union> B) = F g A * F g B"
    88   using assms by (simp add: union_inter_neutral)
    89 
    90 lemma union_diff2:
    91   assumes "finite A" and "finite B"
    92   shows "F g (A \<union> B) = F g (A - B) * F g (B - A) * F g (A \<inter> B)"
    93 proof -
    94   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
    95     by auto
    96   with assms show ?thesis by simp (subst union_disjoint, auto)+
    97 qed
    98 
    99 lemma subset_diff:
   100   assumes "B \<subseteq> A" and "finite A"
   101   shows "F g A = F g (A - B) * F g B"
   102 proof -
   103   from assms have "finite (A - B)" by auto
   104   moreover from assms have "finite B" by (rule finite_subset)
   105   moreover from assms have "(A - B) \<inter> B = {}" by auto
   106   ultimately have "F g (A - B \<union> B) = F g (A - B) * F g B" by (rule union_disjoint)
   107   moreover from assms have "A \<union> B = A" by auto
   108   ultimately show ?thesis by simp
   109 qed
   110 
   111 lemma setdiff_irrelevant:
   112   assumes "finite A"
   113   shows "F g (A - {x. g x = z}) = F g A"
   114   using assms by (induct A) (simp_all add: insert_Diff_if) 
   115 
   116 lemma not_neutral_contains_not_neutral:
   117   assumes "F g A \<noteq> z"
   118   obtains a where "a \<in> A" and "g a \<noteq> z"
   119 proof -
   120   from assms have "\<exists>a\<in>A. g a \<noteq> z"
   121   proof (induct A rule: infinite_finite_induct)
   122     case (insert a A)
   123     then show ?case by simp (rule, simp)
   124   qed simp_all
   125   with that show thesis by blast
   126 qed
   127 
   128 lemma reindex:
   129   assumes "inj_on h A"
   130   shows "F g (h ` A) = F (g \<circ> h) A"
   131 proof (cases "finite A")
   132   case True
   133   with assms show ?thesis by (simp add: eq_fold fold_image comp_assoc)
   134 next
   135   case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
   136   with False show ?thesis by simp
   137 qed
   138 
   139 lemma cong:
   140   assumes "A = B"
   141   assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   142   shows "F g A = F h B"
   143   using g_h unfolding `A = B`
   144   by (induct B rule: infinite_finite_induct) auto
   145 
   146 lemma strong_cong [cong]:
   147   assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
   148   shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
   149   by (rule cong) (insert assms, simp_all add: simp_implies_def)
   150 
   151 lemma reindex_cong:
   152   assumes "inj_on l B"
   153   assumes "A = l ` B"
   154   assumes "\<And>x. x \<in> B \<Longrightarrow> g (l x) = h x"
   155   shows "F g A = F h B"
   156   using assms by (simp add: reindex)
   157 
   158 lemma UNION_disjoint:
   159   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   160   and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   161   shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
   162 apply (insert assms)
   163 apply (induct rule: finite_induct)
   164 apply simp
   165 apply atomize
   166 apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
   167  prefer 2 apply blast
   168 apply (subgoal_tac "A x Int UNION Fa A = {}")
   169  prefer 2 apply blast
   170 apply (simp add: union_disjoint)
   171 done
   172 
   173 lemma Union_disjoint:
   174   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
   175   shows "F g (Union C) = (F \<circ> F) g C"
   176 proof cases
   177   assume "finite C"
   178   from UNION_disjoint [OF this assms]
   179   show ?thesis by simp
   180 qed (auto dest: finite_UnionD intro: infinite)
   181 
   182 lemma distrib:
   183   "F (\<lambda>x. g x * h x) A = F g A * F h A"
   184   using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
   185 
   186 lemma Sigma:
   187   "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (split g) (SIGMA x:A. B x)"
   188 apply (subst Sigma_def)
   189 apply (subst UNION_disjoint, assumption, simp)
   190  apply blast
   191 apply (rule cong)
   192 apply rule
   193 apply (simp add: fun_eq_iff)
   194 apply (subst UNION_disjoint, simp, simp)
   195  apply blast
   196 apply (simp add: comp_def)
   197 done
   198 
   199 lemma related: 
   200   assumes Re: "R 1 1" 
   201   and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   202   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   203   shows "R (F h S) (F g S)"
   204   using fS by (rule finite_subset_induct) (insert assms, auto)
   205 
   206 lemma mono_neutral_cong_left:
   207   assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
   208   and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
   209 proof-
   210   have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
   211   have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
   212   from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
   213     by (auto intro: finite_subset)
   214   show ?thesis using assms(4)
   215     by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
   216 qed
   217 
   218 lemma mono_neutral_cong_right:
   219   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
   220    \<Longrightarrow> F g T = F h S"
   221   by (auto intro!: mono_neutral_cong_left [symmetric])
   222 
   223 lemma mono_neutral_left:
   224   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   225   by (blast intro: mono_neutral_cong_left)
   226 
   227 lemma mono_neutral_right:
   228   "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   229   by (blast intro!: mono_neutral_left [symmetric])
   230 
   231 lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
   232   by (auto simp: bij_betw_def reindex)
   233 
   234 lemma reindex_bij_witness:
   235   assumes witness:
   236     "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a"
   237     "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T"
   238     "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b"
   239     "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S"
   240   assumes eq:
   241     "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
   242   shows "F g S = F h T"
   243 proof -
   244   have "bij_betw j S T"
   245     using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
   246   moreover have "F g S = F (\<lambda>x. h (j x)) S"
   247     by (intro cong) (auto simp: eq)
   248   ultimately show ?thesis
   249     by (simp add: reindex_bij_betw)
   250 qed
   251 
   252 lemma reindex_bij_betw_not_neutral:
   253   assumes fin: "finite S'" "finite T'"
   254   assumes bij: "bij_betw h (S - S') (T - T')"
   255   assumes nn:
   256     "\<And>a. a \<in> S' \<Longrightarrow> g (h a) = z"
   257     "\<And>b. b \<in> T' \<Longrightarrow> g b = z"
   258   shows "F (\<lambda>x. g (h x)) S = F g T"
   259 proof -
   260   have [simp]: "finite S \<longleftrightarrow> finite T"
   261     using bij_betw_finite[OF bij] fin by auto
   262 
   263   show ?thesis
   264   proof cases
   265     assume "finite S"
   266     with nn have "F (\<lambda>x. g (h x)) S = F (\<lambda>x. g (h x)) (S - S')"
   267       by (intro mono_neutral_cong_right) auto
   268     also have "\<dots> = F g (T - T')"
   269       using bij by (rule reindex_bij_betw)
   270     also have "\<dots> = F g T"
   271       using nn `finite S` by (intro mono_neutral_cong_left) auto
   272     finally show ?thesis .
   273   qed simp
   274 qed
   275 
   276 lemma reindex_nontrivial:
   277   assumes "finite A"
   278   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"
   279   shows "F g (h ` A) = F (g \<circ> h) A"
   280 proof (subst reindex_bij_betw_not_neutral [symmetric])
   281   show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = 1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = 1})"
   282     using nz by (auto intro!: inj_onI simp: bij_betw_def)
   283 qed (insert `finite A`, auto)
   284 
   285 lemma reindex_bij_witness_not_neutral:
   286   assumes fin: "finite S'" "finite T'"
   287   assumes witness:
   288     "\<And>a. a \<in> S - S' \<Longrightarrow> i (j a) = a"
   289     "\<And>a. a \<in> S - S' \<Longrightarrow> j a \<in> T - T'"
   290     "\<And>b. b \<in> T - T' \<Longrightarrow> j (i b) = b"
   291     "\<And>b. b \<in> T - T' \<Longrightarrow> i b \<in> S - S'"
   292   assumes nn:
   293     "\<And>a. a \<in> S' \<Longrightarrow> g a = z"
   294     "\<And>b. b \<in> T' \<Longrightarrow> h b = z"
   295   assumes eq:
   296     "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
   297   shows "F g S = F h T"
   298 proof -
   299   have bij: "bij_betw j (S - (S' \<inter> S)) (T - (T' \<inter> T))"
   300     using witness by (intro bij_betw_byWitness[where f'=i]) auto
   301   have F_eq: "F g S = F (\<lambda>x. h (j x)) S"
   302     by (intro cong) (auto simp: eq)
   303   show ?thesis
   304     unfolding F_eq using fin nn eq
   305     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
   306 qed
   307 
   308 lemma delta: 
   309   assumes fS: "finite S"
   310   shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
   311 proof-
   312   let ?f = "(\<lambda>k. if k=a then b k else 1)"
   313   { assume a: "a \<notin> S"
   314     hence "\<forall>k\<in>S. ?f k = 1" by simp
   315     hence ?thesis  using a by simp }
   316   moreover
   317   { assume a: "a \<in> S"
   318     let ?A = "S - {a}"
   319     let ?B = "{a}"
   320     have eq: "S = ?A \<union> ?B" using a by blast 
   321     have dj: "?A \<inter> ?B = {}" by simp
   322     from fS have fAB: "finite ?A" "finite ?B" by auto  
   323     have "F ?f S = F ?f ?A * F ?f ?B"
   324       using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
   325       by simp
   326     then have ?thesis using a by simp }
   327   ultimately show ?thesis by blast
   328 qed
   329 
   330 lemma delta': 
   331   assumes fS: "finite S"
   332   shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
   333   using delta [OF fS, of a b, symmetric] by (auto intro: cong)
   334 
   335 lemma If_cases:
   336   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   337   assumes fA: "finite A"
   338   shows "F (\<lambda>x. if P x then h x else g x) A =
   339     F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
   340 proof -
   341   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
   342           "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
   343     by blast+
   344   from fA 
   345   have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   346   let ?g = "\<lambda>x. if P x then h x else g x"
   347   from union_disjoint [OF f a(2), of ?g] a(1)
   348   show ?thesis
   349     by (subst (1 2) cong) simp_all
   350 qed
   351 
   352 lemma cartesian_product:
   353    "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
   354 apply (rule sym)
   355 apply (cases "finite A") 
   356  apply (cases "finite B") 
   357   apply (simp add: Sigma)
   358  apply (cases "A={}", simp)
   359  apply simp
   360 apply (auto intro: infinite dest: finite_cartesian_productD2)
   361 apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
   362 done
   363 
   364 lemma inter_restrict:
   365   assumes "finite A"
   366   shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else 1) A"
   367 proof -
   368   let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else 1"
   369   have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else 1) = 1"
   370    by simp
   371   moreover have "A \<inter> B \<subseteq> A" by blast
   372   ultimately have "F ?g (A \<inter> B) = F ?g A" using `finite A`
   373     by (intro mono_neutral_left) auto
   374   then show ?thesis by simp
   375 qed
   376 
   377 lemma inter_filter:
   378   "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else 1) A"
   379   by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)
   380 
   381 lemma Union_comp:
   382   assumes "\<forall>A \<in> B. finite A"
   383     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"
   384   shows "F g (\<Union>B) = (F \<circ> F) g B"
   385 using assms proof (induct B rule: infinite_finite_induct)
   386   case (infinite A)
   387   then have "\<not> finite (\<Union>A)" by (blast dest: finite_UnionD)
   388   with infinite show ?case by simp
   389 next
   390   case empty then show ?case by simp
   391 next
   392   case (insert A B)
   393   then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B"
   394     and "\<forall>x\<in>A \<inter> \<Union>B. g x = 1"
   395     and H: "F g (\<Union>B) = (F o F) g B" by auto
   396   then have "F g (A \<union> \<Union>B) = F g A * F g (\<Union>B)"
   397     by (simp add: union_inter_neutral)
   398   with `finite B` `A \<notin> B` show ?case
   399     by (simp add: H)
   400 qed
   401 
   402 lemma commute:
   403   "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
   404   unfolding cartesian_product
   405   by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto
   406 
   407 lemma commute_restrict:
   408   "finite A \<Longrightarrow> finite B \<Longrightarrow>
   409     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"
   410   by (simp add: inter_filter) (rule commute)
   411 
   412 lemma Plus:
   413   fixes A :: "'b set" and B :: "'c set"
   414   assumes fin: "finite A" "finite B"
   415   shows "F g (A <+> B) = F (g \<circ> Inl) A * F (g \<circ> Inr) B"
   416 proof -
   417   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   418   moreover from fin have "finite (Inl ` A :: ('b + 'c) set)" "finite (Inr ` B :: ('b + 'c) set)"
   419     by auto
   420   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('b + 'c) set)" by auto
   421   moreover have "inj_on (Inl :: 'b \<Rightarrow> 'b + 'c) A" "inj_on (Inr :: 'c \<Rightarrow> 'b + 'c) B"
   422     by (auto intro: inj_onI)
   423   ultimately show ?thesis using fin
   424     by (simp add: union_disjoint reindex)
   425 qed
   426 
   427 lemma same_carrier:
   428   assumes "finite C"
   429   assumes subset: "A \<subseteq> C" "B \<subseteq> C"
   430   assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
   431   shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
   432 proof -
   433   from `finite C` subset have
   434     "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)"
   435     by (auto elim: finite_subset)
   436   from subset have [simp]: "A - (C - A) = A" by auto
   437   from subset have [simp]: "B - (C - B) = B" by auto
   438   from subset have "C = A \<union> (C - A)" by auto
   439   then have "F g C = F g (A \<union> (C - A))" by simp
   440   also have "\<dots> = F g (A - (C - A)) * F g (C - A - A) * F g (A \<inter> (C - A))"
   441     using `finite A` `finite (C - A)` by (simp only: union_diff2)
   442   finally have P: "F g C = F g A" using trivial by simp
   443   from subset have "C = B \<union> (C - B)" by auto
   444   then have "F h C = F h (B \<union> (C - B))" by simp
   445   also have "\<dots> = F h (B - (C - B)) * F h (C - B - B) * F h (B \<inter> (C - B))"
   446     using `finite B` `finite (C - B)` by (simp only: union_diff2)
   447   finally have Q: "F h C = F h B" using trivial by simp
   448   from P Q show ?thesis by simp
   449 qed
   450 
   451 lemma same_carrierI:
   452   assumes "finite C"
   453   assumes subset: "A \<subseteq> C" "B \<subseteq> C"
   454   assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
   455   assumes "F g C = F h C"
   456   shows "F g A = F h B"
   457   using assms same_carrier [of C A B] by simp
   458 
   459 end
   460 
   461 notation times (infixl "*" 70)
   462 notation Groups.one ("1")
   463 
   464 
   465 subsection {* Generalized summation over a set *}
   466 
   467 context comm_monoid_add
   468 begin
   469 
   470 definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   471 where
   472   "setsum = comm_monoid_set.F plus 0"
   473 
   474 sublocale setsum!: comm_monoid_set plus 0
   475 where
   476   "comm_monoid_set.F plus 0 = setsum"
   477 proof -
   478   show "comm_monoid_set plus 0" ..
   479   then interpret setsum!: comm_monoid_set plus 0 .
   480   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   481 qed
   482 
   483 abbreviation
   484   Setsum ("\<Sum>_" [1000] 999) where
   485   "\<Sum>A \<equiv> setsum (%x. x) A"
   486 
   487 end
   488 
   489 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   490 written @{text"\<Sum>x\<in>A. e"}. *}
   491 
   492 syntax
   493   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   494 syntax (xsymbols)
   495   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   496 syntax (HTML output)
   497   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   498 
   499 translations -- {* Beware of argument permutation! *}
   500   "SUM i:A. b" == "CONST setsum (%i. b) A"
   501   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   502 
   503 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   504  @{text"\<Sum>x|P. e"}. *}
   505 
   506 syntax
   507   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   508 syntax (xsymbols)
   509   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   510 syntax (HTML output)
   511   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   512 
   513 translations
   514   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   515   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   516 
   517 print_translation {*
   518 let
   519   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   520         if x <> y then raise Match
   521         else
   522           let
   523             val x' = Syntax_Trans.mark_bound_body (x, Tx);
   524             val t' = subst_bound (x', t);
   525             val P' = subst_bound (x', P);
   526           in
   527             Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   528           end
   529     | setsum_tr' _ = raise Match;
   530 in [(@{const_syntax setsum}, K setsum_tr')] end
   531 *}
   532 
   533 text {* TODO generalization candidates *}
   534 
   535 lemma setsum_image_gen:
   536   assumes fS: "finite S"
   537   shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   538 proof-
   539   { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto }
   540   hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
   541     by simp
   542   also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   543     by (rule setsum.commute_restrict [OF fS finite_imageI [OF fS]])
   544   finally show ?thesis .
   545 qed
   546 
   547 
   548 subsubsection {* Properties in more restricted classes of structures *}
   549 
   550 lemma setsum_Un: "finite A ==> finite B ==>
   551   (setsum f (A Un B) :: 'a :: ab_group_add) =
   552    setsum f A + setsum f B - setsum f (A Int B)"
   553 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   554 
   555 lemma setsum_Un2:
   556   assumes "finite (A \<union> B)"
   557   shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
   558 proof -
   559   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   560     by auto
   561   with assms show ?thesis by simp (subst setsum.union_disjoint, auto)+
   562 qed
   563 
   564 lemma setsum_diff1: "finite A \<Longrightarrow>
   565   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   566   (if a:A then setsum f A - f a else setsum f A)"
   567 by (erule finite_induct) (auto simp add: insert_Diff_if)
   568 
   569 lemma setsum_diff:
   570   assumes le: "finite A" "B \<subseteq> A"
   571   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   572 proof -
   573   from le have finiteB: "finite B" using finite_subset by auto
   574   show ?thesis using finiteB le
   575   proof induct
   576     case empty
   577     thus ?case by auto
   578   next
   579     case (insert x F)
   580     thus ?case using le finiteB 
   581       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   582   qed
   583 qed
   584 
   585 lemma setsum_mono:
   586   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   587   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   588 proof (cases "finite K")
   589   case True
   590   thus ?thesis using le
   591   proof induct
   592     case empty
   593     thus ?case by simp
   594   next
   595     case insert
   596     thus ?case using add_mono by fastforce
   597   qed
   598 next
   599   case False then show ?thesis by simp
   600 qed
   601 
   602 lemma setsum_strict_mono:
   603   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   604   assumes "finite A"  "A \<noteq> {}"
   605     and "!!x. x:A \<Longrightarrow> f x < g x"
   606   shows "setsum f A < setsum g A"
   607   using assms
   608 proof (induct rule: finite_ne_induct)
   609   case singleton thus ?case by simp
   610 next
   611   case insert thus ?case by (auto simp: add_strict_mono)
   612 qed
   613 
   614 lemma setsum_strict_mono_ex1:
   615 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   616 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   617 shows "setsum f A < setsum g A"
   618 proof-
   619   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   620   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   621     by(simp add:insert_absorb[OF `a:A`])
   622   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   623     using `finite A` by(subst setsum.union_disjoint) auto
   624   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   625     by(rule setsum_mono)(simp add: assms(2))
   626   also have "setsum f {a} < setsum g {a}" using a by simp
   627   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   628     using `finite A` by(subst setsum.union_disjoint[symmetric]) auto
   629   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   630   finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
   631 qed
   632 
   633 lemma setsum_negf:
   634   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   635 proof (cases "finite A")
   636   case True thus ?thesis by (induct set: finite) auto
   637 next
   638   case False thus ?thesis by simp
   639 qed
   640 
   641 lemma setsum_subtractf:
   642   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   643     setsum f A - setsum g A"
   644   using setsum.distrib [of f "- g" A] by (simp add: setsum_negf)
   645 
   646 lemma setsum_nonneg:
   647   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   648   shows "0 \<le> setsum f A"
   649 proof (cases "finite A")
   650   case True thus ?thesis using nn
   651   proof induct
   652     case empty then show ?case by simp
   653   next
   654     case (insert x F)
   655     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   656     with insert show ?case by simp
   657   qed
   658 next
   659   case False thus ?thesis by simp
   660 qed
   661 
   662 lemma setsum_nonpos:
   663   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   664   shows "setsum f A \<le> 0"
   665 proof (cases "finite A")
   666   case True thus ?thesis using np
   667   proof induct
   668     case empty then show ?case by simp
   669   next
   670     case (insert x F)
   671     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   672     with insert show ?case by simp
   673   qed
   674 next
   675   case False thus ?thesis by simp
   676 qed
   677 
   678 lemma setsum_nonneg_leq_bound:
   679   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   680   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   681   shows "f i \<le> B"
   682 proof -
   683   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   684     using assms by (auto intro!: setsum_nonneg)
   685   moreover
   686   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   687     using assms by (simp add: setsum_diff1)
   688   ultimately show ?thesis by auto
   689 qed
   690 
   691 lemma setsum_nonneg_0:
   692   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   693   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   694   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   695   shows "f i = 0"
   696   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   697 
   698 lemma setsum_mono2:
   699 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   700 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   701 shows "setsum f A \<le> setsum f B"
   702 proof -
   703   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   704     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   705   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   706     by (simp add: setsum.union_disjoint del:Un_Diff_cancel)
   707   also have "A \<union> (B-A) = B" using sub by blast
   708   finally show ?thesis .
   709 qed
   710 
   711 lemma setsum_le_included:
   712   fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
   713   assumes "finite s" "finite t"
   714   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)"
   715   shows "setsum f s \<le> setsum g t"
   716 proof -
   717   have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
   718   proof (rule setsum_mono)
   719     fix y assume "y \<in> s"
   720     with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
   721     with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
   722       using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
   723       by (auto intro!: setsum_mono2)
   724   qed
   725   also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
   726     using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
   727   also have "... \<le> setsum g t"
   728     using assms by (auto simp: setsum_image_gen[symmetric])
   729   finally show ?thesis .
   730 qed
   731 
   732 lemma setsum_mono3: "finite B ==> A <= B ==> 
   733     ALL x: B - A. 
   734       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   735         setsum f A <= setsum f B"
   736   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   737   apply (erule ssubst)
   738   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   739   apply simp
   740   apply (rule add_left_mono)
   741   apply (erule setsum_nonneg)
   742   apply (subst setsum.union_disjoint [THEN sym])
   743   apply (erule finite_subset, assumption)
   744   apply (rule finite_subset)
   745   prefer 2
   746   apply assumption
   747   apply (auto simp add: sup_absorb2)
   748 done
   749 
   750 lemma setsum_right_distrib: 
   751   fixes f :: "'a => ('b::semiring_0)"
   752   shows "r * setsum f A = setsum (%n. r * f n) A"
   753 proof (cases "finite A")
   754   case True
   755   thus ?thesis
   756   proof induct
   757     case empty thus ?case by simp
   758   next
   759     case (insert x A) thus ?case by (simp add: distrib_left)
   760   qed
   761 next
   762   case False thus ?thesis by simp
   763 qed
   764 
   765 lemma setsum_left_distrib:
   766   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   767 proof (cases "finite A")
   768   case True
   769   then show ?thesis
   770   proof induct
   771     case empty thus ?case by simp
   772   next
   773     case (insert x A) thus ?case by (simp add: distrib_right)
   774   qed
   775 next
   776   case False thus ?thesis by simp
   777 qed
   778 
   779 lemma setsum_divide_distrib:
   780   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   781 proof (cases "finite A")
   782   case True
   783   then show ?thesis
   784   proof induct
   785     case empty thus ?case by simp
   786   next
   787     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   788   qed
   789 next
   790   case False thus ?thesis by simp
   791 qed
   792 
   793 lemma setsum_abs[iff]: 
   794   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   795   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   796 proof (cases "finite A")
   797   case True
   798   thus ?thesis
   799   proof induct
   800     case empty thus ?case by simp
   801   next
   802     case (insert x A)
   803     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   804   qed
   805 next
   806   case False thus ?thesis by simp
   807 qed
   808 
   809 lemma setsum_abs_ge_zero[iff]: 
   810   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   811   shows "0 \<le> setsum (%i. abs(f i)) A"
   812 proof (cases "finite A")
   813   case True
   814   thus ?thesis
   815   proof induct
   816     case empty thus ?case by simp
   817   next
   818     case (insert x A) thus ?case by auto
   819   qed
   820 next
   821   case False thus ?thesis by simp
   822 qed
   823 
   824 lemma abs_setsum_abs[simp]: 
   825   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   826   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   827 proof (cases "finite A")
   828   case True
   829   thus ?thesis
   830   proof induct
   831     case empty thus ?case by simp
   832   next
   833     case (insert a A)
   834     hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
   835     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   836     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   837       by (simp del: abs_of_nonneg)
   838     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   839     finally show ?case .
   840   qed
   841 next
   842   case False thus ?thesis by simp
   843 qed
   844 
   845 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   846   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   847   unfolding setsum.remove [OF assms] by auto
   848 
   849 lemma setsum_product:
   850   fixes f :: "'a => ('b::semiring_0)"
   851   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   852   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute)
   853 
   854 lemma setsum_mult_setsum_if_inj:
   855 fixes f :: "'a => ('b::semiring_0)"
   856 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   857   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   858 by(auto simp: setsum_product setsum.cartesian_product
   859         intro!:  setsum.reindex_cong[symmetric])
   860 
   861 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   862 apply (case_tac "finite A")
   863  prefer 2 apply simp
   864 apply (erule rev_mp)
   865 apply (erule finite_induct, auto)
   866 done
   867 
   868 lemma setsum_eq_0_iff [simp]:
   869   "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   870   by (induct set: finite) auto
   871 
   872 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   873   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   874 apply(erule finite_induct)
   875 apply (auto simp add:add_is_1)
   876 done
   877 
   878 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   879 
   880 lemma setsum_Un_nat: "finite A ==> finite B ==>
   881   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   882   -- {* For the natural numbers, we have subtraction. *}
   883 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   884 
   885 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   886   (if a:A then setsum f A - f a else setsum f A)"
   887 apply (case_tac "finite A")
   888  prefer 2 apply simp
   889 apply (erule finite_induct)
   890  apply (auto simp add: insert_Diff_if)
   891 apply (drule_tac a = a in mk_disjoint_insert, auto)
   892 done
   893 
   894 lemma setsum_diff_nat: 
   895 assumes "finite B" and "B \<subseteq> A"
   896 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   897 using assms
   898 proof induct
   899   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   900 next
   901   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   902     and xFinA: "insert x F \<subseteq> A"
   903     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   904   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   905   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   906     by (simp add: setsum_diff1_nat)
   907   from xFinA have "F \<subseteq> A" by simp
   908   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   909   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   910     by simp
   911   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   912   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   913     by simp
   914   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   915   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   916     by simp
   917   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   918 qed
   919 
   920 lemma setsum_comp_morphism:
   921   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   922   shows "setsum (h \<circ> g) A = h (setsum g A)"
   923 proof (cases "finite A")
   924   case False then show ?thesis by (simp add: assms)
   925 next
   926   case True then show ?thesis by (induct A) (simp_all add: assms)
   927 qed
   928 
   929 lemma (in comm_semiring_1) dvd_setsum:
   930   "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
   931   by (induct A rule: infinite_finite_induct) simp_all
   932 
   933 
   934 subsubsection {* Cardinality as special case of @{const setsum} *}
   935 
   936 lemma card_eq_setsum:
   937   "card A = setsum (\<lambda>x. 1) A"
   938 proof -
   939   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   940     by (simp add: fun_eq_iff)
   941   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   942     by (rule arg_cong)
   943   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   944     by (blast intro: fun_cong)
   945   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   946 qed
   947 
   948 lemma setsum_constant [simp]:
   949   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   950 apply (cases "finite A")
   951 apply (erule finite_induct)
   952 apply (auto simp add: algebra_simps)
   953 done
   954 
   955 lemma setsum_Suc: "setsum (%x. Suc(f x)) A = setsum f A + card A"
   956 using setsum.distrib[of f "%_. 1" A] by(simp)
   957 
   958 lemma setsum_bounded:
   959   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   960   shows "setsum f A \<le> of_nat (card A) * K"
   961 proof (cases "finite A")
   962   case True
   963   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   964 next
   965   case False thus ?thesis by simp
   966 qed
   967 
   968 lemma card_UN_disjoint:
   969   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   970     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   971   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   972 proof -
   973   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   974   with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant)
   975 qed
   976 
   977 lemma card_Union_disjoint:
   978   "finite C ==> (ALL A:C. finite A) ==>
   979    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
   980    ==> card (Union C) = setsum card C"
   981 apply (frule card_UN_disjoint [of C id])
   982 apply simp_all
   983 done
   984 
   985 lemma setsum_multicount_gen:
   986   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   987   shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
   988 proof-
   989   have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
   990   also have "\<dots> = ?r" unfolding setsum.commute_restrict [OF assms(1-2)]
   991     using assms(3) by auto
   992   finally show ?thesis .
   993 qed
   994 
   995 lemma setsum_multicount:
   996   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
   997   shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
   998 proof-
   999   have "?l = setsum (\<lambda>i. k) T" by (rule setsum_multicount_gen) (auto simp: assms)
  1000   also have "\<dots> = ?r" by (simp add: mult.commute)
  1001   finally show ?thesis by auto
  1002 qed
  1003 
  1004 lemma (in ordered_comm_monoid_add) setsum_pos: 
  1005   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
  1006   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
  1007 
  1008 
  1009 subsubsection {* Cardinality of products *}
  1010 
  1011 lemma card_SigmaI [simp]:
  1012   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1013   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1014 by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant)
  1015 
  1016 (*
  1017 lemma SigmaI_insert: "y \<notin> A ==>
  1018   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1019   by auto
  1020 *)
  1021 
  1022 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1023   by (cases "finite A \<and> finite B")
  1024     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1025 
  1026 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1027 by (simp add: card_cartesian_product)
  1028 
  1029 
  1030 subsection {* Generalized product over a set *}
  1031 
  1032 context comm_monoid_mult
  1033 begin
  1034 
  1035 definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  1036 where
  1037   "setprod = comm_monoid_set.F times 1"
  1038 
  1039 sublocale setprod!: comm_monoid_set times 1
  1040 where
  1041   "comm_monoid_set.F times 1 = setprod"
  1042 proof -
  1043   show "comm_monoid_set times 1" ..
  1044   then interpret setprod!: comm_monoid_set times 1 .
  1045   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  1046 qed
  1047 
  1048 abbreviation
  1049   Setprod ("\<Prod>_" [1000] 999) where
  1050   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1051 
  1052 end
  1053 
  1054 syntax
  1055   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1056 syntax (xsymbols)
  1057   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1058 syntax (HTML output)
  1059   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1060 
  1061 translations -- {* Beware of argument permutation! *}
  1062   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1063   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1064 
  1065 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1066  @{text"\<Prod>x|P. e"}. *}
  1067 
  1068 syntax
  1069   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1070 syntax (xsymbols)
  1071   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1072 syntax (HTML output)
  1073   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1074 
  1075 translations
  1076   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1077   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1078 
  1079 context comm_monoid_mult
  1080 begin
  1081 
  1082 lemma setprod_dvd_setprod: 
  1083   "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
  1084 proof (induct A rule: infinite_finite_induct)
  1085   case infinite then show ?case by (auto intro: dvdI)
  1086 next
  1087   case empty then show ?case by (auto intro: dvdI)
  1088 next
  1089   case (insert a A) then
  1090   have "f a dvd g a" and "setprod f A dvd setprod g A" by simp_all
  1091   then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s" by (auto elim!: dvdE)
  1092   then have "g a * setprod g A = f a * setprod f A * (r * s)" by (simp add: ac_simps)
  1093   with insert.hyps show ?case by (auto intro: dvdI)
  1094 qed
  1095 
  1096 lemma setprod_dvd_setprod_subset:
  1097   "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
  1098   by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
  1099 
  1100 end
  1101 
  1102 
  1103 subsubsection {* Properties in more restricted classes of structures *}
  1104 
  1105 context comm_semiring_1
  1106 begin
  1107 
  1108 lemma dvd_setprod_eqI [intro]:
  1109   assumes "finite A" and "a \<in> A" and "b = f a"
  1110   shows "b dvd setprod f A"
  1111 proof -
  1112   from `finite A` have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
  1113     by (intro setprod.insert) auto
  1114   also from `a \<in> A` have "insert a (A - {a}) = A" by blast
  1115   finally have "setprod f A = f a * setprod f (A - {a})" .
  1116   with `b = f a` show ?thesis by simp
  1117 qed
  1118 
  1119 lemma dvd_setprodI [intro]:
  1120   assumes "finite A" and "a \<in> A"
  1121   shows "f a dvd setprod f A"
  1122   using assms by auto
  1123 
  1124 lemma setprod_zero:
  1125   assumes "finite A" and "\<exists>a\<in>A. f a = 0"
  1126   shows "setprod f A = 0"
  1127 using assms proof (induct A)
  1128   case empty then show ?case by simp
  1129 next
  1130   case (insert a A)
  1131   then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
  1132   then have "f a * setprod f A = 0" by rule (simp_all add: insert)
  1133   with insert show ?case by simp
  1134 qed
  1135 
  1136 lemma setprod_dvd_setprod_subset2:
  1137   assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
  1138   shows "setprod f A dvd setprod g B"
  1139 proof -
  1140   from assms have "setprod f A dvd setprod g A"
  1141     by (auto intro: setprod_dvd_setprod)
  1142   moreover from assms have "setprod g A dvd setprod g B"
  1143     by (auto intro: setprod_dvd_setprod_subset)
  1144   ultimately show ?thesis by (rule dvd_trans)
  1145 qed
  1146 
  1147 end
  1148 
  1149 lemma setprod_zero_iff [simp]:
  1150   assumes "finite A"
  1151   shows "setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors}) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
  1152   using assms by (induct A) (auto simp: no_zero_divisors)
  1153 
  1154 lemma (in field) setprod_diff1:
  1155   "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
  1156     (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
  1157   by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
  1158 
  1159 lemma (in field_inverse_zero) setprod_inversef: 
  1160   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1161   by (induct A rule: finite_induct) simp_all
  1162 
  1163 lemma (in field_inverse_zero) setprod_dividef:
  1164   "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
  1165   using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
  1166 
  1167 lemma setprod_Un:
  1168   fixes f :: "'b \<Rightarrow> 'a :: field"
  1169   assumes "finite A" and "finite B"
  1170   and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
  1171   shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
  1172 proof -
  1173   from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
  1174     by (simp add: setprod.union_inter [symmetric, of A B])
  1175   with assms show ?thesis by simp
  1176 qed
  1177 
  1178 lemma (in linordered_semidom) setprod_nonneg:
  1179   "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
  1180   by (induct A rule: infinite_finite_induct) simp_all
  1181 
  1182 lemma (in linordered_semidom) setprod_pos:
  1183   "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
  1184   by (induct A rule: infinite_finite_induct) simp_all
  1185 
  1186 lemma (in linordered_semidom) setprod_mono:
  1187   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1188   shows "setprod f A \<le> setprod g A"
  1189   using assms by (induct A rule: infinite_finite_induct)
  1190     (auto intro!: setprod_nonneg mult_mono)
  1191 
  1192 lemma (in linordered_field) abs_setprod:
  1193   "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
  1194   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
  1195 
  1196 lemma setprod_eq_1_iff [simp]:
  1197   "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
  1198   by (induct A rule: finite_induct) simp_all
  1199 
  1200 lemma setprod_pos_nat:
  1201   "finite A \<Longrightarrow> (\<forall>a\<in>A. f a > (0::nat)) \<Longrightarrow> setprod f A > 0"
  1202   using setprod_zero_iff by (simp del: neq0_conv add: neq0_conv [symmetric])
  1203 
  1204 lemma setprod_pos_nat_iff [simp]:
  1205   "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
  1206   using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
  1207 
  1208 end