equal
deleted
inserted
replaced
14 (*Proving freeness results*) |
14 (*Proving freeness results*) |
15 val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
15 val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
16 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)"; |
16 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)"; |
17 |
17 |
18 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))"; |
18 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))"; |
19 by (rtac (llist.unfold RS trans) 1); |
19 let open llist; val rew = rewrite_rule con_defs in |
20 bws llist.con_defs; |
20 by (fast_tac (qsum_cs addSIs (equalityI :: map rew intrs) |
21 br equalityI 1; |
21 addEs [rew elim]) 1) |
22 by (fast_tac qsum_cs 1); |
22 end; |
23 by (fast_tac (qsum_cs addIs codatatype_intrs |
|
24 addDs [llist.dom_subset RS subsetD] |
|
25 addSEs [QSigmaE]) 1); |
|
26 val llist_unfold = result(); |
23 val llist_unfold = result(); |
27 |
24 |
28 (*** Lemmas to justify using "llist" in other recursive type definitions ***) |
25 (*** Lemmas to justify using "llist" in other recursive type definitions ***) |
29 |
26 |
30 goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; |
27 goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; |