clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;

--- a/src/Pure/ML/ml_antiquotations.ML	Mon Oct 25 17:26:27 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon Oct 25 17:37:24 2021 +0200
@@ -243,14 +243,14 @@
     val instT = TVars.make (#1 insts);
     val instantiateT = Term_Subst.instantiateT instT;
     val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts));
-  in Term_Subst.instantiate (instT, inst) end;
+  in Term_Subst.instantiate_beta (instT, inst) end;
 
 fun instantiate_cterm (cinsts: cinsts) =
   let
     val cinstT = TVars.make (#1 cinsts);
     val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT);
     val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts));
-  in Thm.instantiate_cterm (cinstT, cinst) end;
+  in Thm.instantiate_beta_cterm (cinstT, cinst) end;
 
 
 local

--- a/src/Pure/term.ML	Mon Oct 25 17:26:27 2021 +0200
+++ b/src/Pure/term.ML	Mon Oct 25 17:37:24 2021 +0200
@@ -124,6 +124,7 @@
   val a_itselfT: typ
   val argument_type_of: term -> int -> typ
   val abs: string * typ -> term -> term
+  val args_of: term -> term list
   val add_tvar_namesT: typ -> indexname list -> indexname list
   val add_tvar_names: term -> indexname list -> indexname list
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
@@ -423,6 +424,10 @@
         |   stripc  x =  x
     in  stripc(u,[])  end;
 
+fun args_of u =
+    let fun args (f $ x) xs = args f (x :: xs)
+        |   args _ xs = xs
+    in args u [] end;
 
 (*maps   f(t1,...,tn)  to  f , which is never a combination*)
 fun head_of (f$t) = head_of f

--- a/src/Pure/term_subst.ML	Mon Oct 25 17:26:27 2021 +0200
+++ b/src/Pure/term_subst.ML	Mon Oct 25 17:37:24 2021 +0200
@@ -20,10 +20,14 @@
   val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
   val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
     term -> int -> term * int
+  val instantiate_beta_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
+    term -> int -> term * int
   val instantiateT_same: typ TVars.table -> typ Same.operation
   val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation
+  val instantiate_beta_same: typ TVars.table * term Vars.table -> term Same.operation
   val instantiateT: typ TVars.table -> typ -> typ
   val instantiate: typ TVars.table * term Vars.table -> term -> term
+  val instantiate_beta: typ TVars.table * term Vars.table -> term -> term
   val zero_var_indexes_inst: Name.context -> term list -> typ TVars.table * term Vars.table
   val zero_var_indexes: term -> term
   val zero_var_indexes_list: term list -> term list
@@ -171,9 +175,50 @@
           end
       | subst (Bound _) = raise Same.SAME
       | subst (Abs (x, T, t)) =
-          (Abs (x, substT T, Same.commit subst t)
+          (Abs (x, substT T, subst_commit t)
             handle Same.SAME => Abs (x, T, subst t))
-      | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+      | subst (t $ u) = (subst t $ subst_commit u handle Same.SAME => t $ subst u)
+    and subst_commit t = Same.commit subst t;
+  in subst tm end;
+
+(*version with local beta reduction*)
+fun inst_beta_same maxidx (instT, inst) tm =
+  let
+    fun maxify i = if i > ! maxidx then maxidx := i else ();
+
+    val substT = instT_same maxidx instT;
+
+    fun expand_head t =
+      (case Term.head_of t of
+        Var ((x, i), T) =>
+          let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+            (case Vars.lookup inst ((x, i), T') of
+              SOME (u, j) => (maxify j; SOME u)
+            | NONE => (maxify i; if same then NONE else SOME (Var ((x, i), T'))))
+          end
+      | _ => NONE);
+
+    fun subst t =
+      (case expand_head t of
+        NONE =>
+          (case t of
+            Const (c, T) => Const (c, substT T)
+          | Free (x, T) => Free (x, substT T)
+          | Var _ => raise Same.SAME
+          | Bound _ => raise Same.SAME
+          | Abs (x, T, b) =>
+              (Abs (x, substT T, subst_commit b)
+                handle Same.SAME => Abs (x, T, subst b))
+          | _ $ _ => subst_comb t)
+      | SOME (u as Abs _) => Term.betapplys (u, map subst_commit (Term.args_of t))
+      | SOME u => subst_head u t)
+    and subst_comb (t $ u) = (subst_comb t $ subst_commit u handle Same.SAME => t $ subst u)
+      | subst_comb (Var _) = raise Same.SAME
+      | subst_comb t = subst t
+    and subst_head h (t $ u) = subst_head h t $ subst_commit u
+      | subst_head h _ = h
+    and subst_commit t = Same.commit subst t;
+
   in subst tm end;
 
 in
@@ -186,6 +231,11 @@
   let val maxidx = Unsynchronized.ref i
   in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
 
+fun instantiate_beta_maxidx insts tm i =
+  let val maxidx = Unsynchronized.ref i
+  in (Same.commit (inst_beta_same maxidx insts) tm, ! maxidx) end;
+
+
 fun instantiateT_same instT ty =
   if TVars.is_empty instT then raise Same.SAME
   else instT_same (Unsynchronized.ref ~1) (no_indexesT instT) ty;
@@ -194,9 +244,17 @@
   if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
   else inst_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
 
+fun instantiate_beta_same (instT, inst) tm =
+  if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
+  else inst_beta_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
+
+
 fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty;
+
 fun instantiate inst tm = Same.commit (instantiate_same inst) tm;
 
+fun instantiate_beta inst tm = Same.commit (instantiate_beta_same inst) tm;
+
 end;
 
 

--- a/src/Pure/thm.ML	Mon Oct 25 17:26:27 2021 +0200
+++ b/src/Pure/thm.ML	Mon Oct 25 17:37:24 2021 +0200
@@ -157,7 +157,9 @@
   val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm
   val generalize_ctyp: Names.set -> int -> ctyp -> ctyp
   val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm
+  val instantiate_beta: ctyp TVars.table * cterm Vars.table -> thm -> thm
   val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm
+  val instantiate_beta_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm
   val trivial: cterm -> thm
   val of_class: ctyp * class -> thm
   val unconstrainT: thm -> thm
@@ -1675,7 +1677,7 @@
 (*Left-to-right replacements: ctpairs = [..., (vi, ti), ...].
   Instantiates distinct Vars by terms of same type.
   Does NOT normalize the resulting theorem!*)
-fun instantiate (instT, inst) th =
+fun gen_instantiate inst_fn (instT, inst) th =
   if TVars.is_empty instT andalso Vars.is_empty inst then th
   else
     let
@@ -1684,7 +1686,7 @@
         handle CONTEXT (msg, cTs, cts, ths, context) =>
           raise CONTEXT (msg, cTs, cts, th :: ths, context);
 
-      val subst = Term_Subst.instantiate_maxidx (instT', inst');
+      val subst = inst_fn (instT', inst');
       val (prop', maxidx1) = subst prop ~1;
       val (tpairs', maxidx') =
         fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
@@ -1708,19 +1710,25 @@
     end
     handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
 
-fun instantiate_cterm (instT, inst) ct =
+val instantiate = gen_instantiate Term_Subst.instantiate_maxidx;
+val instantiate_beta = gen_instantiate Term_Subst.instantiate_beta_maxidx;
+
+fun gen_instantiate_cterm inst_fn (instT, inst) ct =
   if TVars.is_empty instT andalso Vars.is_empty inst then ct
   else
     let
       val Cterm {cert, t, T, sorts, ...} = ct;
       val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts);
-      val subst = Term_Subst.instantiate_maxidx (instT', inst');
+      val subst = inst_fn (instT', inst');
       val substT = Term_Subst.instantiateT_maxidx instT';
       val (t', maxidx1) = subst t ~1;
       val (T', maxidx') = substT T maxidx1;
     in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
     handle TYPE (msg, _, _) => raise CTERM (msg, [ct]);
 
+val instantiate_cterm = gen_instantiate_cterm Term_Subst.instantiate_maxidx;
+val instantiate_beta_cterm = gen_instantiate_cterm Term_Subst.instantiate_beta_maxidx;
+
 end;