src/HOL/Lazy_Sequence.thy
changeset 36533 f8df589ca2a5
parent 36516 8dac276ab10d
child 36902 c6bae4456741
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Apr 29 15:00:41 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Thu Apr 29 15:00:41 2010 +0200
     1.3 @@ -123,41 +123,18 @@
     1.4  
     1.5  subsection {* Code setup *}
     1.6  
     1.7 -code_reflect
     1.8 -  datatypes lazy_sequence = Lazy_Sequence
     1.9 -  functions map yield
    1.10 -  module_name Lazy_Sequence
    1.11 -
    1.12 -(* FIXME formulate yieldn in the logic with type code_numeral -- get rid of mapa confusion *)
    1.13 -
    1.14 -ML {*
    1.15 -signature LAZY_SEQUENCE =
    1.16 -sig
    1.17 -  datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
    1.18 -  val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
    1.19 -  val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
    1.20 -  val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
    1.21 -  val mapa : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
    1.22 -end;
    1.23 +fun anamorph :: "('a \<Rightarrow> ('b \<times> 'a) option) \<Rightarrow> code_numeral \<Rightarrow> 'a \<Rightarrow> 'b list \<times> 'a" where
    1.24 +  "anamorph f k x = (if k = 0 then ([], x)
    1.25 +    else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow>
    1.26 +      let (vs, z) = anamorph f (k - 1) y
    1.27 +    in (v # vs, z))"
    1.28  
    1.29 -structure Lazy_Sequence : LAZY_SEQUENCE =
    1.30 -struct
    1.31 -
    1.32 -open Lazy_Sequence;
    1.33 -
    1.34 -fun map f = mapa f;
    1.35 +definition yieldn :: "code_numeral \<Rightarrow> 'a lazy_sequence \<Rightarrow> 'a list \<times> 'a lazy_sequence" where
    1.36 +  "yieldn = anamorph yield"
    1.37  
    1.38 -fun anamorph f k x = (if k = 0 then ([], x)
    1.39 -  else case f x
    1.40 -   of NONE => ([], x)
    1.41 -    | SOME (v, y) => let
    1.42 -        val (vs, z) = anamorph f (k - 1) y
    1.43 -      in (v :: vs, z) end);
    1.44 -
    1.45 -fun yieldn S = anamorph yield S;
    1.46 -
    1.47 -end;
    1.48 -*}
    1.49 +code_reflect Lazy_Sequence
    1.50 +  datatypes lazy_sequence = Lazy_Sequence
    1.51 +  functions map yield yieldn
    1.52  
    1.53  section {* With Hit Bound Value *}
    1.54  text {* assuming in negative context *}