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;
```
(*  Title:      Order.thy
ID:         \$Id\$
Author:     Markus Wenzel, TU Muenchen

Basic theory of orders (quasi orders, partial orders, linear orders)
and limits (inf, sup, min, max).
*)

Order = HOL + Set +

(** class definitions **)

(* syntax for orders *)

axclass
le < term

consts
"[="          :: "['a::le, 'a] => bool"             (infixl 50)

(* quasi orders *)

axclass
quasi_order < le
le_refl       "x [= x"
le_trans      "x [= y & y [= z --> x [= z"

(* partial orders *)

axclass
partial_order < quasi_order
le_antisym    "x [= y & y [= x --> x = y"

(* linear orders *)

axclass
linear_order < partial_order
le_linear     "x [= y | y [= x"

(** limits **)

(* infima and suprema (on orders) *)

consts
(*binary*)
is_inf        :: "['a::partial_order, 'a, 'a] => bool"
is_sup        :: "['a::partial_order, 'a, 'a] => bool"
(*general*)
is_Inf        :: "['a::partial_order set, 'a] => bool"
is_Sup        :: "['a::partial_order set, 'a] => bool"

defs
is_inf_def    "is_inf x y inf ==
inf [= x & inf [= y &
(ALL lb. lb [= x & lb [= y --> lb [= inf)"
is_sup_def    "is_sup x y sup ==
x [= sup & y [= sup &
(ALL ub. x [= ub & y [= ub --> sup [= ub)"
is_Inf_def    "is_Inf A inf ==
(ALL x:A. inf [= x) &
(ALL lb. (ALL x:A. lb [= x) --> lb [= inf)"
is_Sup_def    "is_Sup A sup ==
(ALL x:A. x [= sup) &
(ALL ub. (ALL x:A. x [= ub) --> sup [= ub)"

(* binary minima and maxima (on linear_orders) *)

constdefs
minimum      :: "['a::linear_order, 'a] => 'a"
"minimum x y == (if x [= y then x else y)"

maximum      :: "['a::linear_order, 'a] => 'a"
"maximum x y == (if x [= y then y else x)"

end
```