src/HOL/Groups_Big.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 66364 fa3247e6ee4b
child 66804 3f9bb52082c4
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Groups_Big.thy
     2     Author:     Tobias Nipkow
     3     Author:     Lawrence C Paulson
     4     Author:     Markus Wenzel
     5     Author:     Jeremy Avigad
     6 *)
     7 
     8 section \<open>Big sum and product over finite (non-empty) sets\<close>
     9 
    10 theory Groups_Big
    11   imports Power
    12 begin
    13 
    14 subsection \<open>Generic monoid operation over a set\<close>
    15 
    16 locale comm_monoid_set = comm_monoid
    17 begin
    18 
    19 interpretation comp_fun_commute f
    20   by standard (simp add: fun_eq_iff left_commute)
    21 
    22 interpretation comp?: comp_fun_commute "f \<circ> g"
    23   by (fact comp_comp_fun_commute)
    24 
    25 definition F :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    26   where eq_fold: "F g A = Finite_Set.fold (f \<circ> g) \<^bold>1 A"
    27 
    28 lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F g A = \<^bold>1"
    29   by (simp add: eq_fold)
    30 
    31 lemma empty [simp]: "F g {} = \<^bold>1"
    32   by (simp add: eq_fold)
    33 
    34 lemma insert [simp]: "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow> F g (insert x A) = g x \<^bold>* F g A"
    35   by (simp add: eq_fold)
    36 
    37 lemma remove:
    38   assumes "finite A" and "x \<in> A"
    39   shows "F g A = g x \<^bold>* F g (A - {x})"
    40 proof -
    41   from \<open>x \<in> A\<close> obtain B where B: "A = insert x B" and "x \<notin> B"
    42     by (auto dest: mk_disjoint_insert)
    43   moreover from \<open>finite A\<close> B have "finite B" by simp
    44   ultimately show ?thesis by simp
    45 qed
    46 
    47 lemma insert_remove: "finite A \<Longrightarrow> F g (insert x A) = g x \<^bold>* F g (A - {x})"
    48   by (cases "x \<in> A") (simp_all add: remove insert_absorb)
    49 
    50 lemma insert_if: "finite A \<Longrightarrow> F g (insert x A) = (if x \<in> A then F g A else g x \<^bold>* F g A)"
    51   by (cases "x \<in> A") (simp_all add: insert_absorb)
    52 
    53 lemma neutral: "\<forall>x\<in>A. g x = \<^bold>1 \<Longrightarrow> F g A = \<^bold>1"
    54   by (induct A rule: infinite_finite_induct) simp_all
    55 
    56 lemma neutral_const [simp]: "F (\<lambda>_. \<^bold>1) A = \<^bold>1"
    57   by (simp add: neutral)
    58 
    59 lemma union_inter:
    60   assumes "finite A" and "finite B"
    61   shows "F g (A \<union> B) \<^bold>* F g (A \<inter> B) = F g A \<^bold>* F g B"
    62   \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
    63   using assms
    64 proof (induct A)
    65   case empty
    66   then show ?case by simp
    67 next
    68   case (insert x A)
    69   then show ?case
    70     by (auto simp: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
    71 qed
    72 
    73 corollary union_inter_neutral:
    74   assumes "finite A" and "finite B"
    75     and "\<forall>x \<in> A \<inter> B. g x = \<^bold>1"
    76   shows "F g (A \<union> B) = F g A \<^bold>* F g B"
    77   using assms by (simp add: union_inter [symmetric] neutral)
    78 
    79 corollary union_disjoint:
    80   assumes "finite A" and "finite B"
    81   assumes "A \<inter> B = {}"
    82   shows "F g (A \<union> B) = F g A \<^bold>* F g B"
    83   using assms by (simp add: union_inter_neutral)
    84 
    85 lemma union_diff2:
    86   assumes "finite A" and "finite B"
    87   shows "F g (A \<union> B) = F g (A - B) \<^bold>* F g (B - A) \<^bold>* F g (A \<inter> B)"
    88 proof -
    89   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
    90     by auto
    91   with assms show ?thesis
    92     by simp (subst union_disjoint, auto)+
    93 qed
    94 
    95 lemma subset_diff:
    96   assumes "B \<subseteq> A" and "finite A"
    97   shows "F g A = F g (A - B) \<^bold>* F g B"
    98 proof -
    99   from assms have "finite (A - B)" by auto
   100   moreover from assms have "finite B" by (rule finite_subset)
   101   moreover from assms have "(A - B) \<inter> B = {}" by auto
   102   ultimately have "F g (A - B \<union> B) = F g (A - B) \<^bold>* F g B" by (rule union_disjoint)
   103   moreover from assms have "A \<union> B = A" by auto
   104   ultimately show ?thesis by simp
   105 qed
   106 
   107 lemma setdiff_irrelevant:
   108   assumes "finite A"
   109   shows "F g (A - {x. g x = z}) = F g A"
   110   using assms by (induct A) (simp_all add: insert_Diff_if)
   111 
   112 lemma not_neutral_contains_not_neutral:
   113   assumes "F g A \<noteq> \<^bold>1"
   114   obtains a where "a \<in> A" and "g a \<noteq> \<^bold>1"
   115 proof -
   116   from assms have "\<exists>a\<in>A. g a \<noteq> \<^bold>1"
   117   proof (induct A rule: infinite_finite_induct)
   118     case infinite
   119     then show ?case by simp
   120   next
   121     case empty
   122     then show ?case by simp
   123   next
   124     case (insert a A)
   125     then show ?case by fastforce
   126   qed
   127   with that show thesis by blast
   128 qed
   129 
   130 lemma reindex:
   131   assumes "inj_on h A"
   132   shows "F g (h ` A) = F (g \<circ> h) A"
   133 proof (cases "finite A")
   134   case True
   135   with assms show ?thesis
   136     by (simp add: eq_fold fold_image comp_assoc)
   137 next
   138   case False
   139   with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD)
   140   with False show ?thesis by simp
   141 qed
   142 
   143 lemma cong [fundef_cong]:
   144   assumes "A = B"
   145   assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   146   shows "F g A = F h B"
   147   using g_h unfolding \<open>A = B\<close>
   148   by (induct B rule: infinite_finite_induct) auto
   149 
   150 lemma strong_cong [cong]:
   151   assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
   152   shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
   153   by (rule cong) (use assms in \<open>simp_all add: simp_implies_def\<close>)
   154 
   155 lemma reindex_cong:
   156   assumes "inj_on l B"
   157   assumes "A = l ` B"
   158   assumes "\<And>x. x \<in> B \<Longrightarrow> g (l x) = h x"
   159   shows "F g A = F h B"
   160   using assms by (simp add: reindex)
   161 
   162 lemma UNION_disjoint:
   163   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   164     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   165   shows "F g (UNION I A) = F (\<lambda>x. F g (A x)) I"
   166   apply (insert assms)
   167   apply (induct rule: finite_induct)
   168    apply simp
   169   apply atomize
   170   apply (subgoal_tac "\<forall>i\<in>Fa. x \<noteq> i")
   171    prefer 2 apply blast
   172   apply (subgoal_tac "A x \<inter> UNION Fa A = {}")
   173    prefer 2 apply blast
   174   apply (simp add: union_disjoint)
   175   done
   176 
   177 lemma Union_disjoint:
   178   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
   179   shows "F g (\<Union>C) = (F \<circ> F) g C"
   180 proof (cases "finite C")
   181   case True
   182   from UNION_disjoint [OF this assms] show ?thesis by simp
   183 next
   184   case False
   185   then show ?thesis by (auto dest: finite_UnionD intro: infinite)
   186 qed
   187 
   188 lemma distrib: "F (\<lambda>x. g x \<^bold>* h x) A = F g A \<^bold>* F h A"
   189   by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)
   190 
   191 lemma Sigma:
   192   "finite A \<Longrightarrow> \<forall>x\<in>A. finite (B x) \<Longrightarrow> F (\<lambda>x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
   193   apply (subst Sigma_def)
   194   apply (subst UNION_disjoint)
   195      apply assumption
   196     apply simp
   197    apply blast
   198   apply (rule cong)
   199    apply rule
   200   apply (simp add: fun_eq_iff)
   201   apply (subst UNION_disjoint)
   202      apply simp
   203     apply simp
   204    apply blast
   205   apply (simp add: comp_def)
   206   done
   207 
   208 lemma related:
   209   assumes Re: "R \<^bold>1 \<^bold>1"
   210     and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 \<^bold>* y1) (x2 \<^bold>* y2)"
   211     and fin: "finite S"
   212     and R_h_g: "\<forall>x\<in>S. R (h x) (g x)"
   213   shows "R (F h S) (F g S)"
   214   using fin by (rule finite_subset_induct) (use assms in auto)
   215 
   216 lemma mono_neutral_cong_left:
   217   assumes "finite T"
   218     and "S \<subseteq> T"
   219     and "\<forall>i \<in> T - S. h i = \<^bold>1"
   220     and "\<And>x. x \<in> S \<Longrightarrow> g x = h x"
   221   shows "F g S = F h T"
   222 proof-
   223   have eq: "T = S \<union> (T - S)" using \<open>S \<subseteq> T\<close> by blast
   224   have d: "S \<inter> (T - S) = {}" using \<open>S \<subseteq> T\<close> by blast
   225   from \<open>finite T\<close> \<open>S \<subseteq> T\<close> have f: "finite S" "finite (T - S)"
   226     by (auto intro: finite_subset)
   227   show ?thesis using assms(4)
   228     by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
   229 qed
   230 
   231 lemma mono_neutral_cong_right:
   232   "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> g x = h x) \<Longrightarrow>
   233     F g T = F h S"
   234   by (auto intro!: mono_neutral_cong_left [symmetric])
   235 
   236 lemma mono_neutral_left: "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> F g S = F g T"
   237   by (blast intro: mono_neutral_cong_left)
   238 
   239 lemma mono_neutral_right: "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> F g T = F g S"
   240   by (blast intro!: mono_neutral_left [symmetric])
   241 
   242 lemma mono_neutral_cong:
   243   assumes [simp]: "finite T" "finite S"
   244     and *: "\<And>i. i \<in> T - S \<Longrightarrow> h i = \<^bold>1" "\<And>i. i \<in> S - T \<Longrightarrow> g i = \<^bold>1"
   245     and gh: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x = h x"
   246  shows "F g S = F h T"
   247 proof-
   248   have "F g S = F g (S \<inter> T)"
   249     by(rule mono_neutral_right)(auto intro: *)
   250   also have "\<dots> = F h (S \<inter> T)" using refl gh by(rule cong)
   251   also have "\<dots> = F h T"
   252     by(rule mono_neutral_left)(auto intro: *)
   253   finally show ?thesis .
   254 qed
   255 
   256 lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
   257   by (auto simp: bij_betw_def reindex)
   258 
   259 lemma reindex_bij_witness:
   260   assumes witness:
   261     "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a"
   262     "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T"
   263     "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b"
   264     "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S"
   265   assumes eq:
   266     "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
   267   shows "F g S = F h T"
   268 proof -
   269   have "bij_betw j S T"
   270     using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
   271   moreover have "F g S = F (\<lambda>x. h (j x)) S"
   272     by (intro cong) (auto simp: eq)
   273   ultimately show ?thesis
   274     by (simp add: reindex_bij_betw)
   275 qed
   276 
   277 lemma reindex_bij_betw_not_neutral:
   278   assumes fin: "finite S'" "finite T'"
   279   assumes bij: "bij_betw h (S - S') (T - T')"
   280   assumes nn:
   281     "\<And>a. a \<in> S' \<Longrightarrow> g (h a) = z"
   282     "\<And>b. b \<in> T' \<Longrightarrow> g b = z"
   283   shows "F (\<lambda>x. g (h x)) S = F g T"
   284 proof -
   285   have [simp]: "finite S \<longleftrightarrow> finite T"
   286     using bij_betw_finite[OF bij] fin by auto
   287   show ?thesis
   288   proof (cases "finite S")
   289     case True
   290     with nn have "F (\<lambda>x. g (h x)) S = F (\<lambda>x. g (h x)) (S - S')"
   291       by (intro mono_neutral_cong_right) auto
   292     also have "\<dots> = F g (T - T')"
   293       using bij by (rule reindex_bij_betw)
   294     also have "\<dots> = F g T"
   295       using nn \<open>finite S\<close> by (intro mono_neutral_cong_left) auto
   296     finally show ?thesis .
   297   next
   298     case False
   299     then show ?thesis by simp
   300   qed
   301 qed
   302 
   303 lemma reindex_nontrivial:
   304   assumes "finite A"
   305     and nz: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> h x = h y \<Longrightarrow> g (h x) = \<^bold>1"
   306   shows "F g (h ` A) = F (g \<circ> h) A"
   307 proof (subst reindex_bij_betw_not_neutral [symmetric])
   308   show "bij_betw h (A - {x \<in> A. (g \<circ> h) x = \<^bold>1}) (h ` A - h ` {x \<in> A. (g \<circ> h) x = \<^bold>1})"
   309     using nz by (auto intro!: inj_onI simp: bij_betw_def)
   310 qed (use \<open>finite A\<close> in auto)
   311 
   312 lemma reindex_bij_witness_not_neutral:
   313   assumes fin: "finite S'" "finite T'"
   314   assumes witness:
   315     "\<And>a. a \<in> S - S' \<Longrightarrow> i (j a) = a"
   316     "\<And>a. a \<in> S - S' \<Longrightarrow> j a \<in> T - T'"
   317     "\<And>b. b \<in> T - T' \<Longrightarrow> j (i b) = b"
   318     "\<And>b. b \<in> T - T' \<Longrightarrow> i b \<in> S - S'"
   319   assumes nn:
   320     "\<And>a. a \<in> S' \<Longrightarrow> g a = z"
   321     "\<And>b. b \<in> T' \<Longrightarrow> h b = z"
   322   assumes eq:
   323     "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
   324   shows "F g S = F h T"
   325 proof -
   326   have bij: "bij_betw j (S - (S' \<inter> S)) (T - (T' \<inter> T))"
   327     using witness by (intro bij_betw_byWitness[where f'=i]) auto
   328   have F_eq: "F g S = F (\<lambda>x. h (j x)) S"
   329     by (intro cong) (auto simp: eq)
   330   show ?thesis
   331     unfolding F_eq using fin nn eq
   332     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
   333 qed
   334 
   335 lemma delta [simp]:
   336   assumes fS: "finite S"
   337   shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   338 proof -
   339   let ?f = "(\<lambda>k. if k = a then b k else \<^bold>1)"
   340   show ?thesis
   341   proof (cases "a \<in> S")
   342     case False
   343     then have "\<forall>k\<in>S. ?f k = \<^bold>1" by simp
   344     with False show ?thesis by simp
   345   next
   346     case True
   347     let ?A = "S - {a}"
   348     let ?B = "{a}"
   349     from True have eq: "S = ?A \<union> ?B" by blast
   350     have dj: "?A \<inter> ?B = {}" by simp
   351     from fS have fAB: "finite ?A" "finite ?B" by auto
   352     have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
   353       using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
   354     with True show ?thesis by simp
   355   qed
   356 qed
   357 
   358 lemma delta' [simp]:
   359   assumes fin: "finite S"
   360   shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   361   using delta [OF fin, of a b, symmetric] by (auto intro: cong)
   362 
   363 lemma If_cases:
   364   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   365   assumes fin: "finite A"
   366   shows "F (\<lambda>x. if P x then h x else g x) A = F h (A \<inter> {x. P x}) \<^bold>* F g (A \<inter> - {x. P x})"
   367 proof -
   368   have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}"
   369     by blast+
   370   from fin have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto
   371   let ?g = "\<lambda>x. if P x then h x else g x"
   372   from union_disjoint [OF f a(2), of ?g] a(1) show ?thesis
   373     by (subst (1 2) cong) simp_all
   374 qed
   375 
   376 lemma cartesian_product: "F (\<lambda>x. F (g x) B) A = F (case_prod g) (A \<times> B)"
   377   apply (rule sym)
   378   apply (cases "finite A")
   379    apply (cases "finite B")
   380     apply (simp add: Sigma)
   381    apply (cases "A = {}")
   382     apply simp
   383    apply simp
   384    apply (auto intro: infinite dest: finite_cartesian_productD2)
   385   apply (cases "B = {}")
   386    apply (auto intro: infinite dest: finite_cartesian_productD1)
   387   done
   388 
   389 lemma inter_restrict:
   390   assumes "finite A"
   391   shows "F g (A \<inter> B) = F (\<lambda>x. if x \<in> B then g x else \<^bold>1) A"
   392 proof -
   393   let ?g = "\<lambda>x. if x \<in> A \<inter> B then g x else \<^bold>1"
   394   have "\<forall>i\<in>A - A \<inter> B. (if i \<in> A \<inter> B then g i else \<^bold>1) = \<^bold>1" by simp
   395   moreover have "A \<inter> B \<subseteq> A" by blast
   396   ultimately have "F ?g (A \<inter> B) = F ?g A"
   397     using \<open>finite A\<close> by (intro mono_neutral_left) auto
   398   then show ?thesis by simp
   399 qed
   400 
   401 lemma inter_filter:
   402   "finite A \<Longrightarrow> F g {x \<in> A. P x} = F (\<lambda>x. if P x then g x else \<^bold>1) A"
   403   by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)
   404 
   405 lemma Union_comp:
   406   assumes "\<forall>A \<in> B. finite A"
   407     and "\<And>A1 A2 x. A1 \<in> B \<Longrightarrow> A2 \<in> B \<Longrightarrow> A1 \<noteq> A2 \<Longrightarrow> x \<in> A1 \<Longrightarrow> x \<in> A2 \<Longrightarrow> g x = \<^bold>1"
   408   shows "F g (\<Union>B) = (F \<circ> F) g B"
   409   using assms
   410 proof (induct B rule: infinite_finite_induct)
   411   case (infinite A)
   412   then have "\<not> finite (\<Union>A)" by (blast dest: finite_UnionD)
   413   with infinite show ?case by simp
   414 next
   415   case empty
   416   then show ?case by simp
   417 next
   418   case (insert A B)
   419   then have "finite A" "finite B" "finite (\<Union>B)" "A \<notin> B"
   420     and "\<forall>x\<in>A \<inter> \<Union>B. g x = \<^bold>1"
   421     and H: "F g (\<Union>B) = (F \<circ> F) g B" by auto
   422   then have "F g (A \<union> \<Union>B) = F g A \<^bold>* F g (\<Union>B)"
   423     by (simp add: union_inter_neutral)
   424   with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case
   425     by (simp add: H)
   426 qed
   427 
   428 lemma commute: "F (\<lambda>i. F (g i) B) A = F (\<lambda>j. F (\<lambda>i. g i j) A) B"
   429   unfolding cartesian_product
   430   by (rule reindex_bij_witness [where i = "\<lambda>(i, j). (j, i)" and j = "\<lambda>(i, j). (j, i)"]) auto
   431 
   432 lemma commute_restrict:
   433   "finite A \<Longrightarrow> finite B \<Longrightarrow>
   434     F (\<lambda>x. F (g x) {y. y \<in> B \<and> R x y}) A = F (\<lambda>y. F (\<lambda>x. g x y) {x. x \<in> A \<and> R x y}) B"
   435   by (simp add: inter_filter) (rule commute)
   436 
   437 lemma Plus:
   438   fixes A :: "'b set" and B :: "'c set"
   439   assumes fin: "finite A" "finite B"
   440   shows "F g (A <+> B) = F (g \<circ> Inl) A \<^bold>* F (g \<circ> Inr) B"
   441 proof -
   442   have "A <+> B = Inl ` A \<union> Inr ` B" by auto
   443   moreover from fin have "finite (Inl ` A)" "finite (Inr ` B)" by auto
   444   moreover have "Inl ` A \<inter> Inr ` B = {}" by auto
   445   moreover have "inj_on Inl A" "inj_on Inr B" by (auto intro: inj_onI)
   446   ultimately show ?thesis
   447     using fin by (simp add: union_disjoint reindex)
   448 qed
   449 
   450 lemma same_carrier:
   451   assumes "finite C"
   452   assumes subset: "A \<subseteq> C" "B \<subseteq> C"
   453   assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
   454   shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
   455 proof -
   456   have "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)"
   457     using \<open>finite C\<close> subset by (auto elim: finite_subset)
   458   from subset have [simp]: "A - (C - A) = A" by auto
   459   from subset have [simp]: "B - (C - B) = B" by auto
   460   from subset have "C = A \<union> (C - A)" by auto
   461   then have "F g C = F g (A \<union> (C - A))" by simp
   462   also have "\<dots> = F g (A - (C - A)) \<^bold>* F g (C - A - A) \<^bold>* F g (A \<inter> (C - A))"
   463     using \<open>finite A\<close> \<open>finite (C - A)\<close> by (simp only: union_diff2)
   464   finally have *: "F g C = F g A" using trivial by simp
   465   from subset have "C = B \<union> (C - B)" by auto
   466   then have "F h C = F h (B \<union> (C - B))" by simp
   467   also have "\<dots> = F h (B - (C - B)) \<^bold>* F h (C - B - B) \<^bold>* F h (B \<inter> (C - B))"
   468     using \<open>finite B\<close> \<open>finite (C - B)\<close> by (simp only: union_diff2)
   469   finally have "F h C = F h B"
   470     using trivial by simp
   471   with * show ?thesis by simp
   472 qed
   473 
   474 lemma same_carrierI:
   475   assumes "finite C"
   476   assumes subset: "A \<subseteq> C" "B \<subseteq> C"
   477   assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = \<^bold>1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = \<^bold>1"
   478   assumes "F g C = F h C"
   479   shows "F g A = F h B"
   480   using assms same_carrier [of C A B] by simp
   481 
   482 end
   483 
   484 
   485 subsection \<open>Generalized summation over a set\<close>
   486 
   487 context comm_monoid_add
   488 begin
   489 
   490 sublocale sum: comm_monoid_set plus 0
   491   defines sum = sum.F ..
   492 
   493 abbreviation Sum ("\<Sum>_" [1000] 999)
   494   where "\<Sum>A \<equiv> sum (\<lambda>x. x) A"
   495 
   496 end
   497 
   498 text \<open>Now: lot's of fancy syntax. First, @{term "sum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
   499 
   500 syntax (ASCII)
   501   "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM _:_./ _)" [0, 51, 10] 10)
   502 syntax
   503   "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
   504 translations \<comment> \<open>Beware of argument permutation!\<close>
   505   "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST sum (\<lambda>i. b) A"
   506 
   507 text \<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
   508 
   509 syntax (ASCII)
   510   "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
   511 syntax
   512   "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
   513 translations
   514   "\<Sum>x|P. t" => "CONST sum (\<lambda>x. t) {x. P}"
   515 
   516 print_translation \<open>
   517 let
   518   fun sum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] =
   519         if x <> y then raise Match
   520         else
   521           let
   522             val x' = Syntax_Trans.mark_bound_body (x, Tx);
   523             val t' = subst_bound (x', t);
   524             val P' = subst_bound (x', P);
   525           in
   526             Syntax.const @{syntax_const "_qsum"} $ Syntax_Trans.mark_bound_abs (x, Tx) $ P' $ t'
   527           end
   528     | sum_tr' _ = raise Match;
   529 in [(@{const_syntax sum}, K sum_tr')] end
   530 \<close>
   531 
   532 (* TODO generalization candidates *)
   533 
   534 lemma (in comm_monoid_add) sum_image_gen:
   535   assumes fin: "finite S"
   536   shows "sum g S = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   537 proof -
   538   have "{y. y\<in> f`S \<and> f x = y} = {f x}" if "x \<in> S" for x
   539     using that by auto
   540   then have "sum g S = sum (\<lambda>x. sum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S"
   541     by simp
   542   also have "\<dots> = sum (\<lambda>y. sum g {x. x \<in> S \<and> f x = y}) (f ` S)"
   543     by (rule sum.commute_restrict [OF fin finite_imageI [OF fin]])
   544   finally show ?thesis .
   545 qed
   546 
   547 
   548 subsubsection \<open>Properties in more restricted classes of structures\<close>
   549 
   550 lemma sum_Un:
   551   "finite A \<Longrightarrow> finite B \<Longrightarrow> sum f (A \<union> B) = sum f A + sum f B - sum f (A \<inter> B)"
   552   for f :: "'b \<Rightarrow> 'a::ab_group_add"
   553   by (subst sum.union_inter [symmetric]) (auto simp add: algebra_simps)
   554 
   555 lemma sum_Un2:
   556   assumes "finite (A \<union> B)"
   557   shows "sum f (A \<union> B) = sum f (A - B) + sum f (B - A) + sum f (A \<inter> B)"
   558 proof -
   559   have "A \<union> B = A - B \<union> (B - A) \<union> A \<inter> B"
   560     by auto
   561   with assms show ?thesis
   562     by simp (subst sum.union_disjoint, auto)+
   563 qed
   564 
   565 lemma sum_diff1:
   566   fixes f :: "'b \<Rightarrow> 'a::ab_group_add"
   567   assumes "finite A"
   568   shows "sum f (A - {a}) = (if a \<in> A then sum f A - f a else sum f A)"
   569   using assms by induct (auto simp: insert_Diff_if)
   570 
   571 lemma sum_diff:
   572   fixes f :: "'b \<Rightarrow> 'a::ab_group_add"
   573   assumes "finite A" "B \<subseteq> A"
   574   shows "sum f (A - B) = sum f A - sum f B"
   575 proof -
   576   from assms(2,1) have "finite B" by (rule finite_subset)
   577   from this \<open>B \<subseteq> A\<close>
   578   show ?thesis
   579   proof induct
   580     case empty
   581     thus ?case by simp
   582   next
   583     case (insert x F)
   584     with \<open>finite A\<close> \<open>finite B\<close> show ?case
   585       by (simp add: Diff_insert[where a=x and B=F] sum_diff1 insert_absorb)
   586   qed
   587 qed
   588 
   589 lemma (in ordered_comm_monoid_add) sum_mono:
   590   "(\<And>i. i\<in>K \<Longrightarrow> f i \<le> g i) \<Longrightarrow> (\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)"
   591   by (induct K rule: infinite_finite_induct) (use add_mono in auto)
   592 
   593 lemma (in strict_ordered_comm_monoid_add) sum_strict_mono:
   594   assumes "finite A" "A \<noteq> {}"
   595     and "\<And>x. x \<in> A \<Longrightarrow> f x < g x"
   596   shows "sum f A < sum g A"
   597   using assms
   598 proof (induct rule: finite_ne_induct)
   599   case singleton
   600   then show ?case by simp
   601 next
   602   case insert
   603   then show ?case by (auto simp: add_strict_mono)
   604 qed
   605 
   606 lemma sum_strict_mono_ex1:
   607   fixes f g :: "'i \<Rightarrow> 'a::ordered_cancel_comm_monoid_add"
   608   assumes "finite A"
   609     and "\<forall>x\<in>A. f x \<le> g x"
   610     and "\<exists>a\<in>A. f a < g a"
   611   shows "sum f A < sum g A"
   612 proof-
   613   from assms(3) obtain a where a: "a \<in> A" "f a < g a" by blast
   614   have "sum f A = sum f ((A - {a}) \<union> {a})"
   615     by(simp add: insert_absorb[OF \<open>a \<in> A\<close>])
   616   also have "\<dots> = sum f (A - {a}) + sum f {a}"
   617     using \<open>finite A\<close> by(subst sum.union_disjoint) auto
   618   also have "sum f (A - {a}) \<le> sum g (A - {a})"
   619     by (rule sum_mono) (simp add: assms(2))
   620   also from a have "sum f {a} < sum g {a}" by simp
   621   also have "sum g (A - {a}) + sum g {a} = sum g((A - {a}) \<union> {a})"
   622     using \<open>finite A\<close> by (subst sum.union_disjoint[symmetric]) auto
   623   also have "\<dots> = sum g A" by (simp add: insert_absorb[OF \<open>a \<in> A\<close>])
   624   finally show ?thesis
   625     by (auto simp add: add_right_mono add_strict_left_mono)
   626 qed
   627 
   628 lemma sum_mono_inv:
   629   fixes f g :: "'i \<Rightarrow> 'a :: ordered_cancel_comm_monoid_add"
   630   assumes eq: "sum f I = sum g I"
   631   assumes le: "\<And>i. i \<in> I \<Longrightarrow> f i \<le> g i"
   632   assumes i: "i \<in> I"
   633   assumes I: "finite I"
   634   shows "f i = g i"
   635 proof (rule ccontr)
   636   assume "\<not> ?thesis"
   637   with le[OF i] have "f i < g i" by simp
   638   with i have "\<exists>i\<in>I. f i < g i" ..
   639   from sum_strict_mono_ex1[OF I _ this] le have "sum f I < sum g I"
   640     by blast
   641   with eq show False by simp
   642 qed
   643 
   644 lemma member_le_sum:
   645   fixes f :: "_ \<Rightarrow> 'b::{semiring_1, ordered_comm_monoid_add}"
   646   assumes "i \<in> A"
   647     and le: "\<And>x. x \<in> A - {i} \<Longrightarrow> 0 \<le> f x"
   648     and "finite A"
   649   shows "f i \<le> sum f A"
   650 proof -
   651   have "f i \<le> sum f (A \<inter> {i})"
   652     by (simp add: assms)
   653   also have "... = (\<Sum>x\<in>A. if x \<in> {i} then f x else 0)"
   654     using assms sum.inter_restrict by blast
   655   also have "... \<le> sum f A"
   656     apply (rule sum_mono)
   657     apply (auto simp: le)
   658     done
   659   finally show ?thesis .
   660 qed
   661 
   662 lemma sum_negf: "(\<Sum>x\<in>A. - f x) = - (\<Sum>x\<in>A. f x)"
   663   for f :: "'b \<Rightarrow> 'a::ab_group_add"
   664   by (induct A rule: infinite_finite_induct) auto
   665 
   666 lemma sum_subtractf: "(\<Sum>x\<in>A. f x - g x) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
   667   for f g :: "'b \<Rightarrow>'a::ab_group_add"
   668   using sum.distrib [of f "- g" A] by (simp add: sum_negf)
   669 
   670 lemma sum_subtractf_nat:
   671   "(\<And>x. x \<in> A \<Longrightarrow> g x \<le> f x) \<Longrightarrow> (\<Sum>x\<in>A. f x - g x) = (\<Sum>x\<in>A. f x) - (\<Sum>x\<in>A. g x)"
   672   for f g :: "'a \<Rightarrow> nat"
   673   by (induct A rule: infinite_finite_induct) (auto simp: sum_mono)
   674 
   675 context ordered_comm_monoid_add
   676 begin
   677 
   678 lemma sum_nonneg: "(\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> 0 \<le> sum f A"
   679 proof (induct A rule: infinite_finite_induct)
   680   case infinite
   681   then show ?case by simp
   682 next
   683   case empty
   684   then show ?case by simp
   685 next
   686   case (insert x F)
   687   then have "0 + 0 \<le> f x + sum f F" by (blast intro: add_mono)
   688   with insert show ?case by simp
   689 qed
   690 
   691 lemma sum_nonpos: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> 0) \<Longrightarrow> sum f A \<le> 0"
   692 proof (induct A rule: infinite_finite_induct)
   693   case infinite
   694   then show ?case by simp
   695 next
   696   case empty
   697   then show ?case by simp
   698 next
   699   case (insert x F)
   700   then have "f x + sum f F \<le> 0 + 0" by (blast intro: add_mono)
   701   with insert show ?case by simp
   702 qed
   703 
   704 lemma sum_nonneg_eq_0_iff:
   705   "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x) \<Longrightarrow> sum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   706   by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff sum_nonneg)
   707 
   708 lemma sum_nonneg_0:
   709   "finite s \<Longrightarrow> (\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0) \<Longrightarrow> (\<Sum> i \<in> s. f i) = 0 \<Longrightarrow> i \<in> s \<Longrightarrow> f i = 0"
   710   by (simp add: sum_nonneg_eq_0_iff)
   711 
   712 lemma sum_nonneg_leq_bound:
   713   assumes "finite s" "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0" "(\<Sum>i \<in> s. f i) = B" "i \<in> s"
   714   shows "f i \<le> B"
   715 proof -
   716   from assms have "f i \<le> f i + (\<Sum>i \<in> s - {i}. f i)"
   717     by (intro add_increasing2 sum_nonneg) auto
   718   also have "\<dots> = B"
   719     using sum.remove[of s i f] assms by simp
   720   finally show ?thesis by auto
   721 qed
   722 
   723 lemma sum_mono2:
   724   assumes fin: "finite B"
   725     and sub: "A \<subseteq> B"
   726     and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
   727   shows "sum f A \<le> sum f B"
   728 proof -
   729   have "sum f A \<le> sum f A + sum f (B-A)"
   730     by (auto intro: add_increasing2 [OF sum_nonneg] nn)
   731   also from fin finite_subset[OF sub fin] have "\<dots> = sum f (A \<union> (B-A))"
   732     by (simp add: sum.union_disjoint del: Un_Diff_cancel)
   733   also from sub have "A \<union> (B-A) = B" by blast
   734   finally show ?thesis .
   735 qed
   736 
   737 lemma sum_le_included:
   738   assumes "finite s" "finite t"
   739   and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
   740   shows "sum f s \<le> sum g t"
   741 proof -
   742   have "sum f s \<le> sum (\<lambda>y. sum g {x. x\<in>t \<and> i x = y}) s"
   743   proof (rule sum_mono)
   744     fix y
   745     assume "y \<in> s"
   746     with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto
   747     with assms show "f y \<le> sum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y")
   748       using order_trans[of "?A (i z)" "sum g {z}" "?B (i z)", intro]
   749       by (auto intro!: sum_mono2)
   750   qed
   751   also have "\<dots> \<le> sum (\<lambda>y. sum g {x. x\<in>t \<and> i x = y}) (i ` t)"
   752     using assms(2-4) by (auto intro!: sum_mono2 sum_nonneg)
   753   also have "\<dots> \<le> sum g t"
   754     using assms by (auto simp: sum_image_gen[symmetric])
   755   finally show ?thesis .
   756 qed
   757 
   758 end
   759 
   760 lemma (in canonically_ordered_monoid_add) sum_eq_0_iff [simp]:
   761   "finite F \<Longrightarrow> (sum f F = 0) = (\<forall>a\<in>F. f a = 0)"
   762   by (intro ballI sum_nonneg_eq_0_iff zero_le)
   763 
   764 lemma sum_distrib_left: "r * sum f A = sum (\<lambda>n. r * f n) A"
   765   for f :: "'a \<Rightarrow> 'b::semiring_0"
   766 proof (induct A rule: infinite_finite_induct)
   767   case infinite
   768   then show ?case by simp
   769 next
   770   case empty
   771   then show ?case by simp
   772 next
   773   case insert
   774   then show ?case by (simp add: distrib_left)
   775 qed
   776 
   777 lemma sum_distrib_right: "sum f A * r = (\<Sum>n\<in>A. f n * r)"
   778   for r :: "'a::semiring_0"
   779 proof (induct A rule: infinite_finite_induct)
   780   case infinite
   781   then show ?case by simp
   782 next
   783   case empty
   784   then show ?case by simp
   785 next
   786   case insert
   787   then show ?case by (simp add: distrib_right)
   788 qed
   789 
   790 lemma sum_divide_distrib: "sum f A / r = (\<Sum>n\<in>A. f n / r)"
   791   for r :: "'a::field"
   792 proof (induct A rule: infinite_finite_induct)
   793   case infinite
   794   then show ?case by simp
   795 next
   796   case empty
   797   then show ?case by simp
   798 next
   799   case insert
   800   then show ?case by (simp add: add_divide_distrib)
   801 qed
   802 
   803 lemma sum_abs[iff]: "\<bar>sum f A\<bar> \<le> sum (\<lambda>i. \<bar>f i\<bar>) A"
   804   for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   805 proof (induct A rule: infinite_finite_induct)
   806   case infinite
   807   then show ?case by simp
   808 next
   809   case empty
   810   then show ?case by simp
   811 next
   812   case insert
   813   then show ?case by (auto intro: abs_triangle_ineq order_trans)
   814 qed
   815 
   816 lemma sum_abs_ge_zero[iff]: "0 \<le> sum (\<lambda>i. \<bar>f i\<bar>) A"
   817   for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   818   by (simp add: sum_nonneg)
   819 
   820 lemma abs_sum_abs[simp]: "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
   821   for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   822 proof (induct A rule: infinite_finite_induct)
   823   case infinite
   824   then show ?case by simp
   825 next
   826   case empty
   827   then show ?case by simp
   828 next
   829   case (insert a A)
   830   then have "\<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
   831   also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp
   832   also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg)
   833   also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp
   834   finally show ?case .
   835 qed
   836 
   837 lemma sum_diff1_ring:
   838   fixes f :: "'b \<Rightarrow> 'a::ring"
   839   assumes "finite A" "a \<in> A"
   840   shows "sum f (A - {a}) = sum f A - (f a)"
   841   unfolding sum.remove [OF assms] by auto
   842 
   843 lemma sum_product:
   844   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   845   shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   846   by (simp add: sum_distrib_left sum_distrib_right) (rule sum.commute)
   847 
   848 lemma sum_mult_sum_if_inj:
   849   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   850   shows "inj_on (\<lambda>(a, b). f a * g b) (A \<times> B) \<Longrightarrow>
   851     sum f A * sum g B = sum id {f a * g b |a b. a \<in> A \<and> b \<in> B}"
   852   by(auto simp: sum_product sum.cartesian_product intro!: sum.reindex_cong[symmetric])
   853 
   854 lemma sum_SucD: "sum f A = Suc n \<Longrightarrow> \<exists>a\<in>A. 0 < f a"
   855   by (induct A rule: infinite_finite_induct) auto
   856 
   857 lemma sum_eq_Suc0_iff:
   858   "finite A \<Longrightarrow> sum f A = Suc 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = Suc 0 \<and> (\<forall>b\<in>A. a \<noteq> b \<longrightarrow> f b = 0))"
   859   by (induct A rule: finite_induct) (auto simp add: add_is_1)
   860 
   861 lemmas sum_eq_1_iff = sum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   862 
   863 lemma sum_Un_nat:
   864   "finite A \<Longrightarrow> finite B \<Longrightarrow> sum f (A \<union> B) = sum f A + sum f B - sum f (A \<inter> B)"
   865   for f :: "'a \<Rightarrow> nat"
   866   \<comment> \<open>For the natural numbers, we have subtraction.\<close>
   867   by (subst sum.union_inter [symmetric]) (auto simp: algebra_simps)
   868 
   869 lemma sum_diff1_nat: "sum f (A - {a}) = (if a \<in> A then sum f A - f a else sum f A)"
   870   for f :: "'a \<Rightarrow> nat"
   871 proof (induct A rule: infinite_finite_induct)
   872   case infinite
   873   then show ?case by simp
   874 next
   875   case empty
   876   then show ?case by simp
   877 next
   878   case insert
   879   then show ?case
   880     apply (auto simp: insert_Diff_if)
   881     apply (drule mk_disjoint_insert)
   882     apply auto
   883     done
   884 qed
   885 
   886 lemma sum_diff_nat:
   887   fixes f :: "'a \<Rightarrow> nat"
   888   assumes "finite B" and "B \<subseteq> A"
   889   shows "sum f (A - B) = sum f A - sum f B"
   890   using assms
   891 proof induct
   892   case empty
   893   then show ?case by simp
   894 next
   895   case (insert x F)
   896   note IH = \<open>F \<subseteq> A \<Longrightarrow> sum f (A - F) = sum f A - sum f F\<close>
   897   from \<open>x \<notin> F\<close> \<open>insert x F \<subseteq> A\<close> have "x \<in> A - F" by simp
   898   then have A: "sum f ((A - F) - {x}) = sum f (A - F) - f x"
   899     by (simp add: sum_diff1_nat)
   900   from \<open>insert x F \<subseteq> A\<close> have "F \<subseteq> A" by simp
   901   with IH have "sum f (A - F) = sum f A - sum f F" by simp
   902   with A have B: "sum f ((A - F) - {x}) = sum f A - sum f F - f x"
   903     by simp
   904   from \<open>x \<notin> F\<close> have "A - insert x F = (A - F) - {x}" by auto
   905   with B have C: "sum f (A - insert x F) = sum f A - sum f F - f x"
   906     by simp
   907   from \<open>finite F\<close> \<open>x \<notin> F\<close> have "sum f (insert x F) = sum f F + f x"
   908     by simp
   909   with C have "sum f (A - insert x F) = sum f A - sum f (insert x F)"
   910     by simp
   911   then show ?case by simp
   912 qed
   913 
   914 lemma sum_comp_morphism:
   915   "h 0 = 0 \<Longrightarrow> (\<And>x y. h (x + y) = h x + h y) \<Longrightarrow> sum (h \<circ> g) A = h (sum g A)"
   916   by (induct A rule: infinite_finite_induct) simp_all
   917 
   918 lemma (in comm_semiring_1) dvd_sum: "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd sum f A"
   919   by (induct A rule: infinite_finite_induct) simp_all
   920 
   921 lemma (in ordered_comm_monoid_add) sum_pos:
   922   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < sum f I"
   923   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
   924 
   925 lemma (in ordered_comm_monoid_add) sum_pos2:
   926   assumes I: "finite I" "i \<in> I" "0 < f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   927   shows "0 < sum f I"
   928 proof -
   929   have "0 < f i + sum f (I - {i})"
   930     using assms by (intro add_pos_nonneg sum_nonneg) auto
   931   also have "\<dots> = sum f I"
   932     using assms by (simp add: sum.remove)
   933   finally show ?thesis .
   934 qed
   935 
   936 lemma sum_cong_Suc:
   937   assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)"
   938   shows "sum f A = sum g A"
   939 proof (rule sum.cong)
   940   fix x
   941   assume "x \<in> A"
   942   with assms(1) show "f x = g x"
   943     by (cases x) (auto intro!: assms(2))
   944 qed simp_all
   945 
   946 
   947 subsubsection \<open>Cardinality as special case of @{const sum}\<close>
   948 
   949 lemma card_eq_sum: "card A = sum (\<lambda>x. 1) A"
   950 proof -
   951   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   952     by (simp add: fun_eq_iff)
   953   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   954     by (rule arg_cong)
   955   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   956     by (blast intro: fun_cong)
   957   then show ?thesis
   958     by (simp add: card.eq_fold sum.eq_fold)
   959 qed
   960 
   961 lemma sum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   962   by (induct A rule: infinite_finite_induct) (auto simp: algebra_simps)
   963 
   964 lemma sum_Suc: "sum (\<lambda>x. Suc(f x)) A = sum f A + card A"
   965   using sum.distrib[of f "\<lambda>_. 1" A] by simp
   966 
   967 lemma sum_bounded_above:
   968   fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}"
   969   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> K"
   970   shows "sum f A \<le> of_nat (card A) * K"
   971 proof (cases "finite A")
   972   case True
   973   then show ?thesis
   974     using le sum_mono[where K=A and g = "\<lambda>x. K"] by simp
   975 next
   976   case False
   977   then show ?thesis by simp
   978 qed
   979 
   980 lemma sum_bounded_above_strict:
   981   fixes K :: "'a::{ordered_cancel_comm_monoid_add,semiring_1}"
   982   assumes "\<And>i. i\<in>A \<Longrightarrow> f i < K" "card A > 0"
   983   shows "sum f A < of_nat (card A) * K"
   984   using assms sum_strict_mono[where A=A and g = "\<lambda>x. K"]
   985   by (simp add: card_gt_0_iff)
   986 
   987 lemma sum_bounded_below:
   988   fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}"
   989   assumes le: "\<And>i. i\<in>A \<Longrightarrow> K \<le> f i"
   990   shows "of_nat (card A) * K \<le> sum f A"
   991 proof (cases "finite A")
   992   case True
   993   then show ?thesis
   994     using le sum_mono[where K=A and f = "\<lambda>x. K"] by simp
   995 next
   996   case False
   997   then show ?thesis by simp
   998 qed
   999 
  1000 lemma card_UN_disjoint:
  1001   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
  1002     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
  1003   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
  1004 proof -
  1005   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)"
  1006     by simp
  1007   with assms show ?thesis
  1008     by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant)
  1009 qed
  1010 
  1011 lemma card_Union_disjoint:
  1012   "finite C \<Longrightarrow> \<forall>A\<in>C. finite A \<Longrightarrow> \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {} \<Longrightarrow>
  1013     card (\<Union>C) = sum card C"
  1014   by (frule card_UN_disjoint [of C id]) simp_all
  1015 
  1016 lemma sum_multicount_gen:
  1017   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
  1018   shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t"
  1019     (is "?l = ?r")
  1020 proof-
  1021   have "?l = sum (\<lambda>i. sum (\<lambda>x.1) {j\<in>t. R i j}) s"
  1022     by auto
  1023   also have "\<dots> = ?r"
  1024     unfolding sum.commute_restrict [OF assms(1-2)]
  1025     using assms(3) by auto
  1026   finally show ?thesis .
  1027 qed
  1028 
  1029 lemma sum_multicount:
  1030   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
  1031   shows "sum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
  1032 proof-
  1033   have "?l = sum (\<lambda>i. k) T"
  1034     by (rule sum_multicount_gen) (auto simp: assms)
  1035   also have "\<dots> = ?r" by (simp add: mult.commute)
  1036   finally show ?thesis by auto
  1037 qed
  1038 
  1039 
  1040 subsubsection \<open>Cardinality of products\<close>
  1041 
  1042 lemma card_SigmaI [simp]:
  1043   "finite A \<Longrightarrow> \<forall>a\<in>A. finite (B a) \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1044   by (simp add: card_eq_sum sum.Sigma del: sum_constant)
  1045 
  1046 (*
  1047 lemma SigmaI_insert: "y \<notin> A ==>
  1048   (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))"
  1049   by auto
  1050 *)
  1051 
  1052 lemma card_cartesian_product: "card (A \<times> B) = card A * card B"
  1053   by (cases "finite A \<and> finite B")
  1054     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1055 
  1056 lemma card_cartesian_product_singleton:  "card ({x} \<times> A) = card A"
  1057   by (simp add: card_cartesian_product)
  1058 
  1059 
  1060 subsection \<open>Generalized product over a set\<close>
  1061 
  1062 context comm_monoid_mult
  1063 begin
  1064 
  1065 sublocale prod: comm_monoid_set times 1
  1066   defines prod = prod.F ..
  1067 
  1068 abbreviation Prod ("\<Prod>_" [1000] 999)
  1069   where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
  1070 
  1071 end
  1072 
  1073 syntax (ASCII)
  1074   "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
  1075 syntax
  1076   "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
  1077 translations \<comment> \<open>Beware of argument permutation!\<close>
  1078   "\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
  1079 
  1080 text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
  1081 
  1082 syntax (ASCII)
  1083   "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
  1084 syntax
  1085   "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
  1086 translations
  1087   "\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
  1088 
  1089 context comm_monoid_mult
  1090 begin
  1091 
  1092 lemma prod_dvd_prod: "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> prod f A dvd prod g A"
  1093 proof (induct A rule: infinite_finite_induct)
  1094   case infinite
  1095   then show ?case by (auto intro: dvdI)
  1096 next
  1097   case empty
  1098   then show ?case by (auto intro: dvdI)
  1099 next
  1100   case (insert a A)
  1101   then have "f a dvd g a" and "prod f A dvd prod g A"
  1102     by simp_all
  1103   then obtain r s where "g a = f a * r" and "prod g A = prod f A * s"
  1104     by (auto elim!: dvdE)
  1105   then have "g a * prod g A = f a * prod f A * (r * s)"
  1106     by (simp add: ac_simps)
  1107   with insert.hyps show ?case
  1108     by (auto intro: dvdI)
  1109 qed
  1110 
  1111 lemma prod_dvd_prod_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> prod f A dvd prod f B"
  1112   by (auto simp add: prod.subset_diff ac_simps intro: dvdI)
  1113 
  1114 end
  1115 
  1116 
  1117 subsubsection \<open>Properties in more restricted classes of structures\<close>
  1118 
  1119 context linordered_nonzero_semiring
  1120 begin
  1121   
  1122 lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A"
  1123 proof (induct A rule: infinite_finite_induct)
  1124   case infinite
  1125   then show ?case by simp
  1126 next
  1127   case empty
  1128   then show ?case by simp
  1129 next
  1130   case (insert x F)
  1131   have "1 * 1 \<le> f x * prod f F"
  1132     by (rule mult_mono') (use insert in auto)
  1133   with insert show ?case by simp
  1134 qed
  1135 
  1136 lemma prod_le_1:
  1137   fixes f :: "'b \<Rightarrow> 'a"
  1138   assumes "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x \<and> f x \<le> 1"
  1139   shows "prod f A \<le> 1"
  1140     using assms
  1141 proof (induct A rule: infinite_finite_induct)
  1142   case infinite
  1143   then show ?case by simp
  1144 next
  1145   case empty
  1146   then show ?case by simp
  1147 next
  1148   case (insert x F)
  1149   then show ?case by (force simp: mult.commute intro: dest: mult_le_one)
  1150 qed
  1151 
  1152 end
  1153 
  1154 context comm_semiring_1
  1155 begin
  1156 
  1157 lemma dvd_prod_eqI [intro]:
  1158   assumes "finite A" and "a \<in> A" and "b = f a"
  1159   shows "b dvd prod f A"
  1160 proof -
  1161   from \<open>finite A\<close> have "prod f (insert a (A - {a})) = f a * prod f (A - {a})"
  1162     by (intro prod.insert) auto
  1163   also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A"
  1164     by blast
  1165   finally have "prod f A = f a * prod f (A - {a})" .
  1166   with \<open>b = f a\<close> show ?thesis
  1167     by simp
  1168 qed
  1169 
  1170 lemma dvd_prodI [intro]: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> f a dvd prod f A"
  1171   by auto
  1172 
  1173 lemma prod_zero:
  1174   assumes "finite A" and "\<exists>a\<in>A. f a = 0"
  1175   shows "prod f A = 0"
  1176   using assms
  1177 proof (induct A)
  1178   case empty
  1179   then show ?case by simp
  1180 next
  1181   case (insert a A)
  1182   then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
  1183   then have "f a * prod f A = 0" by rule (simp_all add: insert)
  1184   with insert show ?case by simp
  1185 qed
  1186 
  1187 lemma prod_dvd_prod_subset2:
  1188   assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
  1189   shows "prod f A dvd prod g B"
  1190 proof -
  1191   from assms have "prod f A dvd prod g A"
  1192     by (auto intro: prod_dvd_prod)
  1193   moreover from assms have "prod g A dvd prod g B"
  1194     by (auto intro: prod_dvd_prod_subset)
  1195   ultimately show ?thesis by (rule dvd_trans)
  1196 qed
  1197 
  1198 end
  1199 
  1200 lemma (in semidom) prod_zero_iff [simp]:
  1201   fixes f :: "'b \<Rightarrow> 'a"
  1202   assumes "finite A"
  1203   shows "prod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
  1204   using assms by (induct A) (auto simp: no_zero_divisors)
  1205 
  1206 lemma (in semidom_divide) prod_diff1:
  1207   assumes "finite A" and "f a \<noteq> 0"
  1208   shows "prod f (A - {a}) = (if a \<in> A then prod f A div f a else prod f A)"
  1209 proof (cases "a \<notin> A")
  1210   case True
  1211   then show ?thesis by simp
  1212 next
  1213   case False
  1214   with assms show ?thesis
  1215   proof induct
  1216     case empty
  1217     then show ?case by simp
  1218   next
  1219     case (insert b B)
  1220     then show ?case
  1221     proof (cases "a = b")
  1222       case True
  1223       with insert show ?thesis by simp
  1224     next
  1225       case False
  1226       with insert have "a \<in> B" by simp
  1227       define C where "C = B - {a}"
  1228       with \<open>finite B\<close> \<open>a \<in> B\<close> have "B = insert a C" "finite C" "a \<notin> C"
  1229         by auto
  1230       with insert show ?thesis
  1231         by (auto simp add: insert_commute ac_simps)
  1232     qed
  1233   qed
  1234 qed
  1235 
  1236 lemma sum_zero_power [simp]: "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
  1237   for c :: "nat \<Rightarrow> 'a::division_ring"
  1238   by (induct A rule: infinite_finite_induct) auto
  1239 
  1240 lemma sum_zero_power' [simp]:
  1241   "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
  1242   for c :: "nat \<Rightarrow> 'a::field"
  1243   using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto
  1244 
  1245 lemma (in field) prod_inversef: "prod (inverse \<circ> f) A = inverse (prod f A)"
  1246  proof (cases "finite A")
  1247    case True
  1248    then show ?thesis
  1249      by (induct A rule: finite_induct) simp_all
  1250  next
  1251    case False
  1252    then show ?thesis
  1253      by auto
  1254  qed
  1255 
  1256 lemma (in field) prod_dividef: "(\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
  1257   using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib)
  1258 
  1259 lemma prod_Un:
  1260   fixes f :: "'b \<Rightarrow> 'a :: field"
  1261   assumes "finite A" and "finite B"
  1262     and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
  1263   shows "prod f (A \<union> B) = prod f A * prod f B / prod f (A \<inter> B)"
  1264 proof -
  1265   from assms have "prod f A * prod f B = prod f (A \<union> B) * prod f (A \<inter> B)"
  1266     by (simp add: prod.union_inter [symmetric, of A B])
  1267   with assms show ?thesis
  1268     by simp
  1269 qed
  1270 
  1271 lemma (in linordered_semidom) prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
  1272   by (induct A rule: infinite_finite_induct) simp_all
  1273 
  1274 lemma (in linordered_semidom) prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
  1275   by (induct A rule: infinite_finite_induct) simp_all
  1276 
  1277 lemma (in linordered_semidom) prod_mono:
  1278   "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> prod f A \<le> prod g A"
  1279   by (induct A rule: infinite_finite_induct) (auto intro!: prod_nonneg mult_mono)
  1280 
  1281 lemma (in linordered_semidom) prod_mono_strict:
  1282   assumes "finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
  1283   shows "prod f A < prod g A"
  1284   using assms
  1285 proof (induct A rule: finite_induct)
  1286   case empty
  1287   then show ?case by simp
  1288 next
  1289   case insert
  1290   then show ?case by (force intro: mult_strict_mono' prod_nonneg)
  1291 qed
  1292 
  1293 lemma (in linordered_field) abs_prod: "\<bar>prod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
  1294   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
  1295 
  1296 lemma prod_eq_1_iff [simp]: "finite A \<Longrightarrow> prod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)"
  1297   for f :: "'a \<Rightarrow> nat"
  1298   by (induct A rule: finite_induct) simp_all
  1299 
  1300 lemma prod_pos_nat_iff [simp]: "finite A \<Longrightarrow> prod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)"
  1301   for f :: "'a \<Rightarrow> nat"
  1302   using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
  1303 
  1304 lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
  1305   for y :: "'a::comm_monoid_mult"
  1306   by (induct A rule: infinite_finite_induct) simp_all
  1307 
  1308 lemma prod_power_distrib: "prod f A ^ n = prod (\<lambda>x. (f x) ^ n) A"
  1309   for f :: "'a \<Rightarrow> 'b::comm_semiring_1"
  1310   by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib)
  1311 
  1312 lemma power_sum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
  1313   by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
  1314 
  1315 lemma prod_gen_delta:
  1316   fixes b :: "'b \<Rightarrow> 'a::comm_monoid_mult"
  1317   assumes fin: "finite S"
  1318   shows "prod (\<lambda>k. if k = a then b k else c) S =
  1319     (if a \<in> S then b a * c ^ (card S - 1) else c ^ card S)"
  1320 proof -
  1321   let ?f = "(\<lambda>k. if k=a then b k else c)"
  1322   show ?thesis
  1323   proof (cases "a \<in> S")
  1324     case False
  1325     then have "\<forall> k\<in> S. ?f k = c" by simp
  1326     with False show ?thesis by (simp add: prod_constant)
  1327   next
  1328     case True
  1329     let ?A = "S - {a}"
  1330     let ?B = "{a}"
  1331     from True have eq: "S = ?A \<union> ?B" by blast
  1332     have disjoint: "?A \<inter> ?B = {}" by simp
  1333     from fin have fin': "finite ?A" "finite ?B" by auto
  1334     have f_A0: "prod ?f ?A = prod (\<lambda>i. c) ?A"
  1335       by (rule prod.cong) auto
  1336     from fin True have card_A: "card ?A = card S - 1" by auto
  1337     have f_A1: "prod ?f ?A = c ^ card ?A"
  1338       unfolding f_A0 by (rule prod_constant)
  1339     have "prod ?f ?A * prod ?f ?B = prod ?f S"
  1340       using prod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]]
  1341       by simp
  1342     with True card_A show ?thesis
  1343       by (simp add: f_A1 field_simps cong add: prod.cong cong del: if_weak_cong)
  1344   qed
  1345 qed
  1346 
  1347 lemma sum_image_le:
  1348   fixes g :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
  1349   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)"
  1350     shows "sum g (f ` I) \<le> sum (g \<circ> f) I"
  1351   using assms
  1352 proof induction
  1353   case empty
  1354   then show ?case by auto
  1355 next
  1356   case (insert x F) then
  1357   have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp
  1358   also have "\<dots> \<le> g (f x) + sum g (f ` F)"
  1359     by (simp add: insert sum.insert_if)
  1360   also have "\<dots>  \<le> sum (g \<circ> f) (insert x F)"
  1361     using insert by auto
  1362   finally show ?case .
  1363 qed
  1364  
  1365 end