author | lcp |
Thu, 07 Oct 1993 11:47:50 +0100 | |
changeset 38 | 4433428596f9 |
parent 16 | 0b033d50ca1c |
child 434 | 89d45187f04d |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/ex/misc |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Miscellaneous examples for Zermelo-Fraenkel Set Theory |
|
7 |
Cantor's Theorem; Schroeder-Bernstein Theorem; Composition of homomorphisms... |
|
8 |
*) |
|
9 |
||
10 |
writeln"ZF/ex/misc"; |
|
11 |
||
12 |
||
13 |
(*Example 12 (credited to Peter Andrews) from |
|
14 |
W. Bledsoe. A Maximal Method for Set Variables in Automatic Theorem-proving. |
|
15 |
In: J. Hayes and D. Michie and L. Mikulich, eds. Machine Intelligence 9. |
|
16 |
Ellis Horwood, 53-100 (1979). *) |
|
17 |
goal ZF.thy "(ALL F. {x}: F --> {y}:F) --> (ALL A. x:A --> y:A)"; |
|
18 |
by (best_tac ZF_cs 1); |
|
19 |
result(); |
|
20 |
||
21 |
||
22 |
(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) |
|
23 |
||
24 |
val cantor_cs = FOL_cs (*precisely the rules needed for the proof*) |
|
25 |
addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI] |
|
26 |
addSEs [CollectE, equalityCE]; |
|
27 |
||
28 |
(*The search is undirected and similar proof attempts fail*) |
|
38 | 29 |
goal ZF.thy "ALL f: A->Pow(A). EX S: Pow(A). ALL x:A. f`x ~= S"; |
0 | 30 |
by (best_tac cantor_cs 1); |
31 |
result(); |
|
32 |
||
38 | 33 |
(*This form displays the diagonal term, {x: A . x ~: f`x} *) |
0 | 34 |
val [prem] = goal ZF.thy |
38 | 35 |
"f: A->Pow(A) ==> (ALL x:A. f`x ~= ?S) & ?S: Pow(A)"; |
0 | 36 |
by (best_tac cantor_cs 1); |
37 |
result(); |
|
38 |
||
39 |
(*yet another version...*) |
|
38 | 40 |
goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))"; |
0 | 41 |
by (safe_tac ZF_cs); |
42 |
by (etac ballE 1); |
|
43 |
by (best_tac (cantor_cs addSEs [bexE]) 1); |
|
44 |
by (fast_tac ZF_cs 1); |
|
45 |
result(); |
|
46 |
||
47 |
||
48 |
(**** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ****) |
|
49 |
||
50 |
val SB_thy = merge_theories (Fixedpt.thy, Perm.thy); |
|
51 |
||
52 |
(** Lemma: Banach's Decomposition Theorem **) |
|
53 |
||
54 |
goal SB_thy "bnd_mono(X, %W. X - g``(Y - f``W))"; |
|
55 |
by (rtac bnd_monoI 1); |
|
56 |
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); |
|
57 |
val decomp_bnd_mono = result(); |
|
58 |
||
59 |
val [gfun] = goal SB_thy |
|
60 |
"g: Y->X ==> \ |
|
61 |
\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ |
|
62 |
\ X - lfp(X, %W. X - g``(Y - f``W)) "; |
|
63 |
by (res_inst_tac [("P", "%u. ?v = X-u")] |
|
64 |
(decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); |
|
16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
65 |
by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, |
0 | 66 |
gfun RS fun_is_rel RS image_subset]) 1); |
67 |
val Banach_last_equation = result(); |
|
68 |
||
69 |
val prems = goal SB_thy |
|
70 |
"[| f: X->Y; g: Y->X |] ==> \ |
|
71 |
\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ |
|
72 |
\ (YA Int YB = 0) & (YA Un YB = Y) & \ |
|
73 |
\ f``XA=YA & g``YB=XB"; |
|
74 |
by (REPEAT |
|
75 |
(FIRSTGOAL |
|
76 |
(resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); |
|
77 |
by (rtac Banach_last_equation 3); |
|
78 |
by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); |
|
79 |
val decomposition = result(); |
|
80 |
||
81 |
val prems = goal SB_thy |
|
82 |
"[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"; |
|
83 |
by (cut_facts_tac prems 1); |
|
84 |
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); |
|
85 |
by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] |
|
86 |
addIs [bij_converse_bij]) 1); |
|
87 |
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" |
|
88 |
is forced by the context!! *) |
|
89 |
val schroeder_bernstein = result(); |
|
90 |
||
91 |
||
92 |
(*** Composition of homomorphisms is a homomorphism ***) |
|
93 |
||
94 |
(*Given as a challenge problem in |
|
95 |
R. Boyer et al., |
|
96 |
Set Theory in First-Order Logic: Clauses for G\"odel's Axioms, |
|
97 |
JAR 2 (1986), 287-327 |
|
98 |
*) |
|
99 |
||
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
100 |
(*collecting the relevant lemmas*) |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
101 |
val hom_ss = ZF_ss addsimps [comp_func,comp_func_apply,SigmaI,apply_funtype]; |
0 | 102 |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
103 |
(*The problem below is proving conditions of rewrites such as comp_func_apply; |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
104 |
rewriting does not instantiate Vars; we must prove the conditions |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
105 |
explicitly.*) |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
106 |
fun hom_tac hyps = |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
107 |
resolve_tac (TrueI::refl::iff_refl::hyps) ORELSE' |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
108 |
(cut_facts_tac hyps THEN' fast_tac prop_cs); |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
109 |
|
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
110 |
(*This version uses a super application of simp_tac*) |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
111 |
goal Perm.thy |
0 | 112 |
"(ALL A f B g. hom(A,f,B,g) = \ |
113 |
\ {H: A->B. f:A*A->A & g:B*B->B & \ |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
114 |
\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \ |
0 | 115 |
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \ |
116 |
\ (K O J) : hom(A,f,C,h)"; |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
117 |
by (simp_tac (hom_ss setsolver hom_tac) 1); |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
118 |
(*Also works but slower: |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
119 |
by (asm_simp_tac (hom_ss setloop (K (safe_tac FOL_cs))) 1); *) |
0 | 120 |
val comp_homs = result(); |
121 |
||
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
122 |
(*This version uses meta-level rewriting, safe_tac and asm_simp_tac*) |
0 | 123 |
val [hom_def] = goal Perm.thy |
124 |
"(!! A f B g. hom(A,f,B,g) == \ |
|
125 |
\ {H: A->B. f:A*A->A & g:B*B->B & \ |
|
126 |
\ (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \ |
|
127 |
\ J : hom(A,f,B,g) & K : hom(B,g,C,h) --> \ |
|
128 |
\ (K O J) : hom(A,f,C,h)"; |
|
129 |
by (rewtac hom_def); |
|
130 |
by (safe_tac ZF_cs); |
|
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
131 |
by (asm_simp_tac hom_ss 1); |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
132 |
by (asm_simp_tac hom_ss 1); |
0 | 133 |
val comp_homs = result(); |
134 |
||
135 |
||
136 |
(** A characterization of functions, suggested by Tobias Nipkow **) |
|
137 |
||
138 |
goalw ZF.thy [Pi_def] |
|
139 |
"r: domain(r)->B <-> r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)"; |
|
140 |
by (safe_tac ZF_cs); |
|
141 |
by (fast_tac (ZF_cs addSDs [bspec RS ex1_equalsE]) 1); |
|
142 |
by (eres_inst_tac [("x", "{y}")] allE 1); |
|
143 |
by (fast_tac ZF_cs 1); |
|
144 |
result(); |
|
145 |
||
146 |
||
147 |
(**** From D Pastre. Automatic theorem proving in set theory. |
|
148 |
Artificial Intelligence, 10:1--27, 1978. |
|
149 |
These examples require forward reasoning! ****) |
|
150 |
||
151 |
(*reduce the clauses to units by type checking -- beware of nontermination*) |
|
152 |
fun forw_typechk tyrls [] = [] |
|
153 |
| forw_typechk tyrls clauses = |
|
154 |
let val (units, others) = partition (has_fewer_prems 1) clauses |
|
155 |
in gen_union eq_thm (units, forw_typechk tyrls (tyrls RL others)) |
|
156 |
end; |
|
157 |
||
158 |
(*A crude form of forward reasoning*) |
|
159 |
fun forw_iterate tyrls rls facts 0 = facts |
|
160 |
| forw_iterate tyrls rls facts n = |
|
161 |
let val facts' = |
|
162 |
gen_union eq_thm (forw_typechk (tyrls@facts) (facts RL rls), facts); |
|
163 |
in forw_iterate tyrls rls facts' (n-1) end; |
|
164 |
||
165 |
val pastre_rls = |
|
166 |
[comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2]; |
|
167 |
||
168 |
fun pastre_facts (fact1::fact2::fact3::prems) = |
|
169 |
forw_iterate (prems @ [comp_surj, comp_inj, comp_func]) |
|
170 |
pastre_rls [fact1,fact2,fact3] 4; |
|
171 |
||
172 |
val prems = goalw Perm.thy [bij_def] |
|
173 |
"[| (h O g O f): inj(A,A); \ |
|
174 |
\ (f O h O g): surj(B,B); \ |
|
175 |
\ (g O f O h): surj(C,C); \ |
|
176 |
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
|
177 |
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
|
178 |
val pastre1 = result(); |
|
179 |
||
180 |
val prems = goalw Perm.thy [bij_def] |
|
181 |
"[| (h O g O f): surj(A,A); \ |
|
182 |
\ (f O h O g): inj(B,B); \ |
|
183 |
\ (g O f O h): surj(C,C); \ |
|
184 |
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
|
185 |
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
|
186 |
val pastre2 = result(); |
|
187 |
||
188 |
val prems = goalw Perm.thy [bij_def] |
|
189 |
"[| (h O g O f): surj(A,A); \ |
|
190 |
\ (f O h O g): surj(B,B); \ |
|
191 |
\ (g O f O h): inj(C,C); \ |
|
192 |
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
|
193 |
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
|
194 |
val pastre3 = result(); |
|
195 |
||
196 |
val prems = goalw Perm.thy [bij_def] |
|
197 |
"[| (h O g O f): surj(A,A); \ |
|
198 |
\ (f O h O g): inj(B,B); \ |
|
199 |
\ (g O f O h): inj(C,C); \ |
|
200 |
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
|
201 |
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
|
202 |
val pastre4 = result(); |
|
203 |
||
204 |
val prems = goalw Perm.thy [bij_def] |
|
205 |
"[| (h O g O f): inj(A,A); \ |
|
206 |
\ (f O h O g): surj(B,B); \ |
|
207 |
\ (g O f O h): inj(C,C); \ |
|
208 |
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
|
209 |
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
|
210 |
val pastre5 = result(); |
|
211 |
||
212 |
val prems = goalw Perm.thy [bij_def] |
|
213 |
"[| (h O g O f): inj(A,A); \ |
|
214 |
\ (f O h O g): inj(B,B); \ |
|
215 |
\ (g O f O h): surj(C,C); \ |
|
216 |
\ f: A->B; g: B->C; h: C->A |] ==> h: bij(C,A)"; |
|
217 |
by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1)); |
|
218 |
val pastre6 = result(); |
|
219 |
||
7
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
220 |
(** Yet another example... **) |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
221 |
|
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
222 |
goalw (merge_theories(Sum.thy,Perm.thy)) [bij_def,inj_def,surj_def] |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
223 |
"(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \ |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
224 |
\ : bij(Pow(A+B), Pow(A)*Pow(B))"; |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
225 |
by (DO_GOAL |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
226 |
[rtac IntI, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
227 |
DO_GOAL |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
228 |
[rtac CollectI, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
229 |
fast_tac (ZF_cs addSIs [lam_type]), |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
230 |
simp_tac ZF_ss, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
231 |
fast_tac (eq_cs addSEs [sumE] |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
232 |
addEs [equalityD1 RS subsetD RS CollectD2, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
233 |
equalityD2 RS subsetD RS CollectD2])], |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
234 |
DO_GOAL |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
235 |
[rtac CollectI, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
236 |
fast_tac (ZF_cs addSIs [lam_type]), |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
237 |
simp_tac ZF_ss, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
238 |
K(safe_tac ZF_cs), |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
239 |
res_inst_tac [("x", "{Inl(u). u: ?U} Un {Inr(v). v: ?V}")] bexI, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
240 |
DO_GOAL |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
241 |
[res_inst_tac [("t", "Pair")] subst_context2, |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
242 |
fast_tac (sum_cs addSIs [equalityI]), |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
243 |
fast_tac (sum_cs addSIs [equalityI])], |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
244 |
DO_GOAL [fast_tac sum_cs]]] 1); |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
245 |
val Pow_bij = result(); |
268f93ab3bc4
Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp
parents:
0
diff
changeset
|
246 |
|
0 | 247 |
writeln"Reached end of file."; |