# HG changeset patch
# User kuncar
# Date 1362744863 -3600
# Node ID 84d01fd733cf055204fd313161530a7d15d57e06
# Parent  65f4284d3f1a57d1a14cc29214025c4166c5592b
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided

diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Lifting.thy	Fri Mar 08 13:14:23 2013 +0100
@@ -8,6 +8,7 @@
 theory Lifting
 imports Equiv_Relations Transfer
 keywords
+  "parametric" and
   "print_quotmaps" "print_quotients" :: diag and
   "lift_definition" :: thy_goal and
   "setup_lifting" :: thy_decl
@@ -342,6 +343,16 @@
   unfolding bi_unique_def T_def
   by (simp add: type_definition.Rep_inject [OF type])
 
+(* the following two theorems are here only for convinience *)
+
+lemma typedef_right_unique: "right_unique T"
+  using T_def type Quotient_right_unique typedef_to_Quotient 
+  by blast
+
+lemma typedef_right_total: "right_total T"
+  using T_def type Quotient_right_total typedef_to_Quotient 
+  by blast
+
 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
   unfolding fun_rel_def T_def by simp
 
@@ -410,6 +421,125 @@
 lemma reflp_equality: "reflp (op =)"
 by (auto intro: reflpI)
 
+text {* Proving a parametrized correspondence relation *}
+
+lemma eq_OO: "op= OO R = R"
+unfolding OO_def by metis
+
+definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+"POS A B \<equiv> A \<le> B"
+
+definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+"NEG A B \<equiv> B \<le> A"
+
+definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+
+(*
+  The following two rules are here because we don't have any proper
+  left-unique ant left-total relations. Left-unique and left-total
+  assumptions show up in distributivity rules for the function type.
+*)
+
+lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R"
+unfolding bi_unique_def left_unique_def by blast
+
+lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R"
+unfolding bi_total_def left_total_def by blast
+
+lemma pos_OO_eq:
+  shows "POS (A OO op=) A"
+unfolding POS_def OO_def by blast
+
+lemma pos_eq_OO:
+  shows "POS (op= OO A) A"
+unfolding POS_def OO_def by blast
+
+lemma neg_OO_eq:
+  shows "NEG (A OO op=) A"
+unfolding NEG_def OO_def by auto
+
+lemma neg_eq_OO:
+  shows "NEG (op= OO A) A"
+unfolding NEG_def OO_def by blast
+
+lemma POS_trans:
+  assumes "POS A B"
+  assumes "POS B C"
+  shows "POS A C"
+using assms unfolding POS_def by auto
+
+lemma NEG_trans:
+  assumes "NEG A B"
+  assumes "NEG B C"
+  shows "NEG A C"
+using assms unfolding NEG_def by auto
+
+lemma POS_NEG:
+  "POS A B \<equiv> NEG B A"
+  unfolding POS_def NEG_def by auto
+
+lemma NEG_POS:
+  "NEG A B \<equiv> POS B A"
+  unfolding POS_def NEG_def by auto
+
+lemma POS_pcr_rule:
+  assumes "POS (A OO B) C"
+  shows "POS (A OO B OO X) (C OO X)"
+using assms unfolding POS_def OO_def by blast
+
+lemma NEG_pcr_rule:
+  assumes "NEG (A OO B) C"
+  shows "NEG (A OO B OO X) (C OO X)"
+using assms unfolding NEG_def OO_def by blast
+
+lemma POS_apply:
+  assumes "POS R R'"
+  assumes "R f g"
+  shows "R' f g"
+using assms unfolding POS_def by auto
+
+text {* Proving a parametrized correspondence relation *}
+
+lemma fun_mono:
+  assumes "A \<ge> C"
+  assumes "B \<le> D"
+  shows   "(A ===> B) \<le> (C ===> D)"
+using assms unfolding fun_rel_def by blast
+
+lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
+unfolding OO_def fun_rel_def by blast
+
+lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
+unfolding right_unique_def left_total_def by blast
+
+lemma functional_converse_relation: "left_unique R \<Longrightarrow> right_total R \<Longrightarrow> \<forall>y. \<exists>!x. R x y"
+unfolding left_unique_def right_total_def by blast
+
+lemma neg_fun_distr1:
+assumes 1: "left_unique R" "right_total R"
+assumes 2: "right_unique R'" "left_total R'"
+shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
+  using functional_relation[OF 2] functional_converse_relation[OF 1]
+  unfolding fun_rel_def OO_def
+  apply clarify
+  apply (subst all_comm)
+  apply (subst all_conj_distrib[symmetric])
+  apply (intro choice)
+  by metis
+
+lemma neg_fun_distr2:
+assumes 1: "right_unique R'" "left_total R'"
+assumes 2: "left_unique S'" "right_total S'"
+shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
+  using functional_converse_relation[OF 2] functional_relation[OF 1]
+  unfolding fun_rel_def OO_def
+  apply clarify
+  apply (subst all_comm)
+  apply (subst all_conj_distrib[symmetric])
+  apply (intro choice)
+  by metis
+
 subsection {* ML setup *}
 
 ML_file "Tools/Lifting/lifting_util.ML"
@@ -417,8 +547,12 @@
 ML_file "Tools/Lifting/lifting_info.ML"
 setup Lifting_Info.setup
 
+lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
+
+(* setup for the function type *)
 declare fun_quotient[quot_map]
-lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
+declare fun_mono[relator_mono]
+lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
 
 ML_file "Tools/Lifting/lifting_term.ML"
 
@@ -426,6 +560,6 @@
 
 ML_file "Tools/Lifting/lifting_setup.ML"
 
-hide_const (open) invariant
+hide_const (open) invariant POS NEG
 
 end
diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -6,11 +6,14 @@
 
 signature LIFTING_DEF =
 sig
+  val generate_parametric_transfer_rule:
+    Proof.context -> thm -> thm -> thm
+
   val add_lift_def:
-    (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
+    (binding * mixfix) -> typ -> term -> thm -> thm option -> local_theory -> local_theory
 
   val lift_def_cmd:
-    (binding * string option * mixfix) * string -> local_theory -> Proof.state
+    (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
 
   val can_generate_code_cert: thm -> bool
 end;
@@ -22,6 +25,103 @@
 
 infix 0 MRSL
 
+(* Generation of a transfer rule *)
+
+fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
+  let
+    fun preprocess ctxt thm =
+      let
+        val tm = (strip_args 2 o HOLogic.dest_Trueprop o concl_of) thm;
+        val param_rel = (snd o dest_comb o fst o dest_comb) tm;
+        val thy = Proof_Context.theory_of ctxt;
+        val free_vars = Term.add_vars param_rel [];
+        
+        fun make_subst (var as (_, typ)) subst = 
+          let
+            val [rty, rty'] = binder_types typ
+          in
+            if (Term.is_TVar rty andalso is_Type rty') then
+              (Var var, HOLogic.eq_const rty')::subst
+            else
+              subst
+          end;
+        
+        val subst = fold make_subst free_vars [];
+        val csubst = map (pairself (cterm_of thy)) subst;
+        val inst_thm = Drule.cterm_instantiate csubst thm;
+      in
+        Conv.fconv_rule 
+          ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
+            (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+      end
+
+    fun inst_relcomppI thy ant1 ant2 =
+      let
+        val t1 = (HOLogic.dest_Trueprop o concl_of) ant1
+        val t2 = (HOLogic.dest_Trueprop o prop_of) ant2
+        val fun1 = cterm_of thy (strip_args 2 t1)
+        val args1 = map (cterm_of thy) (get_args 2 t1)
+        val fun2 = cterm_of thy (strip_args 2 t2)
+        val args2 = map (cterm_of thy) (get_args 1 t2)
+        val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
+        val vars = (rev (Term.add_vars (prop_of relcomppI) []))
+        val subst = map (apfst ((cterm_of thy) o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
+      in
+        Drule.cterm_instantiate subst relcomppI
+      end
+
+    fun zip_transfer_rules ctxt thm = 
+      let
+        val thy = Proof_Context.theory_of ctxt
+        fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
+        val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
+        val typ = (typ_of o ctyp_of_term) rel
+        val POS_const = cterm_of thy (mk_POS typ)
+        val var = cterm_of thy (Var (("X", #maxidx (rep_cterm (rel)) + 1), typ))
+        val goal = Thm.apply (cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
+      in
+        [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
+      end
+     
+    val thm = (inst_relcomppI (Proof_Context.theory_of ctxt) parametric_transfer_rule transfer_rule) 
+                OF [parametric_transfer_rule, transfer_rule]
+    val preprocessed_thm = preprocess ctxt thm
+    val orig_ctxt = ctxt
+    val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
+    val assms = cprems_of fixed_thm
+    val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
+    val ctxt = Context.proof_map(fold (add_transfer_rule o Thm.assume) assms) ctxt
+    val zipped_thm =
+      fixed_thm
+      |> undisch_all
+      |> zip_transfer_rules ctxt
+      |> implies_intr_list assms
+      |> singleton (Variable.export ctxt orig_ctxt)
+  in
+    zipped_thm
+  end
+
+fun print_generate_transfer_info msg = 
+  let
+    val error_msg = cat_lines 
+      ["Generation of a parametric transfer rule failed.",
+      (Pretty.string_of (Pretty.block
+         [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+  in
+    error error_msg
+  end
+
+fun generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm =
+  let
+    val transfer_rule =
+      ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
+      |> Morphism.thm (Local_Theory.target_morphism lthy)
+      |> Lifting_Term.parametrize_transfer_rule lthy
+  in
+    (option_fold transfer_rule (generate_parametric_transfer_rule lthy transfer_rule) opt_par_thm
+    handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; transfer_rule))
+  end
+
 (* Generation of the code certificate from the rsp theorem *)
 
 fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
@@ -233,8 +333,8 @@
   else
     lthy
   
-fun define_code_using_rep_eq maybe_rep_eq_thm lthy = 
-  case maybe_rep_eq_thm of
+fun define_code_using_rep_eq opt_rep_eq_thm lthy = 
+  case opt_rep_eq_thm of
     SOME rep_eq_thm =>   
       let
         val add_abs_eqn_attribute = 
@@ -267,7 +367,7 @@
       false
   end
 
-fun define_code abs_eq_thm maybe_rep_eq_thm (rty, qty) lthy =
+fun define_code abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
   let
     val (rty_body, qty_body) = get_body_types (rty, qty)
   in
@@ -275,7 +375,7 @@
       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
+        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the opt_rep_eq_thm]) lthy
     else
       let 
         val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
@@ -283,7 +383,7 @@
         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
+          define_code_using_rep_eq opt_rep_eq_thm lthy
         else
           lthy
       end
@@ -300,7 +400,7 @@
     i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
 *)
 
-fun add_lift_def var qty rhs rsp_thm lthy =
+fun add_lift_def var qty rhs rsp_thm opt_par_thm lthy =
   let
     val rty = fastype_of rhs
     val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
@@ -316,10 +416,10 @@
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
     fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
-    val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
+    val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
 
     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)
+    val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
 
     fun qualify defname suffix = Binding.qualified true suffix defname
 
@@ -327,17 +427,17 @@
     val rsp_thm_name = qualify lhs_name "rsp"
     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_rule_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])
+      |> (snd oo Local_Theory.note) ((transfer_rule_name, [transfer_attr]), [transfer_rule])
       |> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm])
-      |> (case maybe_rep_eq_thm of 
+      |> (case opt_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)
+      |> define_code abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
   end
 
 fun mk_readable_rsp_thm_eq tm lthy =
@@ -397,7 +497,7 @@
 
 *)
 
-fun lift_def_cmd (raw_var, rhs_raw) lthy =
+fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy =
   let
     val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy 
     val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw
@@ -422,23 +522,24 @@
     val forced_rhs = force_rty_type lthy' rty_forced rhs;
     val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
     val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy'
-    val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
+    val opt_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
     val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
     val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm
+    val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy')) opt_par_xthm
 
     fun after_qed thm_list lthy = 
       let
         val internal_rsp_thm =
           case thm_list of
-            [] => the maybe_proven_rsp_thm
+            [] => the opt_proven_rsp_thm
           | [[thm]] => Goal.prove lthy [] [] internal_rsp_tm 
             (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
       in
-        add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy
+        add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
       end
 
   in
-    case maybe_proven_rsp_thm of
+    case opt_proven_rsp_thm of
       SOME _ => Proof.theorem NONE after_qed [] lthy'
       | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy'
   end
@@ -480,17 +581,16 @@
       error error_msg
     end
 
-fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy =
-  (lift_def_cmd (raw_var, rhs_raw) lthy
+fun lift_def_cmd_with_err_handling (raw_var, rhs_raw, opt_par_xthm) lthy =
+  (lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy
     handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
     handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => 
       check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw)
 
 (* parser and command *)
 val liftdef_parser =
-  ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
-    --| @{keyword "is"} -- Parse.term
-
+  (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
+    --| @{keyword "is"} -- Parse.term -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)) >> Parse.triple1
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
     "definition for constants over the quotient type"
diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -11,7 +11,8 @@
   val lookup_quotmaps_global: theory -> string -> quotmaps option
   val print_quotmaps: Proof.context -> unit
 
-  type quotients = {quot_thm: thm, pcrel_def: thm option}
+  type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
+  type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
   val transform_quotients: morphism -> quotients -> quotients
   val lookup_quotients: Proof.context -> string -> quotients option
   val lookup_quotients_global: theory -> string -> quotients option
@@ -25,6 +26,11 @@
   val add_reflexivity_rule_attribute: attribute
   val add_reflexivity_rule_attrib: Attrib.src
 
+  type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
+    pos_distr_rules: thm list, neg_distr_rules: thm list}
+  val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
+  val lookup_relator_distr_data_global: theory -> string -> relator_distr_data option
+
   val setup: theory -> theory
 end;
 
@@ -118,7 +124,8 @@
   end
 
 (* info about quotient types *)
-type quotients = {quot_thm: thm, pcrel_def: thm option}
+type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
+type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
 
 structure Quotients = Generic_Data
 (
@@ -128,8 +135,11 @@
   fun merge data = Symtab.merge (K true) data
 )
 
-fun transform_quotients phi {quot_thm, pcrel_def} =
-  {quot_thm = Morphism.thm phi quot_thm, pcrel_def = Option.map (Morphism.thm phi) pcrel_def}
+fun transform_pcrel_info phi {pcrel_def, pcr_cr_eq} =
+  {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
+
+fun transform_quotients phi {quot_thm, pcrel_info} =
+  {quot_thm = Morphism.thm phi quot_thm, pcrel_info = Option.map (transform_pcrel_info phi) pcrel_info}
 
 val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
 val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
@@ -141,9 +151,9 @@
     val (_, qtyp) = quot_thm_rty_qty quot_thm
     val qty_full_name = (fst o dest_Type) qtyp
     val symtab = Quotients.get ctxt
-    val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name
+    val opt_stored_quot_thm = Symtab.lookup symtab qty_full_name
   in
-    case maybe_stored_quot_thm of
+    case opt_stored_quot_thm of
       SOME data => 
         if Thm.eq_thm_prop (#quot_thm data, quot_thm) then
           Quotients.map (Symtab.delete qty_full_name) ctxt
@@ -157,14 +167,16 @@
 
 fun print_quotients ctxt =
   let
-    fun prt_quot (qty_name, {quot_thm, pcrel_def}) =
+    fun prt_quot (qty_name, {quot_thm, pcrel_info}) =
       Pretty.block (separate (Pretty.brk 2)
        [Pretty.str "type:", 
         Pretty.str qty_name,
         Pretty.str "quot. thm:",
         Syntax.pretty_term ctxt (prop_of quot_thm),
         Pretty.str "pcrel_def thm:",
-        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of) pcrel_def])
+        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcrel_info,
+        Pretty.str "pcr_cr_eq thm:",
+        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcrel_info])
   in
     map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
     |> Pretty.big_list "quotients:"
@@ -193,6 +205,211 @@
 val add_reflexivity_rule_attribute = Reflp_Preserve.add
 val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
 
+(* info about relator distributivity theorems *)
+type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
+  pos_distr_rules: thm list, neg_distr_rules: thm list}
+
+fun map_relator_distr_data f1 f2 f3 f4
+  {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
+  {pos_mono_rule   = f1 pos_mono_rule, 
+   neg_mono_rule   = f2 neg_mono_rule,
+   pos_distr_rules = f3 pos_distr_rules, 
+   neg_distr_rules = f4 neg_distr_rules}
+
+fun map_pos_mono_rule f = map_relator_distr_data f I I I
+fun map_neg_mono_rule f = map_relator_distr_data I f I I
+fun map_pos_distr_rules f = map_relator_distr_data I I f I 
+fun map_neg_distr_rules f = map_relator_distr_data I I I f
+
+structure Relator_Distr = Generic_Data
+(
+  type T = relator_distr_data Symtab.table
+  val empty = Symtab.empty
+  val extend = I
+  fun merge data = Symtab.merge (K true) data
+);
+
+fun introduce_polarities rule =
+  let
+    val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT
+    val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (prems_of rule)
+    val equal_prems = filter op= prems_pairs
+    val _ = if null equal_prems then () 
+      else error "The rule contains reflexive assumptions."
+    val concl_pairs = rule 
+      |> concl_of
+      |> HOLogic.dest_Trueprop
+      |> dest_less_eq
+      |> pairself (snd o strip_comb)
+      |> op~~
+      |> filter_out op=
+    
+    val _ = if has_duplicates op= concl_pairs 
+      then error "The rule contains duplicated variables in the conlusion." else ()
+
+    fun mem a l = member op= l a
+
+    fun rewrite_prem prem_pair = 
+      if mem prem_pair concl_pairs 
+      then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))
+      else if mem (swap prem_pair) concl_pairs 
+        then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
+      else error "The rule contains a non-relevant assumption."
+    
+    fun rewrite_prems [] = Conv.all_conv
+      | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs)
+    
+    val rewrite_prems_conv = rewrite_prems prems_pairs
+    val rewrite_concl_conv = 
+      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})))
+  in
+    (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule
+  end
+  handle 
+    TERM _ => error "The rule has a wrong format."
+    | CTERM _ => error "The rule has a wrong format."
+
+fun negate_mono_rule mono_rule = 
+  let
+    val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}])
+  in
+    Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
+  end;
+
+fun add_mono_rule mono_rule ctxt = 
+  let
+    val mono_rule = introduce_polarities mono_rule
+    val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
+      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
+    val _ = if Symtab.defined (Relator_Distr.get ctxt) mono_ruleT_name 
+      then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
+      else ()
+    val neg_mono_rule = negate_mono_rule mono_rule
+    val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, 
+      pos_distr_rules = [], neg_distr_rules = []}
+  in
+    Relator_Distr.map (Symtab.update (mono_ruleT_name, relator_distr_data)) ctxt
+  end;
+
+local 
+  fun add_distr_rule update_entry distr_rule ctxt =
+    let
+      val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
+        dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) distr_rule
+    in
+      if Symtab.defined (Relator_Distr.get ctxt) distr_ruleT_name then 
+        Relator_Distr.map (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) ctxt
+      else error "The monoticity rule is not defined."
+    end
+
+    fun rewrite_concl_conv thm ctm = 
+      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
+      handle CTERM _ => error "The rule has a wrong format."
+
+in
+  fun add_pos_distr_rule distr_rule ctxt = 
+    let
+      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule
+      fun update_entry distr_rule data = 
+        map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data
+    in
+      add_distr_rule update_entry distr_rule ctxt
+    end
+    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
+
+  
+  fun add_neg_distr_rule distr_rule ctxt = 
+    let
+      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule
+      fun update_entry distr_rule data = 
+        map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data
+    in
+      add_distr_rule update_entry distr_rule ctxt
+    end
+    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
+end
+
+local 
+  val eq_refl2 = sym RS @{thm eq_refl}
+in
+  fun add_eq_distr_rule distr_rule ctxt =
+    let 
+      val pos_distr_rule = @{thm eq_refl} OF [distr_rule]
+      val neg_distr_rule = eq_refl2 OF [distr_rule]
+    in
+      ctxt 
+      |> add_pos_distr_rule pos_distr_rule
+      |> add_neg_distr_rule neg_distr_rule
+    end
+end;
+
+local
+  fun sanity_check rule =
+    let
+      val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)
+      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);
+      val (lhs, rhs) = case concl of
+        Const ("Orderings.ord_class.less_eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => 
+          (lhs, rhs)
+        | Const ("Orderings.ord_class.less_eq", _) $ rhs $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) => 
+          (lhs, rhs)
+        | Const ("HOL.eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => (lhs, rhs)
+        | _ => error "The rule has a wrong format."
+      
+      val lhs_vars = Term.add_vars lhs []
+      val rhs_vars = Term.add_vars rhs []
+      val assms_vars = fold Term.add_vars assms [];
+      val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else ()
+      val _ = if subset op= (rhs_vars, lhs_vars) then () 
+        else error "Extra variables in the right-hand side of the rule"
+      val _ = if subset op= (assms_vars, lhs_vars) then () 
+        else error "Extra variables in the assumptions of the rule"
+      val rhs_args = (snd o strip_comb) rhs;
+      fun check_comp t = case t of 
+        Const ("Relation.relcompp", _) $ Var (_, _) $ Var (_,_) => ()
+        | _ => error "There is an argument on the rhs that is not a composition."
+      val _ = map check_comp rhs_args
+    in
+      ()
+    end
+in
+
+  fun add_distr_rule distr_rule ctxt = 
+    let
+      val _ = sanity_check distr_rule
+      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)
+    in
+      case concl of
+        Const ("Orderings.ord_class.less_eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ => 
+          add_pos_distr_rule distr_rule ctxt
+        | Const ("Orderings.ord_class.less_eq", _) $ _ $ (Const ("Relation.relcompp",_) $ _ $ _) => 
+          add_neg_distr_rule distr_rule ctxt
+        | Const ("HOL.eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
+          add_eq_distr_rule distr_rule ctxt
+    end
+end
+
+fun get_distr_rules_raw ctxt = Symtab.fold 
+  (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) 
+    (Relator_Distr.get ctxt) []
+
+fun get_mono_rules_raw ctxt = Symtab.fold 
+  (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) 
+    (Relator_Distr.get ctxt) []
+
+val lookup_relator_distr_data = Symtab.lookup o Relator_Distr.get o Context.Proof
+val lookup_relator_distr_data_global = Symtab.lookup o Relator_Distr.get o Context.Theory
+
+val relator_distr_attribute_setup =
+  Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
+    "declaration of relator's monoticity"
+  #> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule))
+    "declaration of relator's distributivity over OO"
+  #> Global_Theory.add_thms_dynamic
+     (@{binding relator_distr_raw}, get_distr_rules_raw)
+  #> Global_Theory.add_thms_dynamic
+     (@{binding relator_mono_raw}, get_mono_rules_raw)
+
 (* theory setup *)
 
 val setup =
@@ -200,6 +417,7 @@
   #> quot_del_attribute_setup
   #> Invariant_Commute.setup
   #> Reflp_Preserve.setup
+  #> relator_distr_attribute_setup
 
 (* outer syntax commands *)
 
diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -8,7 +8,7 @@
 sig
   exception SETUP_LIFTING_INFR of string
 
-  val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
+  val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
 
   val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
 end;
@@ -26,7 +26,7 @@
   let
     val (qty, rty) = (dest_funT o fastype_of) rep_fun
     val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
-    val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
+    val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph))
     val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
     val crel_name = Binding.prefix_name "cr_" qty_name
     val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
@@ -69,7 +69,7 @@
     val qty_name = (fst o dest_Type) qty
     val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
     val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
-    val rhs = relcomp_op $ param_rel_fixed $ fixed_crel;
+    val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
     val definition_term = Logic.mk_equals (lhs, rhs)
     val ((_, (_, def_thm)), lthy) = Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), 
       ((Binding.empty, []), definition_term)) lthy
@@ -78,16 +78,72 @@
   end
   handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy))
 
+
+local
+  val eq_OO_meta = mk_meta_eq @{thm eq_OO} 
+
+  fun print_generate_pcr_cr_eq_error ctxt term = 
+  let
+    val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
+    val error_msg = cat_lines 
+      ["Generation of a pcr_cr_eq failed.",
+      (Pretty.string_of (Pretty.block
+         [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
+       "Most probably a relator_eq rule for one of the involved types is missing."]
+  in
+    error error_msg
+  end
+in
+  fun define_pcr_cr_eq lthy pcr_rel_def =
+    let
+      val lhs = (term_of o Thm.lhs_of) pcr_rel_def
+      val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type o List.last o binder_types o fastype_of) lhs
+      val args = (snd o strip_comb) lhs
+      
+      fun make_inst var ctxt = 
+        let 
+          val typ = (snd o relation_types o snd o dest_Var) var
+          val sort = Type.sort_of_atyp typ
+          val (fresh_var, ctxt) = yield_singleton Variable.invent_types sort ctxt
+          val thy = Proof_Context.theory_of ctxt
+        in
+          ((cterm_of thy var, cterm_of thy (HOLogic.eq_const (TFree fresh_var))), ctxt)
+        end
+      
+      val orig_lthy = lthy
+      val (args_inst, lthy) = fold_map make_inst args lthy
+      val pcr_cr_eq = 
+        pcr_rel_def
+        |> Drule.cterm_instantiate args_inst    
+        |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (bottom_rewr_conv (Transfer.get_relator_eq lthy))))
+  in
+    case (term_of o Thm.rhs_of) pcr_cr_eq of
+      Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ => 
+        let
+          val thm = 
+            pcr_cr_eq
+            |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
+            |> mk_HOL_eq
+            |> singleton (Variable.export lthy orig_lthy)
+          val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), 
+            [thm]) lthy
+        in
+          (thm, lthy)
+        end
+      | Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
+      | _ => error "generate_pcr_cr_eq: implementation error"
+  end
+end
+
 fun define_code_constr gen_code quot_thm lthy =
   let
     val abs = 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
+    if gen_code andalso is_Const abs then
       let
-        val (fixed_abs_background, lthy') = yield_singleton(Variable.importT_terms) abs_background lthy
+        val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
       in  
-         Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs_background]) lthy'
+         Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
       end
     else
       lthy
@@ -99,7 +155,7 @@
       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);
+        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])
@@ -133,15 +189,24 @@
                                                 @ (map Pretty.string_of errs)))
   end
 
-fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
+fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
   let
     val _ = quot_thm_sanity_check lthy quot_thm
     val (_, qtyp) = quot_thm_rty_qty quot_thm
     val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy
-    val quotients = { quot_thm = quot_thm, pcrel_def = pcrel_def }
+    (**)
+    val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
+    (**)
+    val (pcr_cr_eq, lthy) = case pcrel_def of
+      SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def)
+      | NONE => (NONE, lthy)
+    val pcrel_info = case pcrel_def of
+      SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
+      | NONE => NONE
+    val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
     val qty_full_name = (fst o dest_Type) qtyp  
     fun quot_info phi = Lifting_Info.transform_quotients phi quotients
-    val lthy = case maybe_reflp_thm of
+    val lthy = case opt_reflp_thm of
       SOME reflp_thm => lthy
         |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
               [reflp_thm])
@@ -156,51 +221,247 @@
         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
   end
 
+local 
+  val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
+in
+  fun parametrize_class_constraint ctxt pcr_def constraint =
+    let
+      fun generate_transfer_rule pcr_def constraint goal ctxt =
+        let
+          val thy = Proof_Context.theory_of ctxt
+          val orig_ctxt = ctxt
+          val (fixed_goal, ctxt) = yield_singleton (Variable.import_terms true) goal ctxt
+          val init_goal = Goal.init (cterm_of thy fixed_goal)
+          val rules = Transfer.get_transfer_raw ctxt
+          val rules = constraint :: OO_rules @ rules
+          val tac = K (Local_Defs.unfold_tac ctxt [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac rules)
+        in
+          (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
+        end
+      
+      fun make_goal pcr_def constr =
+        let 
+          val pred_name = (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o prop_of) constr
+          val arg = (fst o Logic.dest_equals o prop_of) pcr_def
+        in
+          HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
+        end
+      
+      val check_assms =
+        let 
+          val right_names = ["bi_total", "bi_unique", "right_total", "right_unique"]
+      
+          fun is_right_name name = member op= right_names (Long_Name.base_name name)
+      
+          fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name
+            | is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name
+            | is_trivial_assm _ = false
+        in
+          fn thm => 
+            let
+              val prems = map HOLogic.dest_Trueprop (prems_of thm)
+              val thm_name = (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o concl_of) thm
+              val non_trivial_assms = filter_out is_trivial_assm prems
+            in
+              if null non_trivial_assms then ()
+              else
+                let
+                  val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
+                    Pretty.str thm_name,
+                    Pretty.str " transfer rule found:",
+                    Pretty.brk 1] @ 
+                    ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
+                                       [Pretty.str "."])
+                in
+                  warning (Pretty.str_of pretty_msg)
+                end
+            end
+        end
+  
+      val goal = make_goal pcr_def constraint
+      val thm = generate_transfer_rule pcr_def constraint goal ctxt
+      val _ = check_assms thm
+    in
+      thm
+    end
+end
+
+local
+  val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def}))
+in
+  fun generate_parametric_id lthy rty id_transfer_rule =
+    let
+      val orig_lthy = lthy
+      (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
+      val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
+      val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
+      val lthy = orig_lthy
+      val id_transfer = 
+         @{thm id_transfer}
+        |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
+        |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
+      val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
+      val thy = Proof_Context.theory_of lthy;
+      val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
+      val id_par_thm = Drule.cterm_instantiate inst id_transfer;
+    in
+      Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
+    end
+    handle Lifting_Term.MERGE_TRANSFER_REL msg => 
+      let
+        val error_msg = cat_lines 
+          ["Generation of a parametric transfer rule for the abs. or the rep. function failed.",
+          "A non-parametric version will be used.",
+          (Pretty.string_of (Pretty.block
+             [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+      in
+        (warning error_msg; id_transfer_rule)
+      end
+end
+
+fun parametrize_quantifier lthy quant_transfer_rule =
+  Lifting_Term.parametrize_transfer_rule lthy quant_transfer_rule
+
+fun get_pcrel_info ctxt qty_full_name =  
+  #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
+
 (*
   Sets up the Lifting package by a quotient theorem.
 
   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
+  opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
     (in the form "reflp R")
 *)
 
-fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
+fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
   let
+    (**)
+    val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
+    (**)
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
-    val (_, qty) = quot_thm_rty_qty quot_thm
+    val (rty, qty) = 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 Long_Name.base_name o fst o dest_Type) qty
+    val qty_full_name = (fst o dest_Type) qty
+    val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
     fun qualify suffix = Binding.qualified true suffix qty_name
-    val lthy = case maybe_reflp_thm of
-      SOME reflp_thm => lthy
-        |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
-          [[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}])
-        |> (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}])
-        |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
-          [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}])
+    val lthy = case opt_reflp_thm of
+      SOME reflp_thm =>
+        let 
+          val thms =
+            [("abs_induct",     @{thm Quotient_total_abs_induct}, [induct_attr]),
+             ("abs_eq_iff",     @{thm Quotient_total_abs_eq_iff}, []           )]
+        in
+          lthy
+            |> fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr), 
+              [[quot_thm, reflp_thm] MRSL thm])) thms
+        end
+      | NONE =>
+        let
+          val thms = 
+            [("abs_induct",     @{thm Quotient_abs_induct},       [induct_attr])]
+        in
+          fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr), 
+            [quot_thm RS thm])) thms lthy
+        end
+
+    fun setup_transfer_rules_nonpar lthy =
+      let
+        val lthy =
+          case opt_reflp_thm of
+            SOME reflp_thm =>
+              let 
+                val thms =
+                  [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
+                   ("bi_total",       @{thm Quotient_bi_total}       )]
+              in
+                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                    [[quot_thm, reflp_thm] MRSL thm])) thms lthy
+              end
+            | NONE =>
+              let
+                val thms = 
+                  [("All_transfer",   @{thm Quotient_All_transfer}   ),
+                   ("Ex_transfer",    @{thm Quotient_Ex_transfer}    ),
+                   ("forall_transfer",@{thm Quotient_forall_transfer})]
+              in
+                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                  [quot_thm RS thm])) thms lthy
+              end
+        val thms = 
+          [("rel_eq_transfer", @{thm Quotient_rel_eq_transfer}),
+           ("right_unique",    @{thm Quotient_right_unique}   ), 
+           ("right_total",     @{thm Quotient_right_total}    )]
+      in
+        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+          [quot_thm RS thm])) thms lthy
+      end
+
+    fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm =
+      option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm
+      handle Lifting_Term.MERGE_TRANSFER_REL msg => 
+        let
+          val error_msg = cat_lines 
+            ["Generation of a parametric transfer rule for the quotient relation failed.",
+            (Pretty.string_of (Pretty.block
+               [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+        in
+          error error_msg
+        end
+
+    fun setup_transfer_rules_par lthy =
+      let
+        val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+        val lthy =
+          case opt_reflp_thm of
+            SOME reflp_thm =>
+              let
+                val id_abs_transfer = generate_parametric_id lthy rty
+                  (Lifting_Term.parametrize_transfer_rule lthy
+                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
+                val bi_total = parametrize_class_constraint lthy pcrel_def 
+                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+                val thms = 
+                  [("id_abs_transfer",id_abs_transfer),
+                   ("bi_total",       bi_total       )]
+              in
+                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                    [thm])) thms lthy
+              end
+            | NONE =>
+              let
+                val thms = 
+                  [("All_transfer",   @{thm Quotient_All_transfer}   ),
+                   ("Ex_transfer",    @{thm Quotient_Ex_transfer}    ),
+                   ("forall_transfer",@{thm Quotient_forall_transfer})]
+              in
+                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                  [parametrize_quantifier lthy (quot_thm RS thm)])) thms lthy
+              end
+        val rel_eq_transfer = generate_parametric_rel_eq lthy 
+          (Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
+            opt_par_thm
+        val right_unique = parametrize_class_constraint lthy pcrel_def 
+            (quot_thm RS @{thm Quotient_right_unique})
+        val right_total = parametrize_class_constraint lthy pcrel_def 
+            (quot_thm RS @{thm Quotient_right_total})
+        val thms = 
+          [("rel_eq_transfer", rel_eq_transfer),
+           ("right_unique",    right_unique   ), 
+           ("right_total",     right_total    )]      
+      in
+        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+          [thm])) thms lthy
+      end
+
+    fun setup_transfer_rules lthy = 
+      if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
+                                                     else setup_transfer_rules_nonpar lthy
   in
     lthy
-      |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
-        [quot_thm RS @{thm Quotient_right_unique}])
-      |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
-        [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_code quot_thm maybe_reflp_thm
+      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+      |> setup_transfer_rules
   end
 
 (*
@@ -215,8 +476,10 @@
   let
     val transfer_attr = Attrib.internal (K Transfer.transfer_add)
     val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
-    val (T_def, lthy') = define_crel rep_fun lthy
-
+    val (T_def, lthy) = define_crel rep_fun lthy
+    (**)
+    val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
+    (**)    
     val quot_thm = case typedef_set of
       Const ("Orderings.top_class.top", _) => 
         [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
@@ -224,49 +487,109 @@
         [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
       | _ => 
         [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
-
-    val (_, qty) = quot_thm_rty_qty quot_thm
-    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+    val (rty, qty) = quot_thm_rty_qty quot_thm
+    val qty_full_name = (fst o dest_Type) qty
+    val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
     fun qualify suffix = Binding.qualified true suffix qty_name
     val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
+    val opt_reflp_thm = 
+      case typedef_set of
+        Const ("Orderings.top_class.top", _) => 
+          SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
+        | _ =>  NONE
 
-    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}
-          val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
-        in
-          lthy'
-            |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
-              [[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}])
-            |> pair (SOME reflp_thm)
-        end
-      | _ => lthy'
-        |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
-          [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
-        |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
-          [[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
+    fun setup_transfer_rules_nonpar lthy =
+      let
+        val lthy =
+          case opt_reflp_thm of
+            SOME reflp_thm =>
+              let 
+                val thms =
+                  [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
+                   ("bi_total",       @{thm Quotient_bi_total}       )]
+              in
+                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                    [[quot_thm, reflp_thm] MRSL thm])) thms lthy
+              end
+            | NONE =>
+              let
+                val thms = 
+                  [("All_transfer",   @{thm typedef_All_transfer}   ),
+                   ("Ex_transfer",    @{thm typedef_Ex_transfer}    )]
+              in
+                lthy
+                |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
+                  [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
+                |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                  [[typedef_thm, T_def] MRSL thm])) thms
+              end
+        val thms = 
+          [("rep_transfer", @{thm typedef_rep_transfer}),
+           ("bi_unique",    @{thm typedef_bi_unique}   ),
+           ("right_unique", @{thm typedef_right_unique}), 
+           ("right_total",  @{thm typedef_right_total} )]
+      in
+        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+          [[typedef_thm, T_def] MRSL thm])) thms lthy
+      end
+
+    fun setup_transfer_rules_par lthy =
+      let
+        val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+        val lthy =
+          case opt_reflp_thm of
+            SOME reflp_thm =>
+              let
+                val id_abs_transfer = generate_parametric_id lthy rty
+                  (Lifting_Term.parametrize_transfer_rule lthy
+                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
+                val bi_total = parametrize_class_constraint lthy pcrel_def 
+                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+                val thms = 
+                  [("id_abs_transfer",id_abs_transfer),
+                   ("bi_total",       bi_total       )]
+              in
+                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                    [thm])) thms lthy
+              end
+            | NONE =>
+              let
+                val thms = 
+                  ("forall_transfer", simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})) 
+                  ::
+                  (map_snd (fn thm => [typedef_thm, T_def] MRSL thm)                
+                  [("All_transfer", @{thm typedef_All_transfer}),
+                   ("Ex_transfer",  @{thm typedef_Ex_transfer} )])
+              in
+                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+                  [parametrize_quantifier lthy thm])) thms lthy
+              end
+        val thms = 
+          ("rep_transfer", generate_parametric_id lthy rty 
+            (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer})))
+          ::
+          (map_snd (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
+          [("bi_unique",    @{thm typedef_bi_unique} ),
+           ("right_unique", @{thm typedef_right_unique}), 
+           ("right_total",  @{thm typedef_right_total} )])
+      in
+        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
+          [thm])) thms lthy
+      end
+
+    fun setup_transfer_rules lthy = 
+      if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
+                                                     else setup_transfer_rules_nonpar lthy
+
   in
-    lthy''
+    lthy
       |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
-        [quot_thm])
-      |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
-        [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
-      |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]), 
-        [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
-      |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
-        [[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_code quot_thm maybe_reflp_thm
+            [quot_thm])
+      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+      |> setup_transfer_rules
   end
 
-fun setup_lifting_cmd gen_code xthm opt_reflp_xthm lthy =
+fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy =
   let 
     val input_thm = singleton (Attrib.eval_thms lthy) xthm
     val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
@@ -283,15 +606,14 @@
       end
 
     fun setup_quotient () = 
-      case opt_reflp_xthm of
-        SOME reflp_xthm => 
-          let
-            val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
-            val _ = sanity_check_reflp_thm reflp_thm
-          in
-            setup_by_quotient gen_code input_thm (SOME reflp_thm) lthy
-          end
-        | NONE => setup_by_quotient gen_code input_thm NONE lthy
+      let
+        val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
+        val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
+        val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
+      in
+        setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
+      end
+      
 
     fun setup_typedef () = 
       case opt_reflp_xthm of
@@ -310,6 +632,8 @@
 val _ = 
   Outer_Syntax.local_theory @{command_spec "setup_lifting"}
     "setup lifting infrastructure" 
-      (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))
+      (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm 
+      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >> 
+        (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => 
+          setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
 end;
diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -8,6 +8,7 @@
 sig
   exception QUOT_THM of typ * typ * Pretty.T
   exception PARAM_QUOT_THM of typ * Pretty.T
+  exception MERGE_TRANSFER_REL of Pretty.T
   exception CHECK_RTY of typ * typ
 
   val prove_quot_thm: Proof.context -> typ * typ -> thm
@@ -19,6 +20,10 @@
   val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context
 
   val generate_parametrized_relator: Proof.context -> typ -> term * term list
+
+  val merge_transfer_relations: Proof.context -> cterm -> thm
+
+  val parametrize_transfer_rule: Proof.context -> thm -> thm
 end
 
 structure Lifting_Term: LIFTING_TERM =
@@ -30,6 +35,7 @@
 exception QUOT_THM_INTERNAL of Pretty.T
 exception QUOT_THM of typ * typ * Pretty.T
 exception PARAM_QUOT_THM of typ * Pretty.T
+exception MERGE_TRANSFER_REL of Pretty.T
 exception CHECK_RTY of typ * typ
 
 fun match ctxt err ty_pat ty =
@@ -53,16 +59,41 @@
        Pretty.str "don't match."])
   end
 
+fun get_quot_data ctxt s =
+  case Lifting_Info.lookup_quotients ctxt s of
+    SOME qdata => qdata
+  | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
+    [Pretty.str ("No quotient type " ^ quote s), 
+     Pretty.brk 1, 
+     Pretty.str "found."])
+
 fun get_quot_thm ctxt s =
   let
     val thy = Proof_Context.theory_of ctxt
   in
-    (case Lifting_Info.lookup_quotients ctxt s of
-      SOME qdata => Thm.transfer thy (#quot_thm qdata)
-    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
-      [Pretty.str ("No quotient type " ^ quote s), 
-       Pretty.brk 1, 
-       Pretty.str "found."]))
+    Thm.transfer thy (#quot_thm (get_quot_data ctxt s))
+  end
+
+fun get_pcrel_info ctxt s =
+  case #pcrel_info (get_quot_data ctxt s) of
+    SOME pcrel_info => pcrel_info
+  | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
+    [Pretty.str ("No parametrized correspondce relation for " ^ quote s), 
+     Pretty.brk 1, 
+     Pretty.str "found."])
+
+fun get_pcrel_def ctxt s =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in
+    Thm.transfer thy (#pcrel_def (get_pcrel_info ctxt s))
+  end
+
+fun get_pcr_cr_eq ctxt s =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in
+    Thm.transfer thy (#pcr_cr_eq (get_pcrel_info ctxt s))
   end
 
 fun get_rel_quot_thm ctxt s =
@@ -77,6 +108,22 @@
        Pretty.str "found."]))
   end
 
+fun get_rel_distr_rules ctxt s tm =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in
+    (case Lifting_Info.lookup_relator_distr_data ctxt s of
+      SOME rel_distr_thm => (
+        case tm of
+          Const (@{const_name POS}, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm)
+          | Const (@{const_name NEG}, _) => map (Thm.transfer thy) (#neg_distr_rules rel_distr_thm)
+      )
+    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
+      [Pretty.str ("No relator distr. data for the type " ^ quote s), 
+       Pretty.brk 1,
+       Pretty.str "found."]))
+  end
+
 fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
 
 fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
@@ -145,6 +192,17 @@
           rel_quot_thm_prems
       end
 
+fun instantiate_rtys ctxt  (Type (rty_name, _)) (qty as Type (qty_name, _)) =
+  let
+    val quot_thm = get_quot_thm ctxt qty_name
+    val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
+    val _ = check_raw_types (rty_name, rs) qty_name
+    val qtyenv = match ctxt equiv_match_err qty_pat qty
+  in
+    map (Envir.subst_type qtyenv) rtys
+  end
+  | instantiate_rtys _ _ _ = error "instantiate_rtys: not Type"
+
 fun prove_schematic_quot_thm ctxt (rty, qty) =
   (case (rty, qty) of
     (Type (s, tys), Type (s', tys')) =>
@@ -161,18 +219,15 @@
         end
       else
         let
-          val quot_thm = get_quot_thm ctxt s'
-          val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
-          val _ = check_raw_types (s, rs) s'
-          val qtyenv = match ctxt equiv_match_err qty_pat qty
-          val rtys' = map (Envir.subst_type qtyenv) rtys
+          val rtys' = instantiate_rtys ctxt rty qty
           val args = map (prove_schematic_quot_thm ctxt) (tys ~~ rtys')
         in
           if forall is_id_quot args
           then
-            quot_thm
+            get_quot_thm ctxt s'
           else
             let
+              val quot_thm = get_quot_thm ctxt s'
               val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
             in
               [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
@@ -286,7 +341,7 @@
         in
           (args MRSL (get_rel_quot_thm ctxt s), table_ctxt)
         end 
-      | generate (ty as (TFree _)) (table, ctxt) =
+      | generate ty (table, ctxt) =
         if AList.defined (op=) table ty 
         then (the (AList.lookup (op=) table ty), (table, ctxt))
         else 
@@ -298,7 +353,6 @@
           in
             (Q_thm, (table', ctxt'))
           end
-      | generate _ _ = error "generate_param_quot_thm: TVar"
 
     val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt)
   in
@@ -317,4 +371,156 @@
     (hd exported_terms, tl exported_terms)
   end
 
+(* Parametrization *)
+
+local
+  fun get_lhs rule = (Thm.dest_fun o Thm.dest_arg o strip_imp_concl o cprop_of) rule;
+  
+  fun no_imp _ = raise CTERM ("no implication", []);
+  
+  infix 0 else_imp
+
+  fun (cv1 else_imp cv2) ct =
+    (cv1 ct
+      handle THM _ => cv2 ct
+        | CTERM _ => cv2 ct
+        | TERM _ => cv2 ct
+        | TYPE _ => cv2 ct);
+  
+  fun first_imp cvs = fold_rev (curry op else_imp) cvs no_imp
+  
+  fun rewr_imp rule ct = 
+    let
+      val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+      val lhs_rule = get_lhs rule1;
+      val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1;
+      val lhs_ct = Thm.dest_fun ct
+    in
+        Thm.instantiate (Thm.match (lhs_rule, lhs_ct)) rule2
+          handle Pattern.MATCH => raise CTERM ("rewr_imp", [lhs_rule, lhs_ct])
+   end
+  
+  fun rewrs_imp rules = first_imp (map rewr_imp rules)
+
+  fun map_interrupt f l =
+    let
+      fun map_interrupt' _ [] l = SOME (rev l)
+       | map_interrupt' f (x::xs) l = (case f x of
+        NONE => NONE
+        | SOME v => map_interrupt' f xs (v::l))
+    in
+      map_interrupt' f l []
+    end
+in
+  fun merge_transfer_relations ctxt ctm =
+    let
+      val ctm = Thm.dest_arg ctm
+      val tm = term_of ctm
+      val rel = (hd o get_args 2) tm
+  
+      fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
+        | same_constants _ _  = false
+      
+      fun prove_extra_assms ctxt ctm distr_rule =
+        let
+          fun prove_assm assm = try (Goal.prove ctxt [] [] (term_of assm))
+            (fn _ => SOLVED' (REPEAT_ALL_NEW (resolve_tac (Transfer.get_transfer_raw ctxt))) 1)
+  
+          fun is_POS_or_NEG ctm =
+            case (head_of o term_of o Thm.dest_arg) ctm of
+              Const (@{const_name POS}, _) => true
+              | Const (@{const_name NEG}, _) => true
+              | _ => false
+  
+          val inst_distr_rule = rewr_imp distr_rule ctm
+          val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule)
+          val proved_assms = map_interrupt prove_assm extra_assms
+        in
+          Option.map (curry op OF inst_distr_rule) proved_assms
+        end
+        handle CTERM _ => NONE
+  
+      fun cannot_merge_error_msg () = Pretty.block
+         [Pretty.str "Rewriting (merging) of this term has failed:",
+          Pretty.brk 1,
+          Syntax.pretty_term ctxt rel]
+  
+    in
+      case get_args 2 rel of
+          [Const (@{const_name "HOL.eq"}, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
+          | [_, Const (@{const_name "HOL.eq"}, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
+          | [_, trans_rel] =>
+            let
+              val (rty', qty) = (relation_types o fastype_of) trans_rel
+              val r = (fst o dest_Type) rty' 
+              val q = (fst o dest_Type) qty
+            in
+              if r = q then
+                let
+                  val distr_rules = get_rel_distr_rules ctxt r (head_of tm)
+                  val distr_rule = get_first (prove_extra_assms ctxt ctm) distr_rules
+                in
+                  case distr_rule of
+                    NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
+                    | SOME distr_rule =>  (map (merge_transfer_relations ctxt) (cprems_of distr_rule)) 
+                      MRSL distr_rule
+                end
+              else
+                let 
+                  val pcrel_def = get_pcrel_def ctxt q
+                  val pcrel_const = (head_of o fst o Logic.dest_equals o prop_of) pcrel_def
+                in
+                  if same_constants pcrel_const (head_of trans_rel) then
+                    let
+                      val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
+                      val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
+                      val result = (map (merge_transfer_relations ctxt) (cprems_of distr_rule)) MRSL distr_rule
+                      val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
+                    in  
+                      Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv 
+                        (Conv.arg_conv (Conv.arg_conv fold_pcr_rel)) fold_pcr_rel)) result
+                    end
+                  else
+                    raise MERGE_TRANSFER_REL (Pretty.str "Non-parametric correspondence relation used.")
+                end
+            end
+    end
+    handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
+end
+
+fun parametrize_transfer_rule ctxt thm =
+  let
+    fun parametrize_relation_conv ctm =
+      let
+        val (rty, qty) = (relation_types o fastype_of) (term_of ctm)
+      in
+        case (rty, qty) of
+          (Type (r, rargs), Type (q, qargs)) =>
+            if r = q then
+              if forall op= (rargs ~~ qargs) then
+                Conv.all_conv ctm
+              else
+                all_args_conv parametrize_relation_conv ctm
+            else
+              if forall op= (rargs ~~ (instantiate_rtys ctxt rty qty)) then
+                let
+                  val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq ctxt q)
+                in
+                  Conv.rewr_conv pcr_cr_eq ctm
+                end
+                handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm
+              else
+                (let 
+                  val pcrel_def = Thm.symmetric (get_pcrel_def ctxt q)
+                in
+                  (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
+                end
+                handle QUOT_THM_INTERNAL _ => 
+                  (Conv.arg1_conv (all_args_conv parametrize_relation_conv)) ctm)
+          | _ => Conv.all_conv ctm
+      end
+    in
+      Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
+    end
+
 end;
diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -8,6 +8,7 @@
 sig
   val MRSL: thm list * thm -> thm
   val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
+  val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list
   val dest_Quotient: term -> term * term * term * term
 
   val quot_thm_rel: thm -> term
@@ -15,6 +16,19 @@
   val quot_thm_rep: thm -> term
   val quot_thm_crel: thm -> term
   val quot_thm_rty_qty: thm -> typ * typ
+
+  val undisch: thm -> thm
+  val undisch_all: thm -> thm
+  val is_fun_type: typ -> bool
+  val get_args: int -> term -> term list
+  val strip_args: int -> term -> term
+  val all_args_conv: conv -> conv
+  val is_Type: typ -> bool
+  val is_fun_rel: term -> bool
+  val relation_types: typ -> typ * typ
+  val bottom_rewr_conv: thm list -> conv
+  val mk_HOL_eq: thm -> thm
+  val safe_HOL_meta_eq: thm -> thm
 end;
 
 
@@ -28,6 +42,8 @@
 fun option_fold a _ NONE = a
   | option_fold _ f (SOME x) = f x
 
+fun map_snd f xs = map (fn (a, b) => (a, f b)) xs
+
 fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
       = (rel, abs, rep, cr)
   | dest_Quotient t = raise TERM ("dest_Quotient", [t])
@@ -61,4 +77,40 @@
     (domain_type abs_type, range_type abs_type)
   end
 
+fun undisch thm =
+  let
+    val assm = Thm.cprem_of thm 1
+  in
+    Thm.implies_elim thm (Thm.assume assm)
+  end
+
+fun undisch_all thm = funpow (nprems_of thm) undisch thm
+
+fun is_fun_type (Type (@{type_name fun}, _)) = true
+  | is_fun_type _ = false
+
+fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
+
+fun strip_args n = funpow n (fst o dest_comb)
+
+fun all_args_conv conv ctm = 
+  (Conv.combination_conv (Conv.try_conv (all_args_conv conv)) conv) ctm
+
+fun is_Type (Type _) = true
+  | is_Type _ = false
+
+fun is_fun_rel (Const (@{const_name "fun_rel"}, _) $ _ $ _) = true
+  | is_fun_rel _ = false
+
+fun relation_types typ = 
+  case strip_type typ of
+    ([typ1, typ2], @{typ bool}) => (typ1, typ2)
+    | _ => error "relation_types: not a relation"
+
+fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
+
+fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq}
+
+fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
+
 end;
diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -7,13 +7,13 @@
 signature QUOTIENT_TYPE =
 sig
   val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
+    ((binding * binding) option * bool * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
 
   val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * 
-    ((binding * binding) option * bool) -> Proof.context -> Proof.state
+    ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
 
-  val quotient_type_cmd: (((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
-    (binding * binding) option -> Proof.context -> Proof.state
+  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
+    (binding * binding) option) * (Facts.ref * Args.src list) option -> Proof.context -> Proof.state
 end;
 
 structure Quotient_Type: QUOTIENT_TYPE =
@@ -110,7 +110,7 @@
     (def_thm, lthy'')
   end;
 
-fun setup_lifting_package gen_code quot3_thm equiv_thm lthy =
+fun setup_lifting_package gen_code quot3_thm equiv_thm opt_par_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
@@ -128,11 +128,11 @@
       )
   in
     lthy'
-      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm
+      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm opt_par_thm
       |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
   end
 
-fun init_quotient_infr gen_code quot_thm equiv_thm lthy =
+fun init_quotient_infr gen_code quot_thm equiv_thm opt_par_thm lthy =
   let
     val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
     val (qtyp, rtyp) = (dest_funT o fastype_of) rep
@@ -147,11 +147,11 @@
       |> 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))
-      |> setup_lifting_package gen_code quot_thm equiv_thm
+      |> setup_lifting_package gen_code quot_thm equiv_thm opt_par_thm
   end
 
 (* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), equiv_thm) lthy =
   let
     val part_equiv =
       if partial
@@ -203,7 +203,7 @@
       quot_thm = quotient_thm}
 
     val lthy4 = lthy3
-      |> init_quotient_infr gen_code quotient_thm equiv_thm
+      |> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm
       |> (snd oo Local_Theory.note)
         ((equiv_thm_name,
           if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
@@ -314,7 +314,7 @@
 
 fun quotient_type_cmd spec lthy =
   let
-    fun parse_spec ((((((gen_code, 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), opt_par_xthm) lthy =
       let
         val rty = Syntax.read_typ lthy rty_str
         val tmp_lthy1 = Variable.declare_typ rty lthy
@@ -323,8 +323,9 @@
           |> Type.constraint (rty --> rty --> @{typ bool})
           |> Syntax.check_term tmp_lthy1
         val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
+        val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
       in
-        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
+        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), tmp_lthy2)
       end
 
     val (spec', _) = parse_spec spec lthy
@@ -343,6 +344,7 @@
       Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
         (@{keyword "/"} |-- (partial -- Parse.term))  --
         Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
+          -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
diff -r 65f4284d3f1a -r 84d01fd733cf src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/transfer.ML	Fri Mar 08 13:14:23 2013 +0100
@@ -9,6 +9,7 @@
   val prep_conv: conv
   val get_relator_eq: Proof.context -> thm list
   val get_sym_relator_eq: Proof.context -> thm list
+  val get_transfer_raw: Proof.context -> thm list
   val transfer_add: attribute
   val transfer_del: attribute
   val transfer_rule_of_term: Proof.context -> term -> thm