src/HOL/Ord.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10460 a8d9a79ed95e
child 11140 a46eaedbeb2d
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
5889
d3ecef6b5682 Classical.setup, attrib_setup;
wenzelm
parents: 4640
diff changeset
    11
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
axclass
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    13
  ord < term
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3143
diff changeset
    15
syntax
46b255e140dc fixed infix syntax;
wenzelm
parents: 3143
diff changeset
    16
  "op <"        :: ['a::ord, 'a] => bool             ("op <")
46b255e140dc fixed infix syntax;
wenzelm
parents: 3143
diff changeset
    17
  "op <="       :: ['a::ord, 'a] => bool             ("op <=")
46b255e140dc fixed infix syntax;
wenzelm
parents: 3143
diff changeset
    18
8882
9df44a4f1bf7 fewer consts declared as global;
wenzelm
parents: 7357
diff changeset
    19
global
9df44a4f1bf7 fewer consts declared as global;
wenzelm
parents: 7357
diff changeset
    20
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
consts
2259
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    22
  "op <"        :: ['a::ord, 'a] => bool             ("(_/ < _)"  [50, 51] 50)
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    23
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ <= _)" [50, 51] 50)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
8882
9df44a4f1bf7 fewer consts declared as global;
wenzelm
parents: 7357
diff changeset
    25
local
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    26
3820
46b255e140dc fixed infix syntax;
wenzelm
parents: 3143
diff changeset
    27
syntax (symbols)
46b255e140dc fixed infix syntax;
wenzelm
parents: 3143
diff changeset
    28
  "op <="       :: ['a::ord, 'a] => bool             ("op \\<le>")
46b255e140dc fixed infix syntax;
wenzelm
parents: 3143
diff changeset
    29
  "op <="       :: ['a::ord, 'a] => bool             ("(_/ \\<le> _)"  [50, 51] 50)
2259
e6d738f2b9a9 fixed comment;
wenzelm
parents: 2006
diff changeset
    30
8882
9df44a4f1bf7 fewer consts declared as global;
wenzelm
parents: 7357
diff changeset
    31
consts
9df44a4f1bf7 fewer consts declared as global;
wenzelm
parents: 7357
diff changeset
    32
  mono          :: ['a::ord => 'b::ord] => bool      (*monotonicity*)
9df44a4f1bf7 fewer consts declared as global;
wenzelm
parents: 7357
diff changeset
    33
  min, max      :: ['a::ord, 'a] => 'a
9df44a4f1bf7 fewer consts declared as global;
wenzelm
parents: 7357
diff changeset
    34
  Least         :: ('a::ord=>bool) => 'a             (binder "LEAST " 10)
3947
eb707467f8c5 adapted to qualified names;
wenzelm
parents: 3820
diff changeset
    35
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    36
defs
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    37
  mono_def      "mono(f) == (!A B. A <= B --> f(A) <= f(B))"
965
24eef3860714 changed syntax of "if"
clasohm
parents: 923
diff changeset
    38
  min_def       "min a b == (if a <= b then a else b)"
24eef3860714 changed syntax of "if"
clasohm
parents: 923
diff changeset
    39
  max_def       "max a b == (if a <= b then b else a)"
3143
d60e49b86c6a Modified def of Least, which, as Markus correctly complained, looked like
nipkow
parents: 2624
diff changeset
    40
  Least_def     "Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
2608
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    41
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    42
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    43
axclass order < ord
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    44
  order_refl    "x <= x"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    45
  order_trans   "[| x <= y; y <= z |] ==> x <= z"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    46
  order_antisym "[| x <= y; y <= x |] ==> x = y"
450c9b682a92 New class "order" and accompanying changes.
nipkow
parents: 2259
diff changeset
    47
  order_less_le "x < y = (x <= y & x ~= y)"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
4640
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 3947
diff changeset
    49
axclass linorder < order
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 3947
diff changeset
    50
  linorder_linear "x <= y | y <= x"
ac6cf9f18653 Congruence rules use == in premises now.
nipkow
parents: 3947
diff changeset
    51
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    52
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    53
(* bounded quantifiers *)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    54
6402
2b23e14dd386 New bounded quantifier syntax: !x<i. P etc
nipkow
parents: 5953
diff changeset
    55
syntax
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    56
  "_lessAll" :: [idt, 'a, bool] => bool   ("(3ALL _<_./ _)"  [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    57
  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3EX _<_./ _)"  [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    58
  "_leAll"   :: [idt, 'a, bool] => bool   ("(3ALL _<=_./ _)" [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    59
  "_leEx"    :: [idt, 'a, bool] => bool   ("(3EX _<=_./ _)" [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    60
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    61
syntax (symbols)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    62
  "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    63
  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
10227
692e29b9d2b2 <= -> \<le>
nipkow
parents: 8882
diff changeset
    64
  "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
692e29b9d2b2 <= -> \<le>
nipkow
parents: 8882
diff changeset
    65
  "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    66
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    67
syntax (HOL)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    68
  "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    69
  "_lessEx"  :: [idt, 'a, bool] => bool   ("(3? _<_./ _)"  [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    70
  "_leAll"   :: [idt, 'a, bool] => bool   ("(3! _<=_./ _)" [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    71
  "_leEx"    :: [idt, 'a, bool] => bool   ("(3? _<=_./ _)" [0, 0, 10] 10)
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    72
6402
2b23e14dd386 New bounded quantifier syntax: !x<i. P etc
nipkow
parents: 5953
diff changeset
    73
translations
7238
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    74
 "ALL x<y. P"   =>  "ALL x. x < y --> P"
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    75
 "EX x<y. P"    =>  "EX x. x < y  & P"
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    76
 "ALL x<=y. P"  =>  "ALL x. x <= y --> P"
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    77
 "EX x<=y. P"   =>  "EX x. x <= y & P"
36e58620ffc8 replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents: 6855
diff changeset
    78
6402
2b23e14dd386 New bounded quantifier syntax: !x<i. P etc
nipkow
parents: 5953
diff changeset
    79
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
end