# Theory Card_Partitions.Set_Partition

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

section ‹Set Partitions›

theory Set_Partition
imports
"HOL-Library.Disjoint_Sets"
"HOL-Library.FuncSet"
begin

subsection ‹Useful Additions to Main Theories›

lemma set_eqI':
assumes "⋀x. x ∈ A ⟹ x ∈ B"
assumes "⋀x. x ∈ B ⟹ x ∈ A"
shows "A = B"
using assms by auto

lemma comp_image:
"((`) f ∘ (`) g) = (`) (f o g)"
by rule auto

subsection ‹Introduction and Elimination Rules›

text ‹The definition of @{const partition_on} is in @{theory "HOL-Library.Disjoint_Sets"}.›

(* TODO: move the following theorems to Disjoint Sets *)

lemma partition_onI:
assumes "⋀p. p ∈ P ⟹ p ≠ {}"
assumes "⋃P = A"
assumes "⋀p p'. p ∈ P ⟹ p' ∈ P ⟹ p ≠ p' ⟹ p ∩ p' = {}"
shows "partition_on A P"
using assms unfolding partition_on_def disjoint_def by blast

lemma partition_onE:
assumes "partition_on A P"
obtains "⋀p. p ∈ P ⟹ p ≠ {}"
"⋃P = A"
"⋀p p'. p ∈ P ⟹ p' ∈ P ⟹ p ≠ p' ⟹ p ∩ p' = {}"
using assms unfolding partition_on_def disjoint_def by blast

subsection ‹Basic Facts on Set Partitions›

lemma partition_onD4: "partition_on A P ⟹ p ∈ P ⟹ q ∈ P ⟹ x ∈ p ⟹ x ∈ q ⟹ p = q"
by (auto simp: partition_on_def disjoint_def)

lemma partition_subset_imp_notin:
assumes "partition_on A P" "X ∈ P"
assumes "X' ⊂ X"
shows "X' ∉ P"
proof
assume "X' ∈ P"
from ‹X' ∈ P› ‹partition_on A P› have "X' ≠ {}"
using partition_onD3 by blast
moreover from ‹X' ∈ P› ‹X ∈ P› ‹partition_on A P› ‹X' ⊂ X› have "disjnt X X'"
by (metis disjnt_def disjointD inf.strict_order_iff partition_onD2)
moreover note ‹X' ⊂ X›
ultimately show False
by (meson all_not_in_conv disjnt_iff psubsetD)
qed

lemma partition_on_Diff:
assumes P: "partition_on A P" shows "Q ⊆ P ⟹ partition_on (A - ⋃Q) (P - Q)"
using P P[THEN partition_onD4] by (auto simp: partition_on_def disjoint_def)

lemma partition_on_UN:
assumes A: "partition_on A B" and B: "⋀b. b ∈ B ⟹ partition_on b (P b)"
shows "partition_on A (⋃b∈B. P b)"
proof (rule partition_onI)
show "⋃(⋃b∈B. P b) = A"
using B[THEN partition_onD1] A[THEN partition_onD1] by blast
next
show "p ≠ {}" if "p ∈ (⋃b∈B. P b)" for p
using B[THEN partition_onD3] that by auto
next
fix p q assume "p ∈ (⋃i∈B. P i)" "q ∈ (⋃i∈B. P i)" and "p ≠ q"
then obtain i j where i: "p ∈ P i" "i ∈ B" and j: "q ∈ P j" "j ∈ B"
by auto
show "p ∩ q = {}"
proof cases
assume "i = j" then show ?thesis
using i j ‹p ≠ q› B[THEN partition_onD2, of i] by (simp add: disjointD)
next
assume "i ≠ j"
then have "disjnt i j"
using i j A[THEN partition_onD2] by (auto simp: pairwise_def)
moreover have "p ⊆ i" "q ⊆ j"
using B[THEN partition_onD1, of i, symmetric] B[THEN partition_onD1, of j, symmetric] i j by auto
ultimately show ?thesis
by (auto simp: disjnt_def)
qed
qed

lemma partition_on_notemptyI:
assumes "partition_on A P"
assumes "A ≠ {}"
shows "P ≠ {}"
using assms by (auto elim: partition_onE)

lemma partition_on_disjoint:
assumes "partition_on A P"
assumes "partition_on B Q"
assumes "A ∩ B = {}"
shows "P ∩ Q = {}"
using assms by (fastforce elim: partition_onE)

lemma partition_on_eq_implies_eq_carrier:
assumes "partition_on A Q"
assumes "partition_on B Q"
shows "A = B"
using assms by (fastforce elim: partition_onE)

lemma partition_on_insert:
assumes "partition_on A P"
assumes "disjnt A X" "X ≠ {}"
assumes "A ∪ X = A'"
shows "partition_on A' (insert X P)"
using assms by (auto simp: partition_on_def disjoint_def disjnt_def)

text ‹An alternative formulation of @{thm partition_on_insert}›
lemma partition_on_insert':
assumes "partition_on (A - X) P"
assumes "X ⊆ A" "X ≠ {}"
shows "partition_on A (insert X P)"
proof -
have "disjnt (A - X) X" by (simp add: disjnt_iff)
from assms(1) this assms(3) have "partition_on ((A - X) ∪ X) (insert X P)"
by (auto intro: partition_on_insert)
from this ‹X ⊆ A› show ?thesis
by (metis Diff_partition sup_commute)
qed

lemma partition_on_insert_singleton:
assumes "partition_on A P" "a ∉ A" "insert a A = A'"
shows "partition_on A' (insert {a} P)"
using assms by (auto simp: partition_on_def disjoint_def disjnt_def)

lemma partition_on_remove_singleton:
assumes "partition_on A P" "X ∈ P" "A - X = A'"
shows "partition_on A' (P - {X})"
using assms partition_on_Diff by (metis Diff_cancel Diff_subset cSup_singleton insert_subset)

subsection ‹The Unique Part Containing an Element in a Set Partition›

lemma partition_on_partition_on_unique:
assumes "partition_on A P"
assumes "x ∈ A"
shows "∃!X. x ∈ X ∧ X ∈ P"
proof -
from ‹partition_on A P› have "⋃P = A"
by (auto elim: partition_onE)
from this ‹x ∈ A› obtain X where X: "x ∈ X ∧ X ∈ P" by blast
{
fix Y
assume "x ∈ Y ∧ Y ∈ P"
from this have "X = Y"
using X ‹partition_on A P› by (meson partition_onE disjoint_iff_not_equal)
}
from this X show ?thesis by auto
qed

lemma partition_on_the_part_mem:
assumes "partition_on A P"
assumes "x ∈ A"
shows "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
proof -
from ‹x ∈ A› have "∃!X. x ∈ X ∧ X ∈ P"
using ‹partition_on A P› by (simp add: partition_on_partition_on_unique)
from this show "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
by (metis (no_types, lifting) theI)
qed

lemma partition_on_in_the_unique_part:
assumes "partition_on A P"
assumes "x ∈ A"
shows "x ∈ (THE X. x ∈ X ∧ X ∈ P)"
proof -
from assms have "∃!X. x ∈ X ∧ X ∈ P"
from this show ?thesis
by (metis (mono_tags, lifting) theI')
qed

lemma partition_on_the_part_eq:
assumes "partition_on A P"
assumes "x ∈ X" "X ∈ P"
shows "(THE X. x ∈ X ∧ X ∈ P) = X"
proof -
from ‹x ∈ X› ‹X ∈ P› have "x ∈ A"
using ‹partition_on A P› by (auto elim: partition_onE)
from this have "∃!X. x ∈ X ∧ X ∈ P"
using ‹partition_on A P› by (simp add: partition_on_partition_on_unique)
from ‹x ∈ X› ‹X ∈ P› this show "(THE X. x ∈ X ∧ X ∈ P) = X"
by (auto intro!: the1_equality)
qed

lemma the_unique_part_alternative_def:
assumes "partition_on A P"
assumes "x ∈ A"
shows "(THE X. x ∈ X ∧ X ∈ P) = {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
proof
show "(THE X. x ∈ X ∧ X ∈ P) ⊆ {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
proof
fix y
assume "y ∈ (THE X. x ∈ X ∧ X ∈ P)"
moreover from ‹x ∈ A› have "x ∈ (THE X. x ∈ X ∧ X ∈ P)"
using ‹partition_on A P› partition_on_in_the_unique_part by force
moreover from ‹x ∈ A› have "(THE X. x ∈ X ∧ X ∈ P) ∈ P"
using ‹partition_on A P› partition_on_the_part_mem by force
ultimately show "y ∈ {y. ∃X∈P. x ∈ X ∧ y ∈ X}" by auto
qed
next
show "{y. ∃X∈P. x ∈ X ∧ y ∈ X} ⊆ (THE X. x ∈ X ∧ X ∈ P)"
proof
fix y
assume "y ∈ {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
from this obtain X where "x ∈ X" and "y ∈ X" and "X ∈ P" by auto
from ‹x ∈ X› ‹X ∈ P› have "(THE X. x ∈ X ∧ X ∈ P) = X"
using ‹partition_on A P› partition_on_the_part_eq by force
from this ‹y ∈ X› show "y ∈ (THE X. x ∈ X ∧ X ∈ P)" by simp
qed
qed

lemma partition_on_all_in_part_eq_part:
assumes "partition_on A P"
assumes "X' ∈ P"
shows "{x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'} = X'"
proof
show "{x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'} ⊆ X'"
using assms(1) partition_on_in_the_unique_part by force
next
show "X' ⊆ {x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'}"
proof
fix x
assume "x ∈ X'"
from ‹x ∈ X'› ‹X' ∈ P› have "x ∈ A"
using ‹partition_on A P› by (auto elim: partition_onE)
moreover from ‹x ∈ X'› ‹X' ∈ P› have "(THE X. x ∈ X ∧ X ∈ P) = X'"
using ‹partition_on A P› partition_on_the_part_eq by fastforce
ultimately show "x ∈ {x ∈ A. (THE X. x ∈ X ∧ X ∈ P) = X'}" by auto
qed
qed

lemma partition_on_part_characteristic:
assumes "partition_on A P"
assumes "X ∈ P" "x ∈ X"
shows "X = {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
proof -
from ‹x ∈ X› ‹X ∈ P› have "x ∈ A"
using ‹partition_on A P› partition_onE by blast
from  ‹x ∈ X› ‹X ∈ P› have "X = (THE X. x ∈ X ∧ X ∈ P)"
using ‹partition_on A P› by (simp add: partition_on_the_part_eq)
also from ‹x ∈ A› have "(THE X. x ∈ X ∧ X ∈ P) = {y. ∃X∈P. x ∈ X ∧ y ∈ X}"
using ‹partition_on A P› the_unique_part_alternative_def by force
finally show ?thesis .
qed

lemma partition_on_no_partition_outside_carrier:
assumes "partition_on A P"
assumes "x ∉ A"
shows "{y. ∃X∈P. x ∈ X ∧ y ∈ X} = {}"
using assms unfolding partition_on_def by auto

subsection ‹Cardinality of Parts in a Set Partition›

lemma partition_on_le_set_elements:
assumes "finite A"
assumes "partition_on A P"
shows "card P ≤ card A"
using assms
proof (induct A arbitrary: P)
case empty
from this show "card P ≤ card {}" by (simp add: partition_on_empty)
next
case (insert a A)
show ?case
proof (cases "{a} ∈ P")
case True
have prop_partition_on: "∀p∈P. p ≠ {}" "⋃P = insert a A"
"∀p∈P. ∀p'∈P. p ≠ p' ⟶ p ∩ p' = {}"
using ‹partition_on (insert a A) P› by (fastforce elim: partition_onE)+
from this(2, 3) ‹a ∉ A› ‹{a} ∈ P› have A_eq: "A = ⋃(P - {{a}})"
by auto (metis Int_iff UnionI empty_iff insert_iff)
from prop_partition_on A_eq have partition_on: "partition_on A (P - {{a}})"
by (intro partition_onI) auto
from insert.hyps(3) this have "card (P - {{a}}) ≤ card A" by simp
from this insert(1, 2, 4) ‹{a} ∈ P› show ?thesis
using finite_elements[OF ‹finite A› partition_on] by simp
next
case False
from ‹partition_on (insert a A) P› obtain p where p_def: "p ∈ P" "a ∈ p"
by (blast elim: partition_onE)
from ‹partition_on (insert a A) P› p_def have a_notmem: "∀p'∈ P - {p}. a ∉ p'"
by (blast elim: partition_onE)
from ‹partition_on (insert a A) P› p_def have "p - {a} ∉ P"
unfolding partition_on_def disjoint_def
by (metis Diff_insert_absorb Diff_subset inf.orderE mk_disjoint_insert)
let ?P' = "insert (p - {a}) (P - {p})"
have "partition_on A ?P'"
proof (rule partition_onI)
from ‹partition_on (insert a A) P› have "∀p∈P. p ≠ {}" by (auto elim: partition_onE)
from this p_def ‹{a} ∉ P› show "⋀p'. p'∈insert (p - {a}) (P - {p}) ⟹ p' ≠ {}"
by (simp; metis (no_types) Diff_eq_empty_iff subset_singletonD)
next
from ‹partition_on (insert a A) P› have "⋃P = insert a A" by (auto elim: partition_onE)
from p_def this ‹a ∉ A› a_notmem show "⋃(insert (p - {a}) (P - {p})) = A" by auto
next
show "⋀pa pa'. pa∈insert (p - {a}) (P - {p}) ⟹ pa'∈insert (p - {a}) (P - {p}) ⟹ pa ≠ pa' ⟹ pa ∩ pa' = {}"
using ‹partition_on (insert a A) P› p_def a_notmem
unfolding partition_on_def disjoint_def
by (metis disjoint_iff_not_equal insert_Diff insert_iff)
qed
have "finite P" using ‹finite A› ‹partition_on A ?P'› finite_elements by fastforce
have "card P = Suc (card (P - {p}))"
using p_def ‹finite P› card.remove by fastforce
also have "… = card ?P'" using ‹p - {a} ∉ P› ‹finite P› by simp
also have "… ≤ card A" using ‹partition_on A ?P'› insert.hyps(3) by simp
also have "… ≤ card (insert a A)" by (simp add: card_insert_le ‹finite A› )
finally show ?thesis .
qed
qed

subsection ‹Operations on Set Partitions›

lemma partition_on_union:
assumes "A ∩ B = {}"
assumes "partition_on A P"
assumes "partition_on B Q"
shows "partition_on (A ∪ B) (P ∪ Q)"
proof (rule partition_onI)
fix X
assume "X ∈ P ∪ Q"
from this ‹partition_on A P› ‹partition_on B Q› show "X ≠ {}"
by (auto elim: partition_onE)
next
show "⋃(P ∪ Q) = A ∪ B"
using ‹partition_on A P› ‹partition_on B Q› by (auto elim: partition_onE)
next
fix X Y
assume "X ∈ P ∪ Q" "Y ∈ P ∪ Q" "X ≠ Y"
from this assms show "X ∩ Y = {}"
by (elim UnE partition_onE) auto
qed

lemma partition_on_split1:
assumes "partition_on A (P ∪ Q)"
shows "partition_on (⋃P) P"
proof (rule partition_onI)
fix p
assume "p ∈ P"
from this assms show "p ≠ {}"
using Un_iff partition_onE by auto
next
show "⋃P = ⋃P" ..
next
fix p p'
assume a: "p ∈ P" "p' ∈ P" "p ≠ p'"
from this assms show "p ∩ p' = {}"
using partition_onE subsetCE sup_ge1 by blast
qed

lemma partition_on_split2:
assumes "partition_on A (P ∪ Q)"
shows "partition_on (⋃Q) Q"
using assms partition_on_split1 sup_commute by metis

lemma partition_on_intersect_on_elements:
assumes "partition_on (A ∪ C) P"
assumes "∀X ∈ P. ∃x. x ∈ X ∩ C"
shows "partition_on C ((λX. X ∩ C) ` P)"
proof (rule partition_onI)
fix p
assume "p ∈ (λX. X ∩ C) ` P"
from this assms show "p ≠ {}" by auto
next
have "⋃P = A ∪ C"
using assms by (auto elim: partition_onE)
from this show "⋃((λX. X ∩ C) ` P) = C" by auto
next
fix p p'
assume "p ∈ (λX. X ∩ C) ` P" "p' ∈ (λX. X ∩ C) ` P" "p ≠ p'"
from this assms(1) show "p ∩ p' = {}"
by (blast elim: partition_onE)
qed

lemma partition_on_insert_elements:
assumes "A ∩ B = {}"
assumes "partition_on B P"
assumes "f ∈ A →⇩E P"
shows "partition_on (A ∪ B) ((λX. X ∪ {x ∈ A. f x = X}) ` P)" (is "partition_on _ ?P")
proof (rule partition_onI)
fix X
assume "X ∈ ?P"
from this ‹partition_on B P› show "X ≠ {}"
by (auto elim: partition_onE)
next
show "⋃?P = A ∪ B"
using ‹partition_on B P› ‹f ∈ A →⇩E P› by (auto elim: partition_onE)
next
fix X Y
assume "X ∈ ?P" "Y ∈ ?P" "X ≠ Y"
from ‹X ∈ ?P› obtain X' where X': "X = X' ∪ {x ∈ A. f x = X'}" "X' ∈ P" by auto
from ‹Y ∈ ?P› obtain Y' where Y': "Y = Y' ∪ {x ∈ A. f x = Y'}" "Y' ∈ P" by auto
from ‹X ≠ Y› X' Y' have "X' ≠ Y'" by auto
from this X' Y' have "X' ∩ Y' = {}"
using ‹partition_on B P› by (auto elim!: partition_onE)
from X' Y' have "X' ⊆ B" "Y' ⊆ B"
using ‹partition_on B P› by (auto elim!: partition_onE)
from this ‹X' ∩ Y' = {}› X' Y' ‹X' ≠ Y'› show "X ∩ Y = {}"
using ‹A ∩ B = {}› by auto
qed

lemma partition_on_map:
assumes "inj_on f A"
assumes "partition_on A P"
shows "partition_on (f ` A) ((`) f ` P)"
proof -
{
fix X Y
assume "X ∈ P" "Y ∈ P" "f ` X ≠ f ` Y"
moreover from assms have "∀p∈P. ∀p'∈P. p ≠ p' ⟶ p ∩ p' = {}" and "inj_on f (⋃P)"
by (auto elim!: partition_onE)
ultimately have "f ` X ∩ f ` Y = {}"
unfolding inj_on_def by auto (metis IntI empty_iff rev_image_eqI)+
}
from assms this show "partition_on (f ` A) ((`) f ` P)"
by (auto intro!: partition_onI elim!: partition_onE)
qed

lemma set_of_partition_on_map:
assumes "inj_on f A"
shows "(`) ((`) f) ` {P. partition_on A P} = {P. partition_on (f ` A) P}"
proof (rule set_eqI')
fix x
assume "x ∈ (`) ((`) f) ` {P. partition_on A P}"
from this ‹inj_on f A› show "x ∈ {P. partition_on (f ` A) P}"
by (auto intro: partition_on_map)
next
fix P
assume "P ∈ {P. partition_on (f ` A) P}"
from this have "partition_on (f ` A) P" by auto
from this have mem: "⋀X x. X ∈ P ⟹ x ∈ X ⟹ x ∈ f ` A"
by (auto elim!: partition_onE)
have "(`) (f ∘ the_inv_into A f) ` P = (`) f ` (`) (the_inv_into A f) ` P"
by (simp add: image_image cong: image_cong_simp)
moreover have "P = (`) (f ∘ the_inv_into A f) ` P"
proof (rule set_eqI')
fix X
assume X: "X ∈ P"
moreover from X mem have in_range: "∀x∈X. x ∈ f ` A" by auto
moreover have "X = (f ∘ the_inv_into A f) ` X"
proof (rule set_eqI')
fix x
assume "x ∈ X"
show "x ∈ (f ∘ the_inv_into A f) ` X"
proof (rule image_eqI)
from in_range ‹x ∈ X› assms show "x = (f ∘ the_inv_into A f) x"
by (auto simp add: f_the_inv_into_f[of f])
from ‹x ∈ X› show "x ∈ X" by assumption
qed
next
fix x
assume "x ∈ (f ∘ the_inv_into A f) ` X"
from this obtain x' where x': "x' ∈ X ∧ x = f (the_inv_into A f x')" by auto
from in_range x' have f: "f (the_inv_into A f x') ∈ X"
by (subst f_the_inv_into_f[of f]) (auto intro: ‹inj_on f A›)
from x' ‹X ∈ P› f show "x ∈ X" by auto
qed
ultimately show "X ∈ (`) (f ∘ the_inv_into A f) ` P" by auto
next
fix X
assume "X ∈ (`) (f ∘ the_inv_into A f) ` P"
moreover
{
fix Y
assume "Y ∈ P"
from this ‹inj_on f A› mem have "∀x∈Y. f (the_inv_into A f x) = x"
from this have "(f ∘ the_inv_into A f) ` Y = Y" by force
}
ultimately show "X ∈ P" by auto
qed
ultimately have P: "P = (`) f ` (`) (the_inv_into A f) ` P" by simp
have A_eq: "A = the_inv_into A f ` f ` A" by (simp add: assms)
from ‹inj_on f A› have "inj_on (the_inv_into A f) (f ` A)"
using ‹partition_on (f ` A) P› by (simp add: inj_on_the_inv_into)
from this have  "(`) (the_inv_into A f) ` P ∈ {P. partition_on A P}"
using ‹partition_on (f ` A) P› by (subst A_eq, auto intro!: partition_on_map)
from P this show "P ∈ (`) ((`) f) ` {P. partition_on A P}" by (rule image_eqI)
qed

end
```