--- a/src/Pure/more_thm.ML Wed Feb 21 18:37:04 2018 +0100
+++ b/src/Pure/more_thm.ML Wed Feb 21 18:41:41 2018 +0100
@@ -72,6 +72,7 @@
val forall_intr_name: string * cterm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
+ val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
val forall_intr_frees: thm -> thm
val unvarify_global: theory -> thm -> thm
@@ -406,6 +407,29 @@
end;
+(* instantiate frees *)
+
+fun instantiate_frees ([], []) th = th
+ | instantiate_frees (instT, inst) th =
+ let
+ val idx = Thm.maxidx_of th + 1;
+ fun index ((a, A), b) = (((a, idx), A), b);
+ val insts = (map index instT, map index inst);
+ val frees = (map (#1 o #1) instT, map (#1 o #1) inst);
+
+ val hyps = Thm.chyps_of th;
+ val inst_cterm =
+ Thm.generalize_cterm frees idx #>
+ Thm.instantiate_cterm insts;
+ in
+ th
+ |> fold_rev Thm.implies_intr hyps
+ |> Thm.generalize frees idx
+ |> Thm.instantiate insts
+ |> fold (elim_implies o Thm.assume o inst_cterm) hyps
+ end;
+
+
(* instantiate by left-to-right occurrence of variables *)
fun instantiate' cTs cts thm =
--- a/src/Pure/morphism.ML Wed Feb 21 18:37:04 2018 +0100
+++ b/src/Pure/morphism.ML Wed Feb 21 18:41:41 2018 +0100
@@ -42,6 +42,8 @@
val transfer_morphism': Proof.context -> morphism
val transfer_morphism'': Context.generic -> morphism
val trim_context_morphism: morphism
+ val instantiate_frees_morphism:
+ ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
val instantiate_morphism:
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
end;
@@ -127,6 +129,22 @@
val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
+
+(* instantiate *)
+
+fun instantiate_frees_morphism ([], []) = identity
+ | instantiate_frees_morphism (cinstT, cinst) =
+ let
+ val instT = map (apsnd Thm.typ_of) cinstT;
+ val inst = map (apsnd Thm.term_of) cinst;
+ in
+ morphism "instantiate_frees"
+ {binding = [],
+ typ = if null instT then [] else [Term_Subst.instantiateT_frees instT],
+ term = [Term_Subst.instantiate_frees (instT, inst)],
+ fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
+ end;
+
fun instantiate_morphism ([], []) = identity
| instantiate_morphism (cinstT, cinst) =
let
--- a/src/Pure/term_subst.ML Wed Feb 21 18:37:04 2018 +0100
+++ b/src/Pure/term_subst.ML Wed Feb 21 18:41:41 2018 +0100
@@ -17,6 +17,12 @@
val instantiate_maxidx:
((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
term -> int -> term * int
+ val instantiateT_frees_same: ((string * sort) * typ) list -> typ Same.operation
+ val instantiate_frees_same: ((string * sort) * typ) list * ((string * typ) * term) list ->
+ term Same.operation
+ val instantiateT_frees: ((string * sort) * typ) list -> typ -> typ
+ val instantiate_frees: ((string * sort) * typ) list * ((string * typ) * term) list ->
+ term -> term
val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
term Same.operation
@@ -92,6 +98,42 @@
fun generalize names i tm = Same.commit (generalize_same names i) tm;
+(* instantiation of free variables (types before terms) *)
+
+fun instantiateT_frees_same [] _ = raise Same.SAME
+ | instantiateT_frees_same instT ty =
+ let
+ fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
+ | subst (TFree v) =
+ (case AList.lookup (op =) instT v of
+ SOME T => T
+ | NONE => raise Same.SAME)
+ | subst _ = raise Same.SAME;
+ in subst ty end;
+
+fun instantiate_frees_same ([], []) _ = raise Same.SAME
+ | instantiate_frees_same (instT, inst) tm =
+ let
+ val substT = instantiateT_frees_same instT;
+ fun subst (Const (c, T)) = Const (c, substT T)
+ | subst (Free (x, T)) =
+ let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+ (case AList.lookup (op =) inst (x, T') of
+ SOME t => t
+ | NONE => if same then raise Same.SAME else Free (x, T'))
+ end
+ | subst (Var (xi, T)) = Var (xi, substT T)
+ | subst (Bound _) = raise Same.SAME
+ | subst (Abs (x, T, t)) =
+ (Abs (x, substT T, Same.commit subst t)
+ handle Same.SAME => Abs (x, T, subst t))
+ | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+ in subst tm end;
+
+fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty;
+fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm;
+
+
(* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
local