removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
--- 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;
--- 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