equal
deleted
inserted
replaced
195 (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since |
195 (* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since |
196 we cannot rely on its presence, we expediently provide our own |
196 we cannot rely on its presence, we expediently provide our own |
197 axiomatization. The examples also work unchanged with Lochbihler's |
197 axiomatization. The examples also work unchanged with Lochbihler's |
198 "Coinductive_List" theory. *) |
198 "Coinductive_List" theory. *) |
199 |
199 |
|
200 (* BEGIN LAZY LIST SETUP *) |
200 definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)" |
201 definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)" |
201 |
202 |
202 typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set" |
203 typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set" |
203 unfolding llist_def by auto |
204 unfolding llist_def by auto |
204 |
205 |
217 |
218 |
218 declaration {* |
219 declaration {* |
219 Nitpick_HOL.register_codatatype @{typ "'a llist"} "" |
220 Nitpick_HOL.register_codatatype @{typ "'a llist"} "" |
220 (map dest_Const [@{term LNil}, @{term LCons}]) |
221 (map dest_Const [@{term LNil}, @{term LCons}]) |
221 *} |
222 *} |
|
223 (* END LAZY LIST SETUP *) |
222 |
224 |
223 lemma "xs \<noteq> LCons a xs" |
225 lemma "xs \<noteq> LCons a xs" |
224 nitpick [expect = genuine] |
226 nitpick [expect = genuine] |
225 oops |
227 oops |
226 |
228 |