author | paulson |
Wed, 15 Jul 1998 14:19:02 +0200 | |
changeset 5148 | 74919e8f221c |
parent 5143 | b94cd208f073 |
child 7219 | 4e3f386c2e37 |
permissions | -rw-r--r-- |
5078 | 1 |
(* Title : Lubs.ML |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : Completeness of the reals. A few of the |
|
5 |
definitions suggested by James Margetson |
|
6 |
*) |
|
7 |
||
8 |
open Lubs; |
|
9 |
||
10 |
(*------------------------------------------------------------------------ |
|
11 |
Rules for *<= and <=* |
|
12 |
------------------------------------------------------------------------*) |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
13 |
Goalw [setle_def] "ALL y: S. y <= x ==> S *<= x"; |
5078 | 14 |
by (assume_tac 1); |
15 |
qed "setleI"; |
|
16 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
17 |
Goalw [setle_def] "[| S *<= x; y: S |] ==> y <= x"; |
5078 | 18 |
by (Fast_tac 1); |
19 |
qed "setleD"; |
|
20 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
21 |
Goalw [setge_def] "ALL y: S. x<= y ==> x <=* S"; |
5078 | 22 |
by (assume_tac 1); |
23 |
qed "setgeI"; |
|
24 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
25 |
Goalw [setge_def] "[| x <=* S; y: S |] ==> x <= y"; |
5078 | 26 |
by (Fast_tac 1); |
27 |
qed "setgeD"; |
|
28 |
||
29 |
(*------------------------------------------------------------------------ |
|
30 |
Rules about leastP, ub and lub |
|
31 |
------------------------------------------------------------------------*) |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
32 |
Goalw [leastP_def] "leastP P x ==> P x"; |
5078 | 33 |
by (Step_tac 1); |
34 |
qed "leastPD1"; |
|
35 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
36 |
Goalw [leastP_def] "leastP P x ==> x <=* Collect P"; |
5078 | 37 |
by (Step_tac 1); |
38 |
qed "leastPD2"; |
|
39 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
40 |
Goal "[| leastP P x; y: Collect P |] ==> x <= y"; |
5078 | 41 |
by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1); |
42 |
qed "leastPD3"; |
|
43 |
||
44 |
Goalw [isLub_def,isUb_def,leastP_def] |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
45 |
"isLub R S x ==> S *<= x"; |
5078 | 46 |
by (Step_tac 1); |
47 |
qed "isLubD1"; |
|
48 |
||
49 |
Goalw [isLub_def,isUb_def,leastP_def] |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
50 |
"isLub R S x ==> x: R"; |
5078 | 51 |
by (Step_tac 1); |
52 |
qed "isLubD1a"; |
|
53 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
54 |
Goalw [isUb_def] "isLub R S x ==> isUb R S x"; |
5078 | 55 |
by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1); |
56 |
qed "isLub_isUb"; |
|
57 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
58 |
Goal "[| isLub R S x; y : S |] ==> y <= x"; |
5078 | 59 |
by (blast_tac (claset() addSDs [isLubD1,setleD]) 1); |
60 |
qed "isLubD2"; |
|
61 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
62 |
Goalw [isLub_def] "isLub R S x ==> leastP(isUb R S) x"; |
5078 | 63 |
by (assume_tac 1); |
64 |
qed "isLubD3"; |
|
65 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
66 |
Goalw [isLub_def] "leastP(isUb R S) x ==> isLub R S x"; |
5078 | 67 |
by (assume_tac 1); |
68 |
qed "isLubI1"; |
|
69 |
||
70 |
Goalw [isLub_def,leastP_def] |
|
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset
|
71 |
"[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"; |
5078 | 72 |
by (Step_tac 1); |
73 |
qed "isLubI2"; |
|
74 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
75 |
Goalw [isUb_def] "[| isUb R S x; y : S |] ==> y <= x"; |
5078 | 76 |
by (fast_tac (claset() addDs [setleD]) 1); |
77 |
qed "isUbD"; |
|
78 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
79 |
Goalw [isUb_def] "isUb R S x ==> S *<= x"; |
5078 | 80 |
by (Step_tac 1); |
81 |
qed "isUbD2"; |
|
82 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
83 |
Goalw [isUb_def] "isUb R S x ==> x: R"; |
5078 | 84 |
by (Step_tac 1); |
85 |
qed "isUbD2a"; |
|
86 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
87 |
Goalw [isUb_def] "[| S *<= x; x: R |] ==> isUb R S x"; |
5078 | 88 |
by (Step_tac 1); |
89 |
qed "isUbI"; |
|
90 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
91 |
Goalw [isLub_def] "[| isLub R S x; isUb R S y |] ==> x <= y"; |
5078 | 92 |
by (blast_tac (claset() addSIs [leastPD3]) 1); |
93 |
qed "isLub_le_isUb"; |
|
94 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
95 |
Goalw [ubs_def,isLub_def] "isLub R S x ==> x <=* ubs R S"; |
5078 | 96 |
by (etac leastPD2 1); |
97 |
qed "isLub_ubs"; |
|
98 |
||
99 |
||
100 |
||
101 |