src/HOL/Predicate.thy

 inductive eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where "eq x x"
 
 lemma eq_is_eq: "eq x y \<equiv> (x = y)"
   by (rule eq_reflection) (auto intro: eq.intros elim: eq.cases)
 
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
+  "map f P = P \<guillemotright>= (single o f)"
+
 ML {*
 signature PREDICATE =
 sig
   datatype 'a pred = Seq of (unit -> 'a seq)
   and 'a seq = Empty | Insert of 'a * 'a pred | Join of 'a pred * 'a seq

 in
 
 val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
   OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]])));
 
-val _ = OuterSyntax.improper_command "values" "evaluate and print enumerations"
+val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions"
   OuterKeyword.diag ((opt_modes -- P.term)
     >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep
         (K ())));
 
 end

   bot ("\<bottom>") and
   bind (infixl "\<guillemotright>=" 70)
 
 hide (open) type pred seq
 hide (open) const Pred eval single bind if_pred not_pred
-  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq
+  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
 
 end