Theory EquivClass1

(* 
    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{EquivClass1.thy}*}

theory EquivClass1 imports EquivClass func_ZF ZF1 

begin

text{*In this theory file we extend the  work on equivalence relations 
  done in the standard Isabelle's EquivClass.thy file. The problem that 
  we have with the EquivClass.thy is that the notions congruent and congruent2
  are defined for meta-functions rather then ZF - functions (subsets of 
  Cartesian products). This causes inflexibility (that is typical for typed 
  set theories) in making the notions depend on additional parameters
  For example the congruent2 there takes $[i,[i,i]=>i]$ as parameters, that is 
  the second parameter is a meta-function that takes two sets and results in 
  a set. So, when our function depends on additional parameters, 
  (for example the function we want to be 
  congruent depends on a group and we want to show that for all groups 
  the function is congruent) there is no easy way to use that notion.
  The ZF functions are sets and there is no problem if in actual 
  application this set depends on some parameters. *}

section{*Congruent functions and projections on the quotient*}

text{*First we define the notion of function that maps equivalent 
  elements to equivalent values. We use similar names as
  in the original @{text "EquivClass.thy"} file to indicate the conceptual 
  correspondence of the notions. Then we define the projection of
  a function onto the quotient space. We will show that if the function is
  congruent the projection is 
  a mapping from the quotient space into itself. In standard math the 
  condion that the function is congruent allows to show that the value
  of the projection does not depend on the choice of elements that represent
  the equivalence classes. We set up things a little differently to avoid
  making choices.*}

constdefs
  "Congruent(r,f) ≡
  (∀x y. <x,y> ∈ r  --> <f`(x),f`(y)> ∈ r)"

  "ProjFun(A,r,f) ≡
  {<c,d> ∈ (A//r)×(A//r). (\<Union>x∈c. r``{f`(x)}) = d}";

text{*Elements of equivalence classes belong to the set.*}

lemma EquivClass_1_L1: 
  assumes A1: "equiv(A,r)" and A2: "C ∈ A//r" and A3: "x∈C"
  shows "x∈A"
proof -;
  from A2 have "C ⊆ \<Union> (A//r)" by auto;
  with A1 A3 show "x∈A"
    using Union_quotient by auto;
qed;

text{*The image of a subset of $X$ under projection is a subset
  of $A/r$.*}

lemma EquivClass_1_L1A: 
  assumes "A⊆X" shows "{r``{x}. x∈A} ⊆ X//r"
  using prems quotientI by auto;

text{*If an element belongs to an equivalence class, then its image
  under relation is this equivalence class.*}

lemma EquivClass_1_L2: 
  assumes A1: "equiv(A,r)"  "C ∈ A//r" and A2: "x∈C"
  shows "r``{x} = C"
proof -;
  from A1 A2 have "x ∈ r``{x}" 
    using EquivClass_1_L1  equiv_class_self by simp;
  with A2 have T1:"r``{x}∩C ≠ 0" by auto;
  from A1 A2 have "r``{x} ∈ A//r"
    using EquivClass_1_L1 quotientI by simp;
  with A1 T1 show ?thesis
    using quotient_disj by blast;
qed;
      
text{*Elements that belong to the same equivalence class are equivalent.*}

lemma EquivClass_1_L2A:
  assumes "equiv(A,r)"  "C ∈ A//r"  "x∈C"  "y∈C"
  shows "<x,y> ∈ r" 
  using prems EquivClass_1_L2 EquivClass_1_L1 equiv_class_eq_iff
  by simp;

text{*Every $x$ is in the class of $y$, then they are equivalent.*}

lemma EquivClass_1_L2B: 
  assumes A1: "equiv(A,r)" and A2: "y∈A" and A3: "x ∈ r``{y}"
  shows "<x,y> ∈ r"
proof -;
  from A2 have  "r``{y} ∈ A//r"
    using quotientI by simp;
  with A1 A3 show ?thesis using
    EquivClass_1_L1 equiv_class_self equiv_class_nondisjoint by blast;
qed;
  
text{*If a function is congruent then the equivalence classes of the values
  that come from the arguments from the same class are the same.*}

lemma EquivClass_1_L3: 
  assumes A1: "equiv(A,r)" and A2: "Congruent(r,f)" 
  and A3: "C ∈ A//r"  "x∈C"  "y∈C" 
  shows "r``{f`(x)} = r``{f`(y)}"
proof -;
  from A1 A3 have "<x,y> ∈ r"
    using EquivClass_1_L2A by simp;
  with A2 have  "<f`(x),f`(y)> ∈ r"
    using Congruent_def by simp;
  with A1 show ?thesis using equiv_class_eq by simp
qed;

text{*The values of congruent functions are in the space.*}

lemma EquivClass_1_L4:
  assumes A1: "equiv(A,r)" and A2: "C ∈ A//r"  "x∈C"
  and A3: "Congruent(r,f)"
  shows "f`(x) ∈ A"
proof -;
  from A1 A2 have "x∈A";
    using EquivClass_1_L1 by simp;
  with A1 have "<x,x> ∈ r"
    using equiv_def refl_def by simp;
  with A3 have  "<f`(x),f`(x)> ∈ r"
    using Congruent_def by simp;
  with A1 show ?thesis using equiv_type by auto;
qed;

text{*Equivalence classes are not empty.*}

lemma EquivClass_1_L5: 
  assumes A1: "refl(A,r)" and A2: "C ∈ A//r"
  shows "C≠0"
proof -;
  from A2 obtain x where D1: "C = r``{x}" and D2: "x∈A"
    using quotient_def by auto;
  from D2 A1 have "x ∈ r``{x}" using refl_def by auto;
  with D1 show ?thesis by auto;
qed;
  
text{*To avoid using an axiom of choice, we define the projection using 
  the expression $\bigcup _{x\in C} r(\{f(x)\})$. 
  The next lemma shows that for
  congruent function this is in the quotient space $A/r$. *}

lemma EquivClass_1_L6:
  assumes A1: "equiv(A,r)" and A2: "Congruent(r,f)" 
  and A3:"C ∈ A//r"
  shows "(\<Union>x∈C. r``{f`(x)}) ∈ A//r"
proof -;
  from A1 A3 have "C≠0"
    using equiv_def EquivClass_1_L5 by auto;
  moreover from A2 A3 A1 have "∀x∈C. r``{f`(x)} ∈ A//r"
    using EquivClass_1_L4 quotientI by auto;
  moreover from A1 A2 A3 have 
    "∀x y. x∈C ∧ y∈C --> r``{f`(x)} = r``{f`(y)}" 
    using EquivClass_1_L3 by blast;
  ultimately show ?thesis by (rule ZF1_1_L2);
qed;

text{*Congruent functions can be projected.*}

lemma EquivClass_1_T1: 
  assumes "equiv(A,r)"  "Congruent(r,f)"
  shows "ProjFun(A,r,f) ∈ A//r -> A//r"
  using prems EquivClass_1_L6 ProjFun_def func1_1_L11A
  by simp;
  
text{*We now define congruent functions of two variables. Congruent2 
  corresponds to congruent2 in @{text "EquivClass.thy"}, 
  but uses ZF-functions rather than meta-functions.*}

constdefs
  "Congruent2(r,f) ≡
  (∀x1 x2 y1 y2. <x1,x2> ∈ r ∧ <y1,y2> ∈ r  --> 
  <f`<x1,y1>,f`<x2,y2> > ∈ r)"

  "ProjFun2(A,r,f) ≡
  {<p,d> ∈ ((A//r)×(A//r))×(A//r) . 
  (\<Union> z ∈ fst(p)×snd(p). r``{f`(z)}) = d}";


text{*The following lemma is a two-variables equivalent 
  of @{text "EquivClass_1_L3"}.*}

lemma EquivClass_1_L7: 
  assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
  and A3: "C1 ∈ A//r"  "C2 ∈ A//r" 
  and A4: "z1 ∈ C1×C2"  "z2 ∈ C1×C2"
  shows "r``{f`(z1)} = r``{f`(z2)}"
proof -;
  from A4 obtain x1 y1 x2 y2 where 
    "x1∈C1" and "y1∈C2" and D1:"z1 = <x1,y1>" and 
    "x2∈C1" and "y2∈C2" and D2:"z2 = <x2,y2>" 
    by auto;
  with A1 A3 have "<x1,x2> ∈ r" and "<y1,y2> ∈ r"
    using EquivClass_1_L2A by auto;
  with A2 have "<f`<x1,y1>,f`<x2,y2> > ∈ r"
    using Congruent2_def by simp;
  with A1 D1 D2 show ?thesis using equiv_class_eq by simp;
qed;

text{*The values of congruent functions of two variables are in the space.*}

lemma EquivClass_1_L8:
  assumes A1: "equiv(A,r)" and A2: "C1 ∈ A//r" and A3: "C2 ∈ A//r"
  and A4: "z ∈ C1×C2" and A5: "Congruent2(r,f)"
  shows "f`(z) ∈ A"
proof -;
  from A4 obtain x y where "x∈C1" and "y∈C2" and D1:"z = <x,y>"  
    by auto;
  with A1 A2 A3 have "x∈A" and "y∈A" 
    using EquivClass_1_L1 by auto;
  with A1 A4 have "<x,x> ∈ r" and "<y,y> ∈ r"
    using equiv_def refl_def by auto;
  with A5 have "<f`<x,y>, f`<x,y> > ∈ r"
    using Congruent2_def by simp;
  with A1 D1 show ?thesis using equiv_type by auto;
qed;

text{*The values of congruent functions are in the space. Note that
  although this lemma is intended to be used with functions, we don't
  need to assume that we $f$ is a function.*}

lemma EquivClass_1_L8A:
  assumes A1: "equiv(A,r)" and A2: "x∈A"  "y∈A"
  and A3: "Congruent2(r,f)"
  shows "f`<x,y> ∈ A"
proof -
  from A1 A2 have "r``{x} ∈ A//r" "r``{y} ∈ A//r" 
    "<x,y> ∈ r``{x}×r``{y}"
    using equiv_class_self quotientI by auto;
  with A1 A3 show ?thesis using EquivClass_1_L8 by simp;
qed;
  
text{*The following lemma is a two-variables equivalent of 
  @{text "EquivClass_1_L6"}.*}

lemma EquivClass_1_L9:
  assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)" 
  and A3: "p ∈ (A//r)×(A//r)"
  shows "(\<Union> z ∈ fst(p)×snd(p). r``{f`(z)}) ∈ A//r"
proof -;
  from A3 have D1:"fst(p) ∈ A//r" and D2:"snd(p) ∈ A//r"
    by auto;
  with A1 A2 have 
    T1:"∀z ∈ fst(p)×snd(p). f`(z) ∈ A"
    using EquivClass_1_L8 by simp;
  from A3 A1 have "fst(p)×snd(p) ≠ 0" 
    using equiv_def EquivClass_1_L5 Sigma_empty_iff
    by auto;
  moreover from A1 T1 have 
    "∀z ∈ fst(p)×snd(p). r``{f`(z)} ∈ A//r"
    using quotientI by simp;
  moreover from A1 A2 D1 D2 have
    "∀z1 z2. z1 ∈ fst(p)×snd(p) ∧ z2 ∈ fst(p)×snd(p) --> 
    r``{f`(z1)} = r``{f`(z2)}"
    using EquivClass_1_L7 by blast;
   ultimately show ?thesis by (rule ZF1_1_L2);
qed;

text{*Congruent functions of two variables can be projected.*}

theorem EquivClass_1_T1: 
  assumes "equiv(A,r)"  "Congruent2(r,f)"
  shows "ProjFun2(A,r,f) ∈ (A//r)×(A//r) -> A//r"
  using prems EquivClass_1_L9 ProjFun2_def func1_1_L11A by simp;

text{*We define the projection on the quotient space as a function that takes
  an element of $A$ and assigns its equivalence class in $A/r$.*}

constdefs
  "Proj(A,r) ≡ {<x,c> ∈ A×(A//r). r``{x} = c}"

text{*The projection diagram commutes. I wish I knew how to draw this diagram
  in \LaTeX. *}

lemma EquivClass_1_L10: assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)" 
  and A3: "x∈A"  "y∈A"
  shows "ProjFun2(A,r,f)`<r``{x},r``{y}> = r``{f`<x,y>}"
proof -;
  from A3 A1 have "r``{x} × r``{y} ≠ 0"
    using quotientI equiv_def EquivClass_1_L5 Sigma_empty_iff
    by auto;
  moreover have 
    "∀z ∈ r``{x}×r``{y}.  r``{f`(z)} = r``{f`<x,y>}"
  proof;
    fix z assume A4:"z ∈ r``{x}×r``{y}"
    from A1 A3 have 
      "r``{x} ∈ A//r" "r``{y} ∈ A//r"
      "<x,y> ∈ r``{x}×r``{y}"
      using quotientI equiv_class_self by auto;
    with A1 A2 A4 show
      "r``{f`(z)} = r``{f`<x,y>}"
      using EquivClass_1_L7 by blast;
  qed;
  ultimately have 
    "(\<Union>z ∈ r``{x}×r``{y}. r``{f`(z)}) =  r``{f`<x,y>}"
    by (rule ZF1_1_L1);
  moreover from A3 A1 A2 have 
    "ProjFun2(A,r,f)`<r``{x},r``{y}> = 
    (\<Union>z ∈ r``{x}×r``{y}. r``{f`(z)})"
    using quotientI EquivClass_1_T1 ProjFun2_def func1_1_L11B 
    by simp;
  ultimately show ?thesis by simp;
qed;

section{*Projecting commutative, associative and distributive operations.*}

text{*In this section we show that if the operations are congruent with
  respect to an equivalence relation then the projection to the quotient 
  space preserves commutativity, associativity and distributivity.*}

text{*The projection of commutative operation is commutative.*}

lemma EquivClass_2_L1: assumes 
  A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
  and A3: "f {is commutative on} A"
  and A4: "c1 ∈ A//r"  "c2 ∈ A//r"
  shows "ProjFun2(A,r,f)` <c1,c2> =  ProjFun2(A,r,f)`<c2,c1>"
proof -;
  from A4 obtain x y where D1:
    "c1 = r``{x}" "c2 = r``{y}"
    "x∈A" "y∈A"
    using quotient_def by auto;
  with A1 A2 have "ProjFun2(A,r,f)` <c1,c2> =  r``{f`<x,y>}"
    using EquivClass_1_L10 by simp;
  also from A3 D1 have
    "r``{f`<x,y>} = r``{f`<y,x>}"
    using IsCommutative_def by simp;
  also from A1 A2 D1 have
    "r``{f`<y,x>} = ProjFun2(A,r,f)` <c2,c1>"
    using EquivClass_1_L10 by simp;
  finally show ?thesis by simp;
qed;

text{*The projection of commutative operation is commutative.*}

theorem EquivClass_2_T1:
  assumes "equiv(A,r)" and "Congruent2(r,f)"
  and "f {is commutative on} A"
  shows "ProjFun2(A,r,f) {is commutative on} A//r"
  using prems IsCommutative_def EquivClass_2_L1 by simp;
    
text{*The projection of an associative operation is associative.*}

lemma EquivClass_2_L2: 
  assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
  and A3: "f {is associative on} A"
  and A4: "c1 ∈ A//r"  "c2 ∈ A//r"  "c3 ∈ A//r"
  and A5: "g = ProjFun2(A,r,f)"
  shows "g`⟨g`<c1,c2>,c3⟩ = g`⟨c1,g`<c2,c3>⟩"
proof -
  from A4 obtain x y z where D1:
    "c1 = r``{x}" "c2 = r``{y}" "c3 = r``{z}"
    "x∈A" "y∈A" "z∈A"
    using quotient_def by auto;
  with A3 have T1:"f`<x,y> ∈ A" "f`<y,z> ∈ A"
    using IsAssociative_def apply_type by auto;
  with A1 A2 D1 A5 have 
    "g`⟨g`<c1,c2>,c3⟩ =  r``{f`<f`<x,y>,z>}"
    using EquivClass_1_L10 by simp;
  also from D1 A3 have 
    "… = r``{f`<x,f`<y,z> >}"
    using IsAssociative_def by simp;
  also from T1 A1 A2 D1 A5 have
    "… = g`⟨c1,g`<c2,c3>⟩"
    using EquivClass_1_L10 by simp;
  finally show ?thesis by simp;
qed;

text{*The projection of an associative operation is associative on the
  quotient.*}

theorem EquivClass_2_T2:
  assumes A1: "equiv(A,r)" and A2: "Congruent2(r,f)"
  and A3: "f {is associative on} A"
  shows "ProjFun2(A,r,f) {is associative on} A//r"
proof -;
  let ?g = "ProjFun2(A,r,f)"
  from A1 A2 have 
    "?g ∈ (A//r)×(A//r) -> A//r"
    using EquivClass_1_T1 by simp;
  moreover from A1 A2 A3 have
    "∀c1 ∈ A//r.∀c2 ∈ A//r.∀c3 ∈ A//r.
    ?g`<?g`<c1,c2>,c3> = ?g`< c1,?g`<c2,c3> >"
    using EquivClass_2_L2 by simp;
  ultimately show ?thesis
    using IsAssociative_def by simp;
qed;

text{*The essential condition to show that distributivity is preserved by 
  projections to quotient spaces, provided both operations are congruent
  with respect to the equivalence relation.*}

lemma EquivClass_2_L3: 
  assumes A1: "IsDistributive(X,A,M)"
  and A2: "equiv(X,r)" 
  and A3: "Congruent2(r,A)" "Congruent2(r,M)"
  and A4: "a ∈ X//r" "b ∈ X//r" "c ∈ X//r"
  and A5: "Ap = ProjFun2(X,r,A)" "Mp = ProjFun2(X,r,M)"
  shows "Mp`⟨a,Ap`<b,c>⟩ = Ap`⟨ Mp`<a,b>,Mp`<a,c>⟩ ∧ 
  Mp`⟨ Ap`<b,c>,a ⟩ = Ap`⟨ Mp`<b,a>,Mp`<c,a>⟩"
proof;
  from A4 obtain x y z where "x∈X" "y∈X" "z∈X"
    "a = r``{x}" "b = r``{y}" "c = r``{z}"   
    using quotient_def by auto;
  with A1 A2 A3 A5 show 
    "Mp`⟨a,Ap`<b,c>⟩ = Ap`⟨ Mp`<a,b>,Mp`<a,c>⟩"
    "Mp`⟨ Ap`<b,c>,a ⟩ = Ap`⟨ Mp`<b,a>,Mp`<c,a>⟩"
    using EquivClass_1_L8A EquivClass_1_L10 IsDistributive_def
    by auto;
qed;

text{*Distributivity is preserved by 
  projections to quotient spaces, provided both operations are congruent
  with respect to the equivalence relation.*}

lemma EquivClass_2_L4: assumes A1: "IsDistributive(X,A,M)"
  and A2: "equiv(X,r)" 
  and A3: "Congruent2(r,A)" "Congruent2(r,M)"
  shows "IsDistributive(X//r,ProjFun2(X,r,A),ProjFun2(X,r,M))"
proof-;
 let ?Ap = "ProjFun2(X,r,A)" 
 let ?Mp = "ProjFun2(X,r,M)"
 from A1 A2 A3 have
   "∀a∈X//r.∀b∈X//r.∀c∈X//r.
   ?Mp`< a,?Ap`<b,c> > = ?Ap`< ?Mp`<a,b>,?Mp`<a,c> > ∧ 
   ?Mp`< ?Ap`<b,c>,a > = ?Ap`< ?Mp`<b,a>,?Mp`<c,a> >"
   using EquivClass_2_L3 by simp;
 then show ?thesis using IsDistributive_def by simp;
qed;

section{*Saturated sets*}

text{* In this section we consider sets that are saturated 
  with respect to an equivalence
  relation. A set $A$ is saturated with respect to a relation 
  $r$ if $A=r^{-1}(r(A))$. 
  For equivalence relations saturated sets are unions of equivalemce classes.
  This makes them useful as a tool to define subsets of 
  the quoutient space using properties
  of representants. Namely, we often define a set 
  $B\subseteq X/r$ by saying that
  $[x]_r \in B$ iff $x\in A$. 
  If $A$ is a saturated set, this definition is consistent in 
  the sense that it does not depend on the choice of $x$ to 
  represent $[x]_r$. *}

text{*The following defines the notion of saturated set. 
  Recall that in Isabelle 
  @{text "r-``(A)"} is the inverse image of $A$ with respect to relation $r$. 
  This definition is not specific to equivalence relations.*}

constdefs
  "IsSaturated(r,A) ≡ A = r-``(r``(A))"

text{*For equivalence relations a set is saturated iff it is an image 
  of itself.*}

lemma EquivClass_3_L1: assumes A1: "equiv(X,r)"
  shows "IsSaturated(r,A) <-> A = r``(A)"
proof;
  assume A2: "IsSaturated(r,A)"
  then have "A = (converse(r) O r)``(A)"
    using IsSaturated_def vimage_def image_comp
    by simp;
  also from A1 have "… = r``(A)"
    using equiv_comp_eq by simp;
  finally show "A = r``(A)" by simp;
next assume "A = r``(A)"
  with A1 have "A = (converse(r) O r)``(A)"
    using equiv_comp_eq by simp;
  also have "… =  r-``(r``(A))"
    using vimage_def image_comp by simp;
  finally have "A =  r-``(r``(A))" by simp;
  then show "IsSaturated(r,A)" using IsSaturated_def
    by simp;
qed;
  
text{*For equivalence relations sets are contained in their images.*} 

lemma EquivClass_3_L2: assumes A1: "equiv(X,r)" and A2: "A⊆X"
  shows "A ⊆ r``(A)"
proof
  fix a assume A3: "a∈A"
  with A1 A2 have "a ∈ r``{a}"
    using equiv_class_self by auto;
  with A3 show "a ∈ r``(A)" by auto;
qed;
  
text{*The next lemma shows that if "$\sim$" 
  is an equivalence relation and a set 
  $A$ is such that $a\in A$ and $a\sim b$ implies $b\in A$, then
  $A$ is saturated with respect to the relation.*}

lemma EquivClass_3_L3: assumes A1: "equiv(X,r)"
  and A2: "r ⊆ X×X" and A3: "A⊆X"
  and A4: "∀x∈A. ∀y∈X. ⟨x,y⟩ ∈ r --> y∈A"
  shows "IsSaturated(r,A)"
proof -
  from A2 A4 have "r``(A) ⊆ A"
    using image_iff by blast;
  moreover from A1 A3 have "A ⊆ r``(A)"
    using EquivClass_3_L2 by simp;
  ultimately have "A = r``(A)" by auto;
  with A1 show "IsSaturated(r,A)" using EquivClass_3_L1
    by simp;
qed;

text{*If $A\subseteq X$ and $A$ is saturated and $x\sim y$, then $x\in A$ iff
  $y\in A$. Here we we show only one direction.*}

lemma EquivClass_3_L4: assumes A1: "equiv(X,r)"
  and A2: "IsSaturated(r,A)" and A3: "A⊆X"
  and A4: "⟨x,y⟩ ∈ r" 
  and A5: "x∈X"  "y∈A"
  shows "x∈A"
proof -
  from A1 A5 have "x ∈ r``{x}"
    using equiv_class_self by simp;
  with A1 A3 A4 A5 have "x ∈ r``(A)"
    using equiv_class_eq equiv_class_self
    by auto;
  with A1 A2 show "x∈A"
    using EquivClass_3_L1 by simp;
qed;

text{*If $A\subseteq X$ and $A$ is saturated and $x\sim y$, then $x\in A$ iff
  $y\in A$.*}

lemma EquivClass_3_L5: assumes A1: "equiv(X,r)"
  and A2: "IsSaturated(r,A)" and A3: "A⊆X"
  and A4: "x∈X"  "y∈X"
  and A5: "⟨x,y⟩ ∈ r"
  shows "x∈A <-> y∈A"
proof
  assume "y∈A" 
  with prems show "x∈A" using EquivClass_3_L4
    by simp;
next assume A6: "x∈A"
  from A1 A5 have "⟨y,x⟩ ∈ r"
    using equiv_is_sym by blast;
  with A1 A2 A3 A4 A6 show "y∈A"
    using EquivClass_3_L4 by simp;
qed;
  
text{*If $A$ is saturated then $x\in A$ iff its class is in the projection 
  of $A$.*}

lemma EquivClass_3_L6: assumes A1: "equiv(X,r)"
  and A2: "IsSaturated(r,A)" and A3: "A⊆X" and A4: "x∈X"
  and A5: "B = {r``{x}. x∈A}"
  shows "x∈A <-> r``{x} ∈ B"
proof
  assume "x∈A"
  with A5 show "r``{x} ∈ B" by auto;
next assume "r``{x} ∈ B"
  with A5 obtain y where I: "y ∈ A" and "r``{x} = r``{y}"
    by auto;
  with A1 A3 have "⟨x,y⟩ ∈ r"
    using eq_equiv_class by auto;
  with A1 A2 A3 A4 I show "x∈A"
    using EquivClass_3_L4 by simp;
qed;

text{*A technical lemma involving a projection of a saturated set and a 
  logical epression with exclusive or.*}

lemma EquivClass_3_L7: assumes A1: "equiv(X,r)"
  and A2: "IsSaturated(r,A)" and A3: "A⊆X"
  and A4: "x∈X"  "y∈X"
  and A5: "B = {r``{x}. x∈A}"
  and A6: "(x∈A) Xor (y∈A)"
  shows "(r``{x} ∈ B)  Xor (r``{y} ∈ B)"
  using prems EquivClass_3_L6 by simp;

  
(*text{*The next lemma shows that if a set 
  $A$ is such that $a\in A$ and $a\sim b$ implies $b\in A$, then equivalent
  elements either both belong or both don't belog to that set.*}

lemma EquivClass_1_L11: assumes A1: "equiv(X,r)"
  and A2: "∀x∈A. ∀y∈X. ⟨x,y⟩ ∈ r --> y∈A" 
  and A3: "a∈X"  "b∈X"  and A4: "⟨a,b⟩ ∈ r"
  shows "a∈A <-> b∈A"
proof
  assume "a∈A"
  with A2 A3 A4 show "b∈A" by blast;
next assume A5: "b∈A"
  from A1 have "sym(r)" using equiv_def by simp;
  then have "∀x y. <x,y> ∈ r --> <y,x> ∈ r"
    by (unfold sym_def);
  with A4 have "⟨b,a⟩ ∈ r" by blast;
  with A2 A3 A5 show "a∈A" by blast;
qed;*)

    
end