# HG changeset patch
# User haftmann
# Date 1314375813 -7200
# Node ID 4d39b032a02191832d36f23cc848a16ca14872c2
# Parent  4a36624c3db68eb088e1ce31851b1759a2cdce86
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)

diff -r 4a36624c3db6 -r 4d39b032a021 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Aug 25 23:32:12 2011 +0200
+++ b/src/HOL/Quotient.thy	Fri Aug 26 18:23:33 2011 +0200
@@ -35,12 +35,11 @@
 definition
   Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
 where
-  "Respects R x = R x x"
+  "Respects R = {x. R x x}"
 
 lemma in_respects:
   shows "x \<in> Respects R \<longleftrightarrow> R x x"
-  unfolding mem_def Respects_def
-  by simp
+  unfolding Respects_def by simp
 
 subsection {* Function map and function relation *}
 
@@ -268,14 +267,14 @@
   by (auto simp add: in_respects)
 
 lemma ball_reg_right:
-  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+  assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
   shows "All P \<longrightarrow> Ball R Q"
-  using a by (metis Collect_def Collect_mem_eq)
+  using a by (metis Collect_mem_eq)
 
 lemma bex_reg_left:
-  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+  assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
   shows "Bex R Q \<longrightarrow> Ex P"
-  using a by (metis Collect_def Collect_mem_eq)
+  using a by (metis Collect_mem_eq)
 
 lemma ball_reg_left:
   assumes a: "equivp R"
@@ -327,16 +326,16 @@
   using a b by metis
 
 lemma ball_reg:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   and     b: "Ball R P"
   shows "Ball R Q"
-  using a b by (metis Collect_def Collect_mem_eq)
+  using a b by (metis Collect_mem_eq)
 
 lemma bex_reg:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   and     b: "Bex R P"
   shows "Bex R Q"
-  using a b by (metis Collect_def Collect_mem_eq)
+  using a b by (metis Collect_mem_eq)
 
 
 lemma ball_all_comm:
@@ -599,16 +598,6 @@
   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
   by (auto intro!: fun_relI elim: fun_relE)
 
-lemma mem_rsp:
-  shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
-  by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
-
-lemma mem_prs:
-  assumes a1: "Quotient R1 Abs1 Rep1"
-  and     a2: "Quotient R2 Abs2 Rep2"
-  shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
-  by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
-
 lemma id_rsp:
   shows "(R ===> R) id id"
   by (auto intro: fun_relI)
@@ -686,8 +675,8 @@
 declare [[map set = (vimage, set_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
-lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs
+lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
+lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
 lemmas [quot_equiv] = identity_equivp