# HG changeset patch # User wenzelm # Date 1315690138 -7200 # Node ID cd60c421b0291c17e81d9d51b8c7994613e27611 # Parent 045fedcfadf6e80c3f41601ab4881b3247d86477# Parent a98ef45122f3eaecb2ecc2fefc15869b8ffc668c merged diff -r a98ef45122f3 -r cd60c421b029 src/HOL/Library/Quotient_Set.thy --- a/src/HOL/Library/Quotient_Set.thy Sat Sep 10 23:27:32 2011 +0200 +++ b/src/HOL/Library/Quotient_Set.thy Sat Sep 10 23:28:58 2011 +0200 @@ -76,10 +76,20 @@ lemma mem_prs[quot_preserve]: assumes "Quotient R Abs Rep" + shows "(Rep ---> (Abs ---> id) ---> id) (op \) = op \" +using Quotient_abs_rep[OF assms] +by(simp add: fun_eq_iff mem_def) + +lemma mem_rsp[quot_respect]: + "(R ===> (R ===> op =) ===> op =) (op \) (op \)" + by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE) + +lemma mem_prs2: + assumes "Quotient R Abs Rep" shows "(Rep ---> op -` Abs ---> id) op \ = op \" by (simp add: fun_eq_iff Quotient_abs_rep[OF assms]) -lemma mem_rsp[quot_respect]: +lemma mem_rsp2: shows "(R ===> set_rel R ===> op =) op \ op \" by (intro fun_relI) (simp add: set_rel_def)