Theory func1

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written 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{func1.thy}*}
theory func1 imports func Fol1 ZF1

begin

text{*We define the notion of function that preserves a collection here.
Given two collection of sets a function preserves the collections if 
the inverse image of sets in one collection belongs to the second one.
This notion does not have a name in romantic math. It is used to define 
continuous functions in @{text "Topology_ZF_2"} theory. 
We define it here so that we can 
use it for other purposes, like defining measurable functions.
Recall that @{text "f-``(A)"} means the inverse image of the set $A$.*}

constdefs
  "PresColl(f,S,T) ≡ ∀ A∈T. f-``(A)∈S";

section{*Properties of functions, function spaces and (inverse) images.*}

text{*If a function maps $A$ into another set, then $A$ is the 
  domain of the function.*}

lemma func1_1_L1: assumes "f:A->C" shows "domain(f) = A"
  using prems domain_of_fun by simp;

text{*A first-order version of @{text "Pi_type"}. *}

lemma func1_1_L1A: assumes A1: "f:X->Y" and A2: "∀x∈X. f`(x) ∈ Z"
  shows "f:X->Z"
proof -
  { fix x assume "x∈X" 
    with A2 have "f`(x) ∈ Z" by simp };
  with A1 show "f:X->Z" by (rule Pi_type);
qed;

text{*There is a value for each argument.*}

lemma func1_1_L2: assumes A1: "f:X->Y"  "x∈X" 
  shows "∃y∈Y. <x,y> ∈ f";  
proof-
  from A1 have "f`(x) ∈ Y" using apply_type by simp;
  moreover from A1 have "<x,f`(x)>∈ f" using apply_Pair by simp;
  ultimately show ?thesis by auto;
qed;

text{*Inverse image of any set is contained in the domain.*}

lemma func1_1_L3: assumes A1: "f:X->Y" shows "f-``(D) ⊆ X"
proof-;
   have "∀x. x∈f-``(D) --> x∈domain(f)"
      using  vimage_iff domain_iff by auto;
    with A1 have "∀x. (x ∈ f-``(D)) --> (x∈X)" using func1_1_L1 by simp
    then show ?thesis by auto;
qed;

text{*The inverse image of the range is the domain.*}

lemma func1_1_L4: assumes "f:X->Y" shows "f-``(Y) = X"
  using prems func1_1_L3 func1_1_L2 vimage_iff by blast;

text{*The arguments belongs to the domain and values to the range.*}

lemma func1_1_L5: 
  assumes A1: "<x,y> ∈ f" and A2: "f:X->Y"  
  shows "x∈X ∧ y∈Y" 
proof
  from A1 A2 show "x∈X" using apply_iff by simp;
  with A2 have "f`(x)∈ Y" using apply_type by simp;
  with A1 A2 show "y∈Y" using apply_iff by simp;
qed;

text{*The (argument, value) pair belongs to the graph of the function.*}

lemma func1_1_L5A: 
  assumes A1: "f:X->Y" "x∈X" "y = f`(x)"
  shows "<x,y> ∈ f" "y ∈ range(f)" 
proof -;
  from A1 show "<x,y> ∈ f" using apply_Pair by simp;
  then show "y ∈ range(f)" using rangeI by simp;
qed;

text{*The range of function thet maps $X$ into $Y$ is contained in $Y$.*}

lemma func1_1_L5B: 
  assumes  A1:"f:X->Y" shows "range(f) ⊆ Y"
proof;
  fix y assume "y ∈ range(f)"
  then obtain x where "<x,y> ∈ f"
    using range_def converse_def domain_def by auto;
  with A1 show "y∈Y" using func1_1_L5 by blast;
qed;

text{*The image of any set is contained in the range.*}

lemma func1_1_L6: assumes A1: "f:X->Y" 
  shows "f``(B) ⊆ range(f)"   "f``(B) ⊆ Y"
proof -
  show "f``(B) ⊆ range(f)" using image_iff rangeI by auto;
  with A1 show "f``(B) ⊆ Y" using func1_1_L5B by blast;
qed;

text{*The inverse image of any set is contained in the domain.*}

lemma func1_1_L6A: assumes A1: "f:X->Y" shows "f-``(A)⊆X"
proof;
  fix x
  assume A2: "x∈f-``(A)" then obtain y where "<x,y> ∈ f" 
    using vimage_iff by auto;
  with A1 show  "x∈X" using func1_1_L5 by fast;
qed;

text{*Inverse image of a greater set is greater.*}

lemma func1_1_L7: assumes "A⊆B" and "function(f)" 
  shows "f-``(A)⊆ f-``(B)" using prems function_vimage_Diff by auto;


text{*Image of a greater set is greater.*}

lemma func1_1_L8: assumes A1: "A⊆B"  shows "f``(A)⊆ f``(B)"
  using prems image_Un by auto;

text{* A set is contained in the the inverse image of its image.
  There is similar theorem in @{text "equalities.thy"}
  (@{text "function_image_vimage"})
  which shows that the image of inverse image of a set 
  is contained in the set.*}

lemma func1_1_L9: assumes A1: "f:X->Y" and A2: "A⊆X"
  shows "A ⊆ f-``(f``(A))"
proof -
  from A1 A2 have "∀x∈A. <x,f`(x)> ∈ f"  using apply_Pair by auto;
  then show ?thesis using image_iff by auto;
qed

text{*A technical lemma needed to make the @{text "func1_1_L11"} 
  proof more clear.*}

lemma func1_1_L10: 
  assumes A1: "f ⊆ X×Y" and A2: "∃!y. (y∈Y & <x,y> ∈ f)"
  shows "∃!y. <x,y> ∈ f"
proof;
  from A2 show "∃y. ⟨x, y⟩ ∈ f" by auto;
  fix y n assume "<x,y> ∈ f" and "<x,n> ∈ f"
  with A1 A2 show "y=n" by auto;
qed;


text{*If $f\subseteq X\times Y$ and for every $x\in X$ there is exactly 
one $y\in Y$ such that $(x,y)\in f$ then $f$ maps $X$ to $Y$.*}

lemma func1_1_L11: 
  assumes "f ⊆ X×Y" and "∀x∈X. ∃!y. y∈Y & <x,y> ∈ f"
  shows "f: X->Y" using prems func1_1_L10 Pi_iff_old by simp;

text{*A set defined by a lambda-type expression is a fuction. There is a 
  similar lemma in func.thy, but I had problems with lamda expressions syntax
  so I could not apply it. This lemma is a workaround this. Besides, lambda 
  expressions are not readable.
  *}

lemma func1_1_L11A: assumes A1: "∀x∈X. b(x)∈Y"
  shows "{<x,y> ∈ X×Y. b(x) = y} : X->Y"
proof -;
  let ?f = "{<x,y> ∈ X×Y. b(x) = y}"
  have "?f ⊆ X×Y" by auto;
  moreover have "∀x∈X. ∃!y. y∈Y & <x,y> ∈ ?f"
  proof;
    fix x assume A2: "x∈X"
    show "∃!y. y∈Y ∧ ⟨x, y⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"
    proof;
      def y ≡ "b(x)";
      with A2 A1 show 
        "∃y. y∈Y & ⟨x, y⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"
        by simp;
    next
      fix y y1
      assume "y∈Y ∧ ⟨x, y⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"
        and "y1∈Y ∧ ⟨x, y1⟩ ∈ {⟨x,y⟩ ∈ X×Y . b(x) = y}"
      then show "y = y1" by simp;
    qed;
  qed;
  ultimately show "{<x,y> ∈ X×Y. b(x) = y} : X->Y" 
    using func1_1_L11 by simp;
qed;

text{*The next lemma will replace @{text "func1_1_L11A"} one day.*}

lemma ZF_fun_from_total: assumes A1: "∀x∈X. b(x)∈Y"
  shows "{⟨x,b(x)⟩. x∈X} : X->Y"
proof -
  let ?f = "{⟨x,b(x)⟩. x∈X}"
  { fix x assume A2: "x∈X"
    have "∃!y. y∈Y ∧ ⟨x, y⟩ ∈ ?f"
    proof;
      def y ≡ "b(x)"
      with A1 A2 show "∃y. y∈Y ∧ ⟨x, y⟩ ∈ ?f"
        by simp;
    next fix y y1 assume "y∈Y ∧ ⟨x, y⟩ ∈ ?f"
        and "y1∈Y ∧ ⟨x, y1⟩ ∈ ?f"
      then show "y = y1" by simp;
    qed;
  } then have "∀x∈X. ∃!y. y∈Y ∧ <x,y> ∈ ?f"
    by simp;
  moreover from A1 have "?f ⊆ X×Y" by auto;
  ultimately show ?thesis using func1_1_L11
    by simp;
qed;
 
text{*The value of a function defined by a meta-function is this 
  meta-function.*}

lemma func1_1_L11B: 
  assumes A1: "f:X->Y"   "x∈X"
  and A2: "f = {<x,y> ∈ X×Y. b(x) = y}"
  shows "f`(x) = b(x)"
proof -;
  from A1 have "<x,f`(x)> ∈ f" using apply_iff by simp;
  with A2 show ?thesis by simp;
qed;

text{*The next lemma will replace @{text "func1_1_L11B"} one day.*}

lemma ZF_fun_from_tot_val: 
  assumes A1: "f:X->Y"   "x∈X"
  and A2: "f = {⟨x,b(x)⟩. x∈X}"
  shows "f`(x) = b(x)"
proof -
  from A1 have "<x,f`(x)> ∈ f" using apply_iff by simp;
   with A2 show ?thesis by simp;
qed;

text{*We can extend a function by specifying its values on a set
  disjoint with the domain.*}

lemma func1_1_L11C: assumes A1: "f:X->Y" and A2: "∀x∈A. b(x)∈B"
  and A3: "X∩A = 0" and Dg : "g = f ∪ {⟨x,b(x)⟩. x∈A}"
  shows 
  "g : X∪A -> Y∪B"
  "∀x∈X. g`(x) = f`(x)"
  "∀x∈A. g`(x) = b(x)"
proof -
  let ?h = "{⟨x,b(x)⟩. x∈A}"
  from A1 A2 A3 have 
    I: "f:X->Y"  "?h : A->B"  "X∩A = 0"
    using ZF_fun_from_total by auto;
  then have "f∪?h : X∪A -> Y∪B"
    by (rule fun_disjoint_Un);
  with Dg show "g : X∪A -> Y∪B" by simp;
  { fix x assume A4: "x∈A"
    with A1 A3 have "(f∪?h)`(x) = ?h`(x)"
      using func1_1_L1 fun_disjoint_apply2
      by blast;
    moreover from I A4 have "?h`(x) = b(x)"
      using ZF_fun_from_tot_val by simp
    ultimately have "(f∪?h)`(x) = b(x)"
      by simp;
  } with Dg show "∀x∈A. g`(x) = b(x)" by simp;
  { fix x assume A5: "x∈X"
    with A3 I have "x ∉ domain(?h)"
      using func1_1_L1 by auto;
    then have "(f∪?h)`(x) = f`(x)"
      using fun_disjoint_apply1 by simp;
  } with Dg show "∀x∈X. g`(x) = f`(x)" by simp;
qed;

text{*We can extend a function by specifying its value at a point that
  does not belong to the domain.*}

lemma func1_1_L11D: assumes A1: "f:X->Y" and A2: "a∉X"
  and Dg: "g = f ∪ {⟨a,b⟩}"
  shows 
  "g : X∪{a} -> Y∪{b}"
  "∀x∈X. g`(x) = f`(x)"
  "g`(a) = b"
proof -
  let ?h = "{⟨a,b⟩}"
  from A1 A2 Dg have I:
    "f:X->Y"  "∀x∈{a}. b∈{b}"  "X∩{a} = 0"  "g = f ∪ {⟨x,b⟩. x∈{a}}"
    by auto;
  then show "g : X∪{a} -> Y∪{b}"
    by (rule func1_1_L11C);
  from I show "∀x∈X. g`(x) = f`(x)"
    by (rule func1_1_L11C)
  from I have "∀x∈{a}. g`(x) = b"
    by (rule func1_1_L11C);
  then show "g`(a) = b" by auto;
qed;

text{*A technical lemma about extending a function both by defining
  on a set disjoint with the domain and on a point that does not belong
  to any of those sets.*}

lemma func1_1_L11E:
  assumes A1: "f:X->Y" and 
  A2: "∀x∈A. b(x)∈B" and 
  A3: "X∩A = 0" and A4: "a∉ X∪A"
  and Dg: "g = f ∪ {⟨x,b(x)⟩. x∈A} ∪ {⟨a,c⟩}"
  shows
  "g : X∪A∪{a} -> Y∪B∪{c}"
  "∀x∈X. g`(x) = f`(x)"
  "∀x∈A. g`(x) = b(x)"
  "g`(a) = c"
proof -
  let ?h = "f ∪ {⟨x,b(x)⟩. x∈A}"
  from prems show "g : X∪A∪{a} -> Y∪B∪{c}"
    using func1_1_L11C func1_1_L11D by simp;
  from A1 A2 A3 have I:
    "f:X->Y"  "∀x∈A. b(x)∈B"  "X∩A = 0"  "?h = f ∪ {⟨x,b(x)⟩. x∈A}"
    by auto
  from prems have 
    II: "?h : X∪A -> Y∪B"  "a∉ X∪A"  "g = ?h ∪ {⟨a,c⟩}"
    using func1_1_L11C by auto;
  then have III: "∀x∈X∪A. g`(x) = ?h`(x)" by (rule func1_1_L11D);
  moreover from I have  "∀x∈X. ?h`(x) = f`(x)"
    by (rule func1_1_L11C);
  ultimately show "∀x∈X. g`(x) = f`(x)" by simp;
  from I have "∀x∈A. ?h`(x) = b(x)" by (rule func1_1_L11C);
  with III show "∀x∈A. g`(x) = b(x)" by simp;
  from II show "g`(a) = c" by (rule func1_1_L11D);
qed;

text{*The inverse image of an intersection of a nonempty collection of sets 
  is the intersection of the 
  inverse images. This generalizes @{text "function_vimage_Int"} 
  which is proven for the case of two sets.*}

lemma  func1_1_L12:
  assumes A1: "B⊆Pow(Y)" and A2: "B≠0" and A3: "f:X->Y"
  shows "f-``(\<Inter>B) = (\<Inter>U∈B. f-``(U))"
proof;
  from A2 show  "f-``(\<Inter>B) ⊆ (\<Inter>U∈B. f-``(U))" by blast;
  show "(\<Inter>U∈B. f-``(U)) ⊆ f-``(\<Inter>B)"
  proof;
    fix x assume A4: "x ∈ (\<Inter>U∈B. f-``(U))";
    from A3 have "∀U∈B. f-``(U) ⊆ X" using func1_1_L6A by simp;
    with A4 have "∀U∈B. x∈X" by auto;
    with A2 have "x∈X" by auto;
    with A3 have "∃!y. <x,y> ∈ f" using Pi_iff_old by simp;
    with A2 A4 show "x ∈ f-``(\<Inter>B)" using vimage_iff by blast;
  qed
qed;

text{*If the inverse image of a set is not empty, then the set is not empty.
  Proof by contradiction.*}

lemma func1_1_L13: assumes A1:"f-``(A)≠0" shows "A≠0"
proof (rule ccontr);
  assume A2:"¬ A ≠ 0" from A2 A1 show False by simp;
qed;

text{*If the image of a set is not empty, then the set is not empty.
  Proof by contradiction.*}

lemma func1_1_L13A: assumes A1: "f``(A)≠0" shows "A≠0"
proof (rule ccontr);
  assume A2:"¬ A ≠ 0" from A2 A1 show False by simp;
qed;

text{*What is the inverse image of a singleton?*}

lemma func1_1_L14: assumes "f∈X->Y" 
  shows "f-``({y}) = {x∈X. f`(x) = y}" 
  using prems func1_1_L6A vimage_singleton_iff apply_iff by auto;

text{* A more familiar definition of inverse image.*}

lemma func1_1_L15: assumes A1: "f:X->Y"
  shows "f-``(A) = {x∈X. f`(x) ∈ A}"
proof -;
  have "f-``(A) = (\<Union>y∈A . f-``{y})" 
    by (rule vimage_eq_UN);
  with A1 show ?thesis using func1_1_L14 by auto;
qed;

text{*A more familiar definition of image.*}
(*This can not be always replaced by image_fun from standard func.thy.*)
lemma func_imagedef: assumes A1: "f:X->Y" and A2: "A⊆X"
  shows "f``(A) = {f`(x). x ∈ A}"
proof;
 from A1 show "f``(A) ⊆ {f`(x). x ∈ A}"
   using image_iff apply_iff by auto;
 show "{f`(x). x ∈ A} ⊆ f``(A)"
 proof;
   fix y assume "y ∈ {f`(x). x ∈ A}"
   then obtain x where "x∈A ∧ y = f`(x)"
     by auto;
   with A1 A2 show "y ∈ f``(A)"
     using apply_iff image_iff by auto;
 qed;
qed;

text{*The image of an intersection is contained in the 
  intersection of the images.*}

lemma image_of_Inter: assumes  A1: "f:X->Y" and
  A2: "I≠0" and A3: "∀i∈I. P(i) ⊆ X"
  shows "f``(\<Inter>i∈I. P(i)) ⊆ ( \<Inter>i∈I. f``(P(i)) )"
proof;
  fix y assume A4: "y ∈ f``(\<Inter>i∈I. P(i))"
  from A1 A2 A3 have "f``(\<Inter>i∈I. P(i)) = {f`(x). x ∈ ( \<Inter>i∈I. P(i) )}"
    using ZF1_1_L7 func_imagedef by simp;
  with A4 obtain x where "x ∈ ( \<Inter>i∈I. P(i) )" and "y = f`(x)"
    by auto;
  with A1 A2 A3 show "y ∈ ( \<Inter>i∈I. f``(P(i)) )" using func_imagedef
    by auto;
qed;
  
text{*The image of a nonempty subset of domain is nonempty.*}

lemma func1_1_L15A: 
  assumes A1: "f: X->Y" and A2: "A⊆X" and A3: "A≠0"
  shows "f``(A) ≠ 0"
proof -
  from A3 obtain x where "x∈A" by auto
  with A1 A2 have "f`(x) ∈ f``(A)"
    using func_imagedef by auto;
  then show "f``(A) ≠ 0" by auto;
qed;

text{*The next lemma allows to prove statements about the values in the
  domain of a function given a statement about values in the range.*}

lemma func1_1_L15B: 
  assumes "f:X->Y" and "A⊆X" and "∀y∈f``(A). P(y)"
  shows "∀x∈A. P(f`(x))"
  using prems func_imagedef by simp;
  
text{*An image of an image is the image of a composition.*}

lemma func1_1_L15C: assumes  A1: "f:X->Y" and A2: "g:Y->Z"
  and A3: "A⊆X"
  shows 
  "g``(f``(A)) =  {g`(f`(x)). x∈A}"
  "g``(f``(A)) = (g O f)``(A)"
proof -
  from A1 A3 have "{f`(x). x∈A} ⊆ Y"
    using apply_funtype by auto;
  with A2 have "g``{f`(x). x∈A} = {g`(f`(x)). x∈A}"
    using func_imagedef by auto;
  with A1 A3 show I: "g``(f``(A)) =  {g`(f`(x)). x∈A}" 
    using func_imagedef by simp;
  from A1 A3 have "∀x∈A. (g O f)`(x) = g`(f`(x))"
    using comp_fun_apply by auto;
  with I have "g``(f``(A)) = {(g O f)`(x). x∈A}"
    by simp;
  moreover from A1 A2 A3 have "(g O f)``(A) = {(g O f)`(x). x∈A}"
    using comp_fun func_imagedef by blast;
  ultimately show "g``(f``(A)) = (g O f)``(A)"
    by simp;
qed;

text{*If an element of the domain of a function belongs to a set, 
  then its value belongs to the imgage of that set.*}

lemma func1_1_L15D: assumes "f:X->Y"  "x∈A"  "A⊆X"
  shows "f`(x) ∈ f``(A)"
  using prems func_imagedef by auto;
  
text{*What is the image of a set defined by a meta-fuction?*}

lemma func1_1_L17: 
  assumes A1: "f ∈ X->Y" and A2: "∀x∈A. b(x) ∈ X"
  shows "f``({b(x). x∈A}) = {f`(b(x)). x∈A}"
proof -;
  from A2 have "{b(x). x∈A} ⊆ X" by auto;
  with A1 show ?thesis using func_imagedef by auto;
qed;

text{*What are the values of composition of three functions?*}

lemma func1_1_L18: assumes A1: "f:A->B"  "g:B->C"  "h:C->D"
  and A2: "x∈A"
  shows
  "(h O g O f)`(x) ∈ D"
  "(h O g O f)`(x) = h`(g`(f`(x)))"  
proof -
  from A1 have "(h O g O f) : A->D"
    using comp_fun by blast;
  with A2 show "(h O g O f)`(x) ∈ D" using apply_funtype
    by simp;
  from A1 A2 have "(h O g O f)`(x) = h`( (g O f)`(x))"
    using comp_fun comp_fun_apply by blast;
  with A1 A2 show "(h O g O f)`(x) = h`(g`(f`(x)))"
    using comp_fun_apply by simp;
qed;

section{*Functions restricted to a set*}
 
text{*What is the inverse image of a set under a restricted fuction?*}

lemma func1_2_L1: assumes A1: "f:X->Y" and A2: "B⊆X"
  shows "restrict(f,B)-``(A) = f-``(A) ∩ B"
proof -;
  let ?g = "restrict(f,B)";
  from A1 A2 have "?g:B->Y" 
    using restrict_type2 by simp;
  with A2 A1 show "?g-``(A) = f-``(A) ∩ B"
    using func1_1_L15 restrict_if by auto;
qed;
   
text{*A criterion for when one function is a restriction of another.
  The lemma below provides a result useful in the actual proof of the 
  criterion and applications.*}

lemma func1_2_L2: 
  assumes A1: "f:X->Y" and A2: "g ∈ A->Z" 
  and A3: "A⊆X" and A4: "f ∩ A×Z = g"
  shows "∀x∈A. g`(x) = f`(x)"
proof;
  fix x assume "x∈A"
  with A2 have "<x,g`(x)> ∈ g" using apply_Pair by simp;
  with A4 A1 show "g`(x) = f`(x)"  using apply_iff by auto; 
qed;

text{*Here is the actual criterion.*}

lemma func1_2_L3: 
  assumes A1: "f:X->Y" and A2: "g:A->Z" 
  and A3: "A⊆X" and A4: "f ∩ A×Z = g"
  shows "g = restrict(f,A)"
proof;
  from A4 show "g ⊆ restrict(f, A)" using restrict_iff by auto;
  show "restrict(f, A) ⊆ g"
  proof;
    fix z assume A5:"z ∈ restrict(f,A)"
    then obtain x y where D1:"z∈f & x∈A  & z = <x,y>"
      using restrict_iff by auto;
    with A1 have "y = f`(x)" using apply_iff by auto;
    with A1 A2 A3 A4 D1 have "y = g`(x)" using func1_2_L2 by simp;
    with A2 D1 show "z∈g" using apply_Pair by simp;
  qed;
qed;

text{*Which function space a restricted function belongs to?*}

lemma func1_2_L4: 
  assumes A1: "f:X->Y" and A2: "A⊆X" and A3: "∀x∈A. f`(x) ∈ Z"
  shows "restrict(f,A) : A->Z"
proof -;
  let ?g = "restrict(f,A)"
  from A1 A2 have "?g : A->Y" 
    using restrict_type2 by simp;
  moreover { 
    fix x assume "x∈A" 
    with A1 A3 have "?g`(x) ∈ Z" using restrict by simp};
  ultimately show ?thesis by (rule Pi_type);
qed;

section{*Constant functions*}

text{*We define constant($=c$) functions on a set $X$  in a natural way as 
  ConstantFunction$(X,c)$. *}

constdefs
  "ConstantFunction(X,c) ≡ X×{c}"

text{*Constant function belongs to the function space.*}

lemma func1_3_L1: 
  assumes A1: "c∈Y" shows "ConstantFunction(X,c) : X->Y"
proof -;
   from A1 have "X×{c} = {<x,y> ∈ X×Y. c = y}" 
     by auto;
   with A1 show ?thesis using func1_1_L11A ConstantFunction_def
     by simp;
qed;

text{*Constant function is equal to the constant on its domain.*}

lemma func1_3_L2: assumes A1: "x∈X"
  shows "ConstantFunction(X,c)`(x) = c"
proof -;
  have "ConstantFunction(X,c) ∈ X->{c}"
    using func1_3_L1 by simp;
  moreover from A1 have "<x,c> ∈ ConstantFunction(X,c)"
    using ConstantFunction_def by simp;
  ultimately show ?thesis using apply_iff by simp;
qed;

section{*Injections, surjections, bijections etc.*}

text{*In this section we prove the properties of the spaces
  of injections, surjections and bijections that we can't find in the
  standard Isabelle's @{text "Perm.thy"}.*}

text{*The domain of a bijection between $X$ and $Y$ is $X$.*}

lemma domain_of_bij: 
  assumes A1: "f ∈ bij(X,Y)" shows "domain(f) = X"
proof -
  from A1 have "f:X->Y" using bij_is_fun by simp;
  then show "domain(f) = X" using func1_1_L1 by simp;
qed;

text{*The value of the inverse of an injection on a point of the image 
  of a set belongs to that set.*}

lemma inj_inv_back_in_set: 
  assumes A1: "f ∈ inj(A,B)" and A2: "C⊆A" and A3: "y ∈ f``(C)"
  shows 
  "converse(f)`(y) ∈ C"
  "f`(converse(f)`(y)) = y"
proof -
  from A1 have I: "f:A->B" using inj_is_fun by simp;
  with A2 A3 obtain x where II: "x∈C"   "y = f`(x)"
    using func_imagedef by auto;
  with A1 A2 show "converse(f)`(y) ∈ C" using left_inverse
    by auto;
  from A1 A2 I II show "f`(converse(f)`(y)) = y"
    using func1_1_L5A right_inverse by auto;
qed;

text{*For injections if a value at a point 
  belongs to the image of a set, then the point
  belongs to the set. *}

lemma inj_point_of_image: 
  assumes A1: "f ∈ inj(A,B)" and A2: "C⊆A" and
  A3: "x∈A" and A4: "f`(x) ∈ f``(C)"
  shows "x ∈ C"
proof -
  from A1 A2 A4 have "converse(f)`(f`(x)) ∈ C"
    using inj_inv_back_in_set by simp;
  moreover from A1 A3 have "converse(f)`(f`(x)) = x"
    using left_inverse_eq by simp;
  ultimately show "x ∈ C" by simp;
qed;

(*text{*The value of the converse on a point in range is in the domain
  of an injection.*}

lemma inj_conv_aply_type: assumes "f ∈ inj(A,B)" and "y ∈ range(f)"
  shows "converse(f)`(y) ∈ A"
  using prems inj_converse_fun apply_funtype by blast;*)
  


text{*For injections the image of intersection is 
  the intersection of images.*}

lemma inj_image_of_Inter: assumes A1: "f ∈ inj(A,B)" and
  A2: "I≠0" and A3: "∀i∈I. P(i) ⊆ A"
  shows "f``(\<Inter>i∈I. P(i)) = ( \<Inter>i∈I. f``(P(i)) )"
proof;
  from A1 A2 A3 show "f``(\<Inter>i∈I. P(i)) ⊆ ( \<Inter>i∈I. f``(P(i)) )"
    using inj_is_fun image_of_Inter by auto;
  from A1 A2 A3 have "f:A->B"  and "( \<Inter>i∈I. P(i) ) ⊆ A"
    using inj_is_fun ZF1_1_L7 by auto;
  then have I: "f``(\<Inter>i∈I. P(i)) = { f`(x). x ∈ ( \<Inter>i∈I. P(i) ) }"
    using func_imagedef by simp;
  { fix y assume A4: "y ∈ ( \<Inter>i∈I. f``(P(i)) )"
    let ?x = "converse(f)`(y)"
    from A2 obtain i0 where "i0 ∈ I" by auto;
    with A1 A4 have II: "y ∈ range(f)" using inj_is_fun func1_1_L6
      by auto;
    with A1 have III: "f`(?x) = y" using right_inverse by simp;
    from A1 II have IV: "?x ∈ A" using inj_converse_fun apply_funtype 
      by blast;
    { fix i assume "i∈I"
      with A3 A4 III have "P(i) ⊆ A" and "f`(?x) ∈  f``(P(i))" 
        by auto;
      with A1 IV have "?x ∈ P(i)" using inj_point_of_image
        by blast;
    } then have "∀i∈I. ?x ∈ P(i)" by simp;
    with A2 I have "f`(?x) ∈ f``( \<Inter>i∈I. P(i) )"
      by auto;
    with III have "y ∈  f``( \<Inter>i∈I. P(i) )" by simp;
  } then show "( \<Inter>i∈I. f``(P(i)) ) ⊆  f``( \<Inter>i∈I. P(i) )"
    by auto;
qed;

text{*This concludes func1.thy.*}

end