src/HOL/Library/Quotient_Set.thy
changeset 47647 ec29cc09599d
parent 47626 f7b1034cb9ce
child 47648 6b9d20a095ae
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 11:15:49 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Sat Apr 21 10:59:52 2012 +0200
     1.3 @@ -10,47 +10,47 @@
     1.4  
     1.5  subsection {* set map (vimage) and set relation *}
     1.6  
     1.7 -definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     1.8 +definition "vset_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
     1.9  
    1.10 -lemma set_rel_eq [id_simps]:
    1.11 -  "set_rel op = = op ="
    1.12 -  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
    1.13 +lemma vset_rel_eq [id_simps]:
    1.14 +  "vset_rel op = = op ="
    1.15 +  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff vset_rel_def)
    1.16  
    1.17 -lemma set_rel_equivp:
    1.18 +lemma vset_rel_equivp:
    1.19    assumes e: "equivp R"
    1.20 -  shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    1.21 -  unfolding set_rel_def
    1.22 +  shows "vset_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    1.23 +  unfolding vset_rel_def
    1.24    using equivp_reflp[OF e]
    1.25    by auto (metis, metis equivp_symp[OF e])
    1.26  
    1.27  lemma set_quotient [quot_thm]:
    1.28    assumes "Quotient3 R Abs Rep"
    1.29 -  shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
    1.30 +  shows "Quotient3 (vset_rel R) (vimage Rep) (vimage Abs)"
    1.31  proof (rule Quotient3I)
    1.32    from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient3_abs_rep)
    1.33    then show "\<And>xs. Rep -` (Abs -` xs) = xs"
    1.34      unfolding vimage_def by auto
    1.35  next
    1.36 -  show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
    1.37 -    unfolding set_rel_def vimage_def
    1.38 +  show "\<And>xs. vset_rel R (Abs -` xs) (Abs -` xs)"
    1.39 +    unfolding vset_rel_def vimage_def
    1.40      by auto (metis Quotient3_rel_abs[OF assms])+
    1.41  next
    1.42    fix r s
    1.43 -  show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
    1.44 -    unfolding set_rel_def vimage_def set_eq_iff
    1.45 +  show "vset_rel R r s = (vset_rel R r r \<and> vset_rel R s s \<and> Rep -` r = Rep -` s)"
    1.46 +    unfolding vset_rel_def vimage_def set_eq_iff
    1.47      by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient3_def])+
    1.48  qed
    1.49  
    1.50 -declare [[mapQ3 set = (set_rel, set_quotient)]]
    1.51 +declare [[mapQ3 set = (vset_rel, set_quotient)]]
    1.52  
    1.53  lemma empty_set_rsp[quot_respect]:
    1.54 -  "set_rel R {} {}"
    1.55 -  unfolding set_rel_def by simp
    1.56 +  "vset_rel R {} {}"
    1.57 +  unfolding vset_rel_def by simp
    1.58  
    1.59  lemma collect_rsp[quot_respect]:
    1.60    assumes "Quotient3 R Abs Rep"
    1.61 -  shows "((R ===> op =) ===> set_rel R) Collect Collect"
    1.62 -  by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
    1.63 +  shows "((R ===> op =) ===> vset_rel R) Collect Collect"
    1.64 +  by (intro fun_relI) (simp add: fun_rel_def vset_rel_def)
    1.65  
    1.66  lemma collect_prs[quot_preserve]:
    1.67    assumes "Quotient3 R Abs Rep"
    1.68 @@ -60,8 +60,8 @@
    1.69  
    1.70  lemma union_rsp[quot_respect]:
    1.71    assumes "Quotient3 R Abs Rep"
    1.72 -  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
    1.73 -  by (intro fun_relI) (simp add: set_rel_def)
    1.74 +  shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<union> op \<union>"
    1.75 +  by (intro fun_relI) (simp add: vset_rel_def)
    1.76  
    1.77  lemma union_prs[quot_preserve]:
    1.78    assumes "Quotient3 R Abs Rep"
    1.79 @@ -71,8 +71,8 @@
    1.80  
    1.81  lemma diff_rsp[quot_respect]:
    1.82    assumes "Quotient3 R Abs Rep"
    1.83 -  shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
    1.84 -  by (intro fun_relI) (simp add: set_rel_def)
    1.85 +  shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op - op -"
    1.86 +  by (intro fun_relI) (simp add: vset_rel_def)
    1.87  
    1.88  lemma diff_prs[quot_preserve]:
    1.89    assumes "Quotient3 R Abs Rep"
    1.90 @@ -82,8 +82,8 @@
    1.91  
    1.92  lemma inter_rsp[quot_respect]:
    1.93    assumes "Quotient3 R Abs Rep"
    1.94 -  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
    1.95 -  by (intro fun_relI) (auto simp add: set_rel_def)
    1.96 +  shows "(vset_rel R ===> vset_rel R ===> vset_rel R) op \<inter> op \<inter>"
    1.97 +  by (intro fun_relI) (auto simp add: vset_rel_def)
    1.98  
    1.99  lemma inter_prs[quot_preserve]:
   1.100    assumes "Quotient3 R Abs Rep"
   1.101 @@ -97,7 +97,7 @@
   1.102    by (simp add: fun_eq_iff Quotient3_abs_rep[OF assms])
   1.103  
   1.104  lemma mem_rsp[quot_respect]:
   1.105 -  shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
   1.106 -  by (intro fun_relI) (simp add: set_rel_def)
   1.107 +  shows "(R ===> vset_rel R ===> op =) op \<in> op \<in>"
   1.108 +  by (intro fun_relI) (simp add: vset_rel_def)
   1.109  
   1.110  end