src/HOLCF/Porder0.thy
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 7661 8c3190b173aa
child 12114 a8e860c86252
permissions -rw-r--r--
GPLed;
slotosch@2640
     1
(*  Title:      HOLCF/Porder0.thy
nipkow@298
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@298
     5
wenzelm@12030
     6
Definition of class porder (partial order).
nipkow@298
     7
*)
nipkow@298
     8
wenzelm@7661
     9
Porder0 = Main +
nipkow@298
    10
slotosch@3323
    11
	(* introduce a (syntactic) class for the constant << *)
slotosch@3323
    12
axclass sq_ord<term
nipkow@298
    13
slotosch@3323
    14
	(* characteristic constant << for po *)
oheimb@2394
    15
consts
slotosch@3323
    16
  "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)
oheimb@2394
    17
oheimb@2394
    18
syntax (symbols)
slotosch@3323
    19
  "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\\<sqsubseteq>" 55)
nipkow@298
    20
slotosch@3323
    21
axclass po < sq_ord
slotosch@3323
    22
        (* class axioms: *)
slotosch@3323
    23
refl_less       "x << x"        
slotosch@3323
    24
antisym_less    "[|x << y; y << x |] ==> x = y"    
slotosch@3323
    25
trans_less      "[|x << y; y << z |] ==> x << z"
slotosch@3323
    26
 
nipkow@298
    27
end 
regensbu@1274
    28
regensbu@1274
    29