diff -r 1f0ec5b8135a -r e455cdaac479 src/HOL/Lifting.thy --- a/src/HOL/Lifting.thy Wed Apr 18 15:09:07 2012 +0200 +++ b/src/HOL/Lifting.thy Wed Apr 18 15:48:32 2012 +0200 @@ -201,6 +201,14 @@ "equivp R \ reflp R" by (erule equivpE) +subsection {* Respects predicate *} + +definition Respects :: "('a \ 'a \ bool) \ 'a set" + where "Respects R = {x. R x x}" + +lemma in_respects: "x \ Respects R \ R x x" + unfolding Respects_def by simp + subsection {* Invariant *} definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" @@ -300,6 +308,22 @@ assumes "\y. R y y \ P (Abs y)" shows "P x" using 1 assms unfolding Quotient_def by metis +lemma Quotient_All_transfer: + "((T ===> op =) ===> op =) (Ball (Respects R)) All" + unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] + by (auto, metis Quotient_abs_induct) + +lemma Quotient_Ex_transfer: + "((T ===> op =) ===> op =) (Bex (Respects R)) Ex" + unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] + by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1]) + +lemma Quotient_forall_transfer: + "((T ===> op =) ===> op =) (transfer_bforall (\x. R x x)) transfer_forall" + using Quotient_All_transfer + unfolding transfer_forall_def transfer_bforall_def + Ball_def [abs_def] in_respects . + end text {* Generating transfer rules for total quotients. *}