# HG changeset patch # User Cezary Kaliszyk # 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 \ = op \" 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 \ 'a \ bool" and Abs :: "('a \ bool) \ '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