# HG changeset patch
# User krauss
# Date 1315687397 -7200
# Node ID 045fedcfadf6e80c3f41601ab4881b3247d86477
# Parent  0d23a8ae14df28e92b768fb73058486e489fe5cf
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)

diff -r 0d23a8ae14df -r 045fedcfadf6 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Sat Sep 10 22:43:17 2011 +0200
@@ -76,10 +76,20 @@
 
 lemma mem_prs[quot_preserve]:
   assumes "Quotient R Abs Rep"
+  shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>"
+using Quotient_abs_rep[OF assms]
+by(simp add: fun_eq_iff mem_def)
+
+lemma mem_rsp[quot_respect]:
+  "(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)"
+  by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE)
+
+lemma mem_prs2:
+  assumes "Quotient R Abs Rep"
   shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
   by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
 
-lemma mem_rsp[quot_respect]:
+lemma mem_rsp2:
   shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
   by (intro fun_relI) (simp add: set_rel_def)