1 (* Title: HOL/ex/set.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Cantor's Theorem; the Schroeder-Berstein Theorem. |
|
7 *) |
|
8 |
|
9 (*These two are cited in Benzmueller and Kohlhase's system description of LEO, |
|
10 CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*) |
|
11 |
|
12 Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))"; |
|
13 by (Blast_tac 1); |
|
14 qed ""; |
|
15 |
|
16 Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))"; |
|
17 by (Blast_tac 1); |
|
18 qed ""; |
|
19 |
|
20 (*trivial example of term synthesis: apparently hard for some provers!*) |
|
21 Goal "a ~= b ==> a:?X & b ~: ?X"; |
|
22 by (Blast_tac 1); |
|
23 qed ""; |
|
24 |
|
25 (** Examples for the Blast_tac paper **) |
|
26 |
|
27 (*Union-image, called Un_Union_image on equalities.ML*) |
|
28 Goal "(UN x:C. f(x) Un g(x)) = Union(f`C) Un Union(g`C)"; |
|
29 by (Blast_tac 1); |
|
30 qed ""; |
|
31 |
|
32 (*Inter-image, called Int_Inter_image on equalities.ML*) |
|
33 Goal "(INT x:C. f(x) Int g(x)) = Inter(f`C) Int Inter(g`C)"; |
|
34 by (Blast_tac 1); |
|
35 qed ""; |
|
36 |
|
37 (*Singleton I. Nice demonstration of blast_tac--and its limitations*) |
|
38 Goal "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
|
39 (*for some unfathomable reason, UNIV_I increases the search space greatly*) |
|
40 by (blast_tac (claset() delrules [UNIV_I]) 1); |
|
41 qed ""; |
|
42 |
|
43 (*Singleton II. variant of the benchmark above*) |
|
44 Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}"; |
|
45 by (blast_tac (claset() delrules [UNIV_I]) 1); |
|
46 (*just Blast_tac takes 5 seconds instead of 1*) |
|
47 qed ""; |
|
48 |
|
49 (*** A unique fixpoint theorem --- fast/best/meson all fail ***) |
|
50 |
|
51 Goal "EX! x. f(g(x))=x ==> EX! y. g(f(y))=y"; |
|
52 by (EVERY1[etac ex1E, rtac ex1I, etac arg_cong, |
|
53 rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); |
|
54 qed ""; |
|
55 |
|
56 |
|
57 (*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
|
58 |
|
59 Goal "~ (EX f:: 'a=>'a set. ALL S. EX x. f(x) = S)"; |
|
60 (*requires best-first search because it is undirectional*) |
|
61 by (Best_tac 1); |
|
62 qed "cantor1"; |
|
63 |
|
64 (*This form displays the diagonal term*) |
|
65 Goal "ALL f:: 'a=>'a set. ALL x. f(x) ~= ?S(f)"; |
|
66 by (Best_tac 1); |
|
67 uresult(); |
|
68 |
|
69 (*This form exploits the set constructs*) |
|
70 Goal "?S ~: range(f :: 'a=>'a set)"; |
|
71 by (rtac notI 1); |
|
72 by (etac rangeE 1); |
|
73 by (etac equalityCE 1); |
|
74 by (dtac CollectD 1); |
|
75 by (contr_tac 1); |
|
76 by (swap_res_tac [CollectI] 1); |
|
77 by (assume_tac 1); |
|
78 |
|
79 choplev 0; |
|
80 by (Best_tac 1); |
|
81 qed ""; |
|
82 |
|
83 |
|
84 (*** The Schroeder-Berstein Theorem ***) |
|
85 |
|
86 Goal "[| -(f`X) = g`(-X); f(a)=g(b); a:X |] ==> b:X"; |
|
87 by (Blast_tac 1); |
|
88 qed "disj_lemma"; |
|
89 |
|
90 Goal "-(f`X) = g`(-X) ==> surj(%z. if z:X then f(z) else g(z))"; |
|
91 by (asm_simp_tac (simpset() addsimps [surj_def]) 1); |
|
92 by (Blast_tac 1); |
|
93 qed "surj_if_then_else"; |
|
94 |
|
95 Goalw [inj_on_def] |
|
96 "[| inj_on f X; inj_on g (-X); -(f`X) = g`(-X); \ |
|
97 \ h = (%z. if z:X then f(z) else g(z)) |] \ |
|
98 \ ==> inj(h) & surj(h)"; |
|
99 by (asm_simp_tac (simpset() addsimps [surj_if_then_else]) 1); |
|
100 by (blast_tac (claset() addDs [disj_lemma, sym]) 1); |
|
101 qed "bij_if_then_else"; |
|
102 |
|
103 Goal "EX X. X = - (g`(- (f`X)))"; |
|
104 by (rtac exI 1); |
|
105 by (rtac lfp_unfold 1); |
|
106 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); |
|
107 qed "decomposition"; |
|
108 |
|
109 val [injf,injg] = goal (the_context ()) |
|
110 "[| inj (f:: 'a=>'b); inj (g:: 'b=>'a) |] \ |
|
111 \ ==> EX h:: 'a=>'b. inj(h) & surj(h)"; |
|
112 by (rtac (decomposition RS exE) 1); |
|
113 by (rtac exI 1); |
|
114 by (rtac bij_if_then_else 1); |
|
115 by (rtac refl 4); |
|
116 by (rtac inj_on_inv 2); |
|
117 by (rtac ([subset_UNIV, injf] MRS subset_inj_on) 1); |
|
118 (**tricky variable instantiations!**) |
|
119 by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, |
|
120 etac imageE, etac ssubst, rtac rangeI]); |
|
121 by (EVERY1 [etac ssubst, stac double_complement, |
|
122 rtac (injg RS inv_image_comp RS sym)]); |
|
123 qed "schroeder_bernstein"; |
|