src/HOL/Quot/PER0.thy
author wenzelm
Fri Oct 10 19:02:28 1997 +0200 (1997-10-10)
changeset 3842 b55686a7b22c
parent 3058 9d6526cacc3c
permissions -rw-r--r--
fixed dots;
     1 (*  Title:      HOL/Quot/PER0.thy
     2     ID:         $Id$
     3     Author:     Oscar Slotosch
     4     Copyright   1997 Technische Universitaet Muenchen
     5 
     6 Definition of classes per and er for (partial) equivalence classes
     7 The polymorphic constant eqv is only for the definition of PERs
     8 The characteristic constant === (sim) is available on the class per
     9 
    10 *)
    11 
    12 PER0 = Set + (* partial equivalence relations *)
    13 
    14 consts  (* polymorphic constant for (partial) equivalence relations *)
    15         eqv    :: "'a::term => 'a => bool" 
    16 
    17 axclass per < term
    18 	(* axioms for partial equivalence relations *)
    19         ax_per_trans    "[|eqv x y; eqv y z|] ==> eqv x z"
    20         ax_per_sym      "eqv x y ==> eqv y x"
    21 
    22 axclass er < per
    23 	ax_er_refl	"eqv x x"
    24 
    25 consts  (* characteristic constant and Domain for per *)
    26         "==="     :: "'a::per => 'a => bool" (infixl 55)
    27         D         :: "'a::per set"
    28 defs
    29         per_def         "(op ===) == eqv"
    30         Dom             "D=={x. x===x}"
    31 (* define ==== on and function type => *)
    32         fun_per_def     "eqv f g == !x y. x:D & y:D & x===y --> f x === g y"
    33 
    34 syntax (symbols)
    35   "op ==="   :: "['a,'a::per] => bool"        (infixl "\\<sim>" 50)
    36 
    37 end