src/HOL/Groups_Big.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 61032 b57df8eecad6
child 61169 4de9ff3ea29a
permissions -rw-r--r--
prefer symbols;
     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 \<open>Big sum and product over finite (non-empty) sets\<close>
     7 
     8 theory Groups_Big
     9 imports Finite_Set
    10 begin
    11 
    12 subsection \<open>Generic monoid operation over a set\<close>
    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 \<open>x \<in> A\<close> obtain B where A: "A = insert x B" and "x \<notin> B"
    48     by (auto dest: mk_disjoint_insert)
    49   moreover from \<open>finite A\<close> 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   -- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
    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 \<open>A = B\<close>
   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 (case_prod 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 \<open>S \<subseteq> T\<close> by blast
   211   have d: "S \<inter> (T - S) = {}" using \<open>S \<subseteq> T\<close> by blast
   212   from \<open>finite T\<close> \<open>S \<subseteq> T\<close> 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 \<open>finite S\<close> 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 \<open>finite A\<close>, 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 (case_prod 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 \<open>finite A\<close>
   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 \<open>finite B\<close> \<open>A \<notin> B\<close> 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 \<open>finite C\<close> 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 \<open>finite A\<close> \<open>finite (C - A)\<close> 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 \<open>finite B\<close> \<open>finite (C - B)\<close> 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 \<open>Generalized summation over a set\<close>
   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\<open>Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   490 written @{text"\<Sum>x\<in>A. e"}.\<close>
   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"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
   496 syntax (HTML output)
   497   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
   498 
   499 translations -- \<open>Beware of argument permutation!\<close>
   500   "SUM i:A. b" == "CONST setsum (%i. b) A"
   501   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   502 
   503 text\<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   504  @{text"\<Sum>x|P. e"}.\<close>
   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" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
   510 syntax (HTML output)
   511   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<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 \<open>
   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 \<close>
   532 
   533 text \<open>TODO generalization candidates\<close>
   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 \<open>Properties in more restricted classes of structures\<close>
   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 \<open>a:A\<close>])
   622   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   623     using \<open>finite A\<close> 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 \<open>finite A\<close> by(subst setsum.union_disjoint[symmetric]) auto
   629   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF \<open>a:A\<close>])
   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   by (simp add: setsum_nonneg)
   814 
   815 lemma abs_setsum_abs[simp]: 
   816   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   817   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   818 proof (cases "finite A")
   819   case True
   820   thus ?thesis
   821   proof induct
   822     case empty thus ?case by simp
   823   next
   824     case (insert a A)
   825     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
   826     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   827     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   828       by (simp del: abs_of_nonneg)
   829     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   830     finally show ?case .
   831   qed
   832 next
   833   case False thus ?thesis by simp
   834 qed
   835 
   836 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   837   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   838   unfolding setsum.remove [OF assms] by auto
   839 
   840 lemma setsum_product:
   841   fixes f :: "'a => ('b::semiring_0)"
   842   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   843   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute)
   844 
   845 lemma setsum_mult_setsum_if_inj:
   846 fixes f :: "'a => ('b::semiring_0)"
   847 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   848   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   849 by(auto simp: setsum_product setsum.cartesian_product
   850         intro!:  setsum.reindex_cong[symmetric])
   851 
   852 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   853 apply (case_tac "finite A")
   854  prefer 2 apply simp
   855 apply (erule rev_mp)
   856 apply (erule finite_induct, auto)
   857 done
   858 
   859 lemma setsum_eq_0_iff [simp]:
   860   "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   861   by (induct set: finite) auto
   862 
   863 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   864   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   865 apply(erule finite_induct)
   866 apply (auto simp add:add_is_1)
   867 done
   868 
   869 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   870 
   871 lemma setsum_Un_nat: "finite A ==> finite B ==>
   872   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   873   -- \<open>For the natural numbers, we have subtraction.\<close>
   874 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   875 
   876 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   877   (if a:A then setsum f A - f a else setsum f A)"
   878 apply (case_tac "finite A")
   879  prefer 2 apply simp
   880 apply (erule finite_induct)
   881  apply (auto simp add: insert_Diff_if)
   882 apply (drule_tac a = a in mk_disjoint_insert, auto)
   883 done
   884 
   885 lemma setsum_diff_nat: 
   886 assumes "finite B" and "B \<subseteq> A"
   887 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   888 using assms
   889 proof induct
   890   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   891 next
   892   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   893     and xFinA: "insert x F \<subseteq> A"
   894     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   895   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   896   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   897     by (simp add: setsum_diff1_nat)
   898   from xFinA have "F \<subseteq> A" by simp
   899   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   900   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   901     by simp
   902   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   903   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   904     by simp
   905   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   906   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   907     by simp
   908   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   909 qed
   910 
   911 lemma setsum_comp_morphism:
   912   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   913   shows "setsum (h \<circ> g) A = h (setsum g A)"
   914 proof (cases "finite A")
   915   case False then show ?thesis by (simp add: assms)
   916 next
   917   case True then show ?thesis by (induct A) (simp_all add: assms)
   918 qed
   919 
   920 lemma (in comm_semiring_1) dvd_setsum:
   921   "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
   922   by (induct A rule: infinite_finite_induct) simp_all
   923 
   924 lemma setsum_pos2:
   925     assumes "finite I" "i \<in> I" "0 < f i" "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i)"
   926       shows "(0::'a::{ordered_ab_group_add,comm_monoid_add}) < setsum f I"
   927 proof -
   928   have "0 \<le> setsum f (I-{i})"
   929     using assms by (simp add: setsum_nonneg)
   930   also have "... < setsum f (I-{i}) + f i"
   931     using assms by auto
   932   also have "... = setsum f I"
   933     using assms by (simp add: setsum.remove)
   934   finally show ?thesis .
   935 qed
   936 
   937 
   938 subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
   939 
   940 lemma card_eq_setsum:
   941   "card A = setsum (\<lambda>x. 1) A"
   942 proof -
   943   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   944     by (simp add: fun_eq_iff)
   945   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   946     by (rule arg_cong)
   947   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   948     by (blast intro: fun_cong)
   949   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   950 qed
   951 
   952 lemma setsum_constant [simp]:
   953   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   954 apply (cases "finite A")
   955 apply (erule finite_induct)
   956 apply (auto simp add: algebra_simps)
   957 done
   958 
   959 lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
   960   using setsum.distrib[of f "\<lambda>_. 1" A] 
   961   by simp
   962 
   963 lemma setsum_bounded_above:
   964   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   965   shows "setsum f A \<le> of_nat (card A) * K"
   966 proof (cases "finite A")
   967   case True
   968   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   969 next
   970   case False thus ?thesis by simp
   971 qed
   972 
   973 lemma setsum_bounded_above_strict:
   974   assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_ab_semigroup_add,semiring_1})"
   975           "card A > 0"
   976   shows "setsum f A < of_nat (card A) * K"
   977 using assms setsum_strict_mono[where A=A and g = "%x. K"]
   978 by (simp add: card_gt_0_iff)
   979 
   980 lemma setsum_bounded_below:
   981   assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_ab_semigroup_add}) \<le> f i"
   982   shows "of_nat (card A) * K \<le> setsum f A"
   983 proof (cases "finite A")
   984   case True
   985   thus ?thesis using le setsum_mono[where K=A and f = "%x. K"] by simp
   986 next
   987   case False thus ?thesis by simp
   988 qed
   989 
   990 lemma card_UN_disjoint:
   991   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   992     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   993   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   994 proof -
   995   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   996   with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant)
   997 qed
   998 
   999 lemma card_Union_disjoint:
  1000   "finite C ==> (ALL A:C. finite A) ==>
  1001    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  1002    ==> card (Union C) = setsum card C"
  1003 apply (frule card_UN_disjoint [of C id])
  1004 apply simp_all
  1005 done
  1006 
  1007 lemma setsum_multicount_gen:
  1008   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
  1009   shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
  1010 proof-
  1011   have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
  1012   also have "\<dots> = ?r" unfolding setsum.commute_restrict [OF assms(1-2)]
  1013     using assms(3) by auto
  1014   finally show ?thesis .
  1015 qed
  1016 
  1017 lemma setsum_multicount:
  1018   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
  1019   shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
  1020 proof-
  1021   have "?l = setsum (\<lambda>i. k) T" by (rule setsum_multicount_gen) (auto simp: assms)
  1022   also have "\<dots> = ?r" by (simp add: mult.commute)
  1023   finally show ?thesis by auto
  1024 qed
  1025 
  1026 lemma (in ordered_comm_monoid_add) setsum_pos: 
  1027   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
  1028   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
  1029 
  1030 
  1031 subsubsection \<open>Cardinality of products\<close>
  1032 
  1033 lemma card_SigmaI [simp]:
  1034   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1035   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1036 by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant)
  1037 
  1038 (*
  1039 lemma SigmaI_insert: "y \<notin> A ==>
  1040   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1041   by auto
  1042 *)
  1043 
  1044 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1045   by (cases "finite A \<and> finite B")
  1046     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1047 
  1048 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1049 by (simp add: card_cartesian_product)
  1050 
  1051 
  1052 subsection \<open>Generalized product over a set\<close>
  1053 
  1054 context comm_monoid_mult
  1055 begin
  1056 
  1057 definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  1058 where
  1059   "setprod = comm_monoid_set.F times 1"
  1060 
  1061 sublocale setprod!: comm_monoid_set times 1
  1062 where
  1063   "comm_monoid_set.F times 1 = setprod"
  1064 proof -
  1065   show "comm_monoid_set times 1" ..
  1066   then interpret setprod!: comm_monoid_set times 1 .
  1067   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  1068 qed
  1069 
  1070 abbreviation
  1071   Setprod ("\<Prod>_" [1000] 999) where
  1072   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1073 
  1074 end
  1075 
  1076 syntax
  1077   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
  1078 syntax (xsymbols)
  1079   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
  1080 syntax (HTML output)
  1081   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
  1082 
  1083 translations -- \<open>Beware of argument permutation!\<close>
  1084   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1085   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1086 
  1087 text\<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1088  @{text"\<Prod>x|P. e"}.\<close>
  1089 
  1090 syntax
  1091   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
  1092 syntax (xsymbols)
  1093   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1094 syntax (HTML output)
  1095   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1096 
  1097 translations
  1098   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1099   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1100 
  1101 context comm_monoid_mult
  1102 begin
  1103 
  1104 lemma setprod_dvd_setprod: 
  1105   "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
  1106 proof (induct A rule: infinite_finite_induct)
  1107   case infinite then show ?case by (auto intro: dvdI)
  1108 next
  1109   case empty then show ?case by (auto intro: dvdI)
  1110 next
  1111   case (insert a A) then
  1112   have "f a dvd g a" and "setprod f A dvd setprod g A" by simp_all
  1113   then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s" by (auto elim!: dvdE)
  1114   then have "g a * setprod g A = f a * setprod f A * (r * s)" by (simp add: ac_simps)
  1115   with insert.hyps show ?case by (auto intro: dvdI)
  1116 qed
  1117 
  1118 lemma setprod_dvd_setprod_subset:
  1119   "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
  1120   by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
  1121 
  1122 end
  1123 
  1124 
  1125 subsubsection \<open>Properties in more restricted classes of structures\<close>
  1126 
  1127 context comm_semiring_1
  1128 begin
  1129 
  1130 lemma dvd_setprod_eqI [intro]:
  1131   assumes "finite A" and "a \<in> A" and "b = f a"
  1132   shows "b dvd setprod f A"
  1133 proof -
  1134   from \<open>finite A\<close> have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
  1135     by (intro setprod.insert) auto
  1136   also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A" by blast
  1137   finally have "setprod f A = f a * setprod f (A - {a})" .
  1138   with \<open>b = f a\<close> show ?thesis by simp
  1139 qed
  1140 
  1141 lemma dvd_setprodI [intro]:
  1142   assumes "finite A" and "a \<in> A"
  1143   shows "f a dvd setprod f A"
  1144   using assms by auto
  1145 
  1146 lemma setprod_zero:
  1147   assumes "finite A" and "\<exists>a\<in>A. f a = 0"
  1148   shows "setprod f A = 0"
  1149 using assms proof (induct A)
  1150   case empty then show ?case by simp
  1151 next
  1152   case (insert a A)
  1153   then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
  1154   then have "f a * setprod f A = 0" by rule (simp_all add: insert)
  1155   with insert show ?case by simp
  1156 qed
  1157 
  1158 lemma setprod_dvd_setprod_subset2:
  1159   assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
  1160   shows "setprod f A dvd setprod g B"
  1161 proof -
  1162   from assms have "setprod f A dvd setprod g A"
  1163     by (auto intro: setprod_dvd_setprod)
  1164   moreover from assms have "setprod g A dvd setprod g B"
  1165     by (auto intro: setprod_dvd_setprod_subset)
  1166   ultimately show ?thesis by (rule dvd_trans)
  1167 qed
  1168 
  1169 end
  1170 
  1171 lemma setprod_zero_iff [simp]:
  1172   assumes "finite A"
  1173   shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
  1174   using assms by (induct A) (auto simp: no_zero_divisors)
  1175 
  1176 lemma (in semidom_divide) setprod_diff1:
  1177   assumes "finite A" and "f a \<noteq> 0"
  1178   shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
  1179 proof (cases "a \<notin> A")
  1180   case True then show ?thesis by simp
  1181 next
  1182   case False with assms show ?thesis
  1183   proof (induct A rule: finite_induct)
  1184     case empty then show ?case by simp
  1185   next
  1186     case (insert b B)
  1187     then show ?case
  1188     proof (cases "a = b")
  1189       case True with insert show ?thesis by simp
  1190     next
  1191       case False with insert have "a \<in> B" by simp
  1192       def C \<equiv> "B - {a}"
  1193       with \<open>finite B\<close> \<open>a \<in> B\<close>
  1194         have *: "B = insert a C" "finite C" "a \<notin> C" by auto
  1195       with insert show ?thesis by (auto simp add: insert_commute ac_simps)
  1196     qed
  1197   qed
  1198 qed
  1199 
  1200 lemma (in field) setprod_inversef: 
  1201   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1202   by (induct A rule: finite_induct) simp_all
  1203 
  1204 lemma (in field) setprod_dividef:
  1205   "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
  1206   using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
  1207 
  1208 lemma setprod_Un:
  1209   fixes f :: "'b \<Rightarrow> 'a :: field"
  1210   assumes "finite A" and "finite B"
  1211   and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
  1212   shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
  1213 proof -
  1214   from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
  1215     by (simp add: setprod.union_inter [symmetric, of A B])
  1216   with assms show ?thesis by simp
  1217 qed
  1218 
  1219 lemma (in linordered_semidom) setprod_nonneg:
  1220   "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
  1221   by (induct A rule: infinite_finite_induct) simp_all
  1222 
  1223 lemma (in linordered_semidom) setprod_pos:
  1224   "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
  1225   by (induct A rule: infinite_finite_induct) simp_all
  1226 
  1227 lemma (in linordered_semidom) setprod_mono:
  1228   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1229   shows "setprod f A \<le> setprod g A"
  1230   using assms by (induct A rule: infinite_finite_induct)
  1231     (auto intro!: setprod_nonneg mult_mono)
  1232 
  1233 lemma (in linordered_semidom) setprod_mono_strict:
  1234     assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
  1235     shows "setprod f A < setprod g A"
  1236 using assms 
  1237 apply (induct A rule: finite_induct)
  1238 apply (simp add: )
  1239 apply (force intro: mult_strict_mono' setprod_nonneg)
  1240 done
  1241 
  1242 lemma (in linordered_field) abs_setprod:
  1243   "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
  1244   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
  1245 
  1246 lemma setprod_eq_1_iff [simp]:
  1247   "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
  1248   by (induct A rule: finite_induct) simp_all
  1249 
  1250 lemma setprod_pos_nat_iff [simp]:
  1251   "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
  1252   using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
  1253 
  1254 lemma setsum_nonneg_eq_0_iff:
  1255   fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
  1256   shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
  1257   apply (induct set: finite, simp)
  1258   apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
  1259   done
  1260 
  1261 end