32 |
32 |
33 Goal "trans r"; |
33 Goal "trans r"; |
34 by (simp_tac (simpset() addsimps PO_simp) 1); |
34 by (simp_tac (simpset() addsimps PO_simp) 1); |
35 qed "PartialOrderE3"; |
35 qed "PartialOrderE3"; |
36 |
36 |
37 Goal "[| refl A r; x: A|] ==> (x, x): r"; |
37 Goal "[| refl A r; x \\<in> A|] ==> (x, x) \\<in> r"; |
38 by (afs [refl_def] 1); |
38 by (afs [refl_def] 1); |
39 qed "reflE"; |
39 qed "reflE"; |
40 (* Interesting: A and r don't get bound because the proof doesn't use |
40 (* Interesting: A and r don't get bound because the proof doesn't use |
41 locale rules |
41 locale rules |
42 val reflE = "[| refl ?A ?r; ?x : ?A |] ==> (?x, ?x) : ?r" *) |
42 val reflE = "[| refl ?A ?r; ?x \\<in> ?A |] ==> (?x, ?x) \\<in> ?r" *) |
43 |
43 |
44 Goal "[| antisym r; (a, b): r; (b, a): r |] ==> a = b"; |
44 Goal "[| antisym r; (a, b) \\<in> r; (b, a) \\<in> r |] ==> a = b"; |
45 by (afs [antisym_def] 1); |
45 by (afs [antisym_def] 1); |
46 qed "antisymE"; |
46 qed "antisymE"; |
47 |
47 |
48 Goalw [trans_def] "[| trans r; (a, b): r; (b, c): r|] ==> (a,c): r"; |
48 Goalw [trans_def] "[| trans r; (a, b) \\<in> r; (b, c) \\<in> r|] ==> (a,c) \\<in> r"; |
49 by (Fast_tac 1); |
49 by (Fast_tac 1); |
50 qed "transE"; |
50 qed "transE"; |
51 |
51 |
52 Goal "[| monotone f A r; x: A; y: A; (x, y): r |] ==> (f x, f y): r"; |
52 Goal "[| monotone f A r; x \\<in> A; y \\<in> A; (x, y) \\<in> r |] ==> (f x, f y) \\<in> r"; |
53 by (afs [monotone_def] 1); |
53 by (afs [monotone_def] 1); |
54 qed "monotoneE"; |
54 qed "monotoneE"; |
55 |
55 |
56 Goal "S <= A ==> (| pset = S, order = induced S r |): PartialOrder"; |
56 Goal "S <= A ==> (| pset = S, order = induced S r |) \\<in> PartialOrder"; |
57 by (simp_tac (simpset() addsimps [PartialOrder_def]) 1); |
57 by (simp_tac (simpset() addsimps [PartialOrder_def]) 1); |
58 by (Step_tac 1); |
58 by Auto_tac; |
59 (* refl *) |
59 (* refl *) |
60 by (afs [refl_def,induced_def] 1); |
60 by (afs [refl_def,induced_def] 1); |
61 by (rtac conjI 1); |
61 by (blast_tac (claset() addIs [PartialOrderE1 RS reflE]) 1); |
62 by (Fast_tac 1); |
|
63 by (rtac ballI 1); |
|
64 by (rtac reflE 1); |
|
65 by (rtac PartialOrderE1 1); |
|
66 by (Fast_tac 1); |
|
67 (* antisym *) |
62 (* antisym *) |
68 by (afs [antisym_def,induced_def] 1); |
63 by (afs [antisym_def,induced_def] 1); |
69 by (Step_tac 1); |
64 by (blast_tac (claset() addIs [PartialOrderE2 RS antisymE]) 1); |
70 by (rtac antisymE 1); |
|
71 by (assume_tac 2); |
|
72 by (assume_tac 2); |
|
73 by (rtac PartialOrderE2 1); |
|
74 (* trans *) |
65 (* trans *) |
75 by (afs [trans_def,induced_def] 1); |
66 by (afs [trans_def,induced_def] 1); |
76 by (Step_tac 1); |
67 by (blast_tac (claset() addIs [PartialOrderE3 RS transE]) 1); |
77 by (rtac transE 1); |
|
78 by (assume_tac 2); |
|
79 by (assume_tac 2); |
|
80 by (rtac PartialOrderE3 1); |
|
81 qed "po_subset_po"; |
68 qed "po_subset_po"; |
82 |
69 |
83 Goal "[| (x, y): induced S r; S <= A |] ==> (x, y): r"; |
70 Goal "[| (x, y) \\<in> induced S r; S <= A |] ==> (x, y) \\<in> r"; |
84 by (afs [induced_def] 1); |
71 by (afs [induced_def] 1); |
85 qed "indE"; |
72 qed "indE"; |
86 |
73 |
87 Goal "[| (x, y): r; x: S; y: S |] ==> (x, y): induced S r"; |
74 Goal "[| (x, y) \\<in> r; x \\<in> S; y \\<in> S |] ==> (x, y) \\<in> induced S r"; |
88 by (afs [induced_def] 1); |
75 by (afs [induced_def] 1); |
89 qed "indI"; |
76 qed "indI"; |
90 |
77 |
91 (* with locales *) |
78 (* with locales *) |
92 Open_locale "CL"; |
79 Open_locale "CL"; |
111 |
98 |
112 Goal "islub S cl = isglb S (dual cl)"; |
99 Goal "islub S cl = isglb S (dual cl)"; |
113 by (afs [islub_def,isglb_def,dual_def,converse_def] 1); |
100 by (afs [islub_def,isglb_def,dual_def,converse_def] 1); |
114 qed "islub_dual_isglb"; |
101 qed "islub_dual_isglb"; |
115 |
102 |
116 Goal "dual cl : PartialOrder"; |
103 Goal "dual cl \\<in> PartialOrder"; |
117 by (simp_tac (simpset() addsimps [PartialOrder_def, dual_def]) 1); |
104 by (simp_tac (simpset() addsimps [PartialOrder_def, dual_def]) 1); |
118 by (afs [simp_PO,refl_converse,trans_converse,antisym_converse] 1); |
105 by (afs [simp_PO,refl_converse,trans_converse,antisym_converse] 1); |
119 qed "dualPO"; |
106 qed "dualPO"; |
120 |
107 |
121 Goal "! S. (S <= A -->( ? L. islub S (| pset = A, order = r|) L)) \ |
108 Goal "\\<forall>S. (S <= A -->( \\<exists>L. islub S (| pset = A, order = r|) L)) \ |
122 \ ==> ! S. (S <= A --> (? G. isglb S (| pset = A, order = r|) G))"; |
109 \ ==> \\<forall>S. (S <= A --> (\\<exists>G. isglb S (| pset = A, order = r|) G))"; |
123 by (Step_tac 1); |
110 by (Step_tac 1); |
124 by (res_inst_tac |
111 by (res_inst_tac |
125 [("x"," lub {y. y: A & (! k: S. (y, k): r)}(|pset = A, order = r|)")] |
112 [("x"," lub {y. y \\<in> A & (\\<forall>k \\<in> S. (y, k) \\<in> r)}(|pset = A, order = r|)")] |
126 exI 1); |
113 exI 1); |
127 by (dres_inst_tac [("x","{y. y: A & (! k: S. (y,k): r)}")] spec 1); |
114 by (dres_inst_tac [("x","{y. y \\<in> A & (\\<forall>k \\<in> S. (y,k) \\<in> r)}")] spec 1); |
128 by (dtac mp 1); |
115 by (dtac mp 1); |
129 by (Fast_tac 1); |
116 by (Fast_tac 1); |
130 by (afs [islub_lub, isglb_def] 1); |
117 by (afs [islub_lub, isglb_def] 1); |
131 by (afs [islub_def] 1); |
118 by (afs [islub_def] 1); |
132 by (Blast_tac 1); |
119 by (Blast_tac 1); |
184 |
171 |
185 Goal "(dual cl.<A>) = cl.<A>"; |
172 Goal "(dual cl.<A>) = cl.<A>"; |
186 by (simp_tac (simpset() addsimps [dual_def]) 1); |
173 by (simp_tac (simpset() addsimps [dual_def]) 1); |
187 qed "dualA_iff"; |
174 qed "dualA_iff"; |
188 |
175 |
189 Goal "((x, y): (dual cl.<r>)) = ((y, x): cl.<r>)"; |
176 Goal "((x, y) \\<in> (dual cl.<r>)) = ((y, x) \\<in> cl.<r>)"; |
190 by (simp_tac (simpset() addsimps [dual_def]) 1); |
177 by (simp_tac (simpset() addsimps [dual_def]) 1); |
191 qed "dualr_iff"; |
178 qed "dualr_iff"; |
192 |
179 |
193 Goal "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)"; |
180 Goal "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)"; |
194 by (afs [monotone_def,dualA_iff,dualr_iff] 1); |
181 by (afs [monotone_def,dualA_iff,dualr_iff] 1); |
195 qed "monotone_dual"; |
182 qed "monotone_dual"; |
196 |
183 |
197 Goal "[| x: A; y: A|] ==> interval r x y = interval (dual cl.<r>) y x"; |
184 Goal "[| x \\<in> A; y \\<in> A|] ==> interval r x y = interval (dual cl.<r>) y x"; |
198 by (simp_tac (simpset() addsimps [interval_def,dualr_iff]) 1); |
185 by (simp_tac (simpset() addsimps [interval_def,dualr_iff]) 1); |
199 by (fold_goals_tac [thm "r_def"]); |
186 by (fold_goals_tac [thm "r_def"]); |
200 by (Fast_tac 1); |
187 by (Fast_tac 1); |
201 qed "interval_dual"; |
188 qed "interval_dual"; |
202 |
189 |
203 Goal "[| trans r; interval r a b ~= {} |] ==> (a, b): r"; |
190 Goal "[| trans r; interval r a b \\<noteq> {} |] ==> (a, b) \\<in> r"; |
204 by (afs [interval_def] 1); |
191 by (afs [interval_def] 1); |
205 by (rewtac trans_def); |
192 by (rewtac trans_def); |
206 by (Blast_tac 1); |
193 by (Blast_tac 1); |
207 qed "interval_not_empty"; |
194 qed "interval_not_empty"; |
208 |
195 |
209 Goal "x: interval r a b ==> (a, x): r"; |
196 Goal "x \\<in> interval r a b ==> (a, x) \\<in> r"; |
210 by (afs [interval_def] 1); |
197 by (afs [interval_def] 1); |
211 qed "intervalE1"; |
198 qed "intervalE1"; |
212 |
199 |
213 Goal "[| a: A; b: A; interval r a b ~= {} |] ==> a: interval r a b"; |
200 Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {} |] ==> a \\<in> interval r a b"; |
214 by (simp_tac (simpset() addsimps [interval_def]) 1); |
201 by (simp_tac (simpset() addsimps [interval_def]) 1); |
215 by (afs [PartialOrderE3,interval_not_empty] 1); |
202 by (afs [PartialOrderE3,interval_not_empty] 1); |
216 by (afs [PartialOrderE1 RS reflE] 1); |
203 by (afs [PartialOrderE1 RS reflE] 1); |
217 qed "left_in_interval"; |
204 qed "left_in_interval"; |
218 |
205 |
219 Goal "[| a: A; b: A; interval r a b ~= {} |] ==> b: interval r a b"; |
206 Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {} |] ==> b \\<in> interval r a b"; |
220 by (simp_tac (simpset() addsimps [interval_def]) 1); |
207 by (simp_tac (simpset() addsimps [interval_def]) 1); |
221 by (afs [PartialOrderE3,interval_not_empty] 1); |
208 by (afs [PartialOrderE3,interval_not_empty] 1); |
222 by (afs [PartialOrderE1 RS reflE] 1); |
209 by (afs [PartialOrderE1 RS reflE] 1); |
223 qed "right_in_interval"; |
210 qed "right_in_interval"; |
224 |
211 |
225 Goal "[| (| pset = A, order = r |) : PartialOrder;\ |
212 Goal "[| (| pset = A, order = r |) \\<in> PartialOrder;\ |
226 \ ! S. S <= A --> (? L. islub S (| pset = A, order = r |) L) |] \ |
213 \ \\<forall>S. S <= A --> (\\<exists>L. islub S (| pset = A, order = r |) L) |] \ |
227 \ ==> (| pset = A, order = r |) : CompleteLattice"; |
214 \ ==> (| pset = A, order = r |) \\<in> CompleteLattice"; |
228 by (afs [CompleteLatticeI, Rdual] 1); |
215 by (afs [CompleteLatticeI, Rdual] 1); |
229 qed "CompleteLatticeI_simp"; |
216 qed "CompleteLatticeI_simp"; |
230 |
217 |
231 (* sublattice *) |
218 (* sublattice *) |
232 Goal "S <<= cl ==> S <= A"; |
219 Goal "S <<= cl ==> S <= A"; |
233 by (afs [sublattice_def, CompleteLattice_def, thm "A_def"] 1); |
220 by (afs [sublattice_def, CompleteLattice_def, thm "A_def"] 1); |
234 qed "sublatticeE1"; |
221 qed "sublatticeE1"; |
235 |
222 |
236 Goal "S <<= cl ==> (| pset = S, order = induced S r |) : CompleteLattice"; |
223 Goal "S <<= cl ==> (| pset = S, order = induced S r |) \\<in> CompleteLattice"; |
237 by (afs ([sublattice_def, CompleteLattice_def] @ PO_simp) 1); |
224 by (afs ([sublattice_def, CompleteLattice_def] @ PO_simp) 1); |
238 qed "sublatticeE2"; |
225 qed "sublatticeE2"; |
239 |
226 |
240 Goal "[| S <= A; (| pset = S, order = induced S r |) : CompleteLattice |] ==> S <<= cl"; |
227 Goal "[| S <= A; (| pset = S, order = induced S r |) \\<in> CompleteLattice |] ==> S <<= cl"; |
241 by (afs ([sublattice_def] @ PO_simp) 1); |
228 by (afs ([sublattice_def] @ PO_simp) 1); |
242 qed "sublatticeI"; |
229 qed "sublatticeI"; |
243 |
230 |
244 (* lub *) |
231 (* lub *) |
245 Goal "[| S <= A; islub S cl x; islub S cl L|] ==> x = L"; |
232 Goal "[| S <= A; islub S cl x; islub S cl L|] ==> x = L"; |
246 by (rtac antisymE 1); |
233 by (rtac antisymE 1); |
247 by (rtac CompleteLatticeE12 1); |
234 by (rtac CompleteLatticeE12 1); |
248 by (rewtac islub_def); |
235 by (auto_tac (claset(), simpset() addsimps [islub_def, thm "r_def"])); |
249 by (rotate_tac ~1 1); |
|
250 by (etac conjE 1); |
|
251 by (dtac conjunct2 1); |
|
252 by (dtac conjunct1 1); |
|
253 by (dtac conjunct2 1); |
|
254 by (rotate_tac ~1 1); |
|
255 by (dres_inst_tac [("x","L")] bspec 1); |
|
256 by (assume_tac 1); |
|
257 by (fold_goals_tac [thm "r_def"]); |
|
258 by (etac mp 1); |
|
259 by (assume_tac 1); |
|
260 (* (L, x) : (cl .<r>) *) |
|
261 by (rotate_tac ~1 1); |
|
262 by (etac conjE 1); |
|
263 by (rotate_tac ~1 1); |
|
264 by (dtac conjunct2 1); |
|
265 by (dtac bspec 1); |
|
266 by (etac conjunct1 1); |
|
267 by (etac mp 1); |
|
268 by (etac (conjunct2 RS conjunct1) 1); |
|
269 qed "lub_unique"; |
236 qed "lub_unique"; |
270 |
237 |
271 Goal "[| S <= A |] ==> ! x: S. (x,lub S cl): r"; |
238 Goal "[| S <= A |] ==> \\<forall>x \\<in> S. (x,lub S cl) \\<in> r"; |
272 by (rtac exE 1); |
239 by (rtac exE 1); |
273 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
240 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
274 by (assume_tac 1); |
241 by (assume_tac 1); |
275 by (rewrite_goals_tac [lub_def,least_def]); |
242 by (rewrite_goals_tac [lub_def,least_def]); |
276 by (stac some_equality 1); |
243 by (stac some_equality 1); |
339 |
306 |
340 Goal "[| S <= A; islub S cl L |] ==> L = lub S cl"; |
307 Goal "[| S <= A; islub S cl L |] ==> L = lub S cl"; |
341 by (afs ([lubI, islub_def] @ PO_simp) 1); |
308 by (afs ([lubI, islub_def] @ PO_simp) 1); |
342 qed "lubIa"; |
309 qed "lubIa"; |
343 |
310 |
344 Goal "islub S cl L ==> L : A"; |
311 Goal "islub S cl L ==> L \\<in> A"; |
345 by (afs [islub_def, thm "A_def"] 1); |
312 by (afs [islub_def, thm "A_def"] 1); |
346 qed "islub_in_lattice"; |
313 qed "islub_in_lattice"; |
347 |
314 |
348 Goal "islub S cl L ==> ! y: S. (y, L): r"; |
315 Goal "islub S cl L ==> \\<forall>y \\<in> S. (y, L) \\<in> r"; |
349 by (afs [islub_def, thm "r_def"] 1); |
316 by (afs [islub_def, thm "r_def"] 1); |
350 qed "islubE1"; |
317 qed "islubE1"; |
351 |
318 |
352 Goal "[| islub S cl L; \ |
319 Goal "[| islub S cl L; \ |
353 \ z: A; ! y: S. (y, z): r|] ==> (L, z): r"; |
320 \ z \\<in> A; \\<forall>y \\<in> S. (y, z) \\<in> r|] ==> (L, z) \\<in> r"; |
354 by (afs ([islub_def] @ PO_simp) 1); |
321 by (afs ([islub_def] @ PO_simp) 1); |
355 qed "islubE2"; |
322 qed "islubE2"; |
356 |
323 |
357 Goal "[| S <= A |] ==> ? L. islub S cl L"; |
324 Goal "[| S <= A |] ==> \\<exists>L. islub S cl L"; |
358 by (afs [thm "A_def"] 1); |
325 by (afs [thm "A_def"] 1); |
359 qed "islubE"; |
326 qed "islubE"; |
360 |
327 |
361 Goal "[| L: A; ! y: S. (y, L): r; \ |
328 Goal "[| L \\<in> A; \\<forall>y \\<in> S. (y, L) \\<in> r; \ |
362 \ (!z: A. (! y: S. (y, z):r) --> (L, z): r)|] ==> islub S cl L"; |
329 \ (\\<forall>z \\<in> A. (\\<forall>y \\<in> S. (y, z):r) --> (L, z) \\<in> r)|] ==> islub S cl L"; |
363 by (afs ([islub_def] @ PO_simp) 1); |
330 by (afs ([islub_def] @ PO_simp) 1); |
364 qed "islubI"; |
331 qed "islubI"; |
365 |
332 |
366 (* glb *) |
333 (* glb *) |
367 Goal "S <= A ==> glb S cl : A"; |
334 Goal "S <= A ==> glb S cl \\<in> A"; |
368 by (stac glb_dual_lub 1); |
335 by (stac glb_dual_lub 1); |
369 by (afs [thm "A_def"] 1); |
336 by (afs [thm "A_def"] 1); |
370 by (rtac (dualA_iff RS subst) 1); |
337 by (rtac (dualA_iff RS subst) 1); |
371 by (rtac (export lub_in_lattice) 1); |
338 by (rtac (export lub_in_lattice) 1); |
372 by (rtac CL_dualCL 1); |
339 by (rtac CL_dualCL 1); |
373 by (afs [dualA_iff] 1); |
340 by (afs [dualA_iff] 1); |
374 qed "glb_in_lattice"; |
341 qed "glb_in_lattice"; |
375 |
342 |
376 Goal "S <= A ==> ! x: S. (glb S cl, x): r"; |
343 Goal "S <= A ==> \\<forall>x \\<in> S. (glb S cl, x) \\<in> r"; |
377 by (stac glb_dual_lub 1); |
344 by (stac glb_dual_lub 1); |
378 by (rtac ballI 1); |
345 by (rtac ballI 1); |
379 by (afs [thm "r_def"] 1); |
346 by (afs [thm "r_def"] 1); |
380 by (rtac (dualr_iff RS subst) 1); |
347 by (rtac (dualr_iff RS subst) 1); |
381 by (rtac (export lubE1 RS bspec) 1); |
348 by (rtac (export lubE1 RS bspec) 1); |
382 by (rtac CL_dualCL 1); |
349 by (rtac CL_dualCL 1); |
383 by (afs [dualA_iff, thm "A_def"] 1); |
350 by (afs [dualA_iff, thm "A_def"] 1); |
384 by (assume_tac 1); |
351 by (assume_tac 1); |
385 qed "glbE1"; |
352 qed "glbE1"; |
386 |
353 |
387 (* Reduce the sublattice property by using substructural properties! *) |
354 (* Reduce the sublattice property by using substructural properties\\<forall>*) |
388 (* abandoned see Tarski_4.ML *) |
355 (* abandoned see Tarski_4.ML *) |
389 |
356 |
390 Open_locale "CLF"; |
357 Open_locale "CLF"; |
391 |
358 |
392 val simp_CLF = simplify (simpset() addsimps [CLF_def]) (thm "f_cl"); |
359 val simp_CLF = simplify (simpset() addsimps [CLF_def]) (thm "f_cl"); |
393 Addsimps [simp_CLF, thm "f_cl"]; |
360 Addsimps [simp_CLF, thm "f_cl"]; |
394 |
361 |
395 Goal "f : A funcset A"; |
362 Goal "f \\<in> A funcset A"; |
396 by (simp_tac (simpset() addsimps [thm "A_def"]) 1); |
363 by (simp_tac (simpset() addsimps [thm "A_def"]) 1); |
397 qed "CLF_E1"; |
364 qed "CLF_E1"; |
398 |
365 |
399 Goal "monotone f A r"; |
366 Goal "monotone f A r"; |
400 by (simp_tac (simpset() addsimps PO_simp) 1); |
367 by (simp_tac (simpset() addsimps PO_simp) 1); |
401 qed "CLF_E2"; |
368 qed "CLF_E2"; |
402 |
369 |
403 Goal "f : CLF `` {cl} ==> f : CLF `` {dual cl}"; |
370 Goal "f \\<in> CLF `` {cl} ==> f \\<in> CLF `` {dual cl}"; |
404 by (afs [CLF_def, CL_dualCL, monotone_dual] 1); |
371 by (afs [CLF_def, CL_dualCL, monotone_dual] 1); |
405 by (afs [dualA_iff] 1); |
372 by (afs [dualA_iff] 1); |
406 qed "CLF_dual"; |
373 qed "CLF_dual"; |
407 |
374 |
408 (* fixed points *) |
375 (* fixed points *) |
409 Goal "P <= A"; |
376 Goal "P <= A"; |
410 by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1); |
377 by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1); |
411 by (Fast_tac 1); |
378 by (Fast_tac 1); |
412 qed "fixfE1"; |
379 qed "fixfE1"; |
413 |
380 |
414 Goal "x: P ==> f x = x"; |
381 Goal "x \\<in> P ==> f x = x"; |
415 by (afs [thm "P_def", fix_def] 1); |
382 by (afs [thm "P_def", fix_def] 1); |
416 qed "fixfE2"; |
383 qed "fixfE2"; |
417 |
384 |
418 Goal "[| A <= B; x: fix (lam y: A. f y) A |] ==> x: fix f B"; |
385 Goal "[| A <= B; x \\<in> fix (lam y: A. f y) A |] ==> x \\<in> fix f B"; |
419 by (forward_tac [export fixfE2] 1); |
386 by (forward_tac [export fixfE2] 1); |
420 by (dtac ((export fixfE1) RS subsetD) 1); |
387 by (dtac ((export fixfE1) RS subsetD) 1); |
421 by (afs [fix_def] 1); |
388 by (asm_full_simp_tac (simpset() addsimps [fix_def, subsetD]) 1); |
422 by (rtac conjI 1); |
|
423 by (Fast_tac 1); |
|
424 by (res_inst_tac [("P","% y. f x = y")] subst 1); |
|
425 by (assume_tac 1); |
|
426 by (rtac sym 1); |
|
427 by (etac restrict_apply1 1); |
|
428 qed "fixf_subset"; |
389 qed "fixf_subset"; |
429 |
390 |
430 (* lemmas for Tarski, lub *) |
391 (* lemmas for Tarski, lub *) |
431 Goal "H = {x. (x, f x) : r & x : A} ==> (lub H cl, f (lub H cl)) : r"; |
392 Goal "H = {x. (x, f x) \\<in> r & x \\<in> A} ==> (lub H cl, f (lub H cl)) \\<in> r"; |
432 by (rtac lubE2 1); |
393 by (rtac lubE2 1); |
433 by (Fast_tac 1); |
394 by (Fast_tac 1); |
434 by (rtac (CLF_E1 RS funcset_mem) 1); |
395 by (rtac (CLF_E1 RS funcset_mem) 1); |
435 by (rtac lub_in_lattice 1); |
396 by (rtac lub_in_lattice 1); |
436 by (Fast_tac 1); |
397 by (Fast_tac 1); |
437 (* ! x:H. (x, f (lub H r)) : r *) |
398 (* \\<forall>x:H. (x, f (lub H r)) \\<in> r *) |
438 by (rtac ballI 1); |
399 by (rtac ballI 1); |
439 by (rtac transE 1); |
400 by (rtac transE 1); |
440 by (rtac CompleteLatticeE13 1); |
401 by (rtac CompleteLatticeE13 1); |
441 (* instantiates (x, ???z): cl.<r> to (x, f x), because of the def of H *) |
402 (* instantiates (x, ???z) \\<in> cl.<r> to (x, f x), because of the def of H *) |
442 by (Fast_tac 1); |
403 by (Fast_tac 1); |
443 (* so it remains to show (f x, f (lub H cl)) : r *) |
404 (* so it remains to show (f x, f (lub H cl)) \\<in> r *) |
444 by (res_inst_tac [("f","f")] monotoneE 1); |
405 by (res_inst_tac [("f","f")] monotoneE 1); |
445 by (rtac CLF_E2 1); |
406 by (rtac CLF_E2 1); |
446 by (Fast_tac 1); |
407 by (Fast_tac 1); |
447 by (rtac lub_in_lattice 1); |
408 by (rtac lub_in_lattice 1); |
448 by (Fast_tac 1); |
409 by (Fast_tac 1); |
449 by (rtac (lubE1 RS bspec) 1); |
410 by (rtac (lubE1 RS bspec) 1); |
450 by (Fast_tac 1); |
411 by (Fast_tac 1); |
451 by (assume_tac 1); |
412 by (assume_tac 1); |
452 qed "lubH_le_flubH"; |
413 qed "lubH_le_flubH"; |
453 |
414 |
454 Goal "[| H = {x. (x, f x) : r & x : A} |] ==> (f (lub H cl), lub H cl) : r"; |
415 Goal "[| H = {x. (x, f x) \\<in> r & x \\<in> A} |] ==> (f (lub H cl), lub H cl) \\<in> r"; |
455 by (rtac (lubE1 RS bspec) 1); |
416 by (rtac (lubE1 RS bspec) 1); |
456 by (Fast_tac 1); |
417 by (Fast_tac 1); |
457 by (res_inst_tac [("t","H")] ssubst 1); |
418 by (res_inst_tac [("t","H")] ssubst 1); |
458 by (assume_tac 1); |
419 by (assume_tac 1); |
459 by (rtac CollectI 1); |
420 by (rtac CollectI 1); |
492 by (rtac CompleteLatticeE11 1); |
453 by (rtac CompleteLatticeE11 1); |
493 by (etac (fixfE1 RS subsetD) 1); |
454 by (etac (fixfE1 RS subsetD) 1); |
494 by (etac (fixfE1 RS subsetD) 1); |
455 by (etac (fixfE1 RS subsetD) 1); |
495 qed "fix_in_H"; |
456 qed "fix_in_H"; |
496 |
457 |
497 Goal "H = {x. (x, f x) : r & x : A} ==> ! x: P. (x, lub H cl) : r"; |
458 Goal "H = {x. (x, f x) \\<in> r & x \\<in> A} ==> \\<forall>x \\<in> P. (x, lub H cl) \\<in> r"; |
498 by (rtac ballI 1); |
459 by (rtac ballI 1); |
499 by (rtac (lubE1 RS bspec) 1); |
460 by (rtac (lubE1 RS bspec) 1); |
500 by (Fast_tac 1); |
461 by (Fast_tac 1); |
501 by (rtac fix_in_H 1); |
462 by (rtac fix_in_H 1); |
502 by (REPEAT (atac 1)); |
463 by (REPEAT (atac 1)); |
503 qed "fixf_le_lubH"; |
464 qed "fixf_le_lubH"; |
504 |
465 |
505 Goal "H = {x. (x, f x) : r & x : A} ==> ! L. (! y: P. (y,L): r) --> (lub H cl, L): r"; |
466 Goal "H = {x. (x, f x) \\<in> r & x \\<in> A} ==> \\<forall>L. (\\<forall>y \\<in> P. (y,L) \\<in> r) --> (lub H cl, L) \\<in> r"; |
506 by (rtac allI 1); |
467 by (rtac allI 1); |
507 by (rtac impI 1); |
468 by (rtac impI 1); |
508 by (etac bspec 1); |
469 by (etac bspec 1); |
509 by (rtac lubH_is_fixp 1); |
470 by (rtac lubH_is_fixp 1); |
510 by (assume_tac 1); |
471 by (assume_tac 1); |
511 qed "lubH_least_fixf"; |
472 qed "lubH_least_fixf"; |
512 |
473 |
513 (* Tarski fixpoint theorem 1, first part *) |
474 (* Tarski fixpoint theorem 1, first part *) |
514 Goal "lub P cl = lub {x. (x, f x) : r & x : A} cl"; |
475 Goal "lub P cl = lub {x. (x, f x) \\<in> r & x \\<in> A} cl"; |
515 by (rtac sym 1); |
476 by (rtac sym 1); |
516 by (rtac lubI 1); |
477 by (rtac lubI 1); |
517 by (rtac fixfE1 1); |
478 by (rtac fixfE1 1); |
518 by (rtac lub_in_lattice 1); |
479 by (rtac lub_in_lattice 1); |
519 by (Fast_tac 1); |
480 by (Fast_tac 1); |
520 by (afs [fixf_le_lubH] 1); |
481 by (afs [fixf_le_lubH] 1); |
521 by (afs [lubH_least_fixf] 1); |
482 by (afs [lubH_least_fixf] 1); |
522 qed "T_thm_1_lub"; |
483 qed "T_thm_1_lub"; |
523 |
484 |
524 (* Tarski for glb *) |
485 (* Tarski for glb *) |
525 Goal "H = {x. (f x, x): r & x : A} ==> glb H cl : P"; |
486 Goal "H = {x. (f x, x) \\<in> r & x \\<in> A} ==> glb H cl \\<in> P"; |
526 by (full_simp_tac |
487 by (full_simp_tac |
527 (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1); |
488 (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1); |
528 by (rtac (dualA_iff RS subst) 1); |
489 by (rtac (dualA_iff RS subst) 1); |
529 by (rtac (CL_dualCL RS (export lubH_is_fixp)) 1); |
490 by (rtac (CL_dualCL RS (export lubH_is_fixp)) 1); |
530 by (rtac (thm "f_cl" RS CLF_dual) 1); |
491 by (rtac (thm "f_cl" RS CLF_dual) 1); |
531 by (afs [dualr_iff, dualA_iff] 1); |
492 by (afs [dualr_iff, dualA_iff] 1); |
532 qed "glbH_is_fixp"; |
493 qed "glbH_is_fixp"; |
533 |
494 |
534 Goal "glb P cl = glb {x. (f x, x): r & x : A} cl"; |
495 Goal "glb P cl = glb {x. (f x, x) \\<in> r & x \\<in> A} cl"; |
535 by (simp_tac (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1); |
496 by (simp_tac (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1); |
536 by (rtac (dualA_iff RS subst) 1); |
497 by (rtac (dualA_iff RS subst) 1); |
537 by (rtac (CL_dualCL RS (export T_thm_1_lub) RS ssubst) 1); |
498 by (rtac (CL_dualCL RS (export T_thm_1_lub) RS ssubst) 1); |
538 by (rtac (thm "f_cl" RS CLF_dual) 1); |
499 by (rtac (thm "f_cl" RS CLF_dual) 1); |
539 by (afs [dualr_iff] 1); |
500 by (afs [dualr_iff] 1); |
542 (* interval *) |
503 (* interval *) |
543 Goal "refl A r ==> r <= A <*> A"; |
504 Goal "refl A r ==> r <= A <*> A"; |
544 by (afs [refl_def] 1); |
505 by (afs [refl_def] 1); |
545 qed "reflE1"; |
506 qed "reflE1"; |
546 |
507 |
547 Goal "(x, y): r ==> x: A"; |
508 Goal "(x, y) \\<in> r ==> x \\<in> A"; |
548 by (rtac SigmaD1 1); |
509 by (rtac SigmaD1 1); |
549 by (rtac (reflE1 RS subsetD) 1); |
510 by (rtac (reflE1 RS subsetD) 1); |
550 by (rtac CompleteLatticeE11 1); |
511 by (rtac CompleteLatticeE11 1); |
551 by (assume_tac 1); |
512 by (assume_tac 1); |
552 qed "rel_imp_elem"; |
513 qed "rel_imp_elem"; |
553 |
514 |
554 Goal "[| a: A; b: A |] ==> interval r a b <= A"; |
515 Goal "[| a \\<in> A; b \\<in> A |] ==> interval r a b <= A"; |
555 by (simp_tac (simpset() addsimps [interval_def]) 1); |
516 by (simp_tac (simpset() addsimps [interval_def]) 1); |
556 by (rtac subsetI 1); |
517 by (blast_tac (claset() addIs [rel_imp_elem]) 1); |
557 by (rtac rel_imp_elem 1); |
|
558 by (dtac CollectD 1); |
|
559 by (etac conjunct2 1); |
|
560 qed "interval_subset"; |
518 qed "interval_subset"; |
561 |
519 |
562 Goal "[| (a, x): r; (x, b): r |] ==> x: interval r a b"; |
520 Goal "[| (a, x) \\<in> r; (x, b) \\<in> r |] ==> x \\<in> interval r a b"; |
563 by (afs [interval_def] 1); |
521 by (afs [interval_def] 1); |
564 qed "intervalI"; |
522 qed "intervalI"; |
565 |
523 |
566 Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (a, x): r"; |
524 Goalw [interval_def] "[| S <= interval r a b; x \\<in> S |] ==> (a, x) \\<in> r"; |
567 by (Fast_tac 1); |
525 by (Fast_tac 1); |
568 qed "interval_lemma1"; |
526 qed "interval_lemma1"; |
569 |
527 |
570 Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (x, b): r"; |
528 Goalw [interval_def] "[| S <= interval r a b; x \\<in> S |] ==> (x, b) \\<in> r"; |
571 by (Fast_tac 1); |
529 by (Fast_tac 1); |
572 qed "interval_lemma2"; |
530 qed "interval_lemma2"; |
573 |
531 |
574 Goal "[| S <= A; S ~= {};\ |
532 Goal "[| S <= A; S \\<noteq> {};\ |
575 \ ! x: S. (a,x): r; ! y: S. (y, L): r |] ==> (a,L): r"; |
533 \ \\<forall>x \\<in> S. (a,x) \\<in> r; \\<forall>y \\<in> S. (y, L) \\<in> r |] ==> (a,L) \\<in> r"; |
576 by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1); |
534 by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1); |
577 qed "a_less_lub"; |
535 qed "a_less_lub"; |
578 |
536 |
579 Goal "[| S <= A; S ~= {};\ |
537 Goal "[| S <= A; S \\<noteq> {};\ |
580 \ ! x: S. (x,b): r; ! y: S. (G, y): r |] ==> (G,b): r"; |
538 \ \\<forall>x \\<in> S. (x,b) \\<in> r; \\<forall>y \\<in> S. (G, y) \\<in> r |] ==> (G,b) \\<in> r"; |
581 by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1); |
539 by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1); |
582 qed "glb_less_b"; |
540 qed "glb_less_b"; |
583 |
541 |
584 Goal "[| a : A; b : A; S <= interval r a b |]==> S <= A"; |
542 Goal "[| a \\<in> A; b \\<in> A; S <= interval r a b |]==> S <= A"; |
585 by (afs [interval_subset RSN(2, subset_trans)] 1); |
543 by (afs [interval_subset RSN(2, subset_trans)] 1); |
586 qed "S_intv_cl"; |
544 qed "S_intv_cl"; |
587 |
545 |
588 Goal "[| a : A; b: A; S <= interval r a b; \ |
546 Goal "[| a \\<in> A; b \\<in> A; S <= interval r a b; \ |
589 \ S ~= {}; islub S cl L; interval r a b ~= {} |] ==> L : interval r a b"; |
547 \ S \\<noteq> {}; islub S cl L; interval r a b \\<noteq> {} |] ==> L \\<in> interval r a b"; |
590 by (rtac intervalI 1); |
548 by (rtac intervalI 1); |
591 by (rtac a_less_lub 1); |
549 by (rtac a_less_lub 1); |
592 by (assume_tac 2); |
550 by (assume_tac 2); |
593 by (afs [S_intv_cl] 1); |
551 by (afs [S_intv_cl] 1); |
594 by (rtac ballI 1); |
552 by (rtac ballI 1); |
595 by (afs [interval_lemma1] 1); |
553 by (afs [interval_lemma1] 1); |
596 by (afs [islubE1] 1); |
554 by (afs [islubE1] 1); |
597 (* (L, b) : r *) |
555 (* (L, b) \\<in> r *) |
598 by (rtac islubE2 1); |
556 by (rtac islubE2 1); |
599 by (assume_tac 1); |
557 by (assume_tac 1); |
600 by (assume_tac 1); |
558 by (assume_tac 1); |
601 by (rtac ballI 1); |
559 by (rtac ballI 1); |
602 by (afs [interval_lemma2] 1); |
560 by (afs [interval_lemma2] 1); |
603 qed "L_in_interval"; |
561 qed "L_in_interval"; |
604 |
562 |
605 Goal "[| a : A; b : A; interval r a b ~= {}; S <= interval r a b; isglb S cl G; \ |
563 Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {}; S <= interval r a b; isglb S cl G; \ |
606 \ S ~= {} |] ==> G : interval r a b"; |
564 \ S \\<noteq> {} |] ==> G \\<in> interval r a b"; |
607 by (afs [interval_dual] 1); |
565 by (afs [interval_dual] 1); |
608 by (rtac (export L_in_interval) 1); |
566 by (rtac (export L_in_interval) 1); |
609 by (rtac dualPO 1); |
567 by (rtac dualPO 1); |
610 by (afs [dualA_iff, thm "A_def"] 1); |
568 by (afs [dualA_iff, thm "A_def"] 1); |
611 by (afs [dualA_iff, thm "A_def"] 1); |
569 by (afs [dualA_iff, thm "A_def"] 1); |
613 by (afs [isglb_dual_islub] 1); |
571 by (afs [isglb_dual_islub] 1); |
614 by (afs [isglb_dual_islub] 1); |
572 by (afs [isglb_dual_islub] 1); |
615 by (assume_tac 1); |
573 by (assume_tac 1); |
616 qed "G_in_interval"; |
574 qed "G_in_interval"; |
617 |
575 |
618 Goal "[| a: A; b: A; interval r a b ~= {} |]\ |
576 Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {} |]\ |
619 \ ==> (| pset = interval r a b, order = induced (interval r a b) r |) : PartialOrder"; |
577 \ ==> (| pset = interval r a b, order = induced (interval r a b) r |) \\<in> PartialOrder"; |
620 by (rtac po_subset_po 1); |
578 by (rtac po_subset_po 1); |
621 by (afs [interval_subset] 1); |
579 by (afs [interval_subset] 1); |
622 qed "intervalPO"; |
580 qed "intervalPO"; |
623 |
581 |
624 Goal "[| a : A; b : A;\ |
582 Goal "[| a \\<in> A; b \\<in> A;\ |
625 \ interval r a b ~= {} |] ==> ! S. S <= interval r a b -->\ |
583 \ interval r a b \\<noteq> {} |] ==> \\<forall>S. S <= interval r a b -->\ |
626 \ (? L. islub S (| pset = interval r a b, order = induced (interval r a b) r |) L)"; |
584 \ (\\<exists>L. islub S (| pset = interval r a b, order = induced (interval r a b) r |) L)"; |
627 by (strip_tac 1); |
585 by (strip_tac 1); |
628 by (forward_tac [S_intv_cl RS islubE] 1); |
586 by (forward_tac [S_intv_cl RS islubE] 1); |
629 by (assume_tac 2); |
587 by (assume_tac 2); |
630 by (assume_tac 1); |
588 by (assume_tac 1); |
631 by (etac exE 1); |
589 by (etac exE 1); |
632 (* define the lub for the interval as: *) |
590 (* define the lub for the interval as *) |
633 by (res_inst_tac [("x","if S = {} then a else L")] exI 1); |
591 by (res_inst_tac [("x","if S = {} then a else L")] exI 1); |
634 by (rtac (export islubI) 1); |
592 by (rtac (export islubI) 1); |
635 (* (if S = {} then a else L) : interval r a b *) |
593 (* (if S = {} then a else L) \\<in> interval r a b *) |
636 by (asm_full_simp_tac |
594 by (asm_full_simp_tac |
637 (simpset() addsimps [CompleteLatticeE1,L_in_interval]) 1); |
595 (simpset() addsimps [CompleteLatticeE1,L_in_interval]) 1); |
638 by (afs [left_in_interval] 1); |
596 by (afs [left_in_interval] 1); |
639 (* lub prop 1 *) |
597 (* lub prop 1 *) |
640 by (case_tac "S = {}" 1); |
598 by (case_tac "S = {}" 1); |
641 (* S = {}, y: S = False => everything *) |
599 (* S = {}, y \\<in> S = False => everything *) |
642 by (Fast_tac 1); |
600 by (Fast_tac 1); |
643 (* S ~= {} *) |
601 (* S \\<noteq> {} *) |
644 by (Asm_full_simp_tac 1); |
602 by (Asm_full_simp_tac 1); |
645 (* ! y:S. (y, L) : induced (interval r a b) r *) |
603 (* \\<forall>y:S. (y, L) \\<in> induced (interval r a b) r *) |
646 by (rtac ballI 1); |
604 by (rtac ballI 1); |
647 by (afs [induced_def, L_in_interval] 1); |
605 by (afs [induced_def, L_in_interval] 1); |
648 by (rtac conjI 1); |
606 by (rtac conjI 1); |
649 by (rtac subsetD 1); |
607 by (rtac subsetD 1); |
650 by (afs [S_intv_cl] 1); |
608 by (afs [S_intv_cl] 1); |
651 by (assume_tac 1); |
609 by (assume_tac 1); |
652 by (afs [islubE1] 1); |
610 by (afs [islubE1] 1); |
653 (* ! z:interval r a b. (! y:S. (y, z) : induced (interval r a b) r --> |
611 (* \\<forall>z:interval r a b. (\\<forall>y:S. (y, z) \\<in> induced (interval r a b) r --> |
654 (if S = {} then a else L, z) : induced (interval r a b) r *) |
612 (if S = {} then a else L, z) \\<in> induced (interval r a b) r *) |
655 by (rtac ballI 1); |
613 by (rtac ballI 1); |
656 by (rtac impI 1); |
614 by (rtac impI 1); |
657 by (case_tac "S = {}" 1); |
615 by (case_tac "S = {}" 1); |
658 (* S = {} *) |
616 (* S = {} *) |
659 by (Asm_full_simp_tac 1); |
617 by (Asm_full_simp_tac 1); |
709 by (rtac subset_refl 1); |
667 by (rtac subset_refl 1); |
710 by (fold_goals_tac [thm "r_def"]); |
668 by (fold_goals_tac [thm "r_def"]); |
711 by (afs [glbE1] 1); |
669 by (afs [glbE1] 1); |
712 qed "Bot_in_lattice"; |
670 qed "Bot_in_lattice"; |
713 |
671 |
714 Goal "Top cl: A"; |
672 Goal "Top cl \\<in> A"; |
715 by (simp_tac (simpset() addsimps [Top_dual_Bot, thm "A_def"]) 1); |
673 by (simp_tac (simpset() addsimps [Top_dual_Bot, thm "A_def"]) 1); |
716 by (rtac (dualA_iff RS subst) 1); |
674 by (rtac (dualA_iff RS subst) 1); |
717 by (afs [export Bot_in_lattice,CL_dualCL] 1); |
675 by (afs [export Bot_in_lattice,CL_dualCL] 1); |
718 qed "Top_in_lattice"; |
676 qed "Top_in_lattice"; |
719 |
677 |
720 Goal "x: A ==> (x, Top cl): r"; |
678 Goal "x \\<in> A ==> (x, Top cl) \\<in> r"; |
721 by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1); |
679 by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1); |
722 by (rtac someI2 1); |
680 by (rtac someI2 1); |
723 by (fold_goals_tac [thm "r_def", thm "A_def"]); |
681 by (fold_goals_tac [thm "r_def", thm "A_def"]); |
724 by (Fast_tac 2); |
682 by (Fast_tac 2); |
725 by (rtac conjI 1); |
683 by (rtac conjI 1); |
726 by (rtac lubE1 2); |
684 by (rtac lubE1 2); |
727 by (afs [lub_in_lattice] 1); |
685 by (afs [lub_in_lattice] 1); |
728 by (rtac subset_refl 1); |
686 by (rtac subset_refl 1); |
729 qed "Top_prop"; |
687 qed "Top_prop"; |
730 |
688 |
731 Goal "x: A ==> (Bot cl, x): r"; |
689 Goal "x \\<in> A ==> (Bot cl, x) \\<in> r"; |
732 by (simp_tac (simpset() addsimps [Bot_dual_Top, thm "r_def"]) 1); |
690 by (simp_tac (simpset() addsimps [Bot_dual_Top, thm "r_def"]) 1); |
733 by (rtac (dualr_iff RS subst) 1); |
691 by (rtac (dualr_iff RS subst) 1); |
734 by (rtac (export Top_prop) 1); |
692 by (rtac (export Top_prop) 1); |
735 by (rtac CL_dualCL 1); |
693 by (rtac CL_dualCL 1); |
736 by (afs [dualA_iff, thm "A_def"] 1); |
694 by (afs [dualA_iff, thm "A_def"] 1); |
737 qed "Bot_prop"; |
695 qed "Bot_prop"; |
738 |
696 |
739 Goal "x: A ==> interval r x (Top cl) ~= {}"; |
697 Goal "x \\<in> A ==> interval r x (Top cl) \\<noteq> {}"; |
740 by (rtac notI 1); |
698 by (rtac notI 1); |
741 by (dres_inst_tac [("a","Top cl")] equals0D 1); |
699 by (dres_inst_tac [("a","Top cl")] equals0D 1); |
742 by (afs [interval_def] 1); |
700 by (afs [interval_def] 1); |
743 by (afs [refl_def,Top_in_lattice,Top_prop] 1); |
701 by (afs [refl_def,Top_in_lattice,Top_prop] 1); |
744 qed "Top_intv_not_empty"; |
702 qed "Top_intv_not_empty"; |
745 |
703 |
746 Goal "x: A ==> interval r (Bot cl) x ~= {}"; |
704 Goal "x \\<in> A ==> interval r (Bot cl) x \\<noteq> {}"; |
747 by (simp_tac (simpset() addsimps [Bot_dual_Top]) 1); |
705 by (simp_tac (simpset() addsimps [Bot_dual_Top]) 1); |
748 by (stac interval_dual 1); |
706 by (stac interval_dual 1); |
749 by (assume_tac 2); |
707 by (assume_tac 2); |
750 by (afs [thm "A_def"] 1); |
708 by (afs [thm "A_def"] 1); |
751 by (rtac (dualA_iff RS subst) 1); |
709 by (rtac (dualA_iff RS subst) 1); |
765 Goal "Y <= A"; |
723 Goal "Y <= A"; |
766 by (rtac (fixfE1 RSN(2,subset_trans)) 1); |
724 by (rtac (fixfE1 RSN(2,subset_trans)) 1); |
767 by (rtac (thm "Y_ss") 1); |
725 by (rtac (thm "Y_ss") 1); |
768 qed "Y_subset_A"; |
726 qed "Y_subset_A"; |
769 |
727 |
770 Goal "lub Y cl : A"; |
728 Goal "lub Y cl \\<in> A"; |
771 by (afs [Y_subset_A RS lub_in_lattice] 1); |
729 by (afs [Y_subset_A RS lub_in_lattice] 1); |
772 qed "lubY_in_A"; |
730 qed "lubY_in_A"; |
773 |
731 |
774 Goal "(lub Y cl, f (lub Y cl)): r"; |
732 Goal "(lub Y cl, f (lub Y cl)) \\<in> r"; |
775 by (rtac lubE2 1); |
733 by (rtac lubE2 1); |
776 by (rtac Y_subset_A 1); |
734 by (rtac Y_subset_A 1); |
777 by (rtac (CLF_E1 RS funcset_mem) 1); |
735 by (rtac (CLF_E1 RS funcset_mem) 1); |
778 by (rtac lubY_in_A 1); |
736 by (rtac lubY_in_A 1); |
779 (* Y <= P ==> f x = x *) |
737 (* Y <= P ==> f x = x *) |
780 by (rtac ballI 1); |
738 by (rtac ballI 1); |
781 by (res_inst_tac [("t","x")] (fixfE2 RS subst) 1); |
739 by (res_inst_tac [("t","x")] (fixfE2 RS subst) 1); |
782 by (etac (thm "Y_ss" RS subsetD) 1); |
740 by (etac (thm "Y_ss" RS subsetD) 1); |
783 (* reduce (f x, f (lub Y cl)) : r to (x, lub Y cl): r by monotonicity *) |
741 (* reduce (f x, f (lub Y cl)) \\<in> r to (x, lub Y cl) \\<in> r by monotonicity *) |
784 by (res_inst_tac [("f","f")] monotoneE 1); |
742 by (res_inst_tac [("f","f")] monotoneE 1); |
785 by (rtac CLF_E2 1); |
743 by (rtac CLF_E2 1); |
786 by (afs [Y_subset_A RS subsetD] 1); |
744 by (afs [Y_subset_A RS subsetD] 1); |
787 by (rtac lubY_in_A 1); |
745 by (rtac lubY_in_A 1); |
788 by (afs [lubE1, Y_subset_A] 1); |
746 by (afs [lubE1, Y_subset_A] 1); |
794 by (rtac Top_in_lattice 1); |
752 by (rtac Top_in_lattice 1); |
795 qed "intY1_subset"; |
753 qed "intY1_subset"; |
796 |
754 |
797 val intY1_elem = intY1_subset RS subsetD; |
755 val intY1_elem = intY1_subset RS subsetD; |
798 |
756 |
799 Goal "(lam x: intY1. f x): intY1 funcset intY1"; |
757 Goal "x \\<in> intY1 \\<Longrightarrow> f x \\<in> intY1"; |
800 by (rtac restrictI 1); |
|
801 by (afs [thm "intY1_def", interval_def] 1); |
758 by (afs [thm "intY1_def", interval_def] 1); |
802 by (rtac conjI 1); |
759 by (rtac conjI 1); |
803 by (rtac transE 1); |
760 by (rtac transE 1); |
804 by (rtac CompleteLatticeE13 1); |
761 by (rtac CompleteLatticeE13 1); |
805 by (rtac lubY_le_flubY 1); |
762 by (rtac lubY_le_flubY 1); |
806 (* (f (lub Y cl), f x) : r *) |
763 (* (f (lub Y cl), f x) \\<in> r *) |
807 by (res_inst_tac [("f","f")]monotoneE 1); |
764 by (res_inst_tac [("f","f")]monotoneE 1); |
808 by (rtac CLF_E2 1); |
765 by (rtac CLF_E2 1); |
809 by (rtac lubY_in_A 1); |
766 by (rtac lubY_in_A 1); |
810 by (afs [thm "intY1_def",interval_def, intY1_elem] 1); |
767 by (afs [thm "intY1_def",interval_def, intY1_elem] 1); |
811 by (afs [thm "intY1_def", interval_def] 1); |
768 by (afs [thm "intY1_def", interval_def] 1); |
812 (* (f x, Top cl) : r *) |
769 (* (f x, Top cl) \\<in> r *) |
813 by (rtac Top_prop 1); |
770 by (rtac Top_prop 1); |
814 by (rtac (CLF_E1 RS funcset_mem) 1); |
771 by (rtac (CLF_E1 RS funcset_mem) 1); |
815 by (afs [thm "intY1_def",interval_def, intY1_elem] 1); |
772 by (afs [thm "intY1_def",interval_def, intY1_elem] 1); |
|
773 qed "intY1_f_closed"; |
|
774 |
|
775 Goal "(lam x: intY1. f x) \\<in> intY1 funcset intY1"; |
|
776 by (rtac restrictI 1); |
|
777 by (etac intY1_f_closed 1); |
816 qed "intY1_func"; |
778 qed "intY1_func"; |
817 |
779 |
818 Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)"; |
780 Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)"; |
819 by (simp_tac (simpset() addsimps [monotone_def]) 1); |
781 by (auto_tac (claset(), |
820 by (Clarify_tac 1); |
782 simpset() addsimps [monotone_def, induced_def, intY1_f_closed])); |
821 by (simp_tac (simpset() addsimps [induced_def]) 1); |
783 by (blast_tac (claset() addIs [intY1_elem, CLF_E2 RS monotoneE]) 1); |
822 by (afs [intY1_func RS funcset_mem] 1); |
|
823 by (afs [restrict_apply1] 1); |
|
824 by (res_inst_tac [("f","f")] monotoneE 1); |
|
825 by (rtac CLF_E2 1); |
|
826 by (etac (intY1_subset RS subsetD) 2); |
|
827 by (etac (intY1_subset RS subsetD) 1); |
|
828 by (afs [induced_def] 1); |
|
829 qed "intY1_mono"; |
784 qed "intY1_mono"; |
830 |
785 |
831 Goalw [thm "intY1_def"] |
786 Goalw [thm "intY1_def"] |
832 "(| pset = intY1, order = induced intY1 r |): CompleteLattice"; |
787 "(| pset = intY1, order = induced intY1 r |) \\<in> CompleteLattice"; |
833 by (rtac interv_is_compl_latt 1); |
788 by (rtac interv_is_compl_latt 1); |
834 by (rtac lubY_in_A 1); |
789 by (rtac lubY_in_A 1); |
835 by (rtac Top_in_lattice 1); |
790 by (rtac Top_in_lattice 1); |
836 by (rtac Top_intv_not_empty 1); |
791 by (rtac Top_intv_not_empty 1); |
837 by (rtac lubY_in_A 1); |
792 by (rtac lubY_in_A 1); |
838 qed "intY1_is_cl"; |
793 qed "intY1_is_cl"; |
839 |
794 |
840 Goalw [thm "P_def"] "v : P"; |
795 Goalw [thm "P_def"] "v \\<in> P"; |
841 by (res_inst_tac [("A","intY1")] fixf_subset 1); |
796 by (res_inst_tac [("A","intY1")] fixf_subset 1); |
842 by (rtac intY1_subset 1); |
797 by (rtac intY1_subset 1); |
843 by (rewrite_goals_tac [thm "v_def"]); |
798 by (rewrite_goals_tac [thm "v_def"]); |
844 by (rtac (simplify (simpset()) (intY1_is_cl RS export glbH_is_fixp)) 1); |
799 by (rtac (simplify (simpset()) (intY1_is_cl RS export glbH_is_fixp)) 1); |
845 by (afs [CLF_def, intY1_is_cl, intY1_func, intY1_mono] 1); |
800 by (afs [CLF_def, intY1_is_cl, intY1_func, intY1_mono] 1); |
846 by (Simp_tac 1); |
801 by (Simp_tac 1); |
847 qed "v_in_P"; |
802 qed "v_in_P"; |
848 |
803 |
849 Goalw [thm "intY1_def"] |
804 Goalw [thm "intY1_def"] |
850 "[| z : P; ! y:Y. (y, z) : induced P r |] ==> z : intY1"; |
805 "[| z \\<in> P; \\<forall>y\\<in>Y. (y, z) \\<in> induced P r |] ==> z \\<in> intY1"; |
851 by (rtac intervalI 1); |
806 by (rtac intervalI 1); |
852 by (etac (fixfE1 RS subsetD RS Top_prop) 2); |
807 by (etac (fixfE1 RS subsetD RS Top_prop) 2); |
853 by (rtac lubE2 1); |
808 by (rtac lubE2 1); |
854 by (rtac Y_subset_A 1); |
809 by (rtac Y_subset_A 1); |
855 by (fast_tac (claset() addSEs [fixfE1 RS subsetD]) 1); |
810 by (fast_tac (claset() addSEs [fixfE1 RS subsetD]) 1); |
857 by (dtac bspec 1); |
812 by (dtac bspec 1); |
858 by (assume_tac 1); |
813 by (assume_tac 1); |
859 by (afs [induced_def] 1); |
814 by (afs [induced_def] 1); |
860 qed "z_in_interval"; |
815 qed "z_in_interval"; |
861 |
816 |
862 Goal "[| z : P; ! y:Y. (y, z) : induced P r |]\ |
817 Goal "[| z \\<in> P; \\<forall>y\\<in>Y. (y, z) \\<in> induced P r |]\ |
863 \ ==> ((lam x: intY1. f x) z, z) : induced intY1 r"; |
818 \ ==> ((lam x: intY1. f x) z, z) \\<in> induced intY1 r"; |
864 by (afs [induced_def,intY1_func RS funcset_mem, z_in_interval] 1); |
819 by (afs [induced_def, intY1_f_closed, z_in_interval] 1); |
865 by (rtac (z_in_interval RS restrict_apply1 RS ssubst) 1); |
820 by (afs [fixfE2, fixfE1 RS subsetD, CompleteLatticeE11 RS reflE] 1); |
866 by (assume_tac 1); |
|
867 by (afs [induced_def] 1); |
|
868 by (afs [fixfE2] 1); |
|
869 by (rtac reflE 1); |
|
870 by (rtac CompleteLatticeE11 1); |
|
871 by (etac (fixfE1 RS subsetD) 1); |
|
872 qed "f'z_in_int_rel"; |
821 qed "f'z_in_int_rel"; |
873 |
822 |
874 Goal "? L. islub Y (| pset = P, order = induced P r |) L"; |
823 Goal "\\<exists>L. islub Y (| pset = P, order = induced P r |) L"; |
875 by (res_inst_tac [("x","v")] exI 1); |
824 by (res_inst_tac [("x","v")] exI 1); |
876 by (simp_tac (simpset() addsimps [islub_def]) 1); |
825 by (simp_tac (simpset() addsimps [islub_def]) 1); |
877 (* v : P *) |
826 (* v \\<in> P *) |
878 by (afs [v_in_P] 1); |
827 by (afs [v_in_P] 1); |
879 by (rtac conjI 1); |
828 by (rtac conjI 1); |
880 (* v is lub *) |
829 (* v is lub *) |
881 (* 1. ! y:Y. (y, v) : induced P r *) |
830 (* 1. \\<forall>y:Y. (y, v) \\<in> induced P r *) |
882 by (rtac ballI 1); |
831 by (rtac ballI 1); |
883 by (afs [induced_def, subsetD, v_in_P] 1); |
832 by (afs [induced_def, subsetD, v_in_P] 1); |
884 by (rtac conjI 1); |
833 by (rtac conjI 1); |
885 by (etac (thm "Y_ss" RS subsetD) 1); |
834 by (etac (thm "Y_ss" RS subsetD) 1); |
886 by (res_inst_tac [("b","lub Y cl")] transE 1); |
835 by (res_inst_tac [("b","lub Y cl")] transE 1); |
890 by (assume_tac 1); |
839 by (assume_tac 1); |
891 by (res_inst_tac [("b","Top cl")] intervalE1 1); |
840 by (res_inst_tac [("b","Top cl")] intervalE1 1); |
892 by (afs [thm "v_def"] 1); |
841 by (afs [thm "v_def"] 1); |
893 by (fold_goals_tac [thm "intY1_def"]); |
842 by (fold_goals_tac [thm "intY1_def"]); |
894 by (rtac (simplify (simpset()) (intY1_is_cl RS export glb_in_lattice)) 1); |
843 by (rtac (simplify (simpset()) (intY1_is_cl RS export glb_in_lattice)) 1); |
895 by (Simp_tac 1); |
844 by (Force_tac 1); |
896 by (rtac subsetI 1); |
|
897 by (dtac CollectD 1); |
|
898 by (etac conjunct2 1); |
|
899 (* v is LEAST ub *) |
845 (* v is LEAST ub *) |
900 by (Clarify_tac 1); |
846 by (Clarify_tac 1); |
901 by (rtac indI 1); |
847 by (rtac indI 1); |
902 by (afs [v_in_P] 2); |
848 by (afs [v_in_P] 2); |
903 by (assume_tac 2); |
849 by (assume_tac 2); |
904 by (rewrite_goals_tac [thm "v_def"]); |
850 by (rewrite_goals_tac [thm "v_def"]); |
905 by (rtac indE 1); |
851 by (rtac indE 1); |
906 by (rtac intY1_subset 2); |
852 by (rtac intY1_subset 2); |
907 by (rtac (simplify (simpset()) (intY1_is_cl RS export (glbE1 RS bspec))) 1); |
853 by (rtac (simplify (simpset()) (intY1_is_cl RS export (glbE1 RS bspec))) 1); |
908 by (Simp_tac 1); |
854 by (Force_tac 1); |
909 by (rtac subsetI 1); |
855 by (afs [induced_def, intY1_f_closed, z_in_interval] 1); |
910 by (dtac CollectD 1); |
856 by (afs [fixfE2, fixfE1 RS subsetD, CompleteLatticeE11 RS reflE] 1); |
911 by (etac conjunct2 1); |
|
912 by (afs [f'z_in_int_rel, z_in_interval] 1); |
|
913 qed "tarski_full_lemma"; |
857 qed "tarski_full_lemma"; |
914 val Tarski_full_lemma = Export tarski_full_lemma; |
858 val Tarski_full_lemma = Export tarski_full_lemma; |
915 |
859 |
916 Close_locale "Tarski"; |
860 Close_locale "Tarski"; |
917 |
861 |
918 Goal "(| pset = P, order = induced P r|) : CompleteLattice"; |
862 Goal "(| pset = P, order = induced P r|) \\<in> CompleteLattice"; |
919 by (rtac CompleteLatticeI_simp 1); |
863 by (rtac CompleteLatticeI_simp 1); |
920 by (afs [fixf_po] 1); |
864 by (afs [fixf_po] 1); |
921 by (Clarify_tac 1); |
865 by (Clarify_tac 1); |
922 by (etac Tarski_full_lemma 1); |
866 by (etac Tarski_full_lemma 1); |
923 qed "Tarski_full"; |
867 qed "Tarski_full"; |