Theory Card_Partial_Equiv_Relations
section ‹Cardinality of Partial Equivalence Relations›
theory Card_Partial_Equiv_Relations
imports
Card_Equiv_Relations
begin
subsection ‹Definition of Partial Equivalence Relation›
definition partial_equiv :: "'a set ⇒ ('a × 'a) set ⇒ bool"
where
"partial_equiv A R = (R ⊆ A × A ∧ sym R ∧ trans R)"
lemma partial_equivI:
assumes "R ⊆ A × A" "sym R" "trans R"
shows "partial_equiv A R"
using assms unfolding partial_equiv_def by auto
lemma partial_equiv_iff:
shows "partial_equiv A R ⟷ (∃A' ⊆ A. equiv A' R)"
proof
assume "partial_equiv A R"
from ‹partial_equiv A R› have "R `` A ⊆ A"
unfolding partial_equiv_def by blast
moreover have "equiv (R `` A) R"
proof (rule equivI)
from ‹partial_equiv A R› show "sym R"
unfolding partial_equiv_def by blast
from ‹partial_equiv A R› show "trans R"
unfolding partial_equiv_def by blast
show "refl_on (R `` A) R"
proof (rule refl_onI)
show "R ⊆ R `` A × R `` A"
proof
fix p
assume "p ∈ R"
obtain x y where "p = (x, y)" by fastforce
moreover have "x ∈ R `` A"
using ‹p ∈ R› ‹p = (x, y)› ‹partial_equiv A R›
partial_equiv_def sym_def by fastforce
moreover have "y ∈ R `` A"
using ‹p ∈ R› ‹p = (x, y)› ‹R `` A ⊆ A› ‹x ∈ R `` A› by blast
ultimately show "p ∈ R `` A × R `` A" by auto
qed
next
fix y
assume "y ∈ R `` A"
from this obtain x where "(x, y) ∈ R" by auto
from ‹(x, y) ∈ R› have "(y, x) ∈ R"
using ‹sym R› by (meson symE)
from ‹(x, y) ∈ R› ‹(y, x) ∈ R› show "(y, y) ∈ R"
using ‹trans R› by (meson transE)
qed
qed
ultimately show "∃A'⊆A. equiv A' R" by blast
next
assume "∃A'⊆A. equiv A' R"
from this obtain A' where "A' ⊆ A" and "equiv A' R" by blast
show "partial_equiv A R"
proof (rule partial_equivI)
from ‹equiv A' R› ‹A' ⊆ A› show "R ⊆ A × A"
using equiv_class_eq_iff by fastforce
from ‹equiv A' R› show "sym R"
using equivE by blast
from ‹equiv A' R› show "trans R"
using equivE by blast
qed
qed
subsection ‹Construction of all Partial Equivalence Relations for a Given Set›
definition all_partial_equivs_on :: "'a set ⇒ (('a × 'a) set) set"
where
"all_partial_equivs_on A =
do {
k ← {0..card A};
A' ← {A'. A' ⊆ A ∧ card A' = k};
{R. equiv A' R}
}"
lemma all_partial_equivs_on:
assumes "finite A"
shows "all_partial_equivs_on A = {R. partial_equiv A R}"
proof
show "all_partial_equivs_on A ⊆ {R. partial_equiv A R}"
proof
fix R
assume "R ∈ all_partial_equivs_on A"
from this obtain A' where "A' ⊆ A" and "equiv A' R"
unfolding all_partial_equivs_on_def by auto
from this have "partial_equiv A R"
using partial_equiv_iff by blast
from this show "R ∈ {R. partial_equiv A R}" ..
qed
next
show "{R. partial_equiv A R} ⊆ all_partial_equivs_on A"
proof
fix R
assume "R ∈ {R. partial_equiv A R}"
from this obtain A' where "A' ⊆ A" and "equiv A' R"
using partial_equiv_iff by (metis mem_Collect_eq)
moreover have "card A' ∈ {0..card A}"
using ‹A' ⊆ A› ‹finite A› by (simp add: card_mono)
ultimately show "R ∈ all_partial_equivs_on A"
unfolding all_partial_equivs_on_def
by (auto simp del: atLeastAtMost_iff)
qed
qed
subsection ‹Injectivity of the Set Construction›
lemma equiv_inject:
assumes "equiv A R" "equiv B R"
shows "A = B"
proof -
from assms have "R ⊆ A × A" "R ⊆ B × B" by (simp add: equiv_type)+
moreover from assms have "∀x∈A. (x, x) ∈ R" "∀x∈B. (x, x) ∈ R"
by (simp add: eq_equiv_class)+
ultimately show ?thesis
using mem_Sigma_iff subset_antisym subset_eq by blast
qed
lemma injectivity:
assumes "(A' ⊆ A ∧ card A' = k) ∧ (A'' ⊆ A ∧ card A'' = k')"
assumes "equiv A' R ∧ equiv A'' R'"
assumes "R = R'"
shows "A' = A''" "k = k'"
proof -
from ‹R = R'› assms(2) show "A' = A''"
using equiv_inject by fast
from this assms(1) show "k = k'" by simp
qed
subsection ‹Cardinality Theorem of Partial Equivalence Relations›
theorem card_partial_equiv:
assumes "finite A"
shows "card {R. partial_equiv A R} = Bell (card A + 1)"
proof -
let ?expr = "do {
k ← {0..card A};
A' ← {A'. A' ⊆ A ∧ card A' = k};
{R. equiv A' R}
}"
have "card {R. partial_equiv A R} = card (all_partial_equivs_on A)"
using ‹finite A› by (simp add: all_partial_equivs_on)
also have "card (all_partial_equivs_on A) = card ?expr"
unfolding all_partial_equivs_on_def ..
also have "card ?expr = (∑k = 0..card A. (card A choose k) * Bell k)"
proof -
let "?S ⤜ ?comp" = ?expr
{
fix k
assume k: "k ∈ {..card A}"
let ?expr = "?comp k"
let "?S ⤜ ?comp" = ?expr
have "finite ?S" using ‹finite A› by simp
moreover {
fix A'
assume A': "A' ∈ {A'. A' ⊆ A ∧ card A' = k}"
from this have "A' ⊆ A" and "card A' = k" by auto
let ?expr = "?comp A'"
have "finite A'"
using ‹finite A› ‹A' ⊆ A› by (simp add: finite_subset)
have "card ?expr = Bell k"
using ‹finite A› ‹finite A'› ‹A' ⊆ A› ‹card A' = k›
by (simp add: card_equiv_rel_eq_Bell)
moreover have "finite ?expr"
using ‹finite A'› by (simp add: finite_equiv)
ultimately have "finite ?expr ∧ card ?expr = Bell k" by blast
} note inner = this
moreover have "disjoint_family_on ?comp ?S"
by (injectivity_solver rule: injectivity(1))
moreover have "card ?S = card A choose k"
using ‹finite A› by (simp add: n_subsets)
ultimately have "card ?expr = (card A choose k) * Bell k" (is "_ = ?formula")
by (subst card_bind_constant) auto
moreover have "finite ?expr"
using ‹finite ?S› inner by (auto intro!: finite_bind)
ultimately have "finite ?expr ∧ card ?expr = ?formula" by blast
}
moreover have "finite ?S" by simp
moreover have "disjoint_family_on ?comp ?S"
by (injectivity_solver rule: injectivity(2))
ultimately show "card ?expr = (∑k = 0..card A. (card A choose k) * Bell k)"
by (subst card_bind) auto
qed
also have "… = (∑k≤card A. (card A choose k) * Bell k)"
by (auto intro: sum.cong)
also have "… = Bell (card A + 1)"
using Bell_recursive_eq by simp
finally show ?thesis .
qed
end