--- a/src/HOL/Lifting.thy Fri May 04 11:08:31 2012 +0200
+++ b/src/HOL/Lifting.thy Fri May 04 17:12:37 2012 +0200
@@ -310,6 +310,9 @@
lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
+lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \<longleftrightarrow> R x y"
+ using Quotient_rel [OF 1] 2 unfolding reflp_def by simp
+
end
text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 04 11:08:31 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri May 04 17:12:37 2012 +0200
@@ -115,6 +115,8 @@
[[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
|> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
+ |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
+ [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
| NONE => lthy
|> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
[quot_thm RS @{thm Quotient_All_transfer}])