renamed 'vset_rel' to 'rel_vset'
authorblanchet
Thu Mar 06 15:10:56 2014 +0100 (2014-03-06)
changeset 559407339ef350739
parent 55939 682fc100dbff
child 55941 a6a380edbec5
renamed 'vset_rel' to 'rel_vset'
NEWS
src/HOL/Library/Quotient_Set.thy
     1.1 --- a/NEWS	Thu Mar 06 14:57:15 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 15:10:56 2014 +0100
     1.3 @@ -193,9 +193,10 @@
     1.4  * The following map functions and relators have been renamed:
     1.5      sum_map ~> map_sum
     1.6      map_pair ~> map_prod
     1.7 -    fset_rel ~> rel_fset
     1.8 -    cset_rel ~> rel_cset
     1.9 +    fset_rel ~> rel_fset (in "Library/FSet.thy")
    1.10 +    cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
    1.11      set_rel ~> rel_set
    1.12 +    rel_vset ~> vset_rel (in "Library/Quotient_Set.thy")
    1.13  
    1.14  * New theory:
    1.15      Cardinals/Ordinal_Arithmetic.thy
     2.1 --- a/src/HOL/Library/Quotient_Set.thy	Thu Mar 06 14:57:15 2014 +0100
     2.2 +++ b/src/HOL/Library/Quotient_Set.thy	Thu Mar 06 15:10:56 2014 +0100
     2.3 @@ -10,47 +10,47 @@
     2.4  
     2.5  subsection {* Contravariant set map (vimage) and set relator, rules for the Quotient package *}
     2.6  
     2.7 -definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     2.8 +definition "rel_vset R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     2.9  
    2.10 -lemma vset_rel_eq [id_simps]:
    2.11 -  "vset_rel op = = op ="
    2.12 -  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff vset_rel_def)
    2.13 +lemma rel_vset_eq [id_simps]:
    2.14 +  "rel_vset op = = op ="
    2.15 +  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff rel_vset_def)
    2.16  
    2.17 -lemma vset_rel_equivp:
    2.18 +lemma rel_vset_equivp:
    2.19    assumes e: "equivp R"
    2.20 -  shows "vset_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    2.21 -  unfolding vset_rel_def
    2.22 +  shows "rel_vset R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    2.23 +  unfolding rel_vset_def
    2.24    using equivp_reflp[OF e]
    2.25    by auto (metis, metis equivp_symp[OF e])
    2.26  
    2.27  lemma set_quotient [quot_thm]:
    2.28    assumes "Quotient3 R Abs Rep"
    2.29 -  shows "Quotient3 (vset_rel R) (vimage Rep) (vimage Abs)"
    2.30 +  shows "Quotient3 (rel_vset R) (vimage Rep) (vimage Abs)"
    2.31  proof (rule Quotient3I)
    2.32    from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
    2.33    then show "\<And>xs. Rep -` (Abs -` xs) = xs"
    2.34      unfolding vimage_def by auto
    2.35  next
    2.36 -  show "\<And>xs. vset_rel R (Abs -` xs) (Abs -` xs)"
    2.37 -    unfolding vset_rel_def vimage_def
    2.38 +  show "\<And>xs. rel_vset R (Abs -` xs) (Abs -` xs)"
    2.39 +    unfolding rel_vset_def vimage_def
    2.40      by auto (metis Quotient3_rel_abs[OF assms])+
    2.41  next
    2.42    fix r s
    2.43 -  show "vset_rel R r s = (vset_rel R r r \<and> vset_rel R s s \<and> Rep -` r = Rep -` s)"
    2.44 -    unfolding vset_rel_def vimage_def set_eq_iff
    2.45 +  show "rel_vset R r s = (rel_vset R r r \<and> rel_vset R s s \<and> Rep -` r = Rep -` s)"
    2.46 +    unfolding rel_vset_def vimage_def set_eq_iff
    2.47      by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
    2.48  qed
    2.49  
    2.50 -declare [[mapQ3 set = (vset_rel, set_quotient)]]
    2.51 +declare [[mapQ3 set = (rel_vset, set_quotient)]]
    2.52  
    2.53  lemma empty_set_rsp[quot_respect]:
    2.54 -  "vset_rel R {} {}"
    2.55 -  unfolding vset_rel_def by simp
    2.56 +  "rel_vset R {} {}"
    2.57 +  unfolding rel_vset_def by simp
    2.58  
    2.59  lemma collect_rsp[quot_respect]:
    2.60    assumes "Quotient3 R Abs Rep"
    2.61 -  shows "((R ===> op =) ===> vset_rel R) Collect Collect"
    2.62 -  by (intro fun_relI) (simp add: fun_rel_def vset_rel_def)
    2.63 +  shows "((R ===> op =) ===> rel_vset R) Collect Collect"
    2.64 +  by (intro fun_relI) (simp add: fun_rel_def rel_vset_def)
    2.65  
    2.66  lemma collect_prs[quot_preserve]:
    2.67    assumes "Quotient3 R Abs Rep"
    2.68 @@ -60,8 +60,8 @@
    2.69  
    2.70  lemma union_rsp[quot_respect]:
    2.71    assumes "Quotient3 R Abs Rep"
    2.72 -  shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<union> op \<union>"
    2.73 -  by (intro fun_relI) (simp add: vset_rel_def)
    2.74 +  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<union> op \<union>"
    2.75 +  by (intro fun_relI) (simp add: rel_vset_def)
    2.76  
    2.77  lemma union_prs[quot_preserve]:
    2.78    assumes "Quotient3 R Abs Rep"
    2.79 @@ -71,8 +71,8 @@
    2.80  
    2.81  lemma diff_rsp[quot_respect]:
    2.82    assumes "Quotient3 R Abs Rep"
    2.83 -  shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op - op -"
    2.84 -  by (intro fun_relI) (simp add: vset_rel_def)
    2.85 +  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op - op -"
    2.86 +  by (intro fun_relI) (simp add: rel_vset_def)
    2.87  
    2.88  lemma diff_prs[quot_preserve]:
    2.89    assumes "Quotient3 R Abs Rep"
    2.90 @@ -82,8 +82,8 @@
    2.91  
    2.92  lemma inter_rsp[quot_respect]:
    2.93    assumes "Quotient3 R Abs Rep"
    2.94 -  shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<inter> op \<inter>"
    2.95 -  by (intro fun_relI) (auto simp add: vset_rel_def)
    2.96 +  shows "(rel_vset R ===> rel_vset R ===> rel_vset R) op \<inter> op \<inter>"
    2.97 +  by (intro fun_relI) (auto simp add: rel_vset_def)
    2.98  
    2.99  lemma inter_prs[quot_preserve]:
   2.100    assumes "Quotient3 R Abs Rep"
   2.101 @@ -97,7 +97,7 @@
   2.102    by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
   2.103  
   2.104  lemma mem_rsp[quot_respect]:
   2.105 -  shows "(R ===> vset_rel R ===> op =) op \<in> op \<in>"
   2.106 -  by (intro fun_relI) (simp add: vset_rel_def)
   2.107 +  shows "(R ===> rel_vset R ===> op =) op \<in> op \<in>"
   2.108 +  by (intro fun_relI) (simp add: rel_vset_def)
   2.109  
   2.110  end