1.1 --- a/src/HOL/Lifting.thy	Wed Apr 04 16:29:17 2012 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Wed Apr 04 17:51:12 2012 +0200
     1.3 @@ -236,16 +236,17 @@
     1.4    shows "invariant P x x \<equiv> P x"
     1.5  using assms by (auto simp add: invariant_def)
     1.6  
     1.7 -lemma copy_type_to_Quotient:
     1.8 +lemma UNIV_typedef_to_Quotient:
     1.9    assumes "type_definition Rep Abs UNIV"
    1.10 -  and T_def: "T \<equiv> (\<lambda>x y. Abs x = y)"
    1.11 +  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.12    shows "Quotient (op =) Abs Rep T"
    1.13  proof -
    1.14    interpret type_definition Rep Abs UNIV by fact
    1.15 -  from Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI)
    1.16 +  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
    1.17 +    by (fastforce intro!: QuotientI fun_eq_iff)
    1.18  qed
    1.19  
    1.20 -lemma copy_type_to_equivp:
    1.21 +lemma UNIV_typedef_to_equivp:
    1.22    fixes Abs :: "'a \<Rightarrow> 'b"
    1.23    and Rep :: "'b \<Rightarrow> 'a"
    1.24    assumes "type_definition Rep Abs (UNIV::'a set)"
    1.25 @@ -253,6 +254,28 @@
    1.26  by (rule identity_equivp)
    1.27  
    1.28  lemma typedef_to_Quotient:
    1.29 +  assumes "type_definition Rep Abs S"
    1.30 +  and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.31 +  shows "Quotient (Lifting.invariant (\<lambda>x. x \<in> S)) Abs Rep T"
    1.32 +proof -
    1.33 +  interpret type_definition Rep Abs S by fact
    1.34 +  from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
    1.35 +    by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
    1.36 +qed
    1.37 +
    1.38 +lemma typedef_to_part_equivp:
    1.39 +  assumes "type_definition Rep Abs S"
    1.40 +  shows "part_equivp (Lifting.invariant (\<lambda>x. x \<in> S))"
    1.41 +proof (intro part_equivpI)
    1.42 +  interpret type_definition Rep Abs S by fact
    1.43 +  show "\<exists>x. Lifting.invariant (\<lambda>x. x \<in> S) x x" using Rep by (auto simp: invariant_def)
    1.44 +next
    1.45 +  show "symp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: sympI simp: invariant_def)
    1.46 +next
    1.47 +  show "transp (Lifting.invariant (\<lambda>x. x \<in> S))" by (auto intro: transpI simp: invariant_def)
    1.48 +qed
    1.49 +
    1.50 +lemma open_typedef_to_Quotient:
    1.51    assumes "type_definition Rep Abs {x. P x}"
    1.52    and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
    1.53    shows "Quotient (invariant P) Abs Rep T"
    1.54 @@ -262,16 +285,7 @@
    1.55      by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
    1.56  qed
    1.57  
    1.58 -lemma invariant_type_to_Quotient:
    1.59 -  assumes "type_definition Rep Abs {x. P x}"
    1.60 -  and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"
    1.61 -  shows "Quotient (invariant P) Abs Rep T"
    1.62 -proof -
    1.63 -  interpret type_definition Rep Abs "{x. P x}" by fact
    1.64 -  from Rep Abs_inject Rep_inverse T_def show ?thesis by (auto intro!: QuotientI simp: invariant_def)
    1.65 -qed
    1.66 -
    1.67 -lemma invariant_type_to_part_equivp:
    1.68 +lemma open_typedef_to_part_equivp:
    1.69    assumes "type_definition Rep Abs {x. P x}"
    1.70    shows "part_equivp (invariant P)"
    1.71  proof (intro part_equivpI)