1(* Title: HOL/Tools/Lifting/lifting_def.ML 2 Author: Ondrej Kuncar 3 4Definitions for constants on quotient types. 5*) 6 7signature LIFTING_DEF = 8sig 9 datatype code_eq = UNKNOWN_EQ | NONE_EQ | ABS_EQ | REP_EQ 10 type lift_def 11 val rty_of_lift_def: lift_def -> typ 12 val qty_of_lift_def: lift_def -> typ 13 val rhs_of_lift_def: lift_def -> term 14 val lift_const_of_lift_def: lift_def -> term 15 val def_thm_of_lift_def: lift_def -> thm 16 val rsp_thm_of_lift_def: lift_def -> thm 17 val abs_eq_of_lift_def: lift_def -> thm 18 val rep_eq_of_lift_def: lift_def -> thm option 19 val code_eq_of_lift_def: lift_def -> code_eq 20 val transfer_rules_of_lift_def: lift_def -> thm list 21 val morph_lift_def: morphism -> lift_def -> lift_def 22 val inst_of_lift_def: Proof.context -> typ -> lift_def -> lift_def 23 val mk_lift_const_of_lift_def: typ -> lift_def -> term 24 25 type config = { notes: bool } 26 val map_config: (bool -> bool) -> config -> config 27 val default_config: config 28 29 val generate_parametric_transfer_rule: 30 Proof.context -> thm -> thm -> thm 31 32 val add_lift_def: 33 config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 34 lift_def * local_theory 35 36 val prepare_lift_def: 37 (binding * mixfix -> typ -> term -> thm -> thm list -> Proof.context -> 38 lift_def * local_theory) -> 39 binding * mixfix -> typ -> term -> thm list -> local_theory -> 40 term option * (thm -> Proof.context -> lift_def * local_theory) 41 42 val gen_lift_def: 43 (binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> 44 lift_def * local_theory) -> 45 binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 46 local_theory -> lift_def * local_theory 47 48 val lift_def: 49 config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> 50 local_theory -> lift_def * local_theory 51 52 val can_generate_code_cert: thm -> bool 53end 54 55structure Lifting_Def: LIFTING_DEF = 56struct 57 58open Lifting_Util 59 60infix 0 MRSL 61 62datatype code_eq = UNKNOWN_EQ | NONE_EQ | ABS_EQ | REP_EQ 63 64datatype lift_def = LIFT_DEF of { 65 rty: typ, 66 qty: typ, 67 rhs: term, 68 lift_const: term, 69 def_thm: thm, 70 rsp_thm: thm, 71 abs_eq: thm, 72 rep_eq: thm option, 73 code_eq: code_eq, 74 transfer_rules: thm list 75}; 76 77fun rep_lift_def (LIFT_DEF lift_def) = lift_def; 78val rty_of_lift_def = #rty o rep_lift_def; 79val qty_of_lift_def = #qty o rep_lift_def; 80val rhs_of_lift_def = #rhs o rep_lift_def; 81val lift_const_of_lift_def = #lift_const o rep_lift_def; 82val def_thm_of_lift_def = #def_thm o rep_lift_def; 83val rsp_thm_of_lift_def = #rsp_thm o rep_lift_def; 84val abs_eq_of_lift_def = #abs_eq o rep_lift_def; 85val rep_eq_of_lift_def = #rep_eq o rep_lift_def; 86val code_eq_of_lift_def = #code_eq o rep_lift_def; 87val transfer_rules_of_lift_def = #transfer_rules o rep_lift_def; 88 89fun mk_lift_def rty qty rhs lift_const def_thm rsp_thm abs_eq rep_eq code_eq transfer_rules = 90 LIFT_DEF {rty = rty, qty = qty, 91 rhs = rhs, lift_const = lift_const, 92 def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, 93 code_eq = code_eq, transfer_rules = transfer_rules }; 94 95fun map_lift_def f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 96 (LIFT_DEF {rty = rty, qty = qty, rhs = rhs, lift_const = lift_const, 97 def_thm = def_thm, rsp_thm = rsp_thm, abs_eq = abs_eq, rep_eq = rep_eq, code_eq = code_eq, 98 transfer_rules = transfer_rules }) = 99 LIFT_DEF {rty = f1 rty, qty = f2 qty, rhs = f3 rhs, lift_const = f4 lift_const, 100 def_thm = f5 def_thm, rsp_thm = f6 rsp_thm, abs_eq = f7 abs_eq, rep_eq = f8 rep_eq, 101 code_eq = f9 code_eq, transfer_rules = f10 transfer_rules } 102 103fun morph_lift_def phi = 104 let 105 val mtyp = Morphism.typ phi 106 val mterm = Morphism.term phi 107 val mthm = Morphism.thm phi 108 in 109 map_lift_def mtyp mtyp mterm mterm mthm mthm mthm (Option.map mthm) I (map mthm) 110 end 111 112fun mk_inst_of_lift_def qty lift_def = Vartab.empty |> Type.raw_match (qty_of_lift_def lift_def, qty) 113 114fun mk_lift_const_of_lift_def qty lift_def = Envir.subst_term_types (mk_inst_of_lift_def qty lift_def) 115 (lift_const_of_lift_def lift_def) 116 117fun inst_of_lift_def ctxt qty lift_def = 118 let 119 val instT = 120 Vartab.fold (fn (a, (S, T)) => cons ((a, S), Thm.ctyp_of ctxt T)) 121 (mk_inst_of_lift_def qty lift_def) [] 122 val phi = Morphism.instantiate_morphism (instT, []) 123 in morph_lift_def phi lift_def end 124 125 126(* Config *) 127 128type config = { notes: bool }; 129fun map_config f1 { notes = notes } = { notes = f1 notes } 130val default_config = { notes = true }; 131 132(* Reflexivity prover *) 133 134fun mono_eq_prover ctxt prop = 135 let 136 val refl_rules = Lifting_Info.get_reflexivity_rules ctxt 137 val transfer_rules = Transfer.get_transfer_raw ctxt 138 139 fun main_tac i = (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt refl_rules) THEN_ALL_NEW 140 (REPEAT_ALL_NEW (DETERM o resolve_tac ctxt transfer_rules))) i 141 in 142 SOME (Goal.prove ctxt [] [] prop (K (main_tac 1))) 143 handle ERROR _ => NONE 144 end 145 146fun try_prove_refl_rel ctxt rel = 147 let 148 fun mk_ge_eq x = 149 let 150 val T = fastype_of x 151 in 152 Const (\<^const_name>\<open>less_eq\<close>, T --> T --> HOLogic.boolT) $ 153 (Const (\<^const_name>\<open>HOL.eq\<close>, T)) $ x 154 end; 155 val goal = HOLogic.mk_Trueprop (mk_ge_eq rel); 156 in 157 mono_eq_prover ctxt goal 158 end; 159 160fun try_prove_reflexivity ctxt prop = 161 let 162 val cprop = Thm.cterm_of ctxt prop 163 val rule = @{thm ge_eq_refl} 164 val concl_pat = Drule.strip_imp_concl (Thm.cprop_of rule) 165 val insts = Thm.first_order_match (concl_pat, cprop) 166 val rule = Drule.instantiate_normalize insts rule 167 val prop = hd (Thm.prems_of rule) 168 in 169 case mono_eq_prover ctxt prop of 170 SOME thm => SOME (thm RS rule) 171 | NONE => NONE 172 end 173 174(* 175 Generates a parametrized transfer rule. 176 transfer_rule - of the form T t f 177 parametric_transfer_rule - of the form par_R t' t 178 179 Result: par_T t' f, after substituing op= for relations in par_R that relate 180 a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f 181 using Lifting_Term.merge_transfer_relations 182*) 183 184fun generate_parametric_transfer_rule ctxt0 transfer_rule parametric_transfer_rule = 185 let 186 fun preprocess ctxt thm = 187 let 188 val tm = (strip_args 2 o HOLogic.dest_Trueprop o Thm.concl_of) thm; 189 val param_rel = (snd o dest_comb o fst o dest_comb) tm; 190 val free_vars = Term.add_vars param_rel []; 191 192 fun make_subst (xi, typ) subst = 193 let 194 val [rty, rty'] = binder_types typ 195 in 196 if Term.is_TVar rty andalso Term.is_Type rty' then 197 (xi, Thm.cterm_of ctxt (HOLogic.eq_const rty')) :: subst 198 else 199 subst 200 end; 201 202 val inst_thm = infer_instantiate ctxt (fold make_subst free_vars []) thm; 203 in 204 Conv.fconv_rule 205 ((Conv.concl_conv (Thm.nprems_of inst_thm) o 206 HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv) 207 (Raw_Simplifier.rewrite ctxt false (Transfer.get_sym_relator_eq ctxt))) inst_thm 208 end 209 210 fun inst_relcomppI ctxt ant1 ant2 = 211 let 212 val t1 = (HOLogic.dest_Trueprop o Thm.concl_of) ant1 213 val t2 = (HOLogic.dest_Trueprop o Thm.prop_of) ant2 214 val fun1 = Thm.cterm_of ctxt (strip_args 2 t1) 215 val args1 = map (Thm.cterm_of ctxt) (get_args 2 t1) 216 val fun2 = Thm.cterm_of ctxt (strip_args 2 t2) 217 val args2 = map (Thm.cterm_of ctxt) (get_args 1 t2) 218 val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI} 219 val vars = map #1 (rev (Term.add_vars (Thm.prop_of relcomppI) [])) 220 in 221 infer_instantiate ctxt (vars ~~ ([fun1] @ args1 @ [fun2] @ args2)) relcomppI 222 end 223 224 fun zip_transfer_rules ctxt thm = 225 let 226 fun mk_POS ty = Const (\<^const_name>\<open>POS\<close>, ty --> ty --> HOLogic.boolT) 227 val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm 228 val typ = Thm.typ_of_cterm rel 229 val POS_const = Thm.cterm_of ctxt (mk_POS typ) 230 val var = Thm.cterm_of ctxt (Var (("X", Thm.maxidx_of_cterm rel + 1), typ)) 231 val goal = 232 Thm.apply (Thm.cterm_of ctxt HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var) 233 in 234 [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply} 235 end 236 237 val thm = 238 inst_relcomppI ctxt0 parametric_transfer_rule transfer_rule 239 OF [parametric_transfer_rule, transfer_rule] 240 val preprocessed_thm = preprocess ctxt0 thm 241 val (fixed_thm, ctxt1) = ctxt0 242 |> yield_singleton (apfst snd oo Variable.import true) preprocessed_thm 243 val assms = cprems_of fixed_thm 244 val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add 245 val (prems, ctxt2) = ctxt1 |> fold_map Thm.assume_hyps assms 246 val ctxt3 = ctxt2 |> Context.proof_map (fold add_transfer_rule prems) 247 val zipped_thm = 248 fixed_thm 249 |> undisch_all 250 |> zip_transfer_rules ctxt3 251 |> implies_intr_list assms 252 |> singleton (Variable.export ctxt3 ctxt0) 253 in 254 zipped_thm 255 end 256 257fun print_generate_transfer_info msg = 258 let 259 val error_msg = cat_lines 260 ["Generation of a parametric transfer rule failed.", 261 (Pretty.string_of (Pretty.block 262 [Pretty.str "Reason:", Pretty.brk 2, msg]))] 263 in 264 error error_msg 265 end 266 267fun map_ter _ x [] = x 268 | map_ter f _ xs = map f xs 269 270fun generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms = 271 let 272 val transfer_rule = 273 ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) 274 |> Lifting_Term.parametrize_transfer_rule lthy 275 in 276 (map_ter (generate_parametric_transfer_rule lthy transfer_rule) [transfer_rule] par_thms 277 handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; [transfer_rule])) 278 end 279 280(* Generation of the code certificate from the rsp theorem *) 281 282fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V) 283 | get_body_types (U, V) = (U, V) 284 285fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W) 286 | get_binder_types _ = [] 287 288fun get_binder_types_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) = 289 (T, V) :: get_binder_types_by_rel S (U, W) 290 | get_binder_types_by_rel _ _ = [] 291 292fun get_body_type_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) = 293 get_body_type_by_rel S (U, V) 294 | get_body_type_by_rel _ (U, V) = (U, V) 295 296fun get_binder_rels (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R $ S) = R :: get_binder_rels S 297 | get_binder_rels _ = [] 298 299fun force_rty_type ctxt rty rhs = 300 let 301 val thy = Proof_Context.theory_of ctxt 302 val rhs_schematic = singleton (Variable.polymorphic ctxt) rhs 303 val rty_schematic = fastype_of rhs_schematic 304 val match = Sign.typ_match thy (rty_schematic, rty) Vartab.empty 305 in 306 Envir.subst_term_types match rhs_schematic 307 end 308 309fun unabs_def ctxt def = 310 let 311 val (_, rhs) = Thm.dest_equals (Thm.cprop_of def) 312 fun dest_abs (Abs (var_name, T, _)) = (var_name, T) 313 | dest_abs tm = raise TERM("get_abs_var",[tm]) 314 val (var_name, T) = dest_abs (Thm.term_of rhs) 315 val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt 316 val refl_thm = Thm.reflexive (Thm.cterm_of ctxt' (Free (hd new_var_names, T))) 317 in 318 Thm.combination def refl_thm |> 319 singleton (Proof_Context.export ctxt' ctxt) 320 end 321 322fun unabs_all_def ctxt def = 323 let 324 val (_, rhs) = Thm.dest_equals (Thm.cprop_of def) 325 val xs = strip_abs_vars (Thm.term_of rhs) 326 in 327 fold (K (unabs_def ctxt)) xs def 328 end 329 330val map_fun_unfolded = 331 @{thm map_fun_def[abs_def]} |> 332 unabs_def \<^context> |> 333 unabs_def \<^context> |> 334 Local_Defs.unfold0 \<^context> [@{thm comp_def}] 335 336fun unfold_fun_maps ctm = 337 let 338 fun unfold_conv ctm = 339 case (Thm.term_of ctm) of 340 Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _ => 341 (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm 342 | _ => Conv.all_conv ctm 343 in 344 (Conv.fun_conv unfold_conv) ctm 345 end 346 347fun unfold_fun_maps_beta ctm = 348 let val try_beta_conv = Conv.try_conv (Thm.beta_conversion false) 349 in 350 (unfold_fun_maps then_conv try_beta_conv) ctm 351 end 352 353fun prove_rel ctxt rsp_thm (rty, qty) = 354 let 355 val ty_args = get_binder_types (rty, qty) 356 fun disch_arg args_ty thm = 357 let 358 val quot_thm = Lifting_Term.prove_quot_thm ctxt args_ty 359 in 360 [quot_thm, thm] MRSL @{thm apply_rsp''} 361 end 362 in 363 fold disch_arg ty_args rsp_thm 364 end 365 366exception CODE_CERT_GEN of string 367 368fun simplify_code_eq ctxt def_thm = 369 Local_Defs.unfold0 ctxt [@{thm o_apply}, @{thm map_fun_def}, @{thm id_apply}] def_thm 370 371(* 372 quot_thm - quotient theorem (Quotient R Abs Rep T). 373 returns: whether the Lifting package is capable to generate code for the abstract type 374 represented by quot_thm 375*) 376 377fun can_generate_code_cert quot_thm = 378 case quot_thm_rel quot_thm of 379 Const (\<^const_name>\<open>HOL.eq\<close>, _) => true 380 | Const (\<^const_name>\<open>eq_onp\<close>, _) $ _ => true 381 | _ => false 382 383fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) = 384 let 385 val unfolded_def = Conv.fconv_rule (Conv.arg_conv unfold_fun_maps_beta) def_thm 386 val unabs_def = unabs_all_def ctxt unfolded_def 387 in 388 if body_type rty = body_type qty then 389 SOME (simplify_code_eq ctxt (HOLogic.mk_obj_eq unabs_def)) 390 else 391 let 392 val quot_thm = Lifting_Term.prove_quot_thm ctxt (get_body_types (rty, qty)) 393 val rel_fun = prove_rel ctxt rsp_thm (rty, qty) 394 val rep_abs_thm = [quot_thm, rel_fun] MRSL @{thm Quotient_rep_abs_eq} 395 in 396 case mono_eq_prover ctxt (hd (Thm.prems_of rep_abs_thm)) of 397 SOME mono_eq_thm => 398 let 399 val rep_abs_eq = mono_eq_thm RS rep_abs_thm 400 val rep = Thm.cterm_of ctxt (quot_thm_rep quot_thm) 401 val rep_refl = HOLogic.mk_obj_eq (Thm.reflexive rep) 402 val repped_eq = [rep_refl, HOLogic.mk_obj_eq unabs_def] MRSL @{thm cong} 403 val code_cert = [repped_eq, rep_abs_eq] MRSL trans 404 in 405 SOME (simplify_code_eq ctxt code_cert) 406 end 407 | NONE => NONE 408 end 409 end 410 411fun generate_abs_eq ctxt def_thm rsp_thm quot_thm = 412 let 413 val abs_eq_with_assms = 414 let 415 val (rty, qty) = quot_thm_rty_qty quot_thm 416 val rel = quot_thm_rel quot_thm 417 val ty_args = get_binder_types_by_rel rel (rty, qty) 418 val body_type = get_body_type_by_rel rel (rty, qty) 419 val quot_ret_thm = Lifting_Term.prove_quot_thm ctxt body_type 420 421 val rep_abs_folded_unmapped_thm = 422 let 423 val rep_id = [quot_thm, def_thm] MRSL @{thm Quotient_Rep_eq} 424 val ctm = Thm.dest_equals_lhs (Thm.cprop_of rep_id) 425 val unfolded_maps_eq = unfold_fun_maps ctm 426 val t1 = [quot_thm, def_thm, rsp_thm] MRSL @{thm Quotient_rep_abs_fold_unmap} 427 val prems_pat = (hd o Drule.cprems_of) t1 428 val insts = Thm.first_order_match (prems_pat, Thm.cprop_of unfolded_maps_eq) 429 in 430 unfolded_maps_eq RS (Drule.instantiate_normalize insts t1) 431 end 432 in 433 rep_abs_folded_unmapped_thm 434 |> fold (fn _ => fn thm => thm RS @{thm rel_funD2}) ty_args 435 |> (fn x => x RS (@{thm Quotient_rel_abs2} OF [quot_ret_thm])) 436 end 437 438 val prem_rels = get_binder_rels (quot_thm_rel quot_thm); 439 val proved_assms = prem_rels |> map (try_prove_refl_rel ctxt) 440 |> map_index (apfst (fn x => x + 1)) |> filter (is_some o snd) |> map (apsnd the) 441 |> map (apsnd (fn assm => assm RS @{thm ge_eq_refl})) 442 val abs_eq = fold_rev (fn (i, assm) => fn thm => assm RSN (i, thm)) proved_assms abs_eq_with_assms 443 in 444 simplify_code_eq ctxt abs_eq 445 end 446 447 448fun register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy = 449 let 450 fun no_abstr (t $ u) = no_abstr t andalso no_abstr u 451 | no_abstr (Abs (_, _, t)) = no_abstr t 452 | no_abstr (Const (name, _)) = not (Code.is_abstr thy name) 453 | no_abstr _ = true 454 fun is_valid_eq eqn = can (Code.assert_eqn thy) (mk_meta_eq eqn, true) 455 andalso no_abstr (Thm.prop_of eqn) 456 fun is_valid_abs_eq abs_eq = can (Code.assert_abs_eqn thy NONE) (mk_meta_eq abs_eq) 457 458 in 459 if is_valid_eq abs_eq_thm then 460 (ABS_EQ, Code.declare_default_eqns_global [(abs_eq_thm, true)] thy) 461 else 462 let 463 val (rty_body, qty_body) = get_body_types (rty, qty) 464 in 465 if rty_body = qty_body then 466 (REP_EQ, Code.declare_default_eqns_global [(the opt_rep_eq_thm, true)] thy) 467 else 468 if is_some opt_rep_eq_thm andalso is_valid_abs_eq (the opt_rep_eq_thm) 469 then 470 (REP_EQ, Code.declare_abstract_eqn_global (the opt_rep_eq_thm) thy) 471 else 472 (NONE_EQ, thy) 473 end 474 end 475 476local 477 fun no_no_code ctxt (rty, qty) = 478 if same_type_constrs (rty, qty) then 479 forall (no_no_code ctxt) (Targs rty ~~ Targs qty) 480 else 481 if Term.is_Type qty then 482 if Lifting_Info.is_no_code_type ctxt (Tname qty) then false 483 else 484 let 485 val (rty', rtyq) = Lifting_Term.instantiate_rtys ctxt (rty, qty) 486 val (rty's, rtyqs) = (Targs rty', Targs rtyq) 487 in 488 forall (no_no_code ctxt) (rty's ~~ rtyqs) 489 end 490 else 491 true 492 493 fun encode_code_eq ctxt abs_eq opt_rep_eq (rty, qty) = 494 let 495 fun mk_type typ = typ |> Logic.mk_type |> Thm.cterm_of ctxt |> Drule.mk_term 496 in 497 Conjunction.intr_balanced [abs_eq, (the_default TrueI opt_rep_eq), mk_type rty, mk_type qty] 498 end 499 500 exception DECODE 501 502 fun decode_code_eq thm = 503 if Thm.nprems_of thm > 0 then raise DECODE 504 else 505 let 506 val [abs_eq, rep_eq, rty, qty] = Conjunction.elim_balanced 4 thm 507 val opt_rep_eq = if Thm.eq_thm_prop (rep_eq, TrueI) then NONE else SOME rep_eq 508 fun dest_type typ = typ |> Drule.dest_term |> Thm.term_of |> Logic.dest_type 509 in 510 (abs_eq, opt_rep_eq, (dest_type rty, dest_type qty)) 511 end 512 513 structure Data = Generic_Data 514 ( 515 type T = code_eq option 516 val empty = NONE 517 val extend = I 518 fun merge _ = NONE 519 ); 520 521 fun register_encoded_code_eq thm thy = 522 let 523 val (abs_eq_thm, opt_rep_eq_thm, (rty, qty)) = decode_code_eq thm 524 val (code_eq, thy) = register_code_eq_thy abs_eq_thm opt_rep_eq_thm (rty, qty) thy 525 in 526 Context.theory_map (Data.put (SOME code_eq)) thy 527 end 528 handle DECODE => thy 529 530 val register_code_eq_attribute = Thm.declaration_attribute 531 (fn thm => Context.mapping (register_encoded_code_eq thm) I) 532 val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute) 533 534in 535 536fun register_code_eq abs_eq_thm opt_rep_eq_thm (rty, qty) lthy = 537 let 538 val encoded_code_eq = encode_code_eq lthy abs_eq_thm opt_rep_eq_thm (rty, qty) 539 in 540 if no_no_code lthy (rty, qty) then 541 let 542 val lthy' = lthy 543 |> (#2 oo Local_Theory.note) ((Binding.empty, [register_code_eq_attrib]), [encoded_code_eq]) 544 val opt_code_eq = Data.get (Context.Theory (Proof_Context.theory_of lthy')) 545 val code_eq = 546 if is_some opt_code_eq then the opt_code_eq 547 else UNKNOWN_EQ (* UNKNOWN_EQ means that we are in a locale and we do not know 548 which code equation is going to be used. This is going to be resolved at the 549 point when an interpretation of the locale is executed. *) 550 val lthy'' = lthy' 551 |> Local_Theory.declaration {syntax = false, pervasive = true} (K (Data.put NONE)) 552 in (code_eq, lthy'') end 553 else 554 (NONE_EQ, lthy) 555 end 556end 557 558(* 559 Defines an operation on an abstract type in terms of a corresponding operation 560 on a representation type. 561 562 var - a binding and a mixfix of the new constant being defined 563 qty - an abstract type of the new constant 564 rhs - a term representing the new constant on the raw level 565 rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'), 566 i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs" 567 par_thms - a parametricity theorem for rhs 568*) 569 570fun add_lift_def (config: config) (binding, mx) qty rhs rsp_thm par_thms lthy0 = 571 let 572 val rty = fastype_of rhs 573 val quot_thm = Lifting_Term.prove_quot_thm lthy0 (rty, qty) 574 val absrep_trm = quot_thm_abs quot_thm 575 val rty_forced = (domain_type o fastype_of) absrep_trm 576 val forced_rhs = force_rty_type lthy0 rty_forced rhs 577 val lhs = Free (Binding.name_of binding, qty) 578 val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) 579 val (_, prop') = Local_Defs.cert_def lthy0 (K []) prop 580 val (_, newrhs) = Local_Defs.abs_def prop' 581 val var = ((#notes config = false ? Binding.concealed) binding, mx) 582 val def_name = Thm.make_def_binding (#notes config) (#1 var) 583 584 val ((lift_const, (_ , def_thm)), lthy1) = lthy0 585 |> Local_Theory.define (var, ((def_name, []), newrhs)) 586 587 val transfer_rules = generate_transfer_rules lthy1 quot_thm rsp_thm def_thm par_thms 588 589 val abs_eq_thm = generate_abs_eq lthy1 def_thm rsp_thm quot_thm 590 val opt_rep_eq_thm = generate_rep_eq lthy1 def_thm rsp_thm (rty_forced, qty) 591 592 fun notes names = 593 let 594 val lhs_name = Binding.reset_pos (#1 var) 595 val rsp_thmN = Binding.qualify_name true lhs_name "rsp" 596 val abs_eq_thmN = Binding.qualify_name true lhs_name "abs_eq" 597 val rep_eq_thmN = Binding.qualify_name true lhs_name "rep_eq" 598 val transfer_ruleN = Binding.qualify_name true lhs_name "transfer" 599 val notes = 600 [(rsp_thmN, [], [rsp_thm]), 601 (transfer_ruleN, @{attributes [transfer_rule]}, transfer_rules), 602 (abs_eq_thmN, [], [abs_eq_thm])] 603 @ (case opt_rep_eq_thm of SOME rep_eq_thm => [(rep_eq_thmN, [], [rep_eq_thm])] | NONE => []) 604 in 605 if names then map (fn (name, attrs, thms) => ((name, []), [(thms, attrs)])) notes 606 else map_filter (fn (_, attrs, thms) => if null attrs then NONE 607 else SOME (Binding.empty_atts, [(thms, attrs)])) notes 608 end 609 val (code_eq, lthy2) = lthy1 610 |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) 611 val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm 612 opt_rep_eq_thm code_eq transfer_rules 613 in 614 lthy2 615 |> Local_Theory.open_target |> snd 616 |> Local_Theory.notes (notes (#notes config)) |> snd 617 |> `(fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def) 618 ||> Local_Theory.close_target 619 end 620 621(* This is not very cheap way of getting the rules but we have only few active 622 liftings in the current setting *) 623fun get_cr_pcr_eqs ctxt = 624 let 625 fun collect (data : Lifting_Info.quotient) l = 626 if is_some (#pcr_info data) 627 then ((Thm.symmetric o safe_mk_meta_eq o Thm.transfer' ctxt o #pcr_cr_eq o the o #pcr_info) data :: l) 628 else l 629 val table = Lifting_Info.get_quotients ctxt 630 in 631 Symtab.fold (fn (_, data) => fn l => collect data l) table [] 632 end 633 634fun prepare_lift_def add_lift_def var qty rhs par_thms ctxt = 635 let 636 val rsp_rel = Lifting_Term.equiv_relation ctxt (fastype_of rhs, qty) 637 val rty_forced = (domain_type o fastype_of) rsp_rel; 638 val forced_rhs = force_rty_type ctxt rty_forced rhs; 639 val cr_to_pcr_conv = HOLogic.Trueprop_conv (Conv.fun2_conv 640 (Raw_Simplifier.rewrite ctxt false (get_cr_pcr_eqs ctxt))) 641 val (prsp_tm, rsp_prsp_eq) = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs) 642 |> Thm.cterm_of ctxt 643 |> cr_to_pcr_conv 644 |> `Thm.concl_of 645 |>> Logic.dest_equals 646 |>> snd 647 val to_rsp = rsp_prsp_eq RS Drule.equal_elim_rule2 648 val opt_proven_rsp_thm = try_prove_reflexivity ctxt prsp_tm 649 650 fun after_qed internal_rsp_thm = 651 add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms 652 in 653 case opt_proven_rsp_thm of 654 SOME thm => (NONE, K (after_qed thm)) 655 | NONE => (SOME prsp_tm, after_qed) 656 end 657 658fun gen_lift_def add_lift_def var qty rhs tac par_thms lthy = 659 let 660 val (goal, after_qed) = prepare_lift_def add_lift_def var qty rhs par_thms lthy 661 in 662 case goal of 663 SOME goal => 664 let 665 val rsp_thm = 666 Goal.prove_sorry lthy [] [] goal (tac o #context) 667 |> Thm.close_derivation \<^here> 668 in 669 after_qed rsp_thm lthy 670 end 671 | NONE => after_qed Drule.dummy_thm lthy 672 end 673 674val lift_def = gen_lift_def o add_lift_def 675 676end (* structure *) 677