Quelle Groups_Big.thy Sprache: Isabelle

(*  Title:      HOL/Groups_Big.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
    Author:     Jeremy Avigad
*)

section \<open>Big sum and product over finite (non-empty) sets\<close>

theory Groups_Big
  imports Power Equiv_Relations
begin

subsection \<open>Generic monoid operation over a set\<close>

locale comm_monoid_set = comm_monoid
begin

subsubsection \<open>Standard sum or product indexed by a finite set\<close>

interpretation comp_fun_commute f
  by standard (simp add: fun_eq_iff left_commute)

interpretation comp?: comp_fun_commute "f \ g"
  by (fact comp_comp_fun_commute)

definition F :: "('b \ 'a) \ 'b set \ 'a"
  where eq_fold: "F g A = Finite_Set.fold (f \ g) \<^bold>1 A"

lemma infinite [simp]: "\ finite A \ F g A = \<^bold>1"
  by (simp add: eq_fold)

lemma empty [simp]: "F g {} = \<^bold>1"
  by (simp add: eq_fold)

lemma insert [simp]: "finite A \ x \ A \ F g (insert x A) = g x \<^bold>* F g A"
  by (simp add: eq_fold)

lemma remove:
  assumes "finite A" and "x \ A"
  shows "F g A = g x \<^bold>* F g (A - {x})"
proof -
  from \<open>x \<in> A\<close> obtain B where B: "A = insert x B" and "x \<notin> B"
    by (auto dest: mk_disjoint_insert)
  moreover from \<open>finite A\<close> B have "finite B" by simp
  ultimately show ?thesis by simp
qed

lemma insert_remove: "finite A \ F g (insert x A) = g x \<^bold>* F g (A - {x})"
  by (cases "x \ A") (simp_all add: remove insert_absorb)

lemma insert_if: "finite A \ F g (insert x A) = (if x \ A then F g A else g x \<^bold>* F g A)"
  by (cases "x \ A") (simp_all add: insert_absorb)

lemma neutral: "\x\A. g x = \<^bold>1 \ F g A = \<^bold>1"
  by (induct A rule: infinite_finite_induct) simp_all

lemma neutral_const [simp]: "F (\_. \<^bold>1) A = \<^bold>1"
  by (simp add: neutral)

lemma union_inter:
  assumes "finite A" and "finite B"
  shows "F g (A \ B) \<^bold>* F g (A \ B) = F g A \<^bold>* F g B"
  \<comment> \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
  using assms
proof (induct A)
  case empty
  then show ?case by simp
next
  case (insert x A)
  then show ?case
    by (auto simp: insert_absorb Int_insert_left commute [of _ "g x"] assoc left_commute)
qed

corollary union_inter_neutral:
  assumes "finite A" and "finite B"
    and "\x \ A \ B. g x = \<^bold>1"
  shows "F g (A \ B) = F g A \<^bold>* F g B"
  using assms by (simp add: union_inter [symmetric] neutral)

corollary union_disjoint:
  assumes "finite A" and "finite B"
  assumes "A \ B = {}"
  shows "F g (A \ B) = F g A \<^bold>* F g B"
  using assms by (simp add: union_inter_neutral)

lemma union_diff2:
  assumes "finite A" and "finite B"
  shows "F g (A \ B) = F g (A - B) \<^bold>* F g (B - A) \<^bold>* F g (A \ B)"
proof -
  have "A \ B = A - B \ (B - A) \ A \ B"
    by auto
  with assms show ?thesis
    by simp (subst union_disjoint, auto)+
qed

lemma subset_diff:
  assumes "B \ A" and "finite A"
  shows "F g A = F g (A - B) \<^bold>* F g B"
proof -
  from assms have "finite (A - B)" by auto
  moreover from assms have "finite B" by (rule finite_subset)
  moreover from assms have "(A - B) \ B = {}" by auto
  ultimately have "F g (A - B \ B) = F g (A - B) \<^bold>* F g B" by (rule union_disjoint)
  moreover from assms have "A \ B = A" by auto
  ultimately show ?thesis by simp
qed

lemma Int_Diff:
  assumes "finite A"
  shows "F g A = F g (A \ B) \<^bold>* F g (A - B)"
  by (subst subset_diff [where B = "A - B"]) (auto simp:  Diff_Diff_Int assms)

lemma setdiff_irrelevant:
  assumes "finite A"
  shows "F g (A - {x. g x = z}) = F g A"
  using assms by (induct A) (simp_all add: insert_Diff_if)

lemma not_neutral_contains_not_neutral:
  assumes "F g A \ \<^bold>1"
  obtains a where "a \ A" and "g a \ \<^bold>1"
proof -
  from assms have "\a\A. g a \ \<^bold>1"
  proof (induct A rule: infinite_finite_induct)
    case infinite
    then show ?case by simp
  next
    case empty
    then show ?case by simp
  next
    case (insert a A)
    then show ?case by fastforce
  qed
  with that show thesis by blast
qed

lemma reindex:
  assumes "inj_on h A"
  shows "F g (h ` A) = F (g \ h) A"
proof (cases "finite A")
  case True
  with assms show ?thesis
    by (simp add: eq_fold fold_image comp_assoc)
next
  case False
  with assms have "\ finite (h ` A)" by (blast dest: finite_imageD)
  with False show ?thesis by simp
qed

lemma cong [fundef_cong]:
  assumes "A = B"
  assumes g_h: "\x. x \ B \ g x = h x"
  shows "F g A = F h B"
  using g_h unfolding \<open>A = B\<close>
  by (induct B rule: infinite_finite_induct) auto

lemma cong_simp [cong]:
  "\ A = B; \x. x \ B =simp=> g x = h x \ \ F (\x. g x) A = F (\x. h x) B"
by (rule cong) (simp_all add: simp_implies_def)

lemma reindex_cong:
  assumes "inj_on l B"
  assumes "A = l ` B"
  assumes "\x. x \ B \ g (l x) = h x"
  shows "F g A = F h B"
  using assms by (simp add: reindex)

lemma image_eq:
  assumes "inj_on g A"
  shows "F (\x. x) (g ` A) = F g A"
  using assms reindex_cong by fastforce

lemma UNION_disjoint:
  assumes "finite I" and "\i\I. finite (A i)"
    and "\i\I. \j\I. i \ j \ A i \ A j = {}"
  shows "F g (\(A ` I)) = F (\x. F g (A x)) I"
  using assms
proof (induction rule: finite_induct)
  case (insert i I)
  then have "\j\I. j \ i"
    by blast
  with insert.prems have "A i \ \(A ` I) = {}"
    by blast
  with insert show ?case
    by (simp add: union_disjoint)
qed auto

lemma Union_disjoint:
  assumes "\A\C. finite A" "\A\C. \B\C. A \ B \ A \ B = {}"
  shows "F g (\C) = (F \ F) g C"
proof (cases "finite C")
  case True
  from UNION_disjoint [OF this assms] show ?thesis by simp
next
  case False
  then show ?thesis by (auto dest: finite_UnionD intro: infinite)
qed

lemma distrib: "F (\x. g x \<^bold>* h x) A = F g A \<^bold>* F h A"
  by (induct A rule: infinite_finite_induct) (simp_all add: assoc commute left_commute)

lemma Sigma:
  assumes "finite A" "\x\A. finite (B x)"
  shows "F (\x. F (g x) (B x)) A = F (case_prod g) (SIGMA x:A. B x)"
  unfolding Sigma_def
proof (subst UNION_disjoint)
  show "F (\x. F (g x) (B x)) A = F (\x. F (\(x, y). g x y) (\y\B x. {(x, y)})) A"
  proof (rule cong [OF refl])
    show "F (g x) (B x) = F (\(x, y). g x y) (\y\B x. {(x, y)})"
      if "x \ A" for x
      using that assms by (simp add: UNION_disjoint)
  qed
qed (use assms in auto)

lemma related:
  assumes Re: "R \<^bold>1 \<^bold>1"
    and Rop: "\x1 y1 x2 y2. R x1 x2 \ R y1 y2 \ R (x1 \<^bold>* y1) (x2 \<^bold>* y2)"
    and fin: "finite S"
    and R_h_g: "\x\S. R (h x) (g x)"
  shows "R (F h S) (F g S)"
  using fin by (rule finite_subset_induct) (use assms in auto)

lemma mono_neutral_cong_left:
  assumes "finite T"
    and "S \ T"
    and "\i \ T - S. h i = \<^bold>1"
    and "\x. x \ S \ g x = h x"
  shows "F g S = F h T"
proof-
  have eq: "T = S \ (T - S)" using \S \ T\ by blast
  have d: "S \ (T - S) = {}" using \S \ T\ by blast
  from \<open>finite T\<close> \<open>S \<subseteq> T\<close> have f: "finite S" "finite (T - S)"
    by (auto intro: finite_subset)
  show ?thesis using assms(4)
    by (simp add: union_disjoint [OF f d, unfolded eq [symmetric]] neutral [OF assms(3)])
qed

lemma mono_neutral_cong_right:
  "finite T \ S \ T \ \i \ T - S. g i = \<^bold>1 \ (\x. x \ S \ g x = h x) \
    F g T = F h S"
  by (auto intro!: mono_neutral_cong_left [symmetric])

lemma mono_neutral_left: "finite T \ S \ T \ \i \ T - S. g i = \<^bold>1 \ F g S = F g T"
  by (blast intro: mono_neutral_cong_left)

lemma mono_neutral_right: "finite T \ S \ T \ \i \ T - S. g i = \<^bold>1 \ F g T = F g S"
  by (blast intro!: mono_neutral_left [symmetric])

lemma mono_neutral_cong:
  assumes [simp]: "finite T" "finite S"
    and *: "\i. i \ T - S \ h i = \<^bold>1" "\i. i \ S - T \ g i = \<^bold>1"
    and gh: "\x. x \ S \ T \ g x = h x"
shows "F g S = F h T"
proof-
  have "F g S = F g (S \ T)"
    by(rule mono_neutral_right)(auto intro: *)
  also have "\ = F h (S \ T)" using refl gh by(rule cong)
  also have "\ = F h T"
    by(rule mono_neutral_left)(auto intro: *)
  finally show ?thesis .
qed

lemma reindex_bij_betw: "bij_betw h S T \ F (\x. g (h x)) S = F g T"
  by (auto simp: bij_betw_def reindex)

lemma reindex_bij_witness:
  assumes witness:
    "\a. a \ S \ i (j a) = a"
    "\a. a \ S \ j a \ T"
    "\b. b \ T \ j (i b) = b"
    "\b. b \ T \ i b \ S"
  assumes eq:
    "\a. a \ S \ h (j a) = g a"
  shows "F g S = F h T"
proof -
  have "bij_betw j S T"
    using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
  moreover have "F g S = F (\x. h (j x)) S"
    by (intro cong) (auto simp: eq)
  ultimately show ?thesis
    by (simp add: reindex_bij_betw)
qed

lemma reindex_bij_betw_not_neutral:
  assumes fin: "finite S'" "finite T'"
  assumes bij: "bij_betw h (S - S') (T - T')"
  assumes nn:
    "\a. a \ S' \ g (h a) = z"
    "\b. b \ T' \ g b = z"
  shows "F (\x. g (h x)) S = F g T"
proof -
  have [simp]: "finite S \ finite T"
    using bij_betw_finite[OF bij] fin by auto
  show ?thesis
  proof (cases "finite S")
    case True
    with nn have "F (\x. g (h x)) S = F (\x. g (h x)) (S - S')"
      by (intro mono_neutral_cong_right) auto
    also have "\ = F g (T - T')"
      using bij by (rule reindex_bij_betw)
    also have "\ = F g T"
      using nn \<open>finite S\<close> by (intro mono_neutral_cong_left) auto
    finally show ?thesis .
  next
    case False
    then show ?thesis by simp
  qed
qed

lemma reindex_nontrivial:
  assumes "finite A"
    and nz: "\x y. x \ A \ y \ A \ x \ y \ h x = h y \ g (h x) = \<^bold>1"
  shows "F g (h ` A) = F (g \ h) A"
proof (subst reindex_bij_betw_not_neutral [symmetric])
  show "bij_betw h (A - {x \ A. (g \ h) x = \<^bold>1}) (h ` A - h ` {x \ A. (g \ h) x = \<^bold>1})"
    using nz by (auto intro!: inj_onI simp: bij_betw_def)
qed (use \<open>finite A\<close> in auto)

lemma reindex_bij_witness_not_neutral:
  assumes fin: "finite S'" "finite T'"
  assumes witness:
    "\a. a \ S - S' \ i (j a) = a"
    "\a. a \ S - S' \ j a \ T - T'"
    "\b. b \ T - T' \ j (i b) = b"
    "\b. b \ T - T' \ i b \ S - S'"
  assumes nn:
    "\a. a \ S' \ g a = z"
    "\b. b \ T' \ h b = z"
  assumes eq:
    "\a. a \ S \ h (j a) = g a"
  shows "F g S = F h T"
proof -
  have bij: "bij_betw j (S - (S' \ S)) (T - (T' \ T))"
    using witness by (intro bij_betw_byWitness[where f'=i]) auto
  have F_eq: "F g S = F (\x. h (j x)) S"
    by (intro cong) (auto simp: eq)
  show ?thesis
    unfolding F_eq using fin nn eq
    by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
qed

lemma delta_remove:
  assumes fS: "finite S"
  shows "F (\k. if k = a then b k else c k) S = (if a \ S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))"
proof -
  let ?f = "(\k. if k = a then b k else c k)"
  show ?thesis
  proof (cases "a \ S")
    case False
    then have "\k\S. ?f k = c k" by simp
    with False show ?thesis by simp
  next
    case True
    let ?A = "S - {a}"
    let ?B = "{a}"
    from True have eq: "S = ?A \ ?B" by blast
    have dj: "?A \ ?B = {}" by simp
    from fS have fAB: "finite ?A" "finite ?B" by auto
    have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
    with True show ?thesis
      using comm_monoid_set.remove comm_monoid_set_axioms fS by fastforce
  qed
qed

lemma delta [simp]:
  assumes fS: "finite S"
  shows "F (\k. if k = a then b k else \<^bold>1) S = (if a \ S then b a else \<^bold>1)"
  by (simp add: delta_remove [OF assms])

lemma delta' [simp]:
  assumes fin: "finite S"
  shows "F (\k. if a = k then b k else \<^bold>1) S = (if a \ S then b a else \<^bold>1)"
  using delta [OF fin, of a b, symmetric] by (auto intro: cong)

lemma If_cases:
  fixes P :: "'b \ bool" and g h :: "'b \ 'a"
  assumes fin: "finite A"
  shows "F (\x. if P x then h x else g x) A = F h (A \ {x. P x}) \<^bold>* F g (A \ - {x. P x})"
proof -
  have a: "A = A \ {x. P x} \ A \ -{x. P x}" "(A \ {x. P x}) \ (A \ -{x. P x}) = {}"
    by blast+
  from fin have f: "finite (A \ {x. P x})" "finite (A \ -{x. P x})" by auto
  let ?g = "\x. if P x then h x else g x"
  from union_disjoint [OF f a(2), of ?g] a(1) show ?thesis
    by (subst (1 2) cong) simp_all
qed

lemma cartesian_product: "F (\x. F (g x) B) A = F (case_prod g) (A \ B)"
proof (cases "A = {} \ B = {}")
  case True
  then show ?thesis
    by auto
next
  case False
  then have "A \ {}" "B \ {}" by auto
  show ?thesis
  proof (cases "finite A \ finite B")
    case True
    then show ?thesis
      by (simp add: Sigma)
  next
    case False
    then consider "infinite A" | "infinite B" by auto
    then have "infinite (A \ B)"
      by cases (use \<open>A \<noteq> {}\<close> \<open>B \<noteq> {}\<close> in \<open>auto dest: finite_cartesian_productD1 finite_cartesian_productD2\<close>)
    then show ?thesis
      using False by auto
  qed
qed

lemma cartesian_product':
  "F g (A \ B) = F (\x. F (\y. g (x,y)) B) A"
  unfolding cartesian_product by simp

lemma inter_restrict:
  assumes "finite A"
  shows "F g (A \ B) = F (\x. if x \ B then g x else \<^bold>1) A"
proof -
  let ?g = "\x. if x \ A \ B then g x else \<^bold>1"
  have "\i\A - A \ B. (if i \ A \ B then g i else \<^bold>1) = \<^bold>1" by simp
  moreover have "A \ B \ A" by blast
  ultimately have "F ?g (A \ B) = F ?g A"
    using \<open>finite A\<close> by (intro mono_neutral_left) auto
  then show ?thesis by simp
qed

lemma inter_filter:
  "finite A \ F g {x \ A. P x} = F (\x. if P x then g x else \<^bold>1) A"
  by (simp add: inter_restrict [symmetric, of A "{x. P x}" g, simplified mem_Collect_eq] Int_def)

lemma Union_comp:
  assumes "\A \ B. finite A"
    and "\A1 A2 x. A1 \ B \ A2 \ B \ A1 \ A2 \ x \ A1 \ x \ A2 \ g x = \<^bold>1"
  shows "F g (\B) = (F \ F) g B"
  using assms
proof (induct B rule: infinite_finite_induct)
  case (infinite A)
  then have "\ finite (\A)" by (blast dest: finite_UnionD)
  with infinite show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert A B)
  then have "finite A" "finite B" "finite (\B)" "A \ B"
    and "\x\A \ \B. g x = \<^bold>1"
    and H: "F g (\B) = (F \ F) g B" by auto
  then have "F g (A \ \B) = F g A \<^bold>* F g (\B)"
    by (simp add: union_inter_neutral)
  with \<open>finite B\<close> \<open>A \<notin> B\<close> show ?case
    by (simp add: H)
qed

lemma swap: "F (\i. F (g i) B) A = F (\j. F (\i. g i j) A) B"
  unfolding cartesian_product
  by (rule reindex_bij_witness [where i = "\(i, j). (j, i)" and j = "\(i, j). (j, i)"]) auto

lemma swap_restrict:
  "finite A \ finite B \
    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"
  by (simp add: inter_filter) (rule swap)

lemma image_gen:
  assumes fin: "finite S"
  shows "F h S = F (\y. F h {x. x \ S \ g x = y}) (g ` S)"
proof -
  have "{y. y\ g`S \ g x = y} = {g x}" if "x \ S" for x
    using that by auto
  then have "F h S = F (\x. F (\y. h x) {y. y\ g`S \ g x = y}) S"
    by simp
  also have "\ = F (\y. F h {x. x \ S \ g x = y}) (g ` S)"
    by (rule swap_restrict [OF fin finite_imageI [OF fin]])
  finally show ?thesis .
qed

lemma group:
  assumes fS: "finite S" and fT: "finite T" and fST: "g ` S \ T"
  shows "F (\y. F h {x. x \ S \ g x = y}) T = F h S"
  unfolding image_gen[OF fS, of h g]
  by (auto intro: neutral mono_neutral_right[OF fT fST])

lemma Plus:
  fixes A :: "'b set" and B :: "'c set"
  assumes fin: "finite A" "finite B"
  shows "F g (A <+> B) = F (g \ Inl) A \<^bold>* F (g \ Inr) B"
proof -
  have "A <+> B = Inl ` A \ Inr ` B" by auto
  moreover from fin have "finite (Inl ` A)" "finite (Inr ` B)" by auto
  moreover have "Inl ` A \ Inr ` B = {}" by auto
  moreover have "inj_on Inl A" "inj_on Inr B" by (auto intro: inj_onI)
  ultimately show ?thesis
    using fin by (simp add: union_disjoint reindex)
qed

lemma same_carrier:
  assumes "finite C"
  assumes subset: "A \ C" "B \ C"
  assumes trivial: "\a. a \ C - A \ g a = \<^bold>1" "\b. b \ C - B \ h b = \<^bold>1"
  shows "F g A = F h B \ F g C = F h C"
proof -
  have "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)"
    using \<open>finite C\<close> subset by (auto elim: finite_subset)
  from subset have [simp]: "A - (C - A) = A" by auto
  from subset have [simp]: "B - (C - B) = B" by auto
  from subset have "C = A \ (C - A)" by auto
  then have "F g C = F g (A \ (C - A))" by simp
  also have "\ = F g (A - (C - A)) \<^bold>* F g (C - A - A) \<^bold>* F g (A \ (C - A))"
    using \<open>finite A\<close> \<open>finite (C - A)\<close> by (simp only: union_diff2)
  finally have *: "F g C = F g A" using trivial by simp
  from subset have "C = B \ (C - B)" by auto
  then have "F h C = F h (B \ (C - B))" by simp
  also have "\ = F h (B - (C - B)) \<^bold>* F h (C - B - B) \<^bold>* F h (B \ (C - B))"
    using \<open>finite B\<close> \<open>finite (C - B)\<close> by (simp only: union_diff2)
  finally have "F h C = F h B"
    using trivial by simp
  with * show ?thesis by simp
qed

lemma same_carrierI:
  assumes "finite C"
  assumes subset: "A \ C" "B \ C"
  assumes trivial: "\a. a \ C - A \ g a = \<^bold>1" "\b. b \ C - B \ h b = \<^bold>1"
  assumes "F g C = F h C"
  shows "F g A = F h B"
  using assms same_carrier [of C A B] by simp

lemma eq_general:
  assumes B: "\y. y \ B \ \!x. x \ A \ h x = y" and A: "\x. x \ A \ h x \ B \ \(h x) = \ x"
  shows "F \ A = F \ B"
proof -
  have eq: "B = h ` A"
    by (auto dest: assms)
  have h: "inj_on h A"
    using assms by (blast intro: inj_onI)
  have "F \ A = F (\ \ h) A"
    using A by auto
  also have "\ = F \ B"
    by (simp add: eq reindex h)
  finally show ?thesis .
qed

lemma eq_general_inverses:
  assumes B: "\y. y \ B \ k y \ A \ h(k y) = y" and A: "\x. x \ A \ h x \ B \ k(h x) = x \ \(h x) = \ x"
  shows "F \ A = F \ B"
  by (rule eq_general [where h=h]) (force intro: dest: A B)+

subsubsection \<open>HOL Light variant: sum/product indexed by the non-neutral subset\<close>
text \<open>NB only a subset of the properties above are proved\<close>

definition G :: "['b \ 'a,'b set] \ 'a"
  where "G p I \ if finite {x \ I. p x \ \<^bold>1} then F p {x \ I. p x \ \<^bold>1} else \<^bold>1"

lemma finite_Collect_op:
  shows "\finite {i \ I. x i \ \<^bold>1}; finite {i \ I. y i \ \<^bold>1}\ \ finite {i \ I. x i \<^bold>* y i \ \<^bold>1}"
  apply (rule finite_subset [where B = "{i \ I. x i \ \<^bold>1} \ {i \ I. y i \ \<^bold>1}"])
  using left_neutral by force+

lemma empty' [simp]: "G p {} = \<^bold>1"
  by (auto simp: G_def)

lemma eq_sum [simp]: "finite I \ G p I = F p I"
  by (auto simp: G_def intro: mono_neutral_cong_left)

lemma insert' [simp]:
  assumes "finite {x \ I. p x \ \<^bold>1}"
  shows "G p (insert i I) = (if i \ I then G p I else p i \<^bold>* G p I)"
proof -
  have "{x. x = i \ p x \ \<^bold>1 \ x \ I \ p x \ \<^bold>1} = (if p i = \<^bold>1 then {x \ I. p x \ \<^bold>1} else insert i {x \ I. p x \ \<^bold>1})"
    by auto
  then show ?thesis
    using assms by (simp add: G_def conj_disj_distribR insert_absorb)
qed

lemma distrib_triv':
  assumes "finite I"
  shows "G (\i. g i \<^bold>* h i) I = G g I \<^bold>* G h I"
  by (simp add: assms local.distrib)

lemma non_neutral': "G g {x \ I. g x \ \<^bold>1} = G g I"
  by (simp add: G_def)

lemma distrib':
  assumes "finite {x \ I. g x \ \<^bold>1}" "finite {x \ I. h x \ \<^bold>1}"
  shows "G (\i. g i \<^bold>* h i) I = G g I \<^bold>* G h I"
proof -
  have "a \<^bold>* a \ a \ a \ \<^bold>1" for a
    by auto
  then have "G (\i. g i \<^bold>* h i) I = G (\i. g i \<^bold>* h i) ({i \ I. g i \ \<^bold>1} \ {i \ I. h i \ \<^bold>1})"
    using assms  by (force simp: G_def finite_Collect_op intro!: mono_neutral_cong)
  also have "\ = G g I \<^bold>* G h I"
  proof -
    have "F g ({i \ I. g i \ \<^bold>1} \ {i \ I. h i \ \<^bold>1}) = G g I"
         "F h ({i \ I. g i \ \<^bold>1} \ {i \ I. h i \ \<^bold>1}) = G h I"
      by (auto simp: G_def assms intro: mono_neutral_right)
    then show ?thesis
      using assms by (simp add: distrib)
  qed
  finally show ?thesis .
qed

lemma cong':
  assumes "A = B"
  assumes g_h: "\x. x \ B \ g x = h x"
  shows "G g A = G h B"
  using assms by (auto simp: G_def cong: conj_cong intro: cong)

lemma mono_neutral_cong_left':
  assumes "S \ T"
    and "\i. i \ T - S \ h i = \<^bold>1"
    and "\x. x \ S \ g x = h x"
  shows "G g S = G h T"
proof -
  have *: "{x \ S. g x \ \<^bold>1} = {x \ T. h x \ \<^bold>1}"
    using assms by (metis DiffI subset_eq)
  then have "finite {x \ S. g x \ \<^bold>1} = finite {x \ T. h x \ \<^bold>1}"
    by simp
  then show ?thesis
    using assms by (auto simp add: G_def * intro: cong)
qed

lemma mono_neutral_cong_right':
  "S \ T \ \i \ T - S. g i = \<^bold>1 \ (\x. x \ S \ g x = h x) \
    G g T = G h S"
  by (auto intro!: mono_neutral_cong_left' [symmetric])

lemma mono_neutral_left': "S \ T \ \i \ T - S. g i = \<^bold>1 \ G g S = G g T"
  by (blast intro: mono_neutral_cong_left')

lemma mono_neutral_right': "S \ T \ \i \ T - S. g i = \<^bold>1 \ G g T = G g S"
  by (blast intro!: mono_neutral_left' [symmetric])

end

subsection \<open>Generalized summation over a set\<close>

context comm_monoid_add
begin

sublocale sum: comm_monoid_set plus 0
  defines sum = sum.F and sum' = sum.G ..

abbreviation Sum (\<open>\<Sum>\<close>)
  where "\ \ sum (\x. x)"

end

text \<open>Now: lots of fancy syntax. First, \<^term>\<open>sum (\<lambda>x. e) A\<close> is written \<open>\<Sum>x\<in>A. e\<close>.\<close>

syntax (ASCII)
  "_sum" :: "pttrn \ 'a set \ 'b \ 'b::comm_monoid_add" (\(\indent=3 notation=\binder SUM\\SUM (_/:_)./ _)\ [0, 51, 10] 10)
syntax
  "_sum" :: "pttrn \ 'a set \ 'b \ 'b::comm_monoid_add" (\(\indent=2 notation=\binder \\\\(_/\_)./ _)\ [0, 51, 10] 10)

syntax_consts
  "_sum" \<rightleftharpoons> sum

translations \<comment> \<open>Beware of argument permutation!\<close>
  "\i\A. b" \ "CONST sum (\i. b) A"

text \<open>Instead of \<^term>\<open>\<Sum>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>

syntax (ASCII)
  "_qsum" :: "pttrn \ bool \ 'a \ 'a" (\(\indent=3 notation=\binder SUM Collect\\SUM _ |/ _./ _)\ [0, 0, 10] 10)
syntax
  "_qsum" :: "pttrn \ bool \ 'a \ 'a" (\(\indent=2 notation=\binder \ Collect\\\_ | (_)./ _)\ [0, 0, 10] 10)

syntax_consts
  "_qsum" == sum
translations
  "\x|P. t" => "CONST sum (\x. t) {x. P}"
print_translation \<open>
  [(\<^const_syntax>\<open>sum\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qsum\<close>))]
\<close>

subsubsection \<open>Properties in more restricted classes of structures\<close>

lemma sum_Un:
  "finite A \ finite B \ sum f (A \ B) = sum f A + sum f B - sum f (A \ B)"
  for f :: "'b \ 'a::ab_group_add"
  by (subst sum.union_inter [symmetric]) (auto simp add: algebra_simps)

lemma sum_Un2:
  assumes "finite (A \ B)"
  shows "sum f (A \ B) = sum f (A - B) + sum f (B - A) + sum f (A \ B)"
proof -
  have "A \ B = A - B \ (B - A) \ A \ B"
    by auto
  with assms show ?thesis
    by simp (subst sum.union_disjoint, auto)+
qed

(*Like sum.subset_diff but expressed perhaps more conveniently using subtraction*)
lemma sum_diff:
  fixes f :: "'b \ 'a::ab_group_add"
  assumes "finite A" "B \ A"
  shows "sum f (A - B) = sum f A - sum f B"
  using sum.subset_diff [of B A f] assms by simp

lemma sum_diff1:
  fixes f :: "'b \ 'a::ab_group_add"
  assumes "finite A"
  shows "sum f (A - {a}) = (if a \ A then sum f A - f a else sum f A)"
  using assms by (simp add: sum_diff)

lemma sum_diff1'_aux:
  fixes f :: "'a \ 'b::ab_group_add"
  assumes "finite F" "{i \ I. f i \ 0} \ F"
  shows "sum' f (I - {i}) = (if i \ I then sum' f I - f i else sum' f I)"
  using assms
proof induct
  case (insert x F)
  have 1: "finite {x \ I. f x \ 0} \ finite {x \ I. x \ i \ f x \ 0}"
    by (erule rev_finite_subset) auto
  have 2: "finite {x \ I. x \ i \ f x \ 0} \ finite {x \ I. f x \ 0}"
    apply (drule finite_insert [THEN iffD2])
    by (erule rev_finite_subset) auto
  have 3: "finite {i \ I. f i \ 0}"
    using finite_subset insert by blast
  show ?case
    using insert sum_diff1 [of "{i \ I. f i \ 0}" f i]
    by (auto simp: sum.G_def 1 2 3 set_diff_eq conj_ac)
qed (simp add: sum.G_def)

lemma sum_diff1':
  fixes f :: "'a \ 'b::ab_group_add"
  assumes "finite {i \ I. f i \ 0}"
  shows "sum' f (I - {i}) = (if i \ I then sum' f I - f i else sum' f I)"
  by (rule sum_diff1'_aux [OF assms order_refl])

lemma (in ordered_comm_monoid_add) sum_mono:
  "(\i. i\K \ f i \ g i) \ (\i\K. f i) \ (\i\K. g i)"
  by (induct K rule: infinite_finite_induct) (use add_mono in auto)

lemma (in ordered_cancel_comm_monoid_add) sum_strict_mono_strong:
  assumes "finite A" "a \ A" "f a < g a"
    and "\x. x \ A \ f x \ g x"
  shows "sum f A < sum g A"
proof -
  have "sum f A = f a + sum f (A-{a})"
    by (simp add: assms sum.remove)
  also have "\ \ f a + sum g (A-{a})"
    using assms by (meson DiffD1 add_left_mono sum_mono)
  also have "\ < g a + sum g (A-{a})"
    using assms add_less_le_mono by blast
  also have "\ = sum g A"
    using assms by (intro sum.remove [symmetric])
  finally show ?thesis .
qed

lemma (in strict_ordered_comm_monoid_add) sum_strict_mono:
  assumes "finite A" "A \ {}"
    and "\x. x \ A \ f x < g x"
  shows "sum f A < sum g A"
  using assms
proof (induct rule: finite_ne_induct)
  case singleton
  then show ?case by simp
next
  case insert
  then show ?case by (auto simp: add_strict_mono)
qed

lemma sum_strict_mono_ex1:
  fixes f g :: "'i \ 'a::ordered_cancel_comm_monoid_add"
  assumes "finite A"
    and "\x\A. f x \ g x"
    and "\a\A. f a < g a"
  shows "sum f A < sum g A"
proof-
  from assms(3) obtain a where a: "a \ A" "f a < g a" by blast
  have "sum f A = sum f ((A - {a}) \ {a})"
    by(simp add: insert_absorb[OF \<open>a \<in> A\<close>])
  also have "\ = sum f (A - {a}) + sum f {a}"
    using \<open>finite A\<close> by(subst sum.union_disjoint) auto
  also have "sum f (A - {a}) \ sum g (A - {a})"
    by (rule sum_mono) (simp add: assms(2))
  also from a have "sum f {a} < sum g {a}" by simp
  also have "sum g (A - {a}) + sum g {a} = sum g((A - {a}) \ {a})"
    using \<open>finite A\<close> by (subst sum.union_disjoint[symmetric]) auto
  also have "\ = sum g A" by (simp add: insert_absorb[OF \a \ A\])
  finally show ?thesis
    by (auto simp add: add_right_mono add_strict_left_mono)
qed

lemma sum_mono_inv:
  fixes f g :: "'i \ 'a :: ordered_cancel_comm_monoid_add"
  assumes eq: "sum f I = sum g I"
  assumes le: "\i. i \ I \ f i \ g i"
  assumes i: "i \ I"
  assumes I: "finite I"
  shows "f i = g i"
proof (rule ccontr)
  assume "\ ?thesis"
  with le[OF i] have "f i < g i" by simp
  with i have "\i\I. f i < g i" ..
  from sum_strict_mono_ex1[OF I _ this] le have "sum f I < sum g I"
    by blast
  with eq show False by simp
qed

lemma member_le_sum:
  fixes f :: "_ \ 'b::{semiring_1, ordered_comm_monoid_add}"
  assumes "i \ A"
    and le: "\x. x \ A - {i} \ 0 \ f x"
    and "finite A"
  shows "f i \ sum f A"
proof -
  have "f i \ sum f (A \ {i})"
    by (simp add: assms)
  also have "... = (\x\A. if x \ {i} then f x else 0)"
    using assms sum.inter_restrict by blast
  also have "... \ sum f A"
    apply (rule sum_mono)
    apply (auto simp: le)
    done
  finally show ?thesis .
qed

lemma sum_negf: "(\x\A. - f x) = - (\x\A. f x)"
  for f :: "'b \ 'a::ab_group_add"
  by (induct A rule: infinite_finite_induct) auto

lemma sum_subtractf: "(\x\A. f x - g x) = (\x\A. f x) - (\x\A. g x)"
  for f g :: "'b \'a::ab_group_add"
  using sum.distrib [of f "- g" A] by (simp add: sum_negf)

lemma sum_subtractf_nat:
  "(\x. x \ A \ g x \ f x) \ (\x\A. f x - g x) = (\x\A. f x) - (\x\A. g x)"
  for f g :: "'a \ nat"
  by (induct A rule: infinite_finite_induct) (auto simp: sum_mono)

context ordered_comm_monoid_add
begin

lemma sum_nonneg: "(\x. x \ A \ 0 \ f x) \ 0 \ sum f A"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  then have "0 + 0 \ f x + sum f F" by (blast intro: add_mono)
  with insert show ?case by simp
qed

lemma sum_nonpos: "(\x. x \ A \ f x \ 0) \ sum f A \ 0"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  then have "f x + sum f F \ 0 + 0" by (blast intro: add_mono)
  with insert show ?case by simp
qed

lemma sum_nonneg_eq_0_iff:
  "finite A \ (\x. x \ A \ 0 \ f x) \ sum f A = 0 \ (\x\A. f x = 0)"
  by (induct set: finite) (simp_all add: add_nonneg_eq_0_iff sum_nonneg)

lemma sum_nonneg_0:
  "finite s \ (\i. i \ s \ f i \ 0) \ (\ i \ s. f i) = 0 \ i \ s \ f i = 0"
  by (simp add: sum_nonneg_eq_0_iff)

lemma sum_nonneg_leq_bound:
  assumes "finite s" "\i. i \ s \ f i \ 0" "(\i \ s. f i) = B" "i \ s"
  shows "f i \ B"
proof -
  from assms have "f i \ f i + (\i \ s - {i}. f i)"
    by (intro add_increasing2 sum_nonneg) auto
  also have "\ = B"
    using sum.remove[of s i f] assms by simp
  finally show ?thesis by auto
qed

lemma sum_mono2:
  assumes fin: "finite B"
    and sub: "A \ B"
    and nn: "\b. b \ B-A \ 0 \ f b"
  shows "sum f A \ sum f B"
proof -
  have "sum f A \ sum f A + sum f (B-A)"
    by (auto intro: add_increasing2 [OF sum_nonneg] nn)
  also from fin finite_subset[OF sub fin] have "\ = sum f (A \ (B-A))"
    by (simp add: sum.union_disjoint del: Un_Diff_cancel)
  also from sub have "A \ (B-A) = B" by blast
  finally show ?thesis .
qed

lemma sum_le_included:
  assumes "finite s" "finite t"
  and "\y\t. 0 \ g y" "(\x\s. \y\t. i y = x \ f x \ g y)"
  shows "sum f s \ sum g t"
proof -
  have "sum f s \ sum (\y. sum g {x. x\t \ i x = y}) s"
  proof (rule sum_mono)
    fix y
    assume "y \ s"
    with assms obtain z where z: "z \ t" "y = i z" "f y \ g z" by auto
    with assms show "f y \ sum g {x \ t. i x = y}" (is "?A y \ ?B y")
      using order_trans[of "?A (i z)" "sum g {z}" "?B (i z)", intro]
      by (auto intro!: sum_mono2)
  qed
  also have "\ \ sum (\y. sum g {x. x\t \ i x = y}) (i ` t)"
    using assms(2-4) by (auto intro!: sum_mono2 sum_nonneg)
  also have "\ \ sum g t"
    using assms by (auto simp: sum.image_gen[symmetric])
  finally show ?thesis .
qed

end

lemma (in canonically_ordered_monoid_add) sum_eq_0_iff [simp]:
  "finite F \ (sum f F = 0) = (\a\F. f a = 0)"
  by (intro ballI sum_nonneg_eq_0_iff zero_le)

context semiring_0
begin

lemma sum_distrib_left: "r * sum f A = (\n\A. r * f n)"
  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)

lemma sum_distrib_right: "sum f A * r = (\n\A. f n * r)"
  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)

end

lemma sum_divide_distrib: "sum f A / r = (\n\A. f n / r)"
  for r :: "'a::field"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case insert
  then show ?case by (simp add: add_divide_distrib)
qed

lemma sum_abs[iff]: "\sum f A\ \ sum (\i. \f i\) A"
  for f :: "'a \ 'b::ordered_ab_group_add_abs"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case insert
  then show ?case by (auto intro: abs_triangle_ineq order_trans)
qed

lemma sum_abs_ge_zero[iff]: "0 \ sum (\i. \f i\) A"
  for f :: "'a \ 'b::ordered_ab_group_add_abs"
  by (simp add: sum_nonneg)

lemma abs_sum_abs[simp]: "\\a\A. \f a\\ = (\a\A. \f a\)"
  for f :: "'a \ 'b::ordered_ab_group_add_abs"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert a A)
  then have "\\a\insert a A. \f a\\ = \\f a\ + (\a\A. \f a\)\" by simp
  also from insert have "\ = \\f a\ + \\a\A. \f a\\\" by simp
  also have "\ = \f a\ + \\a\A. \f a\\" by (simp del: abs_of_nonneg)
  also from insert have "\ = (\a\insert a A. \f a\)" by simp
  finally show ?case .
qed

lemma sum_product:
  fixes f :: "'a \ 'b::semiring_0"
  shows "sum f A * sum g B = (\i\A. \j\B. f i * g j)"
  by (simp add: sum_distrib_left sum_distrib_right) (rule sum.swap)

lemma sum_mult_sum_if_inj:
  fixes f :: "'a \ 'b::semiring_0"
  shows "inj_on (\(a, b). f a * g b) (A \ B) \
    sum f A * sum g B = sum id {f a * g b |a b. a \<in> A \<and> b \<in> B}"
  by(auto simp: sum_product sum.cartesian_product intro!: sum.reindex_cong[symmetric])

lemma sum_SucD: "sum f A = Suc n \ \a\A. 0 < f a"
  by (induct A rule: infinite_finite_induct) auto

lemma sum_eq_Suc0_iff:
  "finite A \ sum f A = Suc 0 \ (\a\A. f a = Suc 0 \ (\b\A. a \ b \ f b = 0))"
  by (induct A rule: finite_induct) (auto simp add: add_is_1)

lemmas sum_eq_1_iff = sum_eq_Suc0_iff[simplified One_nat_def[symmetric]]

lemma sum_Un_nat:
  "finite A \ finite B \ sum f (A \ B) = sum f A + sum f B - sum f (A \ B)"
  for f :: "'a \ nat"
  \<comment> \<open>For the natural numbers, we have subtraction.\<close>
  by (subst sum.union_inter [symmetric]) (auto simp: algebra_simps)

lemma sum_diff1_nat: "sum f (A - {a}) = (if a \ A then sum f A - f a else sum f A)"
  for f :: "'a \ nat"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case
  proof (cases "a \ F")
    case True
    then have "\B. F = insert a B \ a \ B"
      by (auto simp: mk_disjoint_insert)
    then show ?thesis  using insert
      by (auto simp: insert_Diff_if)
  qed (auto)
qed

lemma sum_diff_nat:
  fixes f :: "'a \ nat"
  assumes "finite B" and "B \ A"
  shows "sum f (A - B) = sum f A - sum f B"
  using assms
proof induct
  case empty
  then show ?case by simp
next
  case (insert x F)
  note IH = \<open>F \<subseteq> A \<Longrightarrow> sum f (A - F) = sum f A - sum f F\<close>
  from \<open>x \<notin> F\<close> \<open>insert x F \<subseteq> A\<close> have "x \<in> A - F" by simp
  then have A: "sum f ((A - F) - {x}) = sum f (A - F) - f x"
    by (simp add: sum_diff1_nat)
  from \<open>insert x F \<subseteq> A\<close> have "F \<subseteq> A" by simp
  with IH have "sum f (A - F) = sum f A - sum f F" by simp
  with A have B: "sum f ((A - F) - {x}) = sum f A - sum f F - f x"
    by simp
  from \<open>x \<notin> F\<close> have "A - insert x F = (A - F) - {x}" by auto
  with B have C: "sum f (A - insert x F) = sum f A - sum f F - f x"
    by simp
  from \<open>finite F\<close> \<open>x \<notin> F\<close> have "sum f (insert x F) = sum f F + f x"
    by simp
  with C have "sum f (A - insert x F) = sum f A - sum f (insert x F)"
    by simp
  then show ?case by simp
qed

lemma sum_comp_morphism:
  "h 0 = 0 \ (\x y. h (x + y) = h x + h y) \ sum (h \ g) A = h (sum g A)"
  by (induct A rule: infinite_finite_induct) simp_all

lemma (in comm_semiring_1) dvd_sum: "(\a. a \ A \ d dvd f a) \ d dvd sum f A"
  by (induct A rule: infinite_finite_induct) simp_all

lemma (in ordered_comm_monoid_add) sum_pos:
  "finite I \ I \ {} \ (\i. i \ I \ 0 < f i) \ 0 < sum f I"
  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)

lemma (in ordered_comm_monoid_add) sum_pos2:
  assumes I: "finite I" "i \ I" "0 < f i" "\i. i \ I \ 0 \ f i"
  shows "0 < sum f I"
proof -
  have "0 < f i + sum f (I - {i})"
    using assms by (intro add_pos_nonneg sum_nonneg) auto
  also have "\ = sum f I"
    using assms by (simp add: sum.remove)
  finally show ?thesis .
qed

lemma sum_strict_mono2:
  fixes f :: "'a \ 'b::ordered_cancel_comm_monoid_add"
  assumes "finite B" "A \ B" "b \ B-A" "f b > 0" and "\x. x \ B \ f x \ 0"
  shows "sum f A < sum f B"
proof -
  have "B - A \ {}"
    using assms(3) by blast
  have "sum f (B-A) > 0"
    by (rule sum_pos2) (use assms in auto)
  moreover have "sum f B = sum f (B-A) + sum f A"
    by (rule sum.subset_diff) (use assms in auto)
  ultimately show ?thesis
    using add_strict_increasing by auto
qed

lemma sum_cong_Suc:
  assumes "0 \ A" "\x. Suc x \ A \ f (Suc x) = g (Suc x)"
  shows "sum f A = sum g A"
proof (rule sum.cong)
  fix x
  assume "x \ A"
  with assms(1) show "f x = g x"
    by (cases x) (auto intro!: assms(2))
qed simp_all

subsubsection \<open>Cardinality as special case of \<^const>\<open>sum\<close>\<close>

lemma card_eq_sum: "card A = sum (\x. 1) A"
proof -
  have "plus \ (\_. Suc 0) = (\_. Suc)"
    by (simp add: fun_eq_iff)
  then have "Finite_Set.fold (plus \ (\_. Suc 0)) = Finite_Set.fold (\_. Suc)"
    by (rule arg_cong)
  then have "Finite_Set.fold (plus \ (\_. Suc 0)) 0 A = Finite_Set.fold (\_. Suc) 0 A"
    by (blast intro: fun_cong)
  then show ?thesis
    by (simp add: card.eq_fold sum.eq_fold)
qed

context semiring_1
begin

lemma sum_constant [simp]:
  "(\x \ A. y) = of_nat (card A) * y"
  by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)

context
  fixes A
  assumes \<open>finite A\<close>
begin

lemma sum_of_bool_eq [simp]:
  \<open>(\<Sum>x \<in> A. of_bool (P x)) = of_nat (card (A \<inter> {x. P x}))\<close> if \<open>finite A\<close>
  using \<open>finite A\<close> by induction simp_all

lemma sum_mult_of_bool_eq [simp]:
  \<open>(\<Sum>x \<in> A. f x * of_bool (P x)) = (\<Sum>x \<in> (A \<inter> {x. P x}). f x)\<close>
  by (rule sum.mono_neutral_cong) (use \<open>finite A\<close> in auto)

lemma sum_of_bool_mult_eq [simp]:
  \<open>(\<Sum>x \<in> A. of_bool (P x) * f x) = (\<Sum>x \<in> (A \<inter> {x. P x}). f x)\<close>
  by (rule sum.mono_neutral_cong) (use \<open>finite A\<close> in auto)

end

end

lemma sum_Suc: "sum (\x. Suc(f x)) A = sum f A + card A"
  using sum.distrib[of f "\_. 1" A] by simp

lemma sum_bounded_above:
  fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}"
  assumes le: "\i. i\A \ f i \ K"
  shows "sum f A \ of_nat (card A) * K"
proof (cases "finite A")
  case True
  then show ?thesis
    using le sum_mono[where K=A and g = "\x. K"] by simp
next
  case False
  then show ?thesis by simp
qed

lemma sum_bounded_above_divide:
  fixes K :: "'a::linordered_field"
  assumes le: "\i. i\A \ f i \ K / of_nat (card A)" and fin: "finite A" "A \ {}"
  shows "sum f A \ K"
  using sum_bounded_above [of A f "K / of_nat (card A)", OF le] fin by simp

lemma sum_bounded_above_strict:
  fixes K :: "'a::{ordered_cancel_comm_monoid_add,semiring_1}"
  assumes "\i. i\A \ f i < K" "card A > 0"
  shows "sum f A < of_nat (card A) * K"
  using assms sum_strict_mono[where A=A and g = "\x. K"]
  by (simp add: card_gt_0_iff)

lemma sum_bounded_below:
  fixes K :: "'a::{semiring_1,ordered_comm_monoid_add}"
  assumes le: "\i. i\A \ K \ f i"
  shows "of_nat (card A) * K \ sum f A"
proof (cases "finite A")
  case True
  then show ?thesis
    using le sum_mono[where K=A and f = "\x. K"] by simp
next
  case False
  then show ?thesis by simp
qed

lemma convex_sum_bound_le:
  fixes x :: "'a \ 'b::linordered_idom"
  assumes 0: "\i. i \ I \ 0 \ x i" and 1: "sum x I = 1"
      and \<delta>: "\<And>i. i \<in> I \<Longrightarrow> \<bar>a i - b\<bar> \<le> \<delta>"
    shows "\(\i\I. a i * x i) - b\ \ \"
proof -
  have [simp]: "(\i\I. c * x i) = c" for c
    by (simp flip: sum_distrib_left 1)
  then have "\(\i\I. a i * x i) - b\ = \\i\I. (a i - b) * x i\"
    by (simp add: sum_subtractf left_diff_distrib)
  also have "\ \ (\i\I. \(a i - b) * x i\)"
    using abs_abs abs_of_nonneg by blast
  also have "\ \ (\i\I. \(a i - b)\ * x i)"
    by (simp add: abs_mult 0)
  also have "\ \ (\i\I. \ * x i)"
    by (rule sum_mono) (use \<delta> "0" mult_right_mono in blast)
  also have "\ = \"
    by simp
  finally show ?thesis .
qed

lemma card_UN_disjoint:
  assumes "finite I" and "\i\I. finite (A i)"
    and "\i\I. \j\I. i \ j \ A i \ A j = {}"
  shows "card (\(A ` I)) = (\i\I. card(A i))"
proof -
  have "(\i\I. card (A i)) = (\i\I. \x\A i. 1)"
    by simp
  with assms show ?thesis
    by (simp add: card_eq_sum sum.UNION_disjoint del: sum_constant)
qed

lemma card_Union_disjoint:
  assumes "pairwise disjnt C" and fin: "\A. A \ C \ finite A"
  shows "card (\C) = sum card C"
proof (cases "finite C")
  case True
  then show ?thesis
    using card_UN_disjoint [OF True, of "\x. x"] assms
    by (simp add: disjnt_def fin pairwise_def)
next
  case False
  then show ?thesis
    using assms card_eq_0_iff finite_UnionD by fastforce
qed

lemma card_Union_le_sum_card_weak:
  fixes U :: "'a set set"
  assumes "\u \ U. finite u"
  shows "card (\U) \ sum card U"
proof (cases "finite U")
  case False
  then show "card (\U) \ sum card U"
    using card_eq_0_iff finite_UnionD by auto
next
  case True
  then show "card (\U) \ sum card U"
  proof (induct U rule: finite_induct)
    case empty
    then show ?case by auto
  next
    case (insert x F)
    then have "card(\(insert x F)) \ card(x) + card (\F)" using card_Un_le by auto
    also have "... \ card(x) + sum card F" using insert.hyps by auto
    also have "... = sum card (insert x F)" using sum.insert_if and insert.hyps by auto
    finally show ?case .
  qed
qed

lemma card_Union_le_sum_card:
  fixes U :: "'a set set"
  shows "card (\U) \ sum card U"
  by (metis Union_upper card.infinite card_Union_le_sum_card_weak finite_subset zero_le)

lemma card_UN_le:
  assumes "finite I"
  shows "card(\i\I. A i) \ (\i\I. card(A i))"
  using assms
proof induction
  case (insert i I)
  then show ?case
    using card_Un_le nat_add_left_cancel_le by (force intro: order_trans)
qed auto

lemma card_quotient_disjoint:
  assumes "finite A" "inj_on (\x. {x} // r) A"
  shows "card (A//r) = card A"
proof -
  have "\i\A. \j\A. i \ j \ r `` {j} \ r `` {i}"
    using assms by (fastforce simp add: quotient_def inj_on_def)
  with assms show ?thesis
    by (simp add: quotient_def card_UN_disjoint)
qed

lemma sum_multicount_gen:
  assumes "finite s" "finite t" "\j\t. (card {i\s. R i j} = k j)"
  shows "sum (\i. (card {j\t. R i j})) s = sum k t"
    (is "?l = ?r")
proof-
  have "?l = sum (\i. sum (\x.1) {j\t. R i j}) s"
    by auto
  also have "\ = ?r"
    unfolding sum.swap_restrict [OF assms(1-2)]
    using assms(3) by auto
  finally show ?thesis .
qed

lemma sum_multicount:
  assumes "finite S" "finite T" "\j\T. (card {i\S. R i j} = k)"
  shows "sum (\i. card {j\T. R i j}) S = k * card T" (is "?l = ?r")
proof-
  have "?l = sum (\i. k) T"
    by (rule sum_multicount_gen) (auto simp: assms)
  also have "\ = ?r" by (simp add: mult.commute)
  finally show ?thesis by auto
qed

lemma sum_card_image:
  assumes "finite A"
  assumes "pairwise (\s t. disjnt (f s) (f t)) A"
  shows "sum card (f ` A) = sum (\a. card (f a)) A"
using assms
proof (induct A)
  case (insert a A)
  show ?case
  proof cases
    assume "f a = {}"
    with insert show ?case
      by (subst sum.mono_neutral_right[where S="f ` A"]) (auto simp: pairwise_insert)
  next
    assume "f a \ {}"
    then have "sum card (insert (f a) (f ` A)) = card (f a) + sum card (f ` A)"
      using insert
      by (subst sum.insert) (auto simp: pairwise_insert)
    with insert show ?case by (simp add: pairwise_insert)
  qed
qed simp

text \<open>By Jakub Kądziołka:\<close>

lemma sum_fun_comp:
  assumes "finite S" "finite R" "g ` S \ R"
  shows "(\x \ S. f (g x)) = (\y \ R. of_nat (card {x \ S. g x = y}) * f y)"
proof -
  let ?r = "relation_of (\p q. g p = g q) S"
  have eqv: "equiv S ?r"
    unfolding relation_of_def by (auto intro: comp_equivI)
  have finite: "C \ S//?r \ finite C" for C
    by (fact finite_equiv_class[OF `finite S` equiv_type[OF `equiv S ?r`]])
  have disjoint: "A \ S//?r \ B \ S//?r \ A \ B \ A \ B = {}" for A B
    using eqv quotient_disj by blast

  let ?cls = "\y. {x \ S. y = g x}"
  have quot_as_img: "S//?r = ?cls ` g ` S"
    by (auto simp add: relation_of_def quotient_def)
  have cls_inj: "inj_on ?cls (g ` S)"
    by (auto intro: inj_onI)

  have rest_0: "(\y \ R - g ` S. of_nat (card (?cls y)) * f y) = 0"
  proof -
    have "of_nat (card (?cls y)) * f y = 0" if asm: "y \ R - g ` S" for y
    proof -
      from asm have *: "?cls y = {}" by auto
      show ?thesis unfolding * by simp
    qed
    thus ?thesis by simp
  qed

  have "(\x \ S. f (g x)) = (\C \ S//?r. \x \ C. f (g x))"
    using eqv finite disjoint
    by (simp flip: sum.Union_disjoint[simplified] add: Union_quotient)
  also have "... = (\y \ g ` S. \x \ ?cls y. f (g x))"
    unfolding quot_as_img by (simp add: sum.reindex[OF cls_inj])
  also have "... = (\y \ g ` S. \x \ ?cls y. f y)"
    by auto
  also have "... = (\y \ g ` S. of_nat (card (?cls y)) * f y)"
    by (simp flip: sum_constant)
  also have "... = (\y \ R. of_nat (card (?cls y)) * f y)"
    using rest_0 by (simp add: sum.subset_diff[OF \<open>g ` S \<subseteq> R\<close> \<open>finite R\<close>])
  finally show ?thesis
    by (simp add: eq_commute)
qed

subsubsection \<open>Cardinality of products\<close>

lemma card_SigmaI [simp]:
  "finite A \ \a\A. finite (B a) \ card (SIGMA x: A. B x) = (\a\A. card (B a))"
  by (simp add: card_eq_sum sum.Sigma del: sum_constant)

(*
lemma SigmaI_insert: "y \<notin> A ==>
  (SIGMA x:(insert y A). B x) = (({y} \<times> (B y)) \<union> (SIGMA x: A. B x))"
  by auto
*)

lemma card_cartesian_product: "card (A \ B) = card A * card B"
  by (cases "finite A \ finite B")
    (auto simp add: card_eq_0_iff dest: finite_cartesian_productD1 finite_cartesian_productD2)

lemma card_cartesian_product_singleton:  "card ({x} \ A) = card A"
  by (simp add: card_cartesian_product)

subsection \<open>Generalized product over a set\<close>

context comm_monoid_mult
begin

sublocale prod: comm_monoid_set times 1
  defines prod = prod.F and prod' = prod.G ..

abbreviation Prod (\<open>\<Prod>\<close>)
  where "\ \ prod (\x. x)"

end

syntax (ASCII)
  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  (\<open>(\<open>indent=4 notation=\<open>binder PROD\<close>\<close>PROD (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
  "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  (\<open>(\<open>indent=2 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)

syntax_consts
  "_prod" == prod

translations \<comment> \<open>Beware of argument permutation!\<close>
  "\i\A. b" == "CONST prod (\i. b) A"

text \<open>Instead of \<^term>\<open>\<Prod>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>

syntax (ASCII)
  "_qprod" :: "pttrn \ bool \ 'a \ 'a" (\(\indent=4 notation=\binder PROD Collect\\PROD _ |/ _./ _)\ [0, 0, 10] 10)
syntax
  "_qprod" :: "pttrn \ bool \ 'a \ 'a" (\(\indent=2 notation=\binder \ Collect\\\_ | (_)./ _)\ [0, 0, 10] 10)

syntax_consts
  "_qprod" == prod
translations
  "\x|P. t" => "CONST prod (\x. t) {x. P}"
print_translation \<open>
  [(\<^const_syntax>\<open>prod\<close>, K (Collect_binder_tr' \<^syntax_const>\<open>_qprod\<close>))]
\<close>

context comm_monoid_mult
begin

lemma prod_dvd_prod: "(\a. a \ A \ f a dvd g a) \ prod f A dvd prod g A"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by (auto intro: dvdI)
next
  case empty
  then show ?case by (auto intro: dvdI)
next
  case (insert a A)
  then have "f a dvd g a" and "prod f A dvd prod g A"
    by simp_all
  then obtain r s where "g a = f a * r" and "prod g A = prod f A * s"
    by (auto elim!: dvdE)
  then have "g a * prod g A = f a * prod f A * (r * s)"
    by (simp add: ac_simps)
  with insert.hyps show ?case
    by (auto intro: dvdI)
qed

lemma prod_dvd_prod_subset: "finite B \ A \ B \ prod f A dvd prod f B"
  by (auto simp add: prod.subset_diff ac_simps intro: dvdI)

end

subsubsection \<open>Properties in more restricted classes of structures\<close>

context linordered_nonzero_semiring
begin

lemma prod_ge_1: "(\x. x \ A \ 1 \ f x) \ 1 \ prod f A"
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  have "1 * 1 \ f x * prod f F"
    by (rule mult_mono') (use insert in auto)
  with insert show ?case by simp
qed

lemma prod_le_1:
  fixes f :: "'b \ 'a"
  assumes "\x. x \ A \ 0 \ f x \ f x \ 1"
  shows "prod f A \ 1"
    using assms
proof (induct A rule: infinite_finite_induct)
  case infinite
  then show ?case by simp
next
  case empty
  then show ?case by simp
next
  case (insert x F)
  then show ?case by (force simp: mult.commute intro: dest: mult_le_one)
qed

end

context comm_semiring_1
begin

lemma dvd_prod_eqI [intro]:
  assumes "finite A" and "a \ A" and "b = f a"
  shows "b dvd prod f A"
proof -
  from \<open>finite A\<close> have "prod f (insert a (A - {a})) = f a * prod f (A - {a})"
    by (intro prod.insert) auto
  also from \<open>a \<in> A\<close> have "insert a (A - {a}) = A"
    by blast
  finally have "prod f A = f a * prod f (A - {a})" .
  with \<open>b = f a\<close> show ?thesis
    by simp
qed

lemma dvd_prodI [intro]: "finite A \ a \ A \ f a dvd prod f A"
  by auto

lemma prod_zero:
  assumes "finite A" and "\a\A. f a = 0"
  shows "prod f A = 0"
  using assms
proof (induct A)
  case empty
  then show ?case by simp
next
  case (insert a A)
  then have "f a = 0 \ (\a\A. f a = 0)" by simp
  then have "f a * prod f A = 0" by (rule disjE) (simp_all add: insert)
  with insert show ?case by simp
qed

lemma prod_dvd_prod_subset2:
  assumes "finite B" and "A \ B" and "\a. a \ A \ f a dvd g a"
  shows "prod f A dvd prod g B"
proof -
  from assms have "prod f A dvd prod g A"
    by (auto intro: prod_dvd_prod)
  moreover from assms have "prod g A dvd prod g B"
    by (auto intro: prod_dvd_prod_subset)
  ultimately show ?thesis by (rule dvd_trans)
qed

end

lemma (in semidom) prod_zero_iff [simp]:
  fixes f :: "'b \ 'a"
  assumes "finite A"
  shows "prod f A = 0 \ (\a\A. f a = 0)"
  using assms by (induct A) (auto simp: no_zero_divisors)

lemma (in semidom_divide) prod_diff1:
  assumes "finite A" and "f a \ 0"
  shows "prod f (A - {a}) = (if a \ A then prod f A div f a else prod f A)"
proof (cases "a \ A")
  case True
  then show ?thesis by simp
next
  case False
  with assms show ?thesis
  proof induct
    case empty
    then show ?case by simp
  next
    case (insert b B)
    then show ?case
    proof (cases "a = b")
      case True
      with insert show ?thesis by simp
    next
      case False
      with insert have "a \ B" by simp
      define C where "C = B - {a}"
      with \<open>finite B\<close> \<open>a \<in> B\<close> have "B = insert a C" "finite C" "a \<notin> C"
        by auto
      with insert show ?thesis
        by (auto simp add: insert_commute ac_simps)
    qed
  qed
qed

lemma prod_uminus: "(\x\A. -f x :: 'a :: comm_ring_1) = (-1) ^ card A * (\x\A. f x)"
  by (induction A rule: infinite_finite_induct) (auto simp: algebra_simps)

lemma prod_diff:
  fixes f :: "'a \ 'b :: field"
  assumes "finite A" "B \ A" "\x. x \ B \ f x \ 0"
  shows   "prod f (A - B) = prod f A / prod f B"
  by (metis assms finite_subset nonzero_eq_divide_eq prod.subset_diff
      prod_zero_iff)

lemma sum_zero_power [simp]: "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)"
  for c :: "nat \ 'a::division_ring"
  by (induct A rule: infinite_finite_induct) auto

lemma sum_zero_power' [simp]:
  "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)"
  for c :: "nat \ 'a::field"
  using sum_zero_power [of "\i. c i / d i" A] by auto

lemma (in field) prod_inversef: "prod (inverse \ f) A = inverse (prod f A)"
proof (cases "finite A")
   case True
   then show ?thesis
     by (induct A rule: finite_induct) simp_all
next
   case False
   then show ?thesis
     by auto
qed

lemma (in field) prod_dividef: "(\x\A. f x / g x) = prod f A / prod g A"
  using prod_inversef [of g A] by (simp add: divide_inverse prod.distrib)

lemma prod_Un:
  fixes f :: "'b \ 'a :: field"
  assumes "finite A" and "finite B"
    and "\x\A \ B. f x \ 0"
  shows "prod f (A \ B) = prod f A * prod f B / prod f (A \ B)"
proof -
  from assms have "prod f A * prod f B = prod f (A \ B) * prod f (A \ B)"
    by (simp add: prod.union_inter [symmetric, of A B])
  with assms show ?thesis
    by simp
qed

context linordered_semidom
begin

lemma prod_nonneg: "(\a. a\A \ 0 \ f a) \ 0 \ prod f A"
  by (induct A rule: infinite_finite_induct) simp_all

lemma prod_pos: "(\a. a\A \ 0 < f a) \ 0 < prod f A"
  by (induct A rule: infinite_finite_induct) simp_all

lemma prod_mono:
  "(\i. i \ A \ 0 \ f i \ f i \ g i) \ prod f A \ prod g A"
  by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+

text \<open>Only one needs to be strict\<close>
lemma prod_mono_strict:
  assumes "i \ A" "f i < g i"
  assumes "finite A"
  assumes "\i. i \ A \ 0 \ f i \ f i \ g i"
  assumes "\i. i \ A \ 0 < g i"
  shows   "prod f A < prod g A"
proof -
  have "prod f A = f i * prod f (A - {i})"
    using assms by (intro prod.remove)
  also have "\ \ f i * prod g (A - {i})"
    using assms by (intro mult_left_mono prod_mono) auto
  also have "\ < g i * prod g (A - {i})"
    using assms by (intro mult_strict_right_mono prod_pos) auto
  also have "\ = prod g A"
    using assms by (intro prod.remove [symmetric])
  finally show ?thesis .
qed

lemma prod_le_power:
  assumes A: "\i. i \ A \ 0 \ f i \ f i \ n" "card A \ k" and "n \ 1"
  shows "prod f A \ n ^ k"
  using A
proof (induction A arbitrary: k rule: infinite_finite_induct)
  case (insert i A)
  then obtain k' where k': "card A \ k'" "k = Suc k'"
    using Suc_le_D by force
  have "f i * prod f A \ n * n ^ k'"
    using insert \<open>n \<ge> 1\<close> k' by (intro prod_nonneg mult_mono; force)
  then show ?case
    by (auto simp: \<open>k = Suc k'\<close> insert.hyps)
qed (use \<open>n \<ge> 1\<close> in auto)

end

lemma prod_mono2:
  fixes f :: "'a \ 'b :: linordered_idom"
  assumes fin: "finite B"
    and sub: "A \ B"
    and nn: "\b. b \ B-A \ 1 \ f b"
    and A: "\a. a \ A \ 0 \ f a"
  shows "prod f A \ prod f B"
proof -
  have "prod f A \ prod f A * prod f (B-A)"
    by (metis prod_ge_1 A mult_le_cancel_left1 nn not_less prod_nonneg)
  also from fin finite_subset[OF sub fin] have "\ = prod f (A \ (B-A))"
    by (simp add: prod.union_disjoint del: Un_Diff_cancel)
  also from sub have "A \ (B-A) = B" by blast
  finally show ?thesis .
qed

lemma less_1_prod:
  fixes f :: "'a \ 'b::linordered_idom"
  shows "finite I \ I \ {} \ (\i. i \ I \ 1 < f i) \ 1 < prod f I"
  by (induct I rule: finite_ne_induct) (auto intro: less_1_mult)

lemma less_1_prod2:
  fixes f :: "'a \ 'b::linordered_idom"
  assumes I: "finite I" "i \ I" "1 < f i" "\i. i \ I \ 1 \ f i"
  shows "1 < prod f I"
proof -
  have "1 < f i * prod f (I - {i})"
    using assms
    by (meson DiffD1 leI less_1_mult less_le_trans mult_le_cancel_left1 prod_ge_1)
  also have "\ = prod f I"
    using assms by (simp add: prod.remove)
  finally show ?thesis .
qed

lemma (in linordered_field) abs_prod: "\prod f A\ = (\x\A. \f x\)"
  by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)

lemma prod_eq_1_iff [simp]: "finite A \ prod f A = 1 \ (\a\A. f a = 1)"
  for f :: "'a \ nat"
  by (induct A rule: finite_induct) simp_all

lemma prod_pos_nat_iff [simp]: "finite A \ prod f A > 0 \ (\a\A. f a > 0)"
  for f :: "'a \ nat"
  using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)

lemma prod_constant [simp]: "(\x\ A. y) = y ^ card A"
  for y :: "'a::comm_monoid_mult"
  by (induct A rule: infinite_finite_induct) simp_all

lemma prod_diff_swap:
  fixes f :: "'a \ 'b :: comm_ring_1"
  shows "prod (\x. f x - g x) A = (-1) ^ card A * prod (\x. g x - f x) A"
  using prod.distrib[of "\_. -1" "\x. f x - g x" A]
  by simp

lemma prod_power_distrib: "prod f A ^ n = prod (\x. (f x) ^ n) A"
  for f :: "'a \ 'b::comm_semiring_1"
  by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib)

lemma power_inject_exp':
  assumes "a \ 1" "a > (0 :: 'a :: linordered_semidom)"
  shows   "a ^ m = a ^ n \ m = n"
  by (metis assms not_less_iff_gr_or_eq order_le_less power_decreasing_iff
      power_inject_exp)

lemma power_sum: "c ^ (\a\A. f a) = (\a\A. c ^ f a)"
  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)

lemma prod_gen_delta:
--> --------------------

--> maximum size reached

--> --------------------

quality97%

¤ Dauer der Verarbeitung: 0.36 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.