# HG changeset patch
# User haftmann
# Date 1292855845 -3600
# Node ID de0c906dfe60663438f0da54d8113a29ce22b20f
# Parent  c7699379a72f1cfc188b86db5f4a2955871631e0
type_lifting for predicates

diff -r c7699379a72f -r de0c906dfe60 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Dec 20 09:45:26 2010 +0100
+++ b/src/HOL/Predicate.thy	Mon Dec 20 15:37:25 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"