Theory ZF1
section ‹ZF set theory basics›
theory ZF1 imports ZF.Perm
begin
text‹The standard Isabelle distribution contains lots of facts about basic set
theory. This theory file adds some more.›
subsection‹Lemmas in Zermelo-Fraenkel set theory›
text‹Here we put lemmas from the set theory that we could not find in
the standard Isabelle distribution or just so that they are easier to find.›
text‹A set cannot be a member of itself. This is exactly lemma ‹mem_not_refl›
from Isabelle/ZF ‹upair.thy›, we put it here for easy reference. ›
lemma mem_self: shows "x∉x" by (rule mem_not_refl)
text‹If one collection is contained in another, then we can say the same
about their unions.›
lemma collection_contain: assumes "A⊆B" shows "⋃A ⊆ ⋃B"
proof
fix x assume "x ∈ ⋃A"
then obtain X where "x∈X" and "X∈A" by auto
with assms show "x ∈ ⋃B" by auto
qed
text‹In ZF set theory the zero of natural numbers is the same as the empty set.
In the next abbreviation we declare that we want $0$ and $\emptyset$ to be synonyms
so that we can use $\emptyset$ instead of $0$ when appropriate. ›
abbreviation empty_set ("∅") where "∅ ≡ 0"
text‹If all sets of a nonempty collection are the same, then its union
is the same.›
lemma ZF1_1_L1: assumes "C≠∅" and "∀y∈C. b(y) = A"
shows "(⋃y∈C. b(y)) = A" using assms by blast
text‹The union af all values of a constant meta-function belongs to
the same set as the constant.›
lemma ZF1_1_L2: assumes A1:"C≠∅" and A2: "∀x∈C. b(x) ∈ A"
and A3: "∀x y. x∈C ∧ y∈C ⟶ b(x) = b(y)"
shows "(⋃x∈C. b(x))∈A"
proof -
from A1 obtain x where D1: "x∈C" by auto
with A3 have "∀y∈C. b(y) = b(x)" by blast
with A1 have "(⋃y∈C. b(y)) = b(x)"
using ZF1_1_L1 by simp
with D1 A2 show ?thesis by simp
qed
text‹If two meta-functions are the same on a cartesian product,
then the subsets defined by them are the same. I am surprised Isabelle
can not handle this automatically.›
lemma ZF1_1_L4: assumes A1: "∀x∈X.∀y∈Y. a(x,y) = b(x,y)"
shows "{a(x,y). ⟨x,y⟩ ∈ X×Y} = {b(x,y). ⟨x,y⟩ ∈ X×Y}"
proof
show "{a(x, y). ⟨x,y⟩ ∈ X × Y} ⊆ {b(x, y). ⟨x,y⟩ ∈ X × Y}"
proof
fix z assume "z ∈ {a(x, y) . ⟨x,y⟩ ∈ X × Y}"
with A1 show "z ∈ {b(x,y).⟨x,y⟩ ∈ X×Y}" by auto
qed
show "{b(x, y). ⟨x,y⟩ ∈ X × Y} ⊆ {a(x, y). ⟨x,y⟩ ∈ X × Y}"
proof
fix z assume "z ∈ {b(x, y). ⟨x,y⟩ ∈ X × Y}"
with A1 show "z ∈ {a(x,y).⟨x,y⟩ ∈ X×Y}" by auto
qed
qed
text‹If two meta-functions are the same on a cartesian product,
then the subsets defined by them are the same.
This is similar to ‹ZF1_1_L4›, except that
the set definition varies over ‹p∈X×Y› rather than
‹⟨ x,y⟩∈X×Y›.›
lemma ZF1_1_L4A: assumes A1: "∀x∈X.∀y∈Y. a(⟨ x,y⟩) = b(x,y)"
shows "{a(p). p ∈ X×Y} = {b(x,y). ⟨x,y⟩ ∈ X×Y}"
proof
{ fix z assume "z ∈ {a(p). p∈X×Y}"
then obtain p where D1: "z=a(p)" "p∈X×Y" by auto
let ?x = "fst(p)" let ?y = "snd(p)"
from A1 D1 have "z ∈ {b(x,y). ⟨x,y⟩ ∈ X×Y}" by auto
} then show "{a(p). p ∈ X×Y} ⊆ {b(x,y). ⟨x,y⟩ ∈ X×Y}" by blast
next
{ fix z assume "z ∈ {b(x,y). ⟨x,y⟩ ∈ X×Y}"
then obtain x y where D1: "⟨x,y⟩ ∈ X×Y" "z=b(x,y)" by auto
let ?p = "⟨ x,y⟩"
from A1 D1 have "?p∈X×Y" "z = a(?p)" by auto
then have "z ∈ {a(p). p ∈ X×Y}" by auto
} then show "{b(x,y). ⟨x,y⟩ ∈ X×Y} ⊆ {a(p). p ∈ X×Y}" by blast
qed
text‹A lemma about inclusion in cartesian products. Included here to remember
that we need the $U\times V \neq \emptyset$ assumption.›
lemma prod_subset: assumes "U×V≠∅" "U×V ⊆ X×Y" shows "U⊆X" and "V⊆Y"
using assms by auto
text‹A technical lemma about sections in cartesian products.›
lemma section_proj: assumes "A ⊆ X×Y" and "U×V ⊆ A" and "x ∈ U" "y ∈ V"
shows "U ⊆ {t∈X. ⟨t,y⟩ ∈ A}" and "V ⊆ {t∈Y. ⟨x,t⟩ ∈ A}"
using assms by auto
text‹If two meta-functions are the same on a set, then they define the same
set by separation.›
lemma ZF1_1_L4B: assumes "∀x∈X. a(x) = b(x)"
shows "{a(x). x∈X} = {b(x). x∈X}"
using assms by simp
text‹A set defined by a constant meta-function is a singleton.›
lemma ZF1_1_L5: assumes "X≠∅" and "∀x∈X. b(x) = c"
shows "{b(x). x∈X} = {c}" using assms by blast
text‹Most of the time, ‹auto› does this job, but there are strange
cases when the next lemma is needed.›
lemma subset_with_property: assumes "Y = {x∈X. b(x)}"
shows "Y ⊆ X"
using assms by auto
text‹If set $A$ is contained in set $B$ and exist elements $x,y$ of the set $A$
that satisfy a predicate then exist elements of the set $B$ that satisfy the predicate. ›
lemma exist2_subset: assumes "A⊆B" and "∃x∈A. ∃y∈A. φ(x,y)"
shows "∃x∈B. ∃y∈B. φ(x,y)"
using assms by blast
text‹We can choose an element from a nonempty set.›
lemma nonempty_has_element: assumes "X≠∅" shows "∃x. x∈X"
using assms by auto
text‹In Isabelle/ZF the intersection of an empty family is
empty. This is exactly lemma ‹Inter_0› from Isabelle's
‹equalities› theory. We repeat this lemma here as it is very
difficult to find. This is one reason we need comments before every
theorem: so that we can search for keywords.›
lemma inter_empty_empty: shows "⋂∅ = ∅" by (rule Inter_0)
text‹If an intersection of a collection is not empty, then the collection is
not empty. We are (ab)using the fact the the intersection of empty collection
is defined to be empty.›
lemma inter_nempty_nempty: assumes "⋂A ≠ ∅" shows "A≠∅"
using assms by auto
text‹For two collections $S,T$ of sets we define the product collection
as the collections of cartesian products $A\times B$, where $A\in S, B\in T$.›
definition
"ProductCollection(T,S) ≡ ⋃U∈T.{U×V. V∈S}"
text‹The union of the product collection of collections $S,T$ is the
cartesian product of $\bigcup S$ and $\bigcup T$.›
lemma ZF1_1_L6: shows "⋃ ProductCollection(S,T) = ⋃S × ⋃T"
using ProductCollection_def by auto
text‹An intersection of subsets is a subset.›
lemma ZF1_1_L7: assumes A1: "I≠∅" and A2: "∀i∈I. P(i) ⊆ X"
shows "( ⋂i∈I. P(i) ) ⊆ X"
proof -
from A1 obtain i⇩0 where "i⇩0 ∈ I" by auto
with A2 have "( ⋂i∈I. P(i) ) ⊆ P(i⇩0)" and "P(i⇩0) ⊆ X"
by auto
thus "( ⋂i∈I. P(i) ) ⊆ X" by auto
qed
text‹Isabelle/ZF has a "THE" construct that allows to define an element
if there is only one such that is satisfies given predicate.
In pure ZF we can express something similar using the indentity proven below.›
lemma ZF1_1_L8: shows "⋃ {x} = x" by auto
text‹Some properties of singletons.›
lemma ZF1_1_L9: assumes A1: "∃! x. x∈A ∧ φ(x)"
shows
"∃a. {x∈A. φ(x)} = {a}"
"⋃ {x∈A. φ(x)} ∈ A"
"φ(⋃ {x∈A. φ(x)})"
proof -
from A1 show "∃a. {x∈A. φ(x)} = {a}" by auto
then obtain a where I: "{x∈A. φ(x)} = {a}" by auto
then have "⋃ {x∈A. φ(x)} = a" by auto
moreover
from I have "a ∈ {x∈A. φ(x)}" by simp
hence "a∈A" and "φ(a)" by auto
ultimately show "⋃ {x∈A. φ(x)} ∈ A" and "φ(⋃ {x∈A. φ(x)})"
by auto
qed
text‹A simple version of ‹ ZF1_1_L9›.›
corollary : assumes "∃! x. x∈A"
shows "(⋃ A) ∈ A"
proof -
from assms have "∃! x. x∈A ∧ True" by simp
then have "⋃ {x∈A. True} ∈ A" by (rule ZF1_1_L9)
thus "(⋃ A) ∈ A" by simp
qed
text‹A criterion for when a set defined by comprehension is a singleton.›
lemma singleton_comprehension:
assumes A1: "y∈X" and A2: "∀x∈X. ∀y∈X. P(x) = P(y)"
shows "(⋃{P(x). x∈X}) = P(y)"
proof -
let ?A = "{P(x). x∈X}"
have "∃! c. c ∈ ?A"
proof
from A1 show "∃c. c ∈ ?A" by auto
next
fix a b assume "a ∈ ?A" and "b ∈ ?A"
then obtain x t where
"x ∈ X" "a = P(x)" and "t ∈ X" "b = P(t)"
by auto
with A2 show "a=b" by blast
qed
then have "(⋃?A) ∈ ?A" by (rule singleton_extract)
then obtain x where "x ∈ X" and "(⋃?A) = P(x)"
by auto
from A1 A2 ‹x ∈ X› have "P(x) = P(y)"
by blast
with ‹(⋃?A) = P(x)› show "(⋃?A) = P(y)" by simp
qed
text‹Adding an element of a set to that set does not change the set.›
lemma set_elem_add: assumes "x∈X" shows "X ∪ {x} = X" using assms
by auto
text‹Here we define a restriction of a collection of sets to a given set.
In romantic math this is typically denoted $X\cap M$ and means
$\{X\cap A : A\in M \} $. Note there is also restrict$(f,A)$
defined for relations in ZF.thy.›
definition
RestrictedTo (infixl "{restricted to}" 70) where
"M {restricted to} X ≡ {X ∩ A . A ∈ M}"
text‹A lemma on a union of a restriction of a collection
to a set.›
lemma union_restrict:
shows "⋃(M {restricted to} X) = (⋃M) ∩ X"
using RestrictedTo_def by auto
text‹Next we show a technical identity that is used to prove sufficiency
of some condition for a collection of sets to be a base for a topology.›
lemma ZF1_1_L10: assumes A1: "∀U∈C. ∃A∈B. U = ⋃A"
shows "⋃⋃ {⋃{A∈B. U = ⋃A}. U∈C} = ⋃C"
proof
show "⋃(⋃U∈C. ⋃{A ∈ B . U = ⋃A}) ⊆ ⋃C" by blast
show "⋃C ⊆ ⋃(⋃U∈C. ⋃{A ∈ B . U = ⋃A})"
proof
fix x assume "x ∈ ⋃C"
show "x ∈ ⋃(⋃U∈C. ⋃{A ∈ B . U = ⋃A})"
proof -
from ‹x ∈ ⋃C› obtain U where "U∈C ∧ x∈U" by auto
with A1 obtain A where "A∈B ∧ U = ⋃A" by auto
from ‹U∈C ∧ x∈U› ‹A∈B ∧ U = ⋃A› show "x∈ ⋃(⋃U∈C. ⋃{A ∈ B . U = ⋃A})"
by auto
qed
qed
qed
text‹Standard Isabelle uses a notion of ‹cons(A,a)› that can be thought
of as $A\cup \{a\}$.›
lemma consdef: shows "cons(a,A) = A ∪ {a}"
using cons_def by auto
text‹If a difference between a set and a singleton is empty, then
the set is empty or it is equal to the singleton.›
lemma singl_diff_empty: assumes "A - {x} = ∅"
shows "A = ∅ ∨ A = {x}"
using assms by auto
text‹If a difference between a set and a singleton is the set,
then the only element of the singleton is not in the set.›
lemma singl_diff_eq: assumes A1: "A - {x} = A"
shows "x ∉ A"
proof -
have "x ∉ A - {x}" by auto
with A1 show "x ∉ A" by simp
qed
text‹Simple substitution in membership, has to be used by rule
in very rare cases.›
lemma eq_mem: assumes "x∈A" and "y=x" shows "y∈A"
using assms by simp
text‹A basic property of sets defined by comprehension.›
lemma comprehension: assumes "a ∈ {x∈X. p(x)}"
shows "a∈X" and "p(a)" using assms by auto
text‹A basic property of a set defined by another type of comprehension.›
lemma comprehension_repl: assumes "y ∈ {p(x). x∈X}"
shows "∃x∈X. y = p(x)" using assms by auto
text‹The inverse of the ‹comprehension› lemma.›
lemma mem_cond_in_set: assumes "φ(c)" and "c∈X"
shows "c ∈ {x∈X. φ(x)}" using assms by blast
text‹The image of a set by a greater relation is greater. ›
lemma image_rel_mono: assumes "r⊆s" shows "r``(A) ⊆ s``(A)"
using assms by auto
text‹ A technical lemma about relations: if $x$ is in its image by a relation $U$
and that image is contained in some set $C$, then the image of the singleton
$\{ x\}$ by the relation $U \cup C\times C$ equals $C$. ›
lemma image_greater_rel:
assumes "x ∈ U``{x}" and "U``{x} ⊆ C"
shows "(U ∪ C×C)``{x} = C"
using assms image_Un_left by blast
text‹Reformulation of the definition of composition of two relations: ›
lemma rel_compdef:
shows "⟨x,z⟩ ∈ r O s ⟷ (∃y. ⟨x,y⟩ ∈ s ∧ ⟨y,z⟩ ∈ r)"
unfolding comp_def by auto
text‹Domain and range of the relation of the form $\bigcup \{U\times U : U\in P\}$
is $\bigcup P$: ›
lemma domain_range_sym: shows "domain(⋃{U×U. U∈P}) = ⋃P" and "range(⋃{U×U. U∈P}) = ⋃P"
by auto
text‹An identity for the square (in the sense of composition) of a symmetric relation.›
lemma symm_sq_prod_image: assumes "converse(r) = r"
shows "r O r = ⋃{(r``{x})×(r``{x}). x ∈ domain(r)}"
proof
{ fix p assume "p ∈ r O r"
then obtain y z where "⟨y,z⟩ = p" by auto
with ‹p ∈ r O r› obtain x where "⟨y,x⟩ ∈ r" and "⟨x,z⟩ ∈ r"
using rel_compdef by auto
from ‹⟨y,x⟩ ∈ r› have "⟨x,y⟩ ∈ converse(r)" by simp
with assms ‹⟨x,z⟩ ∈ r› ‹⟨y,z⟩ = p› have "∃x∈domain(r). p ∈ (r``{x})×(r``{x})"
by auto
} thus "r O r ⊆ (⋃{(r``{x})×(r``{x}). x ∈ domain(r)})"
by blast
{ fix x assume "x ∈ domain(r)"
have "(r``{x})×(r``{x}) ⊆ r O r"
proof -
{ fix p assume "p ∈ (r``{x})×(r``{x})"
then obtain y z where "⟨y,z⟩ = p" "y ∈ r``{x}" "z ∈ r``{x}"
by auto
from ‹y ∈ r``{x}› have "⟨x,y⟩ ∈ r" by auto
then have "⟨y,x⟩ ∈ converse(r)" by simp
with assms ‹z ∈ r``{x}› ‹⟨y,z⟩ = p› have "p ∈ r O r" by auto
} thus ?thesis by auto
qed
} thus "(⋃{(r``{x})×(r``{x}). x ∈ domain(r)}) ⊆ r O r"
by blast
qed
text‹Square of a reflexive relation contains the relation.
Recall that in ZF the identity function on $X$ is the same as the diagonal
of $X\times X$, i.e. $id(X) = \{\langle x,x\rangle : x\in X\}$. ›
lemma refl_square_greater: assumes "r ⊆ X×X" "id(X) ⊆ r"
shows "r ⊆ r O r" using assms by auto
text‹A reflexive relation is contained in the union of products of its singleton images. ›
lemma refl_union_singl_image:
assumes "A ⊆ X×X" and "id(X)⊆A" shows "A ⊆ ⋃{A``{x}×A``{x}. x ∈ X}"
proof -
{ fix p assume "p∈A"
with assms(1) obtain x y where "x∈X" "y∈X" and "p=⟨x,y⟩" by auto
with assms(2) ‹p∈A› have "∃x∈X. p ∈ A``{x}×A``{x}" by auto
} thus ?thesis by auto
qed
text‹If the cartesian product of the images of $x$ and $y$ by a
symmetric relation $W$ has a nonempty intersection with $R$
then $x$ is in relation $W\circ (R\circ W)$ with $y$. ›
lemma sym_rel_comp:
assumes "W=converse(W)" and "(W``{x})×(W``{y}) ∩ R ≠ ∅"
shows "⟨x,y⟩ ∈ (W O (R O W))"
proof -
from assms(2) obtain s t where "s∈W``{x}" "t∈W``{y}" and "⟨s,t⟩∈R"
by blast
then have "⟨x,s⟩ ∈ W" and "⟨y,t⟩ ∈ W" by auto
from ‹⟨x,s⟩ ∈ W› ‹⟨s,t⟩ ∈ R› have "⟨x,t⟩ ∈ R O W" by auto
from ‹⟨y,t⟩ ∈ W› have "⟨t,y⟩ ∈ converse(W)" by blast
with assms(1) ‹⟨x,t⟩ ∈ R O W› show ?thesis by auto
qed
text‹ It's hard to believe but there are cases where we have to reference this rule. ›
lemma set_mem_eq: assumes "x∈A" "A=B" shows "x∈B" using assms by simp
text‹Given some family $\mathcal{A}$ of subsets of $X$ we can define the family of supersets of
$\mathcal{A}$. ›
definition
"Supersets(X,𝒜) ≡ {B∈Pow(X). ∃A∈𝒜. A⊆B}"
text‹The family itself is in its supersets. ›
lemma superset_gen: assumes "A⊆X" "A∈𝒜" shows "A ∈ Supersets(X,𝒜)"
using assms unfolding Supersets_def by auto
text‹The whole space is a superset of any nonempty collection of its subsets. ›
lemma space_superset: assumes "𝒜≠∅" "𝒜⊆Pow(X)" shows "X ∈ Supersets(X,𝒜)"
proof -
from assms(1) obtain A where "A∈𝒜" by auto
with assms(2) show ?thesis unfolding Supersets_def by auto
qed
text‹The collection of supersets of an empty set is empty. In particular
the whole space $X$ is not a superset of an empty set. ›
lemma supersets_of_empty: shows "Supersets(X,∅) = ∅"
unfolding Supersets_def by auto
text‹However, when the space is empty the collection of supersets does not have
to be empty - the collection of supersets of the singleton collection containing
only the empty set is this collection. ›
lemma supersets_in_empty: shows "Supersets(∅,{∅}) = {∅}"
unfolding Supersets_def by auto
text‹This can be done by the auto method, but sometimes takes a long time. ›
lemma witness_exists: assumes "x∈X" and "φ(x)" shows "∃x∈X. φ(x)"
using assms by auto
text‹Another lemma that concludes existence of some set.›
lemma witness_exists1: assumes "x∈X" "φ(x)" "ψ(x)"
shows "∃x∈X. φ(x) ∧ ψ(x)"
using assms by auto
text‹The next lemma has to be used as a rule in some rare cases. ›
lemma exists_in_set: assumes "∀x. x∈A ⟶ φ(x)" shows "∀x∈A. φ(x)"
using assms by simp
text‹If $x$ belongs to a set where a property holds, then the property holds
for $x$. This has to be used as rule in rare cases. ›
lemma property_holds: assumes "∀t∈X. φ(t)" and "x∈X"
shows "φ(x)" using assms by simp
text‹Set comprehensions defined by equal expressions are the equal.
The second assertion is actually about functions, which are sets of pairs
as illustrated in lemma ‹fun_is_set_of_pairs› in ‹func1.thy› ›
lemma set_comp_eq: assumes "∀x∈X. p(x) = q(x)"
shows "{p(x). x∈X} = {q(x). x∈X}" and "{⟨x,p(x)⟩. x∈X} = {⟨x,q(x)⟩. x∈X}"
using assms by auto
text‹If every element of a non-empty set $X\subseteq Y$ satisfies a condition
then the set of elements of $Y$ that satisfy the condition is non-empty.›
lemma non_empty_cond: assumes "X≠∅" "X⊆Y" and "∀x∈X. P(x)"
shows "{x∈Y. P(x)} ≠ 0" using assms by auto
text‹If $z$ is a pair, then the cartesian product of the singletons of its
elements is the same as the singleton $\{ z\}$.›
lemma pair_prod: assumes "z = ⟨x,y⟩" shows "{x}×{y} = {z}"
using assms by blast
text‹In Isabelle/ZF the set difference is written with a minus sign $A-B$
because the standard backslash character is reserved for other purposes.
The next abbreviation declares that we want the set difference character $A\setminus B$
to be synonymous with the minus sign. ›
abbreviation set_difference (infixl "∖" 65) where "A∖B ≡ A-B"
end