src/HOLCF/porder0.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 298 3a0485439396
permissions -rw-r--r--
made tutorial first;
nipkow@298
     1
(*  Title: 	HOLCF/porder0.thy
nipkow@298
     2
    ID:         $Id$
nipkow@298
     3
    Author: 	Franz Regensburger
nipkow@298
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@298
     5
nipkow@298
     6
Definition of class porder (partial order)
nipkow@298
     7
nipkow@298
     8
The prototype theory for this class is void.thy 
nipkow@298
     9
nipkow@298
    10
*)
nipkow@298
    11
nipkow@298
    12
Porder0 = Void +
nipkow@298
    13
nipkow@298
    14
(* Introduction of new class. The witness is type void. *)
nipkow@298
    15
nipkow@298
    16
classes po < term
nipkow@298
    17
nipkow@298
    18
(* default type is still term ! *)
nipkow@298
    19
(* void is the prototype in po *)
nipkow@298
    20
nipkow@298
    21
arities void :: po
nipkow@298
    22
nipkow@298
    23
consts	"<<"	::	"['a,'a::po] => bool"	(infixl 55)
nipkow@298
    24
nipkow@298
    25
rules
nipkow@298
    26
nipkow@298
    27
(* class axioms: justification is theory Void *)
nipkow@298
    28
nipkow@298
    29
refl_less	"x << x"	
nipkow@298
    30
				(* witness refl_less_void    *)
nipkow@298
    31
nipkow@298
    32
antisym_less	"[|x<<y ; y<<x |] ==> x = y"	
nipkow@298
    33
				(* witness antisym_less_void *)
nipkow@298
    34
nipkow@298
    35
trans_less	"[|x<<y ; y<<z |] ==> x<<z"
nipkow@298
    36
				(* witness trans_less_void   *)
nipkow@298
    37
nipkow@298
    38
(* instance of << for the prototype void *)
nipkow@298
    39
nipkow@298
    40
inst_void_po	"(op <<)::[void,void]=>bool = less_void"
nipkow@298
    41
nipkow@298
    42
end