theory ZF1 imports ZF.Perm
begin
The standard Isabelle distribution contains lots of facts about basic set theory. This theory file adds some more.
Lemmas in Zermelo-Fraenkel set theory
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.
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\notin x \) by (rule mem_not_refl )If one collection is contained in another, then we can say the same about their unions.
lemma collection_contain:
assumes \( A\subseteq B \)
shows \( \bigcup A \subseteq \bigcup B \)proof fix \( x \)
assume \( x \in \bigcup A \)
then obtain \( X \) where \( x\in X \) and \( X\in A \)
with assms show \( x \in \bigcup B \)
qed
If all sets of a nonempty collection are the same, then its union is the same.
lemma ZF1_1_L1:
assumes \( C\neq 0 \) and \( \forall y\in C.\ b(y) = A \)
shows \( (\bigcup y\in C.\ b(y)) = A \) using assmsThe union af all values of a constant meta-function belongs to the same set as the constant.
lemma ZF1_1_L2:
assumes A1: \( C\neq 0 \) and A2: \( \forall x\in C.\ b(x) \in A \) and A3: \( \forall x y.\ x\in C \wedge y\in C \longrightarrow b(x) = b(y) \)
shows \( (\bigcup x\in C.\ b(x))\in A \)proof from A1 obtain \( x \) where D1: \( x\in C \)
with A3 have \( \forall y\in C.\ b(y) = b(x) \)
with A1 have \( (\bigcup y\in C.\ b(y)) = b(x) \) using ZF1_1_L1
with D1, A2 show \( thesis \)
qed
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: \( \forall x\in X.\ \forall y\in Y.\ a(x,y) = b(x,y) \)
shows \( \{a(x,y).\ \langle x,y\rangle \in X\times Y\} = \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \)proof show \( \{a(x, y).\ \langle x,y\rangle \in X \times Y\} \subseteq \{b(x, y).\ \langle x,y\rangle \in X \times Y\} \)proof
fix \( z \)
assume \( z \in \{a(x, y) .\ \langle x,y\rangle \in X \times Y\} \)
with A1 show \( z \in \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \)
qed
show \( \{b(x, y).\ \langle x,y\rangle \in X \times Y\} \subseteq \{a(x, y).\ \langle x,y\rangle \in X \times Y\} \)proof
qed
fix \( z \)
assume \( z \in \{b(x, y).\ \langle x,y\rangle \in X \times Y\} \)
with A1 show \( z \in \{a(x,y).\ \langle x,y\rangle \in X\times Y\} \)
qed
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\in X\times Y \) rather than \( \langle x,y\rangle \in X\times Y \).
lemma ZF1_1_L4A:
assumes A1: \( \forall x\in X.\ \forall y\in Y.\ a(\langle x,y\rangle ) = b(x,y) \)
shows \( \{a(p).\ p \in X\times Y\} = \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \)proof{
}
}
fix \( z \)
assume \( z \in \{a(p).\ p\in X\times Y\} \)
then obtain \( p \) where D1: \( z=a(p) \), \( p\in X\times Y \)
let \( x = \text{fst}(p) \)
let \( y = \text{snd}(p) \)
from A1, D1 have \( z \in \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \)
then show \( \{a(p).\ p \in X\times Y\} \subseteq \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \)
next
{
fix \( z \)
assume \( z \in \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \)
then obtain \( x \) \( y \) where D1: \( \langle x,y\rangle \in X\times Y \), \( z=b(x,y) \)
let \( p = \langle x,y\rangle \)
from A1, D1 have \( p\in X\times Y \), \( z = a(p) \)
then have \( z \in \{a(p).\ p \in X\times Y\} \)
then show \( \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \subseteq \{a(p).\ p \in X\times Y\} \)
qed
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\times V\neq 0 \), \( U\times V \subseteq X\times Y \)
shows \( U\subseteq X \) and \( V\subseteq Y \) using assmsA technical lemma about sections in cartesian products.
lemma section_proj:
assumes \( A \subseteq X\times Y \) and \( U\times V \subseteq A \) and \( x \in U \), \( y \in V \)
shows \( U \subseteq \{t\in X.\ \langle t,y\rangle \in A\} \) and \( V \subseteq \{t\in Y.\ \langle x,t\rangle \in A\} \) using assmsIf two meta-functions are the same on a set, then they define the same set by separation.
lemma ZF1_1_L4B:
assumes \( \forall x\in X.\ a(x) = b(x) \)
shows \( \{a(x).\ x\in X\} = \{b(x).\ x\in X\} \) using assmsA set defined by a constant meta-function is a singleton.
lemma ZF1_1_L5:
assumes \( X\neq 0 \) and \( \forall x\in X.\ b(x) = c \)
shows \( \{b(x).\ x\in X\} = \{c\} \) using assmsMost 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\in X.\ b(x)\} \)
shows \( Y \subseteq X \) using assmsWe can choose an element from a nonempty set.
lemma nonempty_has_element:
assumes \( X\neq 0 \)
shows \( \exists x.\ x\in X \) using assmsIn 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 \( \bigcap 0 = 0 \) by (rule Inter_0 )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 \( \bigcap A \neq 0 \)
shows \( A\neq 0 \) using assmsFor 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
\( \text{ProductCollection}(T,S) \equiv \bigcup U\in T.\ \{U\times V.\ V\in S\} \)
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 \( \bigcup \text{ProductCollection}(S,T) = \bigcup S \times \bigcup T \) using ProductCollection_defAn intersection of subsets is a subset.
lemma ZF1_1_L7:
assumes A1: \( I\neq 0 \) and A2: \( \forall i\in I.\ P(i) \subseteq X \)
shows \( ( \bigcap i\in I.\ P(i) ) \subseteq X \)proof from A1 obtain \( i_0 \) where \( i_0 \in I \)
with A2 have \( ( \bigcap i\in I.\ P(i) ) \subseteq P(i_0) \) and \( P(i_0) \subseteq X \)
thus \( ( \bigcap i\in I.\ P(i) ) \subseteq X \)
qed
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 \( \bigcup \{x\} = x \)Some properties of singletons.
lemma ZF1_1_L9:
assumes A1: \( \exists ! x.\ x\in A \wedge \phi (x) \)
shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \)proof from A1 show \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \)
then obtain \( a \) where I: \( \{x\in A.\ \phi (x)\} = \{a\} \)
then have \( \bigcup \{x\in A.\ \phi (x)\} = a \)
moreover
qed
from I have \( a \in \{x\in A.\ \phi (x)\} \)
hence \( a\in A \) and \( \phi (a) \)
ultimately show \( \bigcup \{x\in A.\ \phi (x)\} \in A \) and \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \)
A simple version of ZF1_1_L9.
corollary singleton_extract:
assumes \( \exists ! x.\ x\in A \)
shows \( (\bigcup A) \in A \)proof from assms have \( \exists ! x.\ x\in A \wedge True \)
then have \( \bigcup \{x\in A.\ True\} \in A \) by (rule ZF1_1_L9 )
thus \( (\bigcup A) \in A \)
qed
A criterion for when a set defined by comprehension is a singleton.
lemma singleton_comprehension:
assumes A1: \( y\in X \) and A2: \( \forall x\in X.\ \forall y\in X.\ P(x) = P(y) \)
shows \( (\bigcup \{P(x).\ x\in X\}) = P(y) \)proof let \( A = \{P(x).\ x\in X\} \)
have \( \exists ! c.\ c \in A \)proof
from A1 show \( \exists c.\ c \in A \)
next
fix \( a \) \( b \)
assume \( a \in A \) and \( b \in A \)
then obtain \( x \) \( t \) where \( x \in X \), \( a = P(x) \) and \( t \in X \), \( b = P(t) \)
with A2 show \( a=b \)
qed
then have \( (\bigcup A) \in A \) by (rule singleton_extract )
then obtain \( x \) where \( x \in X \) and \( (\bigcup A) = P(x) \)
from A1, A2, \( x \in X \) have \( P(x) = P(y) \)
with \( (\bigcup A) = P(x) \) show \( (\bigcup A) = P(y) \)
qed
Adding an element of a set to that set does not change the set.
lemma set_elem_add:
assumes \( x\in X \)
shows \( X \cup \{x\} = X \) using assmsHere 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
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
A lemma on a union of a restriction of a collection to a set.
lemma union_restrict:
shows \( \bigcup (M \text{ restricted to } X) = (\bigcup M) \cap X \) using RestrictedTo_defNext 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: \( \forall U\in C.\ \exists A\in B.\ U = \bigcup A \)
shows \( \bigcup \bigcup \{\bigcup \{A\in B.\ U = \bigcup A\}.\ U\in C\} = \bigcup C \)proof show \( \bigcup (\bigcup U\in C.\ \bigcup \{A \in B .\ U = \bigcup A\}) \subseteq \bigcup C \)
show \( \bigcup C \subseteq \bigcup (\bigcup U\in C.\ \bigcup \{A \in B .\ U = \bigcup A\}) \)proof
qed
fix \( x \)
assume \( x \in \bigcup C \)
show \( x \in \bigcup (\bigcup U\in C.\ \bigcup \{A \in B .\ U = \bigcup A\}) \)proof
qed
from \( x \in \bigcup C \) obtain \( U \) where \( U\in C \wedge x\in U \)
with A1 obtain \( A \) where \( A\in B \wedge U = \bigcup A \)
from \( U\in C \wedge x\in U \), \( A\in B \wedge U = \bigcup A \) show \( x\in \bigcup (\bigcup U\in C.\ \bigcup \{A \in B .\ U = \bigcup A\}) \)
qed
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 \cup \{a\} \) using cons_defIf 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\} = 0 \)
shows \( A = 0 \vee A = \{x\} \) using assmsIf 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 \notin A \)proof have \( x \notin A - \{x\} \)
with A1 show \( x \notin A \)
qed
Simple substitution in membership, has to be used by rule in very rare cases.
lemma eq_mem:
assumes \( x\in A \) and \( y=x \)
shows \( y\in A \) using assmsA basic property of sets defined by comprehension.
lemma comprehension:
assumes \( a \in \{x\in X.\ p(x)\} \)
shows \( a\in X \) and \( p(a) \) using assmsA basic property of a set defined by another type of comprehension.
lemma comprehension_repl:
assumes \( y \in \{p(x).\ x\in X\} \)
shows \( \exists x\in X.\ y = p(x) \) using assmsThe inverse of the comprehension lemma.
lemma mem_cond_in_set:
assumes \( \phi (c) \) and \( c\in X \)
shows \( c \in \{x\in X.\ \phi (x)\} \) using assmsThe image of a set by a greater relation is greater.
lemma image_rel_mono:
assumes \( r\subseteq s \)
shows \( r(A) \subseteq s(A) \) using assmsA 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 \in U\{x\} \) and \( U\{x\} \subseteq C \)
shows \( (U \cup C\times C)\{x\} = C \) using assms, image_Un_leftReformulation of the definition of composition of two relations:
lemma rel_compdef:
shows \( \langle x,z\rangle \in r\circ s \longleftrightarrow (\exists y.\ \langle x,y\rangle \in s \wedge \langle y,z\rangle \in r) \) unfolding comp_defDomain and range of the relation of the form \(\bigcup \{U\times U : U\in P\}\) is \(\bigcup P\):
lemma domain_range_sym:
shows \( domain(\bigcup \{U\times U.\ U\in P\}) = \bigcup P \) and \( \text{range}(\bigcup \{U\times U.\ U\in P\}) = \bigcup P \)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\circ r = \bigcup \{(r\{x\})\times (r\{x\}).\ x \in domain(r)\} \)proof{
}
}
fix \( p \)
assume \( p \in r\circ r \)
then obtain \( y \) \( z \) where \( \langle y,z\rangle = p \)
with \( p \in r\circ r \) obtain \( x \) where \( \langle y,x\rangle \in r \) and \( \langle x,z\rangle \in r \) using rel_compdef
from \( \langle y,x\rangle \in r \) have \( \langle x,y\rangle \in converse(r) \)
with assms, \( \langle x,z\rangle \in r \), \( \langle y,z\rangle = p \) have \( \exists x\in domain(r).\ p \in (r\{x\})\times (r\{x\}) \)
thus \( r\circ r \subseteq (\bigcup \{(r\{x\})\times (r\{x\}).\ x \in domain(r)\}) \)
{
fix \( x \)
assume \( x \in domain(r) \)
have \( (r\{x\})\times (r\{x\}) \subseteq r\circ r \)proof
{
}
fix \( p \)
assume \( p \in (r\{x\})\times (r\{x\}) \)
then obtain \( y \) \( z \) where \( \langle y,z\rangle = p \), \( y \in r\{x\} \), \( z \in r\{x\} \)
from \( y \in r\{x\} \) have \( \langle x,y\rangle \in r \)
then have \( \langle y,x\rangle \in converse(r) \)
with assms, \( z \in r\{x\} \), \( \langle y,z\rangle = p \) have \( p \in r\circ r \)
thus \( thesis \)
qed
thus \( (\bigcup \{(r\{x\})\times (r\{x\}).\ x \in domain(r)\}) \subseteq r\circ r \)
qed
A reflexive relation is contained in the union of products of its singleton images.
lemma refl_union_singl_image:
assumes \( A \subseteq X\times X \) and \( id(X)\subseteq A \)
shows \( A \subseteq \bigcup \{A\{x\}\times A\{x\}.\ x \in X\} \)proof{
}
fix \( p \)
assume \( p\in A \)
with assms(1) obtain \( x \) \( y \) where \( x\in X \), \( y\in X \) and \( p=\langle x,y\rangle \)
with assms(2), \( p\in A \) have \( \exists x\in X.\ p \in A\{x\}\times A\{x\} \)
thus \( thesis \)
qed
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\})\times (W\{y\}) \cap R \neq 0 \)
shows \( \langle x,y\rangle \in (W\circ (R\circ W)) \)proof from assms(2) obtain \( s \) \( t \) where \( s\in W\{x\} \), \( t\in W\{y\} \) and \( \langle s,t\rangle \in R \)
then have \( \langle x,s\rangle \in W \) and \( \langle y,t\rangle \in W \)
from \( \langle x,s\rangle \in W \), \( \langle s,t\rangle \in R \) have \( \langle x,t\rangle \in R\circ W \)
from \( \langle y,t\rangle \in W \) have \( \langle t,y\rangle \in converse(W) \)
with assms(1), \( \langle x,t\rangle \in R\circ W \) show \( thesis \)
qed
It's hard to believe but there are cases where we have to reference this rule.
lemma set_mem_eq:
assumes \( x\in A \), \( A=B \)
shows \( x\in B \) using assmsGiven some family \(\mathcal{A}\) of subsets of \(X\) we can define the family of supersets of \(\mathcal{A}\).
definition
\( \text{Supersets}(X,\mathcal{A} ) \equiv \{B\in Pow(X).\ \exists A\in \mathcal{A} .\ A\subseteq B\} \)
The family itself is in its supersets.
lemma superset_gen:
assumes \( A\subseteq X \), \( A\in \mathcal{A} \)
shows \( A \in \text{Supersets}(X,\mathcal{A} ) \) using assms unfolding Supersets_defThis can be done by the auto method, but sometimes takes a long time.
lemma witness_exists:
assumes \( x\in X \) and \( \phi (x) \)
shows \( \exists x\in X.\ \phi (x) \) using assmsAnother lemma that concludes existence of some set.
lemma witness_exists1:
assumes \( x\in X \), \( \phi (x) \), \( \psi (x) \)
shows \( \exists x\in X.\ \phi (x) \wedge \psi (x) \) using assmsThe next lemma has to be used as a rule in some rare cases.
lemma exists_in_set:
assumes \( \forall x.\ x\in A \longrightarrow \phi (x) \)
shows \( \forall x\in A.\ \phi (x) \) using assmsIf \(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 \( \forall t\in X.\ \phi (t) \) and \( x\in X \)
shows \( \phi (x) \) using assmsSet 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 \( \forall x\in X.\ p(x) = q(x) \)
shows \( \{p(x).\ x\in X\} = \{q(x).\ x\in X\} \) and \( \{\langle x,p(x)\rangle .\ x\in X\} = \{\langle x,q(x)\rangle .\ x\in X\} \) using assmsIf \(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 = \langle x,y\rangle \)
shows \( \{x\}\times \{y\} = \{z\} \) using assms end
lemma ZF1_1_L1:
assumes \( C\neq 0 \) and \( \forall y\in C.\ b(y) = A \)
shows \( (\bigcup y\in C.\ b(y)) = A \)Definition of ProductCollection:
\( \text{ProductCollection}(T,S) \equiv \bigcup U\in T.\ \{U\times V.\ V\in S\} \)
lemma ZF1_1_L9:
assumes \( \exists ! x.\ x\in A \wedge \phi (x) \)
shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \) corollary singleton_extract:
assumes \( \exists ! x.\ x\in A \)
shows \( (\bigcup A) \in A \)Definition of RestrictedTo:
\( M \text{ restricted to } X \equiv \{X \cap A .\ A \in M\} \)
lemma rel_compdef: shows \( \langle x,z\rangle \in r\circ s \longleftrightarrow (\exists y.\ \langle x,y\rangle \in s \wedge \langle y,z\rangle \in r) \)
Definition of Supersets:
\( \text{Supersets}(X,\mathcal{A} ) \equiv \{B\in Pow(X).\ \exists A\in \mathcal{A} .\ A\subseteq B\} \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8