# HG changeset patch
# User haftmann
# Date 1292862718 -3600
# Node ID 054a4e5ac5fb1ab4321de312bc6571571b3bd82e
# Parent  65631ca437c9d1c96bd82781e516d510ee4f11b0# Parent  de0c906dfe60663438f0da54d8113a29ce22b20f
merged

diff -r 65631ca437c9 -r 054a4e5ac5fb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Dec 20 16:44:33 2010 +0100
+++ b/src/HOL/Predicate.thy	Mon Dec 20 17:31:58 2010 +0100
@@ -788,6 +788,17 @@
 unfolding is_empty_def holds_eq
 by (rule unit_pred_cases) (auto elim: botE intro: singleI)
 
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
+  "map f P = P \<guillemotright>= (single o f)"
+
+lemma eval_map [simp]:
+  "eval (map f P) = image f (eval P)"
+  by (auto simp add: map_def)
+
+type_lifting map
+  by (auto intro!: pred_eqI simp add: image_image)
+
+
 subsubsection {* Implementation *}
 
 datatype 'a seq = Empty | Insert "'a" "'a pred" | Join "'a pred" "'a seq"
@@ -925,9 +936,6 @@
 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)"
-
 primrec null :: "'a seq \<Rightarrow> bool" where
     "null Empty \<longleftrightarrow> True"
   | "null (Insert x P) \<longleftrightarrow> False"