removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
authorbulwahn
Mon Mar 29 17:30:41 2010 +0200 (2010-03-29)
changeset 36024c1ce2f60b0f2
parent 36023 d606ca1674a7
child 36025 d25043e7843f
removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
src/HOL/DSequence.thy
src/HOL/Lazy_Sequence.thy
     1.1 --- a/src/HOL/DSequence.thy	Mon Mar 29 17:30:40 2010 +0200
     1.2 +++ b/src/HOL/DSequence.thy	Mon Mar 29 17:30:41 2010 +0200
     1.3 @@ -27,12 +27,6 @@
     1.4      None => None
     1.5    | Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
     1.6  
     1.7 -definition yieldn :: "code_numeral => 'a dseq => code_numeral => bool => 'a list * 'a dseq"
     1.8 -where
     1.9 -  "yieldn n dseq i pol = (case eval dseq i pol of
    1.10 -    None => ([], %i pol. None)
    1.11 -  | Some s => let (xs, s') = Lazy_Sequence.yieldn n s in (xs, %i pol. Some s))"
    1.12 -
    1.13  fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
    1.14  where
    1.15    "map_seq f xq i pol = (case Lazy_Sequence.yield xq of
    1.16 @@ -91,8 +85,11 @@
    1.17  
    1.18  type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
    1.19  
    1.20 -val yieldn = @{code yieldn}
    1.21  val yield = @{code yield}
    1.22 +fun yieldn n s d pol = case s d pol of  
    1.23 +    NONE => ([], fn d => fn pol => NONE)
    1.24 +  | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
    1.25 +
    1.26  val map = @{code map}
    1.27  
    1.28  end;
     2.1 --- a/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:40 2010 +0200
     2.2 +++ b/src/HOL/Lazy_Sequence.thy	Mon Mar 29 17:30:41 2010 +0200
     2.3 @@ -20,15 +20,6 @@
     2.4    "yield Empty = None"
     2.5  | "yield (Insert x xq) = Some (x, xq)"
     2.6  
     2.7 -fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence"
     2.8 -where
     2.9 -  "yieldn i S = (if i = 0 then ([], S) else
    2.10 -    case yield S of
    2.11 -      None => ([], S)
    2.12 -    | Some (x, S') => let
    2.13 -       (xs, S'') = yieldn (i - 1) S'
    2.14 -      in (x # xs, S''))"
    2.15 -
    2.16  lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
    2.17  by (cases xq) auto
    2.18  
    2.19 @@ -141,7 +132,14 @@
    2.20  
    2.21  val yield = @{code yield}
    2.22  
    2.23 -val yieldn = @{code yieldn}
    2.24 +fun anamorph f k x = (if k = 0 then ([], x)
    2.25 +  else case f x
    2.26 +   of NONE => ([], x)
    2.27 +    | SOME (v, y) => let
    2.28 +        val (vs, z) = anamorph f (k - 1) y
    2.29 +      in (v :: vs, z) end);
    2.30 +
    2.31 +fun yieldn S = anamorph yield S;
    2.32  
    2.33  val map = @{code map}
    2.34  
    2.35 @@ -155,7 +153,7 @@
    2.36  code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
    2.37  
    2.38  hide (open) type lazy_sequence
    2.39 -hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
    2.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
    2.41 +hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq not_seq
    2.42 +hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
    2.43  
    2.44  end