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