src/HOL/Groups_Big.thy
author haftmann
Sat Mar 28 21:32:48 2015 +0100 (2015-03-28)
changeset 59833 ab828c2c5d67
parent 59615 fdfdf89a83a6
child 59867 58043346ca64
permissions -rw-r--r--
clarified no_zero_devisors: makes only sense in a semiring;
actually turn linorder_semidom into a integral domain
     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: "(\<Sum>x\<in>A. - f x::'a::ab_group_add) = - (\<Sum>x\<in>A. f x)"
   634 proof (cases "finite A")
   635   case True thus ?thesis by (induct set: finite) auto
   636 next
   637   case False thus ?thesis by simp
   638 qed
   639 
   640 lemma setsum_subtractf: "(\<Sum>x\<in>A. f x - g x::'a::ab_group_add) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
   641   using setsum.distrib [of f "- g" A] by (simp add: setsum_negf)
   642 
   643 lemma setsum_subtractf_nat:
   644   "(\<And>x. x \<in> A \<Longrightarrow> g x \<le> f x) \<Longrightarrow> (\<Sum>x\<in>A. f x - g x::nat) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
   645   by (induction A rule: infinite_finite_induct) (auto simp: setsum_mono)
   646 
   647 lemma setsum_nonneg:
   648   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   649   shows "0 \<le> setsum f A"
   650 proof (cases "finite A")
   651   case True thus ?thesis using nn
   652   proof induct
   653     case empty then show ?case by simp
   654   next
   655     case (insert x F)
   656     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   657     with insert show ?case by simp
   658   qed
   659 next
   660   case False thus ?thesis by simp
   661 qed
   662 
   663 lemma setsum_nonpos:
   664   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   665   shows "setsum f A \<le> 0"
   666 proof (cases "finite A")
   667   case True thus ?thesis using np
   668   proof induct
   669     case empty then show ?case by simp
   670   next
   671     case (insert x F)
   672     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   673     with insert show ?case by simp
   674   qed
   675 next
   676   case False thus ?thesis by simp
   677 qed
   678 
   679 lemma setsum_nonneg_leq_bound:
   680   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   681   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   682   shows "f i \<le> B"
   683 proof -
   684   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   685     using assms by (auto intro!: setsum_nonneg)
   686   moreover
   687   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   688     using assms by (simp add: setsum_diff1)
   689   ultimately show ?thesis by auto
   690 qed
   691 
   692 lemma setsum_nonneg_0:
   693   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   694   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   695   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   696   shows "f i = 0"
   697   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   698 
   699 lemma setsum_mono2:
   700 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   701 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   702 shows "setsum f A \<le> setsum f B"
   703 proof -
   704   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   705     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   706   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   707     by (simp add: setsum.union_disjoint del:Un_Diff_cancel)
   708   also have "A \<union> (B-A) = B" using sub by blast
   709   finally show ?thesis .
   710 qed
   711 
   712 lemma setsum_le_included:
   713   fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
   714   assumes "finite s" "finite t"
   715   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)"
   716   shows "setsum f s \<le> setsum g t"
   717 proof -
   718   have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
   719   proof (rule setsum_mono)
   720     fix y assume "y \<in> s"
   721     with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
   722     with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
   723       using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
   724       by (auto intro!: setsum_mono2)
   725   qed
   726   also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
   727     using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
   728   also have "... \<le> setsum g t"
   729     using assms by (auto simp: setsum_image_gen[symmetric])
   730   finally show ?thesis .
   731 qed
   732 
   733 lemma setsum_mono3: "finite B ==> A <= B ==> 
   734     ALL x: B - A. 
   735       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   736         setsum f A <= setsum f B"
   737   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   738   apply (erule ssubst)
   739   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   740   apply simp
   741   apply (rule add_left_mono)
   742   apply (erule setsum_nonneg)
   743   apply (subst setsum.union_disjoint [THEN sym])
   744   apply (erule finite_subset, assumption)
   745   apply (rule finite_subset)
   746   prefer 2
   747   apply assumption
   748   apply (auto simp add: sup_absorb2)
   749 done
   750 
   751 lemma setsum_right_distrib: 
   752   fixes f :: "'a => ('b::semiring_0)"
   753   shows "r * setsum f A = setsum (%n. r * f n) A"
   754 proof (cases "finite A")
   755   case True
   756   thus ?thesis
   757   proof induct
   758     case empty thus ?case by simp
   759   next
   760     case (insert x A) thus ?case by (simp add: distrib_left)
   761   qed
   762 next
   763   case False thus ?thesis by simp
   764 qed
   765 
   766 lemma setsum_left_distrib:
   767   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   768 proof (cases "finite A")
   769   case True
   770   then show ?thesis
   771   proof induct
   772     case empty thus ?case by simp
   773   next
   774     case (insert x A) thus ?case by (simp add: distrib_right)
   775   qed
   776 next
   777   case False thus ?thesis by simp
   778 qed
   779 
   780 lemma setsum_divide_distrib:
   781   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   782 proof (cases "finite A")
   783   case True
   784   then show ?thesis
   785   proof induct
   786     case empty thus ?case by simp
   787   next
   788     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   789   qed
   790 next
   791   case False thus ?thesis by simp
   792 qed
   793 
   794 lemma setsum_abs[iff]: 
   795   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   796   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   797 proof (cases "finite A")
   798   case True
   799   thus ?thesis
   800   proof induct
   801     case empty thus ?case by simp
   802   next
   803     case (insert x A)
   804     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   805   qed
   806 next
   807   case False thus ?thesis by simp
   808 qed
   809 
   810 lemma setsum_abs_ge_zero[iff]: 
   811   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   812   shows "0 \<le> setsum (%i. abs(f i)) A"
   813 proof (cases "finite A")
   814   case True
   815   thus ?thesis
   816   proof induct
   817     case empty thus ?case by simp
   818   next
   819     case (insert x A) thus ?case by auto
   820   qed
   821 next
   822   case False thus ?thesis by simp
   823 qed
   824 
   825 lemma abs_setsum_abs[simp]: 
   826   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   827   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   828 proof (cases "finite A")
   829   case True
   830   thus ?thesis
   831   proof induct
   832     case empty thus ?case by simp
   833   next
   834     case (insert a A)
   835     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
   836     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   837     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   838       by (simp del: abs_of_nonneg)
   839     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   840     finally show ?case .
   841   qed
   842 next
   843   case False thus ?thesis by simp
   844 qed
   845 
   846 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   847   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   848   unfolding setsum.remove [OF assms] by auto
   849 
   850 lemma setsum_product:
   851   fixes f :: "'a => ('b::semiring_0)"
   852   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   853   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute)
   854 
   855 lemma setsum_mult_setsum_if_inj:
   856 fixes f :: "'a => ('b::semiring_0)"
   857 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   858   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   859 by(auto simp: setsum_product setsum.cartesian_product
   860         intro!:  setsum.reindex_cong[symmetric])
   861 
   862 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   863 apply (case_tac "finite A")
   864  prefer 2 apply simp
   865 apply (erule rev_mp)
   866 apply (erule finite_induct, auto)
   867 done
   868 
   869 lemma setsum_eq_0_iff [simp]:
   870   "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   871   by (induct set: finite) auto
   872 
   873 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   874   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   875 apply(erule finite_induct)
   876 apply (auto simp add:add_is_1)
   877 done
   878 
   879 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   880 
   881 lemma setsum_Un_nat: "finite A ==> finite B ==>
   882   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   883   -- {* For the natural numbers, we have subtraction. *}
   884 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   885 
   886 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   887   (if a:A then setsum f A - f a else setsum f A)"
   888 apply (case_tac "finite A")
   889  prefer 2 apply simp
   890 apply (erule finite_induct)
   891  apply (auto simp add: insert_Diff_if)
   892 apply (drule_tac a = a in mk_disjoint_insert, auto)
   893 done
   894 
   895 lemma setsum_diff_nat: 
   896 assumes "finite B" and "B \<subseteq> A"
   897 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   898 using assms
   899 proof induct
   900   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   901 next
   902   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   903     and xFinA: "insert x F \<subseteq> A"
   904     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   905   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   906   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   907     by (simp add: setsum_diff1_nat)
   908   from xFinA have "F \<subseteq> A" by simp
   909   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   910   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   911     by simp
   912   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   913   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   914     by simp
   915   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   916   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   917     by simp
   918   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   919 qed
   920 
   921 lemma setsum_comp_morphism:
   922   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   923   shows "setsum (h \<circ> g) A = h (setsum g A)"
   924 proof (cases "finite A")
   925   case False then show ?thesis by (simp add: assms)
   926 next
   927   case True then show ?thesis by (induct A) (simp_all add: assms)
   928 qed
   929 
   930 lemma (in comm_semiring_1) dvd_setsum:
   931   "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
   932   by (induct A rule: infinite_finite_induct) simp_all
   933 
   934 
   935 subsubsection {* Cardinality as special case of @{const setsum} *}
   936 
   937 lemma card_eq_setsum:
   938   "card A = setsum (\<lambda>x. 1) A"
   939 proof -
   940   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   941     by (simp add: fun_eq_iff)
   942   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   943     by (rule arg_cong)
   944   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   945     by (blast intro: fun_cong)
   946   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   947 qed
   948 
   949 lemma setsum_constant [simp]:
   950   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   951 apply (cases "finite A")
   952 apply (erule finite_induct)
   953 apply (auto simp add: algebra_simps)
   954 done
   955 
   956 lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
   957   using setsum.distrib[of f "\<lambda>_. 1" A] 
   958   by simp
   959 
   960 lemma setsum_bounded:
   961   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   962   shows "setsum f A \<le> of_nat (card A) * K"
   963 proof (cases "finite A")
   964   case True
   965   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   966 next
   967   case False thus ?thesis by simp
   968 qed
   969 
   970 lemma card_UN_disjoint:
   971   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   972     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   973   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   974 proof -
   975   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   976   with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant)
   977 qed
   978 
   979 lemma card_Union_disjoint:
   980   "finite C ==> (ALL A:C. finite A) ==>
   981    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
   982    ==> card (Union C) = setsum card C"
   983 apply (frule card_UN_disjoint [of C id])
   984 apply simp_all
   985 done
   986 
   987 lemma setsum_multicount_gen:
   988   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   989   shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
   990 proof-
   991   have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
   992   also have "\<dots> = ?r" unfolding setsum.commute_restrict [OF assms(1-2)]
   993     using assms(3) by auto
   994   finally show ?thesis .
   995 qed
   996 
   997 lemma setsum_multicount:
   998   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
   999   shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
  1000 proof-
  1001   have "?l = setsum (\<lambda>i. k) T" by (rule setsum_multicount_gen) (auto simp: assms)
  1002   also have "\<dots> = ?r" by (simp add: mult.commute)
  1003   finally show ?thesis by auto
  1004 qed
  1005 
  1006 lemma (in ordered_comm_monoid_add) setsum_pos: 
  1007   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
  1008   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
  1009 
  1010 
  1011 subsubsection {* Cardinality of products *}
  1012 
  1013 lemma card_SigmaI [simp]:
  1014   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1015   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1016 by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant)
  1017 
  1018 (*
  1019 lemma SigmaI_insert: "y \<notin> A ==>
  1020   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1021   by auto
  1022 *)
  1023 
  1024 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1025   by (cases "finite A \<and> finite B")
  1026     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1027 
  1028 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1029 by (simp add: card_cartesian_product)
  1030 
  1031 
  1032 subsection {* Generalized product over a set *}
  1033 
  1034 context comm_monoid_mult
  1035 begin
  1036 
  1037 definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  1038 where
  1039   "setprod = comm_monoid_set.F times 1"
  1040 
  1041 sublocale setprod!: comm_monoid_set times 1
  1042 where
  1043   "comm_monoid_set.F times 1 = setprod"
  1044 proof -
  1045   show "comm_monoid_set times 1" ..
  1046   then interpret setprod!: comm_monoid_set times 1 .
  1047   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  1048 qed
  1049 
  1050 abbreviation
  1051   Setprod ("\<Prod>_" [1000] 999) where
  1052   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1053 
  1054 end
  1055 
  1056 syntax
  1057   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1058 syntax (xsymbols)
  1059   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1060 syntax (HTML output)
  1061   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1062 
  1063 translations -- {* Beware of argument permutation! *}
  1064   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1065   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1066 
  1067 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1068  @{text"\<Prod>x|P. e"}. *}
  1069 
  1070 syntax
  1071   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1072 syntax (xsymbols)
  1073   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1074 syntax (HTML output)
  1075   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1076 
  1077 translations
  1078   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1079   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1080 
  1081 context comm_monoid_mult
  1082 begin
  1083 
  1084 lemma setprod_dvd_setprod: 
  1085   "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
  1086 proof (induct A rule: infinite_finite_induct)
  1087   case infinite then show ?case by (auto intro: dvdI)
  1088 next
  1089   case empty then show ?case by (auto intro: dvdI)
  1090 next
  1091   case (insert a A) then
  1092   have "f a dvd g a" and "setprod f A dvd setprod g A" by simp_all
  1093   then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s" by (auto elim!: dvdE)
  1094   then have "g a * setprod g A = f a * setprod f A * (r * s)" by (simp add: ac_simps)
  1095   with insert.hyps show ?case by (auto intro: dvdI)
  1096 qed
  1097 
  1098 lemma setprod_dvd_setprod_subset:
  1099   "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
  1100   by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
  1101 
  1102 end
  1103 
  1104 
  1105 subsubsection {* Properties in more restricted classes of structures *}
  1106 
  1107 context comm_semiring_1
  1108 begin
  1109 
  1110 lemma dvd_setprod_eqI [intro]:
  1111   assumes "finite A" and "a \<in> A" and "b = f a"
  1112   shows "b dvd setprod f A"
  1113 proof -
  1114   from `finite A` have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
  1115     by (intro setprod.insert) auto
  1116   also from `a \<in> A` have "insert a (A - {a}) = A" by blast
  1117   finally have "setprod f A = f a * setprod f (A - {a})" .
  1118   with `b = f a` show ?thesis by simp
  1119 qed
  1120 
  1121 lemma dvd_setprodI [intro]:
  1122   assumes "finite A" and "a \<in> A"
  1123   shows "f a dvd setprod f A"
  1124   using assms by auto
  1125 
  1126 lemma setprod_zero:
  1127   assumes "finite A" and "\<exists>a\<in>A. f a = 0"
  1128   shows "setprod f A = 0"
  1129 using assms proof (induct A)
  1130   case empty then show ?case by simp
  1131 next
  1132   case (insert a A)
  1133   then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
  1134   then have "f a * setprod f A = 0" by rule (simp_all add: insert)
  1135   with insert show ?case by simp
  1136 qed
  1137 
  1138 lemma setprod_dvd_setprod_subset2:
  1139   assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
  1140   shows "setprod f A dvd setprod g B"
  1141 proof -
  1142   from assms have "setprod f A dvd setprod g A"
  1143     by (auto intro: setprod_dvd_setprod)
  1144   moreover from assms have "setprod g A dvd setprod g B"
  1145     by (auto intro: setprod_dvd_setprod_subset)
  1146   ultimately show ?thesis by (rule dvd_trans)
  1147 qed
  1148 
  1149 end
  1150 
  1151 lemma setprod_zero_iff [simp]:
  1152   assumes "finite A"
  1153   shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
  1154   using assms by (induct A) (auto simp: no_zero_divisors)
  1155 
  1156 lemma (in field) setprod_diff1:
  1157   "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
  1158     (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
  1159   by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
  1160 
  1161 lemma (in field_inverse_zero) setprod_inversef: 
  1162   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1163   by (induct A rule: finite_induct) simp_all
  1164 
  1165 lemma (in field_inverse_zero) setprod_dividef:
  1166   "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
  1167   using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
  1168 
  1169 lemma setprod_Un:
  1170   fixes f :: "'b \<Rightarrow> 'a :: field"
  1171   assumes "finite A" and "finite B"
  1172   and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
  1173   shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
  1174 proof -
  1175   from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
  1176     by (simp add: setprod.union_inter [symmetric, of A B])
  1177   with assms show ?thesis by simp
  1178 qed
  1179 
  1180 lemma (in linordered_semidom) setprod_nonneg:
  1181   "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
  1182   by (induct A rule: infinite_finite_induct) simp_all
  1183 
  1184 lemma (in linordered_semidom) setprod_pos:
  1185   "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
  1186   by (induct A rule: infinite_finite_induct) simp_all
  1187 
  1188 lemma (in linordered_semidom) setprod_mono:
  1189   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1190   shows "setprod f A \<le> setprod g A"
  1191   using assms by (induct A rule: infinite_finite_induct)
  1192     (auto intro!: setprod_nonneg mult_mono)
  1193 
  1194 lemma (in linordered_field) abs_setprod:
  1195   "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
  1196   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
  1197 
  1198 lemma setprod_eq_1_iff [simp]:
  1199   "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
  1200   by (induct A rule: finite_induct) simp_all
  1201 
  1202 lemma setprod_pos_nat:
  1203   "finite A \<Longrightarrow> (\<forall>a\<in>A. f a > (0::nat)) \<Longrightarrow> setprod f A > 0"
  1204   using setprod_zero_iff by (simp del: neq0_conv add: neq0_conv [symmetric])
  1205 
  1206 lemma setprod_pos_nat_iff [simp]:
  1207   "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
  1208   using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
  1209 
  1210 end