src/HOL/Library/Quotient_Set.thy
 changeset 47308 9caab698dbe4 parent 47094 1a7ad2601cb5 child 47455 26315a545e26
```     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Tue Apr 03 14:09:37 2012 +0200
1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Tue Apr 03 16:26:48 2012 +0200
1.3 @@ -1,4 +1,4 @@
1.4 -(*  Title:      HOL/Library/Quotient_Set.thy
1.5 +(*  Title:      HOL/Library/Quotient3_Set.thy
1.6      Author:     Cezary Kaliszyk and Christian Urban
1.7  *)
1.8
1.9 @@ -9,77 +9,77 @@
1.10  begin
1.11
1.12  lemma set_quotient [quot_thm]:
1.13 -  assumes "Quotient R Abs Rep"
1.14 -  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
1.15 -proof (rule QuotientI)
1.16 -  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
1.17 +  assumes "Quotient3 R Abs Rep"
1.18 +  shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
1.19 +proof (rule Quotient3I)
1.20 +  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
1.21    then show "\<And>xs. Rep -` (Abs -` xs) = xs"
1.22      unfolding vimage_def by auto
1.23  next
1.24    show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
1.25      unfolding set_rel_def vimage_def
1.26 -    by auto (metis Quotient_rel_abs[OF assms])+
1.27 +    by auto (metis Quotient3_rel_abs[OF assms])+
1.28  next
1.29    fix r s
1.30    show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
1.31      unfolding set_rel_def vimage_def set_eq_iff
1.32 -    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
1.33 +    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
1.34  qed
1.35
1.36 -declare [[map set = (set_rel, set_quotient)]]
1.37 +declare [[mapQ3 set = (set_rel, set_quotient)]]
1.38
1.39  lemma empty_set_rsp[quot_respect]:
1.40    "set_rel R {} {}"
1.41    unfolding set_rel_def by simp
1.42
1.43  lemma collect_rsp[quot_respect]:
1.44 -  assumes "Quotient R Abs Rep"
1.45 +  assumes "Quotient3 R Abs Rep"
1.46    shows "((R ===> op =) ===> set_rel R) Collect Collect"
1.47    by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
1.48
1.49  lemma collect_prs[quot_preserve]:
1.50 -  assumes "Quotient R Abs Rep"
1.51 +  assumes "Quotient3 R Abs Rep"
1.52    shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
1.53    unfolding fun_eq_iff
1.54 -  by (simp add: Quotient_abs_rep[OF assms])
1.55 +  by (simp add: Quotient3_abs_rep[OF assms])
1.56
1.57  lemma union_rsp[quot_respect]:
1.58 -  assumes "Quotient R Abs Rep"
1.59 +  assumes "Quotient3 R Abs Rep"
1.60    shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
1.61    by (intro fun_relI) (simp add: set_rel_def)
1.62
1.63  lemma union_prs[quot_preserve]:
1.64 -  assumes "Quotient R Abs Rep"
1.65 +  assumes "Quotient3 R Abs Rep"
1.66    shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
1.67    unfolding fun_eq_iff
1.68 -  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
1.69 +  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
1.70
1.71  lemma diff_rsp[quot_respect]:
1.72 -  assumes "Quotient R Abs Rep"
1.73 +  assumes "Quotient3 R Abs Rep"
1.74    shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
1.75    by (intro fun_relI) (simp add: set_rel_def)
1.76
1.77  lemma diff_prs[quot_preserve]:
1.78 -  assumes "Quotient R Abs Rep"
1.79 +  assumes "Quotient3 R Abs Rep"
1.80    shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
1.81    unfolding fun_eq_iff
1.82 -  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
1.83 +  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
1.84
1.85  lemma inter_rsp[quot_respect]:
1.86 -  assumes "Quotient R Abs Rep"
1.87 +  assumes "Quotient3 R Abs Rep"
1.88    shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
1.89    by (intro fun_relI) (auto simp add: set_rel_def)
1.90
1.91  lemma inter_prs[quot_preserve]:
1.92 -  assumes "Quotient R Abs Rep"
1.93 +  assumes "Quotient3 R Abs Rep"
1.94    shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
1.95    unfolding fun_eq_iff
1.96 -  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
1.97 +  by (simp add: Quotient3_abs_rep[OF set_quotient[OF assms]])
1.98
1.99  lemma mem_prs[quot_preserve]:
1.100 -  assumes "Quotient R Abs Rep"
1.101 +  assumes "Quotient3 R Abs Rep"
1.102    shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
1.103 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
1.104 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
1.105
1.106  lemma mem_rsp[quot_respect]:
1.107    shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
```