--- a/etc/isar-keywords.el Wed Apr 04 14:27:20 2012 +0200
+++ b/etc/isar-keywords.el Wed Apr 04 12:25:58 2012 +0200
@@ -129,6 +129,7 @@
"lemma"
"lemmas"
"let"
+ "lift_definition"
"linear_undo"
"local_setup"
"locale"
@@ -570,6 +571,7 @@
"instance"
"interpretation"
"lemma"
+ "lift_definition"
"nominal_inductive"
"nominal_inductive2"
"nominal_primrec"
--- 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)"