src/HOL/Ord.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10460 a8d9a79ed95e
child 11140 a46eaedbeb2d
permissions -rw-r--r--
improved theory reference in comment
     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 
    12 axclass
    13   ord < term
    14 
    15 syntax
    16   "op <"        :: ['a::ord, 'a] => bool             ("op <")
    17   "op <="       :: ['a::ord, 'a] => bool             ("op <=")
    18 
    19 global
    20 
    21 consts
    22   "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
    23   "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
    24 
    25 local
    26 
    27 syntax (symbols)
    28   "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
    29   "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
    30 
    31 consts
    32   mono          :: ['a::ord => 'b::ord] => bool      (*monotonicity*)
    33   min, max      :: ['a::ord, 'a] => 'a
    34   Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
    35 
    36 defs
    37   mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
    38   min_def       "min a b == (if a <= b then a else b)"
    39   max_def       "max a b == (if a <= b then b else a)"
    40   Least_def     "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
    41 
    42 
    43 axclass order < ord
    44   order_refl    "x <= x"
    45   order_trans   "[| x <= y; y <= z |] ==> x <= z"
    46   order_antisym "[| x <= y; y <= x |] ==> x = y"
    47   order_less_le "x < y = (x <= y & x ~= y)"
    48 
    49 axclass linorder < order
    50   linorder_linear "x <= y | y <= x"
    51 
    52 
    53 (* bounded quantifiers *)
    54 
    55 syntax
    56   "_lessAll" :: [idt, 'a, bool] => bool   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
    57   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3EX _<_./ _)"  [0, 0, 10] 10)
    58   "_leAll"   :: [idt, 'a, bool] => bool   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
    59   "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
    60 
    61 syntax (symbols)
    62   "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
    63   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
    64   "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
    65   "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
    66 
    67 syntax (HOL)
    68   "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
    69   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
    70   "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
    71   "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
    72 
    73 translations
    74  "ALL x<y. P"   =>  "ALL x. x < y --> P"
    75  "EX x<y. P"    =>  "EX x. x < y  & P"
    76  "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
    77  "EX x<=y. P"   =>  "EX x. x <= y & P"
    78 
    79 
    80 end