1.1 --- a/src/HOL/Predicate.thy	Tue Apr 21 15:48:02 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Wed Apr 22 19:09:19 2009 +0200
     1.3 @@ -622,19 +622,38 @@
     1.4    "pred_rec f P = f (eval P)"
     1.5    by (cases P) simp
     1.6  
     1.7 -export_code Seq in Eval module_name Predicate
     1.8 +text {* for evaluation of predicate enumerations *}
     1.9  
    1.10  ML {*
    1.11  signature PREDICATE =
    1.12  sig
    1.13    datatype 'a pred = Seq of (unit -> 'a seq)
    1.14    and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq
    1.15 +  val yield: 'a pred -> ('a * 'a pred) option
    1.16 +  val yieldn: int -> 'a pred -> 'a list * 'a pred
    1.17  end;
    1.18  
    1.19  structure Predicate : PREDICATE =
    1.20  struct
    1.21  
    1.22 -open Predicate;
    1.23 +@{code_datatype pred = Seq};
    1.24 +@{code_datatype seq = Empty | Insert | Join};
    1.25 +
    1.26 +fun yield (Seq f) = next (f ())
    1.27 +and next @{code Empty} = NONE
    1.28 +  | next (@{code Insert} (x, P)) = SOME (x, P)
    1.29 +  | next (@{code Join} (P, xq)) = (case yield P
    1.30 +     of NONE => next xq
    1.31 +      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))))
    1.32 +
    1.33 +fun anamorph f k x = (if k = 0 then ([], x)
    1.34 +  else case f x
    1.35 +   of NONE => ([], x)
    1.36 +    | SOME (v, y) => let
    1.37 +        val (vs, z) = anamorph f (k - 1) y
    1.38 +      in (v :: vs, z) end)
    1.39 +
    1.40 +fun yieldn P = anamorph yield P;
    1.41  
    1.42  end;
    1.43  *}
    1.44 @@ -647,6 +666,7 @@
    1.45  code_const Seq and Empty and Insert and Join
    1.46    (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
    1.47  
    1.48 +
    1.49  no_notation
    1.50    inf (infixl "\<sqinter>" 70) and
    1.51    sup (infixl "\<squnion>" 65) and