author | clasohm |
Tue, 07 Feb 1995 11:59:32 +0100 | |
changeset 892 | d0dc8d057929 |
parent 442 | 13ac1fd0a14d |
child 1274 | ea0668a1c0ba |
permissions | -rw-r--r-- |
298 | 1 |
(* Title: HOLCF/porder0.thy |
2 |
ID: $Id$ |
|
3 |
Author: Franz Regensburger |
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
|
5 |
||
6 |
Definition of class porder (partial order) |
|
7 |
||
8 |
The prototype theory for this class is void.thy |
|
9 |
||
10 |
*) |
|
11 |
||
12 |
Porder0 = Void + |
|
13 |
||
14 |
(* Introduction of new class. The witness is type void. *) |
|
15 |
||
16 |
classes po < term |
|
17 |
||
18 |
(* default type is still term ! *) |
|
19 |
(* void is the prototype in po *) |
|
20 |
||
21 |
arities void :: po |
|
22 |
||
23 |
consts "<<" :: "['a,'a::po] => bool" (infixl 55) |
|
24 |
||
25 |
rules |
|
26 |
||
27 |
(* class axioms: justification is theory Void *) |
|
28 |
||
29 |
refl_less "x << x" |
|
30 |
(* witness refl_less_void *) |
|
31 |
||
32 |
antisym_less "[|x<<y ; y<<x |] ==> x = y" |
|
33 |
(* witness antisym_less_void *) |
|
34 |
||
35 |
trans_less "[|x<<y ; y<<z |] ==> x<<z" |
|
36 |
(* witness trans_less_void *) |
|
37 |
||
38 |
(* instance of << for the prototype void *) |
|
39 |
||
442
13ac1fd0a14d
added parentheses made necessary by change of constrain's precedence
clasohm
parents:
298
diff
changeset
|
40 |
inst_void_po "((op <<)::[void,void]=>bool) = less_void" |
298 | 41 |
|
42 |
end |