src/HOL/Ord.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5953 d6017ce6b93e
child 6402 2b23e14dd386
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     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 classes for order signatures and orders.
     7 *)
     8 
     9 Ord = HOL +
    10 
    11 (*FIXME move to HOL.thy*)
    12 setup attrib_setup
    13 setup Classical.setup
    14 setup Blast.setup
    15 setup Clasimp.setup
    16 
    17 
    18 axclass
    19   ord < term
    20 
    21 global
    22 
    23 syntax
    24   "op <"        :: ['a::ord, 'a] => bool             ("op <")
    25   "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    26 
    27 consts
    28   "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
    29   "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
    30   mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
    31   min, max      :: ['a::ord, 'a] => 'a
    32 
    33   Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
    34 
    35 syntax (symbols)
    36   "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
    37   "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
    38 
    39 
    40 local
    41 
    42 defs
    43   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
    44   min_def       "min a b == (if a <= b then a else b)"
    45   max_def       "max a b == (if a <= b then b else a)"
    46   Least_def     "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
    47 
    48 
    49 axclass order < ord
    50   order_refl    "x <= x"
    51   order_trans   "[| x <= y; y <= z |] ==> x <= z"
    52   order_antisym "[| x <= y; y <= x |] ==> x = y"
    53   order_less_le "x < y = (x <= y & x ~= y)"
    54 
    55 axclass linorder < order
    56   linorder_linear "x <= y | y <= x"
    57 
    58 end