1.1 --- a/src/HOL/Predicate.thy	Sun Aug 21 22:04:01 2011 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Sun Aug 21 22:56:55 2011 +0200
     1.3 @@ -25,7 +25,6 @@
     1.4  
     1.5  subsection {* Predicates as (complete) lattices *}
     1.6  
     1.7 -
     1.8  text {*
     1.9    Handy introduction and elimination rules for @{text "\<le>"}
    1.10    on unary and binary predicates
    1.11 @@ -423,14 +422,6 @@
    1.12    "(\<And>w. eval P w \<longleftrightarrow> eval Q w) \<Longrightarrow> P = Q"
    1.13    by (cases P, cases Q) (auto simp add: fun_eq_iff)
    1.14  
    1.15 -lemma eval_mem [simp]:
    1.16 -  "x \<in> eval P \<longleftrightarrow> eval P x"
    1.17 -  by (simp add: mem_def)
    1.18 -
    1.19 -lemma eq_mem [simp]:
    1.20 -  "x \<in> (op =) y \<longleftrightarrow> x = y"
    1.21 -  by (auto simp add: mem_def)
    1.22 -
    1.23  instantiation pred :: (type) complete_lattice
    1.24  begin
    1.25  
    1.26 @@ -798,11 +789,11 @@
    1.27    "map f P = P \<guillemotright>= (single o f)"
    1.28  
    1.29  lemma eval_map [simp]:
    1.30 -  "eval (map f P) = image f (eval P)"
    1.31 +  "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
    1.32    by (auto simp add: map_def)
    1.33  
    1.34  enriched_type map: map
    1.35 -  by (auto intro!: pred_eqI simp add: fun_eq_iff image_compose)
    1.36 +  by (rule ext, rule pred_eqI, auto)+
    1.37  
    1.38  
    1.39  subsubsection {* Implementation *}
    1.40 @@ -1040,6 +1031,14 @@
    1.41  end;
    1.42  *}
    1.43  
    1.44 +lemma eval_mem [simp]:
    1.45 +  "x \<in> eval P \<longleftrightarrow> eval P x"
    1.46 +  by (simp add: mem_def)
    1.47 +
    1.48 +lemma eq_mem [simp]:
    1.49 +  "x \<in> (op =) y \<longleftrightarrow> x = y"
    1.50 +  by (auto simp add: mem_def)
    1.51 +
    1.52  no_notation
    1.53    bot ("\<bottom>") and
    1.54    top ("\<top>") and