1.1 --- a/src/HOL/Predicate.thy	Mon May 11 09:39:53 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Mon May 11 17:20:52 2009 +0200
     1.3 @@ -625,7 +625,56 @@
     1.4  inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
     1.5  
     1.6  lemma eq_is_eq: "eq x y \<equiv> (x = y)"
     1.7 -by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
     1.8 +  by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
     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 +@{code_datatype pred = Seq};
    1.23 +@{code_datatype seq = Empty | Insert | Join};
    1.24 +
    1.25 +fun yield (Seq f) = next (f ())
    1.26 +and next @{code Empty} = NONE
    1.27 +  | next (@{code Insert} (x, P)) = SOME (x, P)
    1.28 +  | next (@{code Join} (P, xq)) = (case yield P
    1.29 +     of NONE => next xq
    1.30 +      | SOME (x, Q) => SOME (x, @{code Seq} (fn _ => @{code Join} (Q, xq))))
    1.31 +
    1.32 +fun anamorph f k x = (if k = 0 then ([], x)
    1.33 +  else case f x
    1.34 +   of NONE => ([], x)
    1.35 +    | SOME (v, y) => let
    1.36 +        val (vs, z) = anamorph f (k - 1) y
    1.37 +      in (v :: vs, z) end)
    1.38 +
    1.39 +fun yieldn P = anamorph yield P;
    1.40 +
    1.41 +end;
    1.42 +*}
    1.43 +
    1.44 +code_reserved Eval Predicate
    1.45 +
    1.46 +code_type pred and seq
    1.47 +  (Eval "_/ Predicate.pred" and "_/ Predicate.seq")
    1.48 +
    1.49 +code_const Seq and Empty and Insert and Join
    1.50 +  (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)")
    1.51 +
    1.52 +text {* dummy setup for code_pred keyword *}
    1.53 +
    1.54 +ML {*
    1.55 +OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
    1.56 +  OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]])))
    1.57 +*}
    1.58  
    1.59  no_notation
    1.60    inf (infixl "\<sqinter>" 70) and
    1.61 @@ -640,12 +689,4 @@
    1.62  hide (open) const Pred eval single bind if_pred not_pred
    1.63    Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
    1.64  
    1.65 -text {* dummy setup for code_pred keyword *}
    1.66 -
    1.67 -ML {*
    1.68 -OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
    1.69 -  OuterKeyword.thy_goal (OuterParse.term_group >> (K (Proof.theorem_i NONE (K I) [[]])))
    1.70 -*}
    1.71 -
    1.72 -
    1.73  end