1440
|
1 |
(* Title: Order.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Basic theory of orders (quasi orders, partial orders, linear orders)
|
|
6 |
and limits (inf, sup, min, max).
|
|
7 |
*)
|
|
8 |
|
|
9 |
Order = HOL + Set +
|
|
10 |
|
|
11 |
|
|
12 |
(** class definitions **)
|
|
13 |
|
|
14 |
(* syntax for orders *)
|
|
15 |
|
|
16 |
axclass
|
|
17 |
le < term
|
|
18 |
|
|
19 |
consts
|
|
20 |
"[=" :: "['a::le, 'a] => bool" (infixl 50)
|
|
21 |
|
|
22 |
|
|
23 |
(* quasi orders *)
|
|
24 |
|
|
25 |
axclass
|
|
26 |
quasi_order < le
|
|
27 |
le_refl "x [= x"
|
|
28 |
le_trans "x [= y & y [= z --> x [= z"
|
|
29 |
|
|
30 |
|
|
31 |
(* partial orders *)
|
|
32 |
|
|
33 |
axclass
|
|
34 |
order < quasi_order
|
|
35 |
le_antisym "x [= y & y [= x --> x = y"
|
|
36 |
|
|
37 |
|
|
38 |
(* linear orders *)
|
|
39 |
|
|
40 |
axclass
|
|
41 |
lin_order < order
|
|
42 |
le_lin "x [= y | y [= x"
|
|
43 |
|
|
44 |
|
|
45 |
|
|
46 |
(** limits **)
|
|
47 |
|
|
48 |
(* infima and suprema (on orders) *)
|
|
49 |
|
|
50 |
consts
|
|
51 |
(*binary*)
|
|
52 |
is_inf :: "['a::order, 'a, 'a] => bool"
|
|
53 |
is_sup :: "['a::order, 'a, 'a] => bool"
|
|
54 |
(*general*)
|
|
55 |
is_Inf :: "['a::order set, 'a] => bool"
|
|
56 |
is_Sup :: "['a::order set, 'a] => bool"
|
|
57 |
|
|
58 |
defs
|
|
59 |
is_inf_def "is_inf x y inf ==
|
|
60 |
inf [= x & inf [= y &
|
|
61 |
(ALL lb. lb [= x & lb [= y --> lb [= inf)"
|
|
62 |
is_sup_def "is_sup x y sup ==
|
|
63 |
x [= sup & y [= sup &
|
|
64 |
(ALL ub. x [= ub & y [= ub --> sup [= ub)"
|
|
65 |
is_Inf_def "is_Inf A inf ==
|
|
66 |
(ALL x:A. inf [= x) &
|
|
67 |
(ALL lb. (ALL x:A. lb [= x) --> lb [= inf)"
|
|
68 |
is_Sup_def "is_Sup A sup ==
|
|
69 |
(ALL x:A. x [= sup) &
|
|
70 |
(ALL ub. (ALL x:A. x [= ub) --> sup [= ub)"
|
|
71 |
|
|
72 |
|
1573
|
73 |
|
1440
|
74 |
(* binary minima and maxima (on lin_orders) *)
|
|
75 |
|
1573
|
76 |
constdefs
|
1440
|
77 |
minimum :: "['a::lin_order, 'a] => 'a"
|
1573
|
78 |
"minimum x y == (if x [= y then x else y)"
|
1440
|
79 |
|
1573
|
80 |
maximum :: "['a::lin_order, 'a] => 'a"
|
|
81 |
"maximum x y == (if x [= y then y else x)"
|
1440
|
82 |
|
|
83 |
end
|