# HG changeset patch
# User haftmann
# Date 1313960215 -7200
# Node ID 78c43fb3adb05358f7669ebdc22a24735a821b65
# Parent  36598b3eb20973476bce6c8f3b01ac2ed09333a4# Parent  53f4f82876064122db4c0a004eef97f472284d21
avoid pred/set mixture

diff -r 36598b3eb209 -r 78c43fb3adb0 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sun Aug 21 22:04:01 2011 +0200
+++ b/src/HOL/Predicate.thy	Sun Aug 21 22:56:55 2011 +0200
@@ -25,7 +25,6 @@
 
 subsection {* Predicates as (complete) lattices *}
 
-
 text {*
   Handy introduction and elimination rules for @{text "\<le>"}
   on unary and binary predicates
@@ -423,14 +422,6 @@
   "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q"
   by (cases P, cases Q) (auto simp add: fun_eq_iff)
 
-lemma eval_mem [simp]:
-  "x \<in> eval P \<longleftrightarrow> eval P x"
-  by (simp add: mem_def)
-
-lemma eq_mem [simp]:
-  "x \<in> (op =) y \<longleftrightarrow> x = y"
-  by (auto simp add: mem_def)
-
 instantiation pred :: (type) complete_lattice
 begin
 
@@ -798,11 +789,11 @@
   "map f P = P \<guillemotright>= (single o f)"
 
 lemma eval_map [simp]:
-  "eval (map f P) = image f (eval P)"
+  "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
   by (auto simp add: map_def)
 
 enriched_type map: map
-  by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
+  by (rule ext, rule pred_eqI, auto)+
 
 
 subsubsection {* Implementation *}
@@ -1040,6 +1031,14 @@
 end;
 *}
 
+lemma eval_mem [simp]:
+  "x \<in> eval P \<longleftrightarrow> eval P x"
+  by (simp add: mem_def)
+
+lemma eq_mem [simp]:
+  "x \<in> (op =) y \<longleftrightarrow> x = y"
+  by (auto simp add: mem_def)
+
 no_notation
   bot ("\<bottom>") and
   top ("\<top>") and