src/HOL/Tools/Lifting/lifting_setup.ML
author wenzelm
Sun May 03 14:35:48 2015 +0200 (2015-05-03)
changeset 60239 755e11e2e15d
parent 60231 0daab758e087
child 60784 4f590c08fd5d
permissions -rw-r--r--
make SML/NJ more happy;
     1 (*  Title:      HOL/Tools/Lifting/lifting_setup.ML
     2     Author:     Ondrej Kuncar
     3 
     4 Setting up the lifting infrastructure.
     5 *)
     6 
     7 signature LIFTING_SETUP =
     8 sig
     9   exception SETUP_LIFTING_INFR of string
    10 
    11   type config = { notes: bool };
    12   val default_config: config;
    13 
    14   val setup_by_quotient: config -> thm -> thm option -> thm option -> local_theory -> 
    15     binding * local_theory
    16 
    17   val setup_by_typedef_thm: config -> thm -> local_theory -> binding * local_theory
    18 
    19   val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic
    20 
    21   val lifting_forget: string -> local_theory -> local_theory
    22   val update_transfer_rules: string -> local_theory -> local_theory
    23   val pointer_of_bundle_binding: Proof.context -> binding -> string
    24 end
    25 
    26 structure Lifting_Setup: LIFTING_SETUP =
    27 struct
    28 
    29 open Lifting_Util
    30 
    31 infix 0 MRSL
    32 
    33 exception SETUP_LIFTING_INFR of string
    34 
    35 (* Config *)
    36 
    37 type config = { notes: bool };
    38 val default_config = { notes = true };
    39 
    40 fun define_crel (config: config) rep_fun lthy =
    41   let
    42     val (qty, rty) = (dest_funT o fastype_of) rep_fun
    43     val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
    44     val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph))
    45     val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
    46     val crel_name = Binding.prefix_name "cr_" qty_name
    47     val (fixed_def_term, lthy) = yield_singleton (Variable.importT_terms) def_term lthy
    48     val ((_, (_ , def_thm)), lthy) = if #notes config then
    49         Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy
    50       else 
    51         Local_Theory.define ((Binding.concealed crel_name, NoSyn), ((Binding.empty, []), fixed_def_term)) lthy
    52   in  
    53     (def_thm, lthy)
    54   end
    55 
    56 fun print_define_pcrel_warning msg = 
    57   let
    58     val warning_msg = cat_lines 
    59       ["Generation of a parametrized correspondence relation failed.",
    60       (Pretty.string_of (Pretty.block
    61          [Pretty.str "Reason:", Pretty.brk 2, msg]))]
    62   in
    63     warning warning_msg
    64   end
    65 
    66 fun define_pcrel (config: config) crel lthy =
    67   let
    68     val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
    69     val [rty', qty] = (binder_types o fastype_of) fixed_crel
    70     val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty'
    71     val rty_raw = (domain_type o range_type o fastype_of) param_rel
    72     val thy = Proof_Context.theory_of lthy
    73     val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty
    74     val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel
    75     val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args
    76     val lthy = Variable.declare_names fixed_crel lthy
    77     val (instT, lthy) = Variable.importT_inst (param_rel_subst :: args_subst) lthy
    78     val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
    79     val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
    80     val rty = (domain_type o fastype_of) param_rel_fixed
    81     val relcomp_op = Const (@{const_name "relcompp"}, 
    82           (rty --> rty' --> HOLogic.boolT) --> 
    83           (rty' --> qty --> HOLogic.boolT) --> 
    84           rty --> qty --> HOLogic.boolT)
    85     val qty_name = (fst o dest_Type) qty
    86     val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
    87     val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
    88     val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
    89     val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
    90     val definition_term = Logic.mk_equals (lhs, rhs)
    91     fun note_def lthy =
    92       Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), 
    93         ((Binding.empty, []), definition_term)) lthy |>> (snd #> snd);
    94     fun raw_def lthy =
    95       let
    96         val ((_, rhs), prove) = Local_Defs.derived_def lthy true definition_term;
    97         val ((_, (_, raw_th)), lthy) = lthy
    98           |> Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), ((Binding.empty, []), rhs));
    99         val th = prove lthy raw_th;
   100       in
   101         (th, lthy)
   102       end
   103     val (def_thm, lthy) = if #notes config then note_def lthy else raw_def lthy
   104   in
   105     (SOME def_thm, lthy)
   106   end
   107   handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy))
   108 
   109 
   110 local
   111   val eq_OO_meta = mk_meta_eq @{thm eq_OO} 
   112 
   113   fun print_generate_pcr_cr_eq_error ctxt term = 
   114     let
   115       val goal = Const (@{const_name HOL.eq}, dummyT) $ term $ Const (@{const_name HOL.eq}, dummyT)
   116       val error_msg = cat_lines 
   117         ["Generation of a pcr_cr_eq failed.",
   118         (Pretty.string_of (Pretty.block
   119            [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
   120          "Most probably a relator_eq rule for one of the involved types is missing."]
   121     in
   122       error error_msg
   123     end
   124 in
   125   fun define_pcr_cr_eq (config: config) lthy pcr_rel_def =
   126     let
   127       val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def
   128       val qty_name =
   129         (Binding.name o Long_Name.base_name o fst o dest_Type o
   130           List.last o binder_types o fastype_of) lhs
   131       val args = (snd o strip_comb) lhs
   132       
   133       fun make_inst var ctxt = 
   134         let 
   135           val typ = (snd o relation_types o snd o dest_Var) var
   136           val sort = Type.sort_of_atyp typ
   137           val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt
   138         in
   139           (apply2 (Thm.cterm_of ctxt') (var, HOLogic.eq_const (TFree fresh_var)), ctxt')
   140         end
   141       
   142       val orig_lthy = lthy
   143       val (args_inst, lthy) = fold_map make_inst args lthy
   144       val pcr_cr_eq = 
   145         pcr_rel_def
   146         |> Drule.cterm_instantiate args_inst    
   147         |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv 
   148           (Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy))))
   149   in
   150     case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of
   151       Const (@{const_name "relcompp"}, _) $ Const (@{const_name HOL.eq}, _) $ _ =>
   152         let
   153           val thm = 
   154             pcr_cr_eq
   155             |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
   156             |> mk_HOL_eq
   157             |> singleton (Variable.export lthy orig_lthy)
   158           val lthy = (#notes config ? (Local_Theory.note 
   159               ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) #> snd)) lthy
   160         in
   161           (thm, lthy)
   162         end
   163       | Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
   164       | _ => error "generate_pcr_cr_eq: implementation error"
   165   end
   166 end
   167 
   168 fun define_code_constr quot_thm lthy =
   169   let
   170     val abs = quot_thm_abs quot_thm
   171   in
   172     if is_Const abs then
   173       let
   174         val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy
   175       in  
   176          Local_Theory.background_theory (Code.add_datatype [dest_Const fixed_abs]) lthy'
   177       end
   178     else
   179       lthy
   180   end
   181 
   182 fun define_abs_type quot_thm lthy =
   183   if Lifting_Def.can_generate_code_cert quot_thm then
   184     let
   185       val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
   186       val add_abstype_attribute = 
   187           Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype_default thm) I)
   188         val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
   189     in
   190       lthy
   191         |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
   192     end
   193   else
   194     lthy
   195 
   196 local
   197   exception QUOT_ERROR of Pretty.T list
   198 in
   199 fun quot_thm_sanity_check ctxt quot_thm =
   200   let
   201     val _ = 
   202       if (Thm.nprems_of quot_thm > 0) then   
   203           raise QUOT_ERROR [Pretty.block
   204             [Pretty.str "The Quotient theorem has extra assumptions:",
   205              Pretty.brk 1,
   206              Display.pretty_thm ctxt quot_thm]]
   207       else ()
   208     val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient
   209     handle TERM _ => raise QUOT_ERROR
   210           [Pretty.block
   211             [Pretty.str "The Quotient theorem is not of the right form:",
   212              Pretty.brk 1,
   213              Display.pretty_thm ctxt quot_thm]]
   214     val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt 
   215     val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
   216     val rty_tfreesT = Term.add_tfree_namesT rty []
   217     val qty_tfreesT = Term.add_tfree_namesT qty []
   218     val extra_rty_tfrees =
   219       case subtract (op =) qty_tfreesT rty_tfreesT of
   220         [] => []
   221       | extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
   222                                  Pretty.brk 1] @ 
   223                                  ((Pretty.commas o map (Pretty.str o quote)) extras) @
   224                                  [Pretty.str "."])]
   225     val not_type_constr = 
   226       case qty of
   227          Type _ => []
   228          | _ => [Pretty.block [Pretty.str "The quotient type ",
   229                                 Pretty.quote (Syntax.pretty_typ ctxt' qty),
   230                                 Pretty.brk 1,
   231                                 Pretty.str "is not a type constructor."]]
   232     val errs = extra_rty_tfrees @ not_type_constr
   233   in
   234     if null errs then () else raise QUOT_ERROR errs
   235   end
   236   handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] 
   237                                             @ (map (Pretty.string_of o Pretty.item o single) errs)))
   238 end
   239 
   240 fun lifting_bundle qty_full_name qinfo lthy = 
   241   let
   242     fun qualify suffix defname = Binding.qualified true suffix defname
   243     val binding =  qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting"
   244     val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding
   245     val bundle_name = Name_Space.full_name (Name_Space.naming_of 
   246       (Context.Theory (Proof_Context.theory_of lthy))) morphed_binding
   247     fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo
   248 
   249     val thy = Proof_Context.theory_of lthy
   250     val dummy_thm = Thm.transfer thy Drule.dummy_thm
   251     val pointer =
   252       Token.explode (Thy_Header.get_keywords thy) Position.none (cartouche bundle_name)
   253     val restore_lifting_att = 
   254       ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
   255   in
   256     lthy 
   257       |> Local_Theory.declaration {syntax = false, pervasive = true}
   258            (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
   259       |> Bundle.bundle ((binding, [restore_lifting_att])) []
   260       |> pair binding
   261   end
   262 
   263 fun setup_lifting_infr config quot_thm opt_reflp_thm lthy =
   264   let
   265     val _ = quot_thm_sanity_check lthy quot_thm
   266     val (_, qty) = quot_thm_rty_qty quot_thm
   267     val (pcrel_def, lthy) = define_pcrel config (quot_thm_crel quot_thm) lthy
   268     (**)
   269     val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
   270     (**)
   271     val (pcr_cr_eq, lthy) = case pcrel_def of
   272       SOME pcrel_def => apfst SOME (define_pcr_cr_eq config lthy pcrel_def)
   273       | NONE => (NONE, lthy)
   274     val pcr_info = case pcrel_def of
   275       SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
   276       | NONE => NONE
   277     val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
   278     val qty_full_name = (fst o dest_Type) qty
   279     fun quot_info phi = Lifting_Info.transform_quotient phi quotients
   280     val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
   281     val lthy = case opt_reflp_thm of
   282       SOME reflp_thm => lthy
   283         |> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]),
   284               [reflp_thm RS @{thm reflp_ge_eq}])
   285         |> define_code_constr quot_thm
   286       | NONE => lthy
   287         |> define_abs_type quot_thm
   288   in
   289     lthy
   290       |> Local_Theory.declaration {syntax = false, pervasive = true}
   291         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
   292       |> lifting_bundle qty_full_name quotients
   293   end
   294 
   295 local
   296   fun importT_inst_exclude exclude ts ctxt =
   297     let
   298       val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
   299       val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
   300     in (tvars ~~ map TFree tfrees, ctxt') end
   301   
   302   fun import_inst_exclude exclude ts ctxt =
   303     let
   304       val excludeT = fold (Term.add_tvarsT o snd) exclude []
   305       val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt
   306       val vars = map (apsnd (Term_Subst.instantiateT instT)) 
   307         (rev (subtract op= exclude (fold Term.add_vars ts [])))
   308       val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
   309       val inst = vars ~~ map Free (xs ~~ map #2 vars)
   310     in ((instT, inst), ctxt'') end
   311   
   312   fun import_terms_exclude exclude ts ctxt =
   313     let val (inst, ctxt') = import_inst_exclude exclude ts ctxt
   314     in (map (Term_Subst.instantiate inst) ts, ctxt') end
   315 in
   316   fun reduce_goal not_fix goal tac ctxt =
   317     let
   318       val (fixed_goal, ctxt') = yield_singleton (import_terms_exclude not_fix) goal ctxt
   319       val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
   320     in
   321       (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE tac init_goal))
   322     end
   323 end
   324 
   325 local 
   326   val OO_rules = @{thms left_total_OO left_unique_OO right_total_OO right_unique_OO bi_total_OO
   327     bi_unique_OO}
   328 in
   329   fun parametrize_class_constraint ctxt pcr_def constraint =
   330     let
   331       fun generate_transfer_rule pcr_def constraint goal ctxt =
   332         let
   333           val (fixed_goal, ctxt') = yield_singleton (Variable.import_terms true) goal ctxt
   334           val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal)
   335           val rules = Transfer.get_transfer_raw ctxt'
   336           val rules = constraint :: OO_rules @ rules
   337           val tac =
   338             K (Local_Defs.unfold_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules)
   339         in
   340           (singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
   341         end
   342       
   343       fun make_goal pcr_def constr =
   344         let 
   345           val pred_name =
   346             (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.prop_of) constr
   347           val arg = (fst o Logic.dest_equals o Thm.prop_of) pcr_def
   348         in
   349           HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
   350         end
   351       
   352       val check_assms =
   353         let 
   354           val right_names = ["right_total", "right_unique", "left_total", "left_unique", "bi_total",
   355             "bi_unique"]
   356       
   357           fun is_right_name name = member op= right_names (Long_Name.base_name name)
   358       
   359           fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name
   360             | is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name
   361             | is_trivial_assm _ = false
   362         in
   363           fn thm => 
   364             let
   365               val prems = map HOLogic.dest_Trueprop (Thm.prems_of thm)
   366               val thm_name =
   367                 (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm
   368               val non_trivial_assms = filter_out is_trivial_assm prems
   369             in
   370               if null non_trivial_assms then ()
   371               else
   372                 let
   373                   val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
   374                     Pretty.str thm_name,
   375                     Pretty.str " transfer rule found:",
   376                     Pretty.brk 1] @ 
   377                     ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
   378                                        [Pretty.str "."])
   379                 in
   380                   warning (Pretty.str_of pretty_msg)
   381                 end
   382             end
   383         end
   384   
   385       val goal = make_goal pcr_def constraint
   386       val thm = generate_transfer_rule pcr_def constraint goal ctxt
   387       val _ = check_assms thm
   388     in
   389       thm
   390     end
   391 end
   392 
   393 local
   394   val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def}))
   395 in
   396   fun generate_parametric_id lthy rty id_transfer_rule =
   397     let
   398       (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
   399       val (quot_thm, _, ctxt') = Lifting_Term.prove_param_quot_thm lthy rty
   400       val parametrized_relator =
   401         singleton (Variable.export_terms ctxt' lthy) (quot_thm_crel quot_thm)
   402       val id_transfer = 
   403          @{thm id_transfer}
   404         |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
   405         |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
   406       val var = Var (hd (Term.add_vars (Thm.prop_of id_transfer) []))
   407       val inst = [(Thm.cterm_of lthy var, Thm.cterm_of lthy parametrized_relator)]
   408       val id_par_thm = Drule.cterm_instantiate inst id_transfer
   409     in
   410       Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
   411     end
   412     handle Lifting_Term.MERGE_TRANSFER_REL msg => 
   413       let
   414         val error_msg = cat_lines 
   415           ["Generation of a parametric transfer rule for the abs. or the rep. function failed.",
   416           "A non-parametric version will be used.",
   417           (Pretty.string_of (Pretty.block
   418              [Pretty.str "Reason:", Pretty.brk 2, msg]))]
   419       in
   420         (warning error_msg; id_transfer_rule)
   421       end
   422 end
   423 
   424 local
   425   fun rewrite_first_Domainp_arg rewr_thm thm = Conv.fconv_rule (Conv.concl_conv ~1 (HOLogic.Trueprop_conv 
   426       (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv rewr_thm))))) thm
   427   
   428   fun fold_Domainp_pcrel pcrel_def thm =
   429     let
   430       val ct =
   431         thm |> Thm.cprop_of |> Drule.strip_imp_concl
   432         |> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg
   433       val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def
   434       val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm
   435         handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def])
   436     in
   437       rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm
   438     end
   439 
   440   fun reduce_Domainp ctxt rules thm =
   441     let
   442       val goal = thm |> Thm.prems_of |> hd
   443       val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var 
   444       val reduced_assm =
   445         reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt
   446     in
   447       reduced_assm RS thm
   448     end
   449 in
   450   fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt =
   451     let
   452       fun reduce_first_assm ctxt rules thm =
   453         let
   454           val goal = thm |> Thm.prems_of |> hd
   455           val reduced_assm =
   456             reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt
   457         in
   458           reduced_assm RS thm
   459         end
   460 
   461       val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection}
   462       val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm
   463       val pcrel_def = #pcrel_def pcr_info
   464       val pcr_Domainp_par_left_total = 
   465         (dom_thm RS @{thm pcr_Domainp_par_left_total})
   466           |> fold_Domainp_pcrel pcrel_def
   467           |> reduce_first_assm ctxt (Lifting_Info.get_reflexivity_rules ctxt)
   468       val pcr_Domainp_par = 
   469         (dom_thm RS @{thm pcr_Domainp_par})      
   470           |> fold_Domainp_pcrel pcrel_def
   471           |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
   472       val pcr_Domainp = 
   473         (dom_thm RS @{thm pcr_Domainp})
   474           |> fold_Domainp_pcrel pcrel_def
   475       val thms =
   476         [("domain",                 [pcr_Domainp], @{attributes [transfer_domain_rule]}),
   477          ("domain_par",             [pcr_Domainp_par], @{attributes [transfer_domain_rule]}),
   478          ("domain_par_left_total",  [pcr_Domainp_par_left_total], @{attributes [transfer_domain_rule]}),
   479          ("domain_eq",              [pcr_Domainp_eq], @{attributes [transfer_domain_rule]})]
   480     in
   481       thms
   482     end
   483 
   484   fun parametrize_total_domain left_total pcrel_def ctxt =
   485     let
   486       val thm =
   487         (left_total RS @{thm pcr_Domainp_total})
   488           |> fold_Domainp_pcrel pcrel_def 
   489           |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt)
   490     in
   491       [("domain", [thm], @{attributes [transfer_domain_rule]})]
   492     end
   493 
   494 end
   495 
   496 fun get_pcrel_info ctxt qty_full_name =  
   497   #pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
   498 
   499 fun get_Domainp_thm quot_thm =
   500    the (get_first (try(curry op RS quot_thm)) [@{thm eq_onp_to_Domainp}, @{thm Quotient_to_Domainp}])
   501 
   502 fun notes names thms = 
   503   let
   504     val notes =
   505         if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms
   506         else map_filter (fn (_, thms, attrs) => if null attrs then NONE 
   507           else SOME ((Binding.empty, []), [(thms, attrs)])) thms
   508   in
   509     Local_Theory.notes notes #> snd
   510   end
   511 
   512 fun map_thms map_name map_thm thms = 
   513   map (fn (name, thms, attr) => (map_name name, map map_thm thms, attr)) thms
   514 
   515 (*
   516   Sets up the Lifting package by a quotient theorem.
   517 
   518   quot_thm - a quotient theorem (Quotient R Abs Rep T)
   519   opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
   520     (in the form "reflp R")
   521   opt_par_thm - a parametricity theorem for R
   522 *)
   523 
   524 fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy =
   525   let
   526     (**)
   527     val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
   528     (**)
   529     val (rty, qty) = quot_thm_rty_qty quot_thm
   530     val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
   531     val qty_full_name = (fst o dest_Type) qty
   532     val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
   533     fun qualify suffix = Binding.qualified true suffix qty_name
   534     val notes1 = case opt_reflp_thm of
   535       SOME reflp_thm =>
   536         let 
   537           val thms =
   538             [("abs_induct",     @{thms Quotient_total_abs_induct}, [induct_attr]),
   539              ("abs_eq_iff",     @{thms Quotient_total_abs_eq_iff}, []           )]
   540         in
   541           map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms
   542         end
   543       | NONE =>
   544         let
   545           val thms = 
   546             [("abs_induct",     @{thms Quotient_abs_induct},       [induct_attr])]
   547         in
   548           map_thms qualify (fn thm => quot_thm RS thm) thms
   549         end
   550     val dom_thm = get_Domainp_thm quot_thm
   551 
   552     fun setup_transfer_rules_nonpar notes =
   553       let
   554         val notes1 =
   555           case opt_reflp_thm of
   556             SOME reflp_thm =>
   557               let 
   558                 val thms =
   559                   [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}),
   560                    ("left_total",     @{thms Quotient_left_total},      @{attributes [transfer_rule]}),
   561                    ("bi_total",       @{thms Quotient_bi_total},        @{attributes [transfer_rule]})]
   562               in
   563                 map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms
   564               end
   565             | NONE => map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})]
   566 
   567         val notes2 = map_thms qualify (fn thm => quot_thm RS thm)
   568           [("rel_eq_transfer", @{thms Quotient_rel_eq_transfer}, @{attributes [transfer_rule]}),
   569            ("right_unique",    @{thms Quotient_right_unique},    @{attributes [transfer_rule]}), 
   570            ("right_total",     @{thms Quotient_right_total},     @{attributes [transfer_rule]})]
   571       in
   572          notes2 @ notes1 @ notes
   573       end
   574 
   575     fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm =
   576       option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm
   577       handle Lifting_Term.MERGE_TRANSFER_REL msg => 
   578         let
   579           val error_msg = cat_lines 
   580             ["Generation of a parametric transfer rule for the quotient relation failed.",
   581             (Pretty.string_of (Pretty.block
   582                [Pretty.str "Reason:", Pretty.brk 2, msg]))]
   583         in
   584           error error_msg
   585         end
   586 
   587     fun setup_transfer_rules_par lthy notes =
   588       let
   589         val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
   590         val pcrel_def = #pcrel_def pcrel_info
   591         val notes1 =
   592           case opt_reflp_thm of
   593             SOME reflp_thm =>
   594               let
   595                 val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
   596                 val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
   597                 val domain_thms = parametrize_total_domain left_total pcrel_def lthy
   598                 val id_abs_transfer = generate_parametric_id lthy rty
   599                   (Lifting_Term.parametrize_transfer_rule lthy
   600                     ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
   601                 val left_total = parametrize_class_constraint lthy pcrel_def left_total
   602                 val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
   603                 val thms = 
   604                   [("id_abs_transfer", [id_abs_transfer], @{attributes [transfer_rule]}),
   605                    ("left_total",      [left_total],      @{attributes [transfer_rule]}),  
   606                    ("bi_total",        [bi_total],        @{attributes [transfer_rule]})]
   607               in
   608                 map_thms qualify I thms @ map_thms qualify I domain_thms
   609               end
   610             | NONE =>
   611               let
   612                 val thms = parametrize_domain dom_thm pcrel_info lthy
   613               in
   614                 map_thms qualify I thms
   615               end
   616 
   617         val rel_eq_transfer = generate_parametric_rel_eq lthy 
   618           (Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
   619             opt_par_thm
   620         val right_unique = parametrize_class_constraint lthy pcrel_def 
   621             (quot_thm RS @{thm Quotient_right_unique})
   622         val right_total = parametrize_class_constraint lthy pcrel_def 
   623             (quot_thm RS @{thm Quotient_right_total})
   624         val notes2 = map_thms qualify I
   625           [("rel_eq_transfer", [rel_eq_transfer], @{attributes [transfer_rule]}),
   626            ("right_unique",    [right_unique],    @{attributes [transfer_rule]}), 
   627            ("right_total",     [right_total],     @{attributes [transfer_rule]})]      
   628       in
   629         notes2 @ notes1 @ notes
   630       end
   631 
   632     fun setup_rules lthy = 
   633       let
   634         val thms =  if is_some (get_pcrel_info lthy qty_full_name) 
   635           then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1
   636       in
   637         notes (#notes config) thms lthy
   638       end
   639   in
   640     lthy
   641       |> setup_lifting_infr config quot_thm opt_reflp_thm
   642       ||> setup_rules
   643   end
   644 
   645 (*
   646   Sets up the Lifting package by a typedef theorem.
   647 
   648   gen_code - flag if an abstract type given by typedef_thm should be registred 
   649     as an abstract type in the code generator
   650   typedef_thm - a typedef theorem (type_definition Rep Abs S)
   651 *)
   652 
   653 fun setup_by_typedef_thm config typedef_thm lthy =
   654   let
   655     val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o Thm.prop_of) typedef_thm
   656     val (T_def, lthy) = define_crel config rep_fun lthy
   657     (**)
   658     val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
   659     (**)    
   660     val quot_thm = case typedef_set of
   661       Const (@{const_name top}, _) => 
   662         [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
   663       | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => 
   664         [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
   665       | _ => 
   666         [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
   667     val (rty, qty) = quot_thm_rty_qty quot_thm
   668     val qty_full_name = (fst o dest_Type) qty
   669     val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
   670     fun qualify suffix = Binding.qualified true suffix qty_name
   671     val opt_reflp_thm = 
   672       case typedef_set of
   673         Const (@{const_name top}, _) => 
   674           SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
   675         | _ =>  NONE
   676     val dom_thm = get_Domainp_thm quot_thm
   677 
   678     fun setup_transfer_rules_nonpar notes =
   679       let
   680         val notes1 =
   681           case opt_reflp_thm of
   682             SOME reflp_thm =>
   683               let 
   684                 val thms =
   685                   [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}),
   686                    ("left_total",     @{thms Quotient_left_total},      @{attributes [transfer_rule]}),
   687                    ("bi_total",       @{thms Quotient_bi_total},        @{attributes [transfer_rule]})]
   688               in
   689                 map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms
   690               end
   691             | NONE =>
   692               map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})]
   693         val thms = 
   694           [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]}),
   695            ("left_unique",  @{thms typedef_left_unique},  @{attributes [transfer_rule]}),
   696            ("right_unique", @{thms typedef_right_unique}, @{attributes [transfer_rule]}), 
   697            ("right_total",  @{thms typedef_right_total},  @{attributes [transfer_rule]}),
   698            ("bi_unique",    @{thms typedef_bi_unique},    @{attributes [transfer_rule]})]
   699       in                                               
   700         map_thms qualify (fn thm => [typedef_thm, T_def] MRSL thm) thms @ notes1 @ notes
   701       end
   702 
   703     fun setup_transfer_rules_par lthy notes =
   704       let
   705         val pcrel_info = (the (get_pcrel_info lthy qty_full_name))
   706         val pcrel_def = #pcrel_def pcrel_info
   707 
   708         val notes1 =
   709           case opt_reflp_thm of
   710             SOME reflp_thm =>
   711               let
   712                 val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total})
   713                 val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
   714                 val domain_thms = parametrize_total_domain left_total pcrel_def lthy
   715                 val left_total = parametrize_class_constraint lthy pcrel_def left_total
   716                 val bi_total = parametrize_class_constraint lthy pcrel_def bi_total
   717                 val id_abs_transfer = generate_parametric_id lthy rty
   718                   (Lifting_Term.parametrize_transfer_rule lthy
   719                     ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
   720                 val thms = 
   721                   [("left_total",     [left_total],      @{attributes [transfer_rule]}),
   722                    ("bi_total",       [bi_total],        @{attributes [transfer_rule]}),
   723                    ("id_abs_transfer",[id_abs_transfer], @{attributes [transfer_rule]})]              
   724               in
   725                 map_thms qualify I thms @ map_thms qualify I domain_thms
   726               end
   727             | NONE =>
   728               let
   729                 val thms = parametrize_domain dom_thm pcrel_info lthy
   730               in
   731                 map_thms qualify I thms
   732               end
   733               
   734         val notes2 = map_thms qualify (fn thm => generate_parametric_id lthy rty 
   735             (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL thm)))
   736           [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]})];
   737         val notes3 =
   738           map_thms qualify
   739           (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
   740           [("left_unique",  @{thms typedef_left_unique}, @{attributes [transfer_rule]}),
   741            ("right_unique", @{thms typedef_right_unique},@{attributes [transfer_rule]}),
   742            ("bi_unique",    @{thms typedef_bi_unique},   @{attributes [transfer_rule]}),
   743            ("right_total",  @{thms typedef_right_total}, @{attributes [transfer_rule]})]
   744       in
   745         notes3 @ notes2 @ notes1 @ notes
   746       end
   747 
   748     val notes1 = [(Binding.prefix_name "Quotient_" qty_name, [quot_thm], [])]
   749 
   750     fun setup_rules lthy = 
   751       let
   752         val thms =  if is_some (get_pcrel_info lthy qty_full_name) 
   753           then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1
   754       in
   755         notes (#notes config) thms lthy
   756       end
   757   in
   758     lthy
   759       |> setup_lifting_infr config quot_thm opt_reflp_thm
   760       ||> setup_rules
   761   end
   762 
   763 fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy =
   764   let 
   765     val input_thm = singleton (Attrib.eval_thms lthy) xthm
   766     val input_term = (HOLogic.dest_Trueprop o Thm.prop_of) input_thm
   767       handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   768 
   769     fun sanity_check_reflp_thm reflp_thm = 
   770       let
   771         val reflp_tm = (HOLogic.dest_Trueprop o Thm.prop_of) reflp_thm
   772           handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
   773       in
   774         case reflp_tm of
   775           Const (@{const_name reflp}, _) $ _ => ()
   776           | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
   777       end
   778       
   779     fun check_qty qty = if not (is_Type qty) 
   780           then error "The abstract type must be a type constructor."
   781           else ()
   782    
   783     fun setup_quotient () = 
   784       let
   785         val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
   786         val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
   787         val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
   788         val _ = check_qty (snd (quot_thm_rty_qty input_thm))
   789       in
   790         setup_by_quotient default_config input_thm opt_reflp_thm opt_par_thm lthy |> snd
   791       end
   792 
   793     fun setup_typedef () = 
   794       let
   795         val qty = (range_type o fastype_of o hd o get_args 2) input_term
   796         val _ = check_qty qty
   797       in
   798         case opt_reflp_xthm of
   799           SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
   800           | NONE => (
   801             case opt_par_xthm of
   802               SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
   803               | NONE => setup_by_typedef_thm default_config input_thm lthy |> snd
   804           )
   805       end
   806   in
   807     case input_term of
   808       (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
   809       | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef ()
   810       | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   811   end
   812 
   813 val _ = 
   814   Outer_Syntax.local_theory @{command_keyword setup_lifting}
   815     "setup lifting infrastructure" 
   816       (Parse.xthm -- Scan.option Parse.xthm 
   817       -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> 
   818         (fn ((xthm, opt_reflp_xthm), opt_par_xthm) => 
   819           setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm))
   820 
   821 (* restoring lifting infrastructure *)
   822 
   823 local
   824   exception PCR_ERROR of Pretty.T list
   825 in
   826 
   827 fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) =
   828   let
   829     val quot_thm = (#quot_thm qinfo)
   830     val _ = quot_thm_sanity_check ctxt quot_thm
   831     val pcr_info_err =
   832       (case #pcr_info qinfo of
   833         SOME pcr => 
   834           let
   835             val pcrel_def = #pcrel_def pcr
   836             val pcr_cr_eq = #pcr_cr_eq pcr
   837             val (def_lhs, _) = Logic.dest_equals (Thm.prop_of pcrel_def)
   838               handle TERM _ => raise PCR_ERROR [Pretty.block 
   839                     [Pretty.str "The pcr definiton theorem is not a plain meta equation:",
   840                     Pretty.brk 1,
   841                     Display.pretty_thm ctxt pcrel_def]]
   842             val pcr_const_def = head_of def_lhs
   843             val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq))
   844               handle TERM _ => raise PCR_ERROR [Pretty.block 
   845                     [Pretty.str "The pcr_cr equation theorem is not a plain equation:",
   846                     Pretty.brk 1,
   847                     Display.pretty_thm ctxt pcr_cr_eq]]
   848             val (pcr_const_eq, eqs) = strip_comb eq_lhs
   849             fun is_eq (Const (@{const_name HOL.eq}, _)) = true
   850               | is_eq _ = false
   851             fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
   852               | eq_Const _ _ = false
   853             val all_eqs = if not (forall is_eq eqs) then 
   854               [Pretty.block
   855                     [Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:",
   856                     Pretty.brk 1,
   857                     Display.pretty_thm ctxt pcr_cr_eq]]
   858               else []
   859             val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then
   860               [Pretty.block
   861                     [Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:",
   862                     Pretty.brk 1,
   863                     Syntax.pretty_term ctxt pcr_const_def,
   864                     Pretty.brk 1,
   865                     Pretty.str "vs.",
   866                     Pretty.brk 1,
   867                     Syntax.pretty_term ctxt pcr_const_eq]]
   868               else []
   869             val crel = quot_thm_crel quot_thm
   870             val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then
   871               [Pretty.block
   872                     [Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:",
   873                     Pretty.brk 1,
   874                     Syntax.pretty_term ctxt crel,
   875                     Pretty.brk 1,
   876                     Pretty.str "vs.",
   877                     Pretty.brk 1,
   878                     Syntax.pretty_term ctxt eq_rhs]]
   879               else []
   880           in
   881             all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal
   882           end
   883         | NONE => [])
   884     val errs = pcr_info_err
   885   in
   886     if null errs then () else raise PCR_ERROR errs
   887   end
   888   handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] 
   889                                             @ (map (Pretty.string_of o Pretty.item o single) errs)))
   890 end
   891 
   892 (*
   893   Registers the data in qinfo in the Lifting infrastructure.
   894 *)
   895 
   896 fun lifting_restore qinfo ctxt =
   897   let
   898     val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
   899     val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo)
   900     val qty_full_name = (fst o dest_Type) qty
   901     val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name
   902   in
   903     if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo)))
   904       then error (Pretty.string_of 
   905         (Pretty.block
   906           [Pretty.str "Lifting is already setup for the type",
   907            Pretty.brk 1,
   908            Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)]))
   909       else Lifting_Info.update_quotients qty_full_name qinfo ctxt
   910   end
   911 
   912 val parse_opt_pcr =
   913   Scan.optional (Attrib.thm -- Attrib.thm >> 
   914     (fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE
   915 
   916 val lifting_restore_attribute_setup =
   917   Attrib.setup @{binding lifting_restore}
   918     ((Attrib.thm -- parse_opt_pcr) >>
   919       (fn (quot_thm, opt_pcr) =>
   920         let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr}
   921         in Thm.declaration_attribute (K (lifting_restore qinfo)) end))
   922     "restoring lifting infrastructure"
   923 
   924 val _ = Theory.setup lifting_restore_attribute_setup 
   925 
   926 fun lifting_restore_internal bundle_name ctxt = 
   927   let 
   928     val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name
   929   in
   930     case restore_info of
   931       SOME restore_info =>
   932         ctxt 
   933         |> lifting_restore (#quotient restore_info)
   934         |> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info))
   935       | NONE => ctxt
   936   end
   937 
   938 val lifting_restore_internal_attribute_setup =
   939   Attrib.setup @{binding lifting_restore_internal}
   940     (Scan.lift Parse.cartouche >>
   941       (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
   942     "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
   943 
   944 val _ = Theory.setup lifting_restore_internal_attribute_setup 
   945 
   946 (* lifting_forget *)
   947 
   948 val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total},
   949   @{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}]
   950 
   951 fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel
   952   | fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $ 
   953     (Const (@{const_name Domainp}, _) $ rel) $ _) = f rel
   954   | fold_transfer_rel f (Const (name, _) $ rel) = 
   955     if member op= monotonicity_names name then f rel else f @{term undefined}
   956   | fold_transfer_rel f _ = f @{term undefined}
   957 
   958 fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
   959   let
   960     val transfer_rel_name = transfer_rel |> dest_Const |> fst;
   961     fun has_transfer_rel thm = 
   962       let
   963         val concl = thm |> Thm.concl_of |> HOLogic.dest_Trueprop
   964       in
   965         member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name
   966       end
   967       handle TERM _ => false
   968   in
   969     filter has_transfer_rel transfer_rules
   970   end
   971 
   972 type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T}
   973 
   974 fun get_transfer_rel (qinfo : Lifting_Info.quotient) =
   975   let
   976     fun get_pcrel pcr_def = pcr_def |> Thm.concl_of |> Logic.dest_equals |> fst |> head_of
   977   in
   978     if is_some (#pcr_info qinfo) 
   979       then get_pcrel (#pcrel_def (the (#pcr_info qinfo)))
   980       else quot_thm_crel (#quot_thm qinfo)
   981   end
   982 
   983 fun pointer_of_bundle_name bundle_name ctxt =
   984   let
   985     val bundle = Bundle.get_bundle_cmd ctxt bundle_name
   986   in
   987     case bundle of
   988       [(_, [arg_src])] => 
   989         let
   990           val (name, _) = Token.syntax (Scan.lift Parse.cartouche) arg_src ctxt
   991             handle ERROR _ => error "The provided bundle is not a lifting bundle."
   992         in name end
   993       | _ => error "The provided bundle is not a lifting bundle."
   994   end
   995 
   996 fun pointer_of_bundle_binding ctxt binding = Name_Space.full_name (Name_Space.naming_of 
   997       (Context.Theory (Proof_Context.theory_of ctxt))) binding
   998 
   999 fun lifting_forget pointer lthy =
  1000   let
  1001     fun get_transfer_rules_to_delete qinfo ctxt =
  1002       let
  1003         val transfer_rel = get_transfer_rel qinfo
  1004       in
  1005          filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt)
  1006       end
  1007   in
  1008     case Lifting_Info.lookup_restore_data lthy pointer of
  1009       SOME restore_info =>
  1010         let
  1011           val qinfo = #quotient restore_info
  1012           val quot_thm = #quot_thm qinfo
  1013           val transfer_rules = get_transfer_rules_to_delete qinfo lthy
  1014         in
  1015           Local_Theory.declaration {syntax = false, pervasive = true}
  1016             (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
  1017             lthy
  1018         end
  1019       | NONE => error "The lifting bundle refers to non-existent restore data."
  1020     end
  1021     
  1022 
  1023 fun lifting_forget_cmd bundle_name lthy = 
  1024   lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy
  1025 
  1026 
  1027 val _ =
  1028   Outer_Syntax.local_theory @{command_keyword lifting_forget} 
  1029     "unsetup Lifting and Transfer for the given lifting bundle"
  1030     (Parse.position Parse.xname >> (lifting_forget_cmd))
  1031 
  1032 (* lifting_update *)
  1033 
  1034 fun update_transfer_rules pointer lthy =
  1035   let
  1036     fun new_transfer_rules ({ quotient = qinfo, ... }:Lifting_Info.restore_data) lthy =
  1037       let
  1038         val transfer_rel = get_transfer_rel qinfo
  1039         val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy)
  1040       in
  1041         fn phi => fold_rev 
  1042           (Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules
  1043       end
  1044   in
  1045     case Lifting_Info.lookup_restore_data lthy pointer of
  1046       SOME refresh_data => 
  1047         Local_Theory.declaration {syntax = false, pervasive = true}
  1048           (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer 
  1049             (new_transfer_rules refresh_data lthy phi)) lthy
  1050       | NONE => error "The lifting bundle refers to non-existent restore data."
  1051   end
  1052 
  1053 fun lifting_update_cmd bundle_name lthy = 
  1054   update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy
  1055 
  1056 val _ =
  1057   Outer_Syntax.local_theory @{command_keyword lifting_update}
  1058     "add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
  1059     (Parse.position Parse.xname >> lifting_update_cmd)
  1060 
  1061 end