src/HOL/Ord.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2259 e6d738f2b9a9
child 2608 450c9b682a92
permissions -rw-r--r--
added AxClasses test;
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@2259
     6
Type class for order signatures.
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
Ord = HOL +
clasohm@923
    10
clasohm@923
    11
axclass
clasohm@923
    12
  ord < term
clasohm@923
    13
clasohm@923
    14
consts
wenzelm@2259
    15
  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
wenzelm@2259
    16
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
clasohm@1370
    17
  mono          :: ['a::ord => 'b::ord] => bool       (*monotonicity*)
clasohm@1370
    18
  min, max      :: ['a::ord, 'a] => 'a
clasohm@923
    19
wenzelm@2259
    20
syntax
wenzelm@2259
    21
  "op <"        :: ['a::ord, 'a] => bool             ("op <")
wenzelm@2259
    22
  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
wenzelm@2259
    23
wenzelm@2259
    24
syntax (symbols)
wenzelm@2259
    25
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
wenzelm@2259
    26
  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
wenzelm@2259
    27
clasohm@923
    28
defs
clasohm@923
    29
  mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
clasohm@965
    30
  min_def       "min a b == (if a <= b then a else b)"
clasohm@965
    31
  max_def       "max a b == (if a <= b then b else a)"
clasohm@923
    32
clasohm@923
    33
end