Theory 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::natnat. (i. f i  n)  (im. 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)  (im. f i = 0)})"
  {
    fix g
    assume "i. g i  n" "iSuc 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)  (iSuc 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 "(in. 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 = (iset_mset M. count M i * i)"
proof (induct M)
  show "sum_mset {#} = (iset_mset {#}. count {#} i * i)" by simp
next
  fix M x
  assume hyp: "sum_mset M = (iset_mset M. count M i * i)"
  show "sum_mset (add_mset x M) = (iset_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) = (iset_mset M. count M i * i) + x"
      using hyp by simp
    also have " = (iset_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 + (iset_mset (add_mset x M) - {x}. count (add_mset x M) i * i)"
      by simp
    also have " = (iset_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 "(iset_mset M. count M i * i) = (iA. count M i * i)"
proof -
  note finite A set_mset M  A
  moreover have "iA - 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