IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Finite1 imports ZF.EquivClass ZF.Finite func1 ZF1

begin

This theory extends Isabelle standard Finite theory. It is obsolete and should not be used for new development. Use the Finite_ZF instead.

Finite powerset

In this section we consider various properties of Fin datatype (even though there are no datatypes in ZF set theory).

In Topology_ZF theory we consider induced topology that is obtained by taking a subset of a topological space. To show that a topology restricted to a subset is also a topology on that subset we may need a fact that if \(T\) is a collection of sets and \(A\) is a set then every finite collection \(\{ V_i \}\) is of the form \(V_i=U_i \cap A\), where \(\{U_i\}\) is a finite subcollection of \(T\). This is one of those trivial facts that require suprisingly long formal proof. Actually, the need for this fact is avoided by requiring intersection two open sets to be open (rather than intersection of a finite number of open sets). Still, the fact is left here as an example of a proof by induction. We will use Fin_induct lemma from Finite.thy. First we define a property of finite sets that we want to show.

definition

\( \text{Prfin}(T,A,M) \equiv ( (M = 0) | (\exists N\in Fin(T).\ \forall V\in M.\ \exists U\in N.\ (V = U\cap A))) \)

Now we show the main induction step in a separate lemma. This will make the proof of the theorem FinRestr below look short and nice. The premises of the ind_step lemma are those needed by the main induction step in lemma Fin_induct (see standard Isabelle's Finite.thy).

lemma ind_step:

assumes A: \( \forall V\in TA.\ \exists U\in T.\ V=U\cap A \) and A1: \( W\in TA \) and A2: \( M\in Fin(TA) \) and A3: \( W\notin M \) and A4: \( \text{Prfin}(T,A,M) \)

shows \( \text{Prfin}(T,A,cons(W,M)) \)proof

{

assume A7: \( M=0 \)

have \( \text{Prfin}(T, A, cons(W, M)) \)proof

from A1, A obtain \( U \) where A5: \( U\in T \) and A6: \( W=U\cap A \)

let \( N = \{U\} \)

from A5 have T1: \( N \in Fin(T) \)

from A7, A6 have T2: \( \forall V\in cons(W,M).\ \exists U\in N.\ V=U\cap A \)

from A7, T1, T2 show \( \text{Prfin}(T, A, cons(W, M)) \) using Prfin_def

qed

}

moreover {

assume A8: \( M\neq 0 \)

have \( \text{Prfin}(T, A, cons(W, M)) \)proof

from A1, A obtain \( U \) where A5: \( U\in T \) and A6: \( W=U\cap A \)

from A8, A4 obtain \( N0 \) where A9: \( N0\in Fin(T) \) and A10: \( \forall V\in M.\ \exists U0\in N0.\ (V = U0\cap A) \) using Prfin_def

let \( N = cons(U,N0) \)

from A5, A9 have \( N \in Fin(T) \)

moreover

from A10, A6 have \( \forall V\in cons(W,M).\ \exists U\in N.\ V=U\cap A \)

ultimately have \( \exists N\in Fin(T).\ \forall V\in cons(W,M).\ \exists U\in N.\ V=U\cap A \)

with A8 show \( \text{Prfin}(T, A, cons(W, M)) \) using Prfin_def

qed

} ultimately show \( thesis \)

qed

Now we are ready to prove the statement we need.

theorem FinRestr0:

assumes A: \( \forall V \in TA.\ \exists U\in T.\ V=U\cap A \)

shows \( \forall M\in Fin(TA).\ \text{Prfin}(T,A,M) \)proof

{

fix \( M \)

assume \( M \in Fin(TA) \)

moreover

have \( \text{Prfin}(T,A,0) \) using Prfin_def

moreover {

fix \( W \) \( M \)

assume \( W\in TA \), \( M\in Fin(TA) \), \( W\notin M \), \( \text{Prfin}(T,A,M) \)

with A have \( \text{Prfin}(T,A,cons(W,M)) \) by (rule ind_step )

} ultimately have \( \text{Prfin}(T,A,M) \) by (rule Fin_induct )

}

thus \( thesis \)

qed

This is a different form of the above theorem:

theorem ZF1FinRestr:

assumes A1: \( M\in Fin(TA) \) and A2: \( M\neq 0 \) and A3: \( \forall V\in TA.\ \exists U\in T.\ V=U\cap A \)

shows \( \exists N\in Fin(T).\ (\forall V\in M.\ \exists U\in N.\ (V = U\cap A)) \wedge N\neq 0 \)proof

from A3, A1 have \( \text{Prfin}(T,A,M) \) using FinRestr0

then have \( \exists N\in Fin(T).\ \forall V\in M.\ \exists U\in N.\ (V = U\cap A) \) using A2, Prfin_def

then obtain \( N \) where D1: \( N\in Fin(T) \wedge (\forall V\in M.\ \exists U\in N.\ (V = U\cap A)) \)

with A2 have \( N\neq 0 \)

with D1 show \( thesis \)

qed

Purely technical lemma used in Topology_ZF_1 to show that if a topology is \(T_2\), then it is \(T_1\).

lemma Finite1_L2:

assumes A: \( \exists U V.\ (U\in T \wedge V\in T \wedge x\in U \wedge y\in V \wedge U\cap V=0) \)

shows \( \exists U\in T.\ (x\in U \wedge y\notin U) \)proof

from A obtain \( U \) \( V \) where D1: \( U\in T \wedge V\in T \wedge x\in U \wedge y\in V \wedge U\cap V=0 \)

with D1 show \( thesis \)

qed

A collection closed with respect to taking a union of two sets is closed under taking finite unions. Proof by induction with the induction step formulated in a separate lemma.

lemma Finite1_L3_IndStep:

assumes A1: \( \forall A B.\ ((A\in C \wedge B\in C) \longrightarrow A\cup B\in C) \) and A2: \( A\in C \) and A3: \( N\in Fin(C) \) and A4: \( A\notin N \) and A5: \( \bigcup N \in C \)

shows \( \bigcup cons(A,N) \in C \)proof

have \( \bigcup cons(A,N) = A\cup \bigcup N \)

with A1, A2, A5 show \( thesis \)

qed

The lemma: a collection closed with respect to taking a union of two sets is closed under taking finite unions.

lemma Finite1_L3:

assumes A1: \( 0 \in C \) and A2: \( \forall A B.\ ((A\in C \wedge B\in C) \longrightarrow A\cup B\in C) \) and A3: \( N\in Fin(C) \)

shows \( \bigcup N\in C \)proof

note A3

moreover

from A1 have \( \bigcup 0 \in C \)

moreover {

fix \( A \) \( N \)

assume \( A\in C \), \( N\in Fin(C) \), \( A\notin N \), \( \bigcup N \in C \)

with A2 have \( \bigcup cons(A,N) \in C \) by (rule Finite1_L3_IndStep )

} ultimately show \( \bigcup N\in C \) by (rule Fin_induct )

qed

A collection closed with respect to taking a intersection of two sets is closed under taking finite intersections. Proof by induction with the induction step formulated in a separate lemma. This is sligltly more involved than the union case in Finite1_L3, because the intersection of empty collection is undefined (or should be treated as such). To simplify notation we define the property to be proven for finite sets as a separate notion.

definition

\( \text{IntPr}(T,N) \equiv (N = 0 | \bigcap N \in T) \)

The induction step.

lemma Finite1_L4_IndStep:

assumes A1: \( \forall A B.\ ((A\in T \wedge B\in T) \longrightarrow A\cap B\in T) \) and A2: \( A\in T \) and A3: \( N\in Fin(T) \) and A4: \( A\notin N \) and A5: \( \text{IntPr}(T,N) \)

shows \( \text{IntPr}(T,cons(A,N)) \)proof

{

assume A6: \( N=0 \)

with A2 have \( \text{IntPr}(T,cons(A,N)) \) using IntPr_def

}

moreover {

assume A7: \( N\neq 0 \)

have \( \text{IntPr}(T, cons(A, N)) \)proof

from A7, A5, A2, A1 have \( \bigcap N \cap A \in T \) using IntPr_def

moreover

from A7 have \( \bigcap cons(A, N) = \bigcap N \cap A \)

ultimately show \( \text{IntPr}(T, cons(A, N)) \) using IntPr_def

qed

} ultimately show \( thesis \)

qed

The lemma.

lemma Finite1_L4:

assumes A1: \( \forall A B.\ A\in T \wedge B\in T \longrightarrow A\cap B \in T \) and A2: \( N\in Fin(T) \)

shows \( \text{IntPr}(T,N) \)proof

note A2

moreover

have \( \text{IntPr}(T,0) \) using IntPr_def

moreover {

fix \( A \) \( N \)

assume \( A\in T \), \( N\in Fin(T) \), \( A\notin N \), \( \text{IntPr}(T,N) \)

with A1 have \( \text{IntPr}(T,cons(A,N)) \) by (rule Finite1_L4_IndStep )

} ultimately show \( \text{IntPr}(T,N) \) by (rule Fin_induct )

qed

Next is a restatement of the above lemma that does not depend on the IntPr meta-function.

lemma Finite1_L5:

assumes A1: \( \forall A B.\ ((A\in T \wedge B\in T) \longrightarrow A\cap B\in T) \) and A2: \( N\neq 0 \) and A3: \( N\in Fin(T) \)

shows \( \bigcap N \in T \)proof

from A1, A3 have \( \text{IntPr}(T,N) \) using Finite1_L4

with A2 show \( thesis \) using IntPr_def

qed

The images of finite subsets by a meta-function are finite. For example in topology if we have a finite collection of sets, then closing each of them results in a finite collection of closed sets. This is a very useful lemma with many unexpected applications. The proof is by induction. The next lemma is the induction step.

lemma fin_image_fin_IndStep:

assumes \( \forall V\in B.\ K(V)\in C \) and \( U\in B \) and \( N\in Fin(B) \) and \( U\notin N \) and \( \{K(V).\ V\in N\}\in Fin(C) \)

shows \( \{K(V).\ V\in cons(U,N)\} \in Fin(C) \) using assms

The lemma:

lemma fin_image_fin:

assumes A1: \( \forall V\in B.\ K(V)\in C \) and A2: \( N\in Fin(B) \)

shows \( \{K(V).\ V\in N\} \in Fin(C) \)proof

note A2

moreover

have \( \{K(V).\ V\in 0\} \in Fin(C) \)

moreover {

fix \( U \) \( N \)

assume \( U\in B \), \( N\in Fin(B) \), \( U\notin N \), \( \{K(V).\ V\in N\}\in Fin(C) \)

with A1 have \( \{K(V).\ V\in cons(U,N)\} \in Fin(C) \) by (rule fin_image_fin_IndStep )

} ultimately show \( thesis \) by (rule Fin_induct )

qed

The image of a finite set is finite.

lemma Finite1_L6A:

assumes A1: \( f:X\rightarrow Y \) and A2: \( N \in Fin(X) \)

shows \( f(N) \in Fin(Y) \)proof

from A1 have \( \forall x\in X.\ f(x) \in Y \) using apply_type

moreover

note A2

ultimately have \( \{f(x).\ x\in N\} \in Fin(Y) \) by (rule fin_image_fin )

with A1, A2 show \( thesis \) using FinD, func_imagedef

qed

If the set defined by a meta-function is finite, then every set defined by a composition of this meta function with another one is finite.

lemma Finite1_L6B:

assumes A1: \( \forall x\in X.\ a(x) \in Y \) and A2: \( \{b(y).\ y\in Y\} \in Fin(Z) \)

shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \)proof

from A1 have \( \{b(a(x)).\ x\in X\} \subseteq \{b(y).\ y\in Y\} \)

with A2 show \( thesis \) using Fin_subset_lemma

qed

If the set defined by a meta-function is finite, then every set defined by a composition of this meta function with another one is finite.

lemma Finite1_L6C:

assumes A1: \( \forall y\in Y.\ b(y) \in Z \) and A2: \( \{a(x).\ x\in X\} \in Fin(Y) \)

shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \)proof

let \( N = \{a(x).\ x\in X\} \)

from A1, A2 have \( \{b(y).\ y \in N\} \in Fin(Z) \) by (rule fin_image_fin )

moreover

have \( \{b(a(x)).\ x\in X\} = \{b(y).\ y\in N\} \)

ultimately show \( thesis \)

qed

Cartesian product of finite sets is finite.

lemma Finite1_L12:

assumes A1: \( A \in Fin(A) \) and A2: \( B \in Fin(B) \)

shows \( A\times B \in Fin(A\times B) \)proof

have T1: \( \forall a\in A.\ \forall b\in B.\ \{\langle a,b\rangle \} \in Fin(A\times B) \)

have \( \forall a\in A.\ \{\{\langle a,b\rangle \}.\ b \in B\} \in Fin(Fin(A\times B)) \)proof

fix \( a \)

assume A3: \( a \in A \)

with T1 have \( \forall b\in B.\ \{\langle a,b\rangle \} \in Fin(A\times B) \)

moreover

note A2

ultimately show \( \{\{\langle a,b\rangle \}.\ b \in B\} \in Fin(Fin(A\times B)) \) by (rule fin_image_fin )

qed

then have \( \forall a\in A.\ \bigcup \{\{\langle a,b\rangle \}.\ b \in B\} \in Fin(A\times B) \) using Fin_UnionI

moreover

have \( \forall a\in A.\ \bigcup \{\{\langle a,b\rangle \}.\ b \in B\} = \{a\}\times B \)

ultimately have \( \forall a\in A.\ \{a\}\times B \in Fin(A\times B) \)

moreover

note A1

ultimately have \( \{\{a\}\times B.\ a\in A\} \in Fin(Fin(A\times B)) \) by (rule fin_image_fin )

then have \( \bigcup \{\{a\}\times B.\ a\in A\} \in Fin(A\times B) \) using Fin_UnionI

moreover

have \( \bigcup \{\{a\}\times B.\ a\in A\} = A\times B \)

ultimately show \( thesis \)

qed

We define the characterisic meta-function that is the identity on a set and assigns a default value everywhere else.

definition

\( \text{Characteristic}(A,\text{default},x) \equiv (\text{if }x\in A\text{ then }x\text{ else }\text{default}) \)

A finite subset is a finite subset of itself.

lemma Finite1_L13:

assumes A1: \( A \in Fin(X) \)

shows \( A \in Fin(A) \)proof

{

assume \( A=0 \)

hence \( A \in Fin(A) \)

}

moreover {

assume A2: \( A\neq 0 \)

then obtain \( c \) where D1: \( c\in A \)

then have \( \forall x\in X.\ \text{Characteristic}(A,c,x) \in A \) using Characteristic_def

moreover

note A1

ultimately have \( \{ \text{Characteristic}(A,c,x).\ x\in A\} \in Fin(A) \) by (rule fin_image_fin )

moreover

from D1 have \( \{ \text{Characteristic}(A,c,x).\ x\in A\} = A \) using Characteristic_def

ultimately have \( A \in Fin(A) \)

} ultimately show \( thesis \)

qed

Cartesian product of finite subsets is a finite subset of cartesian product.

lemma Finite1_L14:

assumes A1: \( A \in Fin(X) \), \( B \in Fin(Y) \)

shows \( A\times B \in Fin(X\times Y) \)proof

from A1 have \( A\times B \subseteq X\times Y \) using FinD

then have \( Fin(A\times B) \subseteq Fin(X\times Y) \) using Fin_mono

moreover

from A1 have \( A\times B \in Fin(A\times B) \) using Finite1_L13, Finite1_L12

ultimately show \( thesis \)

qed

The next lemma is needed in the Group_ZF_3 theory in a couple of places.

lemma Finite1_L15:

assumes A1: \( \{b(x).\ x\in A\} \in Fin(B) \), \( \{c(x).\ x\in A\} \in Fin(C) \) and A2: \( f : B\times C\rightarrow E \)

shows \( \{f\langle b(x),c(x)\rangle .\ x\in A\} \in Fin(E) \)proof

from A1 have \( \{b(x).\ x\in A\}\times \{c(x).\ x\in A\} \in Fin(B\times C) \) using Finite1_L14

moreover

have \( \{\langle b(x),c(x)\rangle .\ x\in A\} \subseteq \{b(x).\ x\in A\}\times \{c(x).\ x\in A\} \)

ultimately have T0: \( \{\langle b(x),c(x)\rangle .\ x\in A\} \in Fin(B\times C) \) by (rule Fin_subset_lemma )

with A2 have T1: \( f\{\langle b(x),c(x)\rangle .\ x\in A\} \in Fin(E) \) using Finite1_L6A

from T0 have \( \forall x\in A.\ \langle b(x),c(x)\rangle \in B\times C \) using FinD

with A2 have \( f\{\langle b(x),c(x)\rangle .\ x\in A\} = \{f\langle b(x),c(x)\rangle .\ x\in A\} \) using func1_1_L17

with T1 show \( thesis \)

qed

Singletons are in the finite powerset.

lemma Finite1_L16:

assumes \( x\in X \)

shows \( \{x\} \in Fin(X) \) using assms, emptyI, consI

A special case of Finite1_L15 where the second set is a singleton. In Group_ZF_3 theory this corresponds to the situation where we multiply by a constant.

lemma Finite1_L16AA:

assumes \( \{b(x).\ x\in A\} \in Fin(B) \) and \( c\in C \) and \( f : B\times C\rightarrow E \)

shows \( \{f\langle b(x),c\rangle .\ x\in A\} \in Fin(E) \)proof

from assms have \( \forall y\in B.\ f\langle y,c\rangle \in E \), \( \{b(x).\ x\in A\} \in Fin(B) \) using apply_funtype

then show \( thesis \) by (rule Finite1_L6C )

qed

First order version of the induction for the finite powerset.

lemma Finite1_L16B:

assumes A1: \( P(0) \) and A2: \( B\in Fin(X) \) and A3: \( \forall A\in Fin(X).\ \forall x\in X.\ x\notin A \wedge P(A)\longrightarrow P(A\cup \{x\}) \)

shows \( P(B) \)proof

note \( B\in Fin(X) \), and, \( P(0) \)

moreover {

fix \( A \) \( x \)

assume \( x \in X \), \( A \in Fin(X) \), \( x \notin A \), \( P(A) \)

moreover

have \( cons(x,A) = A\cup \{x\} \)

moreover

note A3

ultimately have \( P(cons(x,A)) \)

} ultimately show \( P(B) \) by (rule Fin_induct )

qed

Finite range functions

In this section we define functions \(f : X\rightarrow Y\), with the property that \(f(X)\) is a finite subset of \(Y\). Such functions play a important role in the construction of real numbers in the Real_ZF series.

Definition of finite range functions.

definition

\( \text{FinRangeFunctions}(X,Y) \equiv \{f:X\rightarrow Y.\ f(X) \in Fin(Y)\} \)

Constant functions have finite range.

lemma Finite1_L17:

assumes \( c\in Y \) and \( X\neq 0 \)

shows \( \text{ConstantFunction}(X,c) \in \text{FinRangeFunctions}(X,Y) \) using assms, func1_3_L1, func_imagedef, func1_3_L2, Finite1_L16, FinRangeFunctions_def

Finite range functions have finite range.

lemma Finite1_L18:

assumes \( f \in \text{FinRangeFunctions}(X,Y) \)

shows \( \{f(x).\ x\in X\} \in Fin(Y) \) using assms, FinRangeFunctions_def, func_imagedef

An alternative form of the definition of finite range functions.

lemma Finite1_L19:

assumes \( f:X\rightarrow Y \) and \( \{f(x).\ x\in X\} \in Fin(Y) \)

shows \( f \in \text{FinRangeFunctions}(X,Y) \) using assms, func_imagedef, FinRangeFunctions_def

A composition of a finite range function with another function is a finite range function.

lemma Finite1_L20:

assumes A1: \( f \in \text{FinRangeFunctions}(X,Y) \) and A2: \( g : Y\rightarrow Z \)

shows \( g\circ f \in \text{FinRangeFunctions}(X,Z) \)proof

from A1, A2 have \( g\{f(x).\ x\in X\} \in Fin(Z) \) using Finite1_L18, Finite1_L6A

with A1, A2 have \( \{(g\circ f)(x).\ x\in X\} \in Fin(Z) \) using FinRangeFunctions_def, apply_funtype, func1_1_L17, comp_fun_apply

with A1, A2 show \( thesis \) using FinRangeFunctions_def, comp_fun, Finite1_L19

qed

Image of any subset of the domain of a finite range function is finite.

lemma Finite1_L21:

assumes \( f \in \text{FinRangeFunctions}(X,Y) \) and \( A\subseteq X \)

shows \( f(A) \in Fin(Y) \)proof

from assms have \( f(X) \in Fin(Y) \), \( f(A) \subseteq f(X) \) using FinRangeFunctions_def, func1_1_L8

then show \( f(A) \in Fin(Y) \) using Fin_subset_lemma

qed

end

Definition of Prfin: \( \text{Prfin}(T,A,M) \equiv ( (M = 0) | (\exists N\in Fin(T).\ \forall V\in M.\ \exists U\in N.\ (V = U\cap A))) \)

lemma ind_step:

assumes \( \forall V\in TA.\ \exists U\in T.\ V=U\cap A \) and \( W\in TA \) and \( M\in Fin(TA) \) and \( W\notin M \) and \( \text{Prfin}(T,A,M) \)

shows \( \text{Prfin}(T,A,cons(W,M)) \)

theorem FinRestr0:

assumes \( \forall V \in TA.\ \exists U\in T.\ V=U\cap A \)

shows \( \forall M\in Fin(TA).\ \text{Prfin}(T,A,M) \)

lemma Finite1_L3_IndStep:

assumes \( \forall A B.\ ((A\in C \wedge B\in C) \longrightarrow A\cup B\in C) \) and \( A\in C \) and \( N\in Fin(C) \) and \( A\notin N \) and \( \bigcup N \in C \)

shows \( \bigcup cons(A,N) \in C \)

Definition of IntPr: \( \text{IntPr}(T,N) \equiv (N = 0 | \bigcap N \in T) \)

lemma Finite1_L4_IndStep:

assumes \( \forall A B.\ ((A\in T \wedge B\in T) \longrightarrow A\cap B\in T) \) and \( A\in T \) and \( N\in Fin(T) \) and \( A\notin N \) and \( \text{IntPr}(T,N) \)

shows \( \text{IntPr}(T,cons(A,N)) \)

lemma Finite1_L4:

assumes \( \forall A B.\ A\in T \wedge B\in T \longrightarrow A\cap B \in T \) and \( N\in Fin(T) \)

shows \( \text{IntPr}(T,N) \)

lemma fin_image_fin_IndStep:

assumes \( \forall V\in B.\ K(V)\in C \) and \( U\in B \) and \( N\in Fin(B) \) and \( U\notin N \) and \( \{K(V).\ V\in N\}\in Fin(C) \)

shows \( \{K(V).\ V\in cons(U,N)\} \in Fin(C) \)

lemma fin_image_fin:

assumes \( \forall V\in B.\ K(V)\in C \) and \( N \in \text{FinPow}(B) \)

shows \( \{K(V).\ V\in N\} \in \text{FinPow}(C) \)

lemma func_imagedef:

assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)

shows \( f(A) = \{f(x).\ x \in A\} \)

Definition of Characteristic: \( \text{Characteristic}(A,\text{default},x) \equiv (\text{if }x\in A\text{ then }x\text{ else }\text{default}) \)

lemma Finite1_L13:

assumes \( A \in Fin(X) \)

shows \( A \in Fin(A) \)

lemma Finite1_L12: