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);
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
(*FIXME move to HOL.thy*)
wenzelm@5953
    12
setup attrib_setup
wenzelm@5889
    13
setup Classical.setup
wenzelm@5953
    14
setup Blast.setup
wenzelm@5953
    15
setup Clasimp.setup
wenzelm@5953
    16
wenzelm@5889
    17
clasohm@923
    18
axclass
clasohm@923
    19
  ord < term
clasohm@923
    20
wenzelm@3947
    21
global
wenzelm@3947
    22
wenzelm@3820
    23
syntax
wenzelm@3820
    24
  "op <"        :: ['a::ord, 'a] => bool             ("op <")
wenzelm@3820
    25
  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
wenzelm@3820
    26
clasohm@923
    27
consts
wenzelm@2259
    28
  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
wenzelm@2259
    29
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
clasohm@1370
    30
  mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
clasohm@1370
    31
  min, max      :: ['a::ord, 'a] => 'a
clasohm@923
    32
nipkow@2608
    33
  Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
nipkow@2608
    34
wenzelm@3820
    35
syntax (symbols)
wenzelm@3820
    36
  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
wenzelm@3820
    37
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
wenzelm@2259
    38
wenzelm@2259
    39
wenzelm@3947
    40
local
wenzelm@3947
    41
clasohm@923
    42
defs
clasohm@923
    43
  mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
clasohm@965
    44
  min_def       "min a b == (if a <= b then a else b)"
clasohm@965
    45
  max_def       "max a b == (if a <= b then b else a)"
nipkow@3143
    46
  Least_def     "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
nipkow@2608
    47
nipkow@2608
    48
nipkow@2608
    49
axclass order < ord
nipkow@2608
    50
  order_refl    "x <= x"
nipkow@2608
    51
  order_trans   "[| x <= y; y <= z |] ==> x <= z"
nipkow@2608
    52
  order_antisym "[| x <= y; y <= x |] ==> x = y"
nipkow@2608
    53
  order_less_le "x < y = (x <= y & x ~= y)"
clasohm@923
    54
nipkow@4640
    55
axclass linorder < order
nipkow@4640
    56
  linorder_linear "x <= y | y <= x"
nipkow@4640
    57
clasohm@923
    58
end