1.1 --- a/src/HOL/Lifting.thy	Thu Apr 05 15:23:26 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 05 15:59:25 2012 +0200
     1.3 @@ -297,6 +297,31 @@
     1.4    show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
     1.5  qed
     1.6  
     1.7 +text {* Generating transfer rules for quotients. *}
     1.8 +
     1.9 +lemma Quotient_right_unique:
    1.10 +  assumes "Quotient R Abs Rep T" shows "right_unique T"
    1.11 +  using assms unfolding Quotient_alt_def right_unique_def by metis
    1.12 +
    1.13 +lemma Quotient_right_total:
    1.14 +  assumes "Quotient R Abs Rep T" shows "right_total T"
    1.15 +  using assms unfolding Quotient_alt_def right_total_def by metis
    1.16 +
    1.17 +lemma Quotient_rel_eq_transfer:
    1.18 +  assumes "Quotient R Abs Rep T"
    1.19 +  shows "(T ===> T ===> op =) R (op =)"
    1.20 +  using assms unfolding Quotient_alt_def fun_rel_def by simp
    1.21 +
    1.22 +lemma Quotient_bi_total:
    1.23 +  assumes "Quotient R Abs Rep T" and "reflp R"
    1.24 +  shows "bi_total T"
    1.25 +  using assms unfolding Quotient_alt_def bi_total_def reflp_def by auto
    1.26 +
    1.27 +lemma Quotient_id_abs_transfer:
    1.28 +  assumes "Quotient R Abs Rep T" and "reflp R"
    1.29 +  shows "(op = ===> T) (\<lambda>x. x) Abs"
    1.30 +  using assms unfolding Quotient_alt_def reflp_def fun_rel_def by simp
    1.31 +
    1.32  text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
    1.33  
    1.34  lemma typedef_bi_unique: