# HG changeset patch
# User wenzelm
# Date 1519234901 -3600
# Node ID 67caf783b9eec34719206bca91a44ea3cafb39ab
# Parent  58f951ce71c884a4560019c7743c521e34c40024
explicit operations to instantiate frees: typ, term, thm, morphism;

diff -r 58f951ce71c8 -r 67caf783b9ee src/Pure/more_thm.ML
--- 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 =
diff -r 58f951ce71c8 -r 67caf783b9ee src/Pure/morphism.ML
--- 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
diff -r 58f951ce71c8 -r 67caf783b9ee src/Pure/term_subst.ML
--- 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