equal
deleted
inserted
replaced
307 \ ALL x:S. ALL y:S. x<=y | y<=x |] ==> \ |
307 \ ALL x:S. ALL y:S. x<=y | y<=x |] ==> \ |
308 \ function(Union(S))"; |
308 \ function(Union(S))"; |
309 by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1); |
309 by (fast_tac (ZF_cs addSDs [bspec RS bspec]) 1); |
310 (*by (Blast_tac 1); takes too long...*) |
310 (*by (Blast_tac 1); takes too long...*) |
311 qed "function_Union"; |
311 qed "function_Union"; |
312 |
|
313 (*Nice Blast_tac benchmark. Proved in 0.3s; old tactics can't manage it!*) |
|
314 goal ZF.thy "!!S. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}"; |
|
315 by (Blast_tac 1); |
|
316 result(); |
|
317 |
312 |
318 goalw ZF.thy [Pi_def] |
313 goalw ZF.thy [Pi_def] |
319 "!!S. [| ALL f:S. EX C D. f:C->D; \ |
314 "!!S. [| ALL f:S. EX C D. f:C->D; \ |
320 \ ALL f:S. ALL y:S. f<=y | y<=f |] ==> \ |
315 \ ALL f:S. ALL y:S. f<=y | y<=f |] ==> \ |
321 \ Union(S) : domain(Union(S)) -> range(Union(S))"; |
316 \ Union(S) : domain(Union(S)) -> range(Union(S))"; |