# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1285310038 -32400
# Node ID 9e3b035841e4ba3b4b4bca691a8b2152b93a197d
# Parent  9d554d257a1075107d4fb0d6ad87a671e1db1daf
quotient package: respectfulness and preservation of identity.

diff -r 9d554d257a10 -r 9e3b035841e4 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Thu Sep 23 21:17:11 2010 +0200
+++ b/src/HOL/Quotient.thy	Fri Sep 24 15:33:58 2010 +0900
@@ -661,6 +661,17 @@
   shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
   by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
 
+lemma id_rsp:
+  shows "(R ===> R) id id"
+  by simp
+
+lemma id_prs:
+  assumes a: "Quotient R Abs Rep"
+  shows "(Rep ---> Abs) id = id"
+  unfolding fun_eq_iff
+  by (simp add: Quotient_abs_rep[OF a])
+
+
 locale quot_type =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -731,8 +742,8 @@
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp
-lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs
+lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
+lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs
 lemmas [quot_equiv] = identity_equivp