author | blanchet |
Tue, 15 Nov 2011 22:13:39 +0100 | |
changeset 45509 | 624872fc47bf |
parent 42798 | 02c88bdabe75 |
child 46822 | 95f1e700b712 |
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 |
|
41779 | 46 |
axiomatization flip :: "i => i" |
47 |
where |
|
48 |
flip_LNil: "flip(LNil) = LNil" and |
|
12867 | 49 |
flip_LCons: "[| x \<in> bool; l \<in> llist(bool) |] |
50 |
==> flip(LCons(x,l)) = LCons(not(x), flip(l))" |
|
51 |
||
52 |
||
53 |
(*These commands cause classical reasoning to regard the subset relation |
|
54 |
as primitive, not reducing it to membership*) |
|
55 |
||
56 |
declare subsetI [rule del] |
|
57 |
subsetCE [rule del] |
|
58 |
||
59 |
declare subset_refl [intro!] |
|
60 |
cons_subsetI [intro!] |
|
61 |
subset_consI [intro!] |
|
62 |
Union_least [intro!] |
|
63 |
UN_least [intro!] |
|
64 |
Un_least [intro!] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
65 |
Inter_greatest [intro!] |
12867 | 66 |
Int_greatest [intro!] |
67 |
RepFun_subset [intro!] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24893
diff
changeset
|
68 |
Un_upper1 [intro!] |
12867 | 69 |
Un_upper2 [intro!] |
70 |
Int_lower1 [intro!] |
|
71 |
Int_lower2 [intro!] |
|
72 |
||
73 |
(*An elimination rule, for type-checking*) |
|
74 |
inductive_cases LConsE: "LCons(a,l) \<in> llist(A)" |
|
75 |
||
76 |
(*Proving freeness results*) |
|
77 |
lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'" |
|
78 |
by auto |
|
79 |
||
80 |
lemma LNil_LCons_iff: "~ LNil=LCons(a,l)" |
|
81 |
by auto |
|
82 |
||
83 |
(* |
|
84 |
lemma llist_unfold: "llist(A) = {0} <+> (A <*> llist(A))"; |
|
85 |
let open llist val rew = rewrite_rule con_defs in |
|
86 |
by (fast_tac (claset() addSIs (subsetI ::map rew intros) addEs [rew elim]) 1) |
|
87 |
end |
|
88 |
done |
|
89 |
*) |
|
90 |
||
91 |
(*** Lemmas to justify using "llist" in other recursive type definitions ***) |
|
92 |
||
93 |
lemma llist_mono: "A \<subseteq> B ==> llist(A) \<subseteq> llist(B)" |
|
94 |
apply (unfold llist.defs ) |
|
95 |
apply (rule gfp_mono) |
|
96 |
apply (rule llist.bnd_mono) |
|
97 |
apply (assumption | rule quniv_mono basic_monos)+ |
|
98 |
done |
|
99 |
||
100 |
(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **) |
|
101 |
||
102 |
declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] |
|
103 |
QPair_subset_univ [intro!] |
|
104 |
empty_subsetI [intro!] |
|
105 |
one_in_quniv [THEN qunivD, intro!] |
|
106 |
declare qunivD [dest!] |
|
107 |
declare Ord_in_Ord [elim!] |
|
108 |
||
109 |
lemma llist_quniv_lemma [rule_format]: |
|
110 |
"Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l Int Vset(i) \<subseteq> univ(eclose(A))" |
|
111 |
apply (erule trans_induct) |
|
112 |
apply (rule ballI) |
|
113 |
apply (erule llist.cases) |
|
114 |
apply (simp_all add: QInl_def QInr_def llist.con_defs) |
|
115 |
(*LCons case: I simply can't get rid of the deepen_tac*) |
|
42798 | 116 |
apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans]) |
12867 | 117 |
done |
118 |
||
119 |
lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)" |
|
120 |
apply (rule qunivI [THEN subsetI]) |
|
121 |
apply (rule Int_Vset_subset) |
|
122 |
apply (assumption | rule llist_quniv_lemma)+ |
|
123 |
done |
|
124 |
||
125 |
lemmas llist_subset_quniv = |
|
126 |
subset_trans [OF llist_mono llist_quniv] |
|
127 |
||
128 |
||
129 |
(*** Lazy List Equality: lleq ***) |
|
130 |
||
131 |
declare QPair_Int_Vset_subset_UN [THEN subset_trans, intro!] |
|
132 |
QPair_mono [intro!] |
|
133 |
||
134 |
declare Ord_in_Ord [elim!] |
|
135 |
||
136 |
(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*) |
|
137 |
lemma lleq_Int_Vset_subset [rule_format]: |
|
138 |
"Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) --> l Int Vset(i) \<subseteq> l'" |
|
139 |
apply (erule trans_induct) |
|
140 |
apply (intro allI impI) |
|
141 |
apply (erule lleq.cases) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
142 |
apply (unfold QInr_def llist.con_defs, safe) |
12867 | 143 |
apply (fast elim!: Ord_trans bspec [elim_format]) |
144 |
done |
|
515 | 145 |
|
12867 | 146 |
(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) |
147 |
lemma lleq_symmetric: "<l,l'> \<in> lleq(A) ==> <l',l> \<in> lleq(A)" |
|
148 |
apply (erule lleq.coinduct [OF converseI]) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
149 |
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
|
150 |
apply (erule lleq.cases, blast+) |
12867 | 151 |
done |
152 |
||
153 |
lemma lleq_implies_equal: "<l,l'> \<in> lleq(A) ==> l=l'" |
|
154 |
apply (rule equalityI) |
|
155 |
apply (assumption | rule lleq_Int_Vset_subset [THEN Int_Vset_subset] | |
|
156 |
erule lleq_symmetric)+ |
|
157 |
done |
|
158 |
||
159 |
lemma equal_llist_implies_leq: |
|
160 |
"[| l=l'; l \<in> llist(A) |] ==> <l,l'> \<in> lleq(A)" |
|
161 |
apply (rule_tac X = "{<l,l>. l \<in> llist (A) }" in lleq.coinduct) |
|
162 |
apply blast |
|
163 |
apply safe |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
164 |
apply (erule_tac a=l in llist.cases, fast+) |
12867 | 165 |
done |
166 |
||
167 |
||
168 |
(*** Lazy List Functions ***) |
|
169 |
||
170 |
(*Examples of coinduction for type-checking and to prove llist equations*) |
|
171 |
||
172 |
(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***) |
|
173 |
||
174 |
lemma lconst_fun_bnd_mono: "bnd_mono(univ(a), %l. LCons(a,l))" |
|
175 |
apply (unfold llist.con_defs ) |
|
176 |
apply (rule bnd_monoI) |
|
177 |
apply (blast intro: A_subset_univ QInr_subset_univ) |
|
178 |
apply (blast intro: subset_refl QInr_mono QPair_mono) |
|
179 |
done |
|
180 |
||
181 |
(* lconst(a) = LCons(a,lconst(a)) *) |
|
182 |
lemmas lconst = def_lfp_unfold [OF lconst_def lconst_fun_bnd_mono] |
|
183 |
lemmas lconst_subset = lconst_def [THEN def_lfp_subset] |
|
184 |
lemmas member_subset_Union_eclose = arg_into_eclose [THEN Union_upper] |
|
185 |
||
186 |
lemma lconst_in_quniv: "a \<in> A ==> lconst(a) \<in> quniv(A)" |
|
187 |
apply (rule lconst_subset [THEN subset_trans, THEN qunivI]) |
|
188 |
apply (erule arg_into_eclose [THEN eclose_subset, THEN univ_mono]) |
|
189 |
done |
|
515 | 190 |
|
12867 | 191 |
lemma lconst_type: "a \<in> A ==> lconst(a): llist(A)" |
192 |
apply (rule singletonI [THEN llist.coinduct]) |
|
193 |
apply (erule lconst_in_quniv [THEN singleton_subsetI]) |
|
194 |
apply (fast intro!: lconst) |
|
195 |
done |
|
196 |
||
197 |
(*** flip --- equations merely assumed; certain consequences proved ***) |
|
198 |
||
199 |
declare flip_LNil [simp] |
|
200 |
flip_LCons [simp] |
|
201 |
not_type [simp] |
|
202 |
||
203 |
lemma bool_Int_subset_univ: "b \<in> bool ==> b Int X \<subseteq> univ(eclose(A))" |
|
204 |
by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE) |
|
205 |
||
206 |
declare not_type [intro!] |
|
207 |
declare bool_Int_subset_univ [intro] |
|
208 |
||
209 |
(*Reasoning borrowed from lleq.ML; a similar proof works for all |
|
210 |
"productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*) |
|
211 |
lemma flip_llist_quniv_lemma [rule_format]: |
|
212 |
"Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> univ(eclose(bool))" |
|
213 |
apply (erule trans_induct) |
|
214 |
apply (rule ballI) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
215 |
apply (erule llist.cases, simp_all) |
12867 | 216 |
apply (simp_all add: QInl_def QInr_def llist.con_defs) |
217 |
(*LCons case: I simply can't get rid of the deepen_tac*) |
|
42798 | 218 |
apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans]) |
12867 | 219 |
done |
220 |
||
221 |
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
|
222 |
by (rule flip_llist_quniv_lemma [THEN Int_Vset_subset, THEN qunivI], assumption+) |
12867 | 223 |
|
224 |
lemma flip_type: "l \<in> llist(bool) ==> flip(l): llist(bool)" |
|
225 |
apply (rule_tac X = "{flip (l) . l \<in> llist (bool) }" in llist.coinduct) |
|
226 |
apply blast |
|
227 |
apply (fast intro!: flip_in_quniv) |
|
228 |
apply (erule RepFunE) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
229 |
apply (erule_tac a=la in llist.cases, auto) |
12867 | 230 |
done |
231 |
||
232 |
lemma flip_flip: "l \<in> llist(bool) ==> flip(flip(l)) = l" |
|
233 |
apply (rule_tac X1 = "{<flip (flip (l)),l> . l \<in> llist (bool) }" in |
|
234 |
lleq.coinduct [THEN lleq_implies_equal]) |
|
235 |
apply blast |
|
236 |
apply (fast intro!: flip_type) |
|
237 |
apply (erule RepFunE) |
|
13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
12867
diff
changeset
|
238 |
apply (erule_tac a=la in llist.cases) |
12867 | 239 |
apply (simp_all add: flip_type not_not) |
240 |
done |
|
515 | 241 |
|
242 |
end |
|
243 |