quotient package: respectfulness and preservation of identity.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri Sep 24 15:33:58 2010 +0900 (2010-09-24)
changeset 396699e3b035841e4
parent 39668 9d554d257a10
child 39671 6fcd95367c67
child 39672 a89040dd6416
quotient package: respectfulness and preservation of identity.
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Quotient.thy	Thu Sep 23 21:17:11 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Fri Sep 24 15:33:58 2010 +0900
     1.3 @@ -661,6 +661,17 @@
     1.4    shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
     1.5    by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
     1.6  
     1.7 +lemma id_rsp:
     1.8 +  shows "(R ===> R) id id"
     1.9 +  by simp
    1.10 +
    1.11 +lemma id_prs:
    1.12 +  assumes a: "Quotient R Abs Rep"
    1.13 +  shows "(Rep ---> Abs) id = id"
    1.14 +  unfolding fun_eq_iff
    1.15 +  by (simp add: Quotient_abs_rep[OF a])
    1.16 +
    1.17 +
    1.18  locale quot_type =
    1.19    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.20    and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
    1.21 @@ -731,8 +742,8 @@
    1.22  declare [[map "fun" = (fun_map, fun_rel)]]
    1.23  
    1.24  lemmas [quot_thm] = fun_quotient
    1.25 -lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp
    1.26 -lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs
    1.27 +lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
    1.28 +lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs
    1.29  lemmas [quot_equiv] = identity_equivp
    1.30  
    1.31