# HG changeset patch # User Cezary Kaliszyk # Date 1283150673 -32400 # Node ID 27c7b620758cf0e972fba22428afd15cf09a2bed # Parent 749d09f52fde5df5f715f9c6a3a0694b09a96e0b Quotient Package: added respectfulness and preservation lemmas for mem. diff -r 749d09f52fde -r 27c7b620758c src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Sat Aug 28 21:17:25 2010 +0800 +++ b/src/HOL/Quotient.thy Mon Aug 30 15:44:33 2010 +0900 @@ -651,6 +651,16 @@ shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" by auto +lemma mem_rsp: + shows "(R1 ===> (R1 ===> R2) ===> R2) op \ op \" + by (simp add: mem_def) + +lemma mem_prs: + assumes a1: "Quotient R1 Abs1 Rep1" + and a2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \ = op \" + by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2]) + locale quot_type = fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" @@ -721,8 +731,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 -lemmas [quot_preserve] = if_prs o_prs let_prs +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_equiv] = identity_equivp