src/HOL/Groups_Big.thy
author hoelzl
Wed Jun 18 07:31:12 2014 +0200 (2014-06-18)
changeset 57275 0ddb5b755cdc
parent 57129 7edb7550663e
child 57418 6ab1c7cb0b8d
permissions -rw-r--r--
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
     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 subset_diff:
    91   assumes "B \<subseteq> A" and "finite A"
    92   shows "F g A = F g (A - B) * F g B"
    93 proof -
    94   from assms have "finite (A - B)" by auto
    95   moreover from assms have "finite B" by (rule finite_subset)
    96   moreover from assms have "(A - B) \<inter> B = {}" by auto
    97   ultimately have "F g (A - B \<union> B) = F g (A - B) * F g B" by (rule union_disjoint)
    98   moreover from assms have "A \<union> B = A" by auto
    99   ultimately show ?thesis by simp
   100 qed
   101 
   102 lemma setdiff_irrelevant:
   103   assumes "finite A"
   104   shows "F g (A - {x. g x = z}) = F g A"
   105   using assms by (induct A) (simp_all add: insert_Diff_if) 
   106   
   107 lemma not_neutral_contains_not_neutral:
   108   assumes "F g A \<noteq> z"
   109   obtains a where "a \<in> A" and "g a \<noteq> z"
   110 proof -
   111   from assms have "\<exists>a\<in>A. g a \<noteq> z"
   112   proof (induct A rule: infinite_finite_induct)
   113     case (insert a A)
   114     then show ?case by simp (rule, simp)
   115   qed simp_all
   116   with that show thesis by blast
   117 qed
   118 
   119 lemma reindex:
   120   assumes "inj_on h A"
   121   shows "F g (h ` A) = F (g \<circ> h) A"
   122 proof (cases "finite A")
   123   case True
   124   with assms show ?thesis by (simp add: eq_fold fold_image comp_assoc)
   125 next
   126   case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
   127   with False show ?thesis by simp
   128 qed
   129 
   130 lemma cong:
   131   assumes "A = B"
   132   assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   133   shows "F g A = F h B"
   134   using g_h unfolding `A = B`
   135   by (induct B rule: infinite_finite_induct) auto
   136 
   137 lemma strong_cong [cong]:
   138   assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
   139   shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
   140   by (rule cong) (insert assms, simp_all add: simp_implies_def)
   141 
   142 lemma UNION_disjoint:
   143   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   144   and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   145   shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
   146 apply (insert assms)
   147 apply (induct rule: finite_induct)
   148 apply simp
   149 apply atomize
   150 apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
   151  prefer 2 apply blast
   152 apply (subgoal_tac "A x Int UNION Fa A = {}")
   153  prefer 2 apply blast
   154 apply (simp add: union_disjoint)
   155 done
   156 
   157 lemma Union_disjoint:
   158   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
   159   shows "F g (Union C) = F (F g) C"
   160 proof cases
   161   assume "finite C"
   162   from UNION_disjoint [OF this assms]
   163   show ?thesis by simp
   164 qed (auto dest: finite_UnionD intro: infinite)
   165 
   166 lemma distrib:
   167   "F (\<lambda>x. g x * h x) A = F g A * F h A"
   168   using assms by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
   169 
   170 lemma Sigma:
   171   "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)"
   172 apply (subst Sigma_def)
   173 apply (subst UNION_disjoint, assumption, simp)
   174  apply blast
   175 apply (rule cong)
   176 apply rule
   177 apply (simp add: fun_eq_iff)
   178 apply (subst UNION_disjoint, simp, simp)
   179  apply blast
   180 apply (simp add: comp_def)
   181 done
   182 
   183 lemma related: 
   184   assumes Re: "R 1 1" 
   185   and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   186   and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   187   shows "R (F h S) (F g S)"
   188   using fS by (rule finite_subset_induct) (insert assms, auto)
   189 
   190 lemma mono_neutral_cong_left:
   191   assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
   192   and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
   193 proof-
   194   have eq: "T = S \<union> (T - S)" using `S \<subseteq> T` by blast
   195   have d: "S \<inter> (T - S) = {}" using `S \<subseteq> T` by blast
   196   from `finite T` `S \<subseteq> T` have f: "finite S" "finite (T - S)"
   197     by (auto intro: finite_subset)
   198   show ?thesis using assms(4)
   199     by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
   200 qed
   201 
   202 lemma mono_neutral_cong_right:
   203   "\<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>
   204    \<Longrightarrow> F g T = F h S"
   205   by (auto intro!: mono_neutral_cong_left [symmetric])
   206 
   207 lemma mono_neutral_left:
   208   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
   209   by (blast intro: mono_neutral_cong_left)
   210 
   211 lemma mono_neutral_right:
   212   "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   213   by (blast intro!: mono_neutral_left [symmetric])
   214 
   215 lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
   216   by (auto simp: bij_betw_def reindex)
   217 
   218 lemma reindex_bij_witness:
   219   assumes witness:
   220     "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a"
   221     "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T"
   222     "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b"
   223     "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S"
   224   assumes eq:
   225     "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
   226   shows "F g S = F h T"
   227 proof -
   228   have "bij_betw j S T"
   229     using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
   230   moreover have "F g S = F (\<lambda>x. h (j x)) S"
   231     by (intro cong) (auto simp: eq)
   232   ultimately show ?thesis
   233     by (simp add: reindex_bij_betw)
   234 qed
   235 
   236 lemma reindex_bij_betw_not_neutral:
   237   assumes fin: "finite S'" "finite T'"
   238   assumes bij: "bij_betw h (S - S') (T - T')"
   239   assumes nn:
   240     "\<And>a. a \<in> S' \<Longrightarrow> g (h a) = z"
   241     "\<And>b. b \<in> T' \<Longrightarrow> g b = z"
   242   shows "F (\<lambda>x. g (h x)) S = F g T"
   243 proof -
   244   have [simp]: "finite S \<longleftrightarrow> finite T"
   245     using bij_betw_finite[OF bij] fin by auto
   246 
   247   show ?thesis
   248   proof cases
   249     assume "finite S"
   250     with nn have "F (\<lambda>x. g (h x)) S = F (\<lambda>x. g (h x)) (S - S')"
   251       by (intro mono_neutral_cong_right) auto
   252     also have "\<dots> = F g (T - T')"
   253       using bij by (rule reindex_bij_betw)
   254     also have "\<dots> = F g T"
   255       using nn `finite S` by (intro mono_neutral_cong_left) auto
   256     finally show ?thesis .
   257   qed simp
   258 qed
   259 
   260 lemma reindex_bij_witness_not_neutral:
   261   assumes fin: "finite S'" "finite T'"
   262   assumes witness:
   263     "\<And>a. a \<in> S - S' \<Longrightarrow> i (j a) = a"
   264     "\<And>a. a \<in> S - S' \<Longrightarrow> j a \<in> T - T'"
   265     "\<And>b. b \<in> T - T' \<Longrightarrow> j (i b) = b"
   266     "\<And>b. b \<in> T - T' \<Longrightarrow> i b \<in> S - S'"
   267   assumes nn:
   268     "\<And>a. a \<in> S' \<Longrightarrow> g a = z"
   269     "\<And>b. b \<in> T' \<Longrightarrow> h b = z"
   270   assumes eq:
   271     "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
   272   shows "F g S = F h T"
   273 proof -
   274   have bij: "bij_betw j (S - (S' \<inter> S)) (T - (T' \<inter> T))"
   275     using witness by (intro bij_betw_byWitness[where f'=i]) auto
   276   have F_eq: "F g S = F (\<lambda>x. h (j x)) S"
   277     by (intro cong) (auto simp: eq)
   278   show ?thesis
   279     unfolding F_eq using fin nn eq
   280     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
   281 qed
   282 
   283 lemma delta: 
   284   assumes fS: "finite S"
   285   shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
   286 proof-
   287   let ?f = "(\<lambda>k. if k=a then b k else 1)"
   288   { assume a: "a \<notin> S"
   289     hence "\<forall>k\<in>S. ?f k = 1" by simp
   290     hence ?thesis  using a by simp }
   291   moreover
   292   { assume a: "a \<in> S"
   293     let ?A = "S - {a}"
   294     let ?B = "{a}"
   295     have eq: "S = ?A \<union> ?B" using a by blast 
   296     have dj: "?A \<inter> ?B = {}" by simp
   297     from fS have fAB: "finite ?A" "finite ?B" by auto  
   298     have "F ?f S = F ?f ?A * F ?f ?B"
   299       using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]]
   300       by simp
   301     then have ?thesis using a by simp }
   302   ultimately show ?thesis by blast
   303 qed
   304 
   305 lemma delta': 
   306   assumes fS: "finite S"
   307   shows "F (\<lambda>k. if a = k then b k else 1) S = (if a \<in> S then b a else 1)"
   308   using delta [OF fS, of a b, symmetric] by (auto intro: cong)
   309 
   310 lemma If_cases:
   311   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   312   assumes fA: "finite A"
   313   shows "F (\<lambda>x. if P x then h x else g x) A =
   314     F h (A \<inter> {x. P x}) * F g (A \<inter> - {x. P x})"
   315 proof -
   316   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" 
   317           "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" 
   318     by blast+
   319   from fA 
   320   have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   321   let ?g = "\<lambda>x. if P x then h x else g x"
   322   from union_disjoint [OF f a(2), of ?g] a(1)
   323   show ?thesis
   324     by (subst (1 2) cong) simp_all
   325 qed
   326 
   327 lemma cartesian_product:
   328    "F (\<lambda>x. F (g x) B) A = F (split g) (A <*> B)"
   329 apply (rule sym)
   330 apply (cases "finite A") 
   331  apply (cases "finite B") 
   332   apply (simp add: Sigma)
   333  apply (cases "A={}", simp)
   334  apply simp
   335 apply (auto intro: infinite dest: finite_cartesian_productD2)
   336 apply (cases "B = {}") apply (auto intro: infinite dest: finite_cartesian_productD1)
   337 done
   338 
   339 end
   340 
   341 notation times (infixl "*" 70)
   342 notation Groups.one ("1")
   343 
   344 
   345 subsection {* Generalized summation over a set *}
   346 
   347 context comm_monoid_add
   348 begin
   349 
   350 definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
   351 where
   352   "setsum = comm_monoid_set.F plus 0"
   353 
   354 sublocale setsum!: comm_monoid_set plus 0
   355 where
   356   "comm_monoid_set.F plus 0 = setsum"
   357 proof -
   358   show "comm_monoid_set plus 0" ..
   359   then interpret setsum!: comm_monoid_set plus 0 .
   360   from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
   361 qed
   362 
   363 abbreviation
   364   Setsum ("\<Sum>_" [1000] 999) where
   365   "\<Sum>A \<equiv> setsum (%x. x) A"
   366 
   367 end
   368 
   369 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
   370 written @{text"\<Sum>x\<in>A. e"}. *}
   371 
   372 syntax
   373   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_. _)" [0, 51, 10] 10)
   374 syntax (xsymbols)
   375   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   376 syntax (HTML output)
   377   "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10)
   378 
   379 translations -- {* Beware of argument permutation! *}
   380   "SUM i:A. b" == "CONST setsum (%i. b) A"
   381   "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
   382 
   383 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
   384  @{text"\<Sum>x|P. e"}. *}
   385 
   386 syntax
   387   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
   388 syntax (xsymbols)
   389   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   390 syntax (HTML output)
   391   "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10)
   392 
   393 translations
   394   "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
   395   "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
   396 
   397 print_translation {*
   398 let
   399   fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   400         if x <> y then raise Match
   401         else
   402           let
   403             val x' = Syntax_Trans.mark_bound_body (x, Tx);
   404             val t' = subst_bound (x', t);
   405             val P' = subst_bound (x', P);
   406           in
   407             Syntax.const @{syntax_const "_qsetsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   408           end
   409     | setsum_tr' _ = raise Match;
   410 in [(@{const_syntax setsum}, K setsum_tr')] end
   411 *}
   412 
   413 text {* TODO These are candidates for generalization *}
   414 
   415 context comm_monoid_add
   416 begin
   417 
   418 lemma setsum_reindex_id: 
   419   "inj_on f B \<Longrightarrow> setsum f B = setsum id (f ` B)"
   420   by (simp add: setsum.reindex)
   421 
   422 lemma setsum_reindex_nonzero:
   423   assumes fS: "finite S"
   424   and nz: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
   425   shows "setsum h (f ` S) = setsum (h \<circ> f) S"
   426 proof (subst setsum.reindex_bij_betw_not_neutral[symmetric])
   427   show "bij_betw f (S - {x\<in>S. h (f x) = 0}) (f`S - f`{x\<in>S. h (f x) = 0})"
   428     using nz by (auto intro!: inj_onI simp: bij_betw_def)
   429 qed (insert fS, auto)
   430 
   431 lemma setsum_cong2:
   432   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
   433   by (auto intro: setsum.cong)
   434 
   435 lemma setsum_reindex_cong:
   436    "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
   437     ==> setsum h B = setsum g A"
   438   by (simp add: setsum.reindex)
   439 
   440 lemma setsum_restrict_set:
   441   assumes fA: "finite A"
   442   shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   443 proof-
   444   from fA have fab: "finite (A \<inter> B)" by auto
   445   have aba: "A \<inter> B \<subseteq> A" by blast
   446   let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   447   from setsum.mono_neutral_left [OF fA aba, of ?g]
   448   show ?thesis by simp
   449 qed
   450 
   451 lemma setsum_Union_disjoint:
   452   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
   453   shows "setsum f (Union C) = setsum (setsum f) C"
   454   using assms by (fact setsum.Union_disjoint)
   455 
   456 lemma setsum_cartesian_product:
   457   "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)"
   458   by (fact setsum.cartesian_product)
   459 
   460 lemma setsum_UNION_zero:
   461   assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   462   and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
   463   shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   464   using fSS f0
   465 proof(induct rule: finite_induct[OF fS])
   466   case 1 thus ?case by simp
   467 next
   468   case (2 T F)
   469   then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   470     and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto
   471   from fTF have fUF: "finite (\<Union>F)" by auto
   472   from "2.prems" TF fTF
   473   show ?case 
   474     by (auto simp add: H [symmetric] intro: setsum.union_inter_neutral [OF fTF(1) fUF, of f])
   475 qed
   476 
   477 text {* Commuting outer and inner summation *}
   478 
   479 lemma setsum_commute:
   480   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
   481   unfolding setsum_cartesian_product
   482   by (rule setsum.reindex_bij_witness[where i="\<lambda>(i, j). (j, i)" and j="\<lambda>(i, j). (j, i)"]) auto
   483 
   484 lemma setsum_Plus:
   485   fixes A :: "'a set" and B :: "'b set"
   486   assumes fin: "finite A" "finite B"
   487   shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B"
   488 proof -
   489   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   490   moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)"
   491     by auto
   492   moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto
   493   moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI)
   494   ultimately show ?thesis using fin by(simp add: setsum.union_disjoint setsum.reindex)
   495 qed
   496 
   497 end
   498 
   499 text {* TODO These are legacy *}
   500 
   501 lemma setsum_empty:
   502   "setsum f {} = 0"
   503   by (fact setsum.empty)
   504 
   505 lemma setsum_insert:
   506   "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   507   by (fact setsum.insert)
   508 
   509 lemma setsum_infinite:
   510   "~ finite A ==> setsum f A = 0"
   511   by (fact setsum.infinite)
   512 
   513 lemma setsum_reindex:
   514   "inj_on f B \<Longrightarrow> setsum h (f ` B) = setsum (h \<circ> f) B"
   515   by (fact setsum.reindex)
   516 
   517 lemma setsum_cong:
   518   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
   519   by (fact setsum.cong)
   520 
   521 lemma strong_setsum_cong:
   522   "A = B ==> (!!x. x:B =simp=> f x = g x)
   523    ==> setsum (%x. f x) A = setsum (%x. g x) B"
   524   by (fact setsum.strong_cong)
   525 
   526 lemmas setsum_0 = setsum.neutral_const
   527 lemmas setsum_0' = setsum.neutral
   528 
   529 lemma setsum_Un_Int: "finite A ==> finite B ==>
   530   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   531   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
   532   by (fact setsum.union_inter)
   533 
   534 lemma setsum_Un_disjoint: "finite A ==> finite B
   535   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
   536   by (fact setsum.union_disjoint)
   537 
   538 lemma setsum_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
   539     setsum f A = setsum f (A - B) + setsum f B"
   540   by (fact setsum.subset_diff)
   541 
   542 lemma setsum_mono_zero_left: 
   543   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 0 \<rbrakk> \<Longrightarrow> setsum f S = setsum f T"
   544   by (fact setsum.mono_neutral_left)
   545 
   546 lemmas setsum_mono_zero_right = setsum.mono_neutral_right
   547 
   548 lemma setsum_mono_zero_cong_left: 
   549   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
   550   \<Longrightarrow> setsum f S = setsum g T"
   551   by (fact setsum.mono_neutral_cong_left)
   552 
   553 lemmas setsum_mono_zero_cong_right = setsum.mono_neutral_cong_right
   554 
   555 lemma setsum_delta: "finite S \<Longrightarrow>
   556   setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
   557   by (fact setsum.delta)
   558 
   559 lemma setsum_delta': "finite S \<Longrightarrow>
   560   setsum (\<lambda>k. if a = k then b k else 0) S = (if a\<in> S then b a else 0)"
   561   by (fact setsum.delta')
   562 
   563 lemma setsum_cases:
   564   assumes "finite A"
   565   shows "setsum (\<lambda>x. if P x then f x else g x) A =
   566          setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})"
   567   using assms by (fact setsum.If_cases)
   568 
   569 (*But we can't get rid of finite I. If infinite, although the rhs is 0, 
   570   the lhs need not be, since UNION I A could still be finite.*)
   571 lemma setsum_UN_disjoint:
   572   assumes "finite I" and "ALL i:I. finite (A i)"
   573     and "ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}"
   574   shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
   575   using assms by (fact setsum.UNION_disjoint)
   576 
   577 (*But we can't get rid of finite A. If infinite, although the lhs is 0, 
   578   the rhs need not be, since SIGMA A B could still be finite.*)
   579 lemma setsum_Sigma:
   580   assumes "finite A" and  "ALL x:A. finite (B x)"
   581   shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
   582   using assms by (fact setsum.Sigma)
   583 
   584 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
   585   by (fact setsum.distrib)
   586 
   587 lemma setsum_Un_zero:  
   588   "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 0 \<rbrakk> \<Longrightarrow>
   589   setsum f (S \<union> T) = setsum f S + setsum f T"
   590   by (fact setsum.union_inter_neutral)
   591 
   592 subsubsection {* Properties in more restricted classes of structures *}
   593 
   594 lemma setsum_Un: "finite A ==> finite B ==>
   595   (setsum f (A Un B) :: 'a :: ab_group_add) =
   596    setsum f A + setsum f B - setsum f (A Int B)"
   597 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   598 
   599 lemma setsum_Un2:
   600   assumes "finite (A \<union> B)"
   601   shows "setsum f (A \<union> B) = setsum f (A - B) + setsum f (B - A) + setsum f (A \<inter> B)"
   602 proof -
   603   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   604     by auto
   605   with assms show ?thesis by simp (subst setsum_Un_disjoint, auto)+
   606 qed
   607 
   608 lemma setsum_diff1: "finite A \<Longrightarrow>
   609   (setsum f (A - {a}) :: ('a::ab_group_add)) =
   610   (if a:A then setsum f A - f a else setsum f A)"
   611 by (erule finite_induct) (auto simp add: insert_Diff_if)
   612 
   613 lemma setsum_diff:
   614   assumes le: "finite A" "B \<subseteq> A"
   615   shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))"
   616 proof -
   617   from le have finiteB: "finite B" using finite_subset by auto
   618   show ?thesis using finiteB le
   619   proof induct
   620     case empty
   621     thus ?case by auto
   622   next
   623     case (insert x F)
   624     thus ?case using le finiteB 
   625       by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb)
   626   qed
   627 qed
   628 
   629 lemma setsum_mono:
   630   assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))"
   631   shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   632 proof (cases "finite K")
   633   case True
   634   thus ?thesis using le
   635   proof induct
   636     case empty
   637     thus ?case by simp
   638   next
   639     case insert
   640     thus ?case using add_mono by fastforce
   641   qed
   642 next
   643   case False then show ?thesis by simp
   644 qed
   645 
   646 lemma setsum_strict_mono:
   647   fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}"
   648   assumes "finite A"  "A \<noteq> {}"
   649     and "!!x. x:A \<Longrightarrow> f x < g x"
   650   shows "setsum f A < setsum g A"
   651   using assms
   652 proof (induct rule: finite_ne_induct)
   653   case singleton thus ?case by simp
   654 next
   655   case insert thus ?case by (auto simp: add_strict_mono)
   656 qed
   657 
   658 lemma setsum_strict_mono_ex1:
   659 fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_cancel_ab_semigroup_add}"
   660 assumes "finite A" and "ALL x:A. f x \<le> g x" and "EX a:A. f a < g a"
   661 shows "setsum f A < setsum g A"
   662 proof-
   663   from assms(3) obtain a where a: "a:A" "f a < g a" by blast
   664   have "setsum f A = setsum f ((A-{a}) \<union> {a})"
   665     by(simp add:insert_absorb[OF `a:A`])
   666   also have "\<dots> = setsum f (A-{a}) + setsum f {a}"
   667     using `finite A` by(subst setsum_Un_disjoint) auto
   668   also have "setsum f (A-{a}) \<le> setsum g (A-{a})"
   669     by(rule setsum_mono)(simp add: assms(2))
   670   also have "setsum f {a} < setsum g {a}" using a by simp
   671   also have "setsum g (A - {a}) + setsum g {a} = setsum g((A-{a}) \<union> {a})"
   672     using `finite A` by(subst setsum_Un_disjoint[symmetric]) auto
   673   also have "\<dots> = setsum g A" by(simp add:insert_absorb[OF `a:A`])
   674   finally show ?thesis by (auto simp add: add_right_mono add_strict_left_mono)
   675 qed
   676 
   677 lemma setsum_negf:
   678   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
   679 proof (cases "finite A")
   680   case True thus ?thesis by (induct set: finite) auto
   681 next
   682   case False thus ?thesis by simp
   683 qed
   684 
   685 lemma setsum_subtractf:
   686   "setsum (%x. ((f x)::'a::ab_group_add) - g x) A =
   687     setsum f A - setsum g A"
   688   using setsum_addf [of f "- g" A] by (simp add: setsum_negf)
   689 
   690 lemma setsum_nonneg:
   691   assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x"
   692   shows "0 \<le> setsum f A"
   693 proof (cases "finite A")
   694   case True thus ?thesis using nn
   695   proof induct
   696     case empty then show ?case by simp
   697   next
   698     case (insert x F)
   699     then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono)
   700     with insert show ?case by simp
   701   qed
   702 next
   703   case False thus ?thesis by simp
   704 qed
   705 
   706 lemma setsum_nonpos:
   707   assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})"
   708   shows "setsum f A \<le> 0"
   709 proof (cases "finite A")
   710   case True thus ?thesis using np
   711   proof induct
   712     case empty then show ?case by simp
   713   next
   714     case (insert x F)
   715     then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono)
   716     with insert show ?case by simp
   717   qed
   718 next
   719   case False thus ?thesis by simp
   720 qed
   721 
   722 lemma setsum_nonneg_leq_bound:
   723   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   724   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   725   shows "f i \<le> B"
   726 proof -
   727   have "0 \<le> (\<Sum> i \<in> s - {i}. f i)" and "0 \<le> f i"
   728     using assms by (auto intro!: setsum_nonneg)
   729   moreover
   730   have "(\<Sum> i \<in> s - {i}. f i) + f i = B"
   731     using assms by (simp add: setsum_diff1)
   732   ultimately show ?thesis by auto
   733 qed
   734 
   735 lemma setsum_nonneg_0:
   736   fixes f :: "'a \<Rightarrow> 'b::{ordered_ab_group_add}"
   737   assumes "finite s" and pos: "\<And> i. i \<in> s \<Longrightarrow> f i \<ge> 0"
   738   and "(\<Sum> i \<in> s. f i) = 0" and i: "i \<in> s"
   739   shows "f i = 0"
   740   using setsum_nonneg_leq_bound[OF assms] pos[OF i] by auto
   741 
   742 lemma setsum_mono2:
   743 fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
   744 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   745 shows "setsum f A \<le> setsum f B"
   746 proof -
   747   have "setsum f A \<le> setsum f A + setsum f (B-A)"
   748     by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
   749   also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
   750     by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
   751   also have "A \<union> (B-A) = B" using sub by blast
   752   finally show ?thesis .
   753 qed
   754 
   755 lemma setsum_mono3: "finite B ==> A <= B ==> 
   756     ALL x: B - A. 
   757       0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==>
   758         setsum f A <= setsum f B"
   759   apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)")
   760   apply (erule ssubst)
   761   apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)")
   762   apply simp
   763   apply (rule add_left_mono)
   764   apply (erule setsum_nonneg)
   765   apply (subst setsum_Un_disjoint [THEN sym])
   766   apply (erule finite_subset, assumption)
   767   apply (rule finite_subset)
   768   prefer 2
   769   apply assumption
   770   apply (auto simp add: sup_absorb2)
   771 done
   772 
   773 lemma setsum_right_distrib: 
   774   fixes f :: "'a => ('b::semiring_0)"
   775   shows "r * setsum f A = setsum (%n. r * f n) A"
   776 proof (cases "finite A")
   777   case True
   778   thus ?thesis
   779   proof induct
   780     case empty thus ?case by simp
   781   next
   782     case (insert x A) thus ?case by (simp add: distrib_left)
   783   qed
   784 next
   785   case False thus ?thesis by simp
   786 qed
   787 
   788 lemma setsum_left_distrib:
   789   "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)"
   790 proof (cases "finite A")
   791   case True
   792   then show ?thesis
   793   proof induct
   794     case empty thus ?case by simp
   795   next
   796     case (insert x A) thus ?case by (simp add: distrib_right)
   797   qed
   798 next
   799   case False thus ?thesis by simp
   800 qed
   801 
   802 lemma setsum_divide_distrib:
   803   "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
   804 proof (cases "finite A")
   805   case True
   806   then show ?thesis
   807   proof induct
   808     case empty thus ?case by simp
   809   next
   810     case (insert x A) thus ?case by (simp add: add_divide_distrib)
   811   qed
   812 next
   813   case False thus ?thesis by simp
   814 qed
   815 
   816 lemma setsum_abs[iff]: 
   817   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   818   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
   819 proof (cases "finite A")
   820   case True
   821   thus ?thesis
   822   proof induct
   823     case empty thus ?case by simp
   824   next
   825     case (insert x A)
   826     thus ?case by (auto intro: abs_triangle_ineq order_trans)
   827   qed
   828 next
   829   case False thus ?thesis by simp
   830 qed
   831 
   832 lemma setsum_abs_ge_zero[iff]: 
   833   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   834   shows "0 \<le> setsum (%i. abs(f i)) A"
   835 proof (cases "finite A")
   836   case True
   837   thus ?thesis
   838   proof induct
   839     case empty thus ?case by simp
   840   next
   841     case (insert x A) thus ?case by auto
   842   qed
   843 next
   844   case False thus ?thesis by simp
   845 qed
   846 
   847 lemma abs_setsum_abs[simp]: 
   848   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   849   shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
   850 proof (cases "finite A")
   851   case True
   852   thus ?thesis
   853   proof induct
   854     case empty thus ?case by simp
   855   next
   856     case (insert a A)
   857     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
   858     also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
   859     also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>"
   860       by (simp del: abs_of_nonneg)
   861     also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
   862     finally show ?case .
   863   qed
   864 next
   865   case False thus ?thesis by simp
   866 qed
   867 
   868 lemma setsum_diff1'[rule_format]:
   869   "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)"
   870 apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"])
   871 apply (auto simp add: insert_Diff_if add_ac)
   872 done
   873 
   874 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A"
   875   shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)"
   876 unfolding setsum_diff1'[OF assms] by auto
   877 
   878 lemma setsum_product:
   879   fixes f :: "'a => ('b::semiring_0)"
   880   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   881   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
   882 
   883 lemma setsum_mult_setsum_if_inj:
   884 fixes f :: "'a => ('b::semiring_0)"
   885 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
   886   setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
   887 by(auto simp: setsum_product setsum_cartesian_product
   888         intro!:  setsum_reindex_cong[symmetric])
   889 
   890 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a"
   891 apply (case_tac "finite A")
   892  prefer 2 apply simp
   893 apply (erule rev_mp)
   894 apply (erule finite_induct, auto)
   895 done
   896 
   897 lemma setsum_eq_0_iff [simp]:
   898   "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   899   by (induct set: finite) auto
   900 
   901 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
   902   setsum f A = Suc 0 \<longleftrightarrow> (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
   903 apply(erule finite_induct)
   904 apply (auto simp add:add_is_1)
   905 done
   906 
   907 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   908 
   909 lemma setsum_Un_nat: "finite A ==> finite B ==>
   910   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   911   -- {* For the natural numbers, we have subtraction. *}
   912 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps)
   913 
   914 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) =
   915   (if a:A then setsum f A - f a else setsum f A)"
   916 apply (case_tac "finite A")
   917  prefer 2 apply simp
   918 apply (erule finite_induct)
   919  apply (auto simp add: insert_Diff_if)
   920 apply (drule_tac a = a in mk_disjoint_insert, auto)
   921 done
   922 
   923 lemma setsum_diff_nat: 
   924 assumes "finite B" and "B \<subseteq> A"
   925 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)"
   926 using assms
   927 proof induct
   928   show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp
   929 next
   930   fix F x assume finF: "finite F" and xnotinF: "x \<notin> F"
   931     and xFinA: "insert x F \<subseteq> A"
   932     and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F"
   933   from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp
   934   from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x"
   935     by (simp add: setsum_diff1_nat)
   936   from xFinA have "F \<subseteq> A" by simp
   937   with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp
   938   with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x"
   939     by simp
   940   from xnotinF have "A - insert x F = (A - F) - {x}" by auto
   941   with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x"
   942     by simp
   943   from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp
   944   with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)"
   945     by simp
   946   thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp
   947 qed
   948 
   949 lemma setsum_comp_morphism:
   950   assumes "h 0 = 0" and "\<And>x y. h (x + y) = h x + h y"
   951   shows "setsum (h \<circ> g) A = h (setsum g A)"
   952 proof (cases "finite A")
   953   case False then show ?thesis by (simp add: assms)
   954 next
   955   case True then show ?thesis by (induct A) (simp_all add: assms)
   956 qed
   957 
   958 
   959 subsubsection {* Cardinality as special case of @{const setsum} *}
   960 
   961 lemma card_eq_setsum:
   962   "card A = setsum (\<lambda>x. 1) A"
   963 proof -
   964   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   965     by (simp add: fun_eq_iff)
   966   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   967     by (rule arg_cong)
   968   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   969     by (blast intro: fun_cong)
   970   then show ?thesis by (simp add: card.eq_fold setsum.eq_fold)
   971 qed
   972 
   973 lemma setsum_constant [simp]:
   974   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   975 apply (cases "finite A")
   976 apply (erule finite_induct)
   977 apply (auto simp add: algebra_simps)
   978 done
   979 
   980 lemma setsum_bounded:
   981   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   982   shows "setsum f A \<le> of_nat (card A) * K"
   983 proof (cases "finite A")
   984   case True
   985   thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
   986 next
   987   case False thus ?thesis by simp
   988 qed
   989 
   990 lemma card_UN_disjoint:
   991   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   992     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   993   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   994 proof -
   995   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)" by simp
   996   with assms show ?thesis by (simp add: card_eq_setsum setsum_UN_disjoint del: setsum_constant)
   997 qed
   998 
   999 lemma card_Union_disjoint:
  1000   "finite C ==> (ALL A:C. finite A) ==>
  1001    (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
  1002    ==> card (Union C) = setsum card C"
  1003 apply (frule card_UN_disjoint [of C id])
  1004 apply simp_all
  1005 done
  1006 
  1007 
  1008 subsubsection {* Cardinality of products *}
  1009 
  1010 lemma card_SigmaI [simp]:
  1011   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
  1012   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1013 by(simp add: card_eq_setsum setsum_Sigma del:setsum_constant)
  1014 
  1015 (*
  1016 lemma SigmaI_insert: "y \<notin> A ==>
  1017   (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))"
  1018   by auto
  1019 *)
  1020 
  1021 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
  1022   by (cases "finite A \<and> finite B")
  1023     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1024 
  1025 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
  1026 by (simp add: card_cartesian_product)
  1027 
  1028 
  1029 subsection {* Generalized product over a set *}
  1030 
  1031 context comm_monoid_mult
  1032 begin
  1033 
  1034 definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
  1035 where
  1036   "setprod = comm_monoid_set.F times 1"
  1037 
  1038 sublocale setprod!: comm_monoid_set times 1
  1039 where
  1040   "comm_monoid_set.F times 1 = setprod"
  1041 proof -
  1042   show "comm_monoid_set times 1" ..
  1043   then interpret setprod!: comm_monoid_set times 1 .
  1044   from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
  1045 qed
  1046 
  1047 abbreviation
  1048   Setprod ("\<Prod>_" [1000] 999) where
  1049   "\<Prod>A \<equiv> setprod (\<lambda>x. x) A"
  1050 
  1051 end
  1052 
  1053 syntax
  1054   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3PROD _:_. _)" [0, 51, 10] 10)
  1055 syntax (xsymbols)
  1056   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1057 syntax (HTML output)
  1058   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10)
  1059 
  1060 translations -- {* Beware of argument permutation! *}
  1061   "PROD i:A. b" == "CONST setprod (%i. b) A" 
  1062   "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
  1063 
  1064 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
  1065  @{text"\<Prod>x|P. e"}. *}
  1066 
  1067 syntax
  1068   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10)
  1069 syntax (xsymbols)
  1070   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1071 syntax (HTML output)
  1072   "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10)
  1073 
  1074 translations
  1075   "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
  1076   "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
  1077 
  1078 text {* TODO These are candidates for generalization *}
  1079 
  1080 context comm_monoid_mult
  1081 begin
  1082 
  1083 lemma setprod_reindex_id:
  1084   "inj_on f B ==> setprod f B = setprod id (f ` B)"
  1085   by (auto simp add: setprod.reindex)
  1086 
  1087 lemma setprod_reindex_cong:
  1088   "inj_on f A ==> B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
  1089   by (frule setprod.reindex, simp)
  1090 
  1091 lemma strong_setprod_reindex_cong:
  1092   "inj_on f A \<Longrightarrow> B = f ` A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x) \<Longrightarrow> setprod h B = setprod g A"
  1093   by (subst setprod.reindex_bij_betw[symmetric, where h=f])
  1094      (auto simp: bij_betw_def)
  1095 
  1096 lemma setprod_Union_disjoint:
  1097   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
  1098   shows "setprod f (Union C) = setprod (setprod f) C"
  1099   using assms by (fact setprod.Union_disjoint)
  1100 
  1101 text{*Here we can eliminate the finiteness assumptions, by cases.*}
  1102 lemma setprod_cartesian_product:
  1103   "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)"
  1104   by (fact setprod.cartesian_product)
  1105 
  1106 lemma setprod_Un2:
  1107   assumes "finite (A \<union> B)"
  1108   shows "setprod f (A \<union> B) = setprod f (A - B) * setprod f (B - A) * setprod f (A \<inter> B)"
  1109 proof -
  1110   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
  1111     by auto
  1112   with assms show ?thesis by simp (subst setprod.union_disjoint, auto)+
  1113 qed
  1114 
  1115 end
  1116 
  1117 text {* TODO These are legacy *}
  1118 
  1119 lemma setprod_empty: "setprod f {} = 1"
  1120   by (fact setprod.empty)
  1121 
  1122 lemma setprod_insert: "[| finite A; a \<notin> A |] ==>
  1123     setprod f (insert a A) = f a * setprod f A"
  1124   by (fact setprod.insert)
  1125 
  1126 lemma setprod_infinite: "~ finite A ==> setprod f A = 1"
  1127   by (fact setprod.infinite)
  1128 
  1129 lemma setprod_reindex:
  1130   "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
  1131   by (fact setprod.reindex)
  1132 
  1133 lemma setprod_cong:
  1134   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
  1135   by (fact setprod.cong)
  1136 
  1137 lemma strong_setprod_cong:
  1138   "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B"
  1139   by (fact setprod.strong_cong)
  1140 
  1141 lemma setprod_Un_one:
  1142   "\<lbrakk> finite S; finite T; \<forall>x \<in> S\<inter>T. f x = 1 \<rbrakk>
  1143   \<Longrightarrow> setprod f (S \<union> T) = setprod f S  * setprod f T"
  1144   by (fact setprod.union_inter_neutral)
  1145 
  1146 lemmas setprod_1 = setprod.neutral_const
  1147 lemmas setprod_1' = setprod.neutral
  1148 
  1149 lemma setprod_Un_Int: "finite A ==> finite B
  1150     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
  1151   by (fact setprod.union_inter)
  1152 
  1153 lemma setprod_Un_disjoint: "finite A ==> finite B
  1154   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
  1155   by (fact setprod.union_disjoint)
  1156 
  1157 lemma setprod_subset_diff: "\<lbrakk> B \<subseteq> A; finite A \<rbrakk> \<Longrightarrow>
  1158     setprod f A = setprod f (A - B) * setprod f B"
  1159   by (fact setprod.subset_diff)
  1160 
  1161 lemma setprod_mono_one_left:
  1162   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. f i = 1 \<rbrakk> \<Longrightarrow> setprod f S = setprod f T"
  1163   by (fact setprod.mono_neutral_left)
  1164 
  1165 lemmas setprod_mono_one_right = setprod.mono_neutral_right
  1166 
  1167 lemma setprod_mono_one_cong_left: 
  1168   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> f x = g x \<rbrakk>
  1169   \<Longrightarrow> setprod f S = setprod g T"
  1170   by (fact setprod.mono_neutral_cong_left)
  1171 
  1172 lemmas setprod_mono_one_cong_right = setprod.mono_neutral_cong_right
  1173 
  1174 lemma setprod_delta: "finite S \<Longrightarrow>
  1175   setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)"
  1176   by (fact setprod.delta)
  1177 
  1178 lemma setprod_delta': "finite S \<Longrightarrow>
  1179   setprod (\<lambda>k. if a = k then b k else 1) S = (if a\<in> S then b a else 1)"
  1180   by (fact setprod.delta')
  1181 
  1182 lemma setprod_UN_disjoint:
  1183     "finite I ==> (ALL i:I. finite (A i)) ==>
  1184         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1185       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
  1186   by (fact setprod.UNION_disjoint)
  1187 
  1188 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
  1189     (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
  1190     (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
  1191   by (fact setprod.Sigma)
  1192 
  1193 lemma setprod_timesf: "setprod (\<lambda>x. f x * g x) A = setprod f A * setprod g A"
  1194   by (fact setprod.distrib)
  1195 
  1196 
  1197 subsubsection {* Properties in more restricted classes of structures *}
  1198 
  1199 lemma setprod_zero:
  1200      "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0"
  1201 apply (induct set: finite, force, clarsimp)
  1202 apply (erule disjE, auto)
  1203 done
  1204 
  1205 lemma setprod_zero_iff[simp]: "finite A ==> 
  1206   (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) =
  1207   (EX x: A. f x = 0)"
  1208 by (erule finite_induct, auto simp:no_zero_divisors)
  1209 
  1210 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==>
  1211   (setprod f (A Un B) :: 'a ::{field})
  1212    = setprod f A * setprod f B / setprod f (A Int B)"
  1213 by (subst setprod_Un_Int [symmetric], auto)
  1214 
  1215 lemma setprod_nonneg [rule_format]:
  1216    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
  1217 by (cases "finite A", induct set: finite, simp_all)
  1218 
  1219 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
  1220   --> 0 < setprod f A"
  1221 by (cases "finite A", induct set: finite, simp_all)
  1222 
  1223 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
  1224   (setprod f (A - {a}) :: 'a :: {field}) =
  1225   (if a:A then setprod f A / f a else setprod f A)"
  1226   by (erule finite_induct) (auto simp add: insert_Diff_if)
  1227 
  1228 lemma setprod_inversef: 
  1229   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1230   shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)"
  1231 by (erule finite_induct) auto
  1232 
  1233 lemma setprod_dividef:
  1234   fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero"
  1235   shows "finite A
  1236     ==> setprod (%x. f x / g x) A = setprod f A / setprod g A"
  1237 apply (subgoal_tac
  1238          "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A")
  1239 apply (erule ssubst)
  1240 apply (subst divide_inverse)
  1241 apply (subst setprod_timesf)
  1242 apply (subst setprod_inversef, assumption+, rule refl)
  1243 apply (rule setprod_cong, rule refl)
  1244 apply (subst divide_inverse, auto)
  1245 done
  1246 
  1247 lemma setprod_dvd_setprod [rule_format]: 
  1248     "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A"
  1249   apply (cases "finite A")
  1250   apply (induct set: finite)
  1251   apply (auto simp add: dvd_def)
  1252   apply (rule_tac x = "k * ka" in exI)
  1253   apply (simp add: algebra_simps)
  1254 done
  1255 
  1256 lemma setprod_dvd_setprod_subset:
  1257   "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B"
  1258   apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)")
  1259   apply (unfold dvd_def, blast)
  1260   apply (subst setprod_Un_disjoint [symmetric])
  1261   apply (auto elim: finite_subset intro: setprod_cong)
  1262 done
  1263 
  1264 lemma setprod_dvd_setprod_subset2:
  1265   "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> 
  1266       setprod f A dvd setprod g B"
  1267   apply (rule dvd_trans)
  1268   apply (rule setprod_dvd_setprod, erule (1) bspec)
  1269   apply (erule (1) setprod_dvd_setprod_subset)
  1270 done
  1271 
  1272 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> 
  1273     (f i ::'a::comm_semiring_1) dvd setprod f A"
  1274 by (induct set: finite) (auto intro: dvd_mult)
  1275 
  1276 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> 
  1277     (d::'a::comm_semiring_1) dvd (SUM x : A. f x)"
  1278   apply (cases "finite A")
  1279   apply (induct set: finite)
  1280   apply auto
  1281 done
  1282 
  1283 lemma setprod_mono:
  1284   fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom"
  1285   assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i"
  1286   shows "setprod f A \<le> setprod g A"
  1287 proof (cases "finite A")
  1288   case True
  1289   hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A]
  1290   proof (induct A rule: finite_subset_induct)
  1291     case (insert a F)
  1292     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
  1293       unfolding setprod_insert[OF insert(1,3)]
  1294       using assms[rule_format,OF insert(2)] insert
  1295       by (auto intro: mult_mono)
  1296   qed auto
  1297   thus ?thesis by simp
  1298 qed auto
  1299 
  1300 lemma abs_setprod:
  1301   fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}"
  1302   shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A"
  1303 proof (cases "finite A")
  1304   case True thus ?thesis
  1305     by induct (auto simp add: field_simps abs_mult)
  1306 qed auto
  1307 
  1308 lemma setprod_eq_1_iff [simp]:
  1309   "finite F ==> setprod f F = 1 \<longleftrightarrow> (ALL a:F. f a = (1::nat))"
  1310   by (induct set: finite) auto
  1311 
  1312 lemma setprod_pos_nat:
  1313   "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
  1314 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1315 
  1316 lemma setprod_pos_nat_iff[simp]:
  1317   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
  1318 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
  1319 
  1320 lemma (in ordered_comm_monoid_add) setsum_pos: 
  1321   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
  1322   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
  1323 
  1324 end