# HG changeset patch
# User bulwahn
# Date 1285317102 -7200
# Node ID 6fcd95367c67150b7be9831e030a58be8648c6a2
# Parent  632bcdb80d8858e739bab85d23c5478cdd8a02e2# Parent  9e3b035841e4ba3b4b4bca691a8b2152b93a197d
merged

diff -r 632bcdb80d88 -r 6fcd95367c67 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Sep 24 08:12:10 2010 +0200
+++ b/src/HOL/Quotient.thy	Fri Sep 24 10:31:42 2010 +0200
@@ -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