section ‹Finite sets›
theory Finite1 imports ZF.EquivClass ZF.Finite func1 ZF1
begin
text‹This theory extends Isabelle standard ‹Finite› theory.
It is obsolete and should not be used for new development.
Use the ‹Finite_ZF› instead.›
subsection‹Finite powerset›
text‹In this section we consider various properties of ‹Fin›
datatype (even though there are no datatypes in ZF set theory).›
text‹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
"Prfin(T,A,M) ≡ ( (M = 0) | (∃N∈ Fin(T). ∀V∈ M. ∃ U∈ N. (V = U∩A)))"
text‹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: "∀ V∈ TA. ∃ U∈T. V=U∩A"
and A1: "W∈TA" and A2: "M∈ Fin(TA)"
and A3: "W∉M" and A4: "Prfin(T,A,M)"
shows "Prfin(T,A,cons(W,M))"
proof -
{ assume A7: "M=0" have "Prfin(T, A, cons(W, M))"
proof-
from A1 A obtain U where A5: "U∈T" and A6: "W=U∩A" by fast
let ?N = "{U}"
from A5 have T1: "?N ∈ Fin(T)" by simp
from A7 A6 have T2: "∀V∈ cons(W,M). ∃ U∈?N. V=U∩A" by simp
from A7 T1 T2 show "Prfin(T, A, cons(W, M))"
using Prfin_def by auto
qed }
moreover
{ assume A8:"M≠0" have "Prfin(T, A, cons(W, M))"
proof-
from A1 A obtain U where A5: "U∈T" and A6:"W=U∩A" by fast
from A8 A4 obtain N0
where A9: "N0∈ Fin(T)" and A10: "∀V∈ M. ∃ U0∈ N0. (V = U0∩A)"
using Prfin_def by auto
let ?N = "cons(U,N0)"
from A5 A9 have "?N ∈ Fin(T)" by simp
moreover from A10 A6 have "∀V∈ cons(W,M). ∃ U∈?N. V=U∩A" by simp
ultimately have "∃ N∈ Fin(T).∀V∈ cons(W,M). ∃ U∈N. V=U∩A" by auto
with A8 show "Prfin(T, A, cons(W, M))"
using Prfin_def by simp
qed }
ultimately show ?thesis by auto
qed
text‹Now we are ready to prove the statement we need.›
theorem FinRestr0: assumes A: "∀ V ∈ TA. ∃ U∈ T. V=U∩A"
shows "∀ M∈ Fin(TA). Prfin(T,A,M)"
proof -
{ fix M
assume "M ∈ Fin(TA)"
moreover have "Prfin(T,A,0)" using Prfin_def by simp
moreover
{ fix W M assume "W∈TA" "M∈ Fin(TA)" "W∉M" "Prfin(T,A,M)"
with A have "Prfin(T,A,cons(W,M))" by (rule ind_step) }
ultimately have "Prfin(T,A,M)" by (rule Fin_induct)
} thus ?thesis by simp
qed
text‹This is a different form of the above theorem:›
theorem ZF1FinRestr:
assumes A1:"M∈ Fin(TA)" and A2: "M≠0"
and A3: "∀ V∈ TA. ∃ U∈ T. V=U∩A"
shows "∃N∈ Fin(T). (∀V∈ M. ∃ U∈ N. (V = U∩A)) ∧ N≠0"
proof -
from A3 A1 have "Prfin(T,A,M)" using FinRestr0 by blast
then have "∃N∈ Fin(T). ∀V∈ M. ∃ U∈ N. (V = U∩A)"
using A2 Prfin_def by simp
then obtain N where
D1:"N∈ Fin(T) ∧ (∀V∈ M. ∃ U∈ N. (V = U∩A))" by auto
with A2 have "N≠0" by auto
with D1 show ?thesis by auto
qed
text‹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:"∃U V. (U∈T ∧ V∈T ∧ x∈U ∧ y∈V ∧ U∩V=0)"
shows "∃U∈T. (x∈U ∧ y∉U)"
proof -
from A obtain U V where D1:"U∈T ∧ V∈T ∧ x∈U ∧ y∈V ∧ U∩V=0" by auto
with D1 show ?thesis by auto
qed
text‹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:"∀A B. ((A∈C ∧ B∈C) ⟶ A∪B∈C)"
and A2: "A∈C" and A3: "N∈Fin(C)" and A4:"A∉N" and A5:"⋃N ∈ C"
shows "⋃cons(A,N) ∈ C"
proof -
have "⋃ cons(A,N) = A∪ ⋃N" by blast
with A1 A2 A5 show ?thesis by simp
qed
text‹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 ∈ C" and A2: "∀A B. ((A∈C ∧ B∈C) ⟶ A∪B∈C)" and
A3: "N∈ Fin(C)"
shows "⋃N∈C"
proof -
note A3
moreover from A1 have "⋃0 ∈ C" by simp
moreover
{ fix A N
assume "A∈C" "N∈Fin(C)" "A∉N" "⋃N ∈ C"
with A2 have "⋃cons(A,N) ∈ C" by (rule Finite1_L3_IndStep) }
ultimately show "⋃N∈ C" by (rule Fin_induct)
qed
text‹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
"IntPr(T,N) ≡ (N = 0 | ⋂N ∈ T)"
text‹The induction step.›
lemma Finite1_L4_IndStep:
assumes A1: "∀A B. ((A∈T ∧ B∈T) ⟶ A∩B∈T)"
and A2: "A∈T" and A3:"N∈Fin(T)" and A4:"A∉N" and A5:"IntPr(T,N)"
shows "IntPr(T,cons(A,N))"
proof -
{ assume A6: "N=0"
with A2 have "IntPr(T,cons(A,N))"
using IntPr_def by simp }
moreover
{ assume A7: "N≠0" have "IntPr(T, cons(A, N))"
proof -
from A7 A5 A2 A1 have "⋂N ∩ A ∈ T" using IntPr_def by simp
moreover from A7 have "⋂cons(A, N) = ⋂N ∩ A" by auto
ultimately show "IntPr(T, cons(A, N))" using IntPr_def by simp
qed }
ultimately show ?thesis by auto
qed
text‹The lemma.›
lemma Finite1_L4:
assumes A1: "∀A B. A∈T ∧ B∈T ⟶ A∩B ∈ T"
and A2: "N∈Fin(T)"
shows "IntPr(T,N)"
proof -
note A2
moreover have "IntPr(T,0)" using IntPr_def by simp
moreover
{ fix A N
assume "A∈T" "N∈Fin(T)" "A∉N" "IntPr(T,N)"
with A1 have "IntPr(T,cons(A,N))" by (rule Finite1_L4_IndStep) }
ultimately show "IntPr(T,N)" by (rule Fin_induct)
qed
text‹Next is a restatement of the above lemma that
does not depend on the IntPr meta-function.›
lemma Finite1_L5:
assumes A1: "∀A B. ((A∈T ∧ B∈T) ⟶ A∩B∈T)"
and A2: "N≠0" and A3: "N∈Fin(T)"
shows "⋂N ∈ T"
proof -
from A1 A3 have "IntPr(T,N)" using Finite1_L4 by simp
with A2 show ?thesis using IntPr_def by simp
qed
text‹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 "∀V∈B. K(V)∈C"
and "U∈B" and "N∈Fin(B)" and "U∉N" and "{K(V). V∈N}∈Fin(C)"
shows "{K(V). V∈cons(U,N)} ∈ Fin(C)"
using assms by simp
text‹The lemma:›
lemma fin_image_fin:
assumes A1: "∀V∈B. K(V)∈C" and A2: "N∈Fin(B)"
shows "{K(V). V∈N} ∈ Fin(C)"
proof -
note A2
moreover have "{K(V). V∈0} ∈ Fin(C)" by simp
moreover
{ fix U N
assume "U∈B" "N∈Fin(B)" "U∉N" "{K(V). V∈N}∈Fin(C)"
with A1 have "{K(V). V∈cons(U,N)} ∈ Fin(C)"
by (rule fin_image_fin_IndStep) }
ultimately show ?thesis by (rule Fin_induct)
qed
text‹The image of a finite set is finite.›
lemma Finite1_L6A: assumes A1: "f:X→Y" and A2: "N ∈ Fin(X)"
shows "f``(N) ∈ Fin(Y)"
proof -
from A1 have "∀x∈X. f`(x) ∈ Y"
using apply_type by simp
moreover note A2
ultimately have "{f`(x). x∈N} ∈ Fin(Y)"
by (rule fin_image_fin)
with A1 A2 show ?thesis
using FinD func_imagedef by simp
qed
text‹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: "∀x∈X. a(x) ∈ Y" and A2: "{b(y).y∈Y} ∈ Fin(Z)"
shows "{b(a(x)).x∈X} ∈ Fin(Z)"
proof -
from A1 have "{b(a(x)).x∈X} ⊆ {b(y).y∈Y}" by auto
with A2 show ?thesis using Fin_subset_lemma by blast
qed
text‹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: "∀y∈Y. b(y) ∈ Z" and A2: "{a(x). x∈X} ∈ Fin(Y)"
shows "{b(a(x)).x∈X} ∈ Fin(Z)"
proof -
let ?N = "{a(x). x∈X}"
from A1 A2 have "{b(y). y ∈ ?N} ∈ Fin(Z)"
by (rule fin_image_fin)
moreover have "{b(a(x)). x∈X} = {b(y). y∈ ?N}"
by auto
ultimately show ?thesis by simp
qed
text‹Cartesian product of finite sets is finite.›
lemma Finite1_L12: assumes A1: "A ∈ Fin(A)" and A2: "B ∈ Fin(B)"
shows "A×B ∈ Fin(A×B)"
proof -
have T1:"∀a∈A. ∀b∈B. {⟨ a,b⟩} ∈ Fin(A×B)" by simp
have "∀a∈A. {{⟨ a,b⟩}. b ∈ B} ∈ Fin(Fin(A×B))"
proof
fix a assume A3: "a ∈ A"
with T1 have "∀b∈B. {⟨ a,b⟩} ∈ Fin(A×B)"
by simp
moreover note A2
ultimately show "{{⟨ a,b⟩}. b ∈ B} ∈ Fin(Fin(A×B))"
by (rule fin_image_fin)
qed
then have "∀a∈A. ⋃ {{⟨ a,b⟩}. b ∈ B} ∈ Fin(A×B)"
using Fin_UnionI by simp
moreover have
"∀a∈A. ⋃ {{⟨ a,b⟩}. b ∈ B} = {a}× B" by blast
ultimately have "∀a∈A. {a}× B ∈ Fin(A×B)" by simp
moreover note A1
ultimately have "{{a}× B. a∈A} ∈ Fin(Fin(A×B))"
by (rule fin_image_fin)
then have "⋃{{a}× B. a∈A} ∈ Fin(A×B)"
using Fin_UnionI by simp
moreover have "⋃{{a}× B. a∈A} = A×B" by blast
ultimately show ?thesis by simp
qed
text‹We define the characterisic meta-function that is the identity
on a set and assigns a default value everywhere else.›
definition
"Characteristic(A,default,x) ≡ (if x∈A then x else default)"
text‹A finite subset is a finite subset of itself.›
lemma Finite1_L13:
assumes A1:"A ∈ Fin(X)" shows "A ∈ Fin(A)"
proof -
{ assume "A=0" hence "A ∈ Fin(A)" by simp }
moreover
{ assume A2: "A≠0" then obtain c where D1:"c∈A"
by auto
then have "∀x∈X. Characteristic(A,c,x) ∈ A"
using Characteristic_def by simp
moreover note A1
ultimately have
"{Characteristic(A,c,x). x∈A} ∈ Fin(A)" by (rule fin_image_fin)
moreover from D1 have
"{Characteristic(A,c,x). x∈A} = A" using Characteristic_def by simp
ultimately have "A ∈ Fin(A)" by simp }
ultimately show ?thesis by blast
qed
text‹Cartesian product of finite subsets is a finite subset of
cartesian product.›
lemma Finite1_L14: assumes A1: "A ∈ Fin(X)" "B ∈ Fin(Y)"
shows "A×B ∈ Fin(X×Y)"
proof -
from A1 have "A×B ⊆ X×Y" using FinD by auto
then have "Fin(A×B) ⊆ Fin(X×Y)" using Fin_mono by simp
moreover from A1 have "A×B ∈ Fin(A×B)"
using Finite1_L13 Finite1_L12 by simp
ultimately show ?thesis by auto
qed
text‹The next lemma is needed in the ‹Group_ZF_3› theory in a
couple of places.›
lemma Finite1_L15:
assumes A1: "{b(x). x∈A} ∈ Fin(B)" "{c(x). x∈A} ∈ Fin(C)"
and A2: "f : B×C→E"
shows "{f`⟨ b(x),c(x)⟩. x∈A} ∈ Fin(E)"
proof -
from A1 have "{b(x). x∈A}×{c(x). x∈A} ∈ Fin(B×C)"
using Finite1_L14 by simp
moreover have
"{⟨ b(x),c(x)⟩. x∈A} ⊆ {b(x). x∈A}×{c(x). x∈A}"
by blast
ultimately have T0: "{⟨ b(x),c(x)⟩. x∈A} ∈ Fin(B×C)"
by (rule Fin_subset_lemma)
with A2 have T1: "f``{⟨ b(x),c(x)⟩. x∈A} ∈ Fin(E)"
using Finite1_L6A by auto
from T0 have "∀x∈A. ⟨ b(x),c(x)⟩ ∈ B×C"
using FinD by auto
with A2 have
"f``{⟨ b(x),c(x)⟩. x∈A} = {f`⟨ b(x),c(x)⟩. x∈A}"
using func1_1_L17 by simp
with T1 show ?thesis by simp
qed
text‹Singletons are in the finite powerset.›
lemma Finite1_L16: assumes "x∈X" shows "{x} ∈ Fin(X)"
using assms emptyI consI by simp
text‹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∈A} ∈ Fin(B)"
and "c∈C" and "f : B×C→E"
shows "{f`⟨ b(x),c⟩. x∈A} ∈ Fin(E)"
proof -
from assms have
"∀y∈B. f`⟨y,c⟩ ∈ E"
"{b(x). x∈A} ∈ Fin(B)"
using apply_funtype by auto
then show ?thesis by (rule Finite1_L6C)
qed
text‹First order version of the induction for the finite powerset.›
lemma Finite1_L16B: assumes A1: "P(0)" and A2: "B∈Fin(X)"
and A3: "∀A∈Fin(X).∀x∈X. x∉A ∧ P(A)⟶P(A∪{x})"
shows "P(B)"
proof -
note ‹B∈Fin(X)› and ‹P(0)›
moreover
{ fix A x
assume "x ∈ X" "A ∈ Fin(X)" "x ∉ A" "P(A)"
moreover have "cons(x,A) = A∪{x}" by auto
moreover note A3
ultimately have "P(cons(x,A))" by simp }
ultimately show "P(B)" by (rule Fin_induct)
qed
subsection‹Finite range functions›
text‹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.
›
text‹Definition of finite range functions.›
definition
"FinRangeFunctions(X,Y) ≡ {f:X→Y. f``(X) ∈ Fin(Y)}"
text‹Constant functions have finite range.›
lemma Finite1_L17: assumes "c∈Y" and "X≠0"
shows "ConstantFunction(X,c) ∈ FinRangeFunctions(X,Y)"
using assms func1_3_L1 func_imagedef func1_3_L2 Finite1_L16
FinRangeFunctions_def by simp
text‹Finite range functions have finite range.›
lemma Finite1_L18: assumes "f ∈ FinRangeFunctions(X,Y)"
shows "{f`(x). x∈X} ∈ Fin(Y)"
using assms FinRangeFunctions_def func_imagedef by simp
text‹An alternative form of the definition of finite range functions.›
lemma Finite1_L19: assumes "f:X→Y"
and "{f`(x). x∈X} ∈ Fin(Y)"
shows "f ∈ FinRangeFunctions(X,Y)"
using assms func_imagedef FinRangeFunctions_def by simp
text‹A composition of a finite range function with another function is
a finite range function.›
lemma Finite1_L20: assumes A1:"f ∈ FinRangeFunctions(X,Y)"
and A2: "g : Y→Z"
shows "g O f ∈ FinRangeFunctions(X,Z)"
proof -
from A1 A2 have "g``{f`(x). x∈X} ∈ Fin(Z)"
using Finite1_L18 Finite1_L6A
by simp
with A1 A2 have "{(g O f)`(x). x∈X} ∈ Fin(Z)"
using FinRangeFunctions_def apply_funtype
func1_1_L17 comp_fun_apply by auto
with A1 A2 show ?thesis using
FinRangeFunctions_def comp_fun Finite1_L19
by auto
qed
text‹Image of any subset of the domain of a finite range function is finite.›
lemma Finite1_L21:
assumes "f ∈ FinRangeFunctions(X,Y)" and "A⊆X"
shows "f``(A) ∈ Fin(Y)"
proof -
from assms have "f``(X) ∈ Fin(Y)" "f``(A) ⊆ f``(X)"
using FinRangeFunctions_def func1_1_L8
by auto
then show "f``(A) ∈ Fin(Y)" using Fin_subset_lemma
by blast
qed
end