src/HOL/Quotient.thy
changeset 39669 9e3b035841e4
parent 39302 d7728f65b353
child 39946 78faa9b31202
     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