src/HOL/Ord.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2624 ab311b6e5e29
child 3143 d60e49b86c6a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     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 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   Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
    21 
    22 syntax
    23   "op <"        :: ['a::ord, 'a] => bool             ("op <")
    24   "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    25 
    26 syntax (symbols)
    27   "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
    28   "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
    29 
    30 defs
    31   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
    32   min_def       "min a b == (if a <= b then a else b)"
    33   max_def       "max a b == (if a <= b then b else a)"
    34   Least_def     "Least P == @x. P(x) & (ALL y. y<x --> ~P(y))"
    35 
    36 
    37 axclass order < ord
    38   order_refl    "x <= x"
    39   order_trans   "[| x <= y; y <= z |] ==> x <= z"
    40   order_antisym "[| x <= y; y <= x |] ==> x = y"
    41   order_less_le "x < y = (x <= y & x ~= y)"
    42 
    43 end