equal
deleted
inserted
replaced
21 val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; |
21 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)"; |
22 val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)"; |
23 |
23 |
24 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))"; |
24 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))"; |
25 let open llist; val rew = rewrite_rule con_defs in |
25 let open llist; val rew = rewrite_rule con_defs in |
26 by (fast_tac (!claset addSIs (subsetI :: equalityI :: map rew intrs) |
26 by (fast_tac (!claset addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1) |
27 addEs [rew elim]) 1) |
|
28 end; |
27 end; |
29 qed "llist_unfold"; |
28 qed "llist_unfold"; |
30 |
29 |
31 (*** Lemmas to justify using "llist" in other recursive type definitions ***) |
30 (*** Lemmas to justify using "llist" in other recursive type definitions ***) |
32 |
31 |