src/HOL/Tools/Lifting/lifting_term.ML
author wenzelm
Sun May 03 14:35:48 2015 +0200 (2015-05-03)
changeset 60239 755e11e2e15d
parent 60222 78fc1b798c61
child 60642 48dd1cefb4ae
permissions -rw-r--r--
make SML/NJ more happy;
     1 (*  Title:      HOL/Tools/Lifting/lifting_term.ML
     2     Author:     Ondrej Kuncar
     3 
     4 Proves Quotient theorem.
     5 *)
     6 
     7 signature LIFTING_TERM =
     8 sig
     9   exception QUOT_THM of typ * typ * Pretty.T
    10   exception PARAM_QUOT_THM of typ * Pretty.T
    11   exception MERGE_TRANSFER_REL of Pretty.T
    12   exception CHECK_RTY of typ * typ
    13 
    14   type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
    15   comp_lift: typ -> thm * 'a -> thm * 'a }
    16 
    17   type quotients = Lifting_Info.quotient Symtab.table
    18   
    19   val force_qty_type: Proof.context -> typ -> thm -> thm
    20 
    21   val prove_schematic_quot_thm: 'a fold_quot_thm -> quotients -> Proof.context -> 
    22     typ * typ -> 'a -> thm * 'a
    23 
    24   val instantiate_rtys: Proof.context -> typ * typ -> typ * typ
    25 
    26   val prove_quot_thm: Proof.context -> typ * typ -> thm
    27 
    28   val abs_fun: Proof.context -> typ * typ -> term
    29 
    30   val equiv_relation: Proof.context -> typ * typ -> term
    31 
    32   val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context
    33 
    34   val generate_parametrized_relator: Proof.context -> typ -> term * term list
    35 
    36   val merge_transfer_relations: Proof.context -> cterm -> thm
    37 
    38   val parametrize_transfer_rule: Proof.context -> thm -> thm
    39 end
    40 
    41 structure Lifting_Term: LIFTING_TERM =
    42 struct
    43 open Lifting_Util
    44 
    45 infix 0 MRSL
    46 
    47 exception QUOT_THM_INTERNAL of Pretty.T
    48 exception QUOT_THM of typ * typ * Pretty.T
    49 exception PARAM_QUOT_THM of typ * Pretty.T
    50 exception MERGE_TRANSFER_REL of Pretty.T
    51 exception CHECK_RTY of typ * typ
    52 
    53 type quotients = Lifting_Info.quotient Symtab.table
    54 
    55 fun match ctxt err ty_pat ty =
    56   let
    57     val thy = Proof_Context.theory_of ctxt
    58   in
    59     Sign.typ_match thy (ty_pat, ty) Vartab.empty
    60       handle Type.TYPE_MATCH => err ctxt ty_pat ty
    61   end
    62 
    63 fun equiv_match_err ctxt ty_pat ty =
    64   let
    65     val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
    66     val ty_str = Syntax.string_of_typ ctxt ty
    67   in
    68     raise QUOT_THM_INTERNAL (Pretty.block
    69       [Pretty.str ("The quotient type " ^ quote ty_str),
    70        Pretty.brk 1,
    71        Pretty.str ("and the quotient type pattern " ^ quote ty_pat_str),
    72        Pretty.brk 1,
    73        Pretty.str "don't match."])
    74   end
    75 
    76 fun get_quot_data (quotients: quotients) s =
    77   case Symtab.lookup quotients s of
    78     SOME qdata => qdata
    79   | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    80     [Pretty.str ("No quotient type " ^ quote s), 
    81      Pretty.brk 1, 
    82      Pretty.str "found."])
    83 
    84 fun get_quot_thm quotients ctxt s =
    85   let
    86     val thy = Proof_Context.theory_of ctxt
    87   in
    88     Thm.transfer thy (#quot_thm (get_quot_data quotients s))
    89   end
    90 
    91 fun has_pcrel_info quotients s = is_some (#pcr_info (get_quot_data quotients s))
    92 
    93 fun get_pcrel_info quotients s =
    94   case #pcr_info (get_quot_data quotients s) of
    95     SOME pcr_info => pcr_info
    96   | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    97     [Pretty.str ("No parametrized correspondce relation for " ^ quote s), 
    98      Pretty.brk 1, 
    99      Pretty.str "found."])
   100 
   101 fun get_pcrel_def quotients ctxt s =
   102   let
   103     val thy = Proof_Context.theory_of ctxt
   104   in
   105     Thm.transfer thy (#pcrel_def (get_pcrel_info quotients s))
   106   end
   107 
   108 fun get_pcr_cr_eq quotients ctxt s =
   109   let
   110     val thy = Proof_Context.theory_of ctxt
   111   in
   112     Thm.transfer thy (#pcr_cr_eq (get_pcrel_info quotients s))
   113   end
   114 
   115 fun get_rel_quot_thm ctxt s =
   116    let
   117     val thy = Proof_Context.theory_of ctxt
   118   in
   119     (case Lifting_Info.lookup_quot_maps ctxt s of
   120       SOME map_data => Thm.transfer thy (#rel_quot_thm map_data)
   121     | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
   122       [Pretty.str ("No relator for the type " ^ quote s), 
   123        Pretty.brk 1,
   124        Pretty.str "found."]))
   125   end
   126 
   127 fun get_rel_distr_rules ctxt s tm =
   128   let
   129     val thy = Proof_Context.theory_of ctxt
   130   in
   131     (case Lifting_Info.lookup_relator_distr_data ctxt s of
   132       SOME rel_distr_thm => (
   133         case tm of
   134           Const (@{const_name POS}, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm)
   135           | Const (@{const_name NEG}, _) => map (Thm.transfer thy) (#neg_distr_rules rel_distr_thm)
   136       )
   137     | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
   138       [Pretty.str ("No relator distr. data for the type " ^ quote s), 
   139        Pretty.brk 1,
   140        Pretty.str "found."]))
   141   end
   142 
   143 fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient})
   144 
   145 fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars =
   146   case try (get_rel_quot_thm ctxt) type_name of
   147     NONE => rty_Tvars ~~ qty_Tvars
   148     | SOME rel_quot_thm =>
   149       let 
   150         fun quot_term_absT quot_term = 
   151           let 
   152             val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term
   153           in
   154             fastype_of abs
   155           end
   156 
   157         fun equiv_univ_err ctxt ty_pat ty =
   158           let
   159             val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
   160             val ty_str = Syntax.string_of_typ ctxt ty
   161           in
   162             raise QUOT_THM_INTERNAL (Pretty.block
   163               [Pretty.str ("The type " ^ quote ty_str),
   164                Pretty.brk 1,
   165                Pretty.str ("and the relator type pattern " ^ quote ty_pat_str),
   166                Pretty.brk 1,
   167                Pretty.str "don't unify."])
   168           end
   169 
   170         fun raw_match (TVar (v, S), T) subs =
   171               (case Vartab.defined subs v of
   172                 false => Vartab.update_new (v, (S, T)) subs
   173               | true => subs)
   174           | raw_match (Type (_, Ts), Type (_, Us)) subs =
   175               raw_matches (Ts, Us) subs
   176           | raw_match _ subs = subs
   177         and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs)
   178           | raw_matches _ subs = subs
   179 
   180         val rty = Type (type_name, rty_Tvars)
   181         val qty = Type (type_name, qty_Tvars)
   182         val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm
   183         val schematic_rel_absT = quot_term_absT rel_quot_thm_concl;
   184         val thy = Proof_Context.theory_of ctxt
   185         val absT = rty --> qty
   186         val schematic_absT = 
   187           absT 
   188           |> Logic.type_map (singleton (Variable.polymorphic ctxt))
   189           |> Logic.incr_tvar (maxidx_of_typ schematic_rel_absT + 1) 
   190             (* because absT can already contain schematic variables from rty patterns *)
   191         val maxidx = Term.maxidx_of_typs [schematic_rel_absT, schematic_absT]
   192         val _ = Sign.typ_unify thy (schematic_rel_absT, schematic_absT) (Vartab.empty,maxidx)
   193           handle Type.TUNIFY => equiv_univ_err ctxt schematic_rel_absT schematic_absT
   194         val subs = raw_match (schematic_rel_absT, absT) Vartab.empty
   195         val rel_quot_thm_prems = (Logic.strip_imp_prems o Thm.prop_of) rel_quot_thm
   196       in
   197         map (dest_funT o 
   198              Envir.subst_type subs o
   199              quot_term_absT) 
   200           rel_quot_thm_prems
   201       end
   202 
   203 fun gen_rty_is_TVar quotients ctxt qty = qty |> Tname |> get_quot_thm quotients ctxt |> 
   204   quot_thm_rty_qty |> fst |> is_TVar
   205 
   206 fun gen_instantiate_rtys quotients ctxt (rty, (qty as Type (qty_name, _))) =
   207   let
   208     val quot_thm = get_quot_thm quotients ctxt qty_name
   209     val (rty_pat, qty_pat) = quot_thm_rty_qty quot_thm
   210 
   211     fun inst_rty (Type (s, tys), Type (s', tys')) = 
   212         if s = s' then Type (s', map inst_rty (tys ~~ tys'))
   213         else raise QUOT_THM_INTERNAL (Pretty.block 
   214           [Pretty.str "The type",
   215            Pretty.brk 1,
   216            Syntax.pretty_typ ctxt rty,
   217            Pretty.brk 1,
   218            Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"),
   219            Pretty.brk 1,
   220            Pretty.str "the correct raw type must be an instance of",
   221            Pretty.brk 1,
   222            Syntax.pretty_typ ctxt rty_pat])
   223       | inst_rty (t as Type (_, _), TFree _) = t
   224       | inst_rty ((TVar _), rty) = rty
   225       | inst_rty ((TFree _), rty) = rty
   226       | inst_rty (_, _) = error "check_raw_types: we should not be here"
   227 
   228     val qtyenv = match ctxt equiv_match_err qty_pat qty
   229   in
   230     (inst_rty (rty_pat, rty), Envir.subst_type qtyenv rty_pat)
   231   end
   232   | gen_instantiate_rtys _ _ _ = error "gen_instantiate_rtys: not Type"
   233 
   234 fun instantiate_rtys ctxt (rty, qty) = 
   235   gen_instantiate_rtys (Lifting_Info.get_quotients ctxt) ctxt (rty, qty)
   236 
   237 type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
   238   comp_lift: typ -> thm * 'a -> thm * 'a }
   239 
   240 fun prove_schematic_quot_thm (actions: 'a fold_quot_thm) quotients ctxt (rty, qty) fold_val =
   241   let
   242     fun lifting_step (rty, qty) =
   243       let
   244         val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty)
   245         val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) 
   246           else (Targs rty', Targs rtyq) 
   247         val (args, fold_val) = 
   248           fold_map (prove_schematic_quot_thm actions quotients ctxt) (rty's ~~ rtyqs) fold_val
   249       in
   250         if forall is_id_quot args
   251         then
   252           let
   253             val quot_thm = get_quot_thm quotients ctxt (Tname qty)
   254           in
   255             #lift actions qty (quot_thm, fold_val)
   256           end
   257         else
   258           let
   259             val quot_thm = get_quot_thm quotients ctxt (Tname qty)
   260             val rel_quot_thm = if gen_rty_is_TVar quotients ctxt qty then the_single args else
   261               args MRSL (get_rel_quot_thm ctxt (Tname rty))
   262             val comp_quot_thm = [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
   263           in
   264             #comp_lift actions qty (comp_quot_thm, fold_val)
   265          end
   266       end
   267   in
   268     (case (rty, qty) of
   269       (Type (s, tys), Type (s', tys')) =>
   270         if s = s'
   271         then
   272           let
   273             val (args, fold_val) = 
   274               fold_map (prove_schematic_quot_thm actions quotients ctxt) 
   275                 (zip_Tvars ctxt s tys tys') fold_val
   276           in
   277             if forall is_id_quot args
   278             then
   279               (@{thm identity_quotient}, fold_val)
   280             else
   281               let
   282                 val quot_thm = args MRSL (get_rel_quot_thm ctxt s)
   283               in
   284                 #constr actions qty (quot_thm, fold_val)
   285               end
   286           end
   287         else
   288           lifting_step (rty, qty)
   289       | (_, Type (s', tys')) => 
   290         (case try (get_quot_thm quotients ctxt) s' of
   291           SOME quot_thm => 
   292             let
   293               val rty_pat = (fst o quot_thm_rty_qty) quot_thm
   294             in
   295               lifting_step (rty_pat, qty)              
   296             end
   297           | NONE =>
   298             let                                               
   299               val rty_pat = Type (s', map (fn _ => TFree ("a",[])) tys')
   300             in
   301               prove_schematic_quot_thm actions quotients ctxt (rty_pat, qty) fold_val
   302             end)
   303       | _ => (@{thm identity_quotient}, fold_val)
   304       )
   305   end
   306   handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg)
   307 
   308 fun force_qty_type ctxt qty quot_thm =
   309   let
   310     val thy = Proof_Context.theory_of ctxt
   311     val (_, qty_schematic) = quot_thm_rty_qty quot_thm
   312     val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
   313     fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty)
   314     val ty_inst = Vartab.fold (cons o prep_ty) match_env []
   315   in
   316     Thm.instantiate (ty_inst, []) quot_thm
   317   end
   318 
   319 fun check_rty_type ctxt rty quot_thm =
   320   let  
   321     val thy = Proof_Context.theory_of ctxt
   322     val (rty_forced, _) = quot_thm_rty_qty quot_thm
   323     val rty_schematic = Logic.type_map (singleton (Variable.polymorphic ctxt)) rty
   324     val _ = Sign.typ_match thy (rty_schematic, rty_forced) Vartab.empty
   325       handle Type.TYPE_MATCH => raise CHECK_RTY (rty_schematic, rty_forced)
   326   in
   327     ()
   328   end
   329 
   330 (*
   331   The function tries to prove that rty and qty form a quotient.
   332 
   333   Returns: Quotient theorem; an abstract type of the theorem is exactly
   334     qty, a representation type of the theorem is an instance of rty in general.
   335 *)
   336 
   337 
   338 local
   339   val id_actions = { constr = K I, lift = K I, comp_lift = K I }
   340 in
   341   fun prove_quot_thm ctxt (rty, qty) =
   342     let
   343       val quotients = Lifting_Info.get_quotients ctxt
   344       val (schematic_quot_thm, _) = prove_schematic_quot_thm id_actions quotients ctxt (rty, qty) ()
   345       val quot_thm = force_qty_type ctxt qty schematic_quot_thm
   346       val _ = check_rty_type ctxt rty quot_thm
   347     in
   348       quot_thm
   349     end
   350 end
   351 
   352 (*
   353   Computes the composed abstraction function for rty and qty.
   354 *)
   355 
   356 fun abs_fun ctxt (rty, qty) =
   357   quot_thm_abs (prove_quot_thm ctxt (rty, qty))
   358 
   359 (*
   360   Computes the composed equivalence relation for rty and qty.
   361 *)
   362 
   363 fun equiv_relation ctxt (rty, qty) =
   364   quot_thm_rel (prove_quot_thm ctxt (rty, qty))
   365 
   366 val get_fresh_Q_t =
   367   let
   368     val Q_t = @{term "Trueprop (Quotient R Abs Rep T)"}
   369     val frees_Q_t = Term.add_free_names Q_t []
   370     val tfrees_Q_t = rev (Term.add_tfree_names Q_t [])
   371   in
   372     fn ctxt =>
   373     let
   374       fun rename_free_var tab (Free (name, typ)) = Free (the_default name (AList.lookup op= tab name),typ)
   375         | rename_free_var _ t = t
   376       
   377       fun rename_free_vars tab = map_aterms (rename_free_var tab)
   378       
   379       fun rename_free_tvars tab =
   380         map_types (map_type_tfree (fn (name, sort) => TFree (the_default name (AList.lookup op= tab name), sort)))
   381       
   382       val (new_frees_Q_t, ctxt) = Variable.variant_fixes frees_Q_t ctxt
   383       val tab_frees = frees_Q_t ~~ new_frees_Q_t
   384       
   385       val (new_tfrees_Q_t, ctxt) = Variable.invent_types (replicate (length tfrees_Q_t) []) ctxt
   386       val tab_tfrees = tfrees_Q_t ~~ (fst o split_list) new_tfrees_Q_t
   387 
   388       val renamed_Q_t = rename_free_vars tab_frees Q_t
   389       val renamed_Q_t = rename_free_tvars tab_tfrees renamed_Q_t
   390     in
   391       (renamed_Q_t, ctxt)
   392     end
   393   end
   394 
   395 (*
   396   For the given type, it proves a composed Quotient map theorem, where for each type variable
   397   extra Quotient assumption is generated. E.g., for 'a list it generates exactly
   398   the Quotient map theorem for the list type. The function generalizes this for the whole
   399   type universe. New fresh variables in the assumptions are fixed in the returned context.
   400 
   401   Returns: the composed Quotient map theorem and list mapping each type variable in ty
   402   to the corresponding assumption in the returned theorem.
   403 *)
   404 
   405 fun prove_param_quot_thm ctxt ty = 
   406   let 
   407     fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) =
   408       if null tys 
   409       then 
   410         let 
   411           val instantiated_id_quot_thm =
   412             instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient}
   413         in
   414           (instantiated_id_quot_thm, (table, ctxt)) 
   415         end
   416       else
   417         let
   418           val (args, table_ctxt) = fold_map generate tys table_ctxt
   419         in
   420           (args MRSL (get_rel_quot_thm ctxt s), table_ctxt)
   421         end 
   422       | generate ty (table, ctxt) =
   423         if AList.defined (op=) table ty 
   424         then (the (AList.lookup (op=) table ty), (table, ctxt))
   425         else 
   426           let
   427             val (Q_t, ctxt') = get_fresh_Q_t ctxt
   428             val Q_thm = Thm.assume (Thm.cterm_of ctxt' Q_t)
   429             val table' = (ty, Q_thm) :: table
   430           in
   431             (Q_thm, (table', ctxt'))
   432           end
   433 
   434     val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt)
   435   in
   436     (param_quot_thm, rev table, ctxt)
   437   end
   438   handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg)
   439 
   440 (*
   441   It computes a parametrized relator for the given type ty. E.g., for 'a dlist:
   442   list_all2 ?R OO cr_dlist with parameters [?R].
   443   
   444   Returns: the definitional term and list of parameters (relations).
   445 *)
   446 
   447 fun generate_parametrized_relator ctxt ty =
   448   let
   449     val orig_ctxt = ctxt
   450     val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty
   451     val parametrized_relator = quot_thm_crel quot_thm
   452     val args = map (fn (_, q_thm) => quot_thm_crel q_thm) table
   453     val exported_terms = Variable.exportT_terms ctxt orig_ctxt (parametrized_relator :: args)
   454   in
   455     (hd exported_terms, tl exported_terms)
   456   end
   457 
   458 (* Parametrization *)
   459 
   460 local
   461   fun get_lhs rule = (Thm.dest_fun o Thm.dest_arg o strip_imp_concl o Thm.cprop_of) rule;
   462   
   463   fun no_imp _ = raise CTERM ("no implication", []);
   464   
   465   infix 0 else_imp
   466 
   467   fun (cv1 else_imp cv2) ct =
   468     (cv1 ct
   469       handle THM _ => cv2 ct
   470         | CTERM _ => cv2 ct
   471         | TERM _ => cv2 ct
   472         | TYPE _ => cv2 ct);
   473   
   474   fun first_imp cvs = fold_rev (curry op else_imp) cvs no_imp
   475   
   476   fun rewr_imp rule ct = 
   477     let
   478       val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
   479       val lhs_rule = get_lhs rule1;
   480       val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1;
   481       val lhs_ct = Thm.dest_fun ct
   482     in
   483         Thm.instantiate (Thm.match (lhs_rule, lhs_ct)) rule2
   484           handle Pattern.MATCH => raise CTERM ("rewr_imp", [lhs_rule, lhs_ct])
   485    end
   486   
   487   fun rewrs_imp rules = first_imp (map rewr_imp rules)
   488 in
   489 
   490   fun gen_merge_transfer_relations quotients ctxt ctm =
   491     let
   492       val ctm = Thm.dest_arg ctm
   493       val tm = Thm.term_of ctm
   494       val rel = (hd o get_args 2) tm
   495   
   496       fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
   497         | same_constants _ _  = false
   498       
   499       fun prove_extra_assms ctxt ctm distr_rule =
   500         let
   501           fun prove_assm assm = try (Goal.prove ctxt [] [] (Thm.term_of assm))
   502             (fn _ => SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (Transfer.get_transfer_raw ctxt))) 1)
   503   
   504           fun is_POS_or_NEG ctm =
   505             case (head_of o Thm.term_of o Thm.dest_arg) ctm of
   506               Const (@{const_name POS}, _) => true
   507               | Const (@{const_name NEG}, _) => true
   508               | _ => false
   509   
   510           val inst_distr_rule = rewr_imp distr_rule ctm
   511           val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule)
   512           val proved_assms = map_interrupt prove_assm extra_assms
   513         in
   514           Option.map (curry op OF inst_distr_rule) proved_assms
   515         end
   516         handle CTERM _ => NONE
   517   
   518       fun cannot_merge_error_msg () = Pretty.block
   519          [Pretty.str "Rewriting (merging) of this term has failed:",
   520           Pretty.brk 1,
   521           Syntax.pretty_term ctxt rel]
   522   
   523     in
   524       case get_args 2 rel of
   525           [Const (@{const_name "HOL.eq"}, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
   526           | [_, Const (@{const_name "HOL.eq"}, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
   527           | [_, trans_rel] =>
   528             let
   529               val (rty', qty) = (relation_types o fastype_of) trans_rel
   530             in
   531               if same_type_constrs (rty', qty) then
   532                 let
   533                   val distr_rules = get_rel_distr_rules ctxt ((fst o dest_Type) rty') (head_of tm)
   534                   val distr_rule = get_first (prove_extra_assms ctxt ctm) distr_rules
   535                 in
   536                   case distr_rule of
   537                     NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
   538                     | SOME distr_rule =>  (map (gen_merge_transfer_relations quotients ctxt) 
   539                                             (cprems_of distr_rule)) 
   540                       MRSL distr_rule
   541                 end
   542               else
   543                 let 
   544                   val pcrel_def = get_pcrel_def quotients ctxt ((fst o dest_Type) qty)
   545                   val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def
   546                 in
   547                   if same_constants pcrel_const (head_of trans_rel) then
   548                     let
   549                       val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
   550                       val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
   551                       val result = (map (gen_merge_transfer_relations quotients ctxt) 
   552                         (cprems_of distr_rule)) MRSL distr_rule
   553                       val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
   554                     in  
   555                       Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv 
   556                         (Conv.arg_conv (Conv.arg_conv fold_pcr_rel)) fold_pcr_rel)) result
   557                     end
   558                   else
   559                     raise MERGE_TRANSFER_REL (Pretty.str "Non-parametric correspondence relation used.")
   560                 end
   561             end
   562     end
   563     handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
   564 
   565   (*
   566     ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer 
   567     relation for t and T is a transfer relation between t and f, which consists only from
   568     parametrized transfer relations (i.e., pcr_?) and equalities op=. POS or NEG encodes
   569     co-variance or contra-variance.
   570     
   571     The function merges par_R OO T using definitions of parametrized correspondence relations
   572     (e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T).
   573   *)
   574 
   575   fun merge_transfer_relations ctxt ctm = gen_merge_transfer_relations 
   576     (Lifting_Info.get_quotients ctxt) ctxt ctm
   577 end
   578 
   579 fun gen_parametrize_transfer_rule quotients ctxt thm =
   580   let
   581     fun parametrize_relation_conv ctm =
   582       let
   583         val (rty, qty) = (relation_types o fastype_of) (Thm.term_of ctm)
   584       in
   585         if same_type_constrs (rty, qty) then
   586           if forall op= (Targs rty ~~ Targs qty) then
   587             Conv.all_conv ctm
   588           else
   589             all_args_conv parametrize_relation_conv ctm
   590         else
   591           if is_Type qty then
   592             let
   593               val q = (fst o dest_Type) qty
   594             in
   595               let
   596                 val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty)
   597                 val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) 
   598                   else (Targs rty', Targs rtyq)
   599               in
   600                 if forall op= (rty's ~~ rtyqs) then
   601                   let
   602                     val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq quotients ctxt q)
   603                   in      
   604                     Conv.rewr_conv pcr_cr_eq ctm
   605                   end
   606                   handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm
   607                 else
   608                   if has_pcrel_info quotients q then
   609                     let 
   610                       val pcrel_def = Thm.symmetric (get_pcrel_def quotients ctxt q)
   611                     in
   612                       (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
   613                     end
   614                   else Conv.arg1_conv (all_args_conv parametrize_relation_conv) ctm
   615               end  
   616             end
   617           else Conv.all_conv ctm
   618       end
   619     in
   620       Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
   621     end
   622 
   623 (*
   624   It replaces cr_T by pcr_T op= in the transfer relation. For composed
   625   abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
   626   correspondce relation does not exist, the original relation is kept.
   627 
   628   thm - a transfer rule
   629 *)
   630 
   631 fun parametrize_transfer_rule ctxt thm = 
   632   gen_parametrize_transfer_rule (Lifting_Info.get_quotients ctxt) ctxt thm
   633 
   634 end