Theory Finite1

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

section{*Finite powerset*}

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{*Here we define a restriction of a collection of sets to a given set. 
In romantic math this is typically denoted $X\cap M$ and means 
$\{X\cap A : A\in M \} $. Note there is also restrict$(f,A)$ 
defined for relations in ZF.thy.*}

constdefs
  RestrictedTo (infixl "{restricted to}" 70)
  "M {restricted to} X ≡ {X ∩ A . A ∈ M}"

text{*In @{text "Topology_ZF"}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.*} 

text{*We will use Fin\_induct lemma from Finite.thy. 
  First we define a property of
  finite sets that we want to show. *}

constdefs
  "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 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 (cases "M=0");
  assume A7: "M=0" show "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;
next;
  assume A8:"M≠0"; show "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;
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 A1: "M∈ Fin(TA)"
  have "Prfin(T,A,0)" using Prfin_def by simp;
  with A1 show "Prfin(T,A,M)" using ind_step by (rule Fin_induct);
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.*}

text{*The induction step:*}

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:*}

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 -;
  from A1 have "\<Union>0 ∈ C" by simp;
  with A3 show "\<Union>N∈ C" using Finite1_L3_IndStep 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 constdef.
*}

constdefs 
  "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 (cases "N=0")
  assume A6:"N=0" show "IntPr(T,cons(A,N))";
  proof-
    from A6 A2 show "IntPr(T, cons(A, N))" using IntPr_def by simp
  qed;
  next;
  assume A7:"N≠0" show "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;
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 -;
  have "IntPr(T,0)" using IntPr_def by simp;
  with A2 show "IntPr(T,N)"  using Finite1_L4_IndStep 
    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.*}

text{*The induction step:*}

lemma Finite1_L6_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 prems by simp;

text{*The lemma:*}

lemma Finite1_L6: assumes A1:"∀V∈B. K(V)∈C" and A2:"N∈Fin(B)"
  shows "{K(V). V∈N} ∈ Fin(C)"
proof -;
  have "{K(V). V∈0}∈Fin(C)" by simp;
  with A2 show ?thesis using Finite1_L6_IndStep 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 from A2 have "N∈Fin(X)" .;
  ultimately have "{f`(x). x∈N} ∈ Fin(Y)"
    by (rule Finite1_L6);
  with A1 A2 show ?thesis
    using FinD (*func_imagedef*) 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 Finite1_L6);
  moreover have "{b(a(x)). x∈X} = {b(y). y∈ ?N}" 
    by auto;
  ultimately show ?thesis by simp;
qed;

(*text{*Next is an interesting set identity that is I thought I needed to 
prove sufficient 
conditions for a collection of sets to be a base for some topology. 
Not used there, but perhaps finds its use somewhere else. 
This should be in ZF1.thy.*}

lemma Finite1_L7: assumes A1:"C∈B" 
  shows "\<Union>C = \<Union> \<Union> {A∈B. \<Union>C = \<Union>A}"
proof;
  from A1 show "\<Union>C ⊆ \<Union>\<Union>{A ∈ B . \<Union>C = \<Union>A}" by blast;
  show "\<Union>\<Union>{A ∈ B . \<Union>C = \<Union>A} ⊆ \<Union>C"
  proof;
    fix x assume A3:"x∈ \<Union>\<Union>{A ∈ B . \<Union>C = \<Union>A}" show "x∈\<Union>C";
    proof -;
      from A3 have "∃K. ∃A. (x∈K ∧ K∈A ∧ A∈B ∧ \<Union> C = \<Union> A)" by auto;
      then have "∃K. ∃A. (x∈\<Union>A ∧ \<Union> C = \<Union> A)" by auto;
      then obtain K A where "x∈\<Union>A ∧ \<Union> C = \<Union> A" by auto;
      thus "x∈\<Union>C" by simp;
    qed
  qed
qed;*)

text{*Next we show an identity that is used to prove sufficiency 
of some condition for 
a collection of sets to be a base for a topology. Should be in ZF1.thy.*}

lemma Finite1_L8: assumes A1:"∀U∈C. ∃A∈B. U = \<Union>A" 
  shows "\<Union>\<Union> {\<Union>{A∈B. U = \<Union>A}. U∈C} = \<Union>C"
proof;
  show "\<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A}) ⊆ \<Union>C" by blast;
  show "\<Union>C ⊆ \<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A})"
  proof;
    fix x assume A2:"x ∈ \<Union>C" 
    show "x∈ \<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A})"
    proof -;
      from A2 obtain U where D1:"U∈C ∧ x∈U" by auto;
      with A1 obtain A where D2:"A∈B ∧ U = \<Union>A" by auto;
      from D1 D2 show "x∈ \<Union>(\<Union>U∈C. \<Union>{A ∈ B . U = \<Union>A})" by auto;
    qed;
  qed;
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 (rule ccontr);
  assume A2: "¬ A ≠ 0" 
  with A1 show False by simp;
qed;

(*text{*A property of sets defined by separation(?). Should be in ZF1.thy.*}

lemma Finite1_L10: assumes A1:"B⊆A" 
  shows "{x ∈ A. p(x)} ∩ B = {x∈B. p(x)}"
proof -;
  from A1 show ?thesis by blast;
qed;*)

(*text{*Another property of sets defined by separation(?). 
  Should be in ZF1.thy.*}

lemma Finite1_L11: shows "{<x,y,z> ∈ X×Y×Z. D(x,y,z)} ⊆ X×Y×Z"
proof -;
  show ?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 from A2 have "B ∈ Fin(B)" .;
    ultimately show "{{<a,b>}. b ∈ B} ∈ Fin(Fin(A×B))"
      by (rule Finite1_L6)
  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 from A1 have "A ∈ Fin(A)" . 
  ultimately have "{{a}× B. a∈A} ∈ Fin(Fin(A×B))"
    by (rule Finite1_L6);
  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.*}

constdefs
  "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 (cases "A=0");
  assume "A=0" then show "A ∈ Fin(A)" by simp;
  next;
  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 from A1 have "A ∈ Fin(X)" .;
  ultimately have 
    "{Characteristic(A,c,x). x∈A} ∈ Fin(A)" 
    by (rule Finite1_L6);
  moreover from D1 have 
    "{Characteristic(A,c,x). x∈A} = A"
    using Characteristic_def by simp;
  ultimately show "A ∈ Fin(A)" by simp;
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 prems 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 A1: "{b(x). x∈A} ∈ Fin(B)" 
  and A2: "c∈C" and A3: "f : B×C->E"
  shows "{f`<b(x),c>. x∈A} ∈ Fin(E)"
proof -
  from prems 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{*In the IsarMathLib coding convention it is rather difficult to use
  results that take $\Longrightarrow$ (that is, another lemma) 
  as one of the assumptions. It is easier to use a condition written with
  the first order implication ($\longrightarrow$). The next lemma is the 
  induction step of the lemma about the first order induction.*}

lemma Finite1_L16A: 
  assumes "∀A∈Fin(X).∀x∈X. x∉A ∧ P(A)-->P(A∪{x})"
  and "x∈X" and "A∈Fin(X)" and "x∉A" and "P(A)"
  shows "P(cons(x,A))"
proof -;
  from prems have "P(A∪{x})" by simp;
  moreover have "cons(x,A) = A∪{x}" by auto;
  ultimately show ?thesis by simp;
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 -;
  from A1 have "P(0)" .;
  with A2 show  "P(B)" using Finite1_L16A 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 Real\_ZF\_x.thy series. *}

constdefs
  "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 prems  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 prems 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 prems 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 A1: "f ∈ FinRangeFunctions(X,Y)" and A2: "A⊆X"
  shows "f``(A) ∈ Fin(Y)" 
proof -
  from A1 A2 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