Theory Equivalence_Relation_Enumeration
section ‹Introduction›
theory Equivalence_Relation_Enumeration
imports "HOL-Library.Sublist" "HOL-Library.Disjoint_Sets"
"Card_Equiv_Relations.Card_Equiv_Relations"
begin
text ‹As mentioned in the abstract the enumeration algorithm relies on the bijection between
restricted growth functions (RGFs) of length @{term "n"} and the equivalence relations on
@{term "{..<n}"}, where the bijection is the operation that forms the equivalence kernels of an RGF.
The method is being dicussed, for example, by~\<^cite>‹"hutchinson1963" and "milne1977"› or
\<^cite>‹‹\textsection 1.5› in "white1986"›.
An enumeration algorithm for RGFs is less convoluted than one for equivalence relations or
partitions and the representation has the advantage that checking whether a pair of elements are
equivalent can be done by performing two list lookup operations.
After a few preliminary results in the following section, Section~\ref{sec:enum_rgf} introduces the
enumeration algorithm for RGFs and shows that the function enumerates all of them (for the given
length) without repetition. Section~\ref{sec:bij_kernel} shows that the operation of forming the
equivalence kernel is a bijection and concludes with the correctness of the entire algorithm. In
Section~\ref{sec:app} an interesting application is being discussed, where the enumeration of
partitions is applied within a proof. Section~\ref{sec:add} contains a few additional results,
such as the fact that the length of the enumerated list is a Bell number. The latter result relies
on the formalization of the cardinality of equivalence relations by
Bulwahn~\<^cite>‹"Card_Equiv_Relations-AFP"›.›
section ‹Preliminary Results›
text ‹This section contains a few preliminary results used in the proofs below.›
lemma length_filter:"length (filter p xs) = sum_list (map (λx. of_bool ( p x)) xs)"
by (induct xs, simp_all)
lemma count_list_expand:"count_list xs x = length (filter ((=) x) xs)"
by (induct xs, simp_all)
text ‹An induction schema (similar to @{thm [source] list_induct2} and @{thm [source] rev_induct})
for two lists of equal length, where induction step is shown appending elements at the end.›
lemma list_induct_2_rev[consumes 1, case_names Nil Cons]:
assumes "length x = length y"
assumes "P [] []"
assumes "⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs@[x]) (ys@[y])"
shows "P x y"
using assms(1)
proof (induct "length x" arbitrary: x y)
case 0
then show ?case using assms(2) by simp
next
case (Suc n)
obtain x1 x2 where a:"x = x1@[x2]" and c:"length x1 = n"
by (metis Suc(2) append_butlast_last_id length_append_singleton
length_greater_0_conv nat.inject zero_less_Suc)
obtain y1 y2 where b:"y = y1@[y2]" and d:"length y1 = n"
by (metis Suc(2,3) append_butlast_last_id length_append_singleton
length_greater_0_conv nat.inject zero_less_Suc)
have "P x1 y1" using c d Suc by simp
hence "P (x1@[x2]) (y1@[y2])" using assms(3) c d by simp
thus ?case using a b by simp
qed
text ‹If all but one value of a sum is zero then it can be evaluated on the remaining point:›
lemma sum_collapse:
fixes f :: "'a ⇒ 'b::{comm_monoid_add}"
assumes "finite A"
assumes "z ∈ A"
assumes "⋀y. y ∈ A ⟹ y ≠ z ⟹ f y = 0"
shows "sum f A = f z"
using sum.union_disjoint[where A="A-{z}" and B="{z}" and g="f"]
by (simp add: assms sum.insert_if)
text ‹Number of occurrences of elements in lists is preserved under injective maps.›
lemma count_list_inj_map:
assumes "inj_on f (set x)"
assumes "y ∈ set x"
shows "count_list (map f x) (f y) = count_list x y"
using assms by (induction x, simp_all, fastforce)
text ‹A relation cannot be an equivalence relation on two distinct sets.›
lemma equiv_on_unique:
assumes "equiv A p"
assumes "equiv B p"
shows "A = B"
by (meson assms equalityI equiv_class_eq_iff subsetI)
text ‹The restriction of an equivalence relation is itself an equivalence relation.›
lemma equiv_subset:
assumes "B ⊆ A"
assumes "equiv A p"
shows "equiv B (Restr p B)"
proof -
have "refl_on B (Restr p B)" using assms by (simp add:refl_on_def equiv_def, blast)
moreover have "sym (Restr p B)" using assms by (simp add:sym_def equiv_def)
moreover have "trans (Restr p B)"
using assms by (simp add:trans_def equiv_def, blast)
ultimately show ?thesis by (simp add:equiv_def)
qed
section ‹Enumerating Restricted Growth Functions\label{sec:enum_rgf}›
fun rgf_limit :: "nat list ⇒ nat"
where
"rgf_limit [] = 0" |
"rgf_limit (x#xs) = max (x+1) (rgf_limit xs)"
lemma rgf_limit_snoc: "rgf_limit (x@[y]) = max (y+1) (rgf_limit x)"
by (induction x, simp_all)
lemma rgf_limit_ge: "y ∈ set xs ⟹ y < rgf_limit xs"
by (induction xs, simp_all, metis lessI max_less_iff_conj not_less_eq)
definition rgf :: "nat list ⇒ bool"
where "rgf x = (∀ys y. prefix (ys@[y]) x ⟶ y ≤ rgf_limit ys)"
text ‹The function @{term "rgf_limit"} returns the smallest natural number larger than all list
elements, it is the largest allowed value following @{term "xs"} for restricted growth functions.
The definition @{term "rgf"} is the predicate capturing the notion.›
fun enum_rgfs :: "nat ⇒ (nat list) list"
where
"enum_rgfs 0 = [[]]" |
"enum_rgfs (Suc n) = [(x@[y]). x ← enum_rgfs n, y ← [0..<rgf_limit x+1]]"
text ‹The function @{term "enum_rgfs n"} returns all RGFs of length @{term "n"} without repetition.
The fact is verified in the three lemmas at the end of this section.›
lemma rgf_snoc:
"rgf (xs@[x]) ⟷ rgf xs ∧ x < rgf_limit xs + 1"
unfolding rgf_def by (rule order_antisym, (simp add:less_Suc_eq_le)+)
lemma rgf_imp_initial_segment:
"rgf xs ⟹ set xs = {..<rgf_limit xs}"
proof (induction xs rule:rev_induct)
case Nil
then show ?case by simp
next
case (snoc x xs)
have c:"rgf xs" using snoc(2) rgf_snoc by simp
hence a:"set xs = {..<rgf_limit xs}" using snoc(1) by simp
have b: "x ≤ rgf_limit xs" using snoc(2) rgf_snoc c by simp
have "set (xs@[x]) = insert x {..<rgf_limit xs}"
using a by simp
also have "... = {..<max (x+1) (rgf_limit xs)}" using b
by (cases "x < rgf_limit xs", simp add:insert_absorb, simp add:lessThan_Suc)
also have "... = {..<rgf_limit (xs@[x])}"
using rgf_limit_snoc by simp
finally show ?case by simp
qed
lemma enum_rgfs_returns_rgfs:
assumes "x ∈ set (enum_rgfs n)"
shows "rgf x"
using assms
proof (induction n arbitrary: x)
case 0
then show ?case by (simp add:rgf_def)
next
case (Suc n)
obtain x1 x2 where
x_def:"x = x1@[x2]" "x2 < rgf_limit x1 + 1" "x1 ∈ set (enum_rgfs n)"
using Suc by (simp add:image_iff, force)
have a:"rgf x1" using Suc x_def by blast
thus ?case using x_def by (simp add:rgf_snoc)
qed
lemma enum_rgfs_len:
assumes "x ∈ set (enum_rgfs n)"
shows "length x = n"
using assms by (induction n arbitrary: x, simp_all, fastforce)
lemma equiv_rels_enum:
assumes "rgf x"
shows "count_list (enum_rgfs (length x)) x = 1"
using assms
proof (induction x rule:rev_induct)
case Nil
then show ?case by simp
next
case (snoc x xs)
have b:"rgf xs" using snoc(2) rgf_def by simp
hence "x < rgf_limit xs + 1" using rgf_snoc snoc by blast
hence a:"card ({0..<rgf_limit xs + 1} ∩ {x}) = 1" by force
have "1 = count_list (enum_rgfs (length xs)) xs" using snoc b by simp
also have "... = (∑r1←enum_rgfs (length xs). of_bool (xs = r1) *
card ({0..<rgf_limit xs + 1} ∩ {x}))"
using a by (simp add:length_concat filter_concat count_list_expand length_filter)
also have "... = (∑r1←enum_rgfs (length xs). of_bool (xs = r1) *
card ({0..<rgf_limit r1 + 1} ∩ {x}))"
by (metis (mono_tags, opaque_lifting) mult_eq_0_iff of_bool_eq_0_iff)
also have "... = (∑r1←enum_rgfs (length xs). of_bool (xs = r1) *
(∑r2←[0..<rgf_limit r1 + 1]. of_bool (x = r2)))"
by (simp add:interv_sum_list_conv_sum_set_nat del:One_nat_def)
also have "... = length (filter ((=) (xs@[x])) (enum_rgfs (length (xs@[x]))))"
by (simp add:length_concat filter_concat length_filter comp_def
of_bool_conj sum_list_const_mult del:upt_Suc)
also have "... = count_list (enum_rgfs (length (xs@[x]))) (xs@[x])"
by (simp add:count_list_expand length_filter del:enum_rgfs.simps)
finally show ?case by presburger
qed
section ‹Enumerating Equivalence Relations\label{sec:bij_kernel}›
text ‹The following definition returns the equivalence relation induced by a list, for example, by
a restricted growth function.›
definition kernel_of :: "'a list ⇒ nat rel"
where "kernel_of xs = {(i,j). i < length xs ∧ j < length xs ∧ xs ! i = xs ! j}"
text ‹Using that the enumeration function for equivalence relations on @{term "{..<n}"} is
straight-forward to define:›
definition equiv_rels where "equiv_rels n = map kernel_of (enum_rgfs n)"
text ‹The following lemma shows that the image of
@{term "kernel_of"} is indeed an equivalence relation:›
lemma kernel_of_equiv: "equiv {..<length xs} (kernel_of xs)"
proof -
have "kernel_of xs ⊆ {..<length xs} × {..<length xs}"
by (rule subsetI, simp add:kernel_of_def mem_Times_iff case_prod_beta)
thus ?thesis by (simp add:equiv_def refl_on_def sym_def trans_def kernel_of_def)
qed
lemma kernel_of_eq_len:
assumes "kernel_of x = kernel_of y"
shows "length x = length y"
proof -
have "{..<length x} = {..<length y}"
by (metis kernel_of_equiv equiv_on_unique assms)
thus ?thesis by simp
qed
lemma kernel_of_eq:
"(kernel_of x = kernel_of y) ⟷
(length x = length y ∧ (∀j < length x. ∀i < j. (x ! i = x ! j) = (y ! i = y ! j)))"
proof (cases "length x = length y")
case True
have "(kernel_of x = kernel_of y) ⟷
(∀j < length x. ∀i < length x. (x ! i = x ! j) = (y ! i = y ! j))"
unfolding set_eq_iff kernel_of_def using True by (simp, blast)
also have "... ⟷ (∀j < length x. ∀i < j. (x ! i = x ! j) = (y ! i = y ! j))"
by (metis (no_types, lifting) linorder_cases order.strict_trans)
finally show ?thesis using True by simp
next
case False
then show ?thesis using kernel_of_eq_len by blast
qed
lemma kernel_of_snoc:
"kernel_of (xs) = Restr (kernel_of (xs@[x])) {..<length xs}"
by (simp add:kernel_of_def nth_append set_eq_iff)
lemma kernel_of_inj_on_rgfs_aux:
assumes "length x = length y"
assumes "rgf x"
assumes "rgf y"
assumes "kernel_of x = kernel_of y"
shows "x = y"
using assms
proof (induct x y rule: list_induct_2_rev)
case Nil
then show ?case by simp
next
case (Cons x xs y ys)
have a:"kernel_of xs = kernel_of ys"
using Cons(1,5) kernel_of_snoc by metis
have d:"rgf xs" "rgf ys" using Cons rgf_def by auto
hence b:"xs = ys" using Cons(2) a by auto
have "⋀i. i < length xs ⟹ (xs ! i = x) = (ys ! i = y)"
proof -
fix i
assume i_l:"i < length xs"
have "(xs ! i = x) ⟷ (i,length xs) ∈ kernel_of (xs@[x])" using i_l
by (simp add:kernel_of_def less_Suc_eq nth_append)
also have "... ⟷ (i,length xs) ∈ kernel_of (ys@[y])"
using Cons(5) by simp
also have "... ⟷ (ys ! i= y)" using i_l Cons(1)
by (simp add:kernel_of_def less_Suc_eq nth_append)
finally show "(xs ! i = x) = (ys ! i = y)" by simp
qed
hence c:"(x ∈ set xs ⟶ x = y) ∧ (x ∉ set xs ⟶ y ∉ set ys)"
by (metis b in_set_conv_nth)
have x_bound:"x < rgf_limit xs + 1"
using Cons(3) rgf_snoc d by simp
have y_bound:"y < rgf_limit ys + 1"
using Cons(4) rgf_snoc d by simp
have "x = y" using b c d rgf_imp_initial_segment Cons x_bound y_bound
apply (cases "x < rgf_limit xs", simp)
by (cases "y < rgf_limit ys", simp+)
then show ?case using b by simp
qed
lemma kernel_of_inj_on_rgfs:
"inj_on kernel_of {x. rgf x}"
by (rule inj_onI, simp, metis kernel_of_eq_len kernel_of_inj_on_rgfs_aux)
text ‹Applying an injective map to a list preserves the induced relation:›
lemma kernel_of_under_inj_map:
assumes "inj_on f (set x)"
shows "kernel_of x = kernel_of (map f x)"
proof -
have "⋀i j. i < length x ⟹ j < length x
⟹ (map f x) ! i = (map f x) ! j ⟹ x ! i = x ! j"
using assms by (simp add: inj_on_eq_iff)
thus ?thesis unfolding kernel_of_def by fastforce
qed
lemma all_rels_are_kernels:
assumes "equiv {..<n} p"
shows "∃(x :: nat set list). kernel_of x = p ∧ length x = n"
proof -
define r where "r = map (λk. p``{k}) [0..<n]"
have "⋀ u v. (u,v) ∈ kernel_of r ⟷ (u,v) ∈ p"
proof -
fix u v :: nat
have "(u,v) ∈ kernel_of r ⟷ ((u,v) ∈ {..<n}×{..<n} ∧ p``{u} = p``{v})"
unfolding kernel_of_def r_def by auto
also have "... ⟷ (u,v) ∈ p" by (metis assms equiv_class_eq_iff mem_Sigma_iff)
finally show "(u,v) ∈ kernel_of r ⟷ (u,v) ∈ p" by simp
qed
hence "kernel_of r = p" by auto
moreover have "length r = n" using r_def by simp
ultimately show ?thesis by auto
qed
text ‹For any list there is always an injective map on its set, such that its image is an RGF.›
lemma map_list_to_rgf:
"∃f. inj_on f (set x) ∧ rgf (map f x)"
proof (induction "length x" arbitrary: x)
case 0
then show ?case by (simp add:rgf_def)
next
case (Suc n)
obtain x1 x2 where x_def: "x = x1@[x2]" and l_x1: "length x1 = n"
by (metis append_butlast_last_id length_append_singleton Suc(2)
length_greater_0_conv nat.inject zero_less_Suc)
obtain f where inj_f: "inj_on f (set x1)" and pc_f: "rgf (map f x1)"
using Suc(1) l_x1 by blast
show ?case
proof (cases "x2 ∈ set x1")
case True
have a:"set x = set x1" using x_def True by auto
hence b:"inj_on f (set x)" using inj_f by auto
have "f x2 < rgf_limit (map f x1)" using rgf_limit_ge True by auto
hence "rgf (map f x)"
by (simp add:x_def rgf_snoc pc_f)
then show ?thesis using b by blast
next
case False
define f' where "f' = (λy. if y ∈ set x1 then f y else rgf_limit (map f x1))"
have "inj_on f' (set x1)" using f'_def inj_f by (simp add: inj_on_def)
moreover have "rgf_limit (map f x1) ∉ set (map f x1)"
using rgf_limit_ge by blast
hence "f' x2 ∉ f' ` set x1" using False by (simp add:f'_def)
ultimately have "inj_on f' (insert x2 (set x1))" using False by simp
hence a:"inj_on f' (set x)" using False x_def by simp
have b:"map f x1 = map f' x1" using f'_def by simp
have c:"f' x2 < Suc (rgf_limit (map f x1))" by (simp add:f'_def False)
have "rgf (map f' x)" by (simp add:x_def b[symmetric] rgf_snoc pc_f c)
then show ?thesis using a by blast
qed
qed
text ‹For any relation there is a corresponding RGF:›
lemma rgf_exists:
assumes "equiv {..<n} r"
shows "∃x. rgf x ∧ length x = n ∧ kernel_of x = r"
proof -
obtain y :: "nat set list" where a:"kernel_of y = r" "length y = n"
using all_rels_are_kernels assms by blast
then obtain f where b:"inj_on f (set y)" "rgf (map f y)"
using map_list_to_rgf by blast
have "kernel_of (map f y) = r"
using kernel_of_under_inj_map a b by blast
moreover have "length (map f y) = n" using a by simp
ultimately show ?thesis
using b by blast
qed
text ‹These are the main result of this entry: The function @{term "equiv_rels n"} enumerates the
equivalence relations on @{term "{..<n}"} without repetition.›
theorem equiv_rels_set:
assumes "x ∈ set (equiv_rels n)"
shows "equiv {..<n} x"
using assms equiv_rels_def kernel_of_equiv enum_rgfs_len by auto
theorem equiv_rels:
assumes "equiv {..<n} r"
shows "count_list (equiv_rels n) r = 1"
proof -
obtain y where y_def: "rgf y" "length y = n" "kernel_of y = r"
using rgf_exists assms by blast
have a: "⋀x. x ∈ set (enum_rgfs n) ⟹ (kernel_of y = kernel_of x) = (y=x)"
using enum_rgfs_returns_rgfs y_def(1,2) enum_rgfs_len inj_onD[OF kernel_of_inj_on_rgfs]
by auto
have "count_list (equiv_rels n) r =
length (filter (λx. r = kernel_of x) (enum_rgfs n))"
by (simp add:equiv_rels_def count_list_expand length_filter comp_def)
also have "... = length (filter (λx. kernel_of y = kernel_of x) (enum_rgfs n))"
using y_def(3) by simp
also have "... = length (filter (λx. y = x) (enum_rgfs n))"
using a by (simp cong:filter_cong)
also have "... = count_list (enum_rgfs n) y"
by (simp add:count_list_expand length_filter)
also have "... = 1"
using equiv_rels_enum y_def(1,2) by auto
finally show ?thesis by simp
qed
text ‹A corollary of the previous theorem is that the sum of the indicator function for a relation
over @{term "equiv_rels n"} is always one.›
corollary equiv_rels_2:
assumes "n = length xs"
shows "(∑x←equiv_rels n. of_bool (kernel_of xs = x)) = (1 :: 'a :: {semiring_1})"
proof -
have "length (filter (λx. kernel_of xs = x) (equiv_rels (length xs))) = 1"
using equiv_rels[OF kernel_of_equiv[where xs="xs"]] assms by (simp add:count_list_expand)
thus ?thesis
using assms by (simp add:of_bool_def sum_list_map_filter'[symmetric] sum_list_triv)
qed
section ‹Example Application\label{sec:app}›
text ‹In this section, I wanted to discuss an interesting application within the context of
a proof in Isabelle. This is motivated by a real-world example \<^cite>‹‹\textsection 2.2› in "alon1999"›,
where a function in a 4-times iterated sum could only be reduced by splitting it according to the
equivalence relation formed by the indices. The notepad below illustrates how this can be done
(in the case of 3 index variables).›
notepad
begin
fix f :: "nat × nat × nat ⇒ nat"
fix I :: "nat set"
assume a:"finite I"
text ‹To be able to break down such a sum by partitions let us introduce the function $P$
which is defined to be sum of an indicator function over all possible equivalence relations
its argument can form:›
define P :: "nat list ⇒ nat"
where "P = (λxs. (∑x ← equiv_rels (length xs). of_bool (kernel_of xs = x) ))"
text ‹Note that its value is always one, hence we can introduce it in an algebraic equation easily:›
have P_one: "⋀xs. P xs = 1"
by (simp add: P_def equiv_rels_2)
note unfold_equiv_rels = P_def equiv_rels_def numeral_eq_Suc kernel_of_eq
neq_commute All_less_Suc comp_def
define r where "r = (∑i ∈ I. (∑j ∈ I. (∑k ∈ I. f (i,j,k))))"
text ‹As a first step, we just introduce the factor @{term "P [i,j,k]"}.›
have "r = (∑i ∈ I. (∑j ∈ I. (∑k ∈ I. f (i,j,k) * P [i,j,k])))"
by (simp add:P_one r_def cong:sum.cong)
text ‹By expanding the definition of P and distributing, the sum can be expanded into 5 sums
each representing a distinct equivalence relation formed by the indices.›
also have "... =
(∑i∈I. f (i, i, i)) +
(∑i∈I. ∑j∈I. f (i, i, j) * of_bool (i ≠ j)) +
(∑i∈I. ∑j∈I. f (i, j, i) * of_bool (i ≠ j)) +
(∑i∈I. ∑j∈I. f (i, j, j) * of_bool (i ≠ j)) +
(∑i∈I. ∑j∈I. ∑k∈I. f (i, j, k) * of_bool (j ≠ k ∧ i ≠ k ∧ i ≠ j))"
(is "_ = ?rhs")
by (simp add:unfold_equiv_rels sum.distrib distrib_left sum_collapse[OF a])
finally have "r = ?rhs" by simp
end
section ‹Additional Results\label{sec:add}›
text ‹If two lists induce the same equivalence relation, then there is a bijection between the sets
that preserves the multiplicities of its elements.›
lemma kernel_of_eq_imp_bij:
assumes "kernel_of x = kernel_of y"
shows "∃f. bij_betw f (set x) (set y) ∧
(∀z ∈ set x. count_list x z = count_list y (f z))"
proof -
obtain x' where x'_def: "inj_on x' (set x)" "rgf (map x' x)"
using map_list_to_rgf by blast
obtain y' where y'_def: "inj_on y' (set y)" "rgf (map y' y)"
using map_list_to_rgf by blast
have "kernel_of (map x' x) = kernel_of (map y' y)"
using assms x'_def(1) y'_def(1)
by (simp add: kernel_of_under_inj_map[symmetric])
hence b:"map x' x = map y' y"
using inj_onD[OF kernel_of_inj_on_rgfs] x'_def(2) y'_def(2) length_map by simp
hence f: "x' ` set x = y' ` set y"
by (metis list.set_map)
define f where "f = the_inv_into (set y) y' ∘ x'"
have g:"⋀z. z ∈ set x ⟹ count_list x z = count_list y (f z)"
proof -
fix z
assume a:"z ∈ set x"
have e: "x' z ∈ y' ` set y"
by (metis a b imageI image_set)
have c: "the_inv_into (set y) y' (x' z) ∈ set y"
using e the_inv_into_into[OF y'_def(1)] by simp
have d: "(y' (the_inv_into (set y) y' (x' z))) = x' z"
using e f_the_inv_into_f y'_def(1) by force
have "count_list x z = count_list (map x' x) (x' z)"
using a x'_def by (simp add: count_list_inj_map)
also have "... = count_list (map y' y) (x' z)"
by (simp add:b)
also have "... = count_list (map y' y) (y' (the_inv_into (set y) y' (x' z)))"
by (simp add:d)
also have "... = count_list y (the_inv_into (set y) y' (x' z))"
using c count_list_inj_map[OF y'_def(1)] by simp
also have "... = count_list y (f z)" by (simp add:f_def)
finally show "count_list x z = count_list y (f z)" by simp
qed
have "bij_betw x' (set x) (x' ` set x)"
using x'_def(1) bij_betw_imageI by auto
moreover have "bij_betw (the_inv_into (set y) y') (y' ` set y) (set y)"
using bij_betw_the_inv_into[OF bij_betw_imageI] y'_def(1) by auto
hence "bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)"
using f by simp
ultimately have "bij_betw f (set x) (set y)"
using bij_betw_trans f_def by blast
thus ?thesis using g by blast
qed
text ‹As expected the length of @{term "equiv_rels n"} is the $n$-th Bell number.›
lemma len_equiv_rels: "length (equiv_rels n) = Bell n"
proof -
have a:"finite {p. equiv {..<n} p}"
by (simp add: finite_equiv)
have b: "set (equiv_rels n) ⊆ {p. equiv {..<n} p}"
using equiv_rels_set by blast
have "length (equiv_rels n) =
(∑x ∈ {p. equiv {..<n} p}. count_list (equiv_rels n) x)"
using a b by (simp add:sum_count_set)
also have "... = card {p. equiv {..<n} p}"
by (simp add: equiv_rels)
also have "... = Bell (card {..<n})"
using card_equiv_rel_eq_Bell by blast
also have "... = Bell n" by simp
finally show ?thesis by simp
qed
text ‹Instead of forming an equivalence relation from a list, it is also possible to induce a
partition from it:›
definition induced_par :: "'a list ⇒ nat set set" where
"induced_par xs = (λk. {i. i < length xs ∧ xs ! i = k}) ` (set xs)"
text ‹The following lemma verifies the commutative diagram, i.e.,
@{term "induced_par xs"} is the same partition as the quotient of @{term "{..<length xs}"} over
the corresponding equivalence relation.›
lemma quotient_of_kernel_is_induced_par:
"{..<length xs} // (kernel_of xs) = (induced_par xs)"
proof (rule set_eqI)
fix x
have "x ∈ {..<length xs} // (kernel_of xs) ⟷
(∃i < length xs. x = {j. j < length xs ∧ xs ! i = xs ! j})"
unfolding quotient_def kernel_of_def by blast
also have "... ⟷ (∃y ∈ set xs. x = {j. j < length xs ∧ y = xs ! j})"
unfolding in_set_conv_nth Bex_def by (rule order_antisym, force+)
also have "... ⟷ (x ∈ induced_par xs)"
unfolding induced_par_def by auto
finally show "x ∈ {..<length xs} // (kernel_of xs) ⟷ (x ∈ induced_par xs)"
by simp
qed
end