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