src/HOL/AxClasses/Lattice/Order.thy

Goal: tuned pris;

(*  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