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