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