src/HOL/ex/PER.thy

--- a/src/HOL/ex/PER.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/ex/PER.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -8,39 +8,40 @@
 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:
+  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.
+  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
@@ -64,9 +65,9 @@
 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)
@@ -81,8 +82,8 @@
   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
@@ -113,18 +114,18 @@
 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"
@@ -145,8 +146,8 @@
 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}"
@@ -159,8 +160,8 @@
   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
@@ -183,8 +184,8 @@
 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>"