|
2904
|
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 *)
|
|
3058
|
19 |
ax_per_trans "[|eqv x y; eqv y z|] ==> eqv x z"
|
|
2904
|
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"
|
|
3842
|
30 |
Dom "D=={x. x===x}"
|
|
2904
|
31 |
(* define ==== on and function type => *)
|
|
3842
|
32 |
fun_per_def "eqv f g == !x y. x:D & y:D & x===y --> f x === g y"
|
|
2904
|
33 |
|
|
|
34 |
syntax (symbols)
|
|
|
35 |
"op ===" :: "['a,'a::per] => bool" (infixl "\\<sim>" 50)
|
|
|
36 |
|
|
|
37 |
end
|