Theory Finite1

theory Finite1
imports Finite func1
(* 
This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2005, 2006 Slawomir Kolodynski

This program is free software; Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)


header{*\isaheader{Finite1.thy}*}

theory Finite1 imports Finite func1 ZF1

begin

text{*This theory extends Isabelle standard @{text "Finite"} theory.
It is obsolete and should not be used for new development.
Use the @{text "Finite_ZF"} instead. *}


section{*Finite powerset*}

text{*In this section we consider various properties of @{text "Fin"}
datatype (even though there are no datatypes in ZF set theory).*}


(*text{*Intersection of a collection is contained in every element
of the collection.*}
lemma ZF11: assumes A: "A ∈ M" shows "\<Inter>M ⊆ A";
proof
fix x;
assume A1: "x ∈ \<Inter>M"
from A1 A show "x ∈ A" ..
qed;

text{*Intersection of a nonempty collection $M$ of subsets of
$X$ is a subset of $X$. *}

lemma ZF12: assumes A1: "∀A∈ M. A⊆X" and A2:"M≠0"
shows "(\<Inter> M) ⊆ X";
proof -;
from A2 have "∀ A∈ M. (\<Inter> M ⊆ A)" using ZF11 by simp;
with A1 A2 show "(\<Inter> M) ⊆ X" by fast;
qed; *)



text{*In @{text "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 @{text "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 @{text "ind_step"} lemma are those needed by
the main induction step in
lemma @{text "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 @{text "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:"\<Union>N ∈ C"
shows "\<Union>cons(A,N) ∈ C"
proof -
have "\<Union> cons(A,N) = A∪ \<Union>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 "\<Union>N∈C"
proof -
note A3
moreover from A1 have "\<Union>0 ∈ C" by simp;
moreover
{ fix A N
assume "A∈C" "N∈Fin(C)" "A∉N" "\<Union>N ∈ C"
with A2 have "\<Union>cons(A,N) ∈ C" by (rule Finite1_L3_IndStep) }
ultimately show "\<Union>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 @{text "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 | \<Inter>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 "\<Inter>N ∩ A ∈ T" using IntPr_def by simp;
moreover from A7 have "\<Inter>cons(A, N) = \<Inter>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 "\<Inter>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{*If an intersection of a collection is not empty, then the collection is
not empty. We are (ab)using the fact the the intesection of empty collection
is defined to be empty and prove by contradiction. Should be in ZF1.thy*}


lemma Finite1_L9: assumes A1:"\<Inter>A ≠ 0" shows "A≠0"
proof -
{ assume A2: "¬ A ≠ 0"
with A1 have False by simp
} thus ?thesis by auto
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. \<Union> {{⟨ a,b⟩}. b ∈ B} ∈ Fin(A×B)"
using Fin_UnionI by simp;
moreover have
"∀a∈A. \<Union> {{⟨ 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 "\<Union>{{a}× B. a∈A} ∈ Fin(A×B)"
using Fin_UnionI by simp;
moreover have "\<Union>{{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 @{text "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 @{text "Finite1_L15"} where the second
set is a singleton. @{text "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;

section{*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 @{text "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