1.1 --- a/src/HOL/Lifting.thy	Thu Apr 19 09:58:54 2012 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 19 08:45:13 2012 +0200
     1.3 @@ -339,6 +339,9 @@
     1.4  lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
     1.5    using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp
     1.6  
     1.7 +lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
     1.8 +  using 1 2 assms unfolding Quotient_alt_def reflp_def by metis
     1.9 +
    1.10  end
    1.11  
    1.12  text {* Generating transfer rules for a type defined with @{text "typedef"}. *}

     2.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 09:58:54 2012 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 19 08:45:13 2012 +0200
     2.3 @@ -96,6 +96,7 @@
     2.4    let
     2.5      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     2.6      val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
     2.7 +    val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
     2.8      val qty_name = (Binding.name o fst o dest_Type) qty
     2.9      fun qualify suffix = Binding.qualified true suffix qty_name
    2.10      val lthy' = case maybe_reflp_thm of
    2.11 @@ -104,6 +105,8 @@
    2.12            [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
    2.13          |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
    2.14            [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
    2.15 +        |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
    2.16 +          [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
    2.17        | NONE => lthy
    2.18          |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
    2.19            [quot_thm RS @{thm Quotient_All_transfer}])
    2.20 @@ -111,6 +114,8 @@
    2.21            [quot_thm RS @{thm Quotient_Ex_transfer}])
    2.22          |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
    2.23            [quot_thm RS @{thm Quotient_forall_transfer}])
    2.24 +        |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
    2.25 +          [quot_thm RS @{thm Quotient_abs_induct}])
    2.26    in
    2.27      lthy'
    2.28        |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),