|
1 (* Title: ZF/ex/llist-fn.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory |
|
7 *) |
|
8 |
|
9 open LListFn; |
|
10 |
|
11 (*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***) |
|
12 |
|
13 goalw LListFn.thy LList.con_defs "bnd_mono(univ(a), %l. LCons(a,l))"; |
|
14 by (rtac bnd_monoI 1); |
|
15 by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2)); |
|
16 by (REPEAT (ares_tac [subset_refl, A_subset_univ, |
|
17 QInr_subset_univ, QPair_subset_univ] 1)); |
|
18 val lconst_fun_bnd_mono = result(); |
|
19 |
|
20 (* lconst(a) = LCons(a,lconst(a)) *) |
|
21 val lconst = standard |
|
22 ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski); |
|
23 |
|
24 val lconst_subset = lconst_def RS def_lfp_subset; |
|
25 |
|
26 val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper); |
|
27 |
|
28 goal LListFn.thy "!!a A. a : A ==> lconst(a) : quniv(A)"; |
|
29 by (rtac (lconst_subset RS subset_trans RS qunivI) 1); |
|
30 by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1); |
|
31 val lconst_in_quniv = result(); |
|
32 |
|
33 goal LListFn.thy "!!a A. a:A ==> lconst(a): llist(A)"; |
|
34 by (rtac (singletonI RS LList.co_induct) 1); |
|
35 by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1); |
|
36 by (fast_tac (ZF_cs addSIs [lconst]) 1); |
|
37 val lconst_type = result(); |