equal
deleted
inserted
replaced
|
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_sym "eqv x y ==> eqv y x" |
|
20 ax_per_trans "[|eqv x y; eqv y z|] ==> eqv x z" |
|
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 Domain "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 |