section ‹Partitions of sets›
theory Partitions_ZF imports Finite_ZF FiniteSeq_ZF
begin
text‹It is a common trick in proofs that we divide a set into non-overlapping
subsets. The first case is when we split the set into
two nonempty disjoint sets. Here this is modeled as an ordered pair of sets
and the set of such divisions of set $X$ is called ‹Bisections(X)›.
The second variation on this theme is a set-valued function (aren't they all
in ZF?) whose values are nonempty and mutually disjoint.
›
subsection‹Bisections›
text‹This section is about dividing sets into two non-overlapping subsets.
›
text‹The set of bisections of a given set $A$ is a set of pairs of nonempty
subsets of $A$ that do not overlap and their union is equal to $A$.›
definition
"Bisections(X) = {p ∈ Pow(X)×Pow(X).
fst(p)≠0 ∧ snd(p)≠0 ∧ fst(p)∩snd(p) = 0 ∧ fst(p)∪snd(p) = X}"
text‹Properties of bisections.›
lemma bisec_props: assumes "⟨A,B⟩ ∈ Bisections(X)" shows
"A≠0" "B≠0" "A ⊆ X" "B ⊆ X" "A ∩ B = 0" "A ∪ B = X" "X ≠ 0"
using assms Bisections_def by auto
text‹Kind of inverse of ‹bisec_props›: a pair of nonempty
disjoint sets form a bisection of their union.›
lemma is_bisec:
assumes "A≠0" "B≠0" "A ∩ B = 0"
shows "⟨A,B⟩ ∈ Bisections(A∪B)" using assms Bisections_def
by auto
text‹Bisection of $X$ is a pair of subsets of $X$.›
lemma bisec_is_pair: assumes "Q ∈ Bisections(X)"
shows "Q = ⟨fst(Q), snd(Q)⟩"
using assms Bisections_def by auto
text‹The set of bisections of the empty set is empty.›
lemma bisec_empty: shows "Bisections(0) = 0"
using Bisections_def by auto
text‹The next lemma shows what can we say about bisections of a set
with another element added.›
lemma bisec_add_point:
assumes A1: "x ∉ X" and A2: "⟨A,B⟩ ∈ Bisections(X ∪ {x})"
shows "(A = {x} ∨ B = {x}) ∨ (⟨A - {x}, B - {x}⟩ ∈ Bisections(X))"
proof -
{ assume "A ≠ {x}" and "B ≠ {x}"
with A2 have "A - {x} ≠ 0" and "B - {x} ≠ 0"
using singl_diff_empty Bisections_def
by auto
moreover have "(A - {x}) ∪ (B - {x}) = X"
proof -
have "(A - {x}) ∪ (B - {x}) = (A ∪ B) - {x}"
by auto
also from assms have "(A ∪ B) - {x} = X"
using Bisections_def by auto
finally show ?thesis by simp
qed
moreover from A2 have "(A - {x}) ∩ (B - {x}) = 0"
using Bisections_def by auto
ultimately have "⟨A - {x}, B - {x}⟩ ∈ Bisections(X)"
using Bisections_def by auto
} thus ?thesis by auto
qed
text‹A continuation of the lemma ‹bisec_add_point›
that refines the case when the pair with removed point bisects
the original set.›
lemma bisec_add_point_case3:
assumes A1: "⟨A,B⟩ ∈ Bisections(X ∪ {x})"
and A2: "⟨A - {x}, B - {x}⟩ ∈ Bisections(X)"
shows
"(⟨A, B - {x}⟩ ∈ Bisections(X) ∧ x ∈ B) ∨
(⟨A - {x}, B⟩ ∈ Bisections(X) ∧ x ∈ A)"
proof -
from A1 have "x ∈ A ∪ B"
using Bisections_def by auto
hence "x∈A ∨ x∈B" by simp
from A1 have "A - {x} = A ∨ B - {x} = B"
using Bisections_def by auto
moreover
{ assume "A - {x} = A"
with A2 ‹x ∈ A ∪ B› have
"⟨A, B - {x}⟩ ∈ Bisections(X) ∧ x ∈ B"
using singl_diff_eq by simp }
moreover
{ assume "B - {x} = B"
with A2 ‹x ∈ A ∪ B› have
"⟨A - {x}, B⟩ ∈ Bisections(X) ∧ x ∈ A"
using singl_diff_eq by simp }
ultimately show ?thesis by auto
qed
text‹Another lemma about bisecting a set with an added point.›
lemma point_set_bisec:
assumes A1: "x ∉ X" and A2: "⟨{x}, A⟩ ∈ Bisections(X ∪ {x})"
shows "A = X" and "X ≠ 0"
proof -
from A2 have "A ⊆ X" using Bisections_def by auto
moreover
{ fix a assume "a∈X"
with A2 have "a ∈ {x} ∪ A" using Bisections_def by simp
with A1 ‹a∈X› have "a ∈ A" by auto }
ultimately show "A = X" by auto
with A2 show "X ≠ 0" using Bisections_def by simp
qed
text‹Yet another lemma about bisecting a set with an added point,
very similar to ‹ point_set_bisec› with almost the same proof.›
lemma set_point_bisec:
assumes A1: "x ∉ X" and A2: "⟨A, {x}⟩ ∈ Bisections(X ∪ {x})"
shows "A = X" and "X ≠ 0"
proof -
from A2 have "A ⊆ X" using Bisections_def by auto
moreover
{ fix a assume "a∈X"
with A2 have "a ∈ A ∪ {x}" using Bisections_def by simp
with A1 ‹a∈X› have "a ∈ A" by auto }
ultimately show "A = X" by auto
with A2 show "X ≠ 0" using Bisections_def by simp
qed
text‹If a pair of sets bisects a finite set, then both
elements of the pair are finite.›
lemma bisect_fin:
assumes A1: "A ∈ FinPow(X)" and A2: "Q ∈ Bisections(A)"
shows "fst(Q) ∈ FinPow(X)" and "snd(Q) ∈ FinPow(X)"
proof -
from A2 have "⟨fst(Q), snd(Q)⟩ ∈ Bisections(A)"
using bisec_is_pair by simp
then have "fst(Q) ⊆ A" and "snd(Q) ⊆ A"
using bisec_props by auto
with A1 show "fst(Q) ∈ FinPow(X)" and "snd(Q) ∈ FinPow(X)"
using FinPow_def subset_Finite by auto
qed
subsection‹Partitions›
text‹This sections covers the situation when we have an arbitrary number
of sets we want to partition into.›
text‹We define a notion of a partition as a set valued function
such that the values for different arguments are disjoint.
The name is derived from the fact that such
function "partitions" the union of its arguments.
Please let me know if you have
a better idea for a name for such notion. We would prefer to say
''is a partition'', but that reserves the letter ''a'' as a keyword(?)
which causes problems.›
definition
Partition ("_ {is partition}" [90] 91) where
"P {is partition} ≡ ∀x ∈ domain(P).
P`(x) ≠ 0 ∧ (∀y ∈ domain(P). x≠y ⟶ P`(x) ∩ P`(y) = 0)"
text‹A fact about lists of mutually disjoint sets.›
lemma list_partition: assumes A1: "n ∈ nat" and
A2: "a : succ(n) → X" "a {is partition}"
shows "(⋃i∈n. a`(i)) ∩ a`(n) = 0"
proof -
{ assume "(⋃i∈n. a`(i)) ∩ a`(n) ≠ 0"
then have "∃x. x ∈ (⋃i∈n. a`(i)) ∩ a`(n)"
by (rule nonempty_has_element)
then obtain x where "x ∈ (⋃i∈n. a`(i))" and I: "x ∈ a`(n)"
by auto
then obtain i where "i ∈ n" and "x ∈ a`(i)" by auto
with A2 I have False
using mem_imp_not_eq func1_1_L1 Partition_def
by auto
} thus ?thesis by auto
qed
text‹We can turn every injection into a partition.›
lemma inj_partition:
assumes A1: "b ∈ inj(X,Y)"
shows
"∀x ∈ X. {⟨x, {b`(x)}⟩. x ∈ X}`(x) = {b`(x)}" and
"{⟨x, {b`(x)}⟩. x ∈ X} {is partition}"
proof -
let ?p = "{⟨x, {b`(x)}⟩. x ∈ X}"
{ fix x assume "x ∈ X"
from A1 have "b : X → Y" using inj_def
by simp
with ‹x ∈ X› have "{b`(x)} ∈ Pow(Y)"
using apply_funtype by simp
} hence "∀x ∈ X. {b`(x)} ∈ Pow(Y)" by simp
then have "?p : X → Pow(Y)" using ZF_fun_from_total
by simp
then have "domain(?p) = X" using func1_1_L1
by simp
from ‹?p : X → Pow(Y)› show I: "∀x ∈ X. ?p`(x) = {b`(x)}"
using ZF_fun_from_tot_val0 by simp
{ fix x assume "x ∈ X"
with I have "?p`(x) = {b`(x)}" by simp
hence "?p`(x) ≠ 0" by simp
moreover
{ fix t assume "t ∈ X" and "x ≠ t"
with A1 ‹x ∈ X› have "b`(x) ≠ b`(t)" using inj_def
by auto
with I ‹x∈X› ‹t ∈ X› have "?p`(x) ∩ ?p`(t) = 0"
by auto }
ultimately have
"?p`(x) ≠ 0 ∧ (∀t ∈ X. x≠t ⟶ ?p`(x) ∩ ?p`(t) = 0)"
by simp
} with ‹domain(?p) = X› show "{⟨x, {b`(x)}⟩. x ∈ X} {is partition}"
using Partition_def by simp
qed
end