generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem

--- a/src/HOL/Quotient.thy	Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Quotient.thy	Fri Mar 23 14:25:31 2012 +0100
@@ -9,6 +9,7 @@
 keywords
   "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
   "quotient_type" :: thy_goal and "/" and
+  "setup_lifting" :: thy_decl and
   "quotient_definition" :: thy_goal
 uses
   ("Tools/Quotient/quotient_info.ML")
@@ -137,6 +138,18 @@
   unfolding Quotient_def
   by blast
 
+lemma Quotient_refl1: 
+  assumes a: "Quotient R Abs Rep" 
+  shows "R r s \<Longrightarrow> R r r"
+  using a unfolding Quotient_def 
+  by fast
+
+lemma Quotient_refl2: 
+  assumes a: "Quotient R Abs Rep" 
+  shows "R r s \<Longrightarrow> R s s"
+  using a unfolding Quotient_def 
+  by fast
+
 lemma Quotient_rel_rep:
   assumes a: "Quotient R Abs Rep"
   shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
@@ -263,6 +276,15 @@
   shows "R2 (f x) (g y)"
   using a by (auto elim: fun_relE)
 
+lemma apply_rsp'':
+  assumes "Quotient R Abs Rep"
+  and "(R ===> S) f f"
+  shows "S (f (Rep x)) (f (Rep x))"
+proof -
+  from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
+  then show ?thesis using assms(2) by (auto intro: apply_rsp')
+qed
+
 subsection {* lemmas for regularisation of ball and bex *}
 
 lemma ball_reg_eqv:
@@ -679,6 +701,153 @@
 
 end
 
+subsection {* Quotient composition *}
+
+lemma OOO_quotient:
+  fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
+  fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
+  fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
+  assumes R1: "Quotient R1 Abs1 Rep1"
+  assumes R2: "Quotient R2 Abs2 Rep2"
+  assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
+  assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
+  shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+apply (rule QuotientI)
+   apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
+  apply simp
+  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
+   apply (rule Quotient_rep_reflp [OF R1])
+  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
+   apply (rule Quotient_rep_reflp [OF R1])
+  apply (rule Rep1)
+  apply (rule Quotient_rep_reflp [OF R2])
+ apply safe
+    apply (rename_tac x y)
+    apply (drule Abs1)
+      apply (erule Quotient_refl2 [OF R1])
+     apply (erule Quotient_refl1 [OF R1])
+    apply (drule Quotient_refl1 [OF R2], drule Rep1)
+    apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
+     apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
+     apply (erule pred_compI)
+     apply (erule Quotient_symp [OF R1, THEN sympD])
+    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+    apply (rule conjI, erule Quotient_refl1 [OF R1])
+    apply (rule conjI, rule Quotient_rep_reflp [OF R1])
+    apply (subst Quotient_abs_rep [OF R1])
+    apply (erule Quotient_rel_abs [OF R1])
+   apply (rename_tac x y)
+   apply (drule Abs1)
+     apply (erule Quotient_refl2 [OF R1])
+    apply (erule Quotient_refl1 [OF R1])
+   apply (drule Quotient_refl2 [OF R2], drule Rep1)
+   apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
+    apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
+    apply (erule pred_compI)
+    apply (erule Quotient_symp [OF R1, THEN sympD])
+   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+   apply (rule conjI, erule Quotient_refl2 [OF R1])
+   apply (rule conjI, rule Quotient_rep_reflp [OF R1])
+   apply (subst Quotient_abs_rep [OF R1])
+   apply (erule Quotient_rel_abs [OF R1, THEN sym])
+  apply simp
+  apply (rule Quotient_rel_abs [OF R2])
+  apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption)
+  apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption)
+  apply (erule Abs1)
+   apply (erule Quotient_refl2 [OF R1])
+  apply (erule Quotient_refl1 [OF R1])
+ apply (rename_tac a b c d)
+ apply simp
+ apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
+  apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+  apply (rule conjI, erule Quotient_refl1 [OF R1])
+  apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
+ apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
+  apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+  apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
+  apply (erule Quotient_refl2 [OF R1])
+ apply (rule Rep1)
+ apply (drule Abs1)
+   apply (erule Quotient_refl2 [OF R1])
+  apply (erule Quotient_refl1 [OF R1])
+ apply (drule Abs1)
+  apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply simp
+ apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2])
+ apply simp
+done
+
+lemma OOO_eq_quotient:
+  fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
+  fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
+  assumes R1: "Quotient R1 Abs1 Rep1"
+  assumes R2: "Quotient op= Abs2 Rep2"
+  shows "Quotient (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+using assms
+by (rule OOO_quotient) auto
+
+subsection {* Invariant *}
+
+definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
+  where "invariant R = (\<lambda>x y. R x \<and> x = y)"
+
+lemma invariant_to_eq:
+  assumes "invariant P x y"
+  shows "x = y"
+using assms by (simp add: invariant_def)
+
+lemma fun_rel_eq_invariant:
+  shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
+by (auto simp add: invariant_def fun_rel_def)
+
+lemma invariant_same_args:
+  shows "invariant P x x \<equiv> P x"
+using assms by (auto simp add: invariant_def)
+
+lemma copy_type_to_Quotient:
+  assumes "type_definition Rep Abs UNIV"
+  shows "Quotient (op =) Abs Rep"
+proof -
+  interpret type_definition Rep Abs UNIV by fact
+  from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI)
+qed
+
+lemma copy_type_to_equivp:
+  fixes Abs :: "'a \<Rightarrow> 'b"
+  and Rep :: "'b \<Rightarrow> 'a"
+  assumes "type_definition Rep Abs (UNIV::'a set)"
+  shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
+by (rule identity_equivp)
+
+lemma invariant_type_to_Quotient:
+  assumes "type_definition Rep Abs {x. P x}"
+  shows "Quotient (invariant P) Abs Rep"
+proof -
+  interpret type_definition Rep Abs "{x. P x}" by fact
+  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def)
+qed
+
+lemma invariant_type_to_part_equivp:
+  assumes "type_definition Rep Abs {x. P x}"
+  shows "part_equivp (invariant P)"
+proof (intro part_equivpI)
+  interpret type_definition Rep Abs "{x. P x}" by fact
+  show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
+next
+  show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
+next
+  show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
+qed
+
 subsection {* ML setup *}
 
 text {* Auxiliary data for the quotient package *}

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 23 14:25:31 2012 +0100
@@ -27,6 +27,130 @@
 
 (** Interface and Syntax Setup **)
 
+(* Generation of the code certificate from the rsp theorem *)
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+  | get_body_types (U, V)  = (U, V)
+
+fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+  | get_binder_types _ = []
+
+fun unabs_def ctxt def = 
+  let
+    val (_, rhs) = Thm.dest_equals (cprop_of def)
+    fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
+      | dest_abs tm = raise TERM("get_abs_var",[tm])
+    val (var_name, T) = dest_abs (term_of rhs)
+    val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
+    val thy = Proof_Context.theory_of ctxt'
+    val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
+  in
+    Thm.combination def refl_thm |>
+    singleton (Proof_Context.export ctxt' ctxt)
+  end
+
+fun unabs_all_def ctxt def = 
+  let
+    val (_, rhs) = Thm.dest_equals (cprop_of def)
+    val xs = strip_abs_vars (term_of rhs)
+  in  
+    fold (K (unabs_def ctxt)) xs def
+  end
+
+val map_fun_unfolded = 
+  @{thm map_fun_def[abs_def]} |>
+  unabs_def @{context} |>
+  unabs_def @{context} |>
+  Local_Defs.unfold @{context} [@{thm comp_def}]
+
+fun unfold_fun_maps ctm =
+  let
+    fun unfold_conv ctm =
+      case (Thm.term_of ctm) of
+        Const (@{const_name "map_fun"}, _) $ _ $ _ => 
+          (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
+        | _ => Conv.all_conv ctm
+    val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
+  in
+    (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
+  end
+
+fun prove_rel ctxt rsp_thm (rty, qty) =
+  let
+    val ty_args = get_binder_types (rty, qty)
+    fun disch_arg args_ty thm = 
+      let
+        val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty
+      in
+        [quot_thm, thm] MRSL @{thm apply_rsp''}
+      end
+  in
+    fold disch_arg ty_args rsp_thm
+  end
+
+exception CODE_CERT_GEN of string
+
+fun simplify_code_eq ctxt def_thm = 
+  Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
+
+fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
+  let
+    val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
+    val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
+    val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
+    val abs_rep_eq = 
+      case (HOLogic.dest_Trueprop o prop_of) fun_rel of
+        Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
+        | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
+        | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
+    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+    val unabs_def = unabs_all_def ctxt unfolded_def
+    val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm
+    val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
+    val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
+    val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
+  in
+    simplify_code_eq ctxt code_cert
+  end
+
+fun define_code_cert def_thm rsp_thm (rty, qty) lthy = 
+  let
+    val quot_thm = Quotient_Term.prove_quot_theorem lthy (get_body_types (rty, qty))
+  in
+    if Quotient_Type.can_generate_code_cert quot_thm then
+      let
+        val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
+        val add_abs_eqn_attribute = 
+          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
+        val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+      in
+        lthy
+          |> (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert])
+      end
+    else
+      lthy
+  end
+
+fun define_code_eq def_thm lthy =
+  let
+    val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+    val code_eq = unabs_all_def lthy unfolded_def
+    val simp_code_eq = simplify_code_eq lthy code_eq
+  in
+    lthy
+      |> (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [simp_code_eq])
+  end
+
+fun define_code def_thm rsp_thm (rty, qty) lthy =
+  if body_type rty = body_type qty then 
+    define_code_eq def_thm lthy
+  else 
+    define_code_cert def_thm rsp_thm (rty, qty) lthy
+
 (* The ML-interface for a quotient definition takes
    as argument:
 
@@ -52,17 +176,19 @@
 
 fun add_quotient_def ((var, (name, atts)), (lhs, rhs)) rsp_thm lthy =
   let
+    val rty = fastype_of rhs
+    val qty = fastype_of lhs
     val absrep_trm = 
-      Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, fastype_of lhs) $ rhs
+      Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
     val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
     val (_, prop') = Local_Defs.cert_def lthy prop
     val (_, newrhs) = Local_Defs.abs_def prop'
 
-    val ((trm, (_ , thm)), lthy') =
+    val ((trm, (_ , def_thm)), lthy') =
       Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
 
     (* data storage *)
-    val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+    val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
     fun get_rsp_thm_name (lhs_name, _) = Binding.suffix_name "_rsp" lhs_name
     
     val lthy'' = lthy'
@@ -75,6 +201,7 @@
       |> (snd oo Local_Theory.note) 
         ((get_rsp_thm_name var, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
         [rsp_thm])
+      |> define_code def_thm rsp_thm (rty, qty)
 
   in
     (qconst_data, lthy'')
@@ -99,7 +226,8 @@
     fun simp_arrows_conv ctm =
       let
         val unfold_conv = Conv.rewrs_conv 
-          [@{thm fun_rel_eq_rel[THEN eq_reflection]}, @{thm fun_rel_def[THEN eq_reflection]}]
+          [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]}, 
+            @{thm fun_rel_def[THEN eq_reflection]}]
         val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
         fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
       in
@@ -109,11 +237,14 @@
           | _ => Conv.all_conv ctm
       end
 
+    val unfold_ret_val_invs = Conv.bottom_conv 
+      (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy 
     val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
     val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
     val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
+    val beta_conv = Thm.beta_conversion true
     val eq_thm = 
-      (simp_conv then_conv univq_prenex_conv then_conv Thm.beta_conversion true) ctm
+      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   in
     Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
   end

--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Mar 23 14:25:31 2012 +0100
@@ -20,6 +20,9 @@
   val equiv_relation: Proof.context -> typ * typ -> term
   val equiv_relation_chk: Proof.context -> typ * typ -> term
 
+  val get_rel_from_quot_thm: thm -> term
+  val prove_quot_theorem: Proof.context -> typ * typ -> thm
+
   val regularize_trm: Proof.context -> term * term -> term
   val regularize_trm_chk: Proof.context -> term * term -> term
 
@@ -331,6 +334,78 @@
   equiv_relation ctxt (rty, qty)
   |> Syntax.check_term ctxt
 
+(* generation of the Quotient theorem  *)
+
+fun get_quot_thm ctxt s =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in
+    (case Quotient_Info.lookup_quotients_global thy s of
+      SOME qdata => #quot_thm qdata
+    | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
+  end
+
+fun get_rel_quot_thm thy s =
+  (case Quotient_Info.lookup_quotmaps thy s of
+    SOME map_data => #quot_thm map_data
+  | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
+
+fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+exception NOT_IMPL of string
+
+fun get_rel_from_quot_thm quot_thm = 
+  let
+    val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
+  in
+    rel
+  end
+
+fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = 
+  let
+    val quot_thm_rel = get_rel_from_quot_thm quot_thm
+  in
+    if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
+    else raise NOT_IMPL "nested quotients: not implemented yet"
+  end
+
+fun prove_quot_theorem ctxt (rty, qty) =
+  if rty = qty
+  then @{thm identity_quotient}
+  else
+    case (rty, qty) of
+      (Type (s, tys), Type (s', tys')) =>
+        if s = s'
+        then
+          let
+            val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+          in
+            args MRSL (get_rel_quot_thm ctxt s)
+          end
+        else
+          let
+            val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
+            val qtyenv = match ctxt equiv_match_err qty_pat qty
+            val rtys' = map (Envir.subst_type qtyenv) rtys
+            val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
+            val quot_thm = get_quot_thm ctxt s'
+          in
+            if forall is_id_quot args
+            then
+              quot_thm
+            else
+              let
+                val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
+              in
+                mk_quot_thm_compose (rel_quot_thm, quot_thm)
+             end
+          end
+    | _ => @{thm identity_quotient}
+
 
 
 (*** Regularization ***)

--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:21:41 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 23 14:25:31 2012 +0100
@@ -6,6 +6,8 @@
 
 signature QUOTIENT_TYPE =
 sig
+  val can_generate_code_cert: thm -> bool
+  
   val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
     ((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
 
@@ -76,6 +78,44 @@
     Goal.prove lthy [] [] goal
       (K (typedef_quot_type_tac equiv_thm typedef_info))
   end
+   
+fun can_generate_code_cert quot_thm  =
+   case Quotient_Term.get_rel_from_quot_thm quot_thm of
+      Const (@{const_name HOL.eq}, _) => true
+      | Const (@{const_name invariant}, _) $ _  => true
+      | _ => false
+
+fun define_abs_type quot_thm lthy =
+  if can_generate_code_cert quot_thm then
+    let
+      val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
+      val add_abstype_attribute = 
+          Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
+        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
+    in
+      lthy
+        |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
+    end
+  else
+    lthy
+
+fun init_quotient_infr quot_thm equiv_thm lthy =
+  let
+    val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
+    val (qtyp, rtyp) = (dest_funT o fastype_of) rep
+    val qty_full_name = (fst o dest_Type) qtyp
+    val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, 
+      quot_thm = quot_thm }
+    fun quot_info phi = Quotient_Info.transform_quotients phi quotients
+    val abs_rep = {abs = abs, rep = rep}
+    fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
+  in
+    lthy
+      |> Local_Theory.declaration {syntax = false, pervasive = true}
+        (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
+          #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
+      |> define_abs_type quot_thm
+  end
 
 (* main function for constructing a quotient type *)
 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
@@ -86,7 +126,7 @@
       else equiv_thm RS @{thm equivp_implies_part_equivp}
 
     (* generates the typedef *)
-    val ((qty_full_name, typedef_info), lthy1) =
+    val ((_, typedef_info), lthy1) =
       typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
 
     (* abs and rep functions from the typedef *)
@@ -108,9 +148,9 @@
         NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
       | SOME morphs => morphs)
 
-    val ((abs_t, (_, abs_def)), lthy2) = lthy1
+    val ((_, (_, abs_def)), lthy2) = lthy1
       |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
-    val ((rep_t, (_, rep_def)), lthy3) = lthy2
+    val ((_, (_, rep_def)), lthy3) = lthy2
       |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
 
     (* quot_type theorem *)
@@ -129,13 +169,8 @@
     val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm, 
       quot_thm = quotient_thm}
 
-    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
-    fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
-
     val lthy4 = lthy3
-      |> Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
-           #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
+      |> init_quotient_infr quotient_thm equiv_thm
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
           if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
@@ -276,6 +311,32 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
     "quotient type definitions (require equivalence proofs)"
-    (quotspec_parser >> quotient_type_cmd)
+      (quotspec_parser >> quotient_type_cmd)
+
+(* Setup lifting using type_def_thm *)
+
+exception SETUP_LIFT_TYPE of string
+
+fun setup_lift_type typedef_thm =
+  let
+    val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
+    val (quot_thm, equivp_thm) = (case typedef_set of
+      Const ("Orderings.top_class.top", _) => 
+        (typedef_thm RS @{thm copy_type_to_Quotient}, 
+         typedef_thm RS @{thm copy_type_to_equivp})
+      | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) => 
+        (typedef_thm RS @{thm invariant_type_to_Quotient}, 
+         typedef_thm RS @{thm invariant_type_to_part_equivp})
+      | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem")
+  in
+    init_quotient_infr quot_thm equivp_thm
+  end
+
+fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy
+
+val _ = 
+  Outer_Syntax.local_theory @{command_spec "setup_lifting"}
+    "Setup lifting infrastracture" 
+      (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm))
 
 end;