src/HOL/Quotient.thy
changeset 44413 80d460bc6fa8
parent 44242 a5cb6aa77ffc
child 44553 4d39b032a021
     1.1 --- a/src/HOL/Quotient.thy	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Tue Aug 23 03:34:17 2011 +0900
     1.3 @@ -69,6 +69,24 @@
     1.4    shows "((op =) ===> (op =)) = (op =)"
     1.5    by (auto simp add: fun_eq_iff elim: fun_relE)
     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 vimage_id:
    1.12 +  "vimage id = id"
    1.13 +  unfolding vimage_def fun_eq_iff by auto
    1.14 +
    1.15 +lemma set_rel_eq:
    1.16 +  "set_rel op = = op ="
    1.17 +  by (subst fun_eq_iff, subst fun_eq_iff) (simp add: set_eq_iff set_rel_def)
    1.18 +
    1.19 +lemma set_rel_equivp:
    1.20 +  assumes e: "equivp R"
    1.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)"
    1.22 +  unfolding set_rel_def
    1.23 +  using equivp_reflp[OF e]
    1.24 +  by auto (metis equivp_symp[OF e])+
    1.25  
    1.26  subsection {* Quotient Predicate *}
    1.27  
    1.28 @@ -665,6 +683,7 @@
    1.29  setup Quotient_Info.setup
    1.30  
    1.31  declare [[map "fun" = (map_fun, fun_rel)]]
    1.32 +declare [[map set = (vimage, set_rel)]]
    1.33  
    1.34  lemmas [quot_thm] = fun_quotient
    1.35  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
    1.36 @@ -680,6 +699,8 @@
    1.37    id_o
    1.38    o_id
    1.39    eq_comp_r
    1.40 +  set_rel_eq
    1.41 +  vimage_id
    1.42  
    1.43  text {* Translation functions for the lifting process. *}
    1.44  use "Tools/Quotient/quotient_term.ML"