src/HOL/Lazy_Sequence.thy
changeset 36533 f8df589ca2a5
parent 36516 8dac276ab10d
child 36902 c6bae4456741
--- a/src/HOL/Lazy_Sequence.thy	Thu Apr 29 15:00:41 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Thu Apr 29 15:00:41 2010 +0200
@@ -123,41 +123,18 @@
 
 subsection {* Code setup *}
 
-code_reflect
-  datatypes lazy_sequence = Lazy_Sequence
-  functions map yield
-  module_name Lazy_Sequence
-
-(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *)
-
-ML {*
-signature LAZY_SEQUENCE =
-sig
-  datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
-  val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
-  val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
-  val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
-  val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
-end;
+fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
+  "anamorph f k x = (if k = 0 then ([], x)
+    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
+      let (vs, z) = anamorph f (k - 1) y
+    in (v # vs, z))"
 
-structure Lazy_Sequence : LAZY_SEQUENCE =
-struct
-
-open Lazy_Sequence;
-
-fun map f = mapa f;
+definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
+  "yieldn = anamorph yield"
 
-fun anamorph f k x = (if k = 0 then ([], x)
-  else case f x
-   of NONE => ([], x)
-    | SOME (v, y) => let
-        val (vs, z) = anamorph f (k - 1) y
-      in (v :: vs, z) end);
-
-fun yieldn S = anamorph yield S;
-
-end;
-*}
+code_reflect Lazy_Sequence
+  datatypes lazy_sequence = Lazy_Sequence
+  functions map yield yieldn
 
 section {* With Hit Bound Value *}
 text {* assuming in negative context *}