|
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 ------------------------------------------------------------------------*) |
|
13 Goalw [setle_def] "!!x. ALL y: S. y <= x ==> S *<= x"; |
|
14 by (assume_tac 1); |
|
15 qed "setleI"; |
|
16 |
|
17 Goalw [setle_def] "!!x. [| S *<= x; y: S |] ==> y <= x"; |
|
18 by (Fast_tac 1); |
|
19 qed "setleD"; |
|
20 |
|
21 Goalw [setge_def] "!!x. ALL y: S. x<= y ==> x <=* S"; |
|
22 by (assume_tac 1); |
|
23 qed "setgeI"; |
|
24 |
|
25 Goalw [setge_def] "!!x. [| x <=* S; y: S |] ==> x <= y"; |
|
26 by (Fast_tac 1); |
|
27 qed "setgeD"; |
|
28 |
|
29 (*------------------------------------------------------------------------ |
|
30 Rules about leastP, ub and lub |
|
31 ------------------------------------------------------------------------*) |
|
32 Goalw [leastP_def] "!!x. leastP P x ==> P x"; |
|
33 by (Step_tac 1); |
|
34 qed "leastPD1"; |
|
35 |
|
36 Goalw [leastP_def] "!!x. leastP P x ==> x <=* Collect P"; |
|
37 by (Step_tac 1); |
|
38 qed "leastPD2"; |
|
39 |
|
40 Goal "!!x. [| leastP P x; y: Collect P |] ==> x <= y"; |
|
41 by (blast_tac (claset() addSDs [leastPD2,setgeD]) 1); |
|
42 qed "leastPD3"; |
|
43 |
|
44 Goalw [isLub_def,isUb_def,leastP_def] |
|
45 "!!x. isLub R S x ==> S *<= x"; |
|
46 by (Step_tac 1); |
|
47 qed "isLubD1"; |
|
48 |
|
49 Goalw [isLub_def,isUb_def,leastP_def] |
|
50 "!!x. isLub R S x ==> x: R"; |
|
51 by (Step_tac 1); |
|
52 qed "isLubD1a"; |
|
53 |
|
54 Goalw [isUb_def] "!!x. isLub R S x ==> isUb R S x"; |
|
55 by (blast_tac (claset() addDs [isLubD1,isLubD1a]) 1); |
|
56 qed "isLub_isUb"; |
|
57 |
|
58 Goal "!!x. [| isLub R S x; y : S |] ==> y <= x"; |
|
59 by (blast_tac (claset() addSDs [isLubD1,setleD]) 1); |
|
60 qed "isLubD2"; |
|
61 |
|
62 Goalw [isLub_def] "!!x. isLub R S x ==> leastP(isUb R S) x"; |
|
63 by (assume_tac 1); |
|
64 qed "isLubD3"; |
|
65 |
|
66 Goalw [isLub_def] "!!x. leastP(isUb R S) x ==> isLub R S x"; |
|
67 by (assume_tac 1); |
|
68 qed "isLubI1"; |
|
69 |
|
70 Goalw [isLub_def,leastP_def] |
|
71 "!!x. [| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"; |
|
72 by (Step_tac 1); |
|
73 qed "isLubI2"; |
|
74 |
|
75 Goalw [isUb_def] "!!x. [| isUb R S x; y : S |] ==> y <= x"; |
|
76 by (fast_tac (claset() addDs [setleD]) 1); |
|
77 qed "isUbD"; |
|
78 |
|
79 Goalw [isUb_def] "!!x. isUb R S x ==> S *<= x"; |
|
80 by (Step_tac 1); |
|
81 qed "isUbD2"; |
|
82 |
|
83 Goalw [isUb_def] "!!x. isUb R S x ==> x: R"; |
|
84 by (Step_tac 1); |
|
85 qed "isUbD2a"; |
|
86 |
|
87 Goalw [isUb_def] "!!x. [| S *<= x; x: R |] ==> isUb R S x"; |
|
88 by (Step_tac 1); |
|
89 qed "isUbI"; |
|
90 |
|
91 Goalw [isLub_def] "!!x. [| isLub R S x; isUb R S y |] ==> x <= y"; |
|
92 by (blast_tac (claset() addSIs [leastPD3]) 1); |
|
93 qed "isLub_le_isUb"; |
|
94 |
|
95 Goalw [ubs_def,isLub_def] "!!x. isLub R S x ==> x <=* ubs R S"; |
|
96 by (etac leastPD2 1); |
|
97 qed "isLub_ubs"; |
|
98 |
|
99 |
|
100 |
|
101 |