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
clasohm@923
     1
(*  Title:      HOL/Ord.thy
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
wenzelm@2624
     6
Type classes for order signatures and orders.
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
Ord = HOL +
clasohm@923
    10
wenzelm@5889
    11
clasohm@923
    12
axclass
clasohm@923
    13
  ord < term
clasohm@923
    14
wenzelm@3820
    15
syntax
wenzelm@3820
    16
  "op <"        :: ['a::ord, 'a] => bool             ("op <")
wenzelm@3820
    17
  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
wenzelm@3820
    18
wenzelm@8882
    19
global
wenzelm@8882
    20
clasohm@923
    21
consts
wenzelm@2259
    22
  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
wenzelm@2259
    23
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
clasohm@923
    24
wenzelm@8882
    25
local
nipkow@2608
    26
wenzelm@3820
    27
syntax (symbols)
wenzelm@3820
    28
  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
wenzelm@3820
    29
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
wenzelm@2259
    30
wenzelm@8882
    31
consts
wenzelm@8882
    32
  mono          :: ['a::ord => 'b::ord] => bool      (*monotonicity*)
wenzelm@8882
    33
  min, max      :: ['a::ord, 'a] => 'a
wenzelm@8882
    34
  Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
wenzelm@3947
    35
clasohm@923
    36
defs
clasohm@923
    37
  mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
clasohm@965
    38
  min_def       "min a b == (if a <= b then a else b)"
clasohm@965
    39
  max_def       "max a b == (if a <= b then b else a)"
nipkow@3143
    40
  Least_def     "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
nipkow@2608
    41
nipkow@2608
    42
nipkow@2608
    43
axclass order < ord
nipkow@2608
    44
  order_refl    "x <= x"
nipkow@2608
    45
  order_trans   "[| x <= y; y <= z |] ==> x <= z"
nipkow@2608
    46
  order_antisym "[| x <= y; y <= x |] ==> x = y"
nipkow@2608
    47
  order_less_le "x < y = (x <= y & x ~= y)"
clasohm@923
    48
nipkow@4640
    49
axclass linorder < order
nipkow@4640
    50
  linorder_linear "x <= y | y <= x"
nipkow@4640
    51
wenzelm@7238
    52
wenzelm@7238
    53
(* bounded quantifiers *)
wenzelm@7238
    54
nipkow@6402
    55
syntax
wenzelm@7238
    56
  "_lessAll" :: [idt, 'a, bool] => bool   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
wenzelm@7238
    57
  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3EX _<_./ _)"  [0, 0, 10] 10)
wenzelm@7238
    58
  "_leAll"   :: [idt, 'a, bool] => bool   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
wenzelm@7238
    59
  "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
wenzelm@7238
    60
wenzelm@7238
    61
syntax (symbols)
wenzelm@7238
    62
  "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
wenzelm@7238
    63
  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
nipkow@10227
    64
  "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
nipkow@10227
    65
  "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
wenzelm@7238
    66
wenzelm@7238
    67
syntax (HOL)
wenzelm@7238
    68
  "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
wenzelm@7238
    69
  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
wenzelm@7238
    70
  "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
wenzelm@7238
    71
  "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
wenzelm@7238
    72
nipkow@6402
    73
translations
wenzelm@7238
    74
 "ALL x<y. P"   =>  "ALL x. x < y --> P"
wenzelm@7238
    75
 "EX x<y. P"    =>  "EX x. x < y  & P"
wenzelm@7238
    76
 "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
wenzelm@7238
    77
 "EX x<=y. P"   =>  "EX x. x <= y & P"
wenzelm@7238
    78
nipkow@6402
    79
clasohm@923
    80
end