src/HOL/Ord.thy
author wenzelm
Fri, 14 Feb 1997 15:32:00 +0100
changeset 2624 ab311b6e5e29
parent 2608 450c9b682a92
child 3143 d60e49b86c6a
permissions -rw-r--r--
fixed comment;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/Ord.thy
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
2624
ab311b6e5e29 fixed comment;
wenzelm
parents: 2608
diff changeset
     6
Type classes for order signatures and orders.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     8
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
Ord = HOL +
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
axclass
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
  ord < term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
consts
2259
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    15
  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    16
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
1370
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 965
diff changeset
    17
  mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
7361ac9b024d removed quotes from types in consts and syntax sections
clasohm
parents: 965
diff changeset
    18
  min, max      :: ['a::ord, 'a] => 'a
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    20
  Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    21
2259
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    22
syntax
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    23
  "op <"        :: ['a::ord, 'a] => bool             ("op <")
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    24
  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    25
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    26
syntax (symbols)
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    27
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    28
  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    29
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
defs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
  mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
965
24eef3860714 changed syntax of "if"
clasohm
parents: 923
diff changeset
    32
  min_def       "min a b == (if a <= b then a else b)"
24eef3860714 changed syntax of "if"
clasohm
parents: 923
diff changeset
    33
  max_def       "max a b == (if a <= b then b else a)"
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    34
  Least_def     "Least P == @x. P(x) & (ALL y. y<x --> ~P(y))"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    35
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    36
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    37
axclass order < ord
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    38
  order_refl    "x <= x"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    39
  order_trans   "[| x <= y; y <= z |] ==> x <= z"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    40
  order_antisym "[| x <= y; y <= x |] ==> x = y"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    41
  order_less_le "x < y = (x <= y & x ~= y)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
end