# HG changeset patch
# User wenzelm
# Date 1702211980 -3600
# Node ID 99bc2dd4511121e4465a608a1689d15753b20427
# Parent  6ad172f08c4320871f38a5b08d21132379881532
more general Logic.incr_indexes_operation;
more special Logic.incr_indexes;

diff -r 6ad172f08c43 -r 99bc2dd45111 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -19,7 +19,7 @@
     val ps = Logic.strip_params (Thm.term_of cgoal);
     val Ts = map snd ps;
     val tinst' = map (fn (t, u) =>
-      (head_of (Logic.incr_indexes ([], Ts, j) t),
+      (head_of (Logic.incr_indexes (Ts, j) t),
        fold_rev Term.abs ps u)) tinst;
     val th' = instf
       (map (apsnd (Thm.ctyp_of ctxt)) tyinst')
diff -r 6ad172f08c43 -r 99bc2dd45111 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -61,7 +61,7 @@
   let
     val ctxt = Proof_Context.init_global thy
     val maxidx = fold (Term.maxidx_term o Thm.prop_of) intros ~1
-    val pats = map (Logic.incr_indexes ([], [], maxidx + 1)) pats
+    val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
     val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
     val result_pats = map Var (fold_rev Term.add_vars pats [])
     fun mk_fresh_name names =
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/Isar/code.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -1386,7 +1386,7 @@
       o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of
       o Thm.transfer thy;
     val args = args_of thm;
-    val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
+    val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
     fun matches_args args' =
       let
         val k = length args' - length args
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -101,7 +101,7 @@
         get_first (fn (_, (prems, (tm1, tm2))) =>
         let
           fun ren t = the_default t (Term.rename_abs tm1 tm t);
-          val inc = Logic.incr_indexes ([], [], maxidx_of_term tm + 1);
+          val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
           val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
           val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems;
           val env' = Envir.Envir
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -253,7 +253,9 @@
     val inc = Thm.maxidx_of st + 1;
     val lift_type = Logic.incr_tvar inc;
     fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T);
-    fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
+    val incr_indexes =
+      Same.commit (Logic.incr_indexes_operation {fixed = fixed, Ts = paramTs, inc = inc, level = 0});
+    fun lift_term t = fold_rev Term.absfree params (incr_indexes t);
 
     val inst_tvars' =
       TVars.build (inst_tvars |> fold (fn (((a, i), S), T) =>
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/logic.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -78,8 +78,9 @@
   val rlist_abs: (string * typ) list * term -> term
   val incr_tvar_same: int -> typ Same.operation
   val incr_tvar: int -> typ -> typ
-  val incr_indexes_same: string list * typ list * int -> term Same.operation
-  val incr_indexes: string list * typ list * int -> term -> term
+  val incr_indexes_operation: {fixed: string list, Ts: typ list, inc: int, level: int} ->
+    term Same.operation
+  val incr_indexes: typ list * int -> term -> term
   val lift_abs: int -> term -> term -> term
   val lift_all: int -> term -> term -> term
   val strip_assums_hyp: term -> term list
@@ -446,37 +447,40 @@
   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
 
 fun incr_tvar_same 0 = Same.same
-  | incr_tvar_same k = Term_Subst.map_atypsT_same
-      (fn TVar ((a, i), S) => TVar ((a, i + k), S)
+  | incr_tvar_same inc = Term_Subst.map_atypsT_same
+      (fn TVar ((a, i), S) => TVar ((a, i + inc), S)
         | _ => raise Same.SAME);
 
-fun incr_tvar k = Same.commit (incr_tvar_same k);
+fun incr_tvar inc = Same.commit (incr_tvar_same inc);
 
 (*For all variables in the term, increment indexnames and lift over the Us
     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
-fun incr_indexes_same ([], [], 0) = Same.same
-  | incr_indexes_same (fixed, Ts, k) =
-      let
-        val n = length Ts;
-        val incrT = incr_tvar_same k;
+fun incr_indexes_operation {fixed, Ts, inc, level} =
+  if null fixed andalso null Ts andalso inc = 0 then Same.same
+  else
+    let
+      val n = length Ts;
+      val incrT = incr_tvar_same inc;
 
-        fun incr lev (Var ((x, i), T)) =
-              combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
-          | incr lev (Free (x, T)) =
-              if member (op =) fixed x then
-                combound (Free (x, Ts ---> Same.commit incrT T), lev, n)
-              else Free (x, incrT T)
-          | incr lev (Abs (x, T, t)) =
-              (Abs (x, incrT T, Same.commit (incr (lev + 1)) t)
-                handle Same.SAME => Abs (x, T, incr (lev + 1) t))
-          | incr lev (t $ u) =
-              (incr lev t $ Same.commit (incr lev) u
-                handle Same.SAME => t $ incr lev u)
-          | incr _ (Const (c, T)) = Const (c, incrT T)
-          | incr _ (Bound _) = raise Same.SAME;
-      in incr 0 end;
+      fun incr lev (Var ((x, i), T)) =
+            combound (Var ((x, i + inc), Ts ---> Same.commit incrT T), lev, n)
+        | incr lev (Free (x, T)) =
+            if member (op =) fixed x then
+              combound (Free (x, Ts ---> Same.commit incrT T), lev, n)
+            else Free (x, incrT T)
+        | incr lev (Abs (x, T, t)) =
+            (Abs (x, incrT T, Same.commit (incr (lev + 1)) t)
+              handle Same.SAME => Abs (x, T, incr (lev + 1) t))
+        | incr lev (t $ u) =
+            (incr lev t $ Same.commit (incr lev) u
+              handle Same.SAME => t $ incr lev u)
+        | incr _ (Const (c, T)) = Const (c, incrT T)
+        | incr _ (Bound _) = raise Same.SAME;
+    in incr level end;
 
-fun incr_indexes arg = Same.commit (incr_indexes_same arg);
+fun incr_indexes (Ts, inc) =
+  if null Ts andalso inc = 0 then I
+  else Same.commit (incr_indexes_operation {fixed = [], Ts = Ts, inc = inc, level = 0});
 
 
 (* Lifting functions from subgoal and increment:
@@ -487,14 +491,14 @@
   let
     fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
       | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
-      | lift Ts _ t = incr_indexes ([], rev Ts, inc) t;
+      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   in lift [] end;
 
 fun lift_all inc =
   let
     fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
       | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
-      | lift Ts _ t = incr_indexes ([], rev Ts, inc) t;
+      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   in lift [] end;
 
 (*Strips assumptions in goal, yielding list of hypotheses.   *)
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/more_unify.ML
--- a/src/Pure/more_unify.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/more_unify.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -28,7 +28,7 @@
 
         val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
         val offset = maxidx + 1;
-        val pairs' = map (apfst (Logic.incr_indexes ([], [], offset))) pairs;
+        val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
         val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
 
         val pat_tvars = TVars.build (fold (TVars.add_tvars o #1) pairs');
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -1012,10 +1012,8 @@
     val typ = Logic.incr_tvar_same inc;
     val typs = Same.map_option (Same.map typ);
 
-    fun term Us Ts t =
-      fold (fn T => fn u => Abs ("", T, u)) Ts t
-      |> Logic.incr_indexes_same ([], Us, inc)
-      |> Term.strip_abs_body' (length Ts);
+    fun term Us Ts =
+      Logic.incr_indexes_operation {fixed = [], Ts = Us, inc = inc, level = length Ts};
 
     fun proof Us Ts (Abst (a, T, p)) =
           (Abst (a, Same.map_option typ T, Same.commit (proof Us (dummyT :: Ts)) p)
@@ -1051,8 +1049,10 @@
   in mk_AbsP prems (lift [] [] 0 0 gprop) end;
 
 fun incr_indexes i =
-  Same.commit (map_proof_terms_same
-    (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i));
+  Same.commit
+    (map_proof_terms_same
+      (Logic.incr_indexes_operation {fixed = [], Ts = [], inc = i, level = 0})
+      (Logic.incr_tvar_same i));
 
 
 (* proof by assumption *)
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/term.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -127,7 +127,6 @@
   val a_itselfT: typ
   val argument_type_of: term -> int -> typ
   val abs: string * typ -> term -> term
-  val strip_abs_body': int -> 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
@@ -402,10 +401,6 @@
 fun strip_abs_vars (Abs (a, T, t)) = strip_abs_vars t |> cons (a, T)
   | strip_abs_vars _ = [];
 
-fun strip_abs_body' 0 t = t
-  | strip_abs_body' n (Abs (_, _, t)) = strip_abs_body' (n - 1) t
-  | strip_abs_body' _ t = t;
-
 
 fun strip_qnt_body qnt =
   let
diff -r 6ad172f08c43 -r 99bc2dd45111 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Dec 10 12:54:52 2023 +0100
+++ b/src/Pure/thm.ML	Sun Dec 10 13:39:40 2023 +0100
@@ -380,7 +380,7 @@
 fun incr_indexes_cterm i (ct as Cterm {cert, t, T, maxidx, sorts}) =
   if i < 0 then raise CTERM ("negative increment", [ct])
   else if i = 0 then ct
-  else Cterm {cert = cert, t = Logic.incr_indexes ([], [], i) t,
+  else Cterm {cert = cert, t = Logic.incr_indexes ([], i) t,
     T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
 
 
@@ -2060,8 +2060,8 @@
         constraints = constraints,
         shyps = shyps,
         hyps = hyps,
-        tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs,
-        prop = Logic.incr_indexes ([], [], i) prop})
+        tpairs = map (apply2 (Logic.incr_indexes ([], i))) tpairs,
+        prop = Logic.incr_indexes ([], i) prop})
     end;
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)