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