src/HOL/AxClasses/Lattice/Order.thy
author wenzelm
Tue, 30 May 2000 16:08:38 +0200
changeset 9000 c20d58286a51
parent 2606 27cdd600a3b1
permissions -rw-r--r--
cleaned up;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     1
(*  Title:      Order.thy
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     4
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     5
Basic theory of orders (quasi orders, partial orders, linear orders)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     6
and limits (inf, sup, min, max).
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     7
*)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     8
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
     9
Order = HOL + Set +
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    10
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    11
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    12
(** class definitions **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    13
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    14
(* syntax for orders *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    15
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    16
axclass
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    17
  le < term
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    18
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    19
consts
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    20
  "[="          :: "['a::le, 'a] => bool"             (infixl 50)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    21
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    22
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    23
(* quasi orders *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    24
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    25
axclass
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    26
  quasi_order < le
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    27
  le_refl       "x [= x"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    28
  le_trans      "x [= y & y [= z --> x [= z"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    29
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    30
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    31
(* partial orders *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    32
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    33
axclass
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    34
  partial_order < quasi_order
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    35
  le_antisym    "x [= y & y [= x --> x = y"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    36
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    37
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    38
(* linear orders *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    39
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    40
axclass
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    41
  linear_order < partial_order
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    42
  le_linear     "x [= y | y [= x"
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    43
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    44
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    45
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    46
(** limits **)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    47
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    48
(* infima and suprema (on orders) *)
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    49
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    50
consts
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    51
  (*binary*)
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    52
  is_inf        :: "['a::partial_order, 'a, 'a] => bool"
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    53
  is_sup        :: "['a::partial_order, 'a, 'a] => bool"
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    54
  (*general*)
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    55
  is_Inf        :: "['a::partial_order set, 'a] => bool"
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    56
  is_Sup        :: "['a::partial_order set, 'a] => bool"
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    57
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    58
defs
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    59
  is_inf_def    "is_inf x y inf ==
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    60
                   inf [= x & inf [= y &
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    61
                   (ALL lb. lb [= x & lb [= y --> lb [= inf)"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    62
  is_sup_def    "is_sup x y sup ==
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    63
                   x [= sup & y [= sup &
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    64
                   (ALL ub. x [= ub & y [= ub --> sup [= ub)"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    65
  is_Inf_def    "is_Inf A inf ==
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    66
                   (ALL x:A. inf [= x) &
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    67
                   (ALL lb. (ALL x:A. lb [= x) --> lb [= inf)"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    68
  is_Sup_def    "is_Sup A sup ==
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    69
                   (ALL x:A. x [= sup) &
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    70
                   (ALL ub. (ALL x:A. x [= ub) --> sup [= ub)"
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    71
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    72
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    73
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    74
(* binary minima and maxima (on linear_orders) *)
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    75
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    76
constdefs
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    77
  minimum      :: "['a::linear_order, 'a] => 'a"
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    78
  "minimum x y == (if x [= y then x else y)"
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    79
2606
27cdd600a3b1 tuned names: partial order, linear order;
wenzelm
parents: 1573
diff changeset
    80
  maximum      :: "['a::linear_order, 'a] => 'a"
1573
6d66b59f94a9 added constdefs section
clasohm
parents: 1440
diff changeset
    81
  "maximum x y == (if x [= y then y else x)"
1440
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    82
de6f18da81bb added this stuff;
wenzelm
parents:
diff changeset
    83
end