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