1.1 --- a/src/HOL/Lifting.thy	Wed Apr 18 14:34:25 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 18 14:59:04 2012 +0200
     1.3 @@ -282,28 +282,36 @@
     1.4  
     1.5  text {* Generating transfer rules for quotients. *}
     1.6  
     1.7 -lemma Quotient_right_unique:
     1.8 -  assumes "Quotient R Abs Rep T" shows "right_unique T"
     1.9 -  using assms unfolding Quotient_alt_def right_unique_def by metis
    1.10 +context
    1.11 +  fixes R Abs Rep T
    1.12 +  assumes 1: "Quotient R Abs Rep T"
    1.13 +begin
    1.14  
    1.15 -lemma Quotient_right_total:
    1.16 -  assumes "Quotient R Abs Rep T" shows "right_total T"
    1.17 -  using assms unfolding Quotient_alt_def right_total_def by metis
    1.18 +lemma Quotient_right_unique: "right_unique T"
    1.19 +  using 1 unfolding Quotient_alt_def right_unique_def by metis
    1.20  
    1.21 -lemma Quotient_rel_eq_transfer:
    1.22 -  assumes "Quotient R Abs Rep T"
    1.23 -  shows "(T ===> T ===> op =) R (op =)"
    1.24 -  using assms unfolding Quotient_alt_def fun_rel_def by simp
    1.25 +lemma Quotient_right_total: "right_total T"
    1.26 +  using 1 unfolding Quotient_alt_def right_total_def by metis
    1.27  
    1.28 -lemma Quotient_bi_total:
    1.29 -  assumes "Quotient R Abs Rep T" and "reflp R"
    1.30 -  shows "bi_total T"
    1.31 -  using assms unfolding Quotient_alt_def bi_total_def reflp_def by auto
    1.32 +lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
    1.33 +  using 1 unfolding Quotient_alt_def fun_rel_def by simp
    1.34  
    1.35 -lemma Quotient_id_abs_transfer:
    1.36 -  assumes "Quotient R Abs Rep T" and "reflp R"
    1.37 -  shows "(op = ===> T) (\<lambda>x. x) Abs"
    1.38 -  using assms unfolding Quotient_alt_def reflp_def fun_rel_def by simp
    1.39 +end
    1.40 +
    1.41 +text {* Generating transfer rules for total quotients. *}
    1.42 +
    1.43 +context
    1.44 +  fixes R Abs Rep T
    1.45 +  assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
    1.46 +begin
    1.47 +
    1.48 +lemma Quotient_bi_total: "bi_total T"
    1.49 +  using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
    1.50 +
    1.51 +lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
    1.52 +  using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
    1.53 +
    1.54 +end
    1.55  
    1.56  text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
    1.57  
    1.58 @@ -341,6 +349,8 @@
    1.59  
    1.60  end
    1.61  
    1.62 +text {* Generating transfer rules for a type copy. *}
    1.63 +
    1.64  lemma copy_type_bi_total:
    1.65    assumes type: "type_definition Rep Abs UNIV"
    1.66    assumes T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"