--- a/src/HOL/Lifting.thy Wed Apr 04 14:27:20 2012 +0200
+++ b/src/HOL/Lifting.thy Wed Apr 04 12:25:58 2012 +0200
@@ -252,6 +252,16 @@
shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
by (rule identity_equivp)
+lemma typedef_to_Quotient:
+ assumes "type_definition Rep Abs {x. P x}"
+ and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
+ shows "Quotient (invariant P) Abs Rep T"
+proof -
+ interpret type_definition Rep Abs "{x. P x}" by fact
+ from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
+ by (auto intro!: QuotientI simp: invariant_def fun_eq_iff)
+qed
+
lemma invariant_type_to_Quotient:
assumes "type_definition Rep Abs {x. P x}"
and T_def: "T \<equiv> (\<lambda>x y. (invariant P) x x \<and> Abs x = y)"