src/HOL/Groups_Big.thy
author haftmann
Sat Jun 28 09:16:42 2014 +0200 (2014-06-28)
changeset 57418 6ab1c7cb0b8d
parent 57275 0ddb5b755cdc
child 57512 cc97b347b301
permissions -rw-r--r--
fact consolidation
     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 header {* Big sum and product over finite (non-empty) sets *}
     7 
     8 theory Groups_Big
     9 imports Finite_Set
    10 begin
    11 
    12 subsection {* Generic monoid operation over a set *}
    13 
    14 no_notation times (infixl "*" 70)
    15 no_notation Groups.one ("1")
    16 
    17 locale comm_monoid_set = comm_monoid
    18 begin
    19 
    20 interpretation comp_fun_commute f
    21   by default (simp add: fun_eq_iff left_commute)
    22 
    23 interpretation comp?: comp_fun_commute "f \<circ> g"
    24   by (fact comp_comp_fun_commute)
    25 
    26 definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    27 where
    28   eq_fold: "F g A = Finite_Set.fold (f \<circ> g) 1 A"
    29 
    30 lemma infinite [simp]:
    31   "\<not> finite A \<Longrightarrow> F g A = 1"
    32   by (simp add: eq_fold)
    33 
    34 lemma empty [simp]:
    35   "F g {} = 1"
    36   by (simp add: eq_fold)
    37 
    38 lemma insert [simp]:
    39   assumes "finite A" and "x \<notin> A"
    40   shows "F g (insert x A) = g x * F g A"
    41   using assms by (simp add: eq_fold)
    42 
    43 lemma remove:
    44   assumes "finite A" and "x \<in> A"
    45   shows "F g A = g x * F g (A - {x})"
    46 proof -
    47   from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
    48     by (auto dest: mk_disjoint_insert)
    49   moreover from `finite A` 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   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
    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 `A = B`
   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 (split 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 `S \<subseteq> T` by blast
   211   have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
   212   from `finite T` `S \<subseteq> T` 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 `finite S` 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 `finite A`, 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 (split g) (A <*> B)"
   354 apply (rule sym)
   355 apply (cases "finite A") 
   356  apply (cases "finite B") 
   357   apply (simp add: Sigma)
   358  apply (cases "A={}", simp)
   359  apply simp
   360 apply (auto intro: infinite dest: finite_cartesian_productD2)
   361 apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
   362 done
   363 
   364 lemma inter_restrict:
   365   assumes "finite A"
   366   shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else 1) A"
   367 proof -
   368   let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else 1"
   369   have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else 1) = 1"
   370    by simp
   371   moreover have "A \<inter> B \<subseteq> A" by blast
   372   ultimately have "F ?g (A \<inter> B) = F ?g A" using `finite A`
   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 `finite B` `A \<notin> B` 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 end
   428 
   429 notation times (infixl "*" 70)
   430 notation Groups.one ("1")
   431 
   432 
   433 subsection {* Generalized summation over a set *}
   434 
   435 context comm_monoid_add
   436 begin
   437 
   438 definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   439 where
   440   "setsum = comm_monoid_set.F plus 0"
   441 
   442 sublocale setsum!: comm_monoid_set plus 0
   443 where
   444   "comm_monoid_set.F plus 0 = setsum"
   445 proof -
   446   show "comm_monoid_set plus 0" ..
   447   then interpret setsum!: comm_monoid_set plus 0 .
   448   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   449 qed
   450 
   451 abbreviation
   452   Setsum ("\<Sum>_" [1000] 999) where
   453   "\<Sum>A \<equiv> setsum (%x. x) A"
   454 
   455 end
   456 
   457 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   458 written @{text"\<Sum>x\<in>A. e"}. *}
   459 
   460 syntax
   461   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   462 syntax (xsymbols)
   463   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   464 syntax (HTML output)
   465   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   466 
   467 translations -- {* Beware of argument permutation! *}
   468   "SUM i:A. b" == "CONST setsum (%i. b) A"
   469   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   470 
   471 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   472  @{text"\<Sum>x|P. e"}. *}
   473 
   474 syntax
   475   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   476 syntax (xsymbols)
   477   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   478 syntax (HTML output)
   479   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   480 
   481 translations
   482   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   483   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   484 
   485 print_translation {*
   486 let
   487   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   488         if x <> y then raise Match
   489         else
   490           let
   491             val x' = Syntax_Trans.mark_bound_body (x, Tx);
   492             val t' = subst_bound (x', t);
   493             val P' = subst_bound (x', P);
   494           in
   495             Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   496           end
   497     | setsum_tr' _ = raise Match;
   498 in [(@{const_syntax setsum}, K setsum_tr')] end
   499 *}
   500 
   501 text {* TODO generalization candidates *}
   502 
   503 lemma setsum_image_gen:
   504   assumes fS: "finite S"
   505   shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   506 proof-
   507   { fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto }
   508   hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
   509     by simp
   510   also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   511     by (rule setsum.commute_restrict [OF fS finite_imageI [OF fS]])
   512   finally show ?thesis .
   513 qed
   514 
   515 
   516 subsubsection {* Properties in more restricted classes of structures *}
   517 
   518 lemma setsum_Un: "finite A ==> finite B ==>
   519   (setsum f (A Un B) :: 'a :: ab_group_add) =
   520    setsum f A + setsum f B - setsum f (A Int B)"
   521 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   522 
   523 lemma setsum_Un2:
   524   assumes "finite (A \<union> B)"
   525   shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
   526 proof -
   527   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   528     by auto
   529   with assms show ?thesis by simp (subst setsum.union_disjoint, auto)+
   530 qed
   531 
   532 lemma setsum_diff1: "finite A \<Longrightarrow>
   533   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   534   (if a:A then setsum f A - f a else setsum f A)"
   535 by (erule finite_induct) (auto simp add: insert_Diff_if)
   536 
   537 lemma setsum_diff:
   538   assumes le: "finite A" "B \<subseteq> A"
   539   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   540 proof -
   541   from le have finiteB: "finite B" using finite_subset by auto
   542   show ?thesis using finiteB le
   543   proof induct
   544     case empty
   545     thus ?case by auto
   546   next
   547     case (insert x F)
   548     thus ?case using le finiteB 
   549       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   550   qed
   551 qed
   552 
   553 lemma setsum_mono:
   554   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   555   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   556 proof (cases "finite K")
   557   case True
   558   thus ?thesis using le
   559   proof induct
   560     case empty
   561     thus ?case by simp
   562   next
   563     case insert
   564     thus ?case using add_mono by fastforce
   565   qed
   566 next
   567   case False then show ?thesis by simp
   568 qed
   569 
   570 lemma setsum_strict_mono:
   571   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   572   assumes "finite A"  "A \<noteq> {}"
   573     and "!!x. x:A \<Longrightarrow> f x < g x"
   574   shows "setsum f A < setsum g A"
   575   using assms
   576 proof (induct rule: finite_ne_induct)
   577   case singleton thus ?case by simp
   578 next
   579   case insert thus ?case by (auto simp: add_strict_mono)
   580 qed
   581 
   582 lemma setsum_strict_mono_ex1:
   583 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   584 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   585 shows "setsum f A < setsum g A"
   586 proof-
   587   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   588   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   589     by(simp add:insert_absorb[OF `a:A`])
   590   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   591     using `finite A` by(subst setsum.union_disjoint) auto
   592   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   593     by(rule setsum_mono)(simp add: assms(2))
   594   also have "setsum f {a} < setsum g {a}" using a by simp
   595   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   596     using `finite A` by(subst setsum.union_disjoint[symmetric]) auto
   597   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   598   finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
   599 qed
   600 
   601 lemma setsum_negf:
   602   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   603 proof (cases "finite A")
   604   case True thus ?thesis by (induct set: finite) auto
   605 next
   606   case False thus ?thesis by simp
   607 qed
   608 
   609 lemma setsum_subtractf:
   610   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   611     setsum f A - setsum g A"
   612   using setsum.distrib [of f "- g" A] by (simp add: setsum_negf)
   613 
   614 lemma setsum_nonneg:
   615   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   616   shows "0 \<le> setsum f A"
   617 proof (cases "finite A")
   618   case True thus ?thesis using nn
   619   proof induct
   620     case empty then show ?case by simp
   621   next
   622     case (insert x F)
   623     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   624     with insert show ?case by simp
   625   qed
   626 next
   627   case False thus ?thesis by simp
   628 qed
   629 
   630 lemma setsum_nonpos:
   631   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   632   shows "setsum f A \<le> 0"
   633 proof (cases "finite A")
   634   case True thus ?thesis using np
   635   proof induct
   636     case empty then show ?case by simp
   637   next
   638     case (insert x F)
   639     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   640     with insert show ?case by simp
   641   qed
   642 next
   643   case False thus ?thesis by simp
   644 qed
   645 
   646 lemma setsum_nonneg_leq_bound:
   647   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   648   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   649   shows "f i \<le> B"
   650 proof -
   651   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   652     using assms by (auto intro!: setsum_nonneg)
   653   moreover
   654   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   655     using assms by (simp add: setsum_diff1)
   656   ultimately show ?thesis by auto
   657 qed
   658 
   659 lemma setsum_nonneg_0:
   660   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   661   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   662   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   663   shows "f i = 0"
   664   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   665 
   666 lemma setsum_mono2:
   667 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   668 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   669 shows "setsum f A \<le> setsum f B"
   670 proof -
   671   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   672     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   673   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   674     by (simp add: setsum.union_disjoint del:Un_Diff_cancel)
   675   also have "A \<union> (B-A) = B" using sub by blast
   676   finally show ?thesis .
   677 qed
   678 
   679 lemma setsum_le_included:
   680   fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
   681   assumes "finite s" "finite t"
   682   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)"
   683   shows "setsum f s \<le> setsum g t"
   684 proof -
   685   have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s"
   686   proof (rule setsum_mono)
   687     fix y assume "y \<in> s"
   688     with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
   689     with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
   690       using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro]
   691       by (auto intro!: setsum_mono2)
   692   qed
   693   also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)"
   694     using assms(2-4) by (auto intro!: setsum_mono2 setsum_nonneg)
   695   also have "... \<le> setsum g t"
   696     using assms by (auto simp: setsum_image_gen[symmetric])
   697   finally show ?thesis .
   698 qed
   699 
   700 lemma setsum_mono3: "finite B ==> A <= B ==> 
   701     ALL x: B - A. 
   702       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   703         setsum f A <= setsum f B"
   704   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   705   apply (erule ssubst)
   706   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   707   apply simp
   708   apply (rule add_left_mono)
   709   apply (erule setsum_nonneg)
   710   apply (subst setsum.union_disjoint [THEN sym])
   711   apply (erule finite_subset, assumption)
   712   apply (rule finite_subset)
   713   prefer 2
   714   apply assumption
   715   apply (auto simp add: sup_absorb2)
   716 done
   717 
   718 lemma setsum_right_distrib: 
   719   fixes f :: "'a => ('b::semiring_0)"
   720   shows "r * setsum f A = setsum (%n. r * f n) A"
   721 proof (cases "finite A")
   722   case True
   723   thus ?thesis
   724   proof induct
   725     case empty thus ?case by simp
   726   next
   727     case (insert x A) thus ?case by (simp add: distrib_left)
   728   qed
   729 next
   730   case False thus ?thesis by simp
   731 qed
   732 
   733 lemma setsum_left_distrib:
   734   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   735 proof (cases "finite A")
   736   case True
   737   then show ?thesis
   738   proof induct
   739     case empty thus ?case by simp
   740   next
   741     case (insert x A) thus ?case by (simp add: distrib_right)
   742   qed
   743 next
   744   case False thus ?thesis by simp
   745 qed
   746 
   747 lemma setsum_divide_distrib:
   748   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   749 proof (cases "finite A")
   750   case True
   751   then show ?thesis
   752   proof induct
   753     case empty thus ?case by simp
   754   next
   755     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   756   qed
   757 next
   758   case False thus ?thesis by simp
   759 qed
   760 
   761 lemma setsum_abs[iff]: 
   762   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   763   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   764 proof (cases "finite A")
   765   case True
   766   thus ?thesis
   767   proof induct
   768     case empty thus ?case by simp
   769   next
   770     case (insert x A)
   771     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   772   qed
   773 next
   774   case False thus ?thesis by simp
   775 qed
   776 
   777 lemma setsum_abs_ge_zero[iff]: 
   778   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   779   shows "0 \<le> setsum (%i. abs(f i)) A"
   780 proof (cases "finite A")
   781   case True
   782   thus ?thesis
   783   proof induct
   784     case empty thus ?case by simp
   785   next
   786     case (insert x A) thus ?case by auto
   787   qed
   788 next
   789   case False thus ?thesis by simp
   790 qed
   791 
   792 lemma abs_setsum_abs[simp]: 
   793   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   794   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   795 proof (cases "finite A")
   796   case True
   797   thus ?thesis
   798   proof induct
   799     case empty thus ?case by simp
   800   next
   801     case (insert a A)
   802     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
   803     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   804     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   805       by (simp del: abs_of_nonneg)
   806     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   807     finally show ?case .
   808   qed
   809 next
   810   case False thus ?thesis by simp
   811 qed
   812 
   813 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   814   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   815   unfolding setsum.remove [OF assms] by auto
   816 
   817 lemma setsum_product:
   818   fixes f :: "'a => ('b::semiring_0)"
   819   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   820   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum.commute)
   821 
   822 lemma setsum_mult_setsum_if_inj:
   823 fixes f :: "'a => ('b::semiring_0)"
   824 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   825   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   826 by(auto simp: setsum_product setsum.cartesian_product
   827         intro!:  setsum.reindex_cong[symmetric])
   828 
   829 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   830 apply (case_tac "finite A")
   831  prefer 2 apply simp
   832 apply (erule rev_mp)
   833 apply (erule finite_induct, auto)
   834 done
   835 
   836 lemma setsum_eq_0_iff [simp]:
   837   "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   838   by (induct set: finite) auto
   839 
   840 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   841   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   842 apply(erule finite_induct)
   843 apply (auto simp add:add_is_1)
   844 done
   845 
   846 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   847 
   848 lemma setsum_Un_nat: "finite A ==> finite B ==>
   849   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   850   -- {* For the natural numbers, we have subtraction. *}
   851 by (subst setsum.union_inter [symmetric], auto simp add: algebra_simps)
   852 
   853 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   854   (if a:A then setsum f A - f a else setsum f A)"
   855 apply (case_tac "finite A")
   856  prefer 2 apply simp
   857 apply (erule finite_induct)
   858  apply (auto simp add: insert_Diff_if)
   859 apply (drule_tac a = a in mk_disjoint_insert, auto)
   860 done
   861 
   862 lemma setsum_diff_nat: 
   863 assumes "finite B" and "B \<subseteq> A"
   864 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   865 using assms
   866 proof induct
   867   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   868 next
   869   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   870     and xFinA: "insert x F \<subseteq> A"
   871     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   872   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   873   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   874     by (simp add: setsum_diff1_nat)
   875   from xFinA have "F \<subseteq> A" by simp
   876   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   877   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   878     by simp
   879   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   880   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   881     by simp
   882   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   883   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   884     by simp
   885   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   886 qed
   887 
   888 lemma setsum_comp_morphism:
   889   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   890   shows "setsum (h \<circ> g) A = h (setsum g A)"
   891 proof (cases "finite A")
   892   case False then show ?thesis by (simp add: assms)
   893 next
   894   case True then show ?thesis by (induct A) (simp_all add: assms)
   895 qed
   896 
   897 
   898 subsubsection {* Cardinality as special case of @{const setsum} *}
   899 
   900 lemma card_eq_setsum:
   901   "card A = setsum (\<lambda>x. 1) A"
   902 proof -
   903   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   904     by (simp add: fun_eq_iff)
   905   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   906     by (rule arg_cong)
   907   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   908     by (blast intro: fun_cong)
   909   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   910 qed
   911 
   912 lemma setsum_constant [simp]:
   913   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   914 apply (cases "finite A")
   915 apply (erule finite_induct)
   916 apply (auto simp add: algebra_simps)
   917 done
   918 
   919 lemma setsum_bounded:
   920   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   921   shows "setsum f A \<le> of_nat (card A) * K"
   922 proof (cases "finite A")
   923   case True
   924   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   925 next
   926   case False thus ?thesis by simp
   927 qed
   928 
   929 lemma card_UN_disjoint:
   930   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   931     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   932   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   933 proof -
   934   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   935   with assms show ?thesis by (simp add: card_eq_setsum setsum.UNION_disjoint del: setsum_constant)
   936 qed
   937 
   938 lemma card_Union_disjoint:
   939   "finite C ==> (ALL A:C. finite A) ==>
   940    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
   941    ==> card (Union C) = setsum card C"
   942 apply (frule card_UN_disjoint [of C id])
   943 apply simp_all
   944 done
   945 
   946 lemma setsum_multicount_gen:
   947   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   948   shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r")
   949 proof-
   950   have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto
   951   also have "\<dots> = ?r" unfolding setsum.commute_restrict [OF assms(1-2)]
   952     using assms(3) by auto
   953   finally show ?thesis .
   954 qed
   955 
   956 lemma setsum_multicount:
   957   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
   958   shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
   959 proof-
   960   have "?l = setsum (\<lambda>i. k) T" by (rule setsum_multicount_gen) (auto simp: assms)
   961   also have "\<dots> = ?r" by (simp add: mult_commute)
   962   finally show ?thesis by auto
   963 qed
   964 
   965 
   966 subsubsection {* Cardinality of products *}
   967 
   968 lemma card_SigmaI [simp]:
   969   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
   970   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
   971 by(simp add: card_eq_setsum setsum.Sigma del:setsum_constant)
   972 
   973 (*
   974 lemma SigmaI_insert: "y \<notin> A ==>
   975   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
   976   by auto
   977 *)
   978 
   979 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
   980   by (cases "finite A \<and> finite B")
   981     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
   982 
   983 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
   984 by (simp add: card_cartesian_product)
   985 
   986 
   987 subsection {* Generalized product over a set *}
   988 
   989 context comm_monoid_mult
   990 begin
   991 
   992 definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   993 where
   994   "setprod = comm_monoid_set.F times 1"
   995 
   996 sublocale setprod!: comm_monoid_set times 1
   997 where
   998   "comm_monoid_set.F times 1 = setprod"
   999 proof -
  1000   show "comm_monoid_set times 1" ..
  1001   then interpret setprod!: comm_monoid_set times 1 .
  1002   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  1003 qed
  1004 
  1005 abbreviation
  1006   Setprod ("\<Prod>_" [1000] 999) where
  1007   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1008 
  1009 end
  1010 
  1011 syntax
  1012   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1013 syntax (xsymbols)
  1014   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1015 syntax (HTML output)
  1016   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1017 
  1018 translations -- {* Beware of argument permutation! *}
  1019   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1020   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1021 
  1022 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1023  @{text"\<Prod>x|P. e"}. *}
  1024 
  1025 syntax
  1026   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1027 syntax (xsymbols)
  1028   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1029 syntax (HTML output)
  1030   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1031 
  1032 translations
  1033   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1034   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1035 
  1036 
  1037 subsubsection {* Properties in more restricted classes of structures *}
  1038 
  1039 lemma setprod_zero:
  1040      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1041 apply (induct set: finite, force, clarsimp)
  1042 apply (erule disjE, auto)
  1043 done
  1044 
  1045 lemma setprod_zero_iff[simp]: "finite A ==> 
  1046   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1047   (EX x: A. f x = 0)"
  1048 by (erule finite_induct, auto simp:no_zero_divisors)
  1049 
  1050 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1051   (setprod f (A Un B) :: 'a ::{field})
  1052    = setprod f A * setprod f B / setprod f (A Int B)"
  1053 by (subst setprod.union_inter [symmetric], auto)
  1054 
  1055 lemma setprod_nonneg [rule_format]:
  1056    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1057 by (cases "finite A", induct set: finite, simp_all)
  1058 
  1059 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  1060   --> 0 < setprod f A"
  1061 by (cases "finite A", induct set: finite, simp_all)
  1062 
  1063 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1064   (setprod f (A - {a}) :: 'a :: {field}) =
  1065   (if a:A then setprod f A / f a else setprod f A)"
  1066   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1067 
  1068 lemma setprod_inversef: 
  1069   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1070   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1071 by (erule finite_induct) auto
  1072 
  1073 lemma setprod_dividef:
  1074   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1075   shows "finite A
  1076     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1077 apply (subgoal_tac
  1078          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1079 apply (erule ssubst)
  1080 apply (subst divide_inverse)
  1081 apply (subst setprod.distrib)
  1082 apply (subst setprod_inversef, assumption+, rule refl)
  1083 apply (rule setprod.cong, rule refl)
  1084 apply (subst divide_inverse, auto)
  1085 done
  1086 
  1087 lemma setprod_dvd_setprod [rule_format]: 
  1088     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1089   apply (cases "finite A")
  1090   apply (induct set: finite)
  1091   apply (auto simp add: dvd_def)
  1092   apply (rule_tac x = "k * ka" in exI)
  1093   apply (simp add: algebra_simps)
  1094 done
  1095 
  1096 lemma setprod_dvd_setprod_subset:
  1097   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1098   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1099   apply (unfold dvd_def, blast)
  1100   apply (subst setprod.union_disjoint [symmetric])
  1101   apply (auto elim: finite_subset intro: setprod.cong)
  1102 done
  1103 
  1104 lemma setprod_dvd_setprod_subset2:
  1105   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1106       setprod f A dvd setprod g B"
  1107   apply (rule dvd_trans)
  1108   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1109   apply (erule (1) setprod_dvd_setprod_subset)
  1110 done
  1111 
  1112 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1113     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1114 by (induct set: finite) (auto intro: dvd_mult)
  1115 
  1116 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1117     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1118   apply (cases "finite A")
  1119   apply (induct set: finite)
  1120   apply auto
  1121 done
  1122 
  1123 lemma setprod_mono:
  1124   fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  1125   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1126   shows "setprod f A \<le> setprod g A"
  1127 proof (cases "finite A")
  1128   case True
  1129   hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  1130   proof (induct A rule: finite_subset_induct)
  1131     case (insert a F)
  1132     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  1133       unfolding setprod.insert[OF insert(1,3)]
  1134       using assms[rule_format,OF insert(2)] insert
  1135       by (auto intro: mult_mono)
  1136   qed auto
  1137   thus ?thesis by simp
  1138 qed auto
  1139 
  1140 lemma abs_setprod:
  1141   fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  1142   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  1143 proof (cases "finite A")
  1144   case True thus ?thesis
  1145     by induct (auto simp add: field_simps abs_mult)
  1146 qed auto
  1147 
  1148 lemma setprod_eq_1_iff [simp]:
  1149   "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
  1150   by (induct set: finite) auto
  1151 
  1152 lemma setprod_pos_nat:
  1153   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1154 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1155 
  1156 lemma setprod_pos_nat_iff[simp]:
  1157   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1158 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1159 
  1160 lemma (in ordered_comm_monoid_add) setsum_pos: 
  1161   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
  1162   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
  1163 
  1164 end