author | clasohm |
Wed, 06 Oct 1993 14:45:04 +0100 | |
changeset 34 | 747f1aad03cf |
parent 16 | 0b033d50ca1c |
child 71 | 729fe026c5f3 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/ex/llist.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Co-Datatype definition of Lazy Lists |
|
7 |
||
8 |
Needs a "take-lemma" to prove llist_subset_quniv and to justify co-induction |
|
9 |
for proving equality |
|
10 |
*) |
|
11 |
||
12 |
structure LList = Co_Datatype_Fun |
|
13 |
(val thy = QUniv.thy; |
|
14 |
val rec_specs = |
|
15 |
[("llist", "quniv(A)", |
|
16 |
[(["LNil"], "i"), |
|
17 |
(["LCons"], "[i,i]=>i")])]; |
|
18 |
val rec_styp = "i=>i"; |
|
19 |
val ext = None |
|
20 |
val sintrs = |
|
21 |
["LNil : llist(A)", |
|
22 |
"[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"]; |
|
23 |
val monos = []; |
|
24 |
val type_intrs = co_data_typechecks |
|
25 |
val type_elims = []); |
|
26 |
||
27 |
val [LNilI, LConsI] = LList.intrs; |
|
28 |
||
29 |
(*An elimination rule, for type-checking*) |
|
30 |
val LConsE = LList.mk_cases LList.con_defs "LCons(a,l) : llist(A)"; |
|
31 |
||
32 |
(*Proving freeness results*) |
|
33 |
val LCons_iff = LList.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
|
34 |
val LNil_LCons_iff = LList.mk_free "~ LNil=LCons(a,l)"; |
|
35 |
||
36 |
(*** Lemmas to justify using "llist" in other recursive type definitions ***) |
|
37 |
||
38 |
goalw LList.thy LList.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; |
|
39 |
by (rtac gfp_mono 1); |
|
40 |
by (REPEAT (rtac LList.bnd_mono 1)); |
|
41 |
by (REPEAT (ares_tac (quniv_mono::basic_monos) 1)); |
|
42 |
val llist_mono = result(); |
|
43 |
||
44 |
(** Closure of quniv(A) under llist -- why so complex? Its a gfp... **) |
|
45 |
||
46 |
val in_quniv_rls = |
|
47 |
[Transset_quniv, QPair_Int_quniv_in_quniv, Int_Vfrom_0_in_quniv, |
|
48 |
zero_Int_in_quniv, one_Int_in_quniv, |
|
49 |
QPair_Int_Vfrom_succ_in_quniv, QPair_Int_Vfrom_in_quniv]; |
|
50 |
||
51 |
val quniv_cs = ZF_cs addSIs in_quniv_rls |
|
52 |
addIs (Int_quniv_in_quniv::co_data_typechecks); |
|
53 |
||
54 |
(*Keep unfolding the lazy list until the induction hypothesis applies*) |
|
55 |
goal LList.thy |
|
56 |
"!!i. i : nat ==> \ |
|
57 |
\ ALL l: llist(quniv(A)). l Int Vfrom(quniv(A), i) : quniv(A)"; |
|
16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
58 |
by (etac complete_induct 1); |
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
59 |
by (rtac ballI 1); |
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
60 |
by (etac LList.elim 1); |
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
61 |
by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs)); |
0 | 62 |
by (fast_tac quniv_cs 1); |
63 |
by (etac natE 1 THEN REPEAT_FIRST hyp_subst_tac); |
|
64 |
by (fast_tac quniv_cs 1); |
|
65 |
by (fast_tac quniv_cs 1); |
|
66 |
val llist_quniv_lemma = result(); |
|
67 |
||
68 |
goal LList.thy "llist(quniv(A)) <= quniv(A)"; |
|
16
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
69 |
by (rtac subsetI 1); |
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
70 |
by (rtac quniv_Int_Vfrom 1); |
0b033d50ca1c
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
7
diff
changeset
|
71 |
by (etac (LList.dom_subset RS subsetD) 1); |
0 | 72 |
by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1)); |
73 |
val llist_quniv = result(); |
|
74 |
||
75 |
val llist_subset_quniv = standard |
|
76 |
(llist_mono RS (llist_quniv RSN (2,subset_trans))); |
|
77 |
||
34
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset
|
78 |
(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow |
747f1aad03cf
changed filenames to lower case name of theory the file contains
clasohm
parents:
16
diff
changeset
|
79 |
automatic association between theory name and filename. *) |