move definition of set_rel into Library/Quotient_Set.thy
authorhuffman
Fri Apr 20 15:34:33 2012 +0200 (2012-04-20)
changeset 47626f7b1034cb9ce
parent 47625 10cfaf771687
child 47627 2b1d3eda59eb
move definition of set_rel into Library/Quotient_Set.thy
src/HOL/Library/Quotient_Set.thy
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Library/Quotient_Set.thy	Fri Apr 20 15:30:13 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Set.thy	Fri Apr 20 15:34:33 2012 +0200
     1.3 @@ -8,6 +8,21 @@
     1.4  imports Main Quotient_Syntax
     1.5  begin
     1.6  
     1.7 +subsection {* set map (vimage) and set relation *}
     1.8 +
     1.9 +definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
    1.10 +
    1.11 +lemma set_rel_eq [id_simps]:
    1.12 +  "set_rel op = = op ="
    1.13 +  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
    1.14 +
    1.15 +lemma set_rel_equivp:
    1.16 +  assumes e: "equivp R"
    1.17 +  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.18 +  unfolding set_rel_def
    1.19 +  using equivp_reflp[OF e]
    1.20 +  by auto (metis, metis equivp_symp[OF e])
    1.21 +
    1.22  lemma set_quotient [quot_thm]:
    1.23    assumes "Quotient3 R Abs Rep"
    1.24    shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
     2.1 --- a/src/HOL/Quotient.thy	Fri Apr 20 15:30:13 2012 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Fri Apr 20 15:34:33 2012 +0200
     2.3 @@ -34,21 +34,6 @@
     2.4    shows "((op =) OOO R) = R"
     2.5    by (auto simp add: fun_eq_iff)
     2.6  
     2.7 -subsection {* set map (vimage) and set relation *}
     2.8 -
     2.9 -definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
    2.10 -
    2.11 -lemma set_rel_eq:
    2.12 -  "set_rel op = = op ="
    2.13 -  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
    2.14 -
    2.15 -lemma set_rel_equivp:
    2.16 -  assumes e: "equivp R"
    2.17 -  shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    2.18 -  unfolding set_rel_def
    2.19 -  using equivp_reflp[OF e]
    2.20 -  by auto (metis, metis equivp_symp[OF e])
    2.21 -
    2.22  subsection {* Quotient Predicate *}
    2.23  
    2.24  definition
    2.25 @@ -799,7 +784,6 @@
    2.26    id_o
    2.27    o_id
    2.28    eq_comp_r
    2.29 -  set_rel_eq
    2.30    vimage_id
    2.31  
    2.32  text {* Translation functions for the lifting process. *}