src/HOL/Library/Quotient_Set.thy

--- a/src/HOL/Library/Quotient_Set.thy	Tue Apr 03 14:09:37 2012 +0200
+++ b/src/HOL/Library/Quotient_Set.thy	Tue Apr 03 16:26:48 2012 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Quotient_Set.thy
+(*  Title:      HOL/Library/Quotient3_Set.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
@@ -9,77 +9,77 @@
 begin
 
 lemma set_quotient [quot_thm]:
-  assumes "Quotient R Abs Rep"
-  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
-proof (rule QuotientI)
-  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
+  assumes "Quotient3 R Abs Rep"
+  shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
+proof (rule Quotient3I)
+  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
   then show "\<And>xs. Rep -` (Abs -` xs) = xs"
     unfolding vimage_def by auto
 next
   show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
     unfolding set_rel_def vimage_def
-    by auto (metis Quotient_rel_abs[OF assms])+
+    by auto (metis Quotient3_rel_abs[OF assms])+
 next
   fix r s
   show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
     unfolding set_rel_def vimage_def set_eq_iff
-    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
+    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
 qed
 
-declare [[map set = (set_rel, set_quotient)]]
+declare [[mapQ3 set = (set_rel, set_quotient)]]
 
 lemma empty_set_rsp[quot_respect]:
   "set_rel R {} {}"
   unfolding set_rel_def by simp
 
 lemma collect_rsp[quot_respect]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "((R ===> op =) ===> set_rel R) Collect Collect"
   by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
 
 lemma collect_prs[quot_preserve]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
   unfolding fun_eq_iff
-  by (simp add: Quotient_abs_rep[OF assms])
+  by (simp add: Quotient3_abs_rep[OF assms])
 
 lemma union_rsp[quot_respect]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
   by (intro fun_relI) (simp add: set_rel_def)
 
 lemma union_prs[quot_preserve]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
   unfolding fun_eq_iff
-  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
 
 lemma diff_rsp[quot_respect]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
   by (intro fun_relI) (simp add: set_rel_def)
 
 lemma diff_prs[quot_preserve]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
   unfolding fun_eq_iff
-  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
+  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
 
 lemma inter_rsp[quot_respect]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
   by (intro fun_relI) (auto simp add: set_rel_def)
 
 lemma inter_prs[quot_preserve]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
   unfolding fun_eq_iff
-  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
+  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
 
 lemma mem_prs[quot_preserve]:
-  assumes "Quotient R Abs Rep"
+  assumes "Quotient3 R Abs Rep"
   shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
-  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
+  by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
 
 lemma mem_rsp[quot_respect]:
   shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"