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

section ‹Additions to Isabelle's Main Theories›

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
```