5078
|
1 |
(* Title : Lubs.thy
|
7219
|
2 |
ID : $Id$
|
5078
|
3 |
Author : Jacques D. Fleuriot
|
|
4 |
Copyright : 1998 University of Cambridge
|
|
5 |
Description : Upper bounds, lubs definitions
|
|
6 |
suggested by James Margetson
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
7562
|
10 |
Lubs = Main +
|
5078
|
11 |
|
|
12 |
consts
|
|
13 |
|
9279
|
14 |
"*<=" :: ['a set, 'a::ord] => bool (infixl 70)
|
|
15 |
"<=*" :: ['a::ord, 'a set] => bool (infixl 70)
|
5078
|
16 |
|
|
17 |
constdefs
|
9279
|
18 |
leastP :: ['a =>bool,'a::ord] => bool
|
5078
|
19 |
"leastP P x == (P x & x <=* Collect P)"
|
|
20 |
|
9279
|
21 |
isLub :: ['a set, 'a set, 'a::ord] => bool
|
5078
|
22 |
"isLub R S x == leastP (isUb R S) x"
|
|
23 |
|
9279
|
24 |
isUb :: ['a set, 'a set, 'a::ord] => bool
|
5078
|
25 |
"isUb R S x == S *<= x & x: R"
|
|
26 |
|
9279
|
27 |
ubs :: ['a set, 'a::ord set] => 'a set
|
5078
|
28 |
"ubs R S == Collect (isUb R S)"
|
|
29 |
|
|
30 |
defs
|
|
31 |
setle_def
|
|
32 |
"S *<= x == (ALL y: S. y <= x)"
|
|
33 |
|
|
34 |
setge_def
|
|
35 |
"x <=* S == (ALL y: S. x <= y)"
|
|
36 |
|
|
37 |
end
|
|
38 |
|
|
39 |
|