4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Codatatype definition of Lazy Lists |
6 Codatatype definition of Lazy Lists |
7 *) |
7 *) |
8 |
8 |
9 open LList; |
9 (*These commands cause classical reasoning to regard the subset relation |
10 |
10 as primitive, not reducing it to membership*) |
|
11 |
11 Delrules [subsetI, subsetCE]; |
12 Delrules [subsetI, subsetCE]; |
12 AddSIs [subset_refl, cons_subsetI, subset_consI, |
13 AddSIs [subset_refl, cons_subsetI, subset_consI, |
13 Union_least, UN_least, Un_least, |
14 Union_least, UN_least, Un_least, |
14 Inter_greatest, Int_greatest, RepFun_subset, |
15 Inter_greatest, Int_greatest, RepFun_subset, |
15 Un_upper1, Un_upper2, Int_lower1, Int_lower2]; |
16 Un_upper1, Un_upper2, Int_lower1, Int_lower2]; |
16 |
17 |
17 (*An elimination rule, for type-checking*) |
18 (*An elimination rule, for type-checking*) |
18 val LConsE = llist.mk_cases llist.con_defs "LCons(a,l) : llist(A)"; |
19 val LConsE = llist.mk_cases "LCons(a,l) : llist(A)"; |
19 |
20 |
20 (*Proving freeness results*) |
21 (*Proving freeness results*) |
21 val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
22 val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
22 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)"; |
23 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)"; |
23 |
24 |