src/HOL/Ord.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2259 e6d738f2b9a9
child 2608 450c9b682a92
permissions -rw-r--r--
added AxClasses test;
     1 (*  Title:      HOL/Ord.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Type class for order signatures.
     7 *)
     8 
     9 Ord = HOL +
    10 
    11 axclass
    12   ord < term
    13 
    14 consts
    15   "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
    16   "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
    17   mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
    18   min, max      :: ['a::ord, 'a] => 'a
    19 
    20 syntax
    21   "op <"        :: ['a::ord, 'a] => bool             ("op <")
    22   "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    23 
    24 syntax (symbols)
    25   "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
    26   "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
    27 
    28 defs
    29   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
    30   min_def       "min a b == (if a <= b then a else b)"
    31   max_def       "max a b == (if a <= b then b else a)"
    32 
    33 end