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