src/HOL/Library/Quotient_Set.thy
changeset 47626 f7b1034cb9ce
parent 47455 26315a545e26
child 47647 ec29cc09599d
equal deleted inserted replaced
47625:10cfaf771687 47626:f7b1034cb9ce
     5 header {* Quotient infrastructure for the set type *}
     5 header {* Quotient infrastructure for the set type *}
     6 
     6 
     7 theory Quotient_Set
     7 theory Quotient_Set
     8 imports Main Quotient_Syntax
     8 imports Main Quotient_Syntax
     9 begin
     9 begin
       
    10 
       
    11 subsection {* set map (vimage) and set relation *}
       
    12 
       
    13 definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
       
    14 
       
    15 lemma set_rel_eq [id_simps]:
       
    16   "set_rel op = = op ="
       
    17   by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
       
    18 
       
    19 lemma set_rel_equivp:
       
    20   assumes e: "equivp R"
       
    21   shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
       
    22   unfolding set_rel_def
       
    23   using equivp_reflp[OF e]
       
    24   by auto (metis, metis equivp_symp[OF e])
    10 
    25 
    11 lemma set_quotient [quot_thm]:
    26 lemma set_quotient [quot_thm]:
    12   assumes "Quotient3 R Abs Rep"
    27   assumes "Quotient3 R Abs Rep"
    13   shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
    28   shows "Quotient3 (set_rel R) (vimage Rep) (vimage Abs)"
    14 proof (rule Quotient3I)
    29 proof (rule Quotient3I)