Theory Infinite_Sums_Enat

section ‹Infinite Sums over Extended Natural Numbers›


text ‹This is a theory of infinite sums of extended natural numbers defined as limits of finite sums. 
The goal is to make reasoning about these infinite sums almost as easy as that about finite sums. 
›


theory Infinite_Sums_Enat
  imports "HOL-Library.Countable_Set" "HOL-Library.Extended_Nat"
begin

subsection ‹Preliminaries›

lemma enat_pm_iff:
  "⋀a b c. b ≤ c ⟹ (a::enat) + b ≤ c ⟷ a ≤ c - b"
  "⋀a b c. a ≤ c ⟹ (a::enat) + b ≤ c ⟷ b ≤ c - a"
  "⋀a b c. a ≤ b ⟹ c ≤ b ⟹ (a::enat) ≤ b - c ⟷ c ≤ b - a"
  by (smt (verit) add.commute add_diff_cancel_enat add_left_mono idiff_infinity le_iff_add nle_le plus_eq_infty_iff_enat)+


lemma disjoint_finite_aux: 
  "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {} ⟹ B ⊆ ⋃ (A ` I) ⟹ finite B ⟹ finite {i ∈ I. B ∩ A i ≠ {}}"
proof -
  assume disj: "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {}"
    and hB: "B ⊆ ⋃ (A ` I)"
    and hfin: "finite B"
  show "finite {i ∈ I. B ∩ A i ≠ {}}"
  proof (rule inj_on_finite[of "λi. SOME b. b ∈ B ∩ A i" _ B])
    show "inj_on (λi. SOME b. b ∈ B ∩ A i) {i ∈ I. B ∩ A i ≠ {}}"
      unfolding inj_on_def
    proof (intro ballI impI)
      fix x y
      assume xI: "x ∈ {i ∈ I. B ∩ A i ≠ {}}" and yI: "y ∈ {i ∈ I. B ∩ A i ≠ {}}"
      assume eq: "(SOME b. b ∈ B ∩ A x) = (SOME b. b ∈ B ∩ A y)"
      have hx: "(SOME b. b ∈ B ∩ A x) ∈ B ∩ A x"
      proof -
        from xI have "B ∩ A x ≠ {}" by simp
        then obtain c where "c ∈ B ∩ A x" by blast
        then show ?thesis by (rule someI[of "λb. b ∈ B ∩ A x"])
      qed
      have hy: "(SOME b. b ∈ B ∩ A y) ∈ B ∩ A y"
      proof -
        from yI have "B ∩ A y ≠ {}" by simp
        then obtain c where "c ∈ B ∩ A y" by blast
        then show ?thesis by (rule someI[of "λb. b ∈ B ∩ A y"])
      qed
      show "x = y"
      proof (rule ccontr)
        assume "x ≠ y"
        with xI yI disj have "A x ∩ A y = {}" by auto
        with hx hy eq show False by auto
      qed
    qed
    show "(λi. SOME b. b ∈ B ∩ A i) ` {i ∈ I. B ∩ A i ≠ {}} ⊆ B"
    proof (intro subsetI)
      fix d assume "d ∈ (λi. SOME b. b ∈ B ∩ A i) ` {i ∈ I. B ∩ A i ≠ {}}"
      then obtain i where iI: "i ∈ {i ∈ I. B ∩ A i ≠ {}}" and deq: "d = (SOME b. b ∈ B ∩ A i)" by blast
      from iI have "B ∩ A i ≠ {}" by simp
      then obtain c where "c ∈ B ∩ A i" by blast
      then have "(SOME b. b ∈ B ∩ A i) ∈ B ∩ A i" by (rule someI[of "λb. b ∈ B ∩ A i"])
      with deq show "d ∈ B" by auto
    qed
    show "finite B" using hfin .
  qed
qed


lemma incl_UNION_aux: "B ⊆ ⋃ (A ` I) ⟹ B = ⋃ ((λi. (B ∩ A i)) ` {i ∈ I. B ∩ A i ≠ {}})"
  by fastforce

lemma incl_UNION_aux2: "B ⊆ ⋃ (A ` I) ⟷ B = ⋃ ((λi. (B ∩ A i)) ` I)"
  by fastforce

lemma sum_singl[simp]: "sum f {a} = f a"  
  by simp

lemma sum_two[simp]: "a1 ≠ a2 ⟹ sum f {a1,a2} = f a1 + f a2"  
  by simp

lemma sum_three[simp]: "a1 ≠ a2 ⟹ a1 ≠ a3 ⟹ a2 ≠ a3 ⟹ 
 sum f {a1,a2,a3} = f a1 + f a2 + f a3"  
  by (simp add: add.assoc)

lemma Sup_leq: 
  "A ≠ {} ⟹ ∀a∈A. ∃b∈B. (a::enat) ≤ b ⟹ Sup A ≤ Sup B"
  by (simp add: cSup_mono)


lemma Sup_image_leq: 
  "A ≠ {} ⟹  ∀a∈A. ∃b∈B. (f a::enat) ≤ g b ⟹
 Sup (f ` A) ≤ Sup (g ` B)"
  by (rule Sup_leq) auto

lemma Sup_cong: 
  assumes "A ≠ {} ∨ B ≠ {}" "∀a∈A. ∃b∈B. (a::enat) ≤ b" "∀b∈B. ∃a∈A. (b::enat) ≤ a"
  shows "Sup A = Sup B" 
proof-
  have "A ≠ {} ∧ B ≠ {}"
    using assms unfolding bdd_above_def using order.trans by blast+
  thus ?thesis using assms
    by (meson Sup_mono order_antisym)
qed

lemma Sup_image_cong: 
  "A ≠ {} ∨ B ≠ {} ⟹ ∀a∈A. ∃b∈B. (f a::enat) ≤ g b ⟹ ∀b∈B. ∃a∈A. (g b::enat) ≤ f a ⟹
 Sup (f ` A) = Sup (g ` B)"
  by (rule Sup_cong) auto

lemma Sup_congL: 
  "A ≠ {} ⟹ ∀a∈A. ∃b∈B. (a::enat) ≤ b ⟹ ∀b∈B. b ≤ Sup A ⟹ Sup A = Sup B"
  by (metis Collect_empty_eq Collect_mem_eq Sup_leq cSup_least dual_order.antisym)

lemma Sup_image_congL: 
  "A ≠ {} ⟹ ∀a∈A. ∃b∈B. (f a::enat) ≤ g b ⟹ ∀b∈B. g b ≤ Sup (f ` A) ⟹ Sup (f ` A) = Sup (g ` B)"
  by (rule Sup_congL) auto

lemma Sup_congR: 
  "B ≠ {} ⟹ ∀a∈A. a ≤ Sup B ⟹ ∀b∈B. ∃a∈A. (b::enat) ≤ a ⟹ Sup A = Sup B"
  by (metis Collect_empty_eq Collect_mem_eq Sup_leq cSup_least dual_order.antisym)

lemma Sup_image_congR: 
  "B ≠ {} ⟹ ∀a∈A. f a ≤ Sup (g ` B) ⟹ ∀b∈B. ∃a∈A. (g b::enat) ≤ f a ⟹ Sup (f ` A) = Sup (g ` B)"
  by (rule Sup_congR) auto

lemma Sup_eq_0_iff: "Sup (A :: enat set) = 0 ⟷ (∀a∈A. a = 0)"
  using Sup_bot_conv(1)[of A] unfolding bot_enat_def by auto


lemma plus_Sup_commute:
  assumes f1: "{f1 b1 | b1. φ1 b1} ≠ {}" and 
          f2: "{f2 b2 | b2. φ2 b2} ≠ {}"
  shows 
    "Sup {(f1 b1::enat) | b1 . φ1 b1} + Sup {f2 b2 | b2 . φ2 b2} = 
     Sup {f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}" (is "?L1 + ?L2 = ?R")
proof-
  have f: 
    "{f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2} ≠ {}"
    using f1 f2 by auto
  show ?thesis proof (rule order.antisym)
    show "?L1 + ?L2 ≤ ?R"
    proof -
      obtain b1_wit where hb1_wit: "φ1 b1_wit" using f1 by auto
      have hL2_le_R: "?L2 ≤ ?R"
      proof (intro cSup_le_iff[OF f2 bdd_above_top, THEN iffD2] ballI)
        fix x assume "x ∈ {f2 b2 | b2. φ2 b2}"
        then obtain b2 where hb: "x = f2 b2" "φ2 b2" by auto
        have mem: "f1 b1_wit + f2 b2 ∈ {f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}"
          using hb1_wit hb(2) by blast
        have "f2 b2 ≤ f1 b1_wit + f2 b2" by (simp add: le_add2)
        also have "... ≤ ?R" using cSup_upper[OF mem bdd_above_top] by simp
        finally show "x ≤ ?R" using hb(1) by simp
      qed
      have hL1_le_R: "⋀b1. φ1 b1 ⟹ f1 b1 ≤ ?R"
      proof -
        fix b1 assume hφ1: "φ1 b1"
        obtain b2 where hb2: "φ2 b2" using f2 by auto
        have mem: "f1 b1 + f2 b2 ∈ {f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}"
          using hφ1 hb2 by blast
        have "f1 b1 ≤ f1 b1 + f2 b2" by (simp add: le_add1)
        also have "... ≤ ?R" using cSup_upper[OF mem bdd_above_top] by simp
        finally show "f1 b1 ≤ ?R" .
      qed
      have hL1_le: "?L1 ≤ ?R - ?L2"
      proof (intro cSup_le_iff[OF f1 bdd_above_top, THEN iffD2] ballI)
        fix x assume "x ∈ {f1 b1 | b1. φ1 b1}"
        then obtain b1 where hb: "x = f1 b1" "φ1 b1" by auto
        have hfb1_le_R: "f1 b1 ≤ ?R" using hL1_le_R hb(2) by blast
        have hL2_le_Rm: "?L2 ≤ ?R - f1 b1"
        proof (intro cSup_le_iff[OF f2 bdd_above_top, THEN iffD2] ballI)
          fix y assume "y ∈ {f2 b2 | b2. φ2 b2}"
          then obtain b2 where hy: "y = f2 b2" "φ2 b2" by auto
          have mem: "f1 b1 + f2 b2 ∈ {f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}"
            using hb(2) hy(2) by blast
          have hle: "f1 b1 + f2 b2 ≤ ?R" using cSup_upper[OF mem bdd_above_top] by simp
          show "y ≤ ?R - f1 b1"
            using enat_pm_iff(2)[OF hfb1_le_R] hle hy(1) by simp
        qed
        show "x ≤ ?R - ?L2"
          using enat_pm_iff(3)[OF hfb1_le_R hL2_le_R] hL2_le_Rm hb(1) by simp
      qed
      show "?L1 + ?L2 ≤ ?R"
        using enat_pm_iff(1)[OF hL2_le_R] hL1_le by simp
    qed
  next
    show "?R ≤ ?L1 + ?L2"
    proof (intro cSup_le_iff[OF f bdd_above_top, THEN iffD2] ballI)
      fix x assume "x ∈ {f1 b1 + f2 b2 | b1 b2. φ1 b1 ∧ φ2 b2}"
      then obtain b1 b2 where hx: "x = f1 b1 + f2 b2" "φ1 b1" "φ2 b2" by auto
      have mem1: "f1 b1 ∈ {f1 b1 | b1. φ1 b1}" using hx(2) by blast
      have mem2: "f2 b2 ∈ {f2 b2 | b2. φ2 b2}" using hx(3) by blast
      have h1: "f1 b1 ≤ ?L1" using cSup_upper[OF mem1 bdd_above_top] by simp
      have h2: "f2 b2 ≤ ?L2" using cSup_upper[OF mem2 bdd_above_top] by simp
      show "x ≤ ?L1 + ?L2" using h1 h2 hx(1) by (simp add: add_mono)
    qed
  qed
qed

lemma plus_Sup_commute':
  assumes f1: "A1 ≠ {}" and f2: "A2 ≠ {}"
  shows "Sup A1 + Sup A2 = Sup {(a1::enat) + a2 | a1 a2. a1 ∈ A1 ∧ a2 ∈ A2}"  
  using plus_Sup_commute[of id "λa1. a1 ∈ A1" id "λa2. a2 ∈ A2"] assms 
  by auto

lemma plus_SupR: "A ≠ {} ⟹ Sup A + (b::enat) = Sup {a + b | a. a ∈ A}"
proof -
  assume hA: "A ≠ {}"
  have "Sup A + b = Sup A + Sup {b}" by simp
  also have "... = Sup {a1 + a2 | a1 a2. a1 ∈ A ∧ a2 ∈ {b}}"
    using plus_Sup_commute'[of A "{b}"] hA by auto
  also have "... = Sup {a + b | a. a ∈ A}" by auto
  finally show ?thesis .
qed

lemma plus_SupL: "A ≠ {} ⟹ (b::enat) + Sup A = Sup {b + a | a. a ∈ A}"
proof -
  assume hA: "A ≠ {}"
  have "b + Sup A = Sup {b} + Sup A" by simp
  also have "... = Sup {a1 + a2 | a1 a2. a1 ∈ {b} ∧ a2 ∈ A}"
    using plus_Sup_commute'[of "{b}" A] hA by auto
  also have "... = Sup {b + a | a. a ∈ A}" by auto
  finally show ?thesis .
qed



lemma sum_mono3: 
  "finite B ⟹ A ⊆ B ⟹ (⋀a. a ∈ A ⟹ (f a::enat) ≤ g a) ⟹ 
 sum f A ≤ sum g B"
  by (metis order_trans sum_mono sum_mono2 zero_le)

lemma sum_Sup_commute: 
  fixes h :: "'a ⇒ enat"
  assumes "finite J" and "∀i∈J. {h b | b. φ i b} ≠ {}"
  shows "sum (λi. Sup {h b | b. φ i b}) J = 
       Sup {sum (λi. h (b i)) J | b . ∀i∈J. φ i (b i)}"
  using assms proof (induction J)
  case empty then show ?case by simp
next
  case (insert j J)
  have note1: "{∑i∈J. h (b i) | b. ∀i∈J. φ i (b i)} ≠ {}"
    if hyp: "∀i∈J. {h b | b. φ i b} ≠ {}"
  proof -
    from hyp have "∀i∈J. ∃b. φ i b" by auto
    then have "∃b. ∀i∈J. φ i (b i)"
      by (intro exI[of _ "λi. SOME b. φ i b"]) (simp add: some_eq_ex)
    then show ?thesis by blast
  qed
  have hJ_ne: "∀i∈J. {h b | b. φ i b} ≠ {}" using insert.prems by auto
  have hIH: "sum (λi. Sup {h b | b. φ i b}) J = Sup {sum (λi. h (b i)) J | b. ∀i∈J. φ i (b i)}"
    using insert.IH[OF hJ_ne] by simp
  have hpsc: "Sup {h b | b. φ j b} + Sup {sum (λi. h (b i)) J | b. ∀i∈J. φ i (b i)} =
              Sup {h b1 + sum (λi. h (b2 i)) J | b1 b2. φ j b1 ∧ (∀i∈J. φ i (b2 i))}"
    using plus_Sup_commute[of h "φ j" "λb. sum (λi. h (b i)) J" "λb2. ∀i∈J. φ i (b2 i)"]
          insert.prems note1[OF hJ_ne]
    by auto
  have hset: "{h b1 + sum (λi. h (b2 i)) J | b1 b2. φ j b1 ∧ (∀i∈J. φ i (b2 i))} =
              {sum (λi. h (b i)) (insert j J) | b. ∀i∈insert j J. φ i (b i)}"
    using insert.hyps
  proof (intro set_eqI iffI)
    fix x
    assume "x ∈ {h b1 + sum (λi. h (b2 i)) J | b1 b2. φ j b1 ∧ (∀i∈J. φ i (b2 i))}"
    then obtain b1 b2 where hx: "x = h b1 + sum (λi. h (b2 i)) J" "φ j b1" "∀i∈J. φ i (b2 i)"
      by auto
    let ?b = "λj'. if j' = j then b1 else b2 j'"
    have hb_J: "∀i∈J. ?b i = b2 i" using insert.hyps by simp
    have hsum_eq: "sum (λi. h (?b i)) J = sum (λi. h (b2 i)) J"
      by (rule sum.cong) (auto simp: hb_J)
    have "x = sum (λi. h (?b i)) (insert j J)"
      using hx insert.hyps by (simp add: hsum_eq)
    moreover have "∀i∈insert j J. φ i (?b i)"
      using hx insert.hyps by (auto simp: insertE)
    ultimately show "x ∈ {sum (λi. h (b i)) (insert j J) | b. ∀i∈insert j J. φ i (b i)}"
      by auto
  next
    fix x
    assume "x ∈ {sum (λi. h (b i)) (insert j J) | b. ∀i∈insert j J. φ i (b i)}"
    then obtain b where hx: "x = sum (λi. h (b i)) (insert j J)" "∀i∈insert j J. φ i (b i)"
      by auto
    have "x = h (b j) + sum (λi. h (b i)) J"
      using insert.hyps hx(1) by simp
    then show "x ∈ {h b1 + sum (λi. h (b2 i)) J | b1 b2. φ j b1 ∧ (∀i∈J. φ i (b2 i))}"
      using hx(2) by auto
  qed
  show ?case
    using insert.hyps
    by (simp add: hIH hpsc hset)
qed


subsection ‹Infinite Summation›

(* Infinite sums *)
definition isum :: "('a ⇒ enat) ⇒ 'a set ⇒ enat" where 
  "isum f A ≡ Sup (sum f  ` {B | B . B ⊆ A ∧ finite B})"

lemma isum_subset_mono: "A ⊆ B ⟹ isum f A ≤ isum f B"
  unfolding isum_def image_def
  by(auto intro: Sup_subset_mono)

(* isum versus sum *)
lemma isum_eq_sum:
  "finite A ⟹ isum f A = sum f A"
proof -
  assume hA: "finite A"
  show "isum f A = sum f A"
    unfolding isum_def
  proof (rule cSup_eq_maximum)
    show "sum f A ∈ sum f ` {B | B. B ⊆ A ∧ finite B}" using hA by blast
    show "⋀x. x ∈ sum f ` {B | B. B ⊆ A ∧ finite B} ⟹ x ≤ sum f A"
      using hA by (auto intro: sum_mono2)
  qed
qed







(* Congruence and monotonicity *)
(* thm sum.cong *)
lemma isum_cong: 
  assumes "A = B" and "⋀x. x ∈ B ⟹ g x = h x" 
  shows "isum g A = isum h B"
  using assms unfolding isum_def 
  by (auto intro!: SUP_cong comm_monoid_add_class.sum.cong)

(* thm sum_mono *)
lemma isum_mono: 
  assumes "⋀x. x ∈ A ⟹ g x ≤ h x" 
  shows "isum g A ≤ isum h A"
  unfolding isum_def
proof (intro cSup_mono)
  show "sum g ` {B | B. B ⊆ A ∧ finite B} ≠ {}" by auto
  show "bdd_above (sum h ` {B | B. B ⊆ A ∧ finite B})"
    unfolding bdd_above_def using bdd_above.unfold by blast
  fix r assume "r ∈ sum g ` {B | B. B ⊆ A ∧ finite B}"
  then obtain B where hB: "B ⊆ A" "finite B" and hr: "r = sum g B" by blast
  show "∃b ∈ sum h ` {B | B. B ⊆ A ∧ finite B}. r ≤ b"
  proof (intro bexI[of _ "sum h B"])
    show "r ≤ sum h B" using hr assms hB by (auto intro: sum_mono)
    show "sum h B ∈ sum h ` {B | B. B ⊆ A ∧ finite B}" using hB by blast
  qed
qed

lemma isum_mono': 
  assumes "A ⊆ B" 
  shows "isum g A ≤ isum g B"
  using assms unfolding isum_def
  by (intro cSup_subset_mono) (auto intro!: exI[of _ "∞"])

(* isum vs. 0 *)
(* thm comm_monoid_add_class.sum.empty *)
lemma isum_empty[simp]: "isum g {} = 0"
  unfolding isum_def by auto

(* thm comm_monoid_add_class.sum.neutral_const *)
lemma isum_const_zero[simp]: "isum (λx. 0) A = 0"
  unfolding isum_def 
  by simp (metis cSUP_const empty_iff empty_subsetI finite.emptyI mem_Collect_eq)

(* thm sum.neutral  *)
lemma isum_const_zero': "∀x∈A. g x = 0 ⟹ isum g A = 0"
  by (simp add: isum_cong)

(* thm sum_eq_0_iff  *)
lemma isum_eq_0_iff: "isum f A = 0 ⟷ (∀a∈A. f a = 0)"
  unfolding isum_def by (subst Sup_eq_0_iff) auto

(* Reindexing: *)
(* thm sum.reindex *)
lemma isum_reindex: "inj_on h A ⟹ isum g (h ` A) = isum (g ∘ h) A"
  unfolding isum_def
proof (intro arg_cong[of _ _ Sup])
  assume "inj_on h A"
  then have "sum (g ∘ h) B = sum g (image h B)" if "B ⊆ A" for B
    by (simp add: inj_on_subset sum.reindex that)
  then show "sum g ` {B |B. B ⊆ h ` A ∧ finite B} =
    sum (g ∘ h) ` {B |B. B ⊆ A ∧ finite B}"
    by (auto simp: image_iff dest: finite_subset_image)
qed

(* thm sum.reindex_cong *)
lemma isum_reindex_cong: "inj_on l B ⟹ A = l ` B ⟹ 
 (⋀x. x ∈ B ⟹ g (l x) = h x) ⟹ isum g A = isum h B"
  by (metis isum_cong comp_def isum_reindex)

(* thm sum.reindex_nontrivial *)
lemma isum_reindex_cong': 
  assumes "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ x ≠ y ⟹ h x = h y ⟹ g (h x) = 0)"
  shows "isum g (h ` A) = isum (g ∘ h) A"
  unfolding isum_def
proof (safe intro!: arg_cong[of _ _ Sup])
  fix B
  assume "B ⊆ h ` A" "finite B"
  with assms show "sum g B ∈ sum (g ∘ h) ` {B |B. B ⊆ A ∧ finite B}"
    by (smt (verit) finite_subset_image image_iff in_mono mem_Collect_eq
        sum.reindex_nontrivial)
next
  fix B
  assume "B ⊆ A" "finite B"
  with assms show "sum (g ∘ h) B ∈ sum g ` {B |B. B ⊆ h ` A ∧ finite B}"
    by (smt (verit, ccfv_SIG) finite_imageI image_iff mem_Collect_eq subset_iff
        sum.reindex_nontrivial)
qed

(* thm sum.mono_neutral_cong *)
lemma isum_zeros_cong:
  assumes "⋀i. i ∈ T - S ⟹ h i = 0" and "⋀i. i ∈ S - T ⟹ g i = 0"
    and "⋀x. x ∈ S ∩ T ⟹ g x = h x"
  shows "isum g S = isum h T"
  unfolding isum_def
proof (rule Sup_image_cong)
  show "{B |B. B ⊆ S ∧ finite B} ≠ {} ∨ {B |B. B ⊆ T ∧ finite B} ≠ {}"
    by auto
next
  show "∀a ∈ {B |B. B ⊆ S ∧ finite B}. ∃b ∈ {B |B. B ⊆ T ∧ finite B}. sum g a ≤ sum h b"
  proof (intro ballI)
    fix a assume "a ∈ {B |B. B ⊆ S ∧ finite B}"
    then have hA: "a ⊆ S" "finite a" by blast+
    show "∃b ∈ {B |B. B ⊆ T ∧ finite B}. sum g a ≤ sum h b"
    proof (intro bexI[of _ "a ∩ T"])
      show "sum g a ≤ sum h (a ∩ T)"
        by (rule order_eq_refl, rule sum.mono_neutral_cong) (use assms hA in auto)
      show "a ∩ T ∈ {B |B. B ⊆ T ∧ finite B}"
        using hA by blast
    qed
  qed
next
  show "∀b ∈ {B |B. B ⊆ T ∧ finite B}. ∃a ∈ {B |B. B ⊆ S ∧ finite B}. sum h b ≤ sum g a"
  proof (intro ballI)
    fix b assume "b ∈ {B |B. B ⊆ T ∧ finite B}"
    then have hB: "b ⊆ T" "finite b" by blast+
    show "∃a ∈ {B |B. B ⊆ S ∧ finite B}. sum h b ≤ sum g a"
    proof (intro bexI[of _ "b ∩ S"])
      show "sum h b ≤ sum g (b ∩ S)"
        by (rule order_eq_refl, rule sum.mono_neutral_cong) (use assms hB in auto)
      show "b ∩ S ∈ {B |B. B ⊆ S ∧ finite B}"
        using hB by blast
    qed
  qed
qed


(* thm sum.mono_neutral_left *)
lemma isum_zeros_congL: 
  "S ⊆ T ⟹ ∀i∈T - S. g i = 0 ⟹ isum g S = isum g T"
  by (metis Diff_eq_empty_iff emptyE isum_zeros_cong)

(* thm sum.mono_neutral_right *)
lemma isum_zeros_congR:
  "S ⊆ T ⟹ ∀i∈T - S. g i = 0 ⟹ isum g T = isum g S"
  by (simp add: isum_zeros_congL)

lemma isum_singl[simp]: "isum f {a} = f a"  
  by (simp add: isum_eq_sum)

lemma isum_two[simp]: "a1 ≠ a2 ⟹ isum f {a1,a2} = f a1 + f a2"  
  by (simp add: isum_eq_sum)

lemma isum_three[simp]: "a1 ≠ a2 ⟹ a1 ≠ a3 ⟹ a2 ≠ a3 ⟹
 isum f {a1,a2,a3} = f a1 + f a2 + f a3"  
  by (simp add: isum_eq_sum)

lemma in_le_isum: "a ∈ A ⟹ f a ≤ isum f A"
  by (metis isum_mono' isum_singl singletonD subsetI)

lemma isum_eq_singl: 
  assumes fx: "f a = x" and f: "∀a'. a' ≠ a ⟶ f a' = 0" and a: "a ∈ A"
  shows "isum f A = x"
proof -
  have "isum f A = isum f {a}"
    by (rule isum_zeros_cong) (use assms in auto)
  then show ?thesis by (simp add: fx)
qed

lemma isum_le_singl: 
  assumes fx: "f a ≤ x" and f: "∀a'. a' ≠ a ⟶ f a' = 0" and a: "a ∈ A"
  shows "isum f A ≤ x"
  by (metis a f fx isum_eq_singl)

lemma isum_insert[simp]: "a ∉ A ⟹ isum f (insert a A) = isum f A + f a"
proof -
  assume ha: "a ∉ A"
  have hA: "sum f ` {B |B. B ⊆ A ∧ finite B} ≠ {}" by auto
  show ?thesis
    unfolding isum_def
  proof (subst plus_SupR[OF hA], rule Sup_cong)
    show "sum f ` {B |B. B ⊆ insert a A ∧ finite B} ≠ {} ∨
          {x + f a |x. x ∈ sum f ` {B |B. B ⊆ A ∧ finite B}} ≠ {}" by auto
  next
    show "∀v ∈ sum f ` {B |B. B ⊆ insert a A ∧ finite B}.
          ∃w ∈ {x + f a |x. x ∈ sum f ` {B |B. B ⊆ A ∧ finite B}}. v ≤ w"
    proof (intro ballI)
      fix v assume "v ∈ sum f ` {B |B. B ⊆ insert a A ∧ finite B}"
      then obtain B where hB: "B ⊆ insert a A" "finite B" and hv: "v = sum f B" by blast
      show "∃w ∈ {x + f a |x. x ∈ sum f ` {B |B. B ⊆ A ∧ finite B}}. v ≤ w"
      proof (intro bexI[of _ "sum f (B - {a}) + f a"])
        show "v ≤ sum f (B - {a}) + f a"
        proof (cases "a ∈ B")
          case True
          then have "sum f B = f a + sum f (B - {a})" using hB by (simp add: sum.remove)
          then show ?thesis unfolding hv by (simp add: add.commute)
        next
          case False
          then show ?thesis unfolding hv by simp
        qed
        show "sum f (B - {a}) + f a ∈ {x + f a |x. x ∈ sum f ` {B |B. B ⊆ A ∧ finite B}}"
          using hB ha by blast
      qed
    qed
  next
    show "∀w ∈ {x + f a |x. x ∈ sum f ` {B |B. B ⊆ A ∧ finite B}}.
          ∃v ∈ sum f ` {B |B. B ⊆ insert a A ∧ finite B}. w ≤ v"
    proof (intro ballI)
      fix w assume "w ∈ {x + f a |x. x ∈ sum f ` {B |B. B ⊆ A ∧ finite B}}"
      then obtain B where hB: "B ⊆ A" "finite B" and hw: "w = sum f B + f a" by blast
      show "∃v ∈ sum f ` {B |B. B ⊆ insert a A ∧ finite B}. w ≤ v"
      proof (intro bexI[of _ "sum f (insert a B)"])
        show "w ≤ sum f (insert a B)"
          unfolding hw using ha hB by force
        show "sum f (insert a B) ∈ sum f ` {B |B. B ⊆ insert a A ∧ finite B}"
          using hB by blast
      qed
    qed
  qed
qed



(* thm sum.UNION_disjoint *)
lemma isum_UNION: 
  assumes dsj: "∀i∈I. ∀j∈I. i ≠ j ⟶ A i ∩ A j = {}"
  shows "isum g (⋃ (A ` I)) = isum (λi. isum g (A i)) I"
proof -
  have step1: "⋀J. J ⊆ I ⟹ finite J ⟹
      (∑i∈J. Sup {y. ∃B⊆A i. finite B ∧ y = sum g B}) ≤
      Sup {y. ∃B⊆⋃ (A ` I). finite B ∧ y = sum g B}"
  proof -
    fix J assume J1: "J ⊆ I" "finite J"
    have hsets_ne: "∀i∈J. {sum g B | B. B ⊆ A i ∧ finite B} ≠ {}"
      by auto
    have step1a:
      "sum (λi. Sup {sum g B | B. B ⊆ A i ∧ finite B}) J =
       Sup {sum (λi. sum g (B i)) J | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
      using sum_Sup_commute[OF J1(2) hsets_ne] by simp
    have step1b:
      "Sup {sum (λi. sum g (B i)) J | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)} =
       Sup {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
    proof (rule arg_cong[of _ _ Sup], intro set_eqI iffI)
      fix x
      assume "x ∈ {sum (λi. sum g (B i)) J | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
      then obtain B where hB: "∀i∈J. B i ⊆ A i ∧ finite (B i)"
        and hx: "x = sum (λi. sum g (B i)) J" by auto
      have hdisj: "∀i∈J. ∀j∈J. i ≠ j ⟶ B i ∩ B j = {}"
      proof (intro ballI impI)
        fix i j assume "i ∈ J" "j ∈ J" "i ≠ j"
        have "A i ∩ A j = {}" using dsj ‹i ∈ J› ‹j ∈ J› ‹i ≠ j› J1(1) by auto
        moreover have "B i ⊆ A i" "B j ⊆ A j" using hB ‹i ∈ J› ‹j ∈ J› by auto
        ultimately show "B i ∩ B j = {}" by auto
      qed
      have "x = sum g (⋃ (B ` J))"
        unfolding hx
        by (rule sum.UNION_disjoint[symmetric]) (use J1(2) hB hdisj in auto)
      then show "x ∈ {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
        using hB by auto
    next
      fix x
      assume "x ∈ {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
      then obtain B where hB: "∀i∈J. B i ⊆ A i ∧ finite (B i)"
        and hx: "x = sum g (⋃ (B ` J))" by auto
      have hdisj: "∀i∈J. ∀j∈J. i ≠ j ⟶ B i ∩ B j = {}"
      proof (intro ballI impI)
        fix i j assume "i ∈ J" "j ∈ J" "i ≠ j"
        have "A i ∩ A j = {}" using dsj ‹i ∈ J› ‹j ∈ J› ‹i ≠ j› J1(1) by auto
        moreover have "B i ⊆ A i" "B j ⊆ A j" using hB ‹i ∈ J› ‹j ∈ J› by auto
        ultimately show "B i ∩ B j = {}" by auto
      qed
      have "x = sum (λi. sum g (B i)) J"
        unfolding hx
        by (rule sum.UNION_disjoint) (use J1(2) hB hdisj in auto)
      then show "x ∈ {sum (λi. sum g (B i)) J | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
        using hB by auto
    qed
    have step1c:
      "Sup {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)} =
       Sup {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B}"
    proof (rule Sup_cong)
      show "{sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)} ≠ {} ∨
            {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B} ≠ {}" by auto
    next
      show "∀a ∈ {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}.
            ∃b ∈ {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B}. a ≤ b"
      proof (intro ballI)
        fix a assume "a ∈ {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
        then obtain B where hB: "∀i∈J. B i ⊆ A i ∧ finite (B i)"
          and ha: "a = sum g (⋃ (B ` J))" by auto
        show "∃b ∈ {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B}. a ≤ b"
        proof (intro bexI[of _ "sum g (⋃ (B ` J))"])
          show "sum g (⋃ (B ` J)) ∈ {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B}"
            using J1 hB by force
          show "a ≤ sum g (⋃ (B ` J))" using ha by simp
        qed
      qed
    next
      show "∀b ∈ {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B}.
            ∃a ∈ {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}. b ≤ a"
      proof (intro ballI)
        fix b assume "b ∈ {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B}"
        then obtain C where hCsub: "C ⊆ ⋃ (A ` J)" "finite C"
          and hb: "b = sum g C" by auto
        show "∃a ∈ {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}. b ≤ a"
        proof (intro bexI[of _ "sum g (⋃ ((λi. C ∩ A i) ` J))"])
          show "b ≤ sum g (⋃ ((λi. C ∩ A i) ` J))"
            using hCsub unfolding incl_UNION_aux2 by (auto simp: hb)
          show "sum g (⋃ ((λi. C ∩ A i) ` J)) ∈
                {sum g (⋃ (B ` J)) | B. ∀i∈J. B i ⊆ A i ∧ finite (B i)}"
            using J1 hCsub by blast
        qed
      qed
    qed
    have step1d:
      "Sup {sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B} ≤
       Sup {sum g B | B. B ⊆ ⋃ (A ` I) ∧ finite B}"
    proof (rule cSup_subset_mono)
      show "{sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B} ≠ {}" by auto
      show "{sum g B | B. B ⊆ ⋃ (A ` J) ∧ finite B} ⊆
            {sum g B | B. B ⊆ ⋃ (A ` I) ∧ finite B}"
        using J1 by (force intro: Union_mono)
    qed simp
    show "(∑i∈J. Sup {y. ∃B⊆A i. finite B ∧ y = sum g B}) ≤
          Sup {y. ∃B⊆⋃ (A ` I). finite B ∧ y = sum g B}"
      using step1a step1b step1c step1d
      by (smt (verit, best) Collect_eqI order.trans order.refl sum_mono)
  qed
  show ?thesis
    unfolding isum_def
  proof (intro Sup_image_congL ballI)
    show "{B |B. B ⊆ ⋃ (A ` I) ∧ finite B} ≠ {}" by auto
  next
    fix B assume hB: "B ∈ {B |B. B ⊆ ⋃ (A ` I) ∧ finite B}"
    then have hBsub: "B ⊆ ⋃ (A ` I)" and hBfin: "finite B" by blast+
    let ?J = "{i. i ∈ I ∧ B ∩ A i ≠ {}}"
    show "∃b ∈ {B |B. B ⊆ I ∧ finite B}.
          sum g B ≤ (∑i∈b. Sup (sum g ` {B |B. B ⊆ A i ∧ finite B}))"
    proof (intro bexI[of _ ?J])
      have "sum g B ≤ sum (λi. Sup {y. ∃x∈{B |B. B ⊆ A i ∧ finite B}. y = sum g x}) ?J"
      proof -
        have hJfin: "finite ?J" using dsj hBsub hBfin disjoint_finite_aux by blast
        have hJsub: "?J ⊆ I" by auto
        have hdecomp: "B = ⋃ ((λi. B ∩ A i) ` ?J)"
          using incl_UNION_aux[OF hBsub] by simp
        have hdisj_J: "∀i∈?J. ∀j∈?J. i ≠ j ⟶ (B ∩ A i) ∩ (B ∩ A j) = {}"
          using dsj hJsub by auto
        have hfin_J: "∀i∈?J. finite (B ∩ A i)"
          using hBfin by auto
        have hsum_eq: "sum g B = sum (λi. sum g (B ∩ A i)) ?J"
          by (subst hdecomp, rule comm_monoid_add_class.sum.UNION_disjoint)
            (use hJfin hdisj_J hfin_J in auto)
        show ?thesis
          unfolding hsum_eq
        proof (rule sum_mono)
          fix i assume "i ∈ ?J"
          then have "B ∩ A i ⊆ A i" "finite (B ∩ A i)" using hBfin by auto
          with hBsub show "sum g (B ∩ A i) ≤ Sup {y. ∃x∈{B |B. B ⊆ A i ∧ finite B}. y = sum g x}"
            by (intro cSup_upper) auto
        qed
      qed
      then show "sum g B ≤ (∑i | i ∈ I ∧ B ∩ A i ≠ {}. Sup (sum g ` {B |B. B ⊆ A i ∧ finite B}))"
        by (rule order_trans) (auto intro!: Sup_mono sum_mono)
      show "?J ∈ {B |B. B ⊆ I ∧ finite B}"
        using dsj hBsub hBfin disjoint_finite_aux by force
    qed
  next
    fix J assume hB: "J ∈ {B |B. B ⊆ I ∧ finite B}"
    then have J1: "J ⊆ I" "finite J" by blast+
    show "(∑i∈J. Sup (sum g ` {B |B. B ⊆ A i ∧ finite B}))
         ≤ Sup (sum g ` {B |B. B ⊆ ⋃ (A ` I) ∧ finite B})"
      using step1[OF J1] by (auto simp: image_def)
  qed
qed

lemma isum_Un[simp]: 
  assumes "A1 ∩ A2 = {}"
  shows "isum f (A1 ∪ A2) = isum f A1 + isum f A2"
proof-
  have [simp]: "isum (λi. isum f (case i of 0 ⇒ A1 | Suc _ ⇒ A2)) {0, Suc 0} = isum f A1 + isum f A2"
    by (subst isum_two) auto
  show ?thesis using assms isum_UNION[of "{0,1::nat}" "λi. case i of 0 ⇒ A1 |_ ⇒ A2" f] by auto
qed

(* thm sum.Sigma *)
lemma isum_Sigma: 
  "isum (λ(a,b). f a b) (Sigma A Bs) = isum (λa. isum (f a) (Bs a)) A"
proof-
  define g where "g ≡ λ(a,b). f a b"
  define Cs where "Cs ≡ λa. {a} × Bs a"
  have 1: "⋀a. {a} × Bs a = Pair a ` (Bs a)" by auto
  have 0: "Sigma A Bs = (⋃a∈A. Cs a)" unfolding Cs_def by auto
  show ?thesis unfolding 0
  proof (subst isum_UNION)
    show "∀i∈A. ∀j∈A. i ≠ j ⟶ Cs i ∩ Cs j = {}" unfolding Cs_def by auto
  next
    show "isum (λi. isum (λ(x, y). f x y) (Cs i)) A = isum (λa. isum (f a) (Bs a)) A"
      unfolding Cs_def
    proof (rule isum_cong)
      show "A = A" ..
    next
      fix a assume "a ∈ A"
      show "isum (λ(x, y). f x y) ({a} × Bs a) = isum (f a) (Bs a)"
      proof -
        have "isum (λ(x, y). f x y) ({a} × Bs a) = isum (λ(x, y). f x y) (Pair a ` Bs a)"
          by (simp add: 1)
        also have "… = isum (f a) (Bs a)"
          by (subst isum_reindex_cong') (auto simp: o_def)
        finally show ?thesis .
      qed
    qed
  qed
qed

(* Redundant but visually useful: *)
(* thm sum.cartesian_product *)
lemma isum_Times: "isum (λ(a,b). f a b) (A × B) = isum (λa. isum (f a) B) A"
  using isum_Sigma .

(* thm sum.swap *)
lemma isum_swap: "isum (λa. isum (f a) B) A = isum (λb. isum (λa. f a b) A) B" (is "?L = ?R")
proof-
  have 0: "A × B = (λ(a,b). (b,a)) ` (B × A)" by auto
  have "?L = isum (λ(a,b). f a b) (A × B)" using isum_Times ..
  also have "… = isum (λ(b,a). f a b) (B × A)" unfolding 0 by (subst isum_reindex_cong') (auto simp: o_def intro!: arg_cong2[of _ _ _ _ isum])
  also have "… = ?R" by (subst isum_Times) auto
  finally show ?thesis .
qed

lemma isum_plus:
  shows "isum (λa. f1 a + f2 a) A = isum f1 A + isum f2 A"
proof -
  let ?S = "sum f1 ` {B |B. B ⊆ A ∧ finite B}"
  let ?T = "sum f2 ` {B |B. B ⊆ A ∧ finite B}"
  have hS: "?S ≠ {}" by auto
  have hT: "?T ≠ {}" by auto
  have "isum (λa. f1 a + f2 a) A =
    Sup {a1 + a2 | a1 a2. a1 ∈ ?S ∧ a2 ∈ ?T}"
  proof (unfold isum_def, rule Sup_cong)
    show "sum (λa. f1 a + f2 a) ` {B |B. B ⊆ A ∧ finite B} ≠ {} ∨
      {a1 + a2 |a1 a2. a1 ∈ ?S ∧ a2 ∈ ?T} ≠ {}" by auto
    show "∀a ∈ sum (λa. f1 a + f2 a) ` {B |B. B ⊆ A ∧ finite B}.
      ∃b ∈ {a1 + a2 |a1 a2. a1 ∈ ?S ∧ a2 ∈ ?T}. a ≤ b"
    proof (intro ballI)
      fix a assume "a ∈ sum (λa. f1 a + f2 a) ` {B |B. B ⊆ A ∧ finite B}"
      then obtain B where hB: "B ⊆ A" "finite B" and ha: "a = sum (λa. f1 a + f2 a) B" by auto
      show "∃b ∈ {a1 + a2 |a1 a2. a1 ∈ ?S ∧ a2 ∈ ?T}. a ≤ b"
        using ha sum.distrib[of f1 f2 B] hB
        by (intro bexI[of _ "sum f1 B + sum f2 B"]) auto
    qed
    show "∀b ∈ {a1 + a2 |a1 a2. a1 ∈ ?S ∧ a2 ∈ ?T}.
      ∃a ∈ sum (λa. f1 a + f2 a) ` {B |B. B ⊆ A ∧ finite B}. b ≤ a"
    proof (intro ballI)
      fix b assume "b ∈ {a1 + a2 |a1 a2. a1 ∈ ?S ∧ a2 ∈ ?T}"
      then obtain B1 B2 where hB1: "B1 ⊆ A" "finite B1" and hB2: "B2 ⊆ A" "finite B2"
        and hb: "b = sum f1 B1 + sum f2 B2" by auto
      show "∃a ∈ sum (λa. f1 a + f2 a) ` {B |B. B ⊆ A ∧ finite B}. b ≤ a"
      proof (intro bexI[of _ "sum (λa. f1 a + f2 a) (B1 ∪ B2)"])
        have h1: "sum f1 B1 ≤ sum f1 (B1 ∪ B2)" using hB1 hB2 by (intro sum_mono2) auto
        have h2: "sum f2 B2 ≤ sum f2 (B1 ∪ B2)" using hB1 hB2 by (intro sum_mono2) auto
        show "b ≤ sum (λa. f1 a + f2 a) (B1 ∪ B2)"
          using hb h1 h2 sum.distrib[of f1 f2 "B1 ∪ B2"] by (simp add: add_mono)
        show "sum (λa. f1 a + f2 a) (B1 ∪ B2) ∈ sum (λa. f1 a + f2 a) ` {B |B. B ⊆ A ∧ finite B}"
          using hB1 hB2 by auto
      qed
    qed
  qed
  also have "... = Sup ?S + Sup ?T"
    by (subst plus_Sup_commute'[symmetric, OF hS hT]) simp
  finally show ?thesis unfolding isum_def .
qed

end