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>"