# HG changeset patch
# User berghofe
# Date 1210150599 -7200
# Node ID a6cb51c314f2ab56125e2b58eeddc3a250927b27
# Parent  c554b77061e5fb377cd8728c276c5ee33d8712e9
- Added mem_def and predicate1I in some of the proofs
- pred_equals_eq and pred_subset_eq are no longer used in the conversion
  between sets and predicates, because sets and predicates can no longer
  be distinguished

diff -r c554b77061e5 -r a6cb51c314f2 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed May 07 10:56:38 2008 +0200
+++ b/src/HOL/Predicate.thy	Wed May 07 10:56:39 2008 +0200
@@ -11,14 +11,14 @@
 
 subsection {* Equality and Subsets *}
 
-lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
-  by (auto simp add: expand_fun_eq)
+lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
+  by (simp add: mem_def)
 
 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
-  by (auto simp add: expand_fun_eq)
+  by (simp add: expand_fun_eq mem_def)
 
-lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
-  by fast
+lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
+  by (simp add: mem_def)
 
 lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
   by fast
@@ -264,7 +264,7 @@
 inductive_cases DomainPE [elim!]: "DomainP r a"
 
 lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
-  by (blast intro!: Orderings.order_antisym)
+  by (blast intro!: Orderings.order_antisym predicate1I)
 
 
 subsection {* Range *}
@@ -278,7 +278,7 @@
 inductive_cases RangePE [elim!]: "RangeP r b"
 
 lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
-  by (blast intro!: Orderings.order_antisym)
+  by (blast intro!: Orderings.order_antisym predicate1I)
 
 
 subsection {* Inverse image *}
@@ -302,6 +302,8 @@
 lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   by (auto simp add: Powp_def expand_fun_eq)
 
+lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
+
 
 subsection {* Properties of relations - predicate versions *}