Email Gateway (Jan 17 2021 at 23:23): Email Gateway (Jan 17 2021 at 23:23):From: Jakub Kądziołka <kuba@kadziolka.net>
Good evening,
I have proven some lemmas that would probably fit into the Isabelle
distribution - a lower bound on the size of a set of natural numbers,
and a summation formula that counts how many times each value occurs.
By the way, I seem to be submitting mails like these somewhat often
lately; please let me know if I should be doing something to make this
more manageable.
Regards,
Jakub Kądziołka
lemma max_ge_card: "finite S ⟹ Suc (Max S) ≥ card S"
proof (rule classical)
assume "finite S" and "¬ Suc (Max S) ≥ card S"
then have "Suc (Max S) < card S"
by simp
with finite S have "S ⊆ {0..Max S}"
by auto
hence "card S ≤ card {0..Max S}"
by (intro card_mono; auto)
thus "card S ≤ Suc (Max S)"
by simp
qed
lemma nat_sum_ge_card_sum:
shows "∑ {0..<card S} ≤ ∑ S"
proof (cases "finite S")
case True
then show ?thesis
proof (induction "card S" arbitrary: S)
case (Suc x)
then have "Max S ≥ x" using max_ge_card by fastforce
let ?S' = "S - {Max S}"
from Suc have "Max S ∈ S" by (auto intro: Max_in)
hence cards: "card S = Suc (card ?S')"
using finite S by (intro card.remove; auto)
hence "∑ {0..<card ?S'} ≤ ∑ ?S'"
using Suc by (intro Suc; auto)
hence "∑ {0..<card ?S'} + x ≤ ∑ ?S' + Max S"
using Max S ≥ x by simp
also have "... = ∑ S"
using sum.remove[OF finite S Max S ∈ S, where g="λx. x"]
by simp
finally show ?case
using cards Suc by auto
qed simp
qed simp
lemma sum_count:
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"
(is "?rest = 0")
proof -
{
fix y
assume "y ∈ R - g S"
then have *: "?cls y = {}"
by auto
have "of_nat (card (?cls y)) * f y = 0"
unfolding * by simp
}
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 ‹g S ⊆ R› ‹finite R›])
finally show ?thesis
by (simp add: eq_commute)
qed
Email Gateway (Jan 19 2021 at 10:30):From: Tobias Nipkow <nipkow@in.tum.de>
Thank you for your contributions, they will be added shortly.
Yes, the process of submitting contributions like yours needs to be improved.
Tobias
smime.p7s
Email Gateway (Jan 20 2021 at 12:51):From: Tobias Nipkow <nipkow@in.tum.de>
Jakub,
I added and renamed your lemmas:
http://isabelle.in.tum.de/repos/isabelle/rev/be9b73dfd3e0
Thanks
Tobias
smime.p7s
Last updated: Jul 15 2022 at 23:21 UTC