|
1 (* Title: ZF/quniv |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 For quniv.thy. A small universe for lazy recursive types |
|
7 *) |
|
8 |
|
9 open QUniv; |
|
10 |
|
11 (** Introduction and elimination rules avoid tiresome folding/unfolding **) |
|
12 |
|
13 goalw QUniv.thy [quniv_def] |
|
14 "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)"; |
|
15 be PowI 1; |
|
16 val qunivI = result(); |
|
17 |
|
18 goalw QUniv.thy [quniv_def] |
|
19 "!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; |
|
20 be PowD 1; |
|
21 val qunivD = result(); |
|
22 |
|
23 goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)"; |
|
24 by (etac (eclose_mono RS univ_mono RS Pow_mono) 1); |
|
25 val quniv_mono = result(); |
|
26 |
|
27 (*** Closure properties ***) |
|
28 |
|
29 goalw QUniv.thy [quniv_def] "univ(eclose(A)) <= quniv(A)"; |
|
30 by (rtac (Transset_iff_Pow RS iffD1) 1); |
|
31 by (rtac (Transset_eclose RS Transset_univ) 1); |
|
32 val univ_eclose_subset_quniv = result(); |
|
33 |
|
34 goal QUniv.thy "univ(A) <= quniv(A)"; |
|
35 by (rtac (arg_subset_eclose RS univ_mono RS subset_trans) 1); |
|
36 by (rtac univ_eclose_subset_quniv 1); |
|
37 val univ_subset_quniv = result(); |
|
38 |
|
39 val univ_into_quniv = standard (univ_subset_quniv RS subsetD); |
|
40 |
|
41 goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)"; |
|
42 by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1); |
|
43 val Pow_univ_subset_quniv = result(); |
|
44 |
|
45 val univ_subset_into_quniv = standard |
|
46 (PowI RS (Pow_univ_subset_quniv RS subsetD)); |
|
47 |
|
48 val zero_in_quniv = standard (zero_in_univ RS univ_into_quniv); |
|
49 val one_in_quniv = standard (one_in_univ RS univ_into_quniv); |
|
50 val two_in_quniv = standard (two_in_univ RS univ_into_quniv); |
|
51 |
|
52 val A_subset_quniv = standard |
|
53 ([A_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
54 |
|
55 val A_into_quniv = A_subset_quniv RS subsetD; |
|
56 |
|
57 (*** univ(A) closure for Quine-inspired pairs and injections ***) |
|
58 |
|
59 (*Quine ordered pairs*) |
|
60 goalw QUniv.thy [QPair_def] |
|
61 "!!A a. [| a <= univ(A); b <= univ(A) |] ==> <a;b> <= univ(A)"; |
|
62 by (REPEAT (ares_tac [sum_subset_univ] 1)); |
|
63 val QPair_subset_univ = result(); |
|
64 |
|
65 (** Quine disjoint sum **) |
|
66 |
|
67 goalw QUniv.thy [QInl_def] "!!A a. a <= univ(A) ==> QInl(a) <= univ(A)"; |
|
68 by (etac (empty_subsetI RS QPair_subset_univ) 1); |
|
69 val QInl_subset_univ = result(); |
|
70 |
|
71 val naturals_subset_nat = |
|
72 rewrite_rule [Transset_def] (Ord_nat RS Ord_is_Transset) |
|
73 RS bspec; |
|
74 |
|
75 val naturals_subset_univ = |
|
76 [naturals_subset_nat, nat_subset_univ] MRS subset_trans; |
|
77 |
|
78 goalw QUniv.thy [QInr_def] "!!A a. a <= univ(A) ==> QInr(a) <= univ(A)"; |
|
79 by (etac (nat_1I RS naturals_subset_univ RS QPair_subset_univ) 1); |
|
80 val QInr_subset_univ = result(); |
|
81 |
|
82 (*** Closure for Quine-inspired products and sums ***) |
|
83 |
|
84 (*Quine ordered pairs*) |
|
85 goalw QUniv.thy [quniv_def,QPair_def] |
|
86 "!!A a. [| a: quniv(A); b: quniv(A) |] ==> <a;b> : quniv(A)"; |
|
87 by (REPEAT (dtac PowD 1)); |
|
88 by (REPEAT (ares_tac [PowI, sum_subset_univ] 1)); |
|
89 val QPair_in_quniv = result(); |
|
90 |
|
91 goal QUniv.thy "quniv(A) <*> quniv(A) <= quniv(A)"; |
|
92 by (REPEAT (ares_tac [subsetI, QPair_in_quniv] 1 |
|
93 ORELSE eresolve_tac [QSigmaE, ssubst] 1)); |
|
94 val QSigma_quniv = result(); |
|
95 |
|
96 val QSigma_subset_quniv = standard |
|
97 (QSigma_mono RS (QSigma_quniv RSN (2,subset_trans))); |
|
98 |
|
99 (*The opposite inclusion*) |
|
100 goalw QUniv.thy [quniv_def,QPair_def] |
|
101 "!!A a b. <a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"; |
|
102 be ([Transset_eclose RS Transset_univ, PowD] MRS |
|
103 Transset_includes_summands RS conjE) 1; |
|
104 by (REPEAT (ares_tac [conjI,PowI] 1)); |
|
105 val quniv_QPair_D = result(); |
|
106 |
|
107 val quniv_QPair_E = standard (quniv_QPair_D RS conjE); |
|
108 |
|
109 goal QUniv.thy "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"; |
|
110 by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1 |
|
111 ORELSE etac conjE 1)); |
|
112 val quniv_QPair_iff = result(); |
|
113 |
|
114 |
|
115 (** Quine disjoint sum **) |
|
116 |
|
117 goalw QUniv.thy [QInl_def] "!!A a. a: quniv(A) ==> QInl(a) : quniv(A)"; |
|
118 by (REPEAT (ares_tac [zero_in_quniv,QPair_in_quniv] 1)); |
|
119 val QInl_in_quniv = result(); |
|
120 |
|
121 goalw QUniv.thy [QInr_def] "!!A b. b: quniv(A) ==> QInr(b) : quniv(A)"; |
|
122 by (REPEAT (ares_tac [one_in_quniv, QPair_in_quniv] 1)); |
|
123 val QInr_in_quniv = result(); |
|
124 |
|
125 goal QUniv.thy "quniv(C) <+> quniv(C) <= quniv(C)"; |
|
126 by (REPEAT (ares_tac [subsetI, QInl_in_quniv, QInr_in_quniv] 1 |
|
127 ORELSE eresolve_tac [qsumE, ssubst] 1)); |
|
128 val qsum_quniv = result(); |
|
129 |
|
130 val qsum_subset_quniv = standard |
|
131 (qsum_mono RS (qsum_quniv RSN (2,subset_trans))); |
|
132 |
|
133 (*** The natural numbers ***) |
|
134 |
|
135 val nat_subset_quniv = standard |
|
136 ([nat_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
137 |
|
138 (* n:nat ==> n:quniv(A) *) |
|
139 val nat_into_quniv = standard (nat_subset_quniv RS subsetD); |
|
140 |
|
141 val bool_subset_quniv = standard |
|
142 ([bool_subset_univ, univ_subset_quniv] MRS subset_trans); |
|
143 |
|
144 val bool_into_quniv = standard (bool_subset_quniv RS subsetD); |
|
145 |
|
146 |
|
147 (**** Properties of Vfrom analogous to the "take-lemma" ****) |
|
148 |
|
149 (*** Intersecting a*b with Vfrom... ***) |
|
150 |
|
151 (*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*) |
|
152 goal Univ.thy |
|
153 "!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
|
154 \ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
|
155 bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1; |
|
156 ba 1; |
|
157 by (fast_tac ZF_cs 1); |
|
158 val doubleton_in_Vfrom_D = result(); |
|
159 |
|
160 (*This weaker version says a, b exist at the same level*) |
|
161 val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D); |
|
162 |
|
163 (** Using only the weaker theorem would prove <a,b> : Vfrom(X,i) |
|
164 implies a, b : Vfrom(X,i), which is useless for induction. |
|
165 Using only the stronger theorem would prove <a,b> : Vfrom(X,succ(succ(i))) |
|
166 implies a, b : Vfrom(X,i), leaving the succ(i) case untreated. |
|
167 The combination gives a reduction by precisely one level, which is |
|
168 most convenient for proofs. |
|
169 **) |
|
170 |
|
171 goalw Univ.thy [Pair_def] |
|
172 "!!X. [| <a,b> : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
|
173 \ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
|
174 by (fast_tac (ZF_cs addSDs [doubleton_in_Vfrom_D, Vfrom_doubleton_D]) 1); |
|
175 val Pair_in_Vfrom_D = result(); |
|
176 |
|
177 goal Univ.thy |
|
178 "!!X. Transset(X) ==> \ |
|
179 \ (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"; |
|
180 by (fast_tac (ZF_cs addSDs [Pair_in_Vfrom_D]) 1); |
|
181 val product_Int_Vfrom_subset = result(); |
|
182 |
|
183 (*** Intersecting <a;b> with Vfrom... ***) |
|
184 |
|
185 goalw QUniv.thy [QPair_def,sum_def] |
|
186 "!!X. Transset(X) ==> \ |
|
187 \ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
|
188 br (Int_Un_distrib RS ssubst) 1; |
|
189 br Un_mono 1; |
|
190 by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, |
|
191 [Int_lower1, subset_refl] MRS Sigma_mono] 1)); |
|
192 val QPair_Int_Vfrom_succ_subset = result(); |
|
193 |
|
194 (** Pairs in quniv -- for handling the base case **) |
|
195 |
|
196 goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))"; |
|
197 be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1; |
|
198 val Pair_in_quniv_D = result(); |
|
199 |
|
200 goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))"; |
|
201 br equalityI 1; |
|
202 br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2; |
|
203 by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1); |
|
204 val product_Int_quniv_eq = result(); |
|
205 |
|
206 goalw QUniv.thy [QPair_def,sum_def] |
|
207 "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))"; |
|
208 by (SIMP_TAC (ZF_ss addrews [Int_Un_distrib, product_Int_quniv_eq]) 1); |
|
209 val QPair_Int_quniv_eq = result(); |
|
210 |
|
211 (**** "Take-lemma" rules for proving c: quniv(A) ****) |
|
212 |
|
213 goalw QUniv.thy [quniv_def] "Transset(quniv(A))"; |
|
214 br (Transset_eclose RS Transset_univ RS Transset_Pow) 1; |
|
215 val Transset_quniv = result(); |
|
216 |
|
217 val [aprem, iprem] = goal QUniv.thy |
|
218 "[| a: quniv(quniv(X)); \ |
|
219 \ !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \ |
|
220 \ |] ==> a : quniv(A)"; |
|
221 br (univ_Int_Vfrom_subset RS qunivI) 1; |
|
222 br (aprem RS qunivD) 1; |
|
223 by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1); |
|
224 be (iprem RS qunivD) 1; |
|
225 val quniv_Int_Vfrom = result(); |
|
226 |
|
227 (** Rules for level 0 **) |
|
228 |
|
229 goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)"; |
|
230 br (QPair_Int_quniv_eq RS ssubst) 1; |
|
231 br (Int_lower2 RS qunivI) 1; |
|
232 val QPair_Int_quniv_in_quniv = result(); |
|
233 |
|
234 (*Unused; kept as an example. QInr rule is similar*) |
|
235 goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)"; |
|
236 br QPair_Int_quniv_in_quniv 1; |
|
237 val QInl_Int_quniv_in_quniv = result(); |
|
238 |
|
239 goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)"; |
|
240 be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1; |
|
241 val Int_quniv_in_quniv = result(); |
|
242 |
|
243 goal QUniv.thy |
|
244 "!!X. a Int X : quniv(A) ==> a Int Vfrom(X, 0) : quniv(A)"; |
|
245 by (etac (Vfrom_0 RS ssubst) 1); |
|
246 val Int_Vfrom_0_in_quniv = result(); |
|
247 |
|
248 (** Rules for level succ(i), decreasing it to i **) |
|
249 |
|
250 goal QUniv.thy |
|
251 "!!X. [| a Int Vfrom(X,i) : quniv(A); \ |
|
252 \ b Int Vfrom(X,i) : quniv(A); \ |
|
253 \ Transset(X) \ |
|
254 \ |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)"; |
|
255 br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1; |
|
256 br (QPair_in_quniv RS qunivD) 2; |
|
257 by (REPEAT (assume_tac 1)); |
|
258 val QPair_Int_Vfrom_succ_in_quniv = result(); |
|
259 |
|
260 val zero_Int_in_quniv = standard |
|
261 ([Int_lower1,empty_subsetI] MRS subset_trans RS qunivI); |
|
262 |
|
263 val one_Int_in_quniv = standard |
|
264 ([Int_lower1, one_in_quniv RS qunivD] MRS subset_trans RS qunivI); |
|
265 |
|
266 (*Unused; kept as an example. QInr rule is similar*) |
|
267 goalw QUniv.thy [QInl_def] |
|
268 "!!X. [| a Int Vfrom(X,i) : quniv(A); Transset(X) \ |
|
269 \ |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)"; |
|
270 br QPair_Int_Vfrom_succ_in_quniv 1; |
|
271 by (REPEAT (ares_tac [zero_Int_in_quniv] 1)); |
|
272 val QInl_Int_Vfrom_succ_in_quniv = result(); |
|
273 |
|
274 (** Rules for level i -- preserving the level, not decreasing it **) |
|
275 |
|
276 goalw QUniv.thy [QPair_def] |
|
277 "!!X. Transset(X) ==> \ |
|
278 \ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
|
279 be (Transset_Vfrom RS Transset_sum_Int_subset) 1; |
|
280 val QPair_Int_Vfrom_subset = result(); |
|
281 |
|
282 goal QUniv.thy |
|
283 "!!X. [| a Int Vfrom(X,i) : quniv(A); \ |
|
284 \ b Int Vfrom(X,i) : quniv(A); \ |
|
285 \ Transset(X) \ |
|
286 \ |] ==> <a;b> Int Vfrom(X,i) : quniv(A)"; |
|
287 br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1; |
|
288 br (QPair_in_quniv RS qunivD) 2; |
|
289 by (REPEAT (assume_tac 1)); |
|
290 val QPair_Int_Vfrom_in_quniv = result(); |
|
291 |
|
292 |
|
293 (**** "Take-lemma" rules for proving a=b by co-induction ****) |
|
294 |
|
295 (** Unfortunately, the technique used above does not apply here, since |
|
296 the base case appears impossible to prove: it involves an intersection |
|
297 with eclose(X) for arbitrary X. So a=b is proved by transfinite induction |
|
298 over ALL ordinals, using Vset(i) instead of Vfrom(X,i). |
|
299 **) |
|
300 |
|
301 (*Rule for level 0*) |
|
302 goal QUniv.thy "a Int Vset(0) <= b"; |
|
303 by (rtac (Vfrom_0 RS ssubst) 1); |
|
304 by (fast_tac ZF_cs 1); |
|
305 val Int_Vset_0_subset = result(); |
|
306 |
|
307 (*Rule for level succ(i), decreasing it to i*) |
|
308 goal QUniv.thy |
|
309 "!!i. [| a Int Vset(i) <= c; \ |
|
310 \ b Int Vset(i) <= d \ |
|
311 \ |] ==> <a;b> Int Vset(succ(i)) <= <c;d>"; |
|
312 br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] |
|
313 MRS subset_trans) 1; |
|
314 by (REPEAT (assume_tac 1)); |
|
315 val QPair_Int_Vset_succ_subset_trans = result(); |
|
316 |
|
317 (*Unused; kept as an example. QInr rule is similar*) |
|
318 goalw QUniv.thy [QInl_def] |
|
319 "!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)"; |
|
320 be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1; |
|
321 val QInl_Int_Vset_succ_subset_trans = result(); |
|
322 |
|
323 (*Rule for level i -- preserving the level, not decreasing it*) |
|
324 goal QUniv.thy |
|
325 "!!i. [| a Int Vset(i) <= c; \ |
|
326 \ b Int Vset(i) <= d \ |
|
327 \ |] ==> <a;b> Int Vset(i) <= <c;d>"; |
|
328 br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] |
|
329 MRS subset_trans) 1; |
|
330 by (REPEAT (assume_tac 1)); |
|
331 val QPair_Int_Vset_subset_trans = result(); |
|
332 |
|
333 |
|
334 |