--- a/NEWS Thu Mar 06 14:57:15 2014 +0100
+++ b/NEWS Thu Mar 06 15:10:56 2014 +0100
@@ -193,9 +193,10 @@
* The following map functions and relators have been renamed:
sum_map ~> map_sum
map_pair ~> map_prod
- fset_rel ~> rel_fset
- cset_rel ~> rel_cset
+ fset_rel ~> rel_fset (in "Library/FSet.thy")
+ cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
set_rel ~> rel_set
+ rel_vset ~> vset_rel (in "Library/Quotient_Set.thy")
* New theory:
Cardinals/Ordinal_Arithmetic.thy
--- a/src/HOL/Library/Quotient_Set.thy Thu Mar 06 14:57:15 2014 +0100
+++ b/src/HOL/Library/Quotient_Set.thy Thu Mar 06 15:10:56 2014 +0100
@@ -10,47 +10,47 @@
subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *}
-definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
+definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
-lemma vset_rel_eq [id_simps]:
- "vset_rel op = = op ="
- by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff vset_rel_def)
+lemma rel_vset_eq [id_simps]:
+ "rel_vset op = = op ="
+ by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)
-lemma vset_rel_equivp:
+lemma rel_vset_equivp:
assumes e: "equivp R"
- shows "vset_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
- unfolding vset_rel_def
+ shows "rel_vset R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
+ unfolding rel_vset_def
using equivp_reflp[OF e]
by auto (metis, metis equivp_symp[OF e])
lemma set_quotient [quot_thm]:
assumes "Quotient3 R Abs Rep"
- shows "Quotient3 (vset_rel R) (vimage Rep) (vimage Abs)"
+ shows "Quotient3 (rel_vset 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. vset_rel R (Abs -` xs) (Abs -` xs)"
- unfolding vset_rel_def vimage_def
+ show "\<And>xs. rel_vset R (Abs -` xs) (Abs -` xs)"
+ unfolding rel_vset_def vimage_def
by auto (metis Quotient3_rel_abs[OF assms])+
next
fix r s
- show "vset_rel R r s = (vset_rel R r r \<and> vset_rel R s s \<and> Rep -` r = Rep -` s)"
- unfolding vset_rel_def vimage_def set_eq_iff
+ show "rel_vset R r s = (rel_vset R r r \<and> rel_vset R s s \<and> Rep -` r = Rep -` s)"
+ unfolding rel_vset_def vimage_def set_eq_iff
by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
qed
-declare [[mapQ3 set = (vset_rel, set_quotient)]]
+declare [[mapQ3 set = (rel_vset, set_quotient)]]
lemma empty_set_rsp[quot_respect]:
- "vset_rel R {} {}"
- unfolding vset_rel_def by simp
+ "rel_vset R {} {}"
+ unfolding rel_vset_def by simp
lemma collect_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
- shows "((R ===> op =) ===> vset_rel R) Collect Collect"
- by (intro fun_relI) (simp add: fun_rel_def vset_rel_def)
+ shows "((R ===> op =) ===> rel_vset R) Collect Collect"
+ by (intro fun_relI) (simp add: fun_rel_def rel_vset_def)
lemma collect_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -60,8 +60,8 @@
lemma union_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
- shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<union> op \<union>"
- by (intro fun_relI) (simp add: vset_rel_def)
+ shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
+ by (intro fun_relI) (simp add: rel_vset_def)
lemma union_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -71,8 +71,8 @@
lemma diff_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
- shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op - op -"
- by (intro fun_relI) (simp add: vset_rel_def)
+ shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
+ by (intro fun_relI) (simp add: rel_vset_def)
lemma diff_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -82,8 +82,8 @@
lemma inter_rsp[quot_respect]:
assumes "Quotient3 R Abs Rep"
- shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<inter> op \<inter>"
- by (intro fun_relI) (auto simp add: vset_rel_def)
+ shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
+ by (intro fun_relI) (auto simp add: rel_vset_def)
lemma inter_prs[quot_preserve]:
assumes "Quotient3 R Abs Rep"
@@ -97,7 +97,7 @@
by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
lemma mem_rsp[quot_respect]:
- shows "(R ===> vset_rel R ===> op =) op \<in> op \<in>"
- by (intro fun_relI) (simp add: vset_rel_def)
+ shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
+ by (intro fun_relI) (simp add: rel_vset_def)
end