src/HOL/Groups_Big.thy
author paulson <lp15@cam.ac.uk>
Mon Feb 22 14:37:56 2016 +0000 (2016-02-22)
changeset 62379 340738057c8c
parent 62378 85ed00c1fe7c
child 62481 b5d8e57826df
permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
     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 standard (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   \<comment> \<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 \<times> 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 sublocale setsum: comm_monoid_set plus 0
   471 defines
   472   setsum = setsum.F ..
   473 
   474 abbreviation Setsum ("\<Sum>_" [1000] 999)
   475   where "\<Sum>A \<equiv> setsum (\<lambda>x. x) A"
   476 
   477 end
   478 
   479 text \<open>Now: lot's of fancy syntax. First, @{term "setsum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
   480 
   481 syntax (ASCII)
   482   "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM _:_./ _)" [0, 51, 10] 10)
   483 syntax
   484   "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
   485 translations \<comment> \<open>Beware of argument permutation!\<close>
   486   "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST setsum (\<lambda>i. b) A"
   487 
   488 text \<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
   489 
   490 syntax (ASCII)
   491   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
   492 syntax
   493   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
   494 translations
   495   "\<Sum>x|P. t" => "CONST setsum (\<lambda>x. t) {x. P}"
   496 
   497 print_translation \<open>
   498 let
   499   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   500         if x <> y then raise Match
   501         else
   502           let
   503             val x' = Syntax_Trans.mark_bound_body (x, Tx);
   504             val t' = subst_bound (x', t);
   505             val P' = subst_bound (x', P);
   506           in
   507             Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   508           end
   509     | setsum_tr' _ = raise Match;
   510 in [(@{const_syntax setsum}, K setsum_tr')] end
   511 \<close>
   512 
   513 text \<open>TODO generalization candidates\<close>
   514 
   515 lemma (in comm_monoid_add) setsum_image_gen:
   516   assumes fS: "finite S"
   517   shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   518 proof-
   519   { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto }
   520   hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
   521     by simp
   522   also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   523     by (rule setsum.commute_restrict [OF fS finite_imageI [OF fS]])
   524   finally show ?thesis .
   525 qed
   526 
   527 
   528 subsubsection \<open>Properties in more restricted classes of structures\<close>
   529 
   530 lemma setsum_Un: "finite A ==> finite B ==>
   531   (setsum f (A Un B) :: 'a :: ab_group_add) =
   532    setsum f A + setsum f B - setsum f (A Int B)"
   533 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   534 
   535 lemma setsum_Un2:
   536   assumes "finite (A \<union> B)"
   537   shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
   538 proof -
   539   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   540     by auto
   541   with assms show ?thesis by simp (subst setsum.union_disjoint, auto)+
   542 qed
   543 
   544 lemma setsum_diff1: "finite A \<Longrightarrow>
   545   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   546   (if a:A then setsum f A - f a else setsum f A)"
   547 by (erule finite_induct) (auto simp add: insert_Diff_if)
   548 
   549 lemma setsum_diff:
   550   assumes le: "finite A" "B \<subseteq> A"
   551   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   552 proof -
   553   from le have finiteB: "finite B" using finite_subset by auto
   554   show ?thesis using finiteB le
   555   proof induct
   556     case empty
   557     thus ?case by auto
   558   next
   559     case (insert x F)
   560     thus ?case using le finiteB
   561       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   562   qed
   563 qed
   564 
   565 lemma (in ordered_comm_monoid_add) setsum_mono:
   566   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i"
   567   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   568 proof (cases "finite K")
   569   case True
   570   thus ?thesis using le
   571   proof induct
   572     case empty
   573     thus ?case by simp
   574   next
   575     case insert
   576     thus ?case using add_mono by fastforce
   577   qed
   578 next
   579   case False then show ?thesis by simp
   580 qed
   581 
   582 lemma (in strict_ordered_comm_monoid_add) setsum_strict_mono:
   583   assumes "finite A"  "A \<noteq> {}" and "\<And>x. x \<in> A \<Longrightarrow> f x < g x"
   584   shows "setsum f A < setsum g A"
   585   using assms
   586 proof (induct rule: finite_ne_induct)
   587   case singleton thus ?case by simp
   588 next
   589   case insert thus ?case by (auto simp: add_strict_mono)
   590 qed
   591 
   592 lemma setsum_strict_mono_ex1:
   593   fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add"
   594   assumes "finite A" and "\<forall>x\<in>A. f x \<le> g x" and "\<exists>a\<in>A. f a < g a"
   595   shows "setsum f A < setsum g A"
   596 proof-
   597   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   598   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   599     by(simp add:insert_absorb[OF \<open>a:A\<close>])
   600   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   601     using \<open>finite A\<close> by(subst setsum.union_disjoint) auto
   602   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   603     by(rule setsum_mono)(simp add: assms(2))
   604   also have "setsum f {a} < setsum g {a}" using a by simp
   605   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   606     using \<open>finite A\<close> by(subst setsum.union_disjoint[symmetric]) auto
   607   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF \<open>a:A\<close>])
   608   finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
   609 qed
   610 
   611 lemma setsum_negf: "(\<Sum>x\<in>A. - f x::'a::ab_group_add) = - (\<Sum>x\<in>A. f x)"
   612 proof (cases "finite A")
   613   case True thus ?thesis by (induct set: finite) auto
   614 next
   615   case False thus ?thesis by simp
   616 qed
   617 
   618 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)"
   619   using setsum.distrib [of f "- g" A] by (simp add: setsum_negf)
   620 
   621 lemma setsum_subtractf_nat:
   622   "(\<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)"
   623   by (induction A rule: infinite_finite_induct) (auto simp: setsum_mono)
   624 
   625 lemma (in ordered_comm_monoid_add) setsum_nonneg:
   626   assumes nn: "\<forall>x\<in>A. 0 \<le> f x"
   627   shows "0 \<le> setsum f A"
   628 proof (cases "finite A")
   629   case True thus ?thesis using nn
   630   proof induct
   631     case empty then show ?case by simp
   632   next
   633     case (insert x F)
   634     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   635     with insert show ?case by simp
   636   qed
   637 next
   638   case False thus ?thesis by simp
   639 qed
   640 
   641 lemma (in ordered_comm_monoid_add) setsum_nonpos:
   642   assumes np: "\<forall>x\<in>A. f x \<le> 0"
   643   shows "setsum f A \<le> 0"
   644 proof (cases "finite A")
   645   case True thus ?thesis using np
   646   proof induct
   647     case empty then show ?case by simp
   648   next
   649     case (insert x F)
   650     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   651     with insert show ?case by simp
   652   qed
   653 next
   654   case False thus ?thesis by simp
   655 qed
   656 
   657 lemma (in ordered_comm_monoid_add) setsum_nonneg_eq_0_iff:
   658   "finite A \<Longrightarrow> \<forall>x\<in>A. 0 \<le> f x \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   659   by (induct set: finite, simp) (simp add: add_nonneg_eq_0_iff setsum_nonneg)
   660 
   661 lemma (in ordered_comm_monoid_add) setsum_nonneg_0:
   662   "finite s \<Longrightarrow> (\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0) \<Longrightarrow> (\<Sum> i \<in> s. f i) = 0 \<Longrightarrow> i \<in> s \<Longrightarrow> f i = 0"
   663   by (simp add: setsum_nonneg_eq_0_iff)
   664 
   665 lemma (in ordered_comm_monoid_add) setsum_nonneg_leq_bound:
   666   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   667   shows "f i \<le> B"
   668 proof -
   669   have "f i \<le> f i + (\<Sum>i \<in> s - {i}. f i)"
   670     using assms by (intro add_increasing2 setsum_nonneg) auto
   671   also have "\<dots> = B"
   672     using setsum.remove[of s i f] assms by simp
   673   finally show ?thesis by auto
   674 qed
   675 
   676 lemma (in ordered_comm_monoid_add) setsum_mono2:
   677   assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   678   shows "setsum f A \<le> setsum f B"
   679 proof -
   680   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   681     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   682   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   683     by (simp add: setsum.union_disjoint del:Un_Diff_cancel)
   684   also have "A \<union> (B-A) = B" using sub by blast
   685   finally show ?thesis .
   686 qed
   687 
   688 lemma (in ordered_comm_monoid_add) setsum_le_included:
   689   assumes "finite s" "finite t"
   690   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)"
   691   shows "setsum f s \<le> setsum g t"
   692 proof -
   693   have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
   694   proof (rule setsum_mono)
   695     fix y assume "y \<in> s"
   696     with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
   697     with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
   698       using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
   699       by (auto intro!: setsum_mono2)
   700   qed
   701   also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
   702     using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
   703   also have "... \<le> setsum g t"
   704     using assms by (auto simp: setsum_image_gen[symmetric])
   705   finally show ?thesis .
   706 qed
   707 
   708 lemma (in ordered_comm_monoid_add) setsum_mono3:
   709   "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> \<forall>x\<in>B - A. 0 \<le> f x \<Longrightarrow> setsum f A \<le> setsum f B"
   710   by (rule setsum_mono2) auto
   711 
   712 lemma (in canonically_ordered_monoid_add) setsum_eq_0_iff [simp]:
   713   "finite F \<Longrightarrow> (setsum f F = 0) = (\<forall>a\<in>F. f a = 0)"
   714   by (intro ballI setsum_nonneg_eq_0_iff zero_le)
   715 
   716 lemma setsum_right_distrib:
   717   fixes f :: "'a => ('b::semiring_0)"
   718   shows "r * setsum f A = setsum (%n. r * f n) A"
   719 proof (cases "finite A")
   720   case True
   721   thus ?thesis
   722   proof induct
   723     case empty thus ?case by simp
   724   next
   725     case (insert x A) thus ?case by (simp add: distrib_left)
   726   qed
   727 next
   728   case False thus ?thesis by simp
   729 qed
   730 
   731 lemma setsum_left_distrib:
   732   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   733 proof (cases "finite A")
   734   case True
   735   then show ?thesis
   736   proof induct
   737     case empty thus ?case by simp
   738   next
   739     case (insert x A) thus ?case by (simp add: distrib_right)
   740   qed
   741 next
   742   case False thus ?thesis by simp
   743 qed
   744 
   745 lemma setsum_divide_distrib:
   746   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   747 proof (cases "finite A")
   748   case True
   749   then show ?thesis
   750   proof induct
   751     case empty thus ?case by simp
   752   next
   753     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   754   qed
   755 next
   756   case False thus ?thesis by simp
   757 qed
   758 
   759 lemma setsum_abs[iff]:
   760   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   761   shows "\<bar>setsum f A\<bar> \<le> setsum (%i. \<bar>f i\<bar>) A"
   762 proof (cases "finite A")
   763   case True
   764   thus ?thesis
   765   proof induct
   766     case empty thus ?case by simp
   767   next
   768     case (insert x A)
   769     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   770   qed
   771 next
   772   case False thus ?thesis by simp
   773 qed
   774 
   775 lemma setsum_abs_ge_zero[iff]:
   776   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   777   shows "0 \<le> setsum (%i. \<bar>f i\<bar>) A"
   778   by (simp add: setsum_nonneg)
   779 
   780 lemma abs_setsum_abs[simp]:
   781   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   782   shows "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
   783 proof (cases "finite A")
   784   case True
   785   thus ?thesis
   786   proof induct
   787     case empty thus ?case by simp
   788   next
   789     case (insert a A)
   790     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
   791     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   792     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   793       by (simp del: abs_of_nonneg)
   794     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   795     finally show ?case .
   796   qed
   797 next
   798   case False thus ?thesis by simp
   799 qed
   800 
   801 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   802   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   803   unfolding setsum.remove [OF assms] by auto
   804 
   805 lemma setsum_product:
   806   fixes f :: "'a => ('b::semiring_0)"
   807   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   808   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute)
   809 
   810 lemma setsum_mult_setsum_if_inj:
   811 fixes f :: "'a => ('b::semiring_0)"
   812 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   813   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   814 by(auto simp: setsum_product setsum.cartesian_product
   815         intro!:  setsum.reindex_cong[symmetric])
   816 
   817 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   818 apply (case_tac "finite A")
   819  prefer 2 apply simp
   820 apply (erule rev_mp)
   821 apply (erule finite_induct, auto)
   822 done
   823 
   824 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   825   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   826 apply(erule finite_induct)
   827 apply (auto simp add:add_is_1)
   828 done
   829 
   830 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   831 
   832 lemma setsum_Un_nat: "finite A ==> finite B ==>
   833   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   834   \<comment> \<open>For the natural numbers, we have subtraction.\<close>
   835 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   836 
   837 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   838   (if a:A then setsum f A - f a else setsum f A)"
   839 apply (case_tac "finite A")
   840  prefer 2 apply simp
   841 apply (erule finite_induct)
   842  apply (auto simp add: insert_Diff_if)
   843 apply (drule_tac a = a in mk_disjoint_insert, auto)
   844 done
   845 
   846 lemma setsum_diff_nat:
   847 assumes "finite B" and "B \<subseteq> A"
   848 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   849 using assms
   850 proof induct
   851   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   852 next
   853   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   854     and xFinA: "insert x F \<subseteq> A"
   855     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   856   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   857   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   858     by (simp add: setsum_diff1_nat)
   859   from xFinA have "F \<subseteq> A" by simp
   860   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   861   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   862     by simp
   863   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   864   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   865     by simp
   866   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   867   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   868     by simp
   869   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   870 qed
   871 
   872 lemma setsum_comp_morphism:
   873   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   874   shows "setsum (h \<circ> g) A = h (setsum g A)"
   875 proof (cases "finite A")
   876   case False then show ?thesis by (simp add: assms)
   877 next
   878   case True then show ?thesis by (induct A) (simp_all add: assms)
   879 qed
   880 
   881 lemma (in comm_semiring_1) dvd_setsum:
   882   "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
   883   by (induct A rule: infinite_finite_induct) simp_all
   884 
   885 lemma (in ordered_comm_monoid_add) setsum_pos:
   886   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
   887   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
   888 
   889 lemma (in ordered_comm_monoid_add) setsum_pos2:
   890   assumes I: "finite I" "i \<in> I" "0 < f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   891   shows "0 < setsum f I"
   892 proof -
   893   have "0 < f i + setsum f (I - {i})"
   894     using assms by (intro add_pos_nonneg setsum_nonneg) auto
   895   also have "\<dots> = setsum f I"
   896     using assms by (simp add: setsum.remove)
   897   finally show ?thesis .
   898 qed
   899 
   900 lemma setsum_cong_Suc:
   901   assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)"
   902   shows   "setsum f A = setsum g A"
   903 proof (rule setsum.cong)
   904   fix x assume "x \<in> A"
   905   with assms(1) show "f x = g x" by (cases x) (auto intro!: assms(2))
   906 qed simp_all
   907 
   908 
   909 subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
   910 
   911 lemma card_eq_setsum:
   912   "card A = setsum (\<lambda>x. 1) A"
   913 proof -
   914   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   915     by (simp add: fun_eq_iff)
   916   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   917     by (rule arg_cong)
   918   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   919     by (blast intro: fun_cong)
   920   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   921 qed
   922 
   923 lemma setsum_constant [simp]:
   924   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   925 apply (cases "finite A")
   926 apply (erule finite_induct)
   927 apply (auto simp add: algebra_simps)
   928 done
   929 
   930 lemma setsum_Suc: "setsum (\<lambda>x. Suc(f x)) A = setsum f A + card A"
   931   using setsum.distrib[of f "\<lambda>_. 1" A]
   932   by simp
   933 
   934 lemma setsum_bounded_above:
   935   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_comm_monoid_add})"
   936   shows "setsum f A \<le> of_nat (card A) * K"
   937 proof (cases "finite A")
   938   case True
   939   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   940 next
   941   case False thus ?thesis by simp
   942 qed
   943 
   944 lemma setsum_bounded_above_strict:
   945   assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_comm_monoid_add,semiring_1})"
   946           "card A > 0"
   947   shows "setsum f A < of_nat (card A) * K"
   948 using assms setsum_strict_mono[where A=A and g = "%x. K"]
   949 by (simp add: card_gt_0_iff)
   950 
   951 lemma setsum_bounded_below:
   952   assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_comm_monoid_add}) \<le> f i"
   953   shows "of_nat (card A) * K \<le> setsum f A"
   954 proof (cases "finite A")
   955   case True
   956   thus ?thesis using le setsum_mono[where K=A and f = "%x. K"] by simp
   957 next
   958   case False thus ?thesis by simp
   959 qed
   960 
   961 lemma card_UN_disjoint:
   962   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   963     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   964   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   965 proof -
   966   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   967   with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant)
   968 qed
   969 
   970 lemma card_Union_disjoint:
   971   "finite C ==> (ALL A:C. finite A) ==>
   972    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
   973    ==> card (\<Union>C) = setsum card C"
   974 apply (frule card_UN_disjoint [of C id])
   975 apply simp_all
   976 done
   977 
   978 lemma setsum_multicount_gen:
   979   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   980   shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
   981 proof-
   982   have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
   983   also have "\<dots> = ?r" unfolding setsum.commute_restrict [OF assms(1-2)]
   984     using assms(3) by auto
   985   finally show ?thesis .
   986 qed
   987 
   988 lemma setsum_multicount:
   989   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
   990   shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
   991 proof-
   992   have "?l = setsum (\<lambda>i. k) T" by (rule setsum_multicount_gen) (auto simp: assms)
   993   also have "\<dots> = ?r" by (simp add: mult.commute)
   994   finally show ?thesis by auto
   995 qed
   996 
   997 subsubsection \<open>Cardinality of products\<close>
   998 
   999 lemma card_SigmaI [simp]:
  1000   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1001   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1002 by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant)
  1003 
  1004 (*
  1005 lemma SigmaI_insert: "y \<notin> A ==>
  1006   (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))"
  1007   by auto
  1008 *)
  1009 
  1010 lemma card_cartesian_product: "card (A \<times> B) = card(A) * card(B)"
  1011   by (cases "finite A \<and> finite B")
  1012     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1013 
  1014 lemma card_cartesian_product_singleton:  "card({x} \<times> A) = card(A)"
  1015 by (simp add: card_cartesian_product)
  1016 
  1017 
  1018 subsection \<open>Generalized product over a set\<close>
  1019 
  1020 context comm_monoid_mult
  1021 begin
  1022 
  1023 sublocale setprod: comm_monoid_set times 1
  1024 defines
  1025   setprod = setprod.F ..
  1026 
  1027 abbreviation
  1028   Setprod ("\<Prod>_" [1000] 999) where
  1029   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1030 
  1031 end
  1032 
  1033 syntax (ASCII)
  1034   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
  1035 syntax
  1036   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
  1037 translations \<comment> \<open>Beware of argument permutation!\<close>
  1038   "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A"
  1039 
  1040 text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
  1041 
  1042 syntax (ASCII)
  1043   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
  1044 syntax
  1045   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
  1046 translations
  1047   "\<Prod>x|P. t" => "CONST setprod (\<lambda>x. t) {x. P}"
  1048 
  1049 context comm_monoid_mult
  1050 begin
  1051 
  1052 lemma setprod_dvd_setprod:
  1053   "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> setprod f A dvd setprod g A"
  1054 proof (induct A rule: infinite_finite_induct)
  1055   case infinite then show ?case by (auto intro: dvdI)
  1056 next
  1057   case empty then show ?case by (auto intro: dvdI)
  1058 next
  1059   case (insert a A) then
  1060   have "f a dvd g a" and "setprod f A dvd setprod g A" by simp_all
  1061   then obtain r s where "g a = f a * r" and "setprod g A = setprod f A * s" by (auto elim!: dvdE)
  1062   then have "g a * setprod g A = f a * setprod f A * (r * s)" by (simp add: ac_simps)
  1063   with insert.hyps show ?case by (auto intro: dvdI)
  1064 qed
  1065 
  1066 lemma setprod_dvd_setprod_subset:
  1067   "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> setprod f A dvd setprod f B"
  1068   by (auto simp add: setprod.subset_diff ac_simps intro: dvdI)
  1069 
  1070 end
  1071 
  1072 
  1073 subsubsection \<open>Properties in more restricted classes of structures\<close>
  1074 
  1075 context comm_semiring_1
  1076 begin
  1077 
  1078 lemma dvd_setprod_eqI [intro]:
  1079   assumes "finite A" and "a \<in> A" and "b = f a"
  1080   shows "b dvd setprod f A"
  1081 proof -
  1082   from \<open>finite A\<close> have "setprod f (insert a (A - {a})) = f a * setprod f (A - {a})"
  1083     by (intro setprod.insert) auto
  1084   also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A" by blast
  1085   finally have "setprod f A = f a * setprod f (A - {a})" .
  1086   with \<open>b = f a\<close> show ?thesis by simp
  1087 qed
  1088 
  1089 lemma dvd_setprodI [intro]:
  1090   assumes "finite A" and "a \<in> A"
  1091   shows "f a dvd setprod f A"
  1092   using assms by auto
  1093 
  1094 lemma setprod_zero:
  1095   assumes "finite A" and "\<exists>a\<in>A. f a = 0"
  1096   shows "setprod f A = 0"
  1097 using assms proof (induct A)
  1098   case empty then show ?case by simp
  1099 next
  1100   case (insert a A)
  1101   then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
  1102   then have "f a * setprod f A = 0" by rule (simp_all add: insert)
  1103   with insert show ?case by simp
  1104 qed
  1105 
  1106 lemma setprod_dvd_setprod_subset2:
  1107   assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
  1108   shows "setprod f A dvd setprod g B"
  1109 proof -
  1110   from assms have "setprod f A dvd setprod g A"
  1111     by (auto intro: setprod_dvd_setprod)
  1112   moreover from assms have "setprod g A dvd setprod g B"
  1113     by (auto intro: setprod_dvd_setprod_subset)
  1114   ultimately show ?thesis by (rule dvd_trans)
  1115 qed
  1116 
  1117 end
  1118 
  1119 lemma setprod_zero_iff [simp]:
  1120   assumes "finite A"
  1121   shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
  1122   using assms by (induct A) (auto simp: no_zero_divisors)
  1123 
  1124 lemma (in semidom_divide) setprod_diff1:
  1125   assumes "finite A" and "f a \<noteq> 0"
  1126   shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
  1127 proof (cases "a \<notin> A")
  1128   case True then show ?thesis by simp
  1129 next
  1130   case False with assms show ?thesis
  1131   proof (induct A rule: finite_induct)
  1132     case empty then show ?case by simp
  1133   next
  1134     case (insert b B)
  1135     then show ?case
  1136     proof (cases "a = b")
  1137       case True with insert show ?thesis by simp
  1138     next
  1139       case False with insert have "a \<in> B" by simp
  1140       def C \<equiv> "B - {a}"
  1141       with \<open>finite B\<close> \<open>a \<in> B\<close>
  1142         have *: "B = insert a C" "finite C" "a \<notin> C" by auto
  1143       with insert show ?thesis by (auto simp add: insert_commute ac_simps)
  1144     qed
  1145   qed
  1146 qed
  1147 
  1148 lemma (in field) setprod_inversef:
  1149   "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1150   by (induct A rule: finite_induct) simp_all
  1151 
  1152 lemma (in field) setprod_dividef:
  1153   "finite A \<Longrightarrow> (\<Prod>x\<in>A. f x / g x) = setprod f A / setprod g A"
  1154   using setprod_inversef [of A g] by (simp add: divide_inverse setprod.distrib)
  1155 
  1156 lemma setprod_Un:
  1157   fixes f :: "'b \<Rightarrow> 'a :: field"
  1158   assumes "finite A" and "finite B"
  1159   and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
  1160   shows "setprod f (A \<union> B) = setprod f A * setprod f B / setprod f (A \<inter> B)"
  1161 proof -
  1162   from assms have "setprod f A * setprod f B = setprod f (A \<union> B) * setprod f (A \<inter> B)"
  1163     by (simp add: setprod.union_inter [symmetric, of A B])
  1164   with assms show ?thesis by simp
  1165 qed
  1166 
  1167 lemma (in linordered_semidom) setprod_nonneg:
  1168   "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> setprod f A"
  1169   by (induct A rule: infinite_finite_induct) simp_all
  1170 
  1171 lemma (in linordered_semidom) setprod_pos:
  1172   "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < setprod f A"
  1173   by (induct A rule: infinite_finite_induct) simp_all
  1174 
  1175 lemma (in linordered_semidom) setprod_mono:
  1176   "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> setprod f A \<le> setprod g A"
  1177   by (induct A rule: infinite_finite_induct) (auto intro!: setprod_nonneg mult_mono)
  1178 
  1179 lemma (in linordered_semidom) setprod_mono_strict:
  1180     assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
  1181     shows "setprod f A < setprod g A"
  1182 using assms
  1183 apply (induct A rule: finite_induct)
  1184 apply (simp add: )
  1185 apply (force intro: mult_strict_mono' setprod_nonneg)
  1186 done
  1187 
  1188 lemma (in linordered_field) abs_setprod:
  1189   "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
  1190   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
  1191 
  1192 lemma setprod_eq_1_iff [simp]:
  1193   "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
  1194   by (induct A rule: finite_induct) simp_all
  1195 
  1196 lemma setprod_pos_nat_iff [simp]:
  1197   "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
  1198   using setprod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
  1199 
  1200 end