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