435 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index |
435 (*Like RSN, but we rename apart only the type variables. Vars here typically have an index |
436 of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars |
436 of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars |
437 could then fail. See comment on mk_var.*) |
437 could then fail. See comment on mk_var.*) |
438 fun resolve_inc_tyvars thy tha i thb = |
438 fun resolve_inc_tyvars thy tha i thb = |
439 let |
439 let |
|
440 val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha |
440 fun aux tha thb = |
441 fun aux tha thb = |
441 let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha in |
442 case Thm.bicompose false (false, tha, nprems_of tha) i thb |
442 case Thm.bicompose false (false, tha, nprems_of tha) i thb |
443 |> Seq.list_of |> distinct Thm.eq_thm of |
443 |> Seq.list_of |> distinct Thm.eq_thm of |
444 [th] => th |
444 [th] => th |
445 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, |
445 | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, |
446 [tha, thb]) |
446 [tha, thb]) |
|
447 end |
|
448 in |
447 in |
449 aux tha thb |
448 aux tha thb |
450 handle TERM _ => |
449 handle TERM z => |
451 (* We could do it right the first time but this error occurs seldom |
450 (* We could do it right the first time but this error occurs seldom |
452 and we don't want to break existing proofs in subtle ways or slow |
451 and we don't want to break existing proofs in subtle ways or slow |
453 them down needlessly. *) |
452 them down needlessly. *) |
454 let |
453 case [] |> fold (Term.add_vars o prop_of) [tha, thb] |
455 val ctyp_pairs = |
454 |> AList.group (op =) |
456 [] |> fold (Term.add_vars o prop_of) [tha, thb] |
455 |> maps (fn ((s, _), T :: Ts) => |
457 |> AList.group (op =) |
456 map (fn T' => (Free (s, T), Free (s, T'))) Ts) |
458 |> maps (fn ((s, _), T :: Ts) => |
457 |> rpair (Envir.empty ~1) |
459 map (fn T' => (Free (s, T), Free (s, T'))) Ts) |
458 |-> fold (Pattern.unify thy) |
460 |> rpair (Envir.empty ~1) |
459 |> Envir.type_env |> Vartab.dest |
461 |-> fold (Pattern.unify thy) |
460 |> map (fn (x, (S, T)) => |
462 |> Envir.type_env |> Vartab.dest |
461 pairself (ctyp_of thy) (TVar (x, S), T)) of |
463 |> map (fn (x, (S, T)) => |
462 [] => raise TERM z |
464 pairself (ctyp_of thy) (TVar (x, S), T)) |
463 | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) |
465 val repair = instantiate (ctyp_pairs, []) |
|
466 in aux (repair tha) (repair thb) end |
|
467 end |
464 end |
468 |
465 |
469 fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = |
466 fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = |
470 let |
467 let |
471 val thy = ProofContext.theory_of ctxt |
468 val thy = ProofContext.theory_of ctxt |