1 (* Title: ZF/ex/llist.ML |
1 (* Title: ZF/ex/LList.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Codatatype definition of Lazy Lists |
6 Codatatype definition of Lazy Lists |
7 *) |
7 *) |
8 |
8 |
9 structure LList = CoDatatype_Fun |
9 open LList; |
10 (val thy = QUniv.thy |
|
11 val thy_name = "LList" |
|
12 val rec_specs = [("llist", "quniv(A)", |
|
13 [(["LNil"], "i", NoSyn), |
|
14 (["LCons"], "[i,i]=>i", NoSyn)])] |
|
15 val rec_styp = "i=>i" |
|
16 val sintrs = ["LNil : llist(A)", |
|
17 "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"] |
|
18 val monos = [] |
|
19 val type_intrs = codatatype_intrs |
|
20 val type_elims = codatatype_elims); |
|
21 |
|
22 val [LNilI, LConsI] = LList.intrs; |
|
23 |
10 |
24 (*An elimination rule, for type-checking*) |
11 (*An elimination rule, for type-checking*) |
25 val LConsE = LList.mk_cases LList.con_defs "LCons(a,l) : llist(A)"; |
12 val LConsE = llist.mk_cases llist.con_defs "LCons(a,l) : llist(A)"; |
26 |
13 |
27 (*Proving freeness results*) |
14 (*Proving freeness results*) |
28 val LCons_iff = LList.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
15 val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
29 val LNil_LCons_iff = LList.mk_free "~ LNil=LCons(a,l)"; |
16 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)"; |
30 |
17 |
31 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))"; |
18 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))"; |
32 by (rtac (LList.unfold RS trans) 1); |
19 by (rtac (llist.unfold RS trans) 1); |
33 bws LList.con_defs; |
20 bws llist.con_defs; |
34 by (fast_tac (qsum_cs addIs ([equalityI] @ codatatype_intrs) |
21 br equalityI 1; |
35 addDs [LList.dom_subset RS subsetD] |
22 by (fast_tac qsum_cs 1); |
36 addEs [A_into_quniv] |
23 by (fast_tac (qsum_cs addIs codatatype_intrs |
37 addSEs [QSigmaE]) 1); |
24 addDs [llist.dom_subset RS subsetD] |
|
25 addSEs [QSigmaE]) 1); |
38 val llist_unfold = result(); |
26 val llist_unfold = result(); |
39 |
27 |
40 (*** Lemmas to justify using "llist" in other recursive type definitions ***) |
28 (*** Lemmas to justify using "llist" in other recursive type definitions ***) |
41 |
29 |
42 goalw LList.thy LList.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; |
30 goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; |
43 by (rtac gfp_mono 1); |
31 by (rtac gfp_mono 1); |
44 by (REPEAT (rtac LList.bnd_mono 1)); |
32 by (REPEAT (rtac llist.bnd_mono 1)); |
45 by (REPEAT (ares_tac (quniv_mono::basic_monos) 1)); |
33 by (REPEAT (ares_tac (quniv_mono::basic_monos) 1)); |
46 val llist_mono = result(); |
34 val llist_mono = result(); |
47 |
35 |
48 (** Closure of quniv(A) under llist -- why so complex? Its a gfp... **) |
36 (** Closure of quniv(A) under llist -- why so complex? Its a gfp... **) |
49 |
37 |
74 val llist_quniv = result(); |
62 val llist_quniv = result(); |
75 |
63 |
76 val llist_subset_quniv = standard |
64 val llist_subset_quniv = standard |
77 (llist_mono RS (llist_quniv RSN (2,subset_trans))); |
65 (llist_mono RS (llist_quniv RSN (2,subset_trans))); |
78 |
66 |
79 (* Definition and use of LList_Eq has been moved to llist_eq.ML to allow |
67 |
80 automatic association between theory name and filename. *) |
68 (*** Lazy List Equality: lleq ***) |
|
69 |
|
70 val lleq_cs = subset_cs |
|
71 addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono] |
|
72 addSEs [Ord_in_Ord, Pair_inject]; |
|
73 |
|
74 (*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*) |
|
75 goal LList.thy |
|
76 "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'"; |
|
77 by (etac trans_induct 1); |
|
78 by (REPEAT (resolve_tac [allI, impI] 1)); |
|
79 by (etac lleq.elim 1); |
|
80 by (rewrite_goals_tac (QInr_def::llist.con_defs)); |
|
81 by (safe_tac lleq_cs); |
|
82 by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1); |
|
83 val lleq_Int_Vset_subset_lemma = result(); |
|
84 |
|
85 val lleq_Int_Vset_subset = standard |
|
86 (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); |
|
87 |
|
88 |
|
89 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) |
|
90 val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)"; |
|
91 by (rtac (prem RS converseI RS lleq.coinduct) 1); |
|
92 by (rtac (lleq.dom_subset RS converse_type) 1); |
|
93 by (safe_tac converse_cs); |
|
94 by (etac lleq.elim 1); |
|
95 by (ALLGOALS (fast_tac qconverse_cs)); |
|
96 val lleq_symmetric = result(); |
|
97 |
|
98 goal LList.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'"; |
|
99 by (rtac equalityI 1); |
|
100 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 |
|
101 ORELSE etac lleq_symmetric 1)); |
|
102 val lleq_implies_equal = result(); |
|
103 |
|
104 val [eqprem,lprem] = goal LList.thy |
|
105 "[| l=l'; l: llist(A) |] ==> <l,l'> : lleq(A)"; |
|
106 by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] lleq.coinduct 1); |
|
107 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); |
|
108 by (safe_tac qpair_cs); |
|
109 by (etac llist.elim 1); |
|
110 by (ALLGOALS (fast_tac pair_cs)); |
|
111 val equal_llist_implies_leq = result(); |
|
112 |
|
113 |
|
114 (*** Lazy List Functions ***) |
|
115 |
|
116 (*Examples of coinduction for type-checking and to prove llist equations*) |
|
117 |
|
118 (*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***) |
|
119 |
|
120 goalw LList.thy llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))"; |
|
121 by (rtac bnd_monoI 1); |
|
122 by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2)); |
|
123 by (REPEAT (ares_tac [subset_refl, A_subset_univ, |
|
124 QInr_subset_univ, QPair_subset_univ] 1)); |
|
125 val lconst_fun_bnd_mono = result(); |
|
126 |
|
127 (* lconst(a) = LCons(a,lconst(a)) *) |
|
128 val lconst = standard |
|
129 ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski); |
|
130 |
|
131 val lconst_subset = lconst_def RS def_lfp_subset; |
|
132 |
|
133 val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper); |
|
134 |
|
135 goal LList.thy "!!a A. a : A ==> lconst(a) : quniv(A)"; |
|
136 by (rtac (lconst_subset RS subset_trans RS qunivI) 1); |
|
137 by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1); |
|
138 val lconst_in_quniv = result(); |
|
139 |
|
140 goal LList.thy "!!a A. a:A ==> lconst(a): llist(A)"; |
|
141 by (rtac (singletonI RS llist.coinduct) 1); |
|
142 by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1); |
|
143 by (fast_tac (ZF_cs addSIs [lconst]) 1); |
|
144 val lconst_type = result(); |
|
145 |
|
146 (*** flip --- equations merely assumed; certain consequences proved ***) |
|
147 |
|
148 val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type]; |
|
149 |
|
150 goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))"; |
|
151 by (fast_tac (quniv_cs addSEs [boolE]) 1); |
|
152 val bool_Int_subset_univ = result(); |
|
153 |
|
154 val flip_cs = quniv_cs addSIs [not_type] |
|
155 addIs [bool_Int_subset_univ]; |
|
156 |
|
157 (*Reasoning borrowed from lleq.ML; a similar proof works for all |
|
158 "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*) |
|
159 goal LList.thy |
|
160 "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \ |
|
161 \ univ(eclose(bool))"; |
|
162 by (etac trans_induct 1); |
|
163 by (rtac ballI 1); |
|
164 by (etac llist.elim 1); |
|
165 by (asm_simp_tac flip_ss 1); |
|
166 by (asm_simp_tac flip_ss 2); |
|
167 by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs)); |
|
168 (*LNil case*) |
|
169 by (fast_tac flip_cs 1); |
|
170 (*LCons case*) |
|
171 by (safe_tac flip_cs); |
|
172 by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec]))); |
|
173 val flip_llist_quniv_lemma = result(); |
|
174 |
|
175 goal LList.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)"; |
|
176 by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1); |
|
177 by (REPEAT (assume_tac 1)); |
|
178 val flip_in_quniv = result(); |
|
179 |
|
180 val [prem] = goal LList.thy "l : llist(bool) ==> flip(l): llist(bool)"; |
|
181 by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")] |
|
182 llist.coinduct 1); |
|
183 by (rtac (prem RS RepFunI) 1); |
|
184 by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1); |
|
185 by (etac RepFunE 1); |
|
186 by (etac llist.elim 1); |
|
187 by (asm_simp_tac flip_ss 1); |
|
188 by (asm_simp_tac flip_ss 1); |
|
189 by (fast_tac (ZF_cs addSIs [not_type]) 1); |
|
190 val flip_type = result(); |
|
191 |
|
192 val [prem] = goal LList.thy |
|
193 "l : llist(bool) ==> flip(flip(l)) = l"; |
|
194 by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")] |
|
195 (lleq.coinduct RS lleq_implies_equal) 1); |
|
196 by (rtac (prem RS RepFunI) 1); |
|
197 by (fast_tac (ZF_cs addSIs [flip_type]) 1); |
|
198 by (etac RepFunE 1); |
|
199 by (etac llist.elim 1); |
|
200 by (asm_simp_tac flip_ss 1); |
|
201 by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1); |
|
202 by (fast_tac (ZF_cs addSIs [not_type]) 1); |
|
203 val flip_flip = result(); |