Theory func_ZF

(* 
    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{func\_ZF.thy}*}

theory func_ZF imports Order func1 Order_ZF 

begin

text{*In this theory we consider properties of functions that are binary 
  operations, that is they map $X\times X$ into $X$. We also consider 
  some properties of functions related to order.*}

section{*Lifting operations to a function space*}

text{*It happens quite often that we have a binary operation on some set and
  we need a similar operation that is defined for functions on that set. 
  For example once we know how to add real numbers we also know how to add
  real-valued functions: for $f,g:X \rightarrow \mathbf{R}$ we define
  $(f+g)(x) = f(x) + g(x)$. Note that formally the $+$ means something 
  different on the left hand side of this equality than on the 
  right hand side.
  This section aims at formalizing this process.
  We will call it "lifting to a function space", if you have a 
  suggestion for a better name, please let me know. *} 

constdefs 
  Lift2FcnSpce (infix "{lifted to function space over}" 65) 
  "f {lifted to function space over} X ≡ 
  {<p,g> ∈ ((X->range(f))×(X->range(f)))×(X->range(f)).
  {<x,y> ∈ X×range(f). f`<fst(p)`(x),snd(p)`(x)> = y} = g}";

text{*The result of the lift belongs to the function space.*}

lemma func_ZF_1_L1: 
  assumes A1: "f : Y×Y->Y" 
  and A2: "p ∈(X->range(f))×(X->range(f))"
  shows 
  "{<x,y> ∈ X×range(f). f`<fst(p)`(x),snd(p)`(x)> = y} : X->range(f)"
  proof -;
    have "∀x∈X. f`<fst(p)`(x),snd(p)`(x)> ∈ range(f)"
    proof;
      fix x assume A3:"x∈X"
      let ?p = "<fst(p)`(x),snd(p)`(x)>"
      from A2 A3 have 
        "fst(p)`(x) ∈ range(f)"  "snd(p)`(x) ∈ range(f)"
        using apply_type by auto;
      with A1 have "?p ∈ Y×Y"
        using func1_1_L5B by blast;
      with A1 have "<?p, f`(?p)> ∈ f"
        using apply_Pair by simp;
      with A1 show 
        "f`(?p) ∈ range(f)"
        using rangeI by simp;
    qed
    then show ?thesis using func1_1_L11A by simp;
qed;

text{*The values of the lift are defined by the value of the liftee in a 
  natural way.*}

lemma func_ZF_1_L2: 
  assumes "f : Y×Y->Y" 
  and "p∈(X->range(f))×(X->range(f))" and "x∈X"
  and "P = {<x,y> ∈ X×range(f). f`<fst(p)`(x),snd(p)`(x)> = y}"
  shows "P`(x) = f`⟨fst(p)`(x),snd(p)`(x)⟩" 
  using prems func_ZF_1_L1 func1_1_L11B by simp;

text{*Function lifted to a function space results in a function space 
  operator.*}

lemma func_ZF_1_L3: 
  assumes "f ∈ Y×Y->Y"
  and "F = f {lifted to function space over} X"
  shows "F : (X->range(f))×(X->range(f))->(X->range(f))"
  using prems Lift2FcnSpce_def func_ZF_1_L1 func1_1_L11A by simp;

text{*The values of the lift are defined by the values of the liftee in
  the natural way. For some reason we need to be extremely detailed and 
  explicit to be able to apply @{text "func1_3_L2"}. simp and auto 
  fail miserably here.*}

lemma func_ZF_1_L4: 
  assumes A1: "f : Y×Y->Y"
  and A2: "F = f {lifted to function space over} X"
  and A3: "s:X->range(f)" "r:X->range(f)"  
  and A4: "x∈X"
  shows "(F`<s,r>)`(x) = f`<s`(x),r`(x)>"
proof -;
  let ?P = "{<x,y> ∈ X×range(f). f`<s`(x),r`(x)> = y}";
  let ?p = "<s,r>"
  from A1 have "f ∈ Y×Y->Y" .;
  moreover from A3 have 
    "?p ∈ (X->range(f))×(X->range(f))"
    by simp;
  moreover from A4 have "x∈X" .;
  moreover have 
    "?P = {<x,y> ∈ X×range(f). f`<fst(?p)`(x),snd(?p)`(x)> = y}"
    by simp;
  ultimately have "?P`(x) = f`⟨fst(?p)`(x),snd(?p)`(x)⟩"
    by (rule func_ZF_1_L2);
  with A1 A2 A3 show ?thesis using func_ZF_1_L3 Lift2FcnSpce_def func1_1_L11B
    by simp;
qed

section{*Associative and commutative operations*}

text{*In this section we define associative and commutative oparations 
  and prove that they remain such when we lift them
  to a function space.*}

constdefs 

  IsAssociative (infix "{is associative on}" 65)
  "f {is associative on} G ≡ f ∈ G×G->G ∧ 
  (∀ x ∈ G. ∀ y ∈ G. ∀ z ∈ G. 
  ( f`(<f`(<x,y>),z>) = f`( < x,f`(<y,z>)> )))"

  IsCommutative (infix "{is commutative on}" 65)
  "f {is commutative on} G ≡ ∀x∈G. ∀y∈G. f`<x,y> = f`<y,x>"

text{*The lift of a commutative function is commutative.*}

lemma func_ZF_2_L1:
  assumes A1: "f : G×G->G"
  and A2: "F = f {lifted to function space over} X"
  and A3: "s : X->range(f)" "r : X->range(f)" 
  and A4: "f {is commutative on} G"
  shows "F`<s,r> = F`<r,s>" 
proof -;
  from A1 A2 have 
    "F : (X->range(f))×(X->range(f))->(X->range(f))"
    using func_ZF_1_L3 by simp; 
  with A3 have 
    "F`<s,r> : X->range(f)" "F`<r,s> : X->range(f)"
    using apply_type by auto;
  moreover have 
    "∀x∈X. (F`<s,r>)`(x) = (F`<r,s>)`(x)"
  proof;
    fix x assume A5:"x∈X"
    from A1 have "range(f)⊆G"
      using func1_1_L5B by simp;
    with A3 A5 have T1:"s`(x) ∈ G" "r`(x) ∈ G"
      using apply_type by auto;
    with A1 A2 A3 A4 A5 show 
      "(F`<s,r>)`(x) = (F`<r,s>)`(x)"
      using func_ZF_1_L4 IsCommutative_def by simp;
  qed;
  ultimately show ?thesis using fun_extension_iff
    by simp;
qed;

text{*The lift of a commutative function is commutative 
  on the function space.*}

lemma func_ZF_2_L2:
  assumes "f : G×G->G"
  and "f {is commutative on} G"
  and "F = f {lifted to function space over} X"
  shows "F {is commutative on} (X->range(f))"
  using prems IsCommutative_def func_ZF_2_L1 by simp;
  
text{*The lift of an associative function is associative.*}

lemma func_ZF_2_L3:
  assumes A2: "F = f {lifted to function space over} X"
  and A3: "s : X->range(f)" "r : X->range(f)" "q : X->range(f)"
  and A4: "f {is associative on} G"
  shows "F`⟨F`<s,r>,q⟩ = F`⟨s,F`<r,q>⟩"
proof -;
  from A4 A2 have 
    "F : (X->range(f))×(X->range(f))->(X->range(f))"
    using IsAssociative_def func_ZF_1_L3 by auto;
  with A3 have T1:
    "F`<s,r> : X->range(f)"
    "F`<r,q> : X->range(f)"
    "F`<F`<s,r>,q> : X->range(f)"
    "F`<s,F`<r,q> >: X->range(f)"
    using apply_type by auto;
  moreover have
    "∀x∈X. (F`⟨F`<s,r>,q⟩)`(x) = (F`⟨s,F`<r,q>⟩)`(x)"
  proof;
    fix x assume A5:"x∈X"
    from A4 have T2:"f:G×G->G"
      using IsAssociative_def by simp;
    then have "range(f)⊆G"
      using func1_1_L5B by simp;
    with A3 A5 have 
      "s`(x) ∈ G" "r`(x) ∈ G" "q`(x) ∈ G"
      using apply_type by auto;
    with T2 A2 T1 A3 A5 A4 show 
      "(F`⟨F`<s,r>,q⟩)`(x) = (F`⟨s,F`<r,q>⟩)`(x)"
      using func_ZF_1_L4 IsAssociative_def by simp;
  qed;
  ultimately show ?thesis using fun_extension_iff
    by simp;
qed;

text{*The lift of an associative function is associative 
  on the function space.*}

lemma func_ZF_2_L4:
  assumes A1: "f {is associative on} G"
  and A2: "F = f {lifted to function space over} X"
  shows "F {is associative on} (X->range(f))"
proof -;
  from A1 A2 have
    "F : (X->range(f))×(X->range(f))->(X->range(f))"
    using IsAssociative_def func_ZF_1_L3 by auto;
  moreover from A1 A2 have
    "∀s ∈ X->range(f). ∀ r ∈ X->range(f). ∀q ∈ X->range(f).
    F`<F`<s,r>,q> = F`<s,F`<r,q> >"
    using func_ZF_2_L3 by simp;
  ultimately show ?thesis using IsAssociative_def 
    by simp;
qed;

section{*Restricting operations*}

text{*In this section we consider when restriction of the operation to a set
  inherits properties like commutativity and associativity.*}

text{*The commutativity is inherited when restricting a function to a set.*}

lemma func_ZF_4_L1: 
  assumes A1: "f:X×X->Y" and A2: "A⊆X"
  and A3: "f {is commutative on} X"
  shows "restrict(f,A×A) {is commutative on} A"
proof -;
  { fix x y assume A4: "x∈A ∧ y∈A"
    with A2 A3 have
      "f`<x,y> = f`<y,x>"
      using IsCommutative_def by auto;
    moreover from A4 have 
      "restrict(f,A×A)`<x,y> = f`<x,y>"
      "restrict(f,A×A)`<y,x> = f`<y,x>"
      using restrict_if by auto;
    ultimately have
      "restrict(f,A×A)`<x,y> = restrict(f,A×A)`<y,x>"
      by simp }
  then show ?thesis using IsCommutative_def by simp;
qed;
  
text{*Next we define sets closed with respect to an operation.*}

constdefs 
  IsOpClosed (infix "{is closed under}" 65) 
  "A {is closed under} f ≡ ∀x∈A. ∀y∈A. f`<x,y> ∈ A";

text{*Associative operation restricted to a set that is closed with
  resp. to this operation is associative.*}

lemma func_ZF_4_L2:assumes A1: "f {is associative on} X"
  and A2: "A⊆X" and A3: "A {is closed under} f"
  and A4: "x∈A" "y∈A" "z∈A"
  and A5: "g = restrict(f,A×A)"
  shows "g`⟨g`<x,y>,z⟩ = g`⟨x,g`<y,z>⟩"
proof -; 
  from A4 A2 have T1:
    "x∈X" "y∈X" "z∈X"
    by auto;
  from A3 A4 A5 have
    "g`<g`<x,y>,z> = f`<f`<x,y>,z>"
    "g`<x,g`<y,z> > = f`<x,f`<y,z> >"
    using IsOpClosed_def restrict_if by auto;
  moreover from A1 T1 have
     "f`<f`<x,y>,z> = f`<x,f`<y,z> >"
    using IsAssociative_def by simp;
  ultimately show ?thesis by simp;
qed;

text{*Associative operation restricted to a set that is closed with
  resp. to this operation is associative on the set.*}

lemma func_ZF_4_L3: assumes A1: "f {is associative on} X"
  and A2: "A⊆X" and A3: "A {is closed under} f"
  shows "restrict(f,A×A) {is associative on} A"
proof -;
  let ?g = "restrict(f,A×A)"
  from A1 have "f:X×X->X"
    using IsAssociative_def by simp;
  moreover from A2 have "A×A ⊆ X×X" by auto;
  moreover from A3 have "∀p ∈ A×A. ?g`(p) ∈ A"
    using IsOpClosed_def restrict_if by auto;
  ultimately have "?g : A×A->A"
    using func1_2_L4 by simp;
  moreover from  A1 A2 A3 have
    "∀ x ∈ A. ∀ y ∈ A. ∀ z ∈ A.
    ?g`<?g`<x,y>,z> = ?g`< x,?g`<y,z> >"
    using func_ZF_4_L2 by simp;
  ultimately show ?thesis 
    using IsAssociative_def by simp;
qed;

text{*The essential condition to show that if a set $A$ is closed 
  with respect to an operation, 
  then it is closed under this operation restricted 
  to any superset of $A$.*}

lemma func_ZF_4_L4: assumes "A {is closed under} f"
  and "A⊆B" and "x∈A"  "y∈A" and "g = restrict(f,B×B)"
  shows "g`<x,y> ∈ A"
  using prems IsOpClosed_def restrict by auto;

text{*If a set $A$ is closed under an operation, 
  then it is closed under this operation restricted 
  to any superset of $A$. *}

lemma func_ZF_4_L5: 
  assumes A1: "A {is closed under} f"
  and A2: "A⊆B"
  shows "A {is closed under} restrict(f,B×B)"
proof -
  let ?g = "restrict(f,B×B)"
  from A1 A2 have "∀x∈A. ∀y∈A. ?g`<x,y> ∈ A"
    using func_ZF_4_L4 by simp
  then show ?thesis using IsOpClosed_def by simp;
qed;

text{*The essential condition to show that intersection of sets that are
  closed with respect to an operation is closed with respect 
  to the operation.*}

lemma func_ZF_4_L6:
  assumes "A {is closed under} f" 
  and "B {is closed under} f"
  and "x ∈ A∩B" "y∈ A∩B"
  shows "f`<x,y> ∈ A∩B" using prems IsOpClosed_def by auto;

text{*Intersection of sets that are
  closed with respect to an operation is closed under 
  the operation.*}

lemma func_ZF_4_L7:
  assumes "A {is closed under} f"
  "B {is closed under} f"
  shows "A∩B {is closed under} f"
  using prems IsOpClosed_def by simp;

section{*Composition*}

text{*For any set $X$ we can consider a binary operation 
  on the set of functions 
  $f:X\rightarrow X$ defined by $C(f,g) = f\circ g$. Composition of functions 
  (or relations) is defined in the standard Isabelle distribution as a higher
  order function. In this section we consider the corresponding two-argument 
  ZF-function (binary operation), that is a subset of 
  $((X\rightarrow X)\times (X\rightarrow X))\times (X\rightarrow X)$.*}

constdefs
  "Composition(X) ≡ 
  {<p,f> ∈ ((X->X)×(X->X))×(X->X). fst(p) O snd(p) = f}"

text{*Composition operation is a function that maps 
  $(X\rightarrow X)\times (X\rightarrow X)$ into $X\rightarrow X$.*}

lemma func_ZF_5_L1: shows "Composition(X) : (X->X)×(X->X)->(X->X)"
  using comp_fun Composition_def func1_1_L11A by simp;

text{*The value of the composition operation is the composition of arguments.*}

lemma func_ZF_5_L2: assumes "f:X->X" "g:X->X"
  shows "Composition(X)`<f,g> = f O g" 
  using prems func_ZF_5_L1 Composition_def func1_1_L11B by simp;

text{*What is the falue of a composition on an argument?*}

lemma func_ZF_5_L3: assumes "f:X->X" and "g:X->X" and "x∈X"
  shows "(Composition(X)`<f,g>)`(x) = f`(g`(x))"
  using prems func_ZF_5_L2 comp_fun_apply by simp;
  
text{*The essential condition to show that composition is associative.*}

lemma func_ZF_5_L4: assumes A1: "f:X->X" "g:X->X" "h:X->X"
  and A2: "C = Composition(X)"
  shows "C`⟨C`<f,g>,h⟩ = C`⟨ f,C`<g,h>⟩"
proof -; 
  from A2 have "C : ((X->X)×(X->X))->(X->X)"
    using func_ZF_5_L1 by simp;
  with A1 have T1:
    "C`<f,g> : X->X"
    "C`<g,h> : X->X"
    "C`<C`<f,g>,h> : X->X"
    "C`< f,C`<g,h> > : X->X"
    using apply_funtype by auto;
  moreover have 
    "∀ x ∈ X. C`⟨C`<f,g>,h⟩`(x) = C`⟨f,C`<g,h>⟩`(x)"
  proof;
    fix x assume A3:"x∈X"
    with A1 A2 T1 have 
      "C`<C`<f,g>,h> ` (x) = f`(g`(h`(x)))"
      "C`< f,C`<g,h> >`(x) = f`(g`(h`(x)))"
      using func_ZF_5_L3 apply_funtype by auto;
    then show "C`⟨C`<f,g>,h⟩`(x) = C`⟨ f,C`<g,h>⟩`(x)"
      by simp;
    qed;
  ultimately show ?thesis using fun_extension_iff by simp;
qed;
  
text{*Composition is an associative operation on $X\rightarrow X$ (the space
  of functions that map $X$ into itself).*}

lemma func_ZF_5_L5: shows "Composition(X) {is associative on} (X->X)"
proof -;
  let ?C = "Composition(X)"
  have "∀f∈X->X. ∀g∈X->X. ∀h∈X->X.
    ?C`<?C`<f,g>,h> = ?C`< f,?C`<g,h> >"
    using func_ZF_5_L4 by simp;
  then show ?thesis using func_ZF_5_L1 IsAssociative_def
    by simp;
qed;

section{*Identity function *}

text{*In this section we show some additional facts about the identity 
  function defined in the standard Isabelle's Perm.thy file.*}

text{*Composing a function with identity does not change the function.*}

lemma func_ZF_6_L1A: assumes A1: "f : X->X"
  shows "Composition(X)`<f,id(X)> = f"
  "Composition(X)`<id(X),f> = f"
proof -;
  have "Composition(X) : (X->X)×(X->X)->(X->X)"
    using func_ZF_5_L1 by simp;
  with A1 have "Composition(X)`<id(X),f> : X->X"
    "Composition(X)`<f,id(X)> : X->X"
    using id_type apply_funtype by auto;
  moreover from A1 have "f : X->X" .
  moreover from A1 have 
    "∀x∈X. (Composition(X)`<id(X),f>)`(x) = f`(x)"
    "∀x∈X. (Composition(X)`<f,id(X)>)`(x) = f`(x)"
    using id_type func_ZF_5_L3 apply_funtype id_conv
    by auto;
  ultimately show "Composition(X)`<id(X),f> = f"
    "Composition(X)`<f,id(X)> = f"
    using fun_extension_iff by auto;
qed;

section{*Distributive operations*}

text{*In this section we deal with pairs of operations such that one is
  distributive with respect to the other, that is 
  $a\cdot (b+c) = a\cdot b + a\cdot c$ and
  $(b+c)\cdot a = b\cdot a + c\cdot a$. We show that this property is 
  preserved under restriction to a set closed with respect to both 
  operations. In EquivClass1.thy we show that this property is 
  preserved by projections to the quotient space if both operations are 
  congruent with respect to the equivalence relation.*}

text{*We define distributivity as a statement about three sets. The first 
  set is the set on which the operations act. The second set is the 
  additive operation (a ZF function) and the third is the multiplicative
  operation.*}

constdefs
  "IsDistributive(X,A,M) ≡ (∀a∈X.∀b∈X.∀c∈X.
  M`⟨a,A`<b,c>⟩ = A`⟨M`<a,b>,M`<a,c>⟩ ∧ 
  M`⟨A`<b,c>,a⟩ = A`⟨M`<b,a>,M`<c,a> ⟩)"

text{*The essential condition to show that distributivity is preserved by 
  restrictions to sets that are closed with
  respect to both operations.*}

lemma func_ZF_7_L1: 
  assumes A1: "IsDistributive(X,A,M)"
  and A2: "Y⊆X"
  and A3: "Y {is closed under} A"  "Y {is closed under} M"
  and A4: "Ar = restrict(A,Y×Y)" "Mr = restrict(M,Y×Y)"
  and A5: "a∈Y"  "b∈Y"  "c∈Y"
  shows "Mr`⟨ a,Ar`<b,c> ⟩  = Ar`⟨ Mr`<a,b>,Mr`<a,c> ⟩  ∧ 
  Mr`⟨ Ar`<b,c>,a ⟩ = Ar`⟨ Mr`<b,a>,Mr`<c,a> ⟩"
proof
  from A3 A5 have "A`<b,c> ∈ Y"  "M`<a,b> ∈ Y"  "M`<a,c> ∈ Y"
    "M`<b,a> ∈ Y"  "M`<c,a> ∈ Y" using IsOpClosed_def by auto;
  with A5 A4 have T1:"Ar`<b,c> ∈ Y" "Mr`<a,b> ∈ Y" "Mr`<a,c> ∈ Y"
    "Mr`<b,a> ∈ Y" "Mr`<c,a> ∈ Y"
    using restrict by auto;
  with A1 A2 A4 A5 show "Mr`⟨ a,Ar`<b,c> ⟩  = Ar`⟨ Mr`<a,b>,Mr`<a,c> ⟩"
    "Mr`⟨ Ar`<b,c>,a ⟩ = Ar`⟨ Mr`<b,a>,Mr`<c,a> ⟩"
    using restrict IsDistributive_def by auto;
qed;
  
text{*Distributivity is preserved by restrictions to sets that are closed with
  respect to both operations.*}

lemma func_ZF_7_L2: 
  assumes "IsDistributive(X,A,M)"
  and "Y⊆X"
  and "Y {is closed under} A" 
  "Y {is closed under} M"
  and "Ar = restrict(A,Y×Y)" "Mr = restrict(M,Y×Y)"
  shows "IsDistributive(Y,Ar,Mr)"
proof -
  from prems have "∀a∈Y.∀b∈Y.∀c∈Y. 
    Mr`⟨ a,Ar`<b,c> ⟩ = Ar`⟨ Mr`<a,b>,Mr`<a,c> ⟩ ∧ 
    Mr`⟨ Ar`<b,c>,a ⟩ = Ar`⟨ Mr`<b,a>,Mr`<c,a> ⟩"
    using func_ZF_7_L1 by simp;
  then show ?thesis using IsDistributive_def by simp;
qed;

section{*Functions and order*}

text{*This section deals with functions between ordered sets.*}

text{*If every value of a function on a set is bounded below by
  a constant, then the image of the set is bounded below.*}

lemma func_ZF_8_L1: 
  assumes "f:X->Y" and "A⊆X" and "∀x∈A. ⟨L,f`(x)⟩ ∈ r"
  shows "IsBoundedBelow(f``(A),r)"
proof -
  from prems have "∀y ∈ f``(A). ⟨L,y⟩ ∈ r"
    using func_imagedef by simp;
  then show "IsBoundedBelow(f``(A),r)" 
    by (rule Order_ZF_3_L9);
qed;

text{*If every value of a function on a set is bounded above by
  a constant, then the image of the set is bounded above.*}


lemma func_ZF_8_L2:  
  assumes "f:X->Y" and "A⊆X" and "∀x∈A. ⟨f`(x),U⟩ ∈ r"
  shows "IsBoundedAbove(f``(A),r)"
proof -
  from prems have "∀y ∈ f``(A). ⟨y,U⟩ ∈ r"
    using func_imagedef by simp;
  then show "IsBoundedAbove(f``(A),r)" 
    by (rule Order_ZF_3_L10);
qed;

(*section{*Fixing variables in functions*}

text{*For every function of two variables we can define families of 
  functions of one variable by fixing the other variable. This section 
  establishes basic definitions and results for this concept.*}

constdefs

  Fix1stVar :: "[i,i]=>i"
  "Fix1stVar(f,x) ≡ 
  {<y,z> ∈ range(domain(f))×range(f). f`<x,y> = z}"

  
  Fix2ndVar :: "[i,i]=>i"
  "Fix2ndVar(f,y) ≡ 
  {<x,z> ∈ domain(domain(f))×range(f). f`<x,y> = z}"*)

section{*Projections in cartesian products*}

text{*In this section we consider maps arising naturally
  in cartesian products. *}

text{*There is a natural bijection etween $X=Y\times \{ y\}$ (a "slice")
  and $Y$. We will call this the @{text "SliceProjection(Y×{y})"}. 
  This is really the ZF equivalent of the meta-function @{text "fst(x)"}.
  *}

constdefs
  "SliceProjection(X) ≡ {⟨p,fst(p)⟩. p ∈ X }"

text{*A slice projection is a bijection between $X\times\{ y\}$ and $X$.*}

lemma slice_proj_bij: shows 
  "SliceProjection(X×{y}): X×{y} -> X"
  "domain(SliceProjection(X×{y})) = X×{y}"
  "∀p∈X×{y}. SliceProjection(X×{y})`(p) = fst(p)"
  "SliceProjection(X×{y}) ∈ bij(X×{y},X)"
proof -
  let ?P = "SliceProjection(X×{y})"
  have  "∀p ∈ X×{y}. fst(p) ∈ X" by simp;
  moreover from this have 
    "{⟨p,fst(p)⟩. p ∈ X×{y} } : X×{y} -> X"
    by (rule ZF_fun_from_total);
  ultimately show 
    I: "?P: X×{y} -> X" and II: "∀p∈X×{y}. ?P`(p) = fst(p)"
    using ZF_fun_from_tot_val SliceProjection_def by auto;
  hence
    "∀a ∈ X×{y}. ∀ b ∈ X×{y}. ?P`(a) = ?P`(b) --> a=b"
    by auto;
  with I have "?P ∈ inj(X×{y},X)" using inj_def 
    by simp;
  moreover from II have "∀x∈X. ∃p∈X×{y}. ?P`(p) = x" 
    by simp;
  with I have "?P ∈ surj(X×{y},X)" using surj_def
    by simp;
  ultimately show "?P ∈ bij(X×{y},X)"
    using bij_def by simp;
  from I show "domain(SliceProjection(X×{y})) = X×{y}"
    using func1_1_L1 by simp
qed;
  
section{*Induced relations and order isomorphisms *}

text{*When we have two sets $X,Y$, function $f:X\rightarrow Y$ and
  a relation $R$ on $Y$ we can define a relation $r$ on $X$
  by saying that $x\ r\ y$ if and only if $f(x) \ R \ f(y)$. 
  This is especially interesting when $f$ is a bijection as all reasonable
  properties of $R$ are inherited by $r$. This section treats mostly the case
  when $R$ is an order relation and $f$ is a bijection.
  The standard Isabelle's @{text "Order.thy"} theory 
  defines the notion of a space of order isomorphisms
  between two sets relative to a relation. We expand that material
  proving that order isomrphisms preserve interesting properties
  of the relation.*}

text{*We call the relation created by a relation on $Y$ and a mapping
  $f:X\rightarrow Y$ the @{text "InducedRelation(f,R)"}.*}

constdefs
  "InducedRelation(f,R) ≡ 
  {p ∈ domain(f)×domain(f). ⟨f`(fst(p)),f`(snd(p))⟩ ∈ R}"

text{*A reformulation of the definition of the relation induced by
  a function.*}

lemma def_of_ind_relA: 
  assumes "⟨x,y⟩ ∈ InducedRelation(f,R)"
  shows "⟨f`(x),f`(y)⟩ ∈ R"
  using prems InducedRelation_def by simp;

text{*A reformulation of the definition of the relation induced by
  a function, kind of converse of @{text "def_of_ind_relA"}.*}

lemma def_of_ind_relB: assumes "f:A->B" and 
  "x∈A"  "y∈A" and "⟨f`(x),f`(y)⟩ ∈ R"
  shows "⟨x,y⟩ ∈ InducedRelation(f,R)"
  using prems func1_1_L1 InducedRelation_def by simp;

text{*A property of order isomorphisms that is missing from
  standard Isabelle's @{text "Order.thy"}.*}

lemma ord_iso_apply_conv: 
  assumes "f ∈ ord_iso(A,r,B,R)" and
  "⟨f`(x),f`(y)⟩ ∈ R" and "x∈A"  "y∈A"
  shows "⟨x,y⟩ ∈ r"
  using prems ord_iso_def by simp;

text{*The next lemma tells us where the induced relation is defined*}

lemma ind_rel_domain: 
  assumes  "R ⊆ B×B" and "f:A->B"
  shows "InducedRelation(f,R) ⊆ A×A"
  using prems func1_1_L1 InducedRelation_def
  by auto;

text{*A bijection is an order homomorphisms between a relation
  and the induced one.*}

lemma bij_is_ord_iso: assumes A1: "f ∈ bij(A,B)"
  shows "f ∈ ord_iso(A,InducedRelation(f,R),B,R)"
proof -
  let ?r = "InducedRelation(f,R)"
  { fix x y assume A2: "x∈A"  "y∈A"
    have "⟨x,y⟩ ∈ ?r <-> ⟨f`(x),f`(y)⟩ ∈ R" 
    proof;
      assume "⟨x,y⟩ ∈ ?r" then show "⟨f`(x),f`(y)⟩ ∈ R" 
        using def_of_ind_relA by simp;
    next assume "⟨f`(x),f`(y)⟩ ∈ R"
      with A1 A2 show "⟨x,y⟩ ∈ ?r"
        using bij_is_fun def_of_ind_relB by blast 
    qed }
  with A1 show "f ∈ ord_iso(A,InducedRelation(f,R),B,R)"
    using ord_isoI by simp
qed;

text{*An order isomoprhism preserves antisymmetry.*}

lemma ord_iso_pres_antsym: assumes A1: "f ∈ ord_iso(A,r,B,R)" and 
  A2: "r ⊆ A×A" and A3: "antisym(R)"
  shows "antisym(r)"
proof -
  { fix x y
    assume A4: "⟨x,y⟩ ∈ r"   "⟨y,x⟩ ∈ r"
    from A1 have "f ∈ inj(A,B)"
      using ord_iso_is_bij bij_is_inj by simp
    moreover
    from A1 A2 A4 have 
      "⟨f`(x), f`(y)⟩ ∈ R" and "⟨f`(y), f`(x)⟩ ∈ R"
      using ord_iso_apply by auto;
    with A3 have "f`(x) = f`(y)" by (rule Fol1_L4);
    moreover from A2 A4 have "x∈A"  "y∈A" by auto;
    ultimately have "x=y" by (rule inj_apply_equality);
  } then have "∀x y. ⟨x,y⟩ ∈ r ∧ ⟨y,x⟩ ∈ r --> x=y" by auto;
  then show "antisym(r)" using imp_conj antisym_def
    by simp;
qed;

text{*Order isomoprhisms preserve transitivity.*}

lemma ord_iso_pres_trans: assumes A1: "f ∈ ord_iso(A,r,B,R)" and 
  A2: "r ⊆ A×A" and A3: "trans(R)"
  shows "trans(r)"
proof -
  { fix x y z
    assume A4: "⟨x, y⟩ ∈ r"   "⟨y, z⟩ ∈ r"
    note A1
    moreover
    from A1 A2 A4 have 
      "⟨f`(x), f`(y)⟩ ∈ R ∧ ⟨f`(y), f`(z)⟩ ∈ R"
      using ord_iso_apply by auto;
    with A3 have "⟨f`(x),f`(z)⟩ ∈ R" by (rule Fol1_L3);
    moreover from A2 A4 have "x∈A"  "z∈A" by auto;
    ultimately have "⟨x, z⟩ ∈ r" using ord_iso_apply_conv
      by simp;
  } then have  "∀ x y z. ⟨x, y⟩ ∈ r ∧ ⟨y, z⟩ ∈ r --> ⟨x, z⟩ ∈ r"
    by blast;
  then show "trans(r)" by (rule Fol1_L2);
qed;
     
text{*Order isomorphisms preserve totality.*}

lemma ord_iso_pres_tot: assumes A1: "f ∈ ord_iso(A,r,B,R)" and 
  A2: "r ⊆ A×A" and A3: "R  {is total on} B"
  shows "r  {is total on} A"
proof -
  { fix x y
    assume A4: "x∈A"  "y∈A"  "⟨x,y⟩ ∉ r"  
    with A1 have "⟨f`(x),f`(y)⟩ ∉ R" using ord_iso_apply_conv
      by auto;
    moreover 
    from A1 have "f:A->B" using ord_iso_is_bij bij_is_fun 
      by simp;
    with A3 A4 have "⟨f`(x),f`(y)⟩ ∈  R ∨ ⟨f`(y),f`(x)⟩ ∈  R"
      using apply_funtype IsTotal_def by simp;
    ultimately have "⟨f`(y),f`(x)⟩ ∈  R" by simp;
    with A1 A4 have "⟨y,x⟩ ∈ r" using ord_iso_apply_conv
      by simp;
  } then have "∀x∈A. ∀y∈A. ⟨x,y⟩ ∈ r ∨  ⟨y,x⟩ ∈ r"
    by blast;
  then show "r  {is total on} A" using IsTotal_def
    by simp;
qed;

text{*Order isomorphisms preserve linearity.*}

lemma ord_iso_pres_lin: assumes "f ∈ ord_iso(A,r,B,R)" and 
  "r ⊆ A×A" and "IsLinOrder(B,R)"
  shows "IsLinOrder(A,r)"
  using prems ord_iso_pres_antsym ord_iso_pres_trans ord_iso_pres_tot
    IsLinOrder_def by simp;

text{*If a relation is a linear order, then the relation induced
  on another set is by a bijection is also a linear order.*}

lemma ind_rel_pres_lin: 
  assumes A1: "f ∈ bij(A,B)" and A2: "IsLinOrder(B,R)"
  shows "IsLinOrder(A,InducedRelation(f,R))"
proof -
  let ?r = "InducedRelation(f,R)"
  from A1 have "f ∈ ord_iso(A,?r,B,R)" and "?r ⊆ A×A"
    using bij_is_ord_iso domain_of_bij InducedRelation_def 
    by auto;
  with A2 show "IsLinOrder(A,?r)" using ord_iso_pres_lin 
    by simp;
qed;

text{*The image by an order isomorphism 
  of a  bounded above and nonempty set is bounded above.*}

lemma ord_iso_pres_bound_above: 
  assumes A1: "f ∈ ord_iso(A,r,B,R)" and A2: "r ⊆ A×A" and
  A3: "IsBoundedAbove(C,r)"   "C≠0"
  shows "IsBoundedAbove(f``(C),R)"   "f``(C) ≠ 0"
proof -
  from A3 obtain u where I: "∀x∈C. ⟨x,u⟩ ∈ r"
    using IsBoundedAbove_def by auto;
  from A1 have II: "f:A->B" using ord_iso_is_bij bij_is_fun
    by simp;
  from A2 A3 have III: "C⊆A" using Order_ZF_3_L1A by blast;
  from A3 obtain x where "x∈C" by auto;
  with A2 I have IV: "u∈A" by auto;
  { fix y assume "y ∈ f``(C)"
    with II III obtain x where "x∈C" and "y = f`(x)"
      using func_imagedef by auto;
    with A1 I III IV have "⟨y,f`(u)⟩ ∈ R"
      using ord_iso_apply by auto;
  } then have "∀y ∈ f``(C).  ⟨y,f`(u)⟩ ∈ R" by simp;
  then show "IsBoundedAbove(f``(C),R)" by (rule Order_ZF_3_L10);
  from A3 II III show "f``(C) ≠ 0" using func1_1_L15A
    by simp;
qed;

text{*Order isomorphisms preserve the property of having a minimum.*}

lemma ord_iso_pres_has_min: 
  assumes A1: "f ∈ ord_iso(A,r,B,R)" and  A2: "r ⊆ A×A" and 
  A3: "C⊆A" and A4: "HasAminimum(R,f``(C))"
  shows "HasAminimum(r,C)"
proof -
  from A4 obtain m where 
    I: "m ∈ f``(C)" and II: "∀y ∈ f``(C). ⟨m,y⟩ ∈ R"
    using HasAminimum_def by auto;
  let ?k = "converse(f)`(m)"
  from A1 have III: "f:A->B" using ord_iso_is_bij bij_is_fun
    by simp
  from A1 have "f ∈ inj(A,B)" using ord_iso_is_bij bij_is_inj
    by simp;
  with A3 I have IV: "?k ∈ C" and V: "f`(?k) = m" 
    using inj_inv_back_in_set by auto;
  moreover
  { fix x assume A5: "x∈C"
    with A3 II III IV V have
      "?k ∈ A"   "x∈A"  "⟨f`(?k),f`(x)⟩ ∈ R"
      using func_imagedef by auto;
    with A1 have "⟨?k,x⟩ ∈ r" using ord_iso_apply_conv
      by simp;
  } then have "∀x∈C.  ⟨?k,x⟩ ∈ r" by simp;
  ultimately show "HasAminimum(r,C)" using HasAminimum_def by auto;
qed;

text{*Order isomorhisms preserve the images of relations.
  In other words taking the image of a point by a relation
  commutes with the function.*}

lemma ord_iso_pres_rel_image: 
  assumes A1: "f ∈ ord_iso(A,r,B,R)" and  
  A2: "r ⊆ A×A"  "R ⊆ B×B" and 
  A3: "a∈A"
  shows "f``(r``{a}) = R``{f`(a)}"
proof;
  from A1 have "f:A->B" using ord_iso_is_bij bij_is_fun
    by simp;
  moreover from A2 A3 have I: "r``{a} ⊆ A" by auto;
  ultimately have I: "f``(r``{a}) = {f`(x). x ∈ r``{a} }"
    using func_imagedef by simp;
  { fix y assume A4: "y ∈ f``(r``{a})" 
    with I obtain x where 
      "x ∈ r``{a}" and II: "y = f`(x)"
      by auto;
    with A1 A2 have "⟨f`(a),f`(x)⟩ ∈ R" using ord_iso_apply
      by auto;
    with II have "y ∈  R``{f`(a)}" by auto;
  } then show  "f``(r``{a}) ⊆ R``{f`(a)}" by auto;
  { fix y assume A5: "y ∈ R``{f`(a)}" 
    let ?x = "converse(f)`(y)"
    from A2 A5 have 
      "⟨f`(a),y⟩ ∈ R"  "f`(a) ∈ B"  and IV: "y∈B"
      by auto;
    with A1 have III: "⟨converse(f)`(f`(a)),?x⟩ ∈ r"
      using ord_iso_converse by simp;
    moreover from A1 A3 have "converse(f)`(f`(a)) = a"
      using ord_iso_is_bij left_inverse_bij by blast;
    ultimately have "f`(?x) ∈ {f`(x). x ∈  r``{a} }"
      by auto;
    moreover from A1 IV have "f`(?x) = y"
      using ord_iso_is_bij right_inverse_bij by blast;
    moreover from A1 I have "f``(r``{a}) = {f`(x). x ∈  r``{a} }"
      using ord_iso_is_bij bij_is_fun func_imagedef by blast;
    ultimately have "y ∈ f``(r``{a})" by simp;
  } then show "R``{f`(a)} ⊆ f``(r``{a})" by auto;
qed;

text{*Order isomorphisms preserve collections of upper bounds.*}

lemma ord_iso_pres_up_bounds: 
  assumes A1: "f ∈ ord_iso(A,r,B,R)" and  
  A2: "r ⊆ A×A"  "R ⊆ B×B" and 
  A3: "C⊆A" 
  shows "{f``(r``{a}). a∈C} = {R``{b}. b ∈ f``(C)}"
proof;
  from A1 have T: "f:A->B"
      using ord_iso_is_bij bij_is_fun by simp
  { fix Y assume "Y ∈ {f``(r``{a}). a∈C}"
    then obtain a where I: "a∈C" and II: "Y = f``(r``{a})"
      by auto;
    from A3 I have "a∈A" by auto;
    with A1 A2 have "f``(r``{a}) = R``{f`(a)}"
      using ord_iso_pres_rel_image by simp;
    moreover from A3 T I have "f`(a) ∈ f``(C)"
      using func_imagedef by auto;
    ultimately have "f``(r``{a}) ∈ { R``{b}. b ∈ f``(C) }"
      by auto;
    with II have "Y ∈ { R``{b}. b ∈ f``(C) }" by simp;
  } then show "{f``(r``{a}). a∈C} ⊆ {R``{b}. b ∈ f``(C)}"
    by blast;
  { fix Y assume "Y ∈ {R``{b}. b ∈ f``(C)}"
    then obtain b where III: "b ∈ f``(C)" and IV: "Y = R``{b}"
      by auto;
    with A3 T obtain a where V: "a∈C" and "b = f`(a)"
      using func_imagedef by auto;
    with A3 IV have "a∈A" and "Y = R``{f`(a)}" by auto; 
    with A1 A2 have "Y = f``(r``{a})"
      using ord_iso_pres_rel_image by simp;
    with V have "Y ∈ {f``(r``{a}). a∈C}" by auto;
  } then show "{R``{b}. b ∈ f``(C)} ⊆ {f``(r``{a}). a∈C}"
    by auto;
qed;
    
text{*The image of the set of upper bounds is the set of upper bounds
  of the image.*}
  
lemma ord_iso_pres_min_up_bounds: 
  assumes A1: "f ∈ ord_iso(A,r,B,R)" and  A2: "r ⊆ A×A"  "R ⊆ B×B" and 
  A3: "C⊆A" and A4: "C≠0"
  shows "f``(\<Inter>a∈C. r``{a}) = (\<Inter>b∈f``(C). R``{b})"
proof -
  from A1 have "f ∈ inj(A,B)"
    using ord_iso_is_bij bij_is_inj by simp;
  moreover note A4
  moreover from A2 A3 have "∀a∈C. r``{a} ⊆ A" by auto;
  ultimately have 
    "f``(\<Inter>a∈C. r``{a}) = ( \<Inter>a∈C. f``(r``{a}) )"
    using inj_image_of_Inter by simp;
  also from A1 A2 A3 have
    "( \<Inter>a∈C. f``(r``{a}) ) = ( \<Inter>b∈f``(C). R``{b} )"
    using ord_iso_pres_up_bounds by simp;
  finally show "f``(\<Inter>a∈C. r``{a}) = (\<Inter>b∈f``(C). R``{b})"
    by simp;
qed;

text{*Order isomorphisms preserve completeness.*}

lemma ord_iso_pres_compl: 
  assumes A1: "f ∈ ord_iso(A,r,B,R)" and 
  A2: "r ⊆ A×A"  "R ⊆ B×B" and A3: "R {is complete}"
  shows "r {is complete}"
proof -
  { fix C
    assume A4: "IsBoundedAbove(C,r)"  "C≠0"
    with A1 A2 A3 have 
      "HasAminimum(R,\<Inter>b ∈ f``(C). R``{b})"
      using ord_iso_pres_bound_above IsComplete_def
      by simp;
    moreover
    from A2 A4 have I: "C ⊆ A" using Order_ZF_3_L1A
      by blast;
    with A1 A2 A4 have "f``(\<Inter>a∈C. r``{a}) = (\<Inter>b∈f``(C). R``{b})"
      using ord_iso_pres_min_up_bounds by simp;
    ultimately have "HasAminimum(R,f``(\<Inter>a∈C. r``{a}))"
      by simp;
    moreover
    from A2 A4 have "C≠0" and "∀a∈C. r``{a} ⊆ A" by auto;
    then have "( \<Inter>a∈C. r``{a} ) ⊆ A" using ZF1_1_L7 by simp;
    moreover note A1 A2 
    ultimately have "HasAminimum(r, \<Inter>a∈C. r``{a} )"
      using ord_iso_pres_has_min by simp;
  } then show "r {is complete}" using IsComplete_def
    by simp;
qed;

text{*If the original relation is complete, then the induced
  one is complete.*}

lemma ind_rel_pres_compl: assumes A1: "f ∈ bij(A,B)"
  and A2: "R ⊆ B×B" and A3: "R {is complete}"
  shows "InducedRelation(f,R) {is complete}"
proof -
  let ?r = "InducedRelation(f,R)"
  from A1 have "f ∈ ord_iso(A,?r,B,R)"
    using bij_is_ord_iso by simp;
  moreover from A1 A2 have "?r ⊆ A×A"
    using bij_is_fun ind_rel_domain by simp;
  moreover note A2 A3
  ultimately show "?r {is complete}"
    using ord_iso_pres_compl by simp; 
qed;
  


end;