src/HOL/Groups_Big.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 66936 cf8d8fc23891
child 67268 bdf25939a550
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     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 swap: "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 swap_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 swap)
   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.swap_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 context semiring_0
   765 begin
   766 
   767 lemma sum_distrib_left: "r * sum f A = (\<Sum>n\<in>A. r * f n)"
   768   by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
   769 
   770 lemma sum_distrib_right: "sum f A * r = (\<Sum>n\<in>A. f n * r)"
   771   by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
   772 
   773 end
   774 
   775 lemma sum_divide_distrib: "sum f A / r = (\<Sum>n\<in>A. f n / r)"
   776   for r :: "'a::field"
   777 proof (induct A rule: infinite_finite_induct)
   778   case infinite
   779   then show ?case by simp
   780 next
   781   case empty
   782   then show ?case by simp
   783 next
   784   case insert
   785   then show ?case by (simp add: add_divide_distrib)
   786 qed
   787 
   788 lemma sum_abs[iff]: "\<bar>sum f A\<bar> \<le> sum (\<lambda>i. \<bar>f i\<bar>) A"
   789   for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   790 proof (induct A rule: infinite_finite_induct)
   791   case infinite
   792   then show ?case by simp
   793 next
   794   case empty
   795   then show ?case by simp
   796 next
   797   case insert
   798   then show ?case by (auto intro: abs_triangle_ineq order_trans)
   799 qed
   800 
   801 lemma sum_abs_ge_zero[iff]: "0 \<le> sum (\<lambda>i. \<bar>f i\<bar>) A"
   802   for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   803   by (simp add: sum_nonneg)
   804 
   805 lemma abs_sum_abs[simp]: "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
   806   for f :: "'a \<Rightarrow> 'b::ordered_ab_group_add_abs"
   807 proof (induct A rule: infinite_finite_induct)
   808   case infinite
   809   then show ?case by simp
   810 next
   811   case empty
   812   then show ?case by simp
   813 next
   814   case (insert a A)
   815   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
   816   also from insert have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" by simp
   817   also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by (simp del: abs_of_nonneg)
   818   also from insert have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" by simp
   819   finally show ?case .
   820 qed
   821 
   822 lemma sum_diff1_ring:
   823   fixes f :: "'b \<Rightarrow> 'a::ring"
   824   assumes "finite A" "a \<in> A"
   825   shows "sum f (A - {a}) = sum f A - (f a)"
   826   unfolding sum.remove [OF assms] by auto
   827 
   828 lemma sum_product:
   829   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   830   shows "sum f A * sum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   831   by (simp add: sum_distrib_left sum_distrib_right) (rule sum.swap)
   832 
   833 lemma sum_mult_sum_if_inj:
   834   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
   835   shows "inj_on (\<lambda>(a, b). f a * g b) (A \<times> B) \<Longrightarrow>
   836     sum f A * sum g B = sum id {f a * g b |a b. a \<in> A \<and> b \<in> B}"
   837   by(auto simp: sum_product sum.cartesian_product intro!: sum.reindex_cong[symmetric])
   838 
   839 lemma sum_SucD: "sum f A = Suc n \<Longrightarrow> \<exists>a\<in>A. 0 < f a"
   840   by (induct A rule: infinite_finite_induct) auto
   841 
   842 lemma sum_eq_Suc0_iff:
   843   "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))"
   844   by (induct A rule: finite_induct) (auto simp add: add_is_1)
   845 
   846 lemmas sum_eq_1_iff = sum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
   847 
   848 lemma sum_Un_nat:
   849   "finite A \<Longrightarrow> finite B \<Longrightarrow> sum f (A \<union> B) = sum f A + sum f B - sum f (A \<inter> B)"
   850   for f :: "'a \<Rightarrow> nat"
   851   \<comment> \<open>For the natural numbers, we have subtraction.\<close>
   852   by (subst sum.union_inter [symmetric]) (auto simp: algebra_simps)
   853 
   854 lemma sum_diff1_nat: "sum f (A - {a}) = (if a \<in> A then sum f A - f a else sum f A)"
   855   for f :: "'a \<Rightarrow> nat"
   856 proof (induct A rule: infinite_finite_induct)
   857   case infinite
   858   then show ?case by simp
   859 next
   860   case empty
   861   then show ?case by simp
   862 next
   863   case insert
   864   then show ?case
   865     apply (auto simp: insert_Diff_if)
   866     apply (drule mk_disjoint_insert)
   867     apply auto
   868     done
   869 qed
   870 
   871 lemma sum_diff_nat:
   872   fixes f :: "'a \<Rightarrow> nat"
   873   assumes "finite B" and "B \<subseteq> A"
   874   shows "sum f (A - B) = sum f A - sum f B"
   875   using assms
   876 proof induct
   877   case empty
   878   then show ?case by simp
   879 next
   880   case (insert x F)
   881   note IH = \<open>F \<subseteq> A \<Longrightarrow> sum f (A - F) = sum f A - sum f F\<close>
   882   from \<open>x \<notin> F\<close> \<open>insert x F \<subseteq> A\<close> have "x \<in> A - F" by simp
   883   then have A: "sum f ((A - F) - {x}) = sum f (A - F) - f x"
   884     by (simp add: sum_diff1_nat)
   885   from \<open>insert x F \<subseteq> A\<close> have "F \<subseteq> A" by simp
   886   with IH have "sum f (A - F) = sum f A - sum f F" by simp
   887   with A have B: "sum f ((A - F) - {x}) = sum f A - sum f F - f x"
   888     by simp
   889   from \<open>x \<notin> F\<close> have "A - insert x F = (A - F) - {x}" by auto
   890   with B have C: "sum f (A - insert x F) = sum f A - sum f F - f x"
   891     by simp
   892   from \<open>finite F\<close> \<open>x \<notin> F\<close> have "sum f (insert x F) = sum f F + f x"
   893     by simp
   894   with C have "sum f (A - insert x F) = sum f A - sum f (insert x F)"
   895     by simp
   896   then show ?case by simp
   897 qed
   898 
   899 lemma sum_comp_morphism:
   900   "h 0 = 0 \<Longrightarrow> (\<And>x y. h (x + y) = h x + h y) \<Longrightarrow> sum (h \<circ> g) A = h (sum g A)"
   901   by (induct A rule: infinite_finite_induct) simp_all
   902 
   903 lemma (in comm_semiring_1) dvd_sum: "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd sum f A"
   904   by (induct A rule: infinite_finite_induct) simp_all
   905 
   906 lemma (in ordered_comm_monoid_add) sum_pos:
   907   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < sum f I"
   908   by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
   909 
   910 lemma (in ordered_comm_monoid_add) sum_pos2:
   911   assumes I: "finite I" "i \<in> I" "0 < f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   912   shows "0 < sum f I"
   913 proof -
   914   have "0 < f i + sum f (I - {i})"
   915     using assms by (intro add_pos_nonneg sum_nonneg) auto
   916   also have "\<dots> = sum f I"
   917     using assms by (simp add: sum.remove)
   918   finally show ?thesis .
   919 qed
   920 
   921 lemma sum_cong_Suc:
   922   assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)"
   923   shows "sum f A = sum g A"
   924 proof (rule sum.cong)
   925   fix x
   926   assume "x \<in> A"
   927   with assms(1) show "f x = g x"
   928     by (cases x) (auto intro!: assms(2))
   929 qed simp_all
   930 
   931 
   932 subsubsection \<open>Cardinality as special case of @{const sum}\<close>
   933 
   934 lemma card_eq_sum: "card A = sum (\<lambda>x. 1) A"
   935 proof -
   936   have "plus \<circ> (\<lambda>_. Suc 0) = (\<lambda>_. Suc)"
   937     by (simp add: fun_eq_iff)
   938   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) = Finite_Set.fold (\<lambda>_. Suc)"
   939     by (rule arg_cong)
   940   then have "Finite_Set.fold (plus \<circ> (\<lambda>_. Suc 0)) 0 A = Finite_Set.fold (\<lambda>_. Suc) 0 A"
   941     by (blast intro: fun_cong)
   942   then show ?thesis
   943     by (simp add: card.eq_fold sum.eq_fold)
   944 qed
   945 
   946 context semiring_1
   947 begin
   948 
   949 lemma sum_constant [simp]:
   950   "(\<Sum>x \<in> A. y) = of_nat (card A) * y"
   951   by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
   952 
   953 end
   954 
   955 lemma sum_Suc: "sum (\<lambda>x. Suc(f x)) A = sum f A + card A"
   956   using sum.distrib[of f "\<lambda>_. 1" A] by simp
   957 
   958 lemma sum_bounded_above:
   959   fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}"
   960   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> K"
   961   shows "sum f A \<le> of_nat (card A) * K"
   962 proof (cases "finite A")
   963   case True
   964   then show ?thesis
   965     using le sum_mono[where K=A and g = "\<lambda>x. K"] by simp
   966 next
   967   case False
   968   then show ?thesis by simp
   969 qed
   970 
   971 lemma sum_bounded_above_strict:
   972   fixes K :: "'a::{ordered_cancel_comm_monoid_add,semiring_1}"
   973   assumes "\<And>i. i\<in>A \<Longrightarrow> f i < K" "card A > 0"
   974   shows "sum f A < of_nat (card A) * K"
   975   using assms sum_strict_mono[where A=A and g = "\<lambda>x. K"]
   976   by (simp add: card_gt_0_iff)
   977 
   978 lemma sum_bounded_below:
   979   fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}"
   980   assumes le: "\<And>i. i\<in>A \<Longrightarrow> K \<le> f i"
   981   shows "of_nat (card A) * K \<le> sum f A"
   982 proof (cases "finite A")
   983   case True
   984   then show ?thesis
   985     using le sum_mono[where K=A and f = "\<lambda>x. K"] by simp
   986 next
   987   case False
   988   then show ?thesis by simp
   989 qed
   990 
   991 lemma card_UN_disjoint:
   992   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
   993     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
   994   shows "card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   995 proof -
   996   have "(\<Sum>i\<in>I. card (A i)) = (\<Sum>i\<in>I. \<Sum>x\<in>A i. 1)"
   997     by simp
   998   with assms show ?thesis
   999     by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant)
  1000 qed
  1001 
  1002 lemma card_Union_disjoint:
  1003   "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>
  1004     card (\<Union>C) = sum card C"
  1005   by (frule card_UN_disjoint [of C id]) simp_all
  1006 
  1007 lemma sum_multicount_gen:
  1008   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
  1009   shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t"
  1010     (is "?l = ?r")
  1011 proof-
  1012   have "?l = sum (\<lambda>i. sum (\<lambda>x.1) {j\<in>t. R i j}) s"
  1013     by auto
  1014   also have "\<dots> = ?r"
  1015     unfolding sum.swap_restrict [OF assms(1-2)]
  1016     using assms(3) by auto
  1017   finally show ?thesis .
  1018 qed
  1019 
  1020 lemma sum_multicount:
  1021   assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)"
  1022   shows "sum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r")
  1023 proof-
  1024   have "?l = sum (\<lambda>i. k) T"
  1025     by (rule sum_multicount_gen) (auto simp: assms)
  1026   also have "\<dots> = ?r" by (simp add: mult.commute)
  1027   finally show ?thesis by auto
  1028 qed
  1029 
  1030 
  1031 subsubsection \<open>Cardinality of products\<close>
  1032 
  1033 lemma card_SigmaI [simp]:
  1034   "finite A \<Longrightarrow> \<forall>a\<in>A. finite (B a) \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
  1035   by (simp add: card_eq_sum sum.Sigma del: sum_constant)
  1036 
  1037 (*
  1038 lemma SigmaI_insert: "y \<notin> A ==>
  1039   (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))"
  1040   by auto
  1041 *)
  1042 
  1043 lemma card_cartesian_product: "card (A \<times> B) = card A * card B"
  1044   by (cases "finite A \<and> finite B")
  1045     (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)
  1046 
  1047 lemma card_cartesian_product_singleton:  "card ({x} \<times> A) = card A"
  1048   by (simp add: card_cartesian_product)
  1049 
  1050 
  1051 subsection \<open>Generalized product over a set\<close>
  1052 
  1053 context comm_monoid_mult
  1054 begin
  1055 
  1056 sublocale prod: comm_monoid_set times 1
  1057   defines prod = prod.F ..
  1058 
  1059 abbreviation Prod ("\<Prod>_" [1000] 999)
  1060   where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
  1061 
  1062 end
  1063 
  1064 syntax (ASCII)
  1065   "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
  1066 syntax
  1067   "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
  1068 translations \<comment> \<open>Beware of argument permutation!\<close>
  1069   "\<Prod>i\<in>A. b" == "CONST prod (\<lambda>i. b) A"
  1070 
  1071 text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
  1072 
  1073 syntax (ASCII)
  1074   "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
  1075 syntax
  1076   "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
  1077 translations
  1078   "\<Prod>x|P. t" => "CONST prod (\<lambda>x. t) {x. P}"
  1079 
  1080 context comm_monoid_mult
  1081 begin
  1082 
  1083 lemma prod_dvd_prod: "(\<And>a. a \<in> A \<Longrightarrow> f a dvd g a) \<Longrightarrow> prod f A dvd prod g A"
  1084 proof (induct A rule: infinite_finite_induct)
  1085   case infinite
  1086   then show ?case by (auto intro: dvdI)
  1087 next
  1088   case empty
  1089   then show ?case by (auto intro: dvdI)
  1090 next
  1091   case (insert a A)
  1092   then have "f a dvd g a" and "prod f A dvd prod g A"
  1093     by simp_all
  1094   then obtain r s where "g a = f a * r" and "prod g A = prod f A * s"
  1095     by (auto elim!: dvdE)
  1096   then have "g a * prod g A = f a * prod f A * (r * s)"
  1097     by (simp add: ac_simps)
  1098   with insert.hyps show ?case
  1099     by (auto intro: dvdI)
  1100 qed
  1101 
  1102 lemma prod_dvd_prod_subset: "finite B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> prod f A dvd prod f B"
  1103   by (auto simp add: prod.subset_diff ac_simps intro: dvdI)
  1104 
  1105 end
  1106 
  1107 
  1108 subsubsection \<open>Properties in more restricted classes of structures\<close>
  1109 
  1110 context linordered_nonzero_semiring
  1111 begin
  1112   
  1113 lemma prod_ge_1: "(\<And>x. x \<in> A \<Longrightarrow> 1 \<le> f x) \<Longrightarrow> 1 \<le> prod f A"
  1114 proof (induct A rule: infinite_finite_induct)
  1115   case infinite
  1116   then show ?case by simp
  1117 next
  1118   case empty
  1119   then show ?case by simp
  1120 next
  1121   case (insert x F)
  1122   have "1 * 1 \<le> f x * prod f F"
  1123     by (rule mult_mono') (use insert in auto)
  1124   with insert show ?case by simp
  1125 qed
  1126 
  1127 lemma prod_le_1:
  1128   fixes f :: "'b \<Rightarrow> 'a"
  1129   assumes "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x \<and> f x \<le> 1"
  1130   shows "prod f A \<le> 1"
  1131     using assms
  1132 proof (induct A rule: infinite_finite_induct)
  1133   case infinite
  1134   then show ?case by simp
  1135 next
  1136   case empty
  1137   then show ?case by simp
  1138 next
  1139   case (insert x F)
  1140   then show ?case by (force simp: mult.commute intro: dest: mult_le_one)
  1141 qed
  1142 
  1143 end
  1144 
  1145 context comm_semiring_1
  1146 begin
  1147 
  1148 lemma dvd_prod_eqI [intro]:
  1149   assumes "finite A" and "a \<in> A" and "b = f a"
  1150   shows "b dvd prod f A"
  1151 proof -
  1152   from \<open>finite A\<close> have "prod f (insert a (A - {a})) = f a * prod f (A - {a})"
  1153     by (intro prod.insert) auto
  1154   also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A"
  1155     by blast
  1156   finally have "prod f A = f a * prod f (A - {a})" .
  1157   with \<open>b = f a\<close> show ?thesis
  1158     by simp
  1159 qed
  1160 
  1161 lemma dvd_prodI [intro]: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> f a dvd prod f A"
  1162   by auto
  1163 
  1164 lemma prod_zero:
  1165   assumes "finite A" and "\<exists>a\<in>A. f a = 0"
  1166   shows "prod f A = 0"
  1167   using assms
  1168 proof (induct A)
  1169   case empty
  1170   then show ?case by simp
  1171 next
  1172   case (insert a A)
  1173   then have "f a = 0 \<or> (\<exists>a\<in>A. f a = 0)" by simp
  1174   then have "f a * prod f A = 0" by rule (simp_all add: insert)
  1175   with insert show ?case by simp
  1176 qed
  1177 
  1178 lemma prod_dvd_prod_subset2:
  1179   assumes "finite B" and "A \<subseteq> B" and "\<And>a. a \<in> A \<Longrightarrow> f a dvd g a"
  1180   shows "prod f A dvd prod g B"
  1181 proof -
  1182   from assms have "prod f A dvd prod g A"
  1183     by (auto intro: prod_dvd_prod)
  1184   moreover from assms have "prod g A dvd prod g B"
  1185     by (auto intro: prod_dvd_prod_subset)
  1186   ultimately show ?thesis by (rule dvd_trans)
  1187 qed
  1188 
  1189 end
  1190 
  1191 lemma (in semidom) prod_zero_iff [simp]:
  1192   fixes f :: "'b \<Rightarrow> 'a"
  1193   assumes "finite A"
  1194   shows "prod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
  1195   using assms by (induct A) (auto simp: no_zero_divisors)
  1196 
  1197 lemma (in semidom_divide) prod_diff1:
  1198   assumes "finite A" and "f a \<noteq> 0"
  1199   shows "prod f (A - {a}) = (if a \<in> A then prod f A div f a else prod f A)"
  1200 proof (cases "a \<notin> A")
  1201   case True
  1202   then show ?thesis by simp
  1203 next
  1204   case False
  1205   with assms show ?thesis
  1206   proof induct
  1207     case empty
  1208     then show ?case by simp
  1209   next
  1210     case (insert b B)
  1211     then show ?case
  1212     proof (cases "a = b")
  1213       case True
  1214       with insert show ?thesis by simp
  1215     next
  1216       case False
  1217       with insert have "a \<in> B" by simp
  1218       define C where "C = B - {a}"
  1219       with \<open>finite B\<close> \<open>a \<in> B\<close> have "B = insert a C" "finite C" "a \<notin> C"
  1220         by auto
  1221       with insert show ?thesis
  1222         by (auto simp add: insert_commute ac_simps)
  1223     qed
  1224   qed
  1225 qed
  1226 
  1227 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)"
  1228   for c :: "nat \<Rightarrow> 'a::division_ring"
  1229   by (induct A rule: infinite_finite_induct) auto
  1230 
  1231 lemma sum_zero_power' [simp]:
  1232   "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
  1233   for c :: "nat \<Rightarrow> 'a::field"
  1234   using sum_zero_power [of "\<lambda>i. c i / d i" A] by auto
  1235 
  1236 lemma (in field) prod_inversef: "prod (inverse \<circ> f) A = inverse (prod f A)"
  1237  proof (cases "finite A")
  1238    case True
  1239    then show ?thesis
  1240      by (induct A rule: finite_induct) simp_all
  1241  next
  1242    case False
  1243    then show ?thesis
  1244      by auto
  1245  qed
  1246 
  1247 lemma (in field) prod_dividef: "(\<Prod>x\<in>A. f x / g x) = prod f A / prod g A"
  1248   using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib)
  1249 
  1250 lemma prod_Un:
  1251   fixes f :: "'b \<Rightarrow> 'a :: field"
  1252   assumes "finite A" and "finite B"
  1253     and "\<forall>x\<in>A \<inter> B. f x \<noteq> 0"
  1254   shows "prod f (A \<union> B) = prod f A * prod f B / prod f (A \<inter> B)"
  1255 proof -
  1256   from assms have "prod f A * prod f B = prod f (A \<union> B) * prod f (A \<inter> B)"
  1257     by (simp add: prod.union_inter [symmetric, of A B])
  1258   with assms show ?thesis
  1259     by simp
  1260 qed
  1261 
  1262 lemma (in linordered_semidom) prod_nonneg: "(\<forall>a\<in>A. 0 \<le> f a) \<Longrightarrow> 0 \<le> prod f A"
  1263   by (induct A rule: infinite_finite_induct) simp_all
  1264 
  1265 lemma (in linordered_semidom) prod_pos: "(\<forall>a\<in>A. 0 < f a) \<Longrightarrow> 0 < prod f A"
  1266   by (induct A rule: infinite_finite_induct) simp_all
  1267 
  1268 lemma (in linordered_semidom) prod_mono:
  1269   "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> prod f A \<le> prod g A"
  1270   by (induct A rule: infinite_finite_induct) (auto intro!: prod_nonneg mult_mono)
  1271 
  1272 lemma (in linordered_semidom) prod_mono_strict:
  1273   assumes "finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
  1274   shows "prod f A < prod g A"
  1275   using assms
  1276 proof (induct A rule: finite_induct)
  1277   case empty
  1278   then show ?case by simp
  1279 next
  1280   case insert
  1281   then show ?case by (force intro: mult_strict_mono' prod_nonneg)
  1282 qed
  1283 
  1284 lemma (in linordered_field) abs_prod: "\<bar>prod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
  1285   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
  1286 
  1287 lemma prod_eq_1_iff [simp]: "finite A \<Longrightarrow> prod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = 1)"
  1288   for f :: "'a \<Rightarrow> nat"
  1289   by (induct A rule: finite_induct) simp_all
  1290 
  1291 lemma prod_pos_nat_iff [simp]: "finite A \<Longrightarrow> prod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > 0)"
  1292   for f :: "'a \<Rightarrow> nat"
  1293   using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
  1294 
  1295 lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
  1296   for y :: "'a::comm_monoid_mult"
  1297   by (induct A rule: infinite_finite_induct) simp_all
  1298 
  1299 lemma prod_power_distrib: "prod f A ^ n = prod (\<lambda>x. (f x) ^ n) A"
  1300   for f :: "'a \<Rightarrow> 'b::comm_semiring_1"
  1301   by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib)
  1302 
  1303 lemma power_sum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
  1304   by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
  1305 
  1306 lemma prod_gen_delta:
  1307   fixes b :: "'b \<Rightarrow> 'a::comm_monoid_mult"
  1308   assumes fin: "finite S"
  1309   shows "prod (\<lambda>k. if k = a then b k else c) S =
  1310     (if a \<in> S then b a * c ^ (card S - 1) else c ^ card S)"
  1311 proof -
  1312   let ?f = "(\<lambda>k. if k=a then b k else c)"
  1313   show ?thesis
  1314   proof (cases "a \<in> S")
  1315     case False
  1316     then have "\<forall> k\<in> S. ?f k = c" by simp
  1317     with False show ?thesis by (simp add: prod_constant)
  1318   next
  1319     case True
  1320     let ?A = "S - {a}"
  1321     let ?B = "{a}"
  1322     from True have eq: "S = ?A \<union> ?B" by blast
  1323     have disjoint: "?A \<inter> ?B = {}" by simp
  1324     from fin have fin': "finite ?A" "finite ?B" by auto
  1325     have f_A0: "prod ?f ?A = prod (\<lambda>i. c) ?A"
  1326       by (rule prod.cong) auto
  1327     from fin True have card_A: "card ?A = card S - 1" by auto
  1328     have f_A1: "prod ?f ?A = c ^ card ?A"
  1329       unfolding f_A0 by (rule prod_constant)
  1330     have "prod ?f ?A * prod ?f ?B = prod ?f S"
  1331       using prod.union_disjoint[OF fin' disjoint, of ?f, unfolded eq[symmetric]]
  1332       by simp
  1333     with True card_A show ?thesis
  1334       by (simp add: f_A1 field_simps cong add: prod.cong cong del: if_weak_cong)
  1335   qed
  1336 qed
  1337 
  1338 lemma sum_image_le:
  1339   fixes g :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
  1340   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)"
  1341     shows "sum g (f ` I) \<le> sum (g \<circ> f) I"
  1342   using assms
  1343 proof induction
  1344   case empty
  1345   then show ?case by auto
  1346 next
  1347   case (insert x F) then
  1348   have "sum g (f ` insert x F) = sum g (insert (f x) (f ` F))" by simp
  1349   also have "\<dots> \<le> g (f x) + sum g (f ` F)"
  1350     by (simp add: insert sum.insert_if)
  1351   also have "\<dots>  \<le> sum (g \<circ> f) (insert x F)"
  1352     using insert by auto
  1353   finally show ?case .
  1354 qed
  1355  
  1356 end