1.1 --- a/src/HOL/Lifting.thy	Wed Apr 18 15:09:07 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 18 15:48:32 2012 +0200
     1.3 @@ -201,6 +201,14 @@
     1.4    "equivp R \<Longrightarrow> reflp R"
     1.5    by (erule equivpE)
     1.6  
     1.7 +subsection {* Respects predicate *}
     1.8 +
     1.9 +definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
    1.10 +  where "Respects R = {x. R x x}"
    1.11 +
    1.12 +lemma in_respects: "x \<in> Respects R \<longleftrightarrow> R x x"
    1.13 +  unfolding Respects_def by simp
    1.14 +
    1.15  subsection {* Invariant *}
    1.16  
    1.17  definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
    1.18 @@ -300,6 +308,22 @@
    1.19    assumes "\<And>y. R y y \<Longrightarrow> P (Abs y)" shows "P x"
    1.20    using 1 assms unfolding Quotient_def by metis
    1.21  
    1.22 +lemma Quotient_All_transfer:
    1.23 +  "((T ===> op =) ===> op =) (Ball (Respects R)) All"
    1.24 +  unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
    1.25 +  by (auto, metis Quotient_abs_induct)
    1.26 +
    1.27 +lemma Quotient_Ex_transfer:
    1.28 +  "((T ===> op =) ===> op =) (Bex (Respects R)) Ex"
    1.29 +  unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1]
    1.30 +  by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1])
    1.31 +
    1.32 +lemma Quotient_forall_transfer:
    1.33 +  "((T ===> op =) ===> op =) (transfer_bforall (\<lambda>x. R x x)) transfer_forall"
    1.34 +  using Quotient_All_transfer
    1.35 +  unfolding transfer_forall_def transfer_bforall_def
    1.36 +    Ball_def [abs_def] in_respects .
    1.37 +
    1.38  end
    1.39  
    1.40  text {* Generating transfer rules for total quotients. *}

     2.1 --- a/src/HOL/Quotient.thy	Wed Apr 18 15:09:07 2012 +0200
     2.2 +++ b/src/HOL/Quotient.thy	Wed Apr 18 15:48:32 2012 +0200
     2.3 @@ -34,17 +34,6 @@
     2.4    shows "((op =) OOO R) = R"
     2.5    by (auto simp add: fun_eq_iff)
     2.6  
     2.7 -subsection {* Respects predicate *}
     2.8 -
     2.9 -definition
    2.10 -  Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
    2.11 -where
    2.12 -  "Respects R = {x. R x x}"
    2.13 -
    2.14 -lemma in_respects:
    2.15 -  shows "x \<in> Respects R \<longleftrightarrow> R x x"
    2.16 -  unfolding Respects_def by simp
    2.17 -
    2.18  subsection {* set map (vimage) and set relation *}
    2.19  
    2.20  definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"