(* 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