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