1.1 --- a/src/Doc/Datatypes/Datatypes.thy Wed Nov 06 12:47:50 2013 +0100
1.2 +++ b/src/Doc/Datatypes/Datatypes.thy Wed Nov 06 13:00:16 2013 +0100
1.3 @@ -1847,12 +1847,14 @@
1.4
1.5 text {*
1.6 \noindent
1.7 -A more natural syntax, also supported by Isabelle, is to move corecursive calls
1.8 -under constructors:
1.9 +Fortunately, it is easy to prove the following lemma, where the corecursive call
1.10 +is moved inside the lazy list constructor, thereby eliminating the need for
1.11 +@{const lmap}:
1.12 *}
1.13
1.14 - primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
1.15 + lemma tree\<^sub>i\<^sub>i_of_stream_alt:
1.16 "tree\<^sub>i\<^sub>i_of_stream s = Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
1.17 + by (subst tree\<^sub>i\<^sub>i_of_stream.code) simp
1.18
1.19 text {*
1.20 The next example illustrates corecursion through functions, which is a bit