4 |
4 |
5 (** basic properties of "Inf" and "Sup" **) |
5 (** basic properties of "Inf" and "Sup" **) |
6 |
6 |
7 (* unique existence *) |
7 (* unique existence *) |
8 |
8 |
9 goalw thy [Inf_def] "is_Inf A (Inf A)"; |
9 Goalw [Inf_def] "is_Inf A (Inf A)"; |
10 by (rtac (ex_Inf RS spec RS selectI1) 1); |
10 by (rtac (ex_Inf RS spec RS selectI1) 1); |
11 qed "Inf_is_Inf"; |
11 qed "Inf_is_Inf"; |
12 |
12 |
13 goal thy "is_Inf A inf --> Inf A = inf"; |
13 Goal "is_Inf A inf --> Inf A = inf"; |
14 by (rtac impI 1); |
14 by (rtac impI 1); |
15 by (rtac (is_Inf_uniq RS mp) 1); |
15 by (rtac (is_Inf_uniq RS mp) 1); |
16 by (rtac conjI 1); |
16 by (rtac conjI 1); |
17 by (rtac Inf_is_Inf 1); |
17 by (rtac Inf_is_Inf 1); |
18 by (assume_tac 1); |
18 by (assume_tac 1); |
19 qed "Inf_uniq"; |
19 qed "Inf_uniq"; |
20 |
20 |
21 goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf"; |
21 Goalw [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf"; |
22 by Safe_tac; |
22 by Safe_tac; |
23 by (Step_tac 1); |
23 by (Step_tac 1); |
24 by (Step_tac 1); |
24 by (Step_tac 1); |
25 by (rtac Inf_is_Inf 1); |
25 by (rtac Inf_is_Inf 1); |
26 by (rtac (Inf_uniq RS mp RS sym) 1); |
26 by (rtac (Inf_uniq RS mp RS sym) 1); |
27 by (assume_tac 1); |
27 by (assume_tac 1); |
28 qed "ex1_Inf"; |
28 qed "ex1_Inf"; |
29 |
29 |
30 |
30 |
31 goalw thy [Sup_def] "is_Sup A (Sup A)"; |
31 Goalw [Sup_def] "is_Sup A (Sup A)"; |
32 by (rtac (ex_Sup RS spec RS selectI1) 1); |
32 by (rtac (ex_Sup RS spec RS selectI1) 1); |
33 qed "Sup_is_Sup"; |
33 qed "Sup_is_Sup"; |
34 |
34 |
35 goal thy "is_Sup A sup --> Sup A = sup"; |
35 Goal "is_Sup A sup --> Sup A = sup"; |
36 by (rtac impI 1); |
36 by (rtac impI 1); |
37 by (rtac (is_Sup_uniq RS mp) 1); |
37 by (rtac (is_Sup_uniq RS mp) 1); |
38 by (rtac conjI 1); |
38 by (rtac conjI 1); |
39 by (rtac Sup_is_Sup 1); |
39 by (rtac Sup_is_Sup 1); |
40 by (assume_tac 1); |
40 by (assume_tac 1); |
41 qed "Sup_uniq"; |
41 qed "Sup_uniq"; |
42 |
42 |
43 goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup"; |
43 Goalw [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup"; |
44 by Safe_tac; |
44 by Safe_tac; |
45 by (Step_tac 1); |
45 by (Step_tac 1); |
46 by (Step_tac 1); |
46 by (Step_tac 1); |
47 by (rtac Sup_is_Sup 1); |
47 by (rtac Sup_is_Sup 1); |
48 by (rtac (Sup_uniq RS mp RS sym) 1); |
48 by (rtac (Sup_uniq RS mp RS sym) 1); |
121 |
121 |
122 |
122 |
123 |
123 |
124 (** Subsets and limits **) |
124 (** Subsets and limits **) |
125 |
125 |
126 goal thy "A <= B --> Inf B [= Inf A"; |
126 Goal "A <= B --> Inf B [= Inf A"; |
127 by (rtac impI 1); |
127 by (rtac impI 1); |
128 by (stac le_Inf_eq 1); |
128 by (stac le_Inf_eq 1); |
129 by (rewtac Ball_def); |
129 by (rewtac Ball_def); |
130 by Safe_tac; |
130 by Safe_tac; |
131 by (dtac subsetD 1); |
131 by (dtac subsetD 1); |
132 by (assume_tac 1); |
132 by (assume_tac 1); |
133 by (etac Inf_lb 1); |
133 by (etac Inf_lb 1); |
134 qed "Inf_subset_antimon"; |
134 qed "Inf_subset_antimon"; |
135 |
135 |
136 goal thy "A <= B --> Sup A [= Sup B"; |
136 Goal "A <= B --> Sup A [= Sup B"; |
137 by (rtac impI 1); |
137 by (rtac impI 1); |
138 by (stac ge_Sup_eq 1); |
138 by (stac ge_Sup_eq 1); |
139 by (rewtac Ball_def); |
139 by (rewtac Ball_def); |
140 by Safe_tac; |
140 by Safe_tac; |
141 by (dtac subsetD 1); |
141 by (dtac subsetD 1); |
144 qed "Sup_subset_mon"; |
144 qed "Sup_subset_mon"; |
145 |
145 |
146 |
146 |
147 (** singleton / empty limits **) |
147 (** singleton / empty limits **) |
148 |
148 |
149 goal thy "Inf {x} = x"; |
149 Goal "Inf {x} = x"; |
150 by (rtac (Inf_uniq RS mp) 1); |
150 by (rtac (Inf_uniq RS mp) 1); |
151 by (rewtac is_Inf_def); |
151 by (rewtac is_Inf_def); |
152 by Safe_tac; |
152 by Safe_tac; |
153 by (rtac le_refl 1); |
153 by (rtac le_refl 1); |
154 by (Fast_tac 1); |
154 by (Fast_tac 1); |
155 qed "sing_Inf_eq"; |
155 qed "sing_Inf_eq"; |
156 |
156 |
157 goal thy "Sup {x} = x"; |
157 Goal "Sup {x} = x"; |
158 by (rtac (Sup_uniq RS mp) 1); |
158 by (rtac (Sup_uniq RS mp) 1); |
159 by (rewtac is_Sup_def); |
159 by (rewtac is_Sup_def); |
160 by Safe_tac; |
160 by Safe_tac; |
161 by (rtac le_refl 1); |
161 by (rtac le_refl 1); |
162 by (Fast_tac 1); |
162 by (Fast_tac 1); |
163 qed "sing_Sup_eq"; |
163 qed "sing_Sup_eq"; |
164 |
164 |
165 |
165 |
166 goal thy "Inf {} = Sup {x. True}"; |
166 Goal "Inf {} = Sup {x. True}"; |
167 by (rtac (Inf_uniq RS mp) 1); |
167 by (rtac (Inf_uniq RS mp) 1); |
168 by (rewtac is_Inf_def); |
168 by (rewtac is_Inf_def); |
169 by Safe_tac; |
169 by Safe_tac; |
170 by (rtac (sing_Sup_eq RS subst) 1); |
170 by (rtac (sing_Sup_eq RS subst) 1); |
171 back(); |
171 back(); |
172 by (rtac (Sup_subset_mon RS mp) 1); |
172 by (rtac (Sup_subset_mon RS mp) 1); |
173 by (Fast_tac 1); |
173 by (Fast_tac 1); |
174 qed "empty_Inf_eq"; |
174 qed "empty_Inf_eq"; |
175 |
175 |
176 goal thy "Sup {} = Inf {x. True}"; |
176 Goal "Sup {} = Inf {x. True}"; |
177 by (rtac (Sup_uniq RS mp) 1); |
177 by (rtac (Sup_uniq RS mp) 1); |
178 by (rewtac is_Sup_def); |
178 by (rewtac is_Sup_def); |
179 by Safe_tac; |
179 by Safe_tac; |
180 by (rtac (sing_Inf_eq RS subst) 1); |
180 by (rtac (sing_Inf_eq RS subst) 1); |
181 by (rtac (Inf_subset_antimon RS mp) 1); |
181 by (rtac (Inf_subset_antimon RS mp) 1); |