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