10 |
10 |
11 (** Introduction and elimination rules avoid tiresome folding/unfolding **) |
11 (** Introduction and elimination rules avoid tiresome folding/unfolding **) |
12 |
12 |
13 goalw QUniv.thy [quniv_def] |
13 goalw QUniv.thy [quniv_def] |
14 "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)"; |
14 "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)"; |
15 be PowI 1; |
15 by (etac PowI 1); |
16 val qunivI = result(); |
16 val qunivI = result(); |
17 |
17 |
18 goalw QUniv.thy [quniv_def] |
18 goalw QUniv.thy [quniv_def] |
19 "!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; |
19 "!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; |
20 be PowD 1; |
20 by (etac PowD 1); |
21 val qunivD = result(); |
21 val qunivD = result(); |
22 |
22 |
23 goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)"; |
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); |
24 by (etac (eclose_mono RS univ_mono RS Pow_mono) 1); |
25 val quniv_mono = result(); |
25 val quniv_mono = result(); |
150 |
150 |
151 (*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*) |
151 (*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*) |
152 goal Univ.thy |
152 goal Univ.thy |
153 "!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
153 "!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \ |
154 \ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
154 \ a: Vfrom(X,i) & b: Vfrom(X,i)"; |
155 bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1; |
155 by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1); |
156 ba 1; |
156 by (assume_tac 1); |
157 by (fast_tac ZF_cs 1); |
157 by (fast_tac ZF_cs 1); |
158 val doubleton_in_Vfrom_D = result(); |
158 val doubleton_in_Vfrom_D = result(); |
159 |
159 |
160 (*This weaker version says a, b exist at the same level*) |
160 (*This weaker version says a, b exist at the same level*) |
161 val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D); |
161 val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D); |
183 (*** Intersecting <a;b> with Vfrom... ***) |
183 (*** Intersecting <a;b> with Vfrom... ***) |
184 |
184 |
185 goalw QUniv.thy [QPair_def,sum_def] |
185 goalw QUniv.thy [QPair_def,sum_def] |
186 "!!X. Transset(X) ==> \ |
186 "!!X. Transset(X) ==> \ |
187 \ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
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; |
188 by (rtac (Int_Un_distrib RS ssubst) 1); |
189 br Un_mono 1; |
189 by (rtac Un_mono 1); |
190 by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, |
190 by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, |
191 [Int_lower1, subset_refl] MRS Sigma_mono] 1)); |
191 [Int_lower1, subset_refl] MRS Sigma_mono] 1)); |
192 val QPair_Int_Vfrom_succ_subset = result(); |
192 val QPair_Int_Vfrom_succ_subset = result(); |
193 |
193 |
194 (** Pairs in quniv -- for handling the base case **) |
194 (** Pairs in quniv -- for handling the base case **) |
195 |
195 |
196 goal QUniv.thy "!!X. <a,b> : quniv(X) ==> <a,b> : univ(eclose(X))"; |
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; |
197 by (etac ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1); |
198 val Pair_in_quniv_D = result(); |
198 val Pair_in_quniv_D = result(); |
199 |
199 |
200 goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))"; |
200 goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))"; |
201 br equalityI 1; |
201 by (rtac equalityI 1); |
202 br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2; |
202 by (rtac ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2); |
203 by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1); |
203 by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1); |
204 val product_Int_quniv_eq = result(); |
204 val product_Int_quniv_eq = result(); |
205 |
205 |
206 goalw QUniv.thy [QPair_def,sum_def] |
206 goalw QUniv.thy [QPair_def,sum_def] |
207 "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))"; |
207 "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))"; |
209 val QPair_Int_quniv_eq = result(); |
209 val QPair_Int_quniv_eq = result(); |
210 |
210 |
211 (**** "Take-lemma" rules for proving c: quniv(A) ****) |
211 (**** "Take-lemma" rules for proving c: quniv(A) ****) |
212 |
212 |
213 goalw QUniv.thy [quniv_def] "Transset(quniv(A))"; |
213 goalw QUniv.thy [quniv_def] "Transset(quniv(A))"; |
214 br (Transset_eclose RS Transset_univ RS Transset_Pow) 1; |
214 by (rtac (Transset_eclose RS Transset_univ RS Transset_Pow) 1); |
215 val Transset_quniv = result(); |
215 val Transset_quniv = result(); |
216 |
216 |
217 val [aprem, iprem] = goal QUniv.thy |
217 val [aprem, iprem] = goal QUniv.thy |
218 "[| a: quniv(quniv(X)); \ |
218 "[| a: quniv(quniv(X)); \ |
219 \ !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \ |
219 \ !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \ |
220 \ |] ==> a : quniv(A)"; |
220 \ |] ==> a : quniv(A)"; |
221 br (univ_Int_Vfrom_subset RS qunivI) 1; |
221 by (rtac (univ_Int_Vfrom_subset RS qunivI) 1); |
222 br (aprem RS qunivD) 1; |
222 by (rtac (aprem RS qunivD) 1); |
223 by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1); |
223 by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1); |
224 be (iprem RS qunivD) 1; |
224 by (etac (iprem RS qunivD) 1); |
225 val quniv_Int_Vfrom = result(); |
225 val quniv_Int_Vfrom = result(); |
226 |
226 |
227 (** Rules for level 0 **) |
227 (** Rules for level 0 **) |
228 |
228 |
229 goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)"; |
229 goal QUniv.thy "<a;b> Int quniv(A) : quniv(A)"; |
230 br (QPair_Int_quniv_eq RS ssubst) 1; |
230 by (rtac (QPair_Int_quniv_eq RS ssubst) 1); |
231 br (Int_lower2 RS qunivI) 1; |
231 by (rtac (Int_lower2 RS qunivI) 1); |
232 val QPair_Int_quniv_in_quniv = result(); |
232 val QPair_Int_quniv_in_quniv = result(); |
233 |
233 |
234 (*Unused; kept as an example. QInr rule is similar*) |
234 (*Unused; kept as an example. QInr rule is similar*) |
235 goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)"; |
235 goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)"; |
236 br QPair_Int_quniv_in_quniv 1; |
236 by (rtac QPair_Int_quniv_in_quniv 1); |
237 val QInl_Int_quniv_in_quniv = result(); |
237 val QInl_Int_quniv_in_quniv = result(); |
238 |
238 |
239 goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)"; |
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; |
240 by (etac ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1); |
241 val Int_quniv_in_quniv = result(); |
241 val Int_quniv_in_quniv = result(); |
242 |
242 |
243 goal QUniv.thy |
243 goal QUniv.thy |
244 "!!X. a Int X : quniv(A) ==> a Int Vfrom(X, 0) : quniv(A)"; |
244 "!!X. a Int X : quniv(A) ==> a Int Vfrom(X, 0) : quniv(A)"; |
245 by (etac (Vfrom_0 RS ssubst) 1); |
245 by (etac (Vfrom_0 RS ssubst) 1); |
250 goal QUniv.thy |
250 goal QUniv.thy |
251 "!!X. [| a Int Vfrom(X,i) : quniv(A); \ |
251 "!!X. [| a Int Vfrom(X,i) : quniv(A); \ |
252 \ b Int Vfrom(X,i) : quniv(A); \ |
252 \ b Int Vfrom(X,i) : quniv(A); \ |
253 \ Transset(X) \ |
253 \ Transset(X) \ |
254 \ |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)"; |
254 \ |] ==> <a;b> Int Vfrom(X, succ(i)) : quniv(A)"; |
255 br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1; |
255 by (rtac (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1); |
256 br (QPair_in_quniv RS qunivD) 2; |
256 by (rtac (QPair_in_quniv RS qunivD) 2); |
257 by (REPEAT (assume_tac 1)); |
257 by (REPEAT (assume_tac 1)); |
258 val QPair_Int_Vfrom_succ_in_quniv = result(); |
258 val QPair_Int_Vfrom_succ_in_quniv = result(); |
259 |
259 |
260 val zero_Int_in_quniv = standard |
260 val zero_Int_in_quniv = standard |
261 ([Int_lower1,empty_subsetI] MRS subset_trans RS qunivI); |
261 ([Int_lower1,empty_subsetI] MRS subset_trans RS qunivI); |
265 |
265 |
266 (*Unused; kept as an example. QInr rule is similar*) |
266 (*Unused; kept as an example. QInr rule is similar*) |
267 goalw QUniv.thy [QInl_def] |
267 goalw QUniv.thy [QInl_def] |
268 "!!X. [| a Int Vfrom(X,i) : quniv(A); Transset(X) \ |
268 "!!X. [| a Int Vfrom(X,i) : quniv(A); Transset(X) \ |
269 \ |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)"; |
269 \ |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)"; |
270 br QPair_Int_Vfrom_succ_in_quniv 1; |
270 by (rtac QPair_Int_Vfrom_succ_in_quniv 1); |
271 by (REPEAT (ares_tac [zero_Int_in_quniv] 1)); |
271 by (REPEAT (ares_tac [zero_Int_in_quniv] 1)); |
272 val QInl_Int_Vfrom_succ_in_quniv = result(); |
272 val QInl_Int_Vfrom_succ_in_quniv = result(); |
273 |
273 |
274 (** Rules for level i -- preserving the level, not decreasing it **) |
274 (** Rules for level i -- preserving the level, not decreasing it **) |
275 |
275 |
276 goalw QUniv.thy [QPair_def] |
276 goalw QUniv.thy [QPair_def] |
277 "!!X. Transset(X) ==> \ |
277 "!!X. Transset(X) ==> \ |
278 \ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"; |
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; |
279 by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); |
280 val QPair_Int_Vfrom_subset = result(); |
280 val QPair_Int_Vfrom_subset = result(); |
281 |
281 |
282 goal QUniv.thy |
282 goal QUniv.thy |
283 "!!X. [| a Int Vfrom(X,i) : quniv(A); \ |
283 "!!X. [| a Int Vfrom(X,i) : quniv(A); \ |
284 \ b Int Vfrom(X,i) : quniv(A); \ |
284 \ b Int Vfrom(X,i) : quniv(A); \ |
285 \ Transset(X) \ |
285 \ Transset(X) \ |
286 \ |] ==> <a;b> Int Vfrom(X,i) : quniv(A)"; |
286 \ |] ==> <a;b> Int Vfrom(X,i) : quniv(A)"; |
287 br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1; |
287 by (rtac (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1); |
288 br (QPair_in_quniv RS qunivD) 2; |
288 by (rtac (QPair_in_quniv RS qunivD) 2); |
289 by (REPEAT (assume_tac 1)); |
289 by (REPEAT (assume_tac 1)); |
290 val QPair_Int_Vfrom_in_quniv = result(); |
290 val QPair_Int_Vfrom_in_quniv = result(); |
291 |
291 |
292 |
292 |
293 (**** "Take-lemma" rules for proving a=b by co-induction ****) |
293 (**** "Take-lemma" rules for proving a=b by co-induction ****) |
307 (*Rule for level succ(i), decreasing it to i*) |
307 (*Rule for level succ(i), decreasing it to i*) |
308 goal QUniv.thy |
308 goal QUniv.thy |
309 "!!i. [| a Int Vset(i) <= c; \ |
309 "!!i. [| a Int Vset(i) <= c; \ |
310 \ b Int Vset(i) <= d \ |
310 \ b Int Vset(i) <= d \ |
311 \ |] ==> <a;b> Int Vset(succ(i)) <= <c;d>"; |
311 \ |] ==> <a;b> Int Vset(succ(i)) <= <c;d>"; |
312 br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] |
312 by (rtac ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] |
313 MRS subset_trans) 1; |
313 MRS subset_trans) 1); |
314 by (REPEAT (assume_tac 1)); |
314 by (REPEAT (assume_tac 1)); |
315 val QPair_Int_Vset_succ_subset_trans = result(); |
315 val QPair_Int_Vset_succ_subset_trans = result(); |
316 |
316 |
317 (*Unused; kept as an example. QInr rule is similar*) |
317 (*Unused; kept as an example. QInr rule is similar*) |
318 goalw QUniv.thy [QInl_def] |
318 goalw QUniv.thy [QInl_def] |
319 "!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)"; |
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; |
320 by (etac (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1); |
321 val QInl_Int_Vset_succ_subset_trans = result(); |
321 val QInl_Int_Vset_succ_subset_trans = result(); |
322 |
322 |
323 (*Rule for level i -- preserving the level, not decreasing it*) |
323 (*Rule for level i -- preserving the level, not decreasing it*) |
324 goal QUniv.thy |
324 goal QUniv.thy |
325 "!!i. [| a Int Vset(i) <= c; \ |
325 "!!i. [| a Int Vset(i) <= c; \ |
326 \ b Int Vset(i) <= d \ |
326 \ b Int Vset(i) <= d \ |
327 \ |] ==> <a;b> Int Vset(i) <= <c;d>"; |
327 \ |] ==> <a;b> Int Vset(i) <= <c;d>"; |
328 br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] |
328 by (rtac ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] |
329 MRS subset_trans) 1; |
329 MRS subset_trans) 1); |
330 by (REPEAT (assume_tac 1)); |
330 by (REPEAT (assume_tac 1)); |
331 val QPair_Int_Vset_subset_trans = result(); |
331 val QPair_Int_Vset_subset_trans = result(); |
332 |
332 |
333 |
333 |
334 |
334 |