Theory func_ZF

theory func_ZF
imports func1
(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2005 - 2008  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 func1

begin

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

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. *}
 
text{*Since we are writing in generic set notation, 
  the definition below is a bit complicated. Here it what it says:
  Given a set $X$ and another set $f$ (that represents a binary function on $X$) 
  we are defining $f$ lifted to function space over $X$
  as the binary function (a set of pairs) on the space 
  $F = X \rightarrow \textrm{range}(f)$ such that the value of this function
  on pair $\langle a,b \rangle$ of functions on $X$ is another function $c$ on $X$
  with values defined by $c(x) = f\langle a(x), b(x)\rangle$. 
  *}

definition
Lift2FcnSpce (infix "{lifted to function space over}" 65) where
 "f {lifted to function space over} X ≡ 
  {⟨ p,{⟨x,f`⟨fst(p)`(x),snd(p)`(x)⟩⟩. x ∈ X}⟩. 
  p ∈ (X->range(f))×(X->range(f))}";

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,f`⟨fst(p)`(x),snd(p)`(x)⟩⟩. x ∈ X} : X->range(f)"
  proof -;
    have "∀x∈X. f`⟨fst(p)`(x),snd(p)`(x)⟩ ∈ range(f)"
    proof;
      fix x assume "x∈X"
      let ?p = "⟨fst(p)`(x),snd(p)`(x)⟩"
      from A2 `x∈X` 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 ZF_fun_from_total 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 A1: "f : Y×Y->Y" 
  and A2: "p ∈ (X->range(f))×(X->range(f))" and A3: "x∈X"
  and A4: "P = {⟨x,f`⟨fst(p)`(x),snd(p)`(x)⟩⟩. x ∈ X}"
  shows "P`(x) = f`⟨fst(p)`(x),snd(p)`(x)⟩" 
proof -
  from A1 A2 have 
    "{⟨x,f`⟨fst(p)`(x),snd(p)`(x)⟩⟩. x ∈ X} : X -> range(f)"
    using func_ZF_1_L1 by simp;
  with A4 have "P :  X -> range(f)" by simp;
  with  A3 A4 show "P`(x) = f`⟨fst(p)`(x),snd(p)`(x)⟩"
    using ZF_fun_from_tot_val by simp;
qed;

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

theorem 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 assms Lift2FcnSpce_def func_ZF_1_L1 ZF_fun_from_total 
  by simp;

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

theorem 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 = "⟨s,r⟩"
  let ?P = "{⟨x,f`⟨fst(?p)`(x),snd(?p)`(x)⟩⟩. x ∈ X}"; 
  from A1 A3 A4 have
    "f : Y×Y->Y"  "?p ∈ (X->range(f))×(X->range(f))"
    "x∈X"  "?P = {⟨x,f`⟨fst(?p)`(x),snd(?p)`(x)⟩⟩. x ∈ X}" 
    by auto;
  then have "?P`(x) = f`⟨fst(?p)`(x),snd(?p)`(x)⟩"
    by (rule func_ZF_1_L2);
  hence "?P`(x) = f`⟨s`(x),r`(x)⟩" by auto;
  moreover have "?P = F`⟨s,r⟩"
  proof -
    from A1 A2 have "F : (X->range(f))×(X->range(f))->(X->range(f))"
      using func_ZF_1_L3 by simp;
    moreover from A3 have "?p ∈ (X->range(f))×(X->range(f))"
      by auto;
    moreover from A2 have
      "F = {⟨p,{⟨x,f`⟨fst(p)`(x),snd(p)`(x)⟩⟩. x ∈ X}⟩. 
      p ∈ (X->range(f))×(X->range(f))}"
      using Lift2FcnSpce_def by simp;
    ultimately show ?thesis using ZF_fun_from_tot_val
      by simp;
  qed;
  ultimately show "(F`⟨s,r⟩)`(x) = f`⟨s`(x),r`(x)⟩" by auto;
qed

section{*Associative and commutative operations*}

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

text{*Typically we say that a binary operation "$\cdot $" 
  on a set $G$ is ''associative''
  if $(x\cdot y)\cdot z = x\cdot (y\cdot z)$ for all $x,y,z \in G$.
  Our actual definition below does not use the multiplicative notation
  so that we can apply it equally to the additive notation $+$ 
  or whatever infix symbol we may want to use. 
  Instead, we use the generic set theory notation
  and write $P\langle x,y \rangle$ to denote the value of the operation
  $P$ on a pair $\langle x,y \rangle \in G\times G$.*}

definition 
  IsAssociative (infix "{is associative on}" 65) where
  "P {is associative on} G ≡ P : G×G->G ∧ 
  (∀ x ∈ G. ∀ y ∈ G. ∀ z ∈ G. 
  ( P`(⟨P`(⟨x,y⟩),z⟩) = P`( ⟨x,P`(⟨y,z⟩)⟩ )))"

text{*A binary function $f: X\times X \rightarrow Y$ is commutative
  if $f\langle x,y \rangle = f\langle y,x \rangle$. Note that
  in the definition of associativity above we talk about binary
  ''operation'' and here we say use the term binary ''function''. 
  This is not set in stone, but usually the word "operation" is used 
  when the range is a factor of the domain, while the word "function"
  allows the range to be a completely unrelated set. *}

definition
  IsCommutative (infix "{is commutative on}" 65) where
  "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)" and "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 "x∈X"
    from A1 have "range(f)⊆G"
      using func1_1_L5B by simp;
    with A3 `x∈X` have "s`(x) ∈ G" and "r`(x) ∈ G"
      using apply_type by auto;
    with A1 A2 A3 A4 `x∈X` 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 assms 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 I:
    "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 "x∈X"
    from A4 have "f:G×G->G"
      using IsAssociative_def by simp;
    then have "range(f)⊆G"
      using func1_1_L5B by simp;
    with A3 `x∈X` have 
      "s`(x) ∈ G" "r`(x) ∈ G" "q`(x) ∈ G"
      using apply_type by auto;
    with A2 I A3 A4 `x∈X` `f:G×G->G` 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 conditions under which
  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 "x∈A" and "y∈A"
    with A2 have "x∈X" and "y∈X" by auto;
    with A3 `x∈A` `y∈A` have 
      "restrict(f,A×A)`⟨x,y⟩ = restrict(f,A×A)`⟨y,x⟩"
      using IsCommutative_def restrict_if by simp }
  then show ?thesis using IsCommutative_def by simp;
qed;
  
text{*Next we define what it means that a set is closed with 
  respect to an operation.*}

definition
  IsOpClosed (infix "{is closed under}" 65) where
  "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 I: "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 I have
    "f`⟨f`⟨x,y⟩,z⟩ = f`⟨x,f`⟨y,z⟩⟩"
    using IsAssociative_def by simp;
  ultimately show ?thesis by simp;
qed;

text{*An 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 assms 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 assms 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 assms IsOpClosed_def by simp;

section{*Compositions*}

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 and denoted with the letter @{text "O"}. 
  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)$.*}

text{*We define the notion of composition on the set $X$ as the
  binary operation on the function space $X\rightarrow X$
  that takes two functions and creates the their composition.*}

definition
  "Composition(X) ≡ 
  {⟨p,fst(p) O snd(p)⟩. p ∈ (X->X)×(X->X)}"

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 ZF_fun_from_total by simp;

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

lemma func_ZF_5_L2: assumes "f:X->X" and "g:X->X"
  shows "Composition(X)`⟨f,g⟩ = f O g" 
proof -
  from assms have 
    "Composition(X) : (X->X)×(X->X)->(X->X)"
    "⟨f,g⟩ ∈ (X->X)×(X->X)"
    "Composition(X) = {⟨p,fst(p) O snd(p)⟩. p ∈ (X->X)×(X->X)}"
    using  func_ZF_5_L1 Composition_def by auto;
  then show "Composition(X)`⟨f,g⟩ = f O g"
    using  ZF_fun_from_tot_val by auto;
qed;

text{*What is the value 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 assms 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 I:
    "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 "x∈X"
    with A1 A2 I 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 @{text "Perm"} theory.*}

text{*A function that maps every point to itself is the identity on its domain.*}

lemma indentity_fun: assumes A1: "f:X->Y" and A2:"∀x∈X. f`(x)=x"
  shows "f = id(X)"
proof -
  from assms have "f:X->Y" and "id(X):X->X" and "∀x∈X. f`(x) = id(X)`(x)"
    using id_type id_conv by auto 
  then show ?thesis by (rule func_eq)
qed

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 note A1
  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;

text{*An intuitively clear, but surprsingly nontrivial fact:identity is the only function from 
  a singleton to itself.*}

lemma singleton_fun_id: shows "({x} -> {x}) = {id({x})}"
proof;
  show "{id({x})} ⊆ ({x} -> {x})"
    using id_def by simp;
  { let ?g = "id({x})"
    fix f assume "f : {x} -> {x}"
    then have "f : {x} -> {x}" and "?g : {x} -> {x}"
      using id_def by auto;
    moreover from `f : {x} -> {x}` have "∀x ∈ {x}. f`(x) = ?g`(x)"
      using apply_funtype id_def by auto;
    ultimately have "f = ?g" by (rule func_eq)
  } then show  "({x} -> {x}) ⊆ {id({x})}" by auto;
qed;

text{*Another trivial fact: identity is the only bijection of a singleton
  with itself.*}

lemma single_bij_id: shows "bij({x},{x}) = {id({x})}"
proof;
  show "{id({x})} ⊆ bij({x},{x})" using id_bij
    by simp;
  { fix f assume "f ∈ bij({x},{x})"
    then have "f : {x} -> {x}" using bij_is_fun
      by simp;
    then have "f ∈ {id({x})}" using singleton_fun_id
      by simp;
  } then show "bij({x},{x}) ⊆ {id({x})}" by auto;
qed;

text{*A kind of induction for the identity: if a function
  $f$ is the identity on a set with a fixpoint of $f$
  removed, then it is the indentity on the whole set.*}

lemma id_fixpoint_rem: assumes A1: "f:X->X" and
  A2: "p∈X" and A3: "f`(p) = p" and 
  A4: "restrict(f, X-{p}) = id(X-{p})"
  shows "f = id(X)"
proof -
  from A1 have "f: X->X" and "id(X) : X->X"
    using id_def by auto;
  moreover
  { fix x assume "x∈X"
    { assume "x ∈ X-{p}"
      then have "f`(x) = restrict(f, X-{p})`(x)"
	using restrict by simp
      with A4 `x ∈ X-{p}` have "f`(x) = x"
	using id_def by simp }
    with A2 A3 `x∈X` have "f`(x) = x" by auto;
  } then have "∀x∈X. f`(x) = id(X)`(x)"
    using id_def by simp;
  ultimately show "f = id(X)" by (rule func_eq);
qed

section{*Lifting to subsets*}

text{*Suppose we have a binary operation $f : X \times X \rightarrow X$
  written additively as $f\langle x,y\rangle = x + y$. Such operation
  naturally defines another binary operation on the subsets of $X$
  that satisfies $A+B = \{ x+y : x \in A, y\in B\}$. This new operation 
  which we will call "$f$ lifted to subsets" inherits many properties
  of $f$, such as associativity, commutativity and existence of the 
  neutral element. This notion is useful for considering interval arithmetics.
  *}

text{*The next definition describes the notion of a binary operation
  lifted to subsets. It is written in a way that might be a bit unexpected,
  but really it is the same as the intuitive definition, but shorter.
  In the definition we take a pair $p \in Pow(X)\times Pow(X)$, say
  $p = \langle A, B\rangle $, where $A,B \subseteq X$. 
  Then we assign this pair of sets the set 
  $\{f\langle x,y \rangle : x\in A, y\in B \} = \{ f(x'): x' \in A\times B\}$
  The set on the right hand side is the same as the image
  of $A\times B$ under $f$. In the definition we don't use $A$ and $B$ symbols,
  but write @{text "fst(p)"} and @{text "snd(p)"}, resp. Recall that in Isabelle/ZF
  @{text "fst(p)"} and  @{text "snd(p)"} denote the first and second components
  of an ordered pair $p$.
  See the lemma @{text "lift_subsets_explained"} for a more intuitive
  notation.*}

definition
  Lift2Subsets (infix "{lifted to subsets of}" 65) where
  "f {lifted to subsets of} X ≡ 
  {⟨p, f``(fst(p)×snd(p))⟩. p ∈ Pow(X)×Pow(X)}";


text{*The lift to subsets defines a binary operation on the subsets.*}

lemma lift_subsets_binop: assumes A1: "f : X × X -> Y"
  shows "(f {lifted to subsets of} X) : Pow(X) × Pow(X) -> Pow(Y)"
proof -
  let ?F = "{⟨p, f``(fst(p)×snd(p))⟩. p ∈ Pow(X)×Pow(X)}"
  from A1 have "∀p ∈ Pow(X) × Pow(X). f``(fst(p)×snd(p)) ∈ Pow(Y)"
    using func1_1_L6 by simp;
  then have "?F : Pow(X) × Pow(X) -> Pow(Y)"
    by (rule ZF_fun_from_total);
  then show ?thesis unfolding Lift2Subsets_def by simp;
qed

text{*The definition of the lift to subsets rewritten in a more intuitive
  notation. We would like to write the last assertion as
  @{text "F`⟨A,B⟩ = {f`⟨x,y⟩. x ∈ A, y ∈ B}"}, but Isabelle/ZF does not allow
  such syntax.*}

lemma lift_subsets_explained: assumes A1: "f : X×X -> Y"
  and A2: "A ⊆ X"  "B ⊆ X" and A3: "F = f {lifted to subsets of} X"
  shows 
  "F`⟨A,B⟩ ⊆ Y" and
  "F`⟨A,B⟩ = f``(A×B)"
  "F`⟨A,B⟩ = {f`(p). p ∈ A×B}"
  "F`⟨A,B⟩ = {f`⟨x,y⟩ . ⟨x,y⟩ ∈ A×B}"
proof -
  let ?p = "⟨A,B⟩"
  from assms have 
    I: "F : Pow(X) × Pow(X) -> Pow(Y)" and  "?p ∈ Pow(X) × Pow(X)"
    using lift_subsets_binop by auto;
  moreover from A3 have "F = {⟨p, f``(fst(p)×snd(p))⟩. p ∈ Pow(X)×Pow(X)}"
    unfolding  Lift2Subsets_def by simp
  ultimately show "F`⟨A,B⟩ =  f``(A×B)"
    using  ZF_fun_from_tot_val by auto;
  also
  from A1 A2 have "A×B ⊆ X×X" by auto;
  with A1 have "f``(A×B) = {f`(p). p ∈ A×B}"
    by (rule func_imagedef)
  finally show  "F`⟨A,B⟩ = {f`(p) . p ∈ A×B}" by simp;
  also
  have "∀x∈A. ∀y ∈ B. f`⟨x,y⟩ = f`⟨x,y⟩" by simp;
  then have "{f`(p). p ∈ A×B} = {f`⟨x,y⟩.  ⟨x,y⟩ ∈ A×B}"
    by (rule ZF1_1_L4A);
  finally show "F`⟨A,B⟩ = {f`⟨x,y⟩ . ⟨x,y⟩ ∈ A×B}"
    by simp
  from A2 I show "F`⟨A,B⟩ ⊆ Y" using apply_funtype by blast
qed

text{*A sufficient condition for a point to belong to a result of
  lifting to subsets.*}

lemma lift_subset_suff:  assumes A1: "f : X × X -> Y" and 
  A2: "A ⊆ X"  "B ⊆ X" and A3: "x∈A" "y∈B" and
  A4: "F = f {lifted to subsets of} X"
  shows "f`⟨x,y⟩ ∈ F`⟨A,B⟩"
proof -
  from A3 have "f`⟨x,y⟩ ∈ {f`(p) . p ∈ A×B}" by auto;
  moreover from A1 A2 A4 have "{f`(p). p ∈ A×B} = F`⟨A,B⟩ "
    using lift_subsets_explained by simp;
  ultimately show "f`⟨x,y⟩ ∈ F`⟨A,B⟩" by simp;
qed;

text{*A kind of converse of @{text "lift_subset_apply"}, providing
  a necessary condition for a point to be in the result of lifting to 
  subsets.*}

lemma lift_subset_nec: assumes A1: "f : X × X -> Y" and 
  A2: "A ⊆ X"  "B ⊆ X" and 
  A3: "F = f {lifted to subsets of} X" and
  A4: "z ∈ F`⟨A,B⟩"
  shows "∃x y. x∈A ∧ y∈B ∧ z = f`⟨x,y⟩"
proof -
  from A1 A2 A3 have "F`⟨A,B⟩ = {f`(p). p ∈ A×B}"
    using lift_subsets_explained by simp;
  with A4 show ?thesis by auto;
qed

text{*Lifting to subsets inherits commutativity.*}

lemma lift_subset_comm: assumes A1: "f : X × X -> Y" and 
  A2: "f {is commutative on} X" and
  A3: "F = f {lifted to subsets of} X"
  shows "F {is commutative on} Pow(X)"
proof -
  have "∀A ∈ Pow(X). ∀B ∈ Pow(X). F`⟨A,B⟩ = F`⟨B,A⟩"
  proof -
    { fix A assume "A ∈ Pow(X)"
      fix B assume "B ∈ Pow(X)"
      have  "F`⟨A,B⟩ = F`⟨B,A⟩"
      proof -
	have "∀z ∈  F`⟨A,B⟩. z ∈  F`⟨B,A⟩"
	proof;
	  fix z assume I: "z ∈ F`⟨A,B⟩"
	  with A1 A3 `A ∈ Pow(X)` `B ∈ Pow(X)` have 
	    "∃x y. x∈A ∧ y∈B ∧ z = f`⟨x,y⟩"
	    using lift_subset_nec by simp;
	  then obtain x y where "x∈A" and "y∈B" and "z = f`⟨x,y⟩"
	    by auto;
	  with A2 `A ∈ Pow(X)` `B ∈ Pow(X)` have "z = f`⟨y,x⟩"
	    using IsCommutative_def by auto;
	  with A1 A3 I `A ∈ Pow(X)` `B ∈ Pow(X)` `x∈A` `y∈B` 
	  show "z ∈ F`⟨B,A⟩" using lift_subset_suff by simp;
	qed
	moreover have "∀z ∈  F`⟨B,A⟩. z ∈  F`⟨A,B⟩"
	proof;
	  fix z assume I: "z ∈ F`⟨B,A⟩"
	  with A1 A3 `A ∈ Pow(X)` `B ∈ Pow(X)` have 
	    "∃x y. x∈B ∧ y∈A ∧ z = f`⟨x,y⟩"
	    using lift_subset_nec by simp;
	  then obtain x y where "x∈B" and "y∈A" and "z = f`⟨x,y⟩"
	    by auto;
	  with A2 `A ∈ Pow(X)` `B ∈ Pow(X)` have "z = f`⟨y,x⟩"
	    using IsCommutative_def by auto;
	  with A1 A3 I `A ∈ Pow(X)` `B ∈ Pow(X)` `x∈B` `y∈A` 
	  show "z ∈ F`⟨A,B⟩" using lift_subset_suff by simp;
	qed;
	ultimately show "F`⟨A,B⟩ = F`⟨B,A⟩" by auto
      qed;
    } thus ?thesis by auto;
  qed;
  then show "F {is commutative on} Pow(X)" 
    unfolding IsCommutative_def by auto;
qed;

text{*Lifting to subsets inherits associativity. 
  To show that 
  $F\langle \langle A,B\rangle C\rangle = F\langle A,F\langle B,C\rangle\rangle$ 
  we prove two inclusions and the proof of the second inclusion is very similar
  to the proof of the first one.*}

lemma lift_subset_assoc:  assumes A1: "f : X × X -> X" and 
  A2: "f {is associative on} X" and
  A3: "F = f {lifted to subsets of} X"
  shows "F {is associative on} Pow(X)"
proof -
  from A1 A3 have "F : Pow(X)×Pow(X) -> Pow(X)"
    using lift_subsets_binop by simp;
  moreover have "∀A ∈ Pow(X).∀B ∈ Pow(X). ∀C ∈ Pow(X). 
    F`⟨F`⟨A,B⟩,C⟩ = F`⟨A,F`⟨B,C⟩⟩"
  proof -
    { fix A B C
      assume "A ∈ Pow(X)"  "B ∈ Pow(X)"  "C ∈ Pow(X)"
      have "F`⟨F`⟨A,B⟩,C⟩ ⊆ F`⟨A,F`⟨B,C⟩⟩"
      proof;
	fix z assume I: "z ∈ F`⟨F`⟨A,B⟩,C⟩"
	from A1 A3 `A ∈ Pow(X)`  `B ∈ Pow(X)`
	have "F`⟨A,B⟩ ∈ Pow(X)"
	  using lift_subsets_binop apply_funtype by blast;
	with A1 A3 `C ∈ Pow(X)` I have
	  "∃x y. x ∈ F`⟨A,B⟩ ∧ y ∈ C ∧ z = f`⟨x,y⟩"
	  using lift_subset_nec by simp;
	then obtain x y where 
	  II: "x ∈ F`⟨A,B⟩" and "y ∈ C" and III: "z = f`⟨x,y⟩"
	  by auto;
	from A1 A3 `A ∈ Pow(X)`  `B ∈ Pow(X)` II have
	  "∃ s t. s ∈ A ∧ t ∈ B ∧ x = f`⟨s,t⟩"
	  using lift_subset_nec by auto;
	then obtain s t where "s∈A" and "t∈B" and "x = f`⟨s,t⟩"
	  by auto;
	with A2 `A ∈ Pow(X)`  `B ∈ Pow(X)` `C ∈ Pow(X)` III 
	  `s∈A` `t∈B` `y∈C` have IV: "z = f`⟨s, f`⟨t,y⟩⟩"
	  using IsAssociative_def by blast;
	from A1 A3 `B ∈ Pow(X)`  `C ∈ Pow(X)`  `t∈B`  `y∈C`
	have "f`⟨t,y⟩ ∈ F`⟨B,C⟩" using lift_subset_suff by simp;
	moreover from A1 A3 `B ∈ Pow(X)`  `C ∈ Pow(X)`
	have "F`⟨B,C⟩ ⊆ X" using lift_subsets_binop apply_funtype 
	  by blast;
	moreover note A1 A3 `A ∈ Pow(X)` `s∈A` IV
	ultimately show "z ∈ F`⟨A,F`⟨B,C⟩⟩"
	  using lift_subset_suff by simp;
      qed;
      moreover have "F`⟨A,F`⟨B,C⟩⟩ ⊆ F`⟨F`⟨A,B⟩,C⟩"
      proof;
	fix z assume I: "z ∈ F`⟨A,F`⟨B,C⟩⟩"
	from A1 A3 `B ∈ Pow(X)`  `C ∈ Pow(X)`
	have "F`⟨B,C⟩ ∈ Pow(X)"
	  using lift_subsets_binop apply_funtype by blast;
	with A1 A3 `A ∈ Pow(X)` I have
	  "∃x y. x ∈ A ∧ y ∈ F`⟨B,C⟩ ∧ z = f`⟨x,y⟩"
	  using lift_subset_nec by simp;
	then obtain x y where 
	  "x ∈ A" and II: "y ∈ F`⟨B,C⟩" and III: "z = f`⟨x,y⟩"
	  by auto;
	from A1 A3 `B ∈ Pow(X)`  `C ∈ Pow(X)` II have
	  "∃ s t. s ∈ B ∧ t ∈ C ∧ y = f`⟨s,t⟩"
	  using lift_subset_nec by auto;
	then obtain s t where "s∈B" and "t∈C" and "y = f`⟨s,t⟩"
	  by auto;
	with III have "z = f`⟨x,f`⟨s,t⟩⟩" by simp;
	moreover from  A2 `A ∈ Pow(X)`  `B ∈ Pow(X)`  `C ∈ Pow(X)`
	  `x∈A` `s∈B` `t∈C` have "f`⟨f`⟨x,s⟩,t⟩ = f`⟨x,f`⟨s,t⟩⟩"
	  using IsAssociative_def by blast;
	ultimately have IV: "z = f`⟨f`⟨x,s⟩,t⟩" by simp;
	from A1 A3 `A ∈ Pow(X)`  `B ∈ Pow(X)`  `x∈A`  `s∈B`
	have "f`⟨x,s⟩ ∈ F`⟨A,B⟩" using lift_subset_suff by simp;
	moreover from A1 A3 `A ∈ Pow(X)`  `B ∈ Pow(X)`
	have "F`⟨A,B⟩ ⊆ X" using lift_subsets_binop apply_funtype 
	  by blast;
	moreover note A1 A3 `C ∈ Pow(X)` `t∈C` IV;
	ultimately show "z ∈ F`⟨F`⟨A,B⟩,C⟩"
	  using lift_subset_suff by simp;
      qed;
      ultimately have "F`⟨F`⟨A,B⟩,C⟩ = F`⟨A,F`⟨B,C⟩⟩" by auto;
    } thus ?thesis by auto;
  qed
  ultimately show ?thesis unfolding IsAssociative_def
    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 @{text "EquivClass1"} theory 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.*}

definition
  "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 
    "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 ?thesis
    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 assms 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


end;