Theory Card_Number_Partitions.Additions_to_Main

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Additions to Isabelle's Main Theories›

theory Additions_to_Main
imports "HOL-Library.Multiset"
begin

subsection ‹Addition to Finite-Set Theory›

lemma bound_domain_and_range_impl_finitely_many_functions:
  "finite {f::nat⇒nat. (∀i. f i ≤ n) ∧ (∀i≥m. f i = 0)}"
proof (induct m)
  case 0
  have eq: "{f. (∀i. f i ≤ n) ∧ (∀i. f i = 0)} = {(λ_. 0)}" by auto
  from this show ?case by auto (subst eq; auto)
next
  case (Suc m)
  let ?S = "(λ(y, f). f(m := y)) ` ({0..n} × {f. (∀i. f i ≤ n) ∧ (∀i≥m. f i = 0)})"
  {
    fix g
    assume "∀i. g i ≤ n" "∀i≥Suc m. g i = 0"
    from this have "g ∈ ?S"
      by (auto intro: image_eqI[where x="(g m, g(m:=0))"])
  }
  from this have "{f. (∀i. f i ≤ n) ∧ (∀i≥Suc m. f i = 0)} = ?S" by auto
  from this Suc show ?case by simp
qed

subsection ‹Addition to Set-Interval Theory›

lemma sum_atMost_remove_nat:
  assumes "k ≤ (n :: nat)"
  shows "(∑i≤n. f i) = f k + (∑i∈{..n}-{k}. f i)"
using assms by (auto simp add: sum.remove[where x=k])

subsection ‹Additions to Multiset Theory›

lemma set_mset_Abs_multiset:
  assumes "finite {x. f x > 0}"
  shows "set_mset (Abs_multiset f) = {x. f x > 0}"
using assms unfolding set_mset_def by simp

lemma sum_mset_sum_count:
  "sum_mset M = (∑i∈set_mset M. count M i * i)"
proof (induct M)
  show "sum_mset {#} = (∑i∈set_mset {#}. count {#} i * i)" by simp
next
  fix M x
  assume hyp: "sum_mset M = (∑i∈set_mset M. count M i * i)"
  show "sum_mset (add_mset x M) = (∑i∈set_mset (add_mset x M). count (add_mset x M) i * i)"
  proof (cases "x ∈# M")
    assume a: "¬ x ∈# M"
    from this have "count M x = 0" by (meson count_inI)
    from ‹¬ x ∈# M› this hyp show ?thesis
      by (auto intro!: sum.cong)
  next
    assume "x ∈# M"
    have "sum_mset (add_mset x M) = (∑i∈set_mset M. count M i * i) + x"
      using hyp by simp
    also have "… = (∑i∈set_mset M - {x}. count M i * i) + count M x * x + x"
      using ‹x ∈# M› by (simp add: sum.remove[of _ x])
    also have "… = count (add_mset x M) x * x + (∑i∈set_mset (add_mset x M) - {x}. count (add_mset x M) i * i)"
      by simp
    also have "… = (∑i∈set_mset (add_mset x M). count (add_mset x M) i * i)"
      using ‹x ∈# M› by (simp add: sum.remove[of _ x])
    finally show ?thesis .
  qed
qed

lemma sum_mset_eq_sum_on_supersets:
  assumes "finite A" "set_mset M ⊆ A"
  shows "(∑i∈set_mset M. count M i * i) = (∑i∈A. count M i * i)"
proof -
  note ‹finite A› ‹set_mset M ⊆ A›
  moreover have "∀i∈A - set_mset M. count M i * i = 0"
    using count_inI by fastforce
  ultimately show ?thesis
    by (auto intro: sum.mono_neutral_cong_left)
qed

end