22 |
22 |
23 header {*Definition of type llist by a greatest fixed point*} |
23 header {*Definition of type llist by a greatest fixed point*} |
24 |
24 |
25 theory LList imports SList begin |
25 theory LList imports SList begin |
26 |
26 |
27 consts |
27 coinductive_set |
28 |
|
29 llist :: "'a item set => 'a item set" |
28 llist :: "'a item set => 'a item set" |
|
29 for A :: "'a item set" |
|
30 where |
|
31 NIL_I: "NIL \<in> llist(A)" |
|
32 | CONS_I: "[| a \<in> A; M \<in> llist(A) |] ==> CONS a M \<in> llist(A)" |
|
33 |
|
34 coinductive_set |
30 LListD :: "('a item * 'a item)set => ('a item * 'a item)set" |
35 LListD :: "('a item * 'a item)set => ('a item * 'a item)set" |
31 |
36 for r :: "('a item * 'a item)set" |
32 |
37 where |
33 coinductive "llist(A)" |
|
34 intros |
|
35 NIL_I: "NIL \<in> llist(A)" |
|
36 CONS_I: "[| a \<in> A; M \<in> llist(A) |] ==> CONS a M \<in> llist(A)" |
|
37 |
|
38 coinductive "LListD(r)" |
|
39 intros |
|
40 NIL_I: "(NIL, NIL) \<in> LListD(r)" |
38 NIL_I: "(NIL, NIL) \<in> LListD(r)" |
41 CONS_I: "[| (a,b) \<in> r; (M,N) \<in> LListD(r) |] |
39 | CONS_I: "[| (a,b) \<in> r; (M,N) \<in> LListD(r) |] |
42 ==> (CONS a M, CONS b N) \<in> LListD(r)" |
40 ==> (CONS a M, CONS b N) \<in> LListD(r)" |
43 |
41 |
44 |
42 |
45 typedef (LList) |
43 typedef (LList) |
46 'a llist = "llist(range Leaf) :: 'a item set" |
44 'a llist = "llist(range Leaf) :: 'a item set" |
157 subsubsection{* Simplification *} |
155 subsubsection{* Simplification *} |
158 |
156 |
159 declare option.split [split] |
157 declare option.split [split] |
160 |
158 |
161 text{*This justifies using llist in other recursive type definitions*} |
159 text{*This justifies using llist in other recursive type definitions*} |
162 lemma llist_mono: "A\<subseteq>B ==> llist(A) \<subseteq> llist(B)" |
160 lemma llist_mono: |
163 apply (simp add: llist.defs) |
161 assumes subset: "A \<subseteq> B" |
164 apply (rule gfp_mono) |
162 shows "llist A \<subseteq> llist B" |
165 apply (assumption | rule basic_monos)+ |
163 proof |
166 done |
164 fix x |
|
165 assume "x \<in> llist A" |
|
166 then show "x \<in> llist B" |
|
167 proof coinduct |
|
168 case llist |
|
169 then show ?case using subset |
|
170 by cases blast+ |
|
171 qed |
|
172 qed |
167 |
173 |
168 |
174 |
169 lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))" |
175 lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))" |
170 by (fast intro!: llist.intros [unfolded NIL_def CONS_def] |
176 by (fast intro!: llist.intros [unfolded NIL_def CONS_def] |
171 elim: llist.cases [unfolded NIL_def CONS_def]) |
177 elim: llist.cases [unfolded NIL_def CONS_def]) |
193 by (simp add: list_Fun_def CONS_def) |
199 by (simp add: list_Fun_def CONS_def) |
194 |
200 |
195 |
201 |
196 text{*Utilise the ``strong'' part, i.e. @{text "gfp(f)"}*} |
202 text{*Utilise the ``strong'' part, i.e. @{text "gfp(f)"}*} |
197 lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))" |
203 lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))" |
198 apply (unfold llist.defs list_Fun_def) |
204 apply (unfold list_Fun_def) |
199 apply (rule gfp_fun_UnI2) |
205 apply (erule llist.cases) |
200 apply (rule monoI, auto) |
206 apply auto |
201 done |
207 done |
202 |
208 |
203 subsection{* @{text LList_corec} satisfies the desired recurion equation *} |
209 subsection{* @{text LList_corec} satisfies the desired recurion equation *} |
204 |
210 |
205 text{*A continuity result?*} |
211 text{*A continuity result?*} |
276 done |
282 done |
277 |
283 |
278 text{*The domain of the @{text LListD} relation*} |
284 text{*The domain of the @{text LListD} relation*} |
279 lemma Domain_LListD: |
285 lemma Domain_LListD: |
280 "Domain (LListD(diag A)) \<subseteq> llist(A)" |
286 "Domain (LListD(diag A)) \<subseteq> llist(A)" |
281 apply (simp add: llist.defs NIL_def CONS_def) |
287 apply (rule subsetI) |
282 apply (rule gfp_upperbound) |
288 apply (erule llist.coinduct) |
283 txt{*avoids unfolding @{text LListD} on the rhs*} |
289 apply (simp add: NIL_def CONS_def) |
284 apply (rule_tac P = "%x. Domain x \<subseteq> ?B" in LListD_unfold [THEN ssubst], auto) |
290 apply (drule_tac P = "%x. xa \<in> Domain x" in LListD_unfold [THEN subst], auto) |
285 done |
291 done |
286 |
292 |
287 text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*} |
293 text{*This inclusion justifies the use of coinduction to show @{text "M = N"}*} |
288 lemma LListD_subset_diag: "LListD(diag A) \<subseteq> diag(llist(A))" |
294 lemma LListD_subset_diag: "LListD(diag A) \<subseteq> diag(llist(A))" |
289 apply (rule subsetI) |
295 apply (rule subsetI) |
303 apply (assumption | rule basic_monos)+ |
309 apply (assumption | rule basic_monos)+ |
304 done |
310 done |
305 |
311 |
306 lemma LListD_coinduct: |
312 lemma LListD_coinduct: |
307 "[| M \<in> X; X \<subseteq> LListD_Fun r (X Un LListD(r)) |] ==> M \<in> LListD(r)" |
313 "[| M \<in> X; X \<subseteq> LListD_Fun r (X Un LListD(r)) |] ==> M \<in> LListD(r)" |
|
314 apply (cases M) |
308 apply (simp add: LListD_Fun_def) |
315 apply (simp add: LListD_Fun_def) |
309 apply (erule LListD.coinduct) |
316 apply (erule LListD.coinduct) |
310 apply (auto ); |
317 apply (auto ); |
311 done |
318 done |
312 |
319 |
318 by (simp add: LListD_Fun_def CONS_def, blast) |
325 by (simp add: LListD_Fun_def CONS_def, blast) |
319 |
326 |
320 text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*} |
327 text{*Utilise the "strong" part, i.e. @{text "gfp(f)"}*} |
321 lemma LListD_Fun_LListD_I: |
328 lemma LListD_Fun_LListD_I: |
322 "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))" |
329 "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))" |
323 apply (unfold LListD.defs LListD_Fun_def) |
330 apply (cases M) |
324 apply (rule gfp_fun_UnI2) |
331 apply (simp add: LListD_Fun_def) |
325 apply (rule monoI, auto) |
332 apply (erule LListD.cases) |
|
333 apply auto |
326 done |
334 done |
327 |
335 |
328 |
336 |
329 text{*This converse inclusion helps to strengthen @{text LList_equalityI}*} |
337 text{*This converse inclusion helps to strengthen @{text LList_equalityI}*} |
330 lemma diag_subset_LListD: "diag(llist(A)) \<subseteq> LListD(diag A)" |
338 lemma diag_subset_LListD: "diag(llist(A)) \<subseteq> LListD(diag A)" |
521 diag(llist(A))) |
529 diag(llist(A))) |
522 |] ==> f(M) = g(M)" |
530 |] ==> f(M) = g(M)" |
523 apply (rule LList_equalityI) |
531 apply (rule LList_equalityI) |
524 apply (erule imageI) |
532 apply (erule imageI) |
525 apply (rule image_subsetI) |
533 apply (rule image_subsetI) |
526 apply (erule_tac aa=x in llist.cases) |
534 apply (erule_tac a=x in llist.cases) |
527 apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) |
535 apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) |
528 done |
536 done |
529 |
537 |
530 |
538 |
531 subsection{* The functional @{text Lmap} *} |
539 subsection{* The functional @{text Lmap} *} |
606 text{*weak co-induction: bisimulation and case analysis on both variables*} |
614 text{*weak co-induction: bisimulation and case analysis on both variables*} |
607 lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)" |
615 lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)" |
608 apply (rule_tac X = "\<Union>u\<in>llist (A) . \<Union>v \<in> llist (A) . {Lappend u v}" in llist_coinduct) |
616 apply (rule_tac X = "\<Union>u\<in>llist (A) . \<Union>v \<in> llist (A) . {Lappend u v}" in llist_coinduct) |
609 apply fast |
617 apply fast |
610 apply safe |
618 apply safe |
611 apply (erule_tac aa = u in llist.cases) |
619 apply (erule_tac a = u in llist.cases) |
612 apply (erule_tac aa = v in llist.cases, simp_all, blast) |
620 apply (erule_tac a = v in llist.cases, simp_all, blast) |
613 done |
621 done |
614 |
622 |
615 text{*strong co-induction: bisimulation and case analysis on one variable*} |
623 text{*strong co-induction: bisimulation and case analysis on one variable*} |
616 lemma Lappend_type': "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)" |
624 lemma Lappend_type': "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)" |
617 apply (rule_tac X = "(%u. Lappend u N) `llist (A)" in llist_coinduct) |
625 apply (rule_tac X = "(%u. Lappend u N) `llist (A)" in llist_coinduct) |
618 apply (erule imageI) |
626 apply (erule imageI) |
619 apply (rule image_subsetI) |
627 apply (rule image_subsetI) |
620 apply (erule_tac aa = x in llist.cases) |
628 apply (erule_tac a = x in llist.cases) |
621 apply (simp add: list_Fun_llist_I, simp) |
629 apply (simp add: list_Fun_llist_I, simp) |
622 done |
630 done |
623 |
631 |
624 subsection{* Lazy lists as the type @{text "'a llist"} -- strongly typed versions of above *} |
632 subsection{* Lazy lists as the type @{text "'a llist"} -- strongly typed versions of above *} |
625 |
633 |