src/HOL/ex/PER.thy

 header {* Partial equivalence relations *}
 
 theory PER = Main:
 
 text {*
- Higher-order quotients are defined over partial equivalence relations
- (PERs) instead of total ones.  We provide axiomatic type classes
- @{text "equiv < partial_equiv"} and a type constructor
- @{text "'a quot"} with basic operations.  This development is based
- on:
-
- Oscar Slotosch: \emph{Higher Order Quotients and their Implementation
- in Isabelle HOL.}  Elsa L. Gunter and Amy Felty, editors, Theorem
- Proving in Higher Order Logics: TPHOLs '97, Springer LNCS 1275, 1997.
+  Higher-order quotients are defined over partial equivalence
+  relations (PERs) instead of total ones.  We provide axiomatic type
+  classes @{text "equiv < partial_equiv"} and a type constructor
+  @{text "'a quot"} with basic operations.  This development is based
+  on:
+
+  Oscar Slotosch: \emph{Higher Order Quotients and their
+  Implementation in Isabelle HOL.}  Elsa L. Gunter and Amy Felty,
+  editors, Theorem Proving in Higher Order Logics: TPHOLs '97,
+  Springer LNCS 1275, 1997.
 *}
 
 
 subsection {* Partial equivalence *}
 
 text {*
- Type class @{text partial_equiv} models partial equivalence relations
- (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,
- which is required to be symmetric and transitive, but not necessarily
- reflexive.
+  Type class @{text partial_equiv} models partial equivalence
+  relations (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a =>
+  bool"} relation, which is required to be symmetric and transitive,
+  but not necessarily reflexive.
 *}
 
 consts
   eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
 
-axclass partial_equiv < "term"
+axclass partial_equiv < type
   partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
   partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
 
 text {*
- \medskip The domain of a partial equivalence relation is the set of
- reflexive elements.  Due to symmetry and transitivity this
- characterizes exactly those elements that are connected with
- \emph{any} other one.
+  \medskip The domain of a partial equivalence relation is the set of
+  reflexive elements.  Due to symmetry and transitivity this
+  characterizes exactly those elements that are connected with
+  \emph{any} other one.
 *}
 
 constdefs
   domain :: "'a::partial_equiv set"
   "domain == {x. x \<sim> x}"

 
 
 subsection {* Equivalence on function spaces *}
 
 text {*
- The @{text \<sim>} relation is lifted to function spaces.  It is
- important to note that this is \emph{not} the direct product, but a
- structural one corresponding to the congruence property.
+  The @{text \<sim>} relation is lifted to function spaces.  It is
+  important to note that this is \emph{not} the direct product, but a
+  structural one corresponding to the congruence property.
 *}
 
 defs (overloaded)
   eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
 

 lemma partial_equiv_funD [dest?]:
     "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"
   by (unfold eqv_fun_def) blast
 
 text {*
- The class of partial equivalence relations is closed under function
- spaces (in \emph{both} argument positions).
+  The class of partial equivalence relations is closed under function
+  spaces (in \emph{both} argument positions).
 *}
 
 instance fun :: (partial_equiv, partial_equiv) partial_equiv
 proof
   fix f g h :: "'a::partial_equiv => 'b::partial_equiv"

 
 
 subsection {* Total equivalence *}
 
 text {*
- The class of total equivalence relations on top of PERs.  It
- coincides with the standard notion of equivalence, i.e.\
- @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive
- and symmetric.
+  The class of total equivalence relations on top of PERs.  It
+  coincides with the standard notion of equivalence, i.e.\ @{text "\<sim>
+  :: 'a => 'a => bool"} is required to be reflexive, transitive and
+  symmetric.
 *}
 
 axclass equiv < partial_equiv
   eqv_refl [intro]: "x \<sim> x"
 
 text {*
- On total equivalences all elements are reflexive, and congruence
- holds unconditionally.
+  On total equivalences all elements are reflexive, and congruence
+  holds unconditionally.
 *}
 
 theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"
 proof
   show "x \<sim> x" ..

 
 
 subsection {* Quotient types *}
 
 text {*
- The quotient type @{text "'a quot"} consists of all \emph{equivalence
- classes} over elements of the base type @{typ 'a}.
+  The quotient type @{text "'a quot"} consists of all
+  \emph{equivalence classes} over elements of the base type @{typ 'a}.
 *}
 
 typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
   by blast
 

 
 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
   by (unfold quot_def) blast
 
 text {*
- \medskip Abstracted equivalence classes are the canonical
- representation of elements of a quotient type.
+  \medskip Abstracted equivalence classes are the canonical
+  representation of elements of a quotient type.
 *}
 
 constdefs
   eqv_class :: "('a::partial_equiv) => 'a quot"    ("\<lfloor>_\<rfloor>")
   "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"

 
 
 subsection {* Equality on quotients *}
 
 text {*
- Equality of canonical quotient elements corresponds to the original
- relation as follows.
+  Equality of canonical quotient elements corresponds to the original
+  relation as follows.
 *}
 
 theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
 proof -
   assume ab: "a \<sim> b"