generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command

--- a/src/HOL/Library/Float.thy	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Library/Float.thy	Wed May 16 19:17:20 2012 +0200
@@ -19,7 +19,7 @@
 lemma type_definition_float': "type_definition real float_of float"
   using type_definition_float unfolding real_of_float_def .
 
-setup_lifting (no_abs_code) type_definition_float'
+setup_lifting (no_code) type_definition_float'
 
 lemmas float_of_inject[simp]
 

--- a/src/HOL/Lifting.thy	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed May 16 19:17:20 2012 +0200
@@ -82,10 +82,31 @@
   using a unfolding Quotient_def
   by blast
 
+lemma Quotient_rep_abs_fold_unmap: 
+  assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
+  shows "R (Rep' x') x"
+proof -
+  have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto
+  then show ?thesis using assms(3) by simp
+qed
+
+lemma Quotient_Rep_eq:
+  assumes "x' \<equiv> Abs x" 
+  shows "Rep x' \<equiv> Rep x'"
+by simp
+
 lemma Quotient_rel_abs: "R r s \<Longrightarrow> Abs r = Abs s"
   using a unfolding Quotient_def
   by blast
 
+lemma Quotient_rel_abs2:
+  assumes "R (Rep x) y"
+  shows "x = Abs y"
+proof -
+  from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs)
+  then show ?thesis using assms(1) by (simp add: Quotient_abs_rep)
+qed
+
 lemma Quotient_symp: "symp R"
   using a unfolding Quotient_def using sympI by (metis (full_types))
 

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 16 19:17:20 2012 +0200
@@ -81,6 +81,10 @@
     done
 qed
 
+text {* We can export code: *}
+
+export_code fnil fcons fappend fmap ffilter fset in SML
+
 text {* Note that the generated transfer rule contains a composition
   of relations. The transfer rule is not yet very useful in this form. *}
 

--- a/src/HOL/Relation.thy	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Relation.thy	Wed May 16 19:17:20 2012 +0200
@@ -173,6 +173,11 @@
   obtains "r x x"
   using assms by (auto dest: refl_onD simp add: reflp_def)
 
+lemma reflpD:
+  assumes "reflp r"
+  shows "r x x"
+  using assms by (auto elim: reflpE)
+
 lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \<inter> B) (r \<inter> s)"
   by (unfold refl_on_def) blast
 

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Wed May 16 19:17:20 2012 +0200
@@ -30,6 +30,14 @@
 fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
   | get_binder_types _ = []
 
+fun get_binder_types_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 
+    (T, V) :: get_binder_types_by_rel S (U, W)
+  | get_binder_types_by_rel _ _ = []
+
+fun get_body_type_by_rel (Const (@{const_name "fun_rel"}, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 
+    get_body_type_by_rel S (U, V)
+  | get_body_type_by_rel _ (U, V)  = (U, V)
+
 fun force_rty_type ctxt rty rhs = 
   let
     val thy = Proof_Context.theory_of ctxt
@@ -75,9 +83,14 @@
         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
+    (Conv.fun_conv unfold_conv) ctm
+  end
+
+fun unfold_fun_maps_beta ctm =
+  let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
+  in 
+    (unfold_fun_maps then_conv try_beta_conv) ctm 
   end
 
 fun prove_rel ctxt rsp_thm (rty, qty) =
@@ -121,7 +134,7 @@
         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 unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
     val unabs_def = unabs_all_def ctxt unfolded_def
     val rep = (cterm_of thy o Lifting_Term.quot_thm_rep) quot_thm
     val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
@@ -131,53 +144,150 @@
     simplify_code_eq ctxt code_cert
   end
 
-fun is_abstype ctxt typ =
+fun generate_trivial_rep_eq ctxt def_thm =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val type_name = (fst o dest_Type) typ
+    val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm
+    val code_eq = unabs_all_def ctxt unfolded_def
+    val simp_code_eq = simplify_code_eq ctxt code_eq
   in
-    (snd oo Code.get_type) thy type_name
+    simp_code_eq
   end
-  
+
+fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
+  if body_type rty = body_type qty then 
+    SOME (generate_trivial_rep_eq ctxt def_thm)
+  else 
+    let
+      val (rty_body, qty_body) = get_body_types (rty, qty)
+      val quot_thm = Lifting_Term.prove_quot_thm ctxt (rty_body, qty_body)
+    in
+      if can_generate_code_cert quot_thm then
+        SOME (generate_code_cert ctxt def_thm rsp_thm (rty, qty))
+      else 
+        NONE
+    end
 
-fun define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy = 
+fun generate_abs_eq ctxt def_thm rsp_thm quot_thm =
   let
-    val (rty_body, qty_body) = get_body_types (rty, qty)
-    val quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
+    fun refl_tac ctxt =
+      let
+        fun intro_reflp_tac (t, i) = 
+        let
+          val concl_pat = Drule.strip_imp_concl (cprop_of @{thm reflpD})
+          val insts = Thm.first_order_match (concl_pat, t)
+        in
+          rtac (Drule.instantiate_normalize insts @{thm reflpD}) i
+        end
+        handle Pattern.MATCH => no_tac
+        
+        val fun_rel_meta_eq = mk_meta_eq @{thm fun_rel_eq}
+        val conv = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv fun_rel_meta_eq))) ctxt
+        val rules = Lifting_Info.get_reflp_preserve_rules ctxt
+      in
+        EVERY' [CSUBGOAL intro_reflp_tac, 
+                CONVERSION conv,
+                REPEAT_ALL_NEW (resolve_tac rules)]
+      end
+    
+    fun try_prove_prem ctxt prop =
+      SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
+        handle ERROR _ => NONE
+
+    val abs_eq_with_assms =
+      let
+        val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
+        val rel = Lifting_Term.quot_thm_rel quot_thm
+        val ty_args = get_binder_types_by_rel rel (rty, qty)
+        val body_type = get_body_type_by_rel rel (rty, qty)
+        val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type
+        
+        val rep_abs_folded_unmapped_thm = 
+          let
+            val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq}
+            val ctm = Thm.dest_equals_lhs (cprop_of rep_id)
+            val unfolded_maps_eq = unfold_fun_maps ctm
+            val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap}
+            val prems_pat = (hd o Drule.cprems_of) t1
+            val insts = Thm.first_order_match (prems_pat, cprop_of unfolded_maps_eq)
+          in
+            unfolded_maps_eq RS (Drule.instantiate_normalize insts t1)
+          end
+      in
+        rep_abs_folded_unmapped_thm
+        |> fold (fn _ => fn thm => thm RS @{thm fun_relD2}) ty_args
+        |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm]))
+      end
+    
+    val prems = prems_of abs_eq_with_assms
+    val indexed_prems = map_index (apfst (fn x => x + 1)) prems
+    val indexed_assms = map (apsnd (try_prove_prem ctxt)) indexed_prems
+    val proved_assms = map (apsnd the) (filter (is_some o snd) indexed_assms)
+    val abs_eq = fold_rev (fn (i, assms) => fn thm => assms RSN (i, thm)) proved_assms abs_eq_with_assms
   in
-    if can_generate_code_cert quot_thm then
+    simplify_code_eq ctxt abs_eq
+  end
+
+fun define_code_using_abs_eq abs_eq_thm lthy =
+  if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
+    (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
+  else
+    lthy
+  
+fun define_code_using_rep_eq maybe_rep_eq_thm lthy = 
+  case maybe_rep_eq_thm of
+    SOME rep_eq_thm =>   
       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);
-        val lthy' = 
-          (snd oo Local_Theory.note) ((code_eqn_thm_name, []), [code_cert]) lthy
       in
-        if is_abstype lthy qty_body then
-          (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert]) lthy'
-        else
-          lthy'
+        (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [rep_eq_thm]) lthy
       end
+    | NONE => lthy
+
+fun has_constr ctxt quot_thm =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
+  in
+    if is_Const abs_fun then
+      Code.is_constr thy ((fst o dest_Const) abs_fun)
     else
-      lthy
+      false
   end
 
-fun define_code_eq code_eqn_thm_name def_thm lthy =
+fun has_abstr ctxt quot_thm =
   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
+    val thy = Proof_Context.theory_of ctxt
+    val abs_fun = Lifting_Term.quot_thm_abs quot_thm
   in
-    lthy
-      |> (snd oo Local_Theory.note) ((code_eqn_thm_name, [Code.add_default_eqn_attrib]), [simp_code_eq])
+    if is_Const abs_fun then
+      Code.is_abstr thy ((fst o dest_Const) abs_fun)
+    else
+      false
   end
 
-fun define_code code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy =
-  if body_type rty = body_type qty then 
-    define_code_eq code_eqn_thm_name def_thm lthy
-  else 
-    define_code_cert code_eqn_thm_name def_thm rsp_thm (rty, qty) lthy
+fun define_code abs_eq_thm maybe_rep_eq_thm (rty, qty) lthy =
+  let
+    val (rty_body, qty_body) = get_body_types (rty, qty)
+  in
+    if rty_body = qty_body then
+      if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
+        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
+      else
+        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the maybe_rep_eq_thm]) lthy
+    else
+      let 
+        val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
+      in
+        if has_constr lthy body_quot_thm then
+          define_code_using_abs_eq abs_eq_thm lthy
+        else if has_abstr lthy body_quot_thm then
+          define_code_using_rep_eq maybe_rep_eq_thm lthy
+        else
+          lthy
+      end
+  end
 
 (*
   Defines an operation on an abstract type in terms of a corresponding operation 
@@ -186,15 +296,15 @@
   var - a binding and a mixfix of the new constant being defined
   qty - an abstract type of the new constant
   rhs - a term representing the new constant on the raw level
-  rsp_thm - a respectfulness theorem in the internal form (like (R ===> R ===> R) f f),
+  rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'),
     i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
 *)
 
 fun add_lift_def var qty rhs rsp_thm lthy =
   let
     val rty = fastype_of rhs
-    val quotient_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
-    val absrep_trm =  Lifting_Term.quot_thm_abs quotient_thm
+    val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
+    val absrep_trm =  Lifting_Term.quot_thm_abs quot_thm
     val rty_forced = (domain_type o fastype_of) absrep_trm
     val forced_rhs = force_rty_type lthy rty_forced rhs
     val lhs = Free (Binding.print (#1 var), qty)
@@ -205,21 +315,29 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
-    val transfer_thm = ([quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
+    val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
         |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
+     
+    val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
+    val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
 
     fun qualify defname suffix = Binding.qualified true suffix defname
 
     val lhs_name = (#1 var)
     val rsp_thm_name = qualify lhs_name "rsp"
-    val code_eqn_thm_name = qualify lhs_name "rep_eq"
+    val abs_eq_thm_name = qualify lhs_name "abs_eq"
+    val rep_eq_thm_name = qualify lhs_name "rep_eq"
     val transfer_thm_name = qualify lhs_name "transfer"
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   in
     lthy'
       |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
       |> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm])
-      |> define_code code_eqn_thm_name def_thm rsp_thm (rty_forced, qty)
+      |> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm])
+      |> (case maybe_rep_eq_thm of 
+            SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
+            | NONE => I)
+      |> define_code abs_eq_thm maybe_rep_eq_thm (rty_forced, qty)
   end
 
 fun mk_readable_rsp_thm_eq tm lthy =
@@ -253,7 +371,7 @@
             (binop_conv2  left_conv simp_arrows_conv then_conv unfold_conv) ctm
           | _ => invariant_commute_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 = Trueprop_conv (Conv.fun2_conv simp_arrows_conv)

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed May 16 19:17:20 2012 +0200
@@ -36,8 +36,26 @@
     (def_thm, lthy'')
   end
 
-fun define_abs_type gen_abs_code quot_thm lthy =
-  if gen_abs_code andalso Lifting_Def.can_generate_code_cert quot_thm then
+fun define_code_constr gen_code quot_thm lthy =
+  let
+    val abs = Lifting_Term.quot_thm_abs quot_thm
+    val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
+  in
+    if gen_code andalso is_Const abs_background then
+      let
+        val (const_name, typ) = dest_Const abs_background
+        val fake_term = Logic.mk_type typ
+        val (fixed_fake_term, lthy') = yield_singleton(Variable.importT_terms) fake_term lthy
+        val fixed_type = Logic.dest_type fixed_fake_term
+      in  
+         Local_Theory.background_theory(Code.add_datatype [(const_name, fixed_type)]) lthy'
+      end
+    else
+      lthy
+  end
+
+fun define_abs_type gen_code quot_thm lthy =
+  if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then
     let
       val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
       val add_abstype_attribute = 
@@ -76,31 +94,37 @@
                                                 @ (map Pretty.string_of errs)))
   end
 
-fun setup_lifting_infr gen_abs_code quot_thm lthy =
+fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
   let
     val _ = quot_thm_sanity_check lthy quot_thm
     val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
     val qty_full_name = (fst o dest_Type) qtyp
     val quotients = { quot_thm = quot_thm }
     fun quot_info phi = Lifting_Info.transform_quotients phi quotients
+    val lthy' = case maybe_reflp_thm of
+      SOME reflp_thm => lthy
+        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
+              [reflp_thm])
+        |> define_code_constr gen_code quot_thm
+      | NONE => lthy
+        |> define_abs_type gen_code quot_thm
   in
-    lthy
+    lthy'
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
-      |> define_abs_type gen_abs_code quot_thm
   end
 
 (*
   Sets up the Lifting package by a quotient theorem.
 
-  gen_abs_code - flag if an abstract type given by quot_thm should be registred 
+  gen_code - flag if an abstract type given by quot_thm should be registred 
     as an abstract type in the code generator
   quot_thm - a quotient theorem (Quotient R Abs Rep T)
   maybe_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
     (in the form "reflp R")
 *)
 
-fun setup_by_quotient gen_abs_code quot_thm maybe_reflp_thm lthy =
+fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm
@@ -117,8 +141,6 @@
           [[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}])
-        |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
-          [reflp_thm])
       | NONE => lthy
         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
           [quot_thm RS @{thm Quotient_All_transfer}])
@@ -136,18 +158,18 @@
         [quot_thm RS @{thm Quotient_right_total}])
       |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
         [quot_thm RS @{thm Quotient_rel_eq_transfer}])
-      |> setup_lifting_infr gen_abs_code quot_thm
+      |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
   end
 
 (*
   Sets up the Lifting package by a typedef theorem.
 
-  gen_abs_code - flag if an abstract type given by typedef_thm should be registred 
+  gen_code - flag if an abstract type given by typedef_thm should be registred 
     as an abstract type in the code generator
   typedef_thm - a typedef theorem (type_definition Rep Abs S)
 *)
 
-fun setup_by_typedef_thm gen_abs_code typedef_thm lthy =
+fun setup_by_typedef_thm gen_code typedef_thm lthy =
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
@@ -166,7 +188,7 @@
     fun qualify suffix = Binding.qualified true suffix qty_name
     val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
 
-    val lthy'' = case typedef_set of
+    val (maybe_reflp_thm, lthy'') = case typedef_set of
       Const ("Orderings.top_class.top", _) => 
         let
           val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
@@ -177,8 +199,7 @@
               [[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) ((Binding.empty, [Lifting_Info.add_reflp_preserve_rule_attrib]),
-              [reflp_thm])
+            |> pair (SOME reflp_thm)
         end
       | _ => lthy'
         |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
@@ -187,6 +208,7 @@
           [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
         |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
           [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
+        |> pair NONE
   in
     lthy''
       |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
@@ -197,10 +219,10 @@
         [[quot_thm] MRSL @{thm Quotient_right_unique}])
       |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
         [[quot_thm] MRSL @{thm Quotient_right_total}])
-      |> setup_lifting_infr gen_abs_code quot_thm
+      |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
   end
 
-fun setup_lifting_cmd gen_abs_code xthm opt_reflp_xthm lthy =
+fun setup_lifting_cmd gen_code xthm opt_reflp_xthm lthy =
   let 
     val input_thm = singleton (Attrib.eval_thms lthy) xthm
     val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
@@ -223,14 +245,14 @@
             val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
             val _ = sanity_check_reflp_thm reflp_thm
           in
-            setup_by_quotient gen_abs_code input_thm (SOME reflp_thm) lthy
+            setup_by_quotient gen_code input_thm (SOME reflp_thm) lthy
           end
-        | NONE => setup_by_quotient gen_abs_code input_thm NONE lthy
+        | NONE => setup_by_quotient gen_code input_thm NONE lthy
 
     fun setup_typedef () = 
       case opt_reflp_xthm of
         SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
-        | NONE => setup_by_typedef_thm gen_abs_code input_thm lthy
+        | NONE => setup_by_typedef_thm gen_code input_thm lthy
   in
     case input_term of
       (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
@@ -238,12 +260,12 @@
       | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   end
 
-val opt_gen_abs_code =
-  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_abs_code" >> K false) --| @{keyword ")"})) true
+val opt_gen_code =
+  Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
 
 val _ = 
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     "Setup lifting infrastructure" 
-      (opt_gen_abs_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
-        (fn ((gen_abs_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_abs_code xthm opt_reflp_xthm))
+      (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
+        (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
 end;

--- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed May 16 19:17:20 2012 +0200
@@ -9,12 +9,12 @@
   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
+    ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
 
   val quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option)) list -> Proof.context -> Proof.state
+    ((binding * binding) option * bool)) list -> Proof.context -> Proof.state
 
-  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
+  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
     (binding * binding) option) list -> Proof.context -> Proof.state
 end;
 
@@ -132,7 +132,7 @@
     (def_thm, lthy'')
   end;
 
-fun setup_lifting_package quot3_thm equiv_thm lthy =
+fun setup_lifting_package gen_code quot3_thm equiv_thm lthy =
   let
     val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
     val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
@@ -150,11 +150,11 @@
       )
   in
     lthy'
-      |> Lifting_Setup.setup_by_quotient false quot_thm reflp_thm
+      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm
       |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
   end
 
-fun init_quotient_infr quot_thm equiv_thm lthy =
+fun init_quotient_infr gen_code 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
@@ -170,11 +170,11 @@
         (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
-      |> setup_lifting_package quot_thm equiv_thm
+      |> setup_lifting_package gen_code quot_thm equiv_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 =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy =
   let
     val part_equiv =
       if partial
@@ -226,7 +226,7 @@
       quot_thm = quotient_thm}
 
     val lthy4 = lthy3
-      |> init_quotient_infr quotient_thm equiv_thm
+      |> init_quotient_infr gen_code quotient_thm equiv_thm
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
           if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
@@ -307,6 +307,7 @@
  - the partial flag (a boolean)
  - the relation according to which the type is quotient
  - optional names of morphisms (rep/abs)
+ - flag if code should be generated by Lifting package
 
  it opens a proof-state in which one has to show that the
  relations are equivalence relations
@@ -336,7 +337,7 @@
 
 fun quotient_type_cmd specs lthy =
   let
-    fun parse_spec (((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
+    fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
       let
         val rty = Syntax.read_typ lthy rty_str
         val tmp_lthy1 = Variable.declare_typ rty lthy
@@ -346,7 +347,7 @@
           |> Syntax.check_term tmp_lthy1
         val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
       in
-        (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), tmp_lthy2)
+        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
       end
 
     val (spec', _) = fold_map parse_spec specs lthy
@@ -354,11 +355,14 @@
     quotient_type spec' lthy
   end
 
+val opt_gen_code =
+  Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true
+
 val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
 
 val quotspec_parser =
   Parse.and_list1
-    ((Parse.type_args -- Parse.binding) --
+    ((opt_gen_code -- Parse.type_args -- Parse.binding) --
       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
       Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
         (@{keyword "/"} |-- (partial -- Parse.term))  --

--- a/src/HOL/Transfer.thy	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Transfer.thy	Wed May 16 19:17:20 2012 +0200
@@ -26,6 +26,11 @@
   shows "B (f x) (g y)"
   using assms by (simp add: fun_rel_def)
 
+lemma fun_relD2:
+  assumes "(A ===> B) f g" and "A x x"
+  shows "B (f x) (g x)"
+  using assms unfolding fun_rel_def by auto
+
 lemma fun_relE:
   assumes "(A ===> B) f g" and "A x y"
   obtains "B (f x) (g y)"