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