# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1314151162 -32400
# Node ID 079ccfb074d95a26ce839947398e8e325279329b
# Parent  f8c2def19f8422a91e0a4a2ef80fbec42a1d030e
Quotient Package: add mem_rsp, mem_prs, tune proofs.

diff -r f8c2def19f84 -r 079ccfb074d9 src/HOL/Library/Quotient_Set.thy
--- a/src/HOL/Library/Quotient_Set.thy	Tue Aug 23 15:46:53 2011 -0700
+++ b/src/HOL/Library/Quotient_Set.thy	Wed Aug 24 10:59:22 2011 +0900
@@ -33,7 +33,7 @@
 lemma collect_rsp[quot_respect]:
   assumes "Quotient R Abs Rep"
   shows "((R ===> op =) ===> set_rel R) Collect Collect"
-  by (auto intro!: fun_relI simp add: fun_rel_def set_rel_def)
+  by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
 
 lemma collect_prs[quot_preserve]:
   assumes "Quotient R Abs Rep"
@@ -44,7 +44,7 @@
 lemma union_rsp[quot_respect]:
   assumes "Quotient R Abs Rep"
   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
-  by (intro fun_relI) (auto simp add: set_rel_def)
+  by (intro fun_relI) (simp add: set_rel_def)
 
 lemma union_prs[quot_preserve]:
   assumes "Quotient R Abs Rep"
@@ -55,7 +55,7 @@
 lemma diff_rsp[quot_respect]:
   assumes "Quotient R Abs Rep"
   shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
-  by (intro fun_relI) (auto simp add: set_rel_def)
+  by (intro fun_relI) (simp add: set_rel_def)
 
 lemma diff_prs[quot_preserve]:
   assumes "Quotient R Abs Rep"
@@ -74,4 +74,13 @@
   unfolding fun_eq_iff
   by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
 
+lemma mem_prs[quot_preserve]:
+  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]:
+  shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
+  by (intro fun_relI) (simp add: set_rel_def)
+
 end