equal
deleted
inserted
replaced
271 Goal "[| S <= A |] ==> ! x: S. (x,lub S cl): r"; |
271 Goal "[| S <= A |] ==> ! x: S. (x,lub S cl): r"; |
272 by (rtac exE 1); |
272 by (rtac exE 1); |
273 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
273 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
274 by (assume_tac 1); |
274 by (assume_tac 1); |
275 by (rewrite_goals_tac [lub_def,least_def]); |
275 by (rewrite_goals_tac [lub_def,least_def]); |
276 by (stac select_equality 1); |
276 by (stac some_equality 1); |
277 by (rtac conjI 1); |
277 by (rtac conjI 1); |
278 by (afs [islub_def] 2); |
278 by (afs [islub_def] 2); |
279 by (etac conjunct2 2); |
279 by (etac conjunct2 2); |
280 by (afs [islub_def] 1); |
280 by (afs [islub_def] 1); |
281 by (rtac lub_unique 1); |
281 by (rtac lub_unique 1); |
288 Goal "[| S <= A; L: A; ! x: S. (x,L): r |] ==> (lub S cl, L): r"; |
288 Goal "[| S <= A; L: A; ! x: S. (x,L): r |] ==> (lub S cl, L): r"; |
289 by (rtac exE 1); |
289 by (rtac exE 1); |
290 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
290 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
291 by (assume_tac 1); |
291 by (assume_tac 1); |
292 by (rewrite_goals_tac [lub_def,least_def]); |
292 by (rewrite_goals_tac [lub_def,least_def]); |
293 by (stac select_equality 1); |
293 by (stac some_equality 1); |
294 by (rtac conjI 1); |
294 by (rtac conjI 1); |
295 by (afs [islub_def] 2); |
295 by (afs [islub_def] 2); |
296 by (etac conjunct2 2); |
296 by (etac conjunct2 2); |
297 by (afs [islub_def] 1); |
297 by (afs [islub_def] 1); |
298 by (rtac lub_unique 1); |
298 by (rtac lub_unique 1); |
313 Goal "[| S <= A |] ==> lub S cl : A"; |
313 Goal "[| S <= A |] ==> lub S cl : A"; |
314 by (rtac exE 1); |
314 by (rtac exE 1); |
315 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
315 by (rtac (CompleteLatticeE2 RS spec RS mp) 1); |
316 by (assume_tac 1); |
316 by (assume_tac 1); |
317 by (rewrite_goals_tac [lub_def,least_def]); |
317 by (rewrite_goals_tac [lub_def,least_def]); |
318 by (stac select_equality 1); |
318 by (stac some_equality 1); |
319 by (afs [islub_def] 1); |
319 by (afs [islub_def] 1); |
320 by (afs [islub_def, thm "A_def"] 2); |
320 by (afs [islub_def, thm "A_def"] 2); |
321 by (rtac lub_unique 1); |
321 by (rtac lub_unique 1); |
322 by (afs [thm "A_def"] 1); |
322 by (afs [thm "A_def"] 1); |
323 by (afs [islub_def] 1); |
323 by (afs [islub_def] 1); |
699 by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1); |
699 by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1); |
700 qed "Bot_dual_Top"; |
700 qed "Bot_dual_Top"; |
701 |
701 |
702 Goal "Bot cl: A"; |
702 Goal "Bot cl: A"; |
703 by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1); |
703 by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1); |
704 by (rtac selectI2 1); |
704 by (rtac someI2 1); |
705 by (fold_goals_tac [thm "A_def"]); |
705 by (fold_goals_tac [thm "A_def"]); |
706 by (etac conjunct1 2); |
706 by (etac conjunct1 2); |
707 by (rtac conjI 1); |
707 by (rtac conjI 1); |
708 by (rtac glb_in_lattice 1); |
708 by (rtac glb_in_lattice 1); |
709 by (rtac subset_refl 1); |
709 by (rtac subset_refl 1); |
717 by (afs [export Bot_in_lattice,CL_dualCL] 1); |
717 by (afs [export Bot_in_lattice,CL_dualCL] 1); |
718 qed "Top_in_lattice"; |
718 qed "Top_in_lattice"; |
719 |
719 |
720 Goal "x: A ==> (x, Top cl): r"; |
720 Goal "x: A ==> (x, Top cl): r"; |
721 by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1); |
721 by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1); |
722 by (rtac selectI2 1); |
722 by (rtac someI2 1); |
723 by (fold_goals_tac [thm "r_def", thm "A_def"]); |
723 by (fold_goals_tac [thm "r_def", thm "A_def"]); |
724 by (Fast_tac 2); |
724 by (Fast_tac 2); |
725 by (rtac conjI 1); |
725 by (rtac conjI 1); |
726 by (rtac lubE1 2); |
726 by (rtac lubE1 2); |
727 by (afs [lub_in_lattice] 1); |
727 by (afs [lub_in_lattice] 1); |