src/HOL/Lazy_Sequence.thy
changeset 36024 c1ce2f60b0f2
parent 36020 3ee4c29ead7f
child 36030 1cd962a0b1a6
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:40 2010 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:41 2010 +0200
     1.3 @@ -20,15 +20,6 @@
     1.4    "yield Empty = None"
     1.5  | "yield (Insert x xq) = Some (x, xq)"
     1.6  
     1.7 -fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence"
     1.8 -where
     1.9 -  "yieldn i S = (if i = 0 then ([], S) else
    1.10 -    case yield S of
    1.11 -      None => ([], S)
    1.12 -    | Some (x, S') => let
    1.13 -       (xs, S'') = yieldn (i - 1) S'
    1.14 -      in (x # xs, S''))"
    1.15 -
    1.16  lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
    1.17  by (cases xq) auto
    1.18  
    1.19 @@ -141,7 +132,14 @@
    1.20  
    1.21  val yield = @{code yield}
    1.22  
    1.23 -val yieldn = @{code yieldn}
    1.24 +fun anamorph f k x = (if k = 0 then ([], x)
    1.25 +  else case f x
    1.26 +   of NONE => ([], x)
    1.27 +    | SOME (v, y) => let
    1.28 +        val (vs, z) = anamorph f (k - 1) y
    1.29 +      in (v :: vs, z) end);
    1.30 +
    1.31 +fun yieldn S = anamorph yield S;
    1.32  
    1.33  val map = @{code map}
    1.34  
    1.35 @@ -155,7 +153,7 @@
    1.36  code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
    1.37  
    1.38  hide (open) type lazy_sequence
    1.39 -hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
    1.40 -hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
    1.41 +hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
    1.42 +hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
    1.43  
    1.44  end