--- a/src/Pure/drule.ML Fri Jul 24 22:29:06 2015 +0200
+++ b/src/Pure/drule.ML Sat Jul 25 21:37:09 2015 +0200
@@ -22,6 +22,7 @@
val implies_intr_list: cterm list -> thm -> thm
val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
thm -> thm
+ val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
val zero_var_indexes_list: thm list -> thm list
val zero_var_indexes: thm -> thm
val implies_intr_hyps: thm -> thm
@@ -739,6 +740,55 @@
fun instantiate_normalize instpair th =
Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
+(*instantiation with type-inference for variables*)
+fun infer_instantiate _ [] th = th
+ | infer_instantiate ctxt args th =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ val vars = Term.add_vars (Thm.full_prop_of th) [];
+ val dups = duplicates (eq_fst op =) vars;
+ val _ = null dups orelse
+ raise THM ("infer_instantiate: inconsistent types for variables " ^
+ commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups),
+ 0, [th]);
+ fun var_type xi =
+ (case AList.lookup (op =) vars xi of
+ SOME T => T
+ | NONE => raise THM ("infer_instantiate: no variable " ^ string_of_indexname xi, 0, [th]));
+
+ fun infer (xi, cu) (tyenv, maxidx) =
+ let
+ val T = var_type xi;
+ val U = Thm.typ_of_cterm cu;
+ val (tyenv', maxidx') =
+ Sign.typ_unify thy (T, U)
+ (tyenv, maxidx |> Integer.max (#2 xi) |> Integer.max (Thm.maxidx_of_cterm cu))
+ handle Type.TUNIFY =>
+ let
+ val t = Var (xi, T);
+ val u = Thm.term_of cu;
+ in
+ raise TYPE ("Ill-typed instantiation:\nType\n" ^
+ Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^
+ "\nof variable " ^
+ Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^
+ "\ncannot be unified with type\n" ^
+ Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ "\nof term " ^
+ Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
+ [T, U], [t, u])
+ end;
+ in (((xi, T), cu), (tyenv', maxidx')) end;
+
+ val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0);
+ val instT =
+ Vartab.fold (fn (xi, (S, T)) =>
+ cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv [];
+ val inst = args' |> map (fn ((xi, T), cu) =>
+ ((xi, Envir.norm_type tyenv T),
+ Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu)));
+ in instantiate_normalize (instT, inst) th end;
+
(*Left-to-right replacements: tpairs = [..., (vi, ti), ...].
Instantiates distinct Vars by terms, inferring type instantiations.*)
local