author | wenzelm |
Sat, 17 Oct 2009 14:43:18 +0200 | |
changeset 32960 | 69916a850301 |
parent 24893 | b8ef7afe3a6b |
child 41779 | a68f503805ed |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/ex/LList.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
515 | 3 |
Copyright 1994 University of Cambridge |
4 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
5 |
Codatatype definition of Lazy Lists. |
515 | 6 |
|
7 |
Equality for llist(A) as a greatest fixed point |
|
8 |
||
9 |
Functions for Lazy Lists |
|
10 |
||
11 |
STILL NEEDS: |
|
12 |
co_recursion for defining lconst, flip, etc. |
|
13 |
a typing rule for it, based on some notion of "productivity..." |
|
14 |
*) |
|
15 |
||
16417 | 16 |
theory LList imports Main begin |
515 | 17 |
|
18 |
consts |
|
12867 | 19 |
llist :: "i=>i"; |
515 | 20 |
|
21 |
codatatype |
|
12867 | 22 |
"llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)") |
515 | 23 |
|
24 |
||
25 |
(*Coinductive definition of equality*) |
|
26 |
consts |
|
12867 | 27 |
lleq :: "i=>i" |
515 | 28 |
|
29 |
(*Previously used <*> in the domain and variant pairs as elements. But |
|
30 |
standard pairs work just as well. To use variant pairs, must change prefix |
|
31 |
a q/Q to the Sigma, Pair and converse rules.*) |
|
32 |
coinductive |
|
33 |
domains "lleq(A)" <= "llist(A) * llist(A)" |
|
12867 | 34 |
intros |
35 |
LNil: "<LNil, LNil> \<in> lleq(A)" |
|
36 |
LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |] |
|
37 |
==> <LCons(a,l), LCons(a,l')> \<in> lleq(A)" |
|
38 |
type_intros llist.intros |
|
515 | 39 |
|
40 |
||
41 |
(*Lazy list functions; flip is not definitional!*) |
|
24893 | 42 |
definition |
43 |
lconst :: "i => i" where |
|
44 |
"lconst(a) == lfp(univ(a), %l. LCons(a,l))" |
|
515 | 45 |
|
24893 | 46 |
consts |
47 |
flip :: "i => i" |
|
12867 | 48 |
axioms |
49 |
flip_LNil: "flip(LNil) = LNil" |
|
50 |
||
51 |
flip_LCons: "[| x \<in> bool; l \<in> llist(bool) |] |
|
52 |
==> flip(LCons(x,l)) = LCons(not(x), flip(l))" |
|
53 |
||
54 |
||
55 |
(*These commands cause classical reasoning to regard the subset relation |
|
56 |
as primitive, not reducing it to membership*) |
|
57 |
||
58 |
declare subsetI [rule del] |
|
59 |
subsetCE [rule del] |
|
60 |
||
61 |
declare subset_refl [intro!] |
|
62 |
cons_subsetI [intro!] |
|
63 |
subset_consI [intro!] |
|
64 |
Union_least [intro!] |
|
65 |
UN_least [intro!] |
|
66 |
Un_least [intro!] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
67 |
Inter_greatest [intro!] |
12867 | 68 |
Int_greatest [intro!] |
69 |
RepFun_subset [intro!] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
70 |
Un_upper1 [intro!] |
12867 | 71 |
Un_upper2 [intro!] |
72 |
Int_lower1 [intro!] |
|
73 |
Int_lower2 [intro!] |
|
74 |
||
75 |
(*An elimination rule, for type-checking*) |
|
76 |
inductive_cases LConsE: "LCons(a,l) \<in> llist(A)" |
|
77 |
||
78 |
(*Proving freeness results*) |
|
79 |
lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'" |
|
80 |
by auto |
|
81 |
||
82 |
lemma LNil_LCons_iff: "~ LNil=LCons(a,l)" |
|
83 |
by auto |
|
84 |
||
85 |
(* |
|
86 |
lemma llist_unfold: "llist(A) = {0} <+> (A <*> llist(A))"; |
|
87 |
let open llist val rew = rewrite_rule con_defs in |
|
88 |
by (fast_tac (claset() addSIs (subsetI ::map rew intros) addEs [rew elim]) 1) |
|
89 |
end |
|
90 |
done |
|
91 |
*) |
|
92 |
||
93 |
(*** Lemmas to justify using "llist" in other recursive type definitions ***) |
|
94 |
||
95 |
lemma llist_mono: "A \<subseteq> B ==> llist(A) \<subseteq> llist(B)" |
|
96 |
apply (unfold llist.defs ) |
|
97 |
apply (rule gfp_mono) |
|
98 |
apply (rule llist.bnd_mono) |
|
99 |
apply (assumption | rule quniv_mono basic_monos)+ |
|
100 |
done |
|
101 |
||
102 |
(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **) |
|
103 |
||
104 |
declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] |
|
105 |
QPair_subset_univ [intro!] |
|
106 |
empty_subsetI [intro!] |
|
107 |
one_in_quniv [THEN qunivD, intro!] |
|
108 |
declare qunivD [dest!] |
|
109 |
declare Ord_in_Ord [elim!] |
|
110 |
||
111 |
lemma llist_quniv_lemma [rule_format]: |
|
112 |
"Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l Int Vset(i) \<subseteq> univ(eclose(A))" |
|
113 |
apply (erule trans_induct) |
|
114 |
apply (rule ballI) |
|
115 |
apply (erule llist.cases) |
|
116 |
apply (simp_all add: QInl_def QInr_def llist.con_defs) |
|
117 |
(*LCons case: I simply can't get rid of the deepen_tac*) |
|
24893 | 118 |
apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}] |
119 |
addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1") |
|
12867 | 120 |
done |
121 |
||
122 |
lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)" |
|
123 |
apply (rule qunivI [THEN subsetI]) |
|
124 |
apply (rule Int_Vset_subset) |
|
125 |
apply (assumption | rule llist_quniv_lemma)+ |
|
126 |
done |
|
127 |
||
128 |
lemmas llist_subset_quniv = |
|
129 |
subset_trans [OF llist_mono llist_quniv] |
|
130 |
||
131 |
||
132 |
(*** Lazy List Equality: lleq ***) |
|
133 |
||
134 |
declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] |
|
135 |
QPair_mono [intro!] |
|
136 |
||
137 |
declare Ord_in_Ord [elim!] |
|
138 |
||
139 |
(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*) |
|
140 |
lemma lleq_Int_Vset_subset [rule_format]: |
|
141 |
"Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) --> l Int Vset(i) \<subseteq> l'" |
|
142 |
apply (erule trans_induct) |
|
143 |
apply (intro allI impI) |
|
144 |
apply (erule lleq.cases) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
145 |
apply (unfold QInr_def llist.con_defs, safe) |
12867 | 146 |
apply (fast elim!: Ord_trans bspec [elim_format]) |
147 |
done |
|
515 | 148 |
|
12867 | 149 |
(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) |
150 |
lemma lleq_symmetric: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> lleq(A)" |
|
151 |
apply (erule lleq.coinduct [OF converseI]) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
152 |
apply (rule lleq.dom_subset [THEN converse_type], safe) |
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
153 |
apply (erule lleq.cases, blast+) |
12867 | 154 |
done |
155 |
||
156 |
lemma lleq_implies_equal: "<l,l'> \<in> lleq(A) ==> l=l'" |
|
157 |
apply (rule equalityI) |
|
158 |
apply (assumption | rule lleq_Int_Vset_subset [THEN Int_Vset_subset] | |
|
159 |
erule lleq_symmetric)+ |
|
160 |
done |
|
161 |
||
162 |
lemma equal_llist_implies_leq: |
|
163 |
"[| l=l'; l \<in> llist(A) |] ==> <l,l'> \<in> lleq(A)" |
|
164 |
apply (rule_tac X = "{<l,l>. l \<in> llist (A) }" in lleq.coinduct) |
|
165 |
apply blast |
|
166 |
apply safe |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
167 |
apply (erule_tac a=l in llist.cases, fast+) |
12867 | 168 |
done |
169 |
||
170 |
||
171 |
(*** Lazy List Functions ***) |
|
172 |
||
173 |
(*Examples of coinduction for type-checking and to prove llist equations*) |
|
174 |
||
175 |
(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***) |
|
176 |
||
177 |
lemma lconst_fun_bnd_mono: "bnd_mono(univ(a), %l. LCons(a,l))" |
|
178 |
apply (unfold llist.con_defs ) |
|
179 |
apply (rule bnd_monoI) |
|
180 |
apply (blast intro: A_subset_univ QInr_subset_univ) |
|
181 |
apply (blast intro: subset_refl QInr_mono QPair_mono) |
|
182 |
done |
|
183 |
||
184 |
(* lconst(a) = LCons(a,lconst(a)) *) |
|
185 |
lemmas lconst = def_lfp_unfold [OF lconst_def lconst_fun_bnd_mono] |
|
186 |
lemmas lconst_subset = lconst_def [THEN def_lfp_subset] |
|
187 |
lemmas member_subset_Union_eclose = arg_into_eclose [THEN Union_upper] |
|
188 |
||
189 |
lemma lconst_in_quniv: "a \<in> A ==> lconst(a) \<in> quniv(A)" |
|
190 |
apply (rule lconst_subset [THEN subset_trans, THEN qunivI]) |
|
191 |
apply (erule arg_into_eclose [THEN eclose_subset, THEN univ_mono]) |
|
192 |
done |
|
515 | 193 |
|
12867 | 194 |
lemma lconst_type: "a \<in> A ==> lconst(a): llist(A)" |
195 |
apply (rule singletonI [THEN llist.coinduct]) |
|
196 |
apply (erule lconst_in_quniv [THEN singleton_subsetI]) |
|
197 |
apply (fast intro!: lconst) |
|
198 |
done |
|
199 |
||
200 |
(*** flip --- equations merely assumed; certain consequences proved ***) |
|
201 |
||
202 |
declare flip_LNil [simp] |
|
203 |
flip_LCons [simp] |
|
204 |
not_type [simp] |
|
205 |
||
206 |
lemma bool_Int_subset_univ: "b \<in> bool ==> b Int X \<subseteq> univ(eclose(A))" |
|
207 |
by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE) |
|
208 |
||
209 |
declare not_type [intro!] |
|
210 |
declare bool_Int_subset_univ [intro] |
|
211 |
||
212 |
(*Reasoning borrowed from lleq.ML; a similar proof works for all |
|
213 |
"productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*) |
|
214 |
lemma flip_llist_quniv_lemma [rule_format]: |
|
215 |
"Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> univ(eclose(bool))" |
|
216 |
apply (erule trans_induct) |
|
217 |
apply (rule ballI) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
218 |
apply (erule llist.cases, simp_all) |
12867 | 219 |
apply (simp_all add: QInl_def QInr_def llist.con_defs) |
220 |
(*LCons case: I simply can't get rid of the deepen_tac*) |
|
24893 | 221 |
apply (tactic "deepen_tac (@{claset} addIs [@{thm Ord_trans}] |
222 |
addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1") |
|
12867 | 223 |
done |
224 |
||
225 |
lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)" |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
226 |
by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+) |
12867 | 227 |
|
228 |
lemma flip_type: "l \<in> llist(bool) ==> flip(l): llist(bool)" |
|
229 |
apply (rule_tac X = "{flip (l) . l \<in> llist (bool) }" in llist.coinduct) |
|
230 |
apply blast |
|
231 |
apply (fast intro!: flip_in_quniv) |
|
232 |
apply (erule RepFunE) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
233 |
apply (erule_tac a=la in llist.cases, auto) |
12867 | 234 |
done |
235 |
||
236 |
lemma flip_flip: "l \<in> llist(bool) ==> flip(flip(l)) = l" |
|
237 |
apply (rule_tac X1 = "{<flip (flip (l)),l> . l \<in> llist (bool) }" in |
|
238 |
lleq.coinduct [THEN lleq_implies_equal]) |
|
239 |
apply blast |
|
240 |
apply (fast intro!: flip_type) |
|
241 |
apply (erule RepFunE) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
242 |
apply (erule_tac a=la in llist.cases) |
12867 | 243 |
apply (simp_all add: flip_type not_not) |
244 |
done |
|
515 | 245 |
|
246 |
end |
|
247 |