# HG changeset patch
# User bulwahn
# Date 1269876641 -7200
# Node ID c1ce2f60b0f2daa9438de775ec88add2338e71b8
# Parent  d606ca1674a7ce07b8c3ec9780e4d32040614687
removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command

diff -r d606ca1674a7 -r c1ce2f60b0f2 src/HOL/DSequence.thy
--- a/src/HOL/DSequence.thy	Mon Mar 29 17:30:40 2010 +0200
+++ b/src/HOL/DSequence.thy	Mon Mar 29 17:30:41 2010 +0200
@@ -27,12 +27,6 @@
     None => None
   | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
 
-definition yieldn :: "code_numeral => 'a dseq => code_numeral => bool => 'a list * 'a dseq"
-where
-  "yieldn n dseq i pol = (case eval dseq i pol of
-    None => ([], %i pol. None)
-  | Some s => let (xs, s') = Lazy_Sequence.yieldn n s in (xs, %i pol. Some s))"
-
 fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
 where
   "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
@@ -91,8 +85,11 @@
 
 type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
 
-val yieldn = @{code yieldn}
 val yield = @{code yield}
+fun yieldn n s d pol = case s d pol of  
+    NONE => ([], fn d => fn pol => NONE)
+  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
+
 val map = @{code map}
 
 end;
diff -r d606ca1674a7 -r c1ce2f60b0f2 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:40 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:41 2010 +0200
@@ -20,15 +20,6 @@
   "yield Empty = None"
 | "yield (Insert x xq) = Some (x, xq)"
 
-fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence"
-where
-  "yieldn i S = (if i = 0 then ([], S) else
-    case yield S of
-      None => ([], S)
-    | Some (x, S') => let
-       (xs, S'') = yieldn (i - 1) S'
-      in (x # xs, S''))"
-
 lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
 by (cases xq) auto
 
@@ -141,7 +132,14 @@
 
 val yield = @{code yield}
 
-val yieldn = @{code yieldn}
+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;
 
 val map = @{code map}
 
@@ -155,7 +153,7 @@
 code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
 
 hide (open) type lazy_sequence
-hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
-hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
+hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
+hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
 
 end