src/HOL/Quot/PER0.thy

(partial) equivalecne relations. classes er<per

(*  Title:      HOL/Quot/PER0.thy
    ID:         $Id$
    Author:     Oscar Slotosch
    Copyright   1997 Technische Universitaet Muenchen

Definition of classes per and er for (partial) equivalence classes
The polymorphic constant eqv is only for the definition of PERs
The characteristic constant === (sim) is available on the class per

*)

PER0 = Set + (* partial equivalence relations *)

consts  (* polymorphic constant for (partial) equivalence relations *)
        eqv    :: "'a::term => 'a => bool" 

axclass per < term
	(* axioms for partial equivalence relations *)
        ax_per_sym      "eqv x y ==> eqv y x"
        ax_per_trans    "[|eqv x y; eqv y z|] ==> eqv x z"

axclass er < per
	ax_er_refl	"eqv x x"

consts  (* characteristic constant and Domain for per *)
        "==="     :: "'a::per => 'a => bool" (infixl 55)
        D         :: "'a::per set"
defs
        per_def         "(op ===) == eqv"
        Domain          "D=={x.x===x}"
(* define ==== on and function type => *)
        fun_per_def     "eqv f g == !x y.x:D & y:D & x===y --> f x === g y"

syntax (symbols)
  "op ==="   :: "['a,'a::per] => bool"        (infixl "\\<sim>" 50)

end