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