lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
authorkuncar
Fri Mar 08 13:14:23 2013 +0100 (2013-03-08)
changeset 5137484d01fd733cf
parent 51373 65f4284d3f1a
child 51375 d9e62d9c98de
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
src/HOL/Lifting.thy
src/HOL/Tools/Lifting/lifting_def.ML
src/HOL/Tools/Lifting/lifting_info.ML
src/HOL/Tools/Lifting/lifting_setup.ML
src/HOL/Tools/Lifting/lifting_term.ML
src/HOL/Tools/Lifting/lifting_util.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/transfer.ML
     1.1 --- a/src/HOL/Lifting.thy	Fri Mar 08 11:28:20 2013 +0100
     1.2 +++ b/src/HOL/Lifting.thy	Fri Mar 08 13:14:23 2013 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  theory Lifting
     1.5  imports Equiv_Relations Transfer
     1.6  keywords
     1.7 +  "parametric" and
     1.8    "print_quotmaps" "print_quotients" :: diag and
     1.9    "lift_definition" :: thy_goal and
    1.10    "setup_lifting" :: thy_decl
    1.11 @@ -342,6 +343,16 @@
    1.12    unfolding bi_unique_def T_def
    1.13    by (simp add: type_definition.Rep_inject [OF type])
    1.14  
    1.15 +(* the following two theorems are here only for convinience *)
    1.16 +
    1.17 +lemma typedef_right_unique: "right_unique T"
    1.18 +  using T_def type Quotient_right_unique typedef_to_Quotient 
    1.19 +  by blast
    1.20 +
    1.21 +lemma typedef_right_total: "right_total T"
    1.22 +  using T_def type Quotient_right_total typedef_to_Quotient 
    1.23 +  by blast
    1.24 +
    1.25  lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
    1.26    unfolding fun_rel_def T_def by simp
    1.27  
    1.28 @@ -410,6 +421,125 @@
    1.29  lemma reflp_equality: "reflp (op =)"
    1.30  by (auto intro: reflpI)
    1.31  
    1.32 +text {* Proving a parametrized correspondence relation *}
    1.33 +
    1.34 +lemma eq_OO: "op= OO R = R"
    1.35 +unfolding OO_def by metis
    1.36 +
    1.37 +definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
    1.38 +"POS A B \<equiv> A \<le> B"
    1.39 +
    1.40 +definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
    1.41 +"NEG A B \<equiv> B \<le> A"
    1.42 +
    1.43 +definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    1.44 +  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    1.45 +
    1.46 +(*
    1.47 +  The following two rules are here because we don't have any proper
    1.48 +  left-unique ant left-total relations. Left-unique and left-total
    1.49 +  assumptions show up in distributivity rules for the function type.
    1.50 +*)
    1.51 +
    1.52 +lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R"
    1.53 +unfolding bi_unique_def left_unique_def by blast
    1.54 +
    1.55 +lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R"
    1.56 +unfolding bi_total_def left_total_def by blast
    1.57 +
    1.58 +lemma pos_OO_eq:
    1.59 +  shows "POS (A OO op=) A"
    1.60 +unfolding POS_def OO_def by blast
    1.61 +
    1.62 +lemma pos_eq_OO:
    1.63 +  shows "POS (op= OO A) A"
    1.64 +unfolding POS_def OO_def by blast
    1.65 +
    1.66 +lemma neg_OO_eq:
    1.67 +  shows "NEG (A OO op=) A"
    1.68 +unfolding NEG_def OO_def by auto
    1.69 +
    1.70 +lemma neg_eq_OO:
    1.71 +  shows "NEG (op= OO A) A"
    1.72 +unfolding NEG_def OO_def by blast
    1.73 +
    1.74 +lemma POS_trans:
    1.75 +  assumes "POS A B"
    1.76 +  assumes "POS B C"
    1.77 +  shows "POS A C"
    1.78 +using assms unfolding POS_def by auto
    1.79 +
    1.80 +lemma NEG_trans:
    1.81 +  assumes "NEG A B"
    1.82 +  assumes "NEG B C"
    1.83 +  shows "NEG A C"
    1.84 +using assms unfolding NEG_def by auto
    1.85 +
    1.86 +lemma POS_NEG:
    1.87 +  "POS A B \<equiv> NEG B A"
    1.88 +  unfolding POS_def NEG_def by auto
    1.89 +
    1.90 +lemma NEG_POS:
    1.91 +  "NEG A B \<equiv> POS B A"
    1.92 +  unfolding POS_def NEG_def by auto
    1.93 +
    1.94 +lemma POS_pcr_rule:
    1.95 +  assumes "POS (A OO B) C"
    1.96 +  shows "POS (A OO B OO X) (C OO X)"
    1.97 +using assms unfolding POS_def OO_def by blast
    1.98 +
    1.99 +lemma NEG_pcr_rule:
   1.100 +  assumes "NEG (A OO B) C"
   1.101 +  shows "NEG (A OO B OO X) (C OO X)"
   1.102 +using assms unfolding NEG_def OO_def by blast
   1.103 +
   1.104 +lemma POS_apply:
   1.105 +  assumes "POS R R'"
   1.106 +  assumes "R f g"
   1.107 +  shows "R' f g"
   1.108 +using assms unfolding POS_def by auto
   1.109 +
   1.110 +text {* Proving a parametrized correspondence relation *}
   1.111 +
   1.112 +lemma fun_mono:
   1.113 +  assumes "A \<ge> C"
   1.114 +  assumes "B \<le> D"
   1.115 +  shows   "(A ===> B) \<le> (C ===> D)"
   1.116 +using assms unfolding fun_rel_def by blast
   1.117 +
   1.118 +lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
   1.119 +unfolding OO_def fun_rel_def by blast
   1.120 +
   1.121 +lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
   1.122 +unfolding right_unique_def left_total_def by blast
   1.123 +
   1.124 +lemma functional_converse_relation: "left_unique R \<Longrightarrow> right_total R \<Longrightarrow> \<forall>y. \<exists>!x. R x y"
   1.125 +unfolding left_unique_def right_total_def by blast
   1.126 +
   1.127 +lemma neg_fun_distr1:
   1.128 +assumes 1: "left_unique R" "right_total R"
   1.129 +assumes 2: "right_unique R'" "left_total R'"
   1.130 +shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
   1.131 +  using functional_relation[OF 2] functional_converse_relation[OF 1]
   1.132 +  unfolding fun_rel_def OO_def
   1.133 +  apply clarify
   1.134 +  apply (subst all_comm)
   1.135 +  apply (subst all_conj_distrib[symmetric])
   1.136 +  apply (intro choice)
   1.137 +  by metis
   1.138 +
   1.139 +lemma neg_fun_distr2:
   1.140 +assumes 1: "right_unique R'" "left_total R'"
   1.141 +assumes 2: "left_unique S'" "right_total S'"
   1.142 +shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
   1.143 +  using functional_converse_relation[OF 2] functional_relation[OF 1]
   1.144 +  unfolding fun_rel_def OO_def
   1.145 +  apply clarify
   1.146 +  apply (subst all_comm)
   1.147 +  apply (subst all_conj_distrib[symmetric])
   1.148 +  apply (intro choice)
   1.149 +  by metis
   1.150 +
   1.151  subsection {* ML setup *}
   1.152  
   1.153  ML_file "Tools/Lifting/lifting_util.ML"
   1.154 @@ -417,8 +547,12 @@
   1.155  ML_file "Tools/Lifting/lifting_info.ML"
   1.156  setup Lifting_Info.setup
   1.157  
   1.158 +lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
   1.159 +
   1.160 +(* setup for the function type *)
   1.161  declare fun_quotient[quot_map]
   1.162 -lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
   1.163 +declare fun_mono[relator_mono]
   1.164 +lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
   1.165  
   1.166  ML_file "Tools/Lifting/lifting_term.ML"
   1.167  
   1.168 @@ -426,6 +560,6 @@
   1.169  
   1.170  ML_file "Tools/Lifting/lifting_setup.ML"
   1.171  
   1.172 -hide_const (open) invariant
   1.173 +hide_const (open) invariant POS NEG
   1.174  
   1.175  end
     2.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 08 11:28:20 2013 +0100
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Mar 08 13:14:23 2013 +0100
     2.3 @@ -6,11 +6,14 @@
     2.4  
     2.5  signature LIFTING_DEF =
     2.6  sig
     2.7 +  val generate_parametric_transfer_rule:
     2.8 +    Proof.context -> thm -> thm -> thm
     2.9 +
    2.10    val add_lift_def:
    2.11 -    (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
    2.12 +    (binding * mixfix) -> typ -> term -> thm -> thm option -> local_theory -> local_theory
    2.13  
    2.14    val lift_def_cmd:
    2.15 -    (binding * string option * mixfix) * string -> local_theory -> Proof.state
    2.16 +    (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
    2.17  
    2.18    val can_generate_code_cert: thm -> bool
    2.19  end;
    2.20 @@ -22,6 +25,103 @@
    2.21  
    2.22  infix 0 MRSL
    2.23  
    2.24 +(* Generation of a transfer rule *)
    2.25 +
    2.26 +fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
    2.27 +  let
    2.28 +    fun preprocess ctxt thm =
    2.29 +      let
    2.30 +        val tm = (strip_args 2 o HOLogic.dest_Trueprop o concl_of) thm;
    2.31 +        val param_rel = (snd o dest_comb o fst o dest_comb) tm;
    2.32 +        val thy = Proof_Context.theory_of ctxt;
    2.33 +        val free_vars = Term.add_vars param_rel [];
    2.34 +        
    2.35 +        fun make_subst (var as (_, typ)) subst = 
    2.36 +          let
    2.37 +            val [rty, rty'] = binder_types typ
    2.38 +          in
    2.39 +            if (Term.is_TVar rty andalso is_Type rty') then
    2.40 +              (Var var, HOLogic.eq_const rty')::subst
    2.41 +            else
    2.42 +              subst
    2.43 +          end;
    2.44 +        
    2.45 +        val subst = fold make_subst free_vars [];
    2.46 +        val csubst = map (pairself (cterm_of thy)) subst;
    2.47 +        val inst_thm = Drule.cterm_instantiate csubst thm;
    2.48 +      in
    2.49 +        Conv.fconv_rule 
    2.50 +          ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
    2.51 +            (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
    2.52 +      end
    2.53 +
    2.54 +    fun inst_relcomppI thy ant1 ant2 =
    2.55 +      let
    2.56 +        val t1 = (HOLogic.dest_Trueprop o concl_of) ant1
    2.57 +        val t2 = (HOLogic.dest_Trueprop o prop_of) ant2
    2.58 +        val fun1 = cterm_of thy (strip_args 2 t1)
    2.59 +        val args1 = map (cterm_of thy) (get_args 2 t1)
    2.60 +        val fun2 = cterm_of thy (strip_args 2 t2)
    2.61 +        val args2 = map (cterm_of thy) (get_args 1 t2)
    2.62 +        val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
    2.63 +        val vars = (rev (Term.add_vars (prop_of relcomppI) []))
    2.64 +        val subst = map (apfst ((cterm_of thy) o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
    2.65 +      in
    2.66 +        Drule.cterm_instantiate subst relcomppI
    2.67 +      end
    2.68 +
    2.69 +    fun zip_transfer_rules ctxt thm = 
    2.70 +      let
    2.71 +        val thy = Proof_Context.theory_of ctxt
    2.72 +        fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
    2.73 +        val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
    2.74 +        val typ = (typ_of o ctyp_of_term) rel
    2.75 +        val POS_const = cterm_of thy (mk_POS typ)
    2.76 +        val var = cterm_of thy (Var (("X", #maxidx (rep_cterm (rel)) + 1), typ))
    2.77 +        val goal = Thm.apply (cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
    2.78 +      in
    2.79 +        [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
    2.80 +      end
    2.81 +     
    2.82 +    val thm = (inst_relcomppI (Proof_Context.theory_of ctxt) parametric_transfer_rule transfer_rule) 
    2.83 +                OF [parametric_transfer_rule, transfer_rule]
    2.84 +    val preprocessed_thm = preprocess ctxt thm
    2.85 +    val orig_ctxt = ctxt
    2.86 +    val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
    2.87 +    val assms = cprems_of fixed_thm
    2.88 +    val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
    2.89 +    val ctxt = Context.proof_map(fold (add_transfer_rule o Thm.assume) assms) ctxt
    2.90 +    val zipped_thm =
    2.91 +      fixed_thm
    2.92 +      |> undisch_all
    2.93 +      |> zip_transfer_rules ctxt
    2.94 +      |> implies_intr_list assms
    2.95 +      |> singleton (Variable.export ctxt orig_ctxt)
    2.96 +  in
    2.97 +    zipped_thm
    2.98 +  end
    2.99 +
   2.100 +fun print_generate_transfer_info msg = 
   2.101 +  let
   2.102 +    val error_msg = cat_lines 
   2.103 +      ["Generation of a parametric transfer rule failed.",
   2.104 +      (Pretty.string_of (Pretty.block
   2.105 +         [Pretty.str "Reason:", Pretty.brk 2, msg]))]
   2.106 +  in
   2.107 +    error error_msg
   2.108 +  end
   2.109 +
   2.110 +fun generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm =
   2.111 +  let
   2.112 +    val transfer_rule =
   2.113 +      ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
   2.114 +      |> Morphism.thm (Local_Theory.target_morphism lthy)
   2.115 +      |> Lifting_Term.parametrize_transfer_rule lthy
   2.116 +  in
   2.117 +    (option_fold transfer_rule (generate_parametric_transfer_rule lthy transfer_rule) opt_par_thm
   2.118 +    handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; transfer_rule))
   2.119 +  end
   2.120 +
   2.121  (* Generation of the code certificate from the rsp theorem *)
   2.122  
   2.123  fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
   2.124 @@ -233,8 +333,8 @@
   2.125    else
   2.126      lthy
   2.127    
   2.128 -fun define_code_using_rep_eq maybe_rep_eq_thm lthy = 
   2.129 -  case maybe_rep_eq_thm of
   2.130 +fun define_code_using_rep_eq opt_rep_eq_thm lthy = 
   2.131 +  case opt_rep_eq_thm of
   2.132      SOME rep_eq_thm =>   
   2.133        let
   2.134          val add_abs_eqn_attribute = 
   2.135 @@ -267,7 +367,7 @@
   2.136        false
   2.137    end
   2.138  
   2.139 -fun define_code abs_eq_thm maybe_rep_eq_thm (rty, qty) lthy =
   2.140 +fun define_code abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
   2.141    let
   2.142      val (rty_body, qty_body) = get_body_types (rty, qty)
   2.143    in
   2.144 @@ -275,7 +375,7 @@
   2.145        if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
   2.146          (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
   2.147        else
   2.148 -        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the maybe_rep_eq_thm]) lthy
   2.149 +        (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the opt_rep_eq_thm]) lthy
   2.150      else
   2.151        let 
   2.152          val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
   2.153 @@ -283,7 +383,7 @@
   2.154          if has_constr lthy body_quot_thm then
   2.155            define_code_using_abs_eq abs_eq_thm lthy
   2.156          else if has_abstr lthy body_quot_thm then
   2.157 -          define_code_using_rep_eq maybe_rep_eq_thm lthy
   2.158 +          define_code_using_rep_eq opt_rep_eq_thm lthy
   2.159          else
   2.160            lthy
   2.161        end
   2.162 @@ -300,7 +400,7 @@
   2.163      i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
   2.164  *)
   2.165  
   2.166 -fun add_lift_def var qty rhs rsp_thm lthy =
   2.167 +fun add_lift_def var qty rhs rsp_thm opt_par_thm lthy =
   2.168    let
   2.169      val rty = fastype_of rhs
   2.170      val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
   2.171 @@ -316,10 +416,10 @@
   2.172        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
   2.173  
   2.174      fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
   2.175 -    val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
   2.176 +    val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
   2.177  
   2.178      val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
   2.179 -    val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
   2.180 +    val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
   2.181  
   2.182      fun qualify defname suffix = Binding.qualified true suffix defname
   2.183  
   2.184 @@ -327,17 +427,17 @@
   2.185      val rsp_thm_name = qualify lhs_name "rsp"
   2.186      val abs_eq_thm_name = qualify lhs_name "abs_eq"
   2.187      val rep_eq_thm_name = qualify lhs_name "rep_eq"
   2.188 -    val transfer_thm_name = qualify lhs_name "transfer"
   2.189 +    val transfer_rule_name = qualify lhs_name "transfer"
   2.190      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   2.191    in
   2.192      lthy'
   2.193        |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
   2.194 -      |> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm])
   2.195 +      |> (snd oo Local_Theory.note) ((transfer_rule_name, [transfer_attr]), [transfer_rule])
   2.196        |> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm])
   2.197 -      |> (case maybe_rep_eq_thm of 
   2.198 +      |> (case opt_rep_eq_thm of 
   2.199              SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
   2.200              | NONE => I)
   2.201 -      |> define_code abs_eq_thm maybe_rep_eq_thm (rty_forced, qty)
   2.202 +      |> define_code abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
   2.203    end
   2.204  
   2.205  fun mk_readable_rsp_thm_eq tm lthy =
   2.206 @@ -397,7 +497,7 @@
   2.207  
   2.208  *)
   2.209  
   2.210 -fun lift_def_cmd (raw_var, rhs_raw) lthy =
   2.211 +fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy =
   2.212    let
   2.213      val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy 
   2.214      val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw
   2.215 @@ -422,23 +522,24 @@
   2.216      val forced_rhs = force_rty_type lthy' rty_forced rhs;
   2.217      val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
   2.218      val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy'
   2.219 -    val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
   2.220 +    val opt_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
   2.221      val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
   2.222      val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm
   2.223 +    val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy')) opt_par_xthm
   2.224  
   2.225      fun after_qed thm_list lthy = 
   2.226        let
   2.227          val internal_rsp_thm =
   2.228            case thm_list of
   2.229 -            [] => the maybe_proven_rsp_thm
   2.230 +            [] => the opt_proven_rsp_thm
   2.231            | [[thm]] => Goal.prove lthy [] [] internal_rsp_tm 
   2.232              (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
   2.233        in
   2.234 -        add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy
   2.235 +        add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
   2.236        end
   2.237  
   2.238    in
   2.239 -    case maybe_proven_rsp_thm of
   2.240 +    case opt_proven_rsp_thm of
   2.241        SOME _ => Proof.theorem NONE after_qed [] lthy'
   2.242        | NONE =>  Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy'
   2.243    end
   2.244 @@ -480,17 +581,16 @@
   2.245        error error_msg
   2.246      end
   2.247  
   2.248 -fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy =
   2.249 -  (lift_def_cmd (raw_var, rhs_raw) lthy
   2.250 +fun lift_def_cmd_with_err_handling (raw_var, rhs_raw, opt_par_xthm) lthy =
   2.251 +  (lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy
   2.252      handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
   2.253      handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => 
   2.254        check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw)
   2.255  
   2.256  (* parser and command *)
   2.257  val liftdef_parser =
   2.258 -  ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
   2.259 -    --| @{keyword "is"} -- Parse.term
   2.260 -
   2.261 +  (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
   2.262 +    --| @{keyword "is"} -- Parse.term -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)) >> Parse.triple1
   2.263  val _ =
   2.264    Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
   2.265      "definition for constants over the quotient type"
     3.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Fri Mar 08 11:28:20 2013 +0100
     3.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Fri Mar 08 13:14:23 2013 +0100
     3.3 @@ -11,7 +11,8 @@
     3.4    val lookup_quotmaps_global: theory -> string -> quotmaps option
     3.5    val print_quotmaps: Proof.context -> unit
     3.6  
     3.7 -  type quotients = {quot_thm: thm, pcrel_def: thm option}
     3.8 +  type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
     3.9 +  type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
    3.10    val transform_quotients: morphism -> quotients -> quotients
    3.11    val lookup_quotients: Proof.context -> string -> quotients option
    3.12    val lookup_quotients_global: theory -> string -> quotients option
    3.13 @@ -25,6 +26,11 @@
    3.14    val add_reflexivity_rule_attribute: attribute
    3.15    val add_reflexivity_rule_attrib: Attrib.src
    3.16  
    3.17 +  type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
    3.18 +    pos_distr_rules: thm list, neg_distr_rules: thm list}
    3.19 +  val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
    3.20 +  val lookup_relator_distr_data_global: theory -> string -> relator_distr_data option
    3.21 +
    3.22    val setup: theory -> theory
    3.23  end;
    3.24  
    3.25 @@ -118,7 +124,8 @@
    3.26    end
    3.27  
    3.28  (* info about quotient types *)
    3.29 -type quotients = {quot_thm: thm, pcrel_def: thm option}
    3.30 +type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
    3.31 +type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
    3.32  
    3.33  structure Quotients = Generic_Data
    3.34  (
    3.35 @@ -128,8 +135,11 @@
    3.36    fun merge data = Symtab.merge (K true) data
    3.37  )
    3.38  
    3.39 -fun transform_quotients phi {quot_thm, pcrel_def} =
    3.40 -  {quot_thm = Morphism.thm phi quot_thm, pcrel_def = Option.map (Morphism.thm phi) pcrel_def}
    3.41 +fun transform_pcrel_info phi {pcrel_def, pcr_cr_eq} =
    3.42 +  {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
    3.43 +
    3.44 +fun transform_quotients phi {quot_thm, pcrel_info} =
    3.45 +  {quot_thm = Morphism.thm phi quot_thm, pcrel_info = Option.map (transform_pcrel_info phi) pcrel_info}
    3.46  
    3.47  val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
    3.48  val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
    3.49 @@ -141,9 +151,9 @@
    3.50      val (_, qtyp) = quot_thm_rty_qty quot_thm
    3.51      val qty_full_name = (fst o dest_Type) qtyp
    3.52      val symtab = Quotients.get ctxt
    3.53 -    val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name
    3.54 +    val opt_stored_quot_thm = Symtab.lookup symtab qty_full_name
    3.55    in
    3.56 -    case maybe_stored_quot_thm of
    3.57 +    case opt_stored_quot_thm of
    3.58        SOME data => 
    3.59          if Thm.eq_thm_prop (#quot_thm data, quot_thm) then
    3.60            Quotients.map (Symtab.delete qty_full_name) ctxt
    3.61 @@ -157,14 +167,16 @@
    3.62  
    3.63  fun print_quotients ctxt =
    3.64    let
    3.65 -    fun prt_quot (qty_name, {quot_thm, pcrel_def}) =
    3.66 +    fun prt_quot (qty_name, {quot_thm, pcrel_info}) =
    3.67        Pretty.block (separate (Pretty.brk 2)
    3.68         [Pretty.str "type:", 
    3.69          Pretty.str qty_name,
    3.70          Pretty.str "quot. thm:",
    3.71          Syntax.pretty_term ctxt (prop_of quot_thm),
    3.72          Pretty.str "pcrel_def thm:",
    3.73 -        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of) pcrel_def])
    3.74 +        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcrel_info,
    3.75 +        Pretty.str "pcr_cr_eq thm:",
    3.76 +        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcrel_info])
    3.77    in
    3.78      map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
    3.79      |> Pretty.big_list "quotients:"
    3.80 @@ -193,6 +205,211 @@
    3.81  val add_reflexivity_rule_attribute = Reflp_Preserve.add
    3.82  val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
    3.83  
    3.84 +(* info about relator distributivity theorems *)
    3.85 +type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
    3.86 +  pos_distr_rules: thm list, neg_distr_rules: thm list}
    3.87 +
    3.88 +fun map_relator_distr_data f1 f2 f3 f4
    3.89 +  {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
    3.90 +  {pos_mono_rule   = f1 pos_mono_rule, 
    3.91 +   neg_mono_rule   = f2 neg_mono_rule,
    3.92 +   pos_distr_rules = f3 pos_distr_rules, 
    3.93 +   neg_distr_rules = f4 neg_distr_rules}
    3.94 +
    3.95 +fun map_pos_mono_rule f = map_relator_distr_data f I I I
    3.96 +fun map_neg_mono_rule f = map_relator_distr_data I f I I
    3.97 +fun map_pos_distr_rules f = map_relator_distr_data I I f I 
    3.98 +fun map_neg_distr_rules f = map_relator_distr_data I I I f
    3.99 +
   3.100 +structure Relator_Distr = Generic_Data
   3.101 +(
   3.102 +  type T = relator_distr_data Symtab.table
   3.103 +  val empty = Symtab.empty
   3.104 +  val extend = I
   3.105 +  fun merge data = Symtab.merge (K true) data
   3.106 +);
   3.107 +
   3.108 +fun introduce_polarities rule =
   3.109 +  let
   3.110 +    val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT
   3.111 +    val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (prems_of rule)
   3.112 +    val equal_prems = filter op= prems_pairs
   3.113 +    val _ = if null equal_prems then () 
   3.114 +      else error "The rule contains reflexive assumptions."
   3.115 +    val concl_pairs = rule 
   3.116 +      |> concl_of
   3.117 +      |> HOLogic.dest_Trueprop
   3.118 +      |> dest_less_eq
   3.119 +      |> pairself (snd o strip_comb)
   3.120 +      |> op~~
   3.121 +      |> filter_out op=
   3.122 +    
   3.123 +    val _ = if has_duplicates op= concl_pairs 
   3.124 +      then error "The rule contains duplicated variables in the conlusion." else ()
   3.125 +
   3.126 +    fun mem a l = member op= l a
   3.127 +
   3.128 +    fun rewrite_prem prem_pair = 
   3.129 +      if mem prem_pair concl_pairs 
   3.130 +      then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))
   3.131 +      else if mem (swap prem_pair) concl_pairs 
   3.132 +        then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
   3.133 +      else error "The rule contains a non-relevant assumption."
   3.134 +    
   3.135 +    fun rewrite_prems [] = Conv.all_conv
   3.136 +      | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs)
   3.137 +    
   3.138 +    val rewrite_prems_conv = rewrite_prems prems_pairs
   3.139 +    val rewrite_concl_conv = 
   3.140 +      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})))
   3.141 +  in
   3.142 +    (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule
   3.143 +  end
   3.144 +  handle 
   3.145 +    TERM _ => error "The rule has a wrong format."
   3.146 +    | CTERM _ => error "The rule has a wrong format."
   3.147 +
   3.148 +fun negate_mono_rule mono_rule = 
   3.149 +  let
   3.150 +    val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}])
   3.151 +  in
   3.152 +    Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
   3.153 +  end;
   3.154 +
   3.155 +fun add_mono_rule mono_rule ctxt = 
   3.156 +  let
   3.157 +    val mono_rule = introduce_polarities mono_rule
   3.158 +    val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
   3.159 +      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
   3.160 +    val _ = if Symtab.defined (Relator_Distr.get ctxt) mono_ruleT_name 
   3.161 +      then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
   3.162 +      else ()
   3.163 +    val neg_mono_rule = negate_mono_rule mono_rule
   3.164 +    val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule, 
   3.165 +      pos_distr_rules = [], neg_distr_rules = []}
   3.166 +  in
   3.167 +    Relator_Distr.map (Symtab.update (mono_ruleT_name, relator_distr_data)) ctxt
   3.168 +  end;
   3.169 +
   3.170 +local 
   3.171 +  fun add_distr_rule update_entry distr_rule ctxt =
   3.172 +    let
   3.173 +      val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
   3.174 +        dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) distr_rule
   3.175 +    in
   3.176 +      if Symtab.defined (Relator_Distr.get ctxt) distr_ruleT_name then 
   3.177 +        Relator_Distr.map (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) ctxt
   3.178 +      else error "The monoticity rule is not defined."
   3.179 +    end
   3.180 +
   3.181 +    fun rewrite_concl_conv thm ctm = 
   3.182 +      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
   3.183 +      handle CTERM _ => error "The rule has a wrong format."
   3.184 +
   3.185 +in
   3.186 +  fun add_pos_distr_rule distr_rule ctxt = 
   3.187 +    let
   3.188 +      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule
   3.189 +      fun update_entry distr_rule data = 
   3.190 +        map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data
   3.191 +    in
   3.192 +      add_distr_rule update_entry distr_rule ctxt
   3.193 +    end
   3.194 +    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
   3.195 +
   3.196 +  
   3.197 +  fun add_neg_distr_rule distr_rule ctxt = 
   3.198 +    let
   3.199 +      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule
   3.200 +      fun update_entry distr_rule data = 
   3.201 +        map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data
   3.202 +    in
   3.203 +      add_distr_rule update_entry distr_rule ctxt
   3.204 +    end
   3.205 +    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
   3.206 +end
   3.207 +
   3.208 +local 
   3.209 +  val eq_refl2 = sym RS @{thm eq_refl}
   3.210 +in
   3.211 +  fun add_eq_distr_rule distr_rule ctxt =
   3.212 +    let 
   3.213 +      val pos_distr_rule = @{thm eq_refl} OF [distr_rule]
   3.214 +      val neg_distr_rule = eq_refl2 OF [distr_rule]
   3.215 +    in
   3.216 +      ctxt 
   3.217 +      |> add_pos_distr_rule pos_distr_rule
   3.218 +      |> add_neg_distr_rule neg_distr_rule
   3.219 +    end
   3.220 +end;
   3.221 +
   3.222 +local
   3.223 +  fun sanity_check rule =
   3.224 +    let
   3.225 +      val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)
   3.226 +      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);
   3.227 +      val (lhs, rhs) = case concl of
   3.228 +        Const ("Orderings.ord_class.less_eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => 
   3.229 +          (lhs, rhs)
   3.230 +        | Const ("Orderings.ord_class.less_eq", _) $ rhs $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) => 
   3.231 +          (lhs, rhs)
   3.232 +        | Const ("HOL.eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => (lhs, rhs)
   3.233 +        | _ => error "The rule has a wrong format."
   3.234 +      
   3.235 +      val lhs_vars = Term.add_vars lhs []
   3.236 +      val rhs_vars = Term.add_vars rhs []
   3.237 +      val assms_vars = fold Term.add_vars assms [];
   3.238 +      val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else ()
   3.239 +      val _ = if subset op= (rhs_vars, lhs_vars) then () 
   3.240 +        else error "Extra variables in the right-hand side of the rule"
   3.241 +      val _ = if subset op= (assms_vars, lhs_vars) then () 
   3.242 +        else error "Extra variables in the assumptions of the rule"
   3.243 +      val rhs_args = (snd o strip_comb) rhs;
   3.244 +      fun check_comp t = case t of 
   3.245 +        Const ("Relation.relcompp", _) $ Var (_, _) $ Var (_,_) => ()
   3.246 +        | _ => error "There is an argument on the rhs that is not a composition."
   3.247 +      val _ = map check_comp rhs_args
   3.248 +    in
   3.249 +      ()
   3.250 +    end
   3.251 +in
   3.252 +
   3.253 +  fun add_distr_rule distr_rule ctxt = 
   3.254 +    let
   3.255 +      val _ = sanity_check distr_rule
   3.256 +      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)
   3.257 +    in
   3.258 +      case concl of
   3.259 +        Const ("Orderings.ord_class.less_eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ => 
   3.260 +          add_pos_distr_rule distr_rule ctxt
   3.261 +        | Const ("Orderings.ord_class.less_eq", _) $ _ $ (Const ("Relation.relcompp",_) $ _ $ _) => 
   3.262 +          add_neg_distr_rule distr_rule ctxt
   3.263 +        | Const ("HOL.eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
   3.264 +          add_eq_distr_rule distr_rule ctxt
   3.265 +    end
   3.266 +end
   3.267 +
   3.268 +fun get_distr_rules_raw ctxt = Symtab.fold 
   3.269 +  (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) 
   3.270 +    (Relator_Distr.get ctxt) []
   3.271 +
   3.272 +fun get_mono_rules_raw ctxt = Symtab.fold 
   3.273 +  (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) 
   3.274 +    (Relator_Distr.get ctxt) []
   3.275 +
   3.276 +val lookup_relator_distr_data = Symtab.lookup o Relator_Distr.get o Context.Proof
   3.277 +val lookup_relator_distr_data_global = Symtab.lookup o Relator_Distr.get o Context.Theory
   3.278 +
   3.279 +val relator_distr_attribute_setup =
   3.280 +  Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
   3.281 +    "declaration of relator's monoticity"
   3.282 +  #> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule))
   3.283 +    "declaration of relator's distributivity over OO"
   3.284 +  #> Global_Theory.add_thms_dynamic
   3.285 +     (@{binding relator_distr_raw}, get_distr_rules_raw)
   3.286 +  #> Global_Theory.add_thms_dynamic
   3.287 +     (@{binding relator_mono_raw}, get_mono_rules_raw)
   3.288 +
   3.289  (* theory setup *)
   3.290  
   3.291  val setup =
   3.292 @@ -200,6 +417,7 @@
   3.293    #> quot_del_attribute_setup
   3.294    #> Invariant_Commute.setup
   3.295    #> Reflp_Preserve.setup
   3.296 +  #> relator_distr_attribute_setup
   3.297  
   3.298  (* outer syntax commands *)
   3.299  
     4.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Mar 08 11:28:20 2013 +0100
     4.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Mar 08 13:14:23 2013 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  sig
     4.5    exception SETUP_LIFTING_INFR of string
     4.6  
     4.7 -  val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
     4.8 +  val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
     4.9  
    4.10    val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
    4.11  end;
    4.12 @@ -26,7 +26,7 @@
    4.13    let
    4.14      val (qty, rty) = (dest_funT o fastype_of) rep_fun
    4.15      val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
    4.16 -    val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
    4.17 +    val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph))
    4.18      val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
    4.19      val crel_name = Binding.prefix_name "cr_" qty_name
    4.20      val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
    4.21 @@ -69,7 +69,7 @@
    4.22      val qty_name = (fst o dest_Type) qty
    4.23      val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
    4.24      val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
    4.25 -    val rhs = relcomp_op $ param_rel_fixed $ fixed_crel;
    4.26 +    val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
    4.27      val definition_term = Logic.mk_equals (lhs, rhs)
    4.28      val ((_, (_, def_thm)), lthy) = Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), 
    4.29        ((Binding.empty, []), definition_term)) lthy
    4.30 @@ -78,16 +78,72 @@
    4.31    end
    4.32    handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy))
    4.33  
    4.34 +
    4.35 +local
    4.36 +  val eq_OO_meta = mk_meta_eq @{thm eq_OO} 
    4.37 +
    4.38 +  fun print_generate_pcr_cr_eq_error ctxt term = 
    4.39 +  let
    4.40 +    val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
    4.41 +    val error_msg = cat_lines 
    4.42 +      ["Generation of a pcr_cr_eq failed.",
    4.43 +      (Pretty.string_of (Pretty.block
    4.44 +         [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
    4.45 +       "Most probably a relator_eq rule for one of the involved types is missing."]
    4.46 +  in
    4.47 +    error error_msg
    4.48 +  end
    4.49 +in
    4.50 +  fun define_pcr_cr_eq lthy pcr_rel_def =
    4.51 +    let
    4.52 +      val lhs = (term_of o Thm.lhs_of) pcr_rel_def
    4.53 +      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
    4.54 +      val args = (snd o strip_comb) lhs
    4.55 +      
    4.56 +      fun make_inst var ctxt = 
    4.57 +        let 
    4.58 +          val typ = (snd o relation_types o snd o dest_Var) var
    4.59 +          val sort = Type.sort_of_atyp typ
    4.60 +          val (fresh_var, ctxt) = yield_singleton Variable.invent_types sort ctxt
    4.61 +          val thy = Proof_Context.theory_of ctxt
    4.62 +        in
    4.63 +          ((cterm_of thy var, cterm_of thy (HOLogic.eq_const (TFree fresh_var))), ctxt)
    4.64 +        end
    4.65 +      
    4.66 +      val orig_lthy = lthy
    4.67 +      val (args_inst, lthy) = fold_map make_inst args lthy
    4.68 +      val pcr_cr_eq = 
    4.69 +        pcr_rel_def
    4.70 +        |> Drule.cterm_instantiate args_inst    
    4.71 +        |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (bottom_rewr_conv (Transfer.get_relator_eq lthy))))
    4.72 +  in
    4.73 +    case (term_of o Thm.rhs_of) pcr_cr_eq of
    4.74 +      Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ => 
    4.75 +        let
    4.76 +          val thm = 
    4.77 +            pcr_cr_eq
    4.78 +            |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
    4.79 +            |> mk_HOL_eq
    4.80 +            |> singleton (Variable.export lthy orig_lthy)
    4.81 +          val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), 
    4.82 +            [thm]) lthy
    4.83 +        in
    4.84 +          (thm, lthy)
    4.85 +        end
    4.86 +      | Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
    4.87 +      | _ => error "generate_pcr_cr_eq: implementation error"
    4.88 +  end
    4.89 +end
    4.90 +
    4.91  fun define_code_constr gen_code quot_thm lthy =
    4.92    let
    4.93      val abs = quot_thm_abs quot_thm
    4.94 -    val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
    4.95    in
    4.96 -    if gen_code andalso is_Const abs_background then
    4.97 +    if gen_code andalso is_Const abs then
    4.98        let
    4.99 -        val (fixed_abs_background, lthy') = yield_singleton(Variable.importT_terms) abs_background lthy
   4.100 +        val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
   4.101        in  
   4.102 -         Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs_background]) lthy'
   4.103 +         Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
   4.104        end
   4.105      else
   4.106        lthy
   4.107 @@ -99,7 +155,7 @@
   4.108        val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
   4.109        val add_abstype_attribute = 
   4.110            Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
   4.111 -        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
   4.112 +        val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
   4.113      in
   4.114        lthy
   4.115          |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
   4.116 @@ -133,15 +189,24 @@
   4.117                                                  @ (map Pretty.string_of errs)))
   4.118    end
   4.119  
   4.120 -fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
   4.121 +fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
   4.122    let
   4.123      val _ = quot_thm_sanity_check lthy quot_thm
   4.124      val (_, qtyp) = quot_thm_rty_qty quot_thm
   4.125      val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy
   4.126 -    val quotients = { quot_thm = quot_thm, pcrel_def = pcrel_def }
   4.127 +    (**)
   4.128 +    val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
   4.129 +    (**)
   4.130 +    val (pcr_cr_eq, lthy) = case pcrel_def of
   4.131 +      SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def)
   4.132 +      | NONE => (NONE, lthy)
   4.133 +    val pcrel_info = case pcrel_def of
   4.134 +      SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
   4.135 +      | NONE => NONE
   4.136 +    val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
   4.137      val qty_full_name = (fst o dest_Type) qtyp  
   4.138      fun quot_info phi = Lifting_Info.transform_quotients phi quotients
   4.139 -    val lthy = case maybe_reflp_thm of
   4.140 +    val lthy = case opt_reflp_thm of
   4.141        SOME reflp_thm => lthy
   4.142          |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
   4.143                [reflp_thm])
   4.144 @@ -156,51 +221,247 @@
   4.145          (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
   4.146    end
   4.147  
   4.148 +local 
   4.149 +  val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
   4.150 +in
   4.151 +  fun parametrize_class_constraint ctxt pcr_def constraint =
   4.152 +    let
   4.153 +      fun generate_transfer_rule pcr_def constraint goal ctxt =
   4.154 +        let
   4.155 +          val thy = Proof_Context.theory_of ctxt
   4.156 +          val orig_ctxt = ctxt
   4.157 +          val (fixed_goal, ctxt) = yield_singleton (Variable.import_terms true) goal ctxt
   4.158 +          val init_goal = Goal.init (cterm_of thy fixed_goal)
   4.159 +          val rules = Transfer.get_transfer_raw ctxt
   4.160 +          val rules = constraint :: OO_rules @ rules
   4.161 +          val tac = K (Local_Defs.unfold_tac ctxt [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac rules)
   4.162 +        in
   4.163 +          (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
   4.164 +        end
   4.165 +      
   4.166 +      fun make_goal pcr_def constr =
   4.167 +        let 
   4.168 +          val pred_name = (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o prop_of) constr
   4.169 +          val arg = (fst o Logic.dest_equals o prop_of) pcr_def
   4.170 +        in
   4.171 +          HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
   4.172 +        end
   4.173 +      
   4.174 +      val check_assms =
   4.175 +        let 
   4.176 +          val right_names = ["bi_total", "bi_unique", "right_total", "right_unique"]
   4.177 +      
   4.178 +          fun is_right_name name = member op= right_names (Long_Name.base_name name)
   4.179 +      
   4.180 +          fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name
   4.181 +            | is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name
   4.182 +            | is_trivial_assm _ = false
   4.183 +        in
   4.184 +          fn thm => 
   4.185 +            let
   4.186 +              val prems = map HOLogic.dest_Trueprop (prems_of thm)
   4.187 +              val thm_name = (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o concl_of) thm
   4.188 +              val non_trivial_assms = filter_out is_trivial_assm prems
   4.189 +            in
   4.190 +              if null non_trivial_assms then ()
   4.191 +              else
   4.192 +                let
   4.193 +                  val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
   4.194 +                    Pretty.str thm_name,
   4.195 +                    Pretty.str " transfer rule found:",
   4.196 +                    Pretty.brk 1] @ 
   4.197 +                    ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
   4.198 +                                       [Pretty.str "."])
   4.199 +                in
   4.200 +                  warning (Pretty.str_of pretty_msg)
   4.201 +                end
   4.202 +            end
   4.203 +        end
   4.204 +  
   4.205 +      val goal = make_goal pcr_def constraint
   4.206 +      val thm = generate_transfer_rule pcr_def constraint goal ctxt
   4.207 +      val _ = check_assms thm
   4.208 +    in
   4.209 +      thm
   4.210 +    end
   4.211 +end
   4.212 +
   4.213 +local
   4.214 +  val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def}))
   4.215 +in
   4.216 +  fun generate_parametric_id lthy rty id_transfer_rule =
   4.217 +    let
   4.218 +      val orig_lthy = lthy
   4.219 +      (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
   4.220 +      val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
   4.221 +      val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
   4.222 +      val lthy = orig_lthy
   4.223 +      val id_transfer = 
   4.224 +         @{thm id_transfer}
   4.225 +        |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
   4.226 +        |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
   4.227 +      val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
   4.228 +      val thy = Proof_Context.theory_of lthy;
   4.229 +      val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
   4.230 +      val id_par_thm = Drule.cterm_instantiate inst id_transfer;
   4.231 +    in
   4.232 +      Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
   4.233 +    end
   4.234 +    handle Lifting_Term.MERGE_TRANSFER_REL msg => 
   4.235 +      let
   4.236 +        val error_msg = cat_lines 
   4.237 +          ["Generation of a parametric transfer rule for the abs. or the rep. function failed.",
   4.238 +          "A non-parametric version will be used.",
   4.239 +          (Pretty.string_of (Pretty.block
   4.240 +             [Pretty.str "Reason:", Pretty.brk 2, msg]))]
   4.241 +      in
   4.242 +        (warning error_msg; id_transfer_rule)
   4.243 +      end
   4.244 +end
   4.245 +
   4.246 +fun parametrize_quantifier lthy quant_transfer_rule =
   4.247 +  Lifting_Term.parametrize_transfer_rule lthy quant_transfer_rule
   4.248 +
   4.249 +fun get_pcrel_info ctxt qty_full_name =  
   4.250 +  #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
   4.251 +
   4.252  (*
   4.253    Sets up the Lifting package by a quotient theorem.
   4.254  
   4.255    gen_code - flag if an abstract type given by quot_thm should be registred 
   4.256      as an abstract type in the code generator
   4.257    quot_thm - a quotient theorem (Quotient R Abs Rep T)
   4.258 -  maybe_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
   4.259 +  opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
   4.260      (in the form "reflp R")
   4.261  *)
   4.262  
   4.263 -fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
   4.264 +fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
   4.265    let
   4.266 +    (**)
   4.267 +    val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
   4.268 +    (**)
   4.269      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   4.270 -    val (_, qty) = quot_thm_rty_qty quot_thm
   4.271 +    val (rty, qty) = quot_thm_rty_qty quot_thm
   4.272      val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
   4.273 -    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
   4.274 +    val qty_full_name = (fst o dest_Type) qty
   4.275 +    val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
   4.276      fun qualify suffix = Binding.qualified true suffix qty_name
   4.277 -    val lthy = case maybe_reflp_thm of
   4.278 -      SOME reflp_thm => lthy
   4.279 -        |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
   4.280 -          [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
   4.281 -        |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
   4.282 -          [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
   4.283 -        |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
   4.284 -          [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
   4.285 -        |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
   4.286 -          [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
   4.287 -      | NONE => lthy
   4.288 -        |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
   4.289 -          [quot_thm RS @{thm Quotient_All_transfer}])
   4.290 -        |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
   4.291 -          [quot_thm RS @{thm Quotient_Ex_transfer}])
   4.292 -        |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
   4.293 -          [quot_thm RS @{thm Quotient_forall_transfer}])
   4.294 -        |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
   4.295 -          [quot_thm RS @{thm Quotient_abs_induct}])
   4.296 +    val lthy = case opt_reflp_thm of
   4.297 +      SOME reflp_thm =>
   4.298 +        let 
   4.299 +          val thms =
   4.300 +            [("abs_induct",     @{thm Quotient_total_abs_induct}, [induct_attr]),
   4.301 +             ("abs_eq_iff",     @{thm Quotient_total_abs_eq_iff}, []           )]
   4.302 +        in
   4.303 +          lthy
   4.304 +            |> fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr), 
   4.305 +              [[quot_thm, reflp_thm] MRSL thm])) thms
   4.306 +        end
   4.307 +      | NONE =>
   4.308 +        let
   4.309 +          val thms = 
   4.310 +            [("abs_induct",     @{thm Quotient_abs_induct},       [induct_attr])]
   4.311 +        in
   4.312 +          fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr), 
   4.313 +            [quot_thm RS thm])) thms lthy
   4.314 +        end
   4.315 +
   4.316 +    fun setup_transfer_rules_nonpar lthy =
   4.317 +      let
   4.318 +        val lthy =
   4.319 +          case opt_reflp_thm of
   4.320 +            SOME reflp_thm =>
   4.321 +              let 
   4.322 +                val thms =
   4.323 +                  [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
   4.324 +                   ("bi_total",       @{thm Quotient_bi_total}       )]
   4.325 +              in
   4.326 +                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.327 +                    [[quot_thm, reflp_thm] MRSL thm])) thms lthy
   4.328 +              end
   4.329 +            | NONE =>
   4.330 +              let
   4.331 +                val thms = 
   4.332 +                  [("All_transfer",   @{thm Quotient_All_transfer}   ),
   4.333 +                   ("Ex_transfer",    @{thm Quotient_Ex_transfer}    ),
   4.334 +                   ("forall_transfer",@{thm Quotient_forall_transfer})]
   4.335 +              in
   4.336 +                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.337 +                  [quot_thm RS thm])) thms lthy
   4.338 +              end
   4.339 +        val thms = 
   4.340 +          [("rel_eq_transfer", @{thm Quotient_rel_eq_transfer}),
   4.341 +           ("right_unique",    @{thm Quotient_right_unique}   ), 
   4.342 +           ("right_total",     @{thm Quotient_right_total}    )]
   4.343 +      in
   4.344 +        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.345 +          [quot_thm RS thm])) thms lthy
   4.346 +      end
   4.347 +
   4.348 +    fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm =
   4.349 +      option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm
   4.350 +      handle Lifting_Term.MERGE_TRANSFER_REL msg => 
   4.351 +        let
   4.352 +          val error_msg = cat_lines 
   4.353 +            ["Generation of a parametric transfer rule for the quotient relation failed.",
   4.354 +            (Pretty.string_of (Pretty.block
   4.355 +               [Pretty.str "Reason:", Pretty.brk 2, msg]))]
   4.356 +        in
   4.357 +          error error_msg
   4.358 +        end
   4.359 +
   4.360 +    fun setup_transfer_rules_par lthy =
   4.361 +      let
   4.362 +        val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
   4.363 +        val lthy =
   4.364 +          case opt_reflp_thm of
   4.365 +            SOME reflp_thm =>
   4.366 +              let
   4.367 +                val id_abs_transfer = generate_parametric_id lthy rty
   4.368 +                  (Lifting_Term.parametrize_transfer_rule lthy
   4.369 +                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
   4.370 +                val bi_total = parametrize_class_constraint lthy pcrel_def 
   4.371 +                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
   4.372 +                val thms = 
   4.373 +                  [("id_abs_transfer",id_abs_transfer),
   4.374 +                   ("bi_total",       bi_total       )]
   4.375 +              in
   4.376 +                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.377 +                    [thm])) thms lthy
   4.378 +              end
   4.379 +            | NONE =>
   4.380 +              let
   4.381 +                val thms = 
   4.382 +                  [("All_transfer",   @{thm Quotient_All_transfer}   ),
   4.383 +                   ("Ex_transfer",    @{thm Quotient_Ex_transfer}    ),
   4.384 +                   ("forall_transfer",@{thm Quotient_forall_transfer})]
   4.385 +              in
   4.386 +                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.387 +                  [parametrize_quantifier lthy (quot_thm RS thm)])) thms lthy
   4.388 +              end
   4.389 +        val rel_eq_transfer = generate_parametric_rel_eq lthy 
   4.390 +          (Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
   4.391 +            opt_par_thm
   4.392 +        val right_unique = parametrize_class_constraint lthy pcrel_def 
   4.393 +            (quot_thm RS @{thm Quotient_right_unique})
   4.394 +        val right_total = parametrize_class_constraint lthy pcrel_def 
   4.395 +            (quot_thm RS @{thm Quotient_right_total})
   4.396 +        val thms = 
   4.397 +          [("rel_eq_transfer", rel_eq_transfer),
   4.398 +           ("right_unique",    right_unique   ), 
   4.399 +           ("right_total",     right_total    )]      
   4.400 +      in
   4.401 +        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.402 +          [thm])) thms lthy
   4.403 +      end
   4.404 +
   4.405 +    fun setup_transfer_rules lthy = 
   4.406 +      if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
   4.407 +                                                     else setup_transfer_rules_nonpar lthy
   4.408    in
   4.409      lthy
   4.410 -      |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
   4.411 -        [quot_thm RS @{thm Quotient_right_unique}])
   4.412 -      |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
   4.413 -        [quot_thm RS @{thm Quotient_right_total}])
   4.414 -      |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), 
   4.415 -        [quot_thm RS @{thm Quotient_rel_eq_transfer}])
   4.416 -      |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
   4.417 +      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
   4.418 +      |> setup_transfer_rules
   4.419    end
   4.420  
   4.421  (*
   4.422 @@ -215,8 +476,10 @@
   4.423    let
   4.424      val transfer_attr = Attrib.internal (K Transfer.transfer_add)
   4.425      val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
   4.426 -    val (T_def, lthy') = define_crel rep_fun lthy
   4.427 -
   4.428 +    val (T_def, lthy) = define_crel rep_fun lthy
   4.429 +    (**)
   4.430 +    val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
   4.431 +    (**)    
   4.432      val quot_thm = case typedef_set of
   4.433        Const ("Orderings.top_class.top", _) => 
   4.434          [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
   4.435 @@ -224,49 +487,109 @@
   4.436          [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
   4.437        | _ => 
   4.438          [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
   4.439 -
   4.440 -    val (_, qty) = quot_thm_rty_qty quot_thm
   4.441 -    val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
   4.442 +    val (rty, qty) = quot_thm_rty_qty quot_thm
   4.443 +    val qty_full_name = (fst o dest_Type) qty
   4.444 +    val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
   4.445      fun qualify suffix = Binding.qualified true suffix qty_name
   4.446      val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
   4.447 +    val opt_reflp_thm = 
   4.448 +      case typedef_set of
   4.449 +        Const ("Orderings.top_class.top", _) => 
   4.450 +          SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
   4.451 +        | _ =>  NONE
   4.452  
   4.453 -    val (maybe_reflp_thm, lthy'') = case typedef_set of
   4.454 -      Const ("Orderings.top_class.top", _) => 
   4.455 -        let
   4.456 -          val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
   4.457 -          val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
   4.458 -        in
   4.459 -          lthy'
   4.460 -            |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), 
   4.461 -              [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
   4.462 -            |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]), 
   4.463 -              [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
   4.464 -            |> pair (SOME reflp_thm)
   4.465 -        end
   4.466 -      | _ => lthy'
   4.467 -        |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]), 
   4.468 -          [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
   4.469 -        |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]), 
   4.470 -          [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
   4.471 -        |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
   4.472 -          [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
   4.473 -        |> pair NONE
   4.474 +    fun setup_transfer_rules_nonpar lthy =
   4.475 +      let
   4.476 +        val lthy =
   4.477 +          case opt_reflp_thm of
   4.478 +            SOME reflp_thm =>
   4.479 +              let 
   4.480 +                val thms =
   4.481 +                  [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
   4.482 +                   ("bi_total",       @{thm Quotient_bi_total}       )]
   4.483 +              in
   4.484 +                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.485 +                    [[quot_thm, reflp_thm] MRSL thm])) thms lthy
   4.486 +              end
   4.487 +            | NONE =>
   4.488 +              let
   4.489 +                val thms = 
   4.490 +                  [("All_transfer",   @{thm typedef_All_transfer}   ),
   4.491 +                   ("Ex_transfer",    @{thm typedef_Ex_transfer}    )]
   4.492 +              in
   4.493 +                lthy
   4.494 +                |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]), 
   4.495 +                  [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
   4.496 +                |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.497 +                  [[typedef_thm, T_def] MRSL thm])) thms
   4.498 +              end
   4.499 +        val thms = 
   4.500 +          [("rep_transfer", @{thm typedef_rep_transfer}),
   4.501 +           ("bi_unique",    @{thm typedef_bi_unique}   ),
   4.502 +           ("right_unique", @{thm typedef_right_unique}), 
   4.503 +           ("right_total",  @{thm typedef_right_total} )]
   4.504 +      in
   4.505 +        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.506 +          [[typedef_thm, T_def] MRSL thm])) thms lthy
   4.507 +      end
   4.508 +
   4.509 +    fun setup_transfer_rules_par lthy =
   4.510 +      let
   4.511 +        val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
   4.512 +        val lthy =
   4.513 +          case opt_reflp_thm of
   4.514 +            SOME reflp_thm =>
   4.515 +              let
   4.516 +                val id_abs_transfer = generate_parametric_id lthy rty
   4.517 +                  (Lifting_Term.parametrize_transfer_rule lthy
   4.518 +                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
   4.519 +                val bi_total = parametrize_class_constraint lthy pcrel_def 
   4.520 +                    ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
   4.521 +                val thms = 
   4.522 +                  [("id_abs_transfer",id_abs_transfer),
   4.523 +                   ("bi_total",       bi_total       )]
   4.524 +              in
   4.525 +                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.526 +                    [thm])) thms lthy
   4.527 +              end
   4.528 +            | NONE =>
   4.529 +              let
   4.530 +                val thms = 
   4.531 +                  ("forall_transfer", simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})) 
   4.532 +                  ::
   4.533 +                  (map_snd (fn thm => [typedef_thm, T_def] MRSL thm)                
   4.534 +                  [("All_transfer", @{thm typedef_All_transfer}),
   4.535 +                   ("Ex_transfer",  @{thm typedef_Ex_transfer} )])
   4.536 +              in
   4.537 +                fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.538 +                  [parametrize_quantifier lthy thm])) thms lthy
   4.539 +              end
   4.540 +        val thms = 
   4.541 +          ("rep_transfer", generate_parametric_id lthy rty 
   4.542 +            (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer})))
   4.543 +          ::
   4.544 +          (map_snd (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
   4.545 +          [("bi_unique",    @{thm typedef_bi_unique} ),
   4.546 +           ("right_unique", @{thm typedef_right_unique}), 
   4.547 +           ("right_total",  @{thm typedef_right_total} )])
   4.548 +      in
   4.549 +        fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), 
   4.550 +          [thm])) thms lthy
   4.551 +      end
   4.552 +
   4.553 +    fun setup_transfer_rules lthy = 
   4.554 +      if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
   4.555 +                                                     else setup_transfer_rules_nonpar lthy
   4.556 +
   4.557    in
   4.558 -    lthy''
   4.559 +    lthy
   4.560        |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), 
   4.561 -        [quot_thm])
   4.562 -      |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]), 
   4.563 -        [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
   4.564 -      |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]), 
   4.565 -        [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
   4.566 -      |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), 
   4.567 -        [[quot_thm] MRSL @{thm Quotient_right_unique}])
   4.568 -      |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), 
   4.569 -        [[quot_thm] MRSL @{thm Quotient_right_total}])
   4.570 -      |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
   4.571 +            [quot_thm])
   4.572 +      |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
   4.573 +      |> setup_transfer_rules
   4.574    end
   4.575  
   4.576 -fun setup_lifting_cmd gen_code xthm opt_reflp_xthm lthy =
   4.577 +fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy =
   4.578    let 
   4.579      val input_thm = singleton (Attrib.eval_thms lthy) xthm
   4.580      val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
   4.581 @@ -283,15 +606,14 @@
   4.582        end
   4.583  
   4.584      fun setup_quotient () = 
   4.585 -      case opt_reflp_xthm of
   4.586 -        SOME reflp_xthm => 
   4.587 -          let
   4.588 -            val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
   4.589 -            val _ = sanity_check_reflp_thm reflp_thm
   4.590 -          in
   4.591 -            setup_by_quotient gen_code input_thm (SOME reflp_thm) lthy
   4.592 -          end
   4.593 -        | NONE => setup_by_quotient gen_code input_thm NONE lthy
   4.594 +      let
   4.595 +        val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
   4.596 +        val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
   4.597 +        val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
   4.598 +      in
   4.599 +        setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
   4.600 +      end
   4.601 +      
   4.602  
   4.603      fun setup_typedef () = 
   4.604        case opt_reflp_xthm of
   4.605 @@ -310,6 +632,8 @@
   4.606  val _ = 
   4.607    Outer_Syntax.local_theory @{command_spec "setup_lifting"}
   4.608      "setup lifting infrastructure" 
   4.609 -      (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> 
   4.610 -        (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
   4.611 +      (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm 
   4.612 +      -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >> 
   4.613 +        (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) => 
   4.614 +          setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
   4.615  end;
     5.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Fri Mar 08 11:28:20 2013 +0100
     5.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Fri Mar 08 13:14:23 2013 +0100
     5.3 @@ -8,6 +8,7 @@
     5.4  sig
     5.5    exception QUOT_THM of typ * typ * Pretty.T
     5.6    exception PARAM_QUOT_THM of typ * Pretty.T
     5.7 +  exception MERGE_TRANSFER_REL of Pretty.T
     5.8    exception CHECK_RTY of typ * typ
     5.9  
    5.10    val prove_quot_thm: Proof.context -> typ * typ -> thm
    5.11 @@ -19,6 +20,10 @@
    5.12    val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context
    5.13  
    5.14    val generate_parametrized_relator: Proof.context -> typ -> term * term list
    5.15 +
    5.16 +  val merge_transfer_relations: Proof.context -> cterm -> thm
    5.17 +
    5.18 +  val parametrize_transfer_rule: Proof.context -> thm -> thm
    5.19  end
    5.20  
    5.21  structure Lifting_Term: LIFTING_TERM =
    5.22 @@ -30,6 +35,7 @@
    5.23  exception QUOT_THM_INTERNAL of Pretty.T
    5.24  exception QUOT_THM of typ * typ * Pretty.T
    5.25  exception PARAM_QUOT_THM of typ * Pretty.T
    5.26 +exception MERGE_TRANSFER_REL of Pretty.T
    5.27  exception CHECK_RTY of typ * typ
    5.28  
    5.29  fun match ctxt err ty_pat ty =
    5.30 @@ -53,16 +59,41 @@
    5.31         Pretty.str "don't match."])
    5.32    end
    5.33  
    5.34 +fun get_quot_data ctxt s =
    5.35 +  case Lifting_Info.lookup_quotients ctxt s of
    5.36 +    SOME qdata => qdata
    5.37 +  | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    5.38 +    [Pretty.str ("No quotient type " ^ quote s), 
    5.39 +     Pretty.brk 1, 
    5.40 +     Pretty.str "found."])
    5.41 +
    5.42  fun get_quot_thm ctxt s =
    5.43    let
    5.44      val thy = Proof_Context.theory_of ctxt
    5.45    in
    5.46 -    (case Lifting_Info.lookup_quotients ctxt s of
    5.47 -      SOME qdata => Thm.transfer thy (#quot_thm qdata)
    5.48 -    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    5.49 -      [Pretty.str ("No quotient type " ^ quote s), 
    5.50 -       Pretty.brk 1, 
    5.51 -       Pretty.str "found."]))
    5.52 +    Thm.transfer thy (#quot_thm (get_quot_data ctxt s))
    5.53 +  end
    5.54 +
    5.55 +fun get_pcrel_info ctxt s =
    5.56 +  case #pcrel_info (get_quot_data ctxt s) of
    5.57 +    SOME pcrel_info => pcrel_info
    5.58 +  | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    5.59 +    [Pretty.str ("No parametrized correspondce relation for " ^ quote s), 
    5.60 +     Pretty.brk 1, 
    5.61 +     Pretty.str "found."])
    5.62 +
    5.63 +fun get_pcrel_def ctxt s =
    5.64 +  let
    5.65 +    val thy = Proof_Context.theory_of ctxt
    5.66 +  in
    5.67 +    Thm.transfer thy (#pcrel_def (get_pcrel_info ctxt s))
    5.68 +  end
    5.69 +
    5.70 +fun get_pcr_cr_eq ctxt s =
    5.71 +  let
    5.72 +    val thy = Proof_Context.theory_of ctxt
    5.73 +  in
    5.74 +    Thm.transfer thy (#pcr_cr_eq (get_pcrel_info ctxt s))
    5.75    end
    5.76  
    5.77  fun get_rel_quot_thm ctxt s =
    5.78 @@ -77,6 +108,22 @@
    5.79         Pretty.str "found."]))
    5.80    end
    5.81  
    5.82 +fun get_rel_distr_rules ctxt s tm =
    5.83 +  let
    5.84 +    val thy = Proof_Context.theory_of ctxt
    5.85 +  in
    5.86 +    (case Lifting_Info.lookup_relator_distr_data ctxt s of
    5.87 +      SOME rel_distr_thm => (
    5.88 +        case tm of
    5.89 +          Const (@{const_name POS}, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm)
    5.90 +          | Const (@{const_name NEG}, _) => map (Thm.transfer thy) (#neg_distr_rules rel_distr_thm)
    5.91 +      )
    5.92 +    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    5.93 +      [Pretty.str ("No relator distr. data for the type " ^ quote s), 
    5.94 +       Pretty.brk 1,
    5.95 +       Pretty.str "found."]))
    5.96 +  end
    5.97 +
    5.98  fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
    5.99  
   5.100  fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
   5.101 @@ -145,6 +192,17 @@
   5.102            rel_quot_thm_prems
   5.103        end
   5.104  
   5.105 +fun instantiate_rtys ctxt  (Type (rty_name, _)) (qty as Type (qty_name, _)) =
   5.106 +  let
   5.107 +    val quot_thm = get_quot_thm ctxt qty_name
   5.108 +    val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
   5.109 +    val _ = check_raw_types (rty_name, rs) qty_name
   5.110 +    val qtyenv = match ctxt equiv_match_err qty_pat qty
   5.111 +  in
   5.112 +    map (Envir.subst_type qtyenv) rtys
   5.113 +  end
   5.114 +  | instantiate_rtys _ _ _ = error "instantiate_rtys: not Type"
   5.115 +
   5.116  fun prove_schematic_quot_thm ctxt (rty, qty) =
   5.117    (case (rty, qty) of
   5.118      (Type (s, tys), Type (s', tys')) =>
   5.119 @@ -161,18 +219,15 @@
   5.120          end
   5.121        else
   5.122          let
   5.123 -          val quot_thm = get_quot_thm ctxt s'
   5.124 -          val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
   5.125 -          val _ = check_raw_types (s, rs) s'
   5.126 -          val qtyenv = match ctxt equiv_match_err qty_pat qty
   5.127 -          val rtys' = map (Envir.subst_type qtyenv) rtys
   5.128 +          val rtys' = instantiate_rtys ctxt rty qty
   5.129            val args = map (prove_schematic_quot_thm ctxt) (tys ~~ rtys')
   5.130          in
   5.131            if forall is_id_quot args
   5.132            then
   5.133 -            quot_thm
   5.134 +            get_quot_thm ctxt s'
   5.135            else
   5.136              let
   5.137 +              val quot_thm = get_quot_thm ctxt s'
   5.138                val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
   5.139              in
   5.140                [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
   5.141 @@ -286,7 +341,7 @@
   5.142          in
   5.143            (args MRSL (get_rel_quot_thm ctxt s), table_ctxt)
   5.144          end 
   5.145 -      | generate (ty as (TFree _)) (table, ctxt) =
   5.146 +      | generate ty (table, ctxt) =
   5.147          if AList.defined (op=) table ty 
   5.148          then (the (AList.lookup (op=) table ty), (table, ctxt))
   5.149          else 
   5.150 @@ -298,7 +353,6 @@
   5.151            in
   5.152              (Q_thm, (table', ctxt'))
   5.153            end
   5.154 -      | generate _ _ = error "generate_param_quot_thm: TVar"
   5.155  
   5.156      val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt)
   5.157    in
   5.158 @@ -317,4 +371,156 @@
   5.159      (hd exported_terms, tl exported_terms)
   5.160    end
   5.161  
   5.162 +(* Parametrization *)
   5.163 +
   5.164 +local
   5.165 +  fun get_lhs rule = (Thm.dest_fun o Thm.dest_arg o strip_imp_concl o cprop_of) rule;
   5.166 +  
   5.167 +  fun no_imp _ = raise CTERM ("no implication", []);
   5.168 +  
   5.169 +  infix 0 else_imp
   5.170 +
   5.171 +  fun (cv1 else_imp cv2) ct =
   5.172 +    (cv1 ct
   5.173 +      handle THM _ => cv2 ct
   5.174 +        | CTERM _ => cv2 ct
   5.175 +        | TERM _ => cv2 ct
   5.176 +        | TYPE _ => cv2 ct);
   5.177 +  
   5.178 +  fun first_imp cvs = fold_rev (curry op else_imp) cvs no_imp
   5.179 +  
   5.180 +  fun rewr_imp rule ct = 
   5.181 +    let
   5.182 +      val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
   5.183 +      val lhs_rule = get_lhs rule1;
   5.184 +      val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1;
   5.185 +      val lhs_ct = Thm.dest_fun ct
   5.186 +    in
   5.187 +        Thm.instantiate (Thm.match (lhs_rule, lhs_ct)) rule2
   5.188 +          handle Pattern.MATCH => raise CTERM ("rewr_imp", [lhs_rule, lhs_ct])
   5.189 +   end
   5.190 +  
   5.191 +  fun rewrs_imp rules = first_imp (map rewr_imp rules)
   5.192 +
   5.193 +  fun map_interrupt f l =
   5.194 +    let
   5.195 +      fun map_interrupt' _ [] l = SOME (rev l)
   5.196 +       | map_interrupt' f (x::xs) l = (case f x of
   5.197 +        NONE => NONE
   5.198 +        | SOME v => map_interrupt' f xs (v::l))
   5.199 +    in
   5.200 +      map_interrupt' f l []
   5.201 +    end
   5.202 +in
   5.203 +  fun merge_transfer_relations ctxt ctm =
   5.204 +    let
   5.205 +      val ctm = Thm.dest_arg ctm
   5.206 +      val tm = term_of ctm
   5.207 +      val rel = (hd o get_args 2) tm
   5.208 +  
   5.209 +      fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
   5.210 +        | same_constants _ _  = false
   5.211 +      
   5.212 +      fun prove_extra_assms ctxt ctm distr_rule =
   5.213 +        let
   5.214 +          fun prove_assm assm = try (Goal.prove ctxt [] [] (term_of assm))
   5.215 +            (fn _ => SOLVED' (REPEAT_ALL_NEW (resolve_tac (Transfer.get_transfer_raw ctxt))) 1)
   5.216 +  
   5.217 +          fun is_POS_or_NEG ctm =
   5.218 +            case (head_of o term_of o Thm.dest_arg) ctm of
   5.219 +              Const (@{const_name POS}, _) => true
   5.220 +              | Const (@{const_name NEG}, _) => true
   5.221 +              | _ => false
   5.222 +  
   5.223 +          val inst_distr_rule = rewr_imp distr_rule ctm
   5.224 +          val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule)
   5.225 +          val proved_assms = map_interrupt prove_assm extra_assms
   5.226 +        in
   5.227 +          Option.map (curry op OF inst_distr_rule) proved_assms
   5.228 +        end
   5.229 +        handle CTERM _ => NONE
   5.230 +  
   5.231 +      fun cannot_merge_error_msg () = Pretty.block
   5.232 +         [Pretty.str "Rewriting (merging) of this term has failed:",
   5.233 +          Pretty.brk 1,
   5.234 +          Syntax.pretty_term ctxt rel]
   5.235 +  
   5.236 +    in
   5.237 +      case get_args 2 rel of
   5.238 +          [Const (@{const_name "HOL.eq"}, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
   5.239 +          | [_, Const (@{const_name "HOL.eq"}, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
   5.240 +          | [_, trans_rel] =>
   5.241 +            let
   5.242 +              val (rty', qty) = (relation_types o fastype_of) trans_rel
   5.243 +              val r = (fst o dest_Type) rty' 
   5.244 +              val q = (fst o dest_Type) qty
   5.245 +            in
   5.246 +              if r = q then
   5.247 +                let
   5.248 +                  val distr_rules = get_rel_distr_rules ctxt r (head_of tm)
   5.249 +                  val distr_rule = get_first (prove_extra_assms ctxt ctm) distr_rules
   5.250 +                in
   5.251 +                  case distr_rule of
   5.252 +                    NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
   5.253 +                    | SOME distr_rule =>  (map (merge_transfer_relations ctxt) (cprems_of distr_rule)) 
   5.254 +                      MRSL distr_rule
   5.255 +                end
   5.256 +              else
   5.257 +                let 
   5.258 +                  val pcrel_def = get_pcrel_def ctxt q
   5.259 +                  val pcrel_const = (head_of o fst o Logic.dest_equals o prop_of) pcrel_def
   5.260 +                in
   5.261 +                  if same_constants pcrel_const (head_of trans_rel) then
   5.262 +                    let
   5.263 +                      val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
   5.264 +                      val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
   5.265 +                      val result = (map (merge_transfer_relations ctxt) (cprems_of distr_rule)) MRSL distr_rule
   5.266 +                      val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
   5.267 +                    in  
   5.268 +                      Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv 
   5.269 +                        (Conv.arg_conv (Conv.arg_conv fold_pcr_rel)) fold_pcr_rel)) result
   5.270 +                    end
   5.271 +                  else
   5.272 +                    raise MERGE_TRANSFER_REL (Pretty.str "Non-parametric correspondence relation used.")
   5.273 +                end
   5.274 +            end
   5.275 +    end
   5.276 +    handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
   5.277 +end
   5.278 +
   5.279 +fun parametrize_transfer_rule ctxt thm =
   5.280 +  let
   5.281 +    fun parametrize_relation_conv ctm =
   5.282 +      let
   5.283 +        val (rty, qty) = (relation_types o fastype_of) (term_of ctm)
   5.284 +      in
   5.285 +        case (rty, qty) of
   5.286 +          (Type (r, rargs), Type (q, qargs)) =>
   5.287 +            if r = q then
   5.288 +              if forall op= (rargs ~~ qargs) then
   5.289 +                Conv.all_conv ctm
   5.290 +              else
   5.291 +                all_args_conv parametrize_relation_conv ctm
   5.292 +            else
   5.293 +              if forall op= (rargs ~~ (instantiate_rtys ctxt rty qty)) then
   5.294 +                let
   5.295 +                  val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq ctxt q)
   5.296 +                in
   5.297 +                  Conv.rewr_conv pcr_cr_eq ctm
   5.298 +                end
   5.299 +                handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm
   5.300 +              else
   5.301 +                (let 
   5.302 +                  val pcrel_def = Thm.symmetric (get_pcrel_def ctxt q)
   5.303 +                in
   5.304 +                  (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
   5.305 +                end
   5.306 +                handle QUOT_THM_INTERNAL _ => 
   5.307 +                  (Conv.arg1_conv (all_args_conv parametrize_relation_conv)) ctm)
   5.308 +          | _ => Conv.all_conv ctm
   5.309 +      end
   5.310 +    in
   5.311 +      Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
   5.312 +    end
   5.313 +
   5.314  end;
     6.1 --- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Mar 08 11:28:20 2013 +0100
     6.2 +++ b/src/HOL/Tools/Lifting/lifting_util.ML	Fri Mar 08 13:14:23 2013 +0100
     6.3 @@ -8,6 +8,7 @@
     6.4  sig
     6.5    val MRSL: thm list * thm -> thm
     6.6    val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
     6.7 +  val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list
     6.8    val dest_Quotient: term -> term * term * term * term
     6.9  
    6.10    val quot_thm_rel: thm -> term
    6.11 @@ -15,6 +16,19 @@
    6.12    val quot_thm_rep: thm -> term
    6.13    val quot_thm_crel: thm -> term
    6.14    val quot_thm_rty_qty: thm -> typ * typ
    6.15 +
    6.16 +  val undisch: thm -> thm
    6.17 +  val undisch_all: thm -> thm
    6.18 +  val is_fun_type: typ -> bool
    6.19 +  val get_args: int -> term -> term list
    6.20 +  val strip_args: int -> term -> term
    6.21 +  val all_args_conv: conv -> conv
    6.22 +  val is_Type: typ -> bool
    6.23 +  val is_fun_rel: term -> bool
    6.24 +  val relation_types: typ -> typ * typ
    6.25 +  val bottom_rewr_conv: thm list -> conv
    6.26 +  val mk_HOL_eq: thm -> thm
    6.27 +  val safe_HOL_meta_eq: thm -> thm
    6.28  end;
    6.29  
    6.30  
    6.31 @@ -28,6 +42,8 @@
    6.32  fun option_fold a _ NONE = a
    6.33    | option_fold _ f (SOME x) = f x
    6.34  
    6.35 +fun map_snd f xs = map (fn (a, b) => (a, f b)) xs
    6.36 +
    6.37  fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
    6.38        = (rel, abs, rep, cr)
    6.39    | dest_Quotient t = raise TERM ("dest_Quotient", [t])
    6.40 @@ -61,4 +77,40 @@
    6.41      (domain_type abs_type, range_type abs_type)
    6.42    end
    6.43  
    6.44 +fun undisch thm =
    6.45 +  let
    6.46 +    val assm = Thm.cprem_of thm 1
    6.47 +  in
    6.48 +    Thm.implies_elim thm (Thm.assume assm)
    6.49 +  end
    6.50 +
    6.51 +fun undisch_all thm = funpow (nprems_of thm) undisch thm
    6.52 +
    6.53 +fun is_fun_type (Type (@{type_name fun}, _)) = true
    6.54 +  | is_fun_type _ = false
    6.55 +
    6.56 +fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
    6.57 +
    6.58 +fun strip_args n = funpow n (fst o dest_comb)
    6.59 +
    6.60 +fun all_args_conv conv ctm = 
    6.61 +  (Conv.combination_conv (Conv.try_conv (all_args_conv conv)) conv) ctm
    6.62 +
    6.63 +fun is_Type (Type _) = true
    6.64 +  | is_Type _ = false
    6.65 +
    6.66 +fun is_fun_rel (Const (@{const_name "fun_rel"}, _) $ _ $ _) = true
    6.67 +  | is_fun_rel _ = false
    6.68 +
    6.69 +fun relation_types typ = 
    6.70 +  case strip_type typ of
    6.71 +    ([typ1, typ2], @{typ bool}) => (typ1, typ2)
    6.72 +    | _ => error "relation_types: not a relation"
    6.73 +
    6.74 +fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
    6.75 +
    6.76 +fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq}
    6.77 +
    6.78 +fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
    6.79 +
    6.80  end;
     7.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 08 11:28:20 2013 +0100
     7.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Mar 08 13:14:23 2013 +0100
     7.3 @@ -7,13 +7,13 @@
     7.4  signature QUOTIENT_TYPE =
     7.5  sig
     7.6    val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
     7.7 -    ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
     7.8 +    ((binding * binding) option * bool * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
     7.9  
    7.10    val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * 
    7.11 -    ((binding * binding) option * bool) -> Proof.context -> Proof.state
    7.12 +    ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
    7.13  
    7.14 -  val quotient_type_cmd: (((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
    7.15 -    (binding * binding) option -> Proof.context -> Proof.state
    7.16 +  val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
    7.17 +    (binding * binding) option) * (Facts.ref * Args.src list) option -> Proof.context -> Proof.state
    7.18  end;
    7.19  
    7.20  structure Quotient_Type: QUOTIENT_TYPE =
    7.21 @@ -110,7 +110,7 @@
    7.22      (def_thm, lthy'')
    7.23    end;
    7.24  
    7.25 -fun setup_lifting_package gen_code quot3_thm equiv_thm lthy =
    7.26 +fun setup_lifting_package gen_code quot3_thm equiv_thm opt_par_thm lthy =
    7.27    let
    7.28      val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
    7.29      val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
    7.30 @@ -128,11 +128,11 @@
    7.31        )
    7.32    in
    7.33      lthy'
    7.34 -      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm
    7.35 +      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm opt_par_thm
    7.36        |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
    7.37    end
    7.38  
    7.39 -fun init_quotient_infr gen_code quot_thm equiv_thm lthy =
    7.40 +fun init_quotient_infr gen_code quot_thm equiv_thm opt_par_thm lthy =
    7.41    let
    7.42      val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
    7.43      val (qtyp, rtyp) = (dest_funT o fastype_of) rep
    7.44 @@ -147,11 +147,11 @@
    7.45        |> Local_Theory.declaration {syntax = false, pervasive = true}
    7.46          (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
    7.47            #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
    7.48 -      |> setup_lifting_package gen_code quot_thm equiv_thm
    7.49 +      |> setup_lifting_package gen_code quot_thm equiv_thm opt_par_thm
    7.50    end
    7.51  
    7.52  (* main function for constructing a quotient type *)
    7.53 -fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy =
    7.54 +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), equiv_thm) lthy =
    7.55    let
    7.56      val part_equiv =
    7.57        if partial
    7.58 @@ -203,7 +203,7 @@
    7.59        quot_thm = quotient_thm}
    7.60  
    7.61      val lthy4 = lthy3
    7.62 -      |> init_quotient_infr gen_code quotient_thm equiv_thm
    7.63 +      |> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm
    7.64        |> (snd oo Local_Theory.note)
    7.65          ((equiv_thm_name,
    7.66            if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
    7.67 @@ -314,7 +314,7 @@
    7.68  
    7.69  fun quotient_type_cmd spec lthy =
    7.70    let
    7.71 -    fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
    7.72 +    fun parse_spec (((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
    7.73        let
    7.74          val rty = Syntax.read_typ lthy rty_str
    7.75          val tmp_lthy1 = Variable.declare_typ rty lthy
    7.76 @@ -323,8 +323,9 @@
    7.77            |> Type.constraint (rty --> rty --> @{typ bool})
    7.78            |> Syntax.check_term tmp_lthy1
    7.79          val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
    7.80 +        val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
    7.81        in
    7.82 -        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
    7.83 +        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), tmp_lthy2)
    7.84        end
    7.85  
    7.86      val (spec', _) = parse_spec spec lthy
    7.87 @@ -343,6 +344,7 @@
    7.88        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
    7.89          (@{keyword "/"} |-- (partial -- Parse.term))  --
    7.90          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
    7.91 +          -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)
    7.92  
    7.93  val _ =
    7.94    Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
     8.1 --- a/src/HOL/Tools/transfer.ML	Fri Mar 08 11:28:20 2013 +0100
     8.2 +++ b/src/HOL/Tools/transfer.ML	Fri Mar 08 13:14:23 2013 +0100
     8.3 @@ -9,6 +9,7 @@
     8.4    val prep_conv: conv
     8.5    val get_relator_eq: Proof.context -> thm list
     8.6    val get_sym_relator_eq: Proof.context -> thm list
     8.7 +  val get_transfer_raw: Proof.context -> thm list
     8.8    val transfer_add: attribute
     8.9    val transfer_del: attribute
    8.10    val transfer_rule_of_term: Proof.context -> term -> thm