# HG changeset patch
# User huffman
# Date 1336144357 -7200
# Node ID 29212a4bb866adc5f8f94a85602acb8dbcd65f81
# Parent  45bf22d8a81d88edc5d6c28dfece85d11a6449d6
lifting package produces abs_eq_iff rules for total quotients

diff -r 45bf22d8a81d -r 29212a4bb866 src/HOL/Lifting.thy
--- 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"}. *}
diff -r 45bf22d8a81d -r 29212a4bb866 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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}])