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
```