# HG changeset patch
# User huffman
# Date 1334817913 -7200
# Node ID b90cd7016d4f331264535a94d7bf88065c837d0c
# Parent  6b362107e6d99894717e83b35a33a3b9491a3dbc
generate abs_induct rules for quotient types

diff -r 6b362107e6d9 -r b90cd7016d4f src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Thu Apr 19 09:58:54 2012 +0200
+++ b/src/HOL/Lifting.thy	Thu Apr 19 08:45:13 2012 +0200
@@ -339,6 +339,9 @@
 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
   using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
 
+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
+
 end
 
 text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
diff -r 6b362107e6d9 -r b90cd7016d4f src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 09:58:54 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 08:45:13 2012 +0200
@@ -96,6 +96,7 @@
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
+    val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
     val qty_name = (Binding.name o fst o dest_Type) qty
     fun qualify suffix = Binding.qualified true suffix qty_name
     val lthy' = case maybe_reflp_thm of
@@ -104,6 +105,8 @@
           [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
         |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
           [[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}])
       | NONE => lthy
         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
           [quot_thm RS @{thm Quotient_All_transfer}])
@@ -111,6 +114,8 @@
           [quot_thm RS @{thm Quotient_Ex_transfer}])
         |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
           [quot_thm RS @{thm Quotient_forall_transfer}])
+        |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
+          [quot_thm RS @{thm Quotient_abs_induct}])
   in
     lthy'
       |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),