src/HOL/Tools/Lifting/lifting_term.ML
 author kuncar Tue Nov 18 16:19:57 2014 +0100 (2014-11-18) changeset 60222 78fc1b798c61 parent 60217 40c63ffce97f child 60239 755e11e2e15d permissions -rw-r--r--
parametrize liting of terms by quotients
```     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 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 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
```