# HG changeset patch
# User wenzelm
# Date 1702065381 -3600
# Node ID 8857975b99a94682395b0daad612f5f660e48ed4
# Parent  a0e8efbcf18d25161711bf0b30729a15d5467db4# Parent  5073bbdfa2b86bec0ece9eaa0cfa209bc7dd1141
merged

diff -r a0e8efbcf18d -r 8857975b99a9 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -141,7 +141,7 @@
             (case head_of (strip_abs_body f) of
               Free (s, T) =>
                 let val T' = Logic.varifyT_global T in
-                  Abst (s, SOME T', Proofterm.prf_abstract_over
+                  Abst (s, SOME T', Proofterm.abstract_over
                     (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
                 end
             | _ => AbsP ("H", SOME p, prf)))
diff -r a0e8efbcf18d -r 8857975b99a9 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/envir.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -206,24 +206,23 @@
 
 in
 
-fun norm_type_same tyenv T =
-  if Vartab.is_empty tyenv then raise Same.SAME
-  else norm_type0 tyenv T;
+fun norm_type_same tyenv =
+  if Vartab.is_empty tyenv then Same.same
+  else norm_type0 tyenv;
 
-fun norm_types_same tyenv Ts =
-  if Vartab.is_empty tyenv then raise Same.SAME
-  else Same.map (norm_type0 tyenv) Ts;
+fun norm_types_same tyenv =
+  if Vartab.is_empty tyenv then Same.same
+  else Same.map (norm_type0 tyenv);
 
 fun norm_type tyenv = Same.commit (norm_type_same tyenv);
 
-fun norm_term_same (envir as Envir {tenv, tyenv, ...}) =
-  if Vartab.is_empty tyenv then norm_term1 tenv
-  else norm_term2 envir;
+fun norm_term_same (envir as Envir {tenv, tyenv, ...}) t =
+  if is_empty envir andalso not (Term.could_beta_contract t) then raise Same.SAME
+  else if Vartab.is_empty tyenv then norm_term1 tenv t else norm_term2 envir t;
 
 fun norm_term envir = Same.commit (norm_term_same envir);
 
-fun beta_norm t =
-  if Term.could_beta_contract t then norm_term init t else t;
+val beta_norm = norm_term init;
 
 end;
 
@@ -376,13 +375,13 @@
 
 in
 
-fun subst_type_same tyenv T =
-  if Vartab.is_empty tyenv then raise Same.SAME
-  else subst_type0 tyenv T;
+fun subst_type_same tyenv =
+  if Vartab.is_empty tyenv then Same.same
+  else subst_type0 tyenv;
 
-fun subst_term_types_same tyenv t =
-  if Vartab.is_empty tyenv then raise Same.SAME
-  else Term_Subst.map_types_same (subst_type0 tyenv) t;
+fun subst_term_types_same tyenv =
+  if Vartab.is_empty tyenv then Same.same
+  else Term_Subst.map_types_same (subst_type0 tyenv);
 
 fun subst_term_same (tyenv, tenv) =
   if Vartab.is_empty tenv then subst_term_types_same tyenv
diff -r a0e8efbcf18d -r 8857975b99a9 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/logic.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -450,7 +450,7 @@
       (fn TVar ((a, i), S) => TVar ((a, i + k), S)
         | _ => raise Same.SAME);
 
-fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
+fun incr_tvar k = Same.commit (incr_tvar_same k);
 
 (*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 *)
@@ -476,7 +476,7 @@
           | incr _ (Bound _) = raise Same.SAME;
       in incr 0 end;
 
-fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
+fun incr_indexes arg = Same.commit (incr_indexes_same arg);
 
 
 (* Lifting functions from subgoal and increment:
diff -r a0e8efbcf18d -r 8857975b99a9 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -103,7 +103,7 @@
   val maxidx_proof: proof -> int -> int
   val size_of_proof: proof -> int
   val change_types: typ list option -> proof -> proof
-  val prf_abstract_over: term -> proof -> proof
+  val abstract_over: term -> proof -> proof
   val incr_bv_same: int -> int -> int -> int -> proof Same.operation
   val incr_bv: int -> int -> int -> int -> proof -> proof
   val incr_boundvars: int -> int -> proof -> proof
@@ -616,27 +616,30 @@
     which must contain no loose bound variables.
   The resulting proof term is ready to become the body of an Abst.*)
 
-fun prf_abstract_over v =
+fun abstract_over v =
   let
-    fun abst' lev u = if v aconv u then Bound lev else
-      (case u of
-         Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t)
-       | f $ t => (abst' lev f $ absth' lev t handle Same.SAME => f $ abst' lev t)
-       | _ => raise Same.SAME)
-    and absth' lev t = (abst' lev t handle Same.SAME => t);
+    fun term lev u =
+      if v aconv u then Bound lev
+      else
+        (case u of
+           Abs (a, T, t) => Abs (a, T, term (lev + 1) t)
+         | t $ u =>
+            (term lev t $ Same.commit (term lev) u
+              handle Same.SAME => t $ term lev u)
+         | _ => raise Same.SAME);
 
-    fun abst lev (AbsP (a, t, prf)) =
-          (AbsP (a, Same.map_option (abst' lev) t, absth lev prf)
-           handle Same.SAME => AbsP (a, t, abst lev prf))
-      | abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf)
-      | abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2
-          handle Same.SAME => prf1 %% abst lev prf2)
-      | abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t
-          handle Same.SAME => prf % Same.map_option (abst' lev) t)
-      | abst _ _ = raise Same.SAME
-    and absth lev prf = (abst lev prf handle Same.SAME => prf);
+    fun proof lev (AbsP (a, t, p)) =
+          (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
+           handle Same.SAME => AbsP (a, t, proof lev p))
+      | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
+      | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
+          handle Same.SAME => p %% proof lev q)
+      | proof lev (p % t) =
+          (proof lev p % Option.map (Same.commit (term lev)) t
+            handle Same.SAME => p % Same.map_option (term lev) t)
+      | proof _ _ = raise Same.SAME;
 
-  in absth 0 end;
+  in Same.commit (proof 0) end;
 
 
 (*increments a proof term's non-local bound variables
@@ -739,35 +742,35 @@
 
 in
 
-fun norm_proof env =
+fun norm_proof envir =
   let
-    val envT = Envir.type_env env;
+    val tyenv = Envir.type_env envir;
     fun msg s = warning ("type conflict in norm_proof:\n" ^ s);
-    fun norm_term_same t = Envir.norm_term_same env t handle TYPE (s, _, _) =>
-      (msg s; Envir.norm_term_same env (del_conflicting_vars env t));
-    fun norm_type_same T = Envir.norm_type_same envT T handle TYPE (s, _, _) =>
-      (msg s; Envir.norm_type_same envT (del_conflicting_tvars envT T));
-    fun norm_types_same Ts = Envir.norm_types_same envT Ts handle TYPE (s, _, _) =>
-      (msg s;  Envir.norm_types_same envT (map (del_conflicting_tvars envT) Ts));
+    fun norm_term_same t = Envir.norm_term_same envir t handle TYPE (s, _, _) =>
+      (msg s; Envir.norm_term_same envir (del_conflicting_vars envir t));
+    fun norm_type_same T = Envir.norm_type_same tyenv T handle TYPE (s, _, _) =>
+      (msg s; Envir.norm_type_same tyenv (del_conflicting_tvars tyenv T));
+    fun norm_types_same Ts = Envir.norm_types_same tyenv Ts handle TYPE (s, _, _) =>
+      (msg s;  Envir.norm_types_same tyenv (map (del_conflicting_tvars tyenv) Ts));
 
-    fun norm (Abst (s, T, prf)) =
-          (Abst (s, Same.map_option norm_type_same T, Same.commit norm prf)
-            handle Same.SAME => Abst (s, T, norm prf))
-      | norm (AbsP (s, t, prf)) =
-          (AbsP (s, Same.map_option norm_term_same t, Same.commit norm prf)
-            handle Same.SAME => AbsP (s, t, norm prf))
-      | norm (prf % t) =
-          (norm prf % Option.map (Same.commit norm_term_same) t
-            handle Same.SAME => prf % Same.map_option norm_term_same t)
-      | norm (prf1 %% prf2) =
-          (norm prf1 %% Same.commit norm prf2
-            handle Same.SAME => prf1 %% norm prf2)
-      | norm (PAxm (s, prop, Ts)) =
-          PAxm (s, prop, Same.map_option norm_types_same Ts)
+    fun norm (Abst (a, T, p)) =
+          (Abst (a, Same.map_option norm_type_same T, Same.commit norm p)
+            handle Same.SAME => Abst (a, T, norm p))
+      | norm (AbsP (a, t, p)) =
+          (AbsP (a, Same.map_option norm_term_same t, Same.commit norm p)
+            handle Same.SAME => AbsP (a, t, norm p))
+      | norm (p % t) =
+          (norm p % Option.map (Same.commit norm_term_same) t
+            handle Same.SAME => p % Same.map_option norm_term_same t)
+      | norm (p %% q) =
+          (norm p %% Same.commit norm q
+            handle Same.SAME => p %% norm q)
+      | norm (PAxm (a, prop, Ts)) =
+          PAxm (a, prop, Same.map_option norm_types_same Ts)
       | norm (PClass (T, c)) =
           PClass (norm_type_same T, c)
-      | norm (Oracle (s, prop, Ts)) =
-          Oracle (s, prop, Same.map_option norm_types_same Ts)
+      | norm (Oracle (a, prop, Ts)) =
+          Oracle (a, prop, Same.map_option norm_types_same Ts)
       | norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) =
           PThm (thm_header i p theory_name a t
             (Same.map_option norm_types_same Ts), thm_body)
@@ -793,27 +796,21 @@
 (* substitution of bound variables *)
 
 fun subst_bounds args prf =
-  let
-    val n = length args;
-    fun term lev (Bound i) =
-         (if i < lev then raise Same.SAME    (*var is locally bound*)
-          else if i - lev < n then Term.incr_boundvars lev (nth args (i - lev))
-          else Bound (i - n))  (*loose: change it*)
-      | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
-      | term lev (t $ u) = (term lev t $ Same.commit (term lev) u
-          handle Same.SAME => t $ term lev u)
-      | term _ _ = raise Same.SAME;
+  if null args then prf
+  else
+    let
+      val term = Term.subst_bounds_same args;
 
-    fun proof lev (AbsP (a, t, p)) =
-        (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
-          handle Same.SAME => AbsP (a, t, proof lev p))
-      | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
-      | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
-          handle Same.SAME => p %% proof lev q)
-      | proof lev (p % t) = (proof lev p % Option.map (Same.commit (term lev)) t
-          handle Same.SAME => p % Same.map_option (term lev) t)
-      | proof _ _ = raise Same.SAME;
-  in if null args then prf else Same.commit (proof 0) prf end;
+      fun proof lev (AbsP (a, t, p)) =
+          (AbsP (a, Same.map_option (term lev) t, Same.commit (proof lev) p)
+            handle Same.SAME => AbsP (a, t, proof lev p))
+        | proof lev (Abst (a, T, p)) = Abst (a, T, proof (lev + 1) p)
+        | proof lev (p %% q) = (proof lev p %% Same.commit (proof lev) q
+            handle Same.SAME => p %% proof lev q)
+        | proof lev (p % t) = (proof lev p % Option.map (Same.commit (term lev)) t
+            handle Same.SAME => p % Same.map_option (term lev) t)
+        | proof _ _ = raise Same.SAME;
+    in Same.commit (proof 0) prf end;
 
 fun subst_pbounds args prf =
   let
@@ -923,7 +920,7 @@
 
 (* forall introduction *)
 
-fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf);
+fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, abstract_over v prf);
 
 fun forall_intr_proof' v prf =
   let val (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T))
@@ -1011,47 +1008,45 @@
 
 fun lift_proof Bi inc prop prf =
   let
-    fun lift'' Us Ts t =
-      strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t));
+    val typ = Logic.incr_tvar_same inc;
+    val typs = Same.map_option (Same.map typ);
+
+    fun term Us Ts t =
+      strip_abs Ts (Logic.incr_indexes_same ([], Us, inc) (mk_abs Ts t));
 
-    fun lift' Us Ts (Abst (s, T, prf)) =
-          (Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf)
-           handle Same.SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
-      | lift' Us Ts (AbsP (s, t, prf)) =
-          (AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf)
-           handle Same.SAME => AbsP (s, t, lift' Us Ts prf))
-      | lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t
-          handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t)
-      | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
-          handle Same.SAME => prf1 %% lift' Us Ts prf2)
-      | lift' _ _ (PAxm (s, prop, Ts)) =
-          PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
-      | lift' _ _ (PClass (T, c)) =
-          PClass (Logic.incr_tvar_same inc T, c)
-      | lift' _ _ (Oracle (s, prop, Ts)) =
-          Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts)
-      | lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) =
-          PThm (thm_header i p theory_name s prop
-            ((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body)
-      | lift' _ _ _ = raise Same.SAME
-    and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf);
+    fun proof Us Ts (Abst (a, T, p)) =
+          (Abst (a, Same.map_option typ T, Same.commit (proof Us (dummyT :: Ts)) p)
+            handle Same.SAME => Abst (a, T, proof Us (dummyT :: Ts) p))
+      | proof Us Ts (AbsP (a, t, p)) =
+          (AbsP (a, Same.map_option (term Us Ts) t, Same.commit (proof Us Ts) p)
+            handle Same.SAME => AbsP (a, t, proof Us Ts p))
+      | proof Us Ts (p % t) =
+          (proof Us Ts p % Option.map (Same.commit (term Us Ts)) t
+            handle Same.SAME => p % Same.map_option (term Us Ts) t)
+      | proof Us Ts (p %% q) =
+          (proof Us Ts p %% Same.commit (proof Us Ts) q
+            handle Same.SAME => p %% proof Us Ts q)
+      | proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts)
+      | proof _ _ (PClass (T, c)) = PClass (typ T, c)
+      | proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts)
+      | proof _ _ (PThm ({serial, pos, theory_name, name, prop, types}, thm_body)) =
+          PThm (thm_header serial pos theory_name name prop (typs types), thm_body)
+      | proof _ _ _ = raise Same.SAME;
 
     val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
     val k = length ps;
 
     fun mk_app b (i, j, prf) =
-          if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
+      if b then (i - 1, j, prf %% PBound i) else (i, j - 1, prf %> Bound j);
 
     fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) =
-            AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
+          AbsP ("H", NONE (*A*), lift Us (true::bs) (i + 1) j B)
       | lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) =
-            Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
-      | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
-            map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
-              (i + k - 1 downto i));
-  in
-    mk_AbsP ps (lift [] [] 0 0 Bi)
-  end;
+          Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j + 1) t)
+      | lift Us bs i j _ =
+          proof_combP (Same.commit (proof (rev Us) []) prf,
+            map (fn k => (#3 (fold_rev mk_app bs (i - 1, j - 1, PBound k)))) (i + k - 1 downto i));
+  in mk_AbsP ps (lift [] [] 0 0 Bi) end;
 
 fun incr_indexes i =
   Same.commit (map_proof_terms_same
@@ -1060,14 +1055,14 @@
 
 (* proof by assumption *)
 
-fun mk_asm_prf t i m =
+fun mk_asm_prf C i m =
   let
     fun imp_prf _ i 0 = PBound i
       | imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m-1))
       | imp_prf _ i _ = PBound i;
     fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t)
       | all_prf t = imp_prf t (~i) m
-  in all_prf t end;
+  in all_prf C end;
 
 fun assumption_proof Bs Bi n prf =
   mk_AbsP Bs (proof_combP (prf, map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
diff -r a0e8efbcf18d -r 8857975b99a9 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/term.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -90,6 +90,7 @@
   val loose_bnos: term -> int list
   val loose_bvar: term * int -> bool
   val loose_bvar1: term * int -> bool
+  val subst_bounds_same: term list -> int -> term Same.operation
   val subst_bounds: term list * term -> term
   val subst_bound: term * term -> term
   val betapply: term * term -> term
@@ -704,22 +705,27 @@
   Loose bound variables >=n are reduced by "n" to
      compensate for the disappearance of lambdas.
 *)
-fun subst_bounds (args: term list, tm) : term =
-  let
-    val n = length args;
-    fun term lev (Bound i) =
-         (if i < lev then raise Same.SAME   (*var is locally bound*)
-          else if i - lev < n then incr_boundvars lev (nth args (i - lev))
-          else Bound (i - n))  (*loose: change it*)
-      | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
-      | term lev (t $ u) =
-          (term lev t $ Same.commit (term lev) u
-            handle Same.SAME => t $ term lev u)
-      | term _ _ = raise Same.SAME;
-  in if null args then tm else Same.commit (term 0) tm end;
+fun subst_bounds_same args =
+  if null args then fn _ => Same.same
+  else
+    let
+      val n = length args;
+      fun term lev (Bound i) =
+           (if i < lev then raise Same.SAME   (*var is locally bound*)
+            else if i - lev < n then incr_boundvars lev (nth args (i - lev))
+            else Bound (i - n))  (*loose: change it*)
+        | term lev (Abs (a, T, t)) = Abs (a, T, term (lev + 1) t)
+        | term lev (t $ u) =
+            (term lev t $ Same.commit (term lev) u
+              handle Same.SAME => t $ term lev u)
+        | term _ _ = raise Same.SAME;
+    in term end;
+
+fun subst_bounds (args: term list, body) : term =
+  if null args then body else Same.commit (subst_bounds_same args 0) body;
 
 (*Special case: one argument*)
-fun subst_bound (arg, tm) : term =
+fun subst_bound (arg, body) : term =
   let
     fun term lev (Bound i) =
           if i < lev then raise Same.SAME   (*var is locally bound*)
@@ -730,7 +736,7 @@
           (term lev t $ Same.commit (term lev) u
             handle Same.SAME => t $ term lev u)
       | term _ _ = raise Same.SAME;
-  in term 0 tm handle Same.SAME => tm end;
+  in Same.commit (term 0) body end;
 
 (*beta-reduce if possible, else form application*)
 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
@@ -780,16 +786,16 @@
   The resulting term is ready to become the body of an Abs.*)
 fun abstract_over (v, body) =
   let
-    fun abs lev tm =
+    fun term lev tm =
       if v aconv tm then Bound lev
       else
         (case tm of
-          Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
+          Abs (a, T, t) => Abs (a, T, term (lev + 1) t)
         | t $ u =>
-            (abs lev t $ (abs lev u handle Same.SAME => u)
-              handle Same.SAME => t $ abs lev u)
+            (term lev t $ Same.commit (term lev) u
+              handle Same.SAME => t $ term lev u)
         | _ => raise Same.SAME);
-  in abs 0 body handle Same.SAME => body end;
+  in Same.commit (term 0) body end;
 
 fun term_name (Const (x, _)) = Long_Name.base_name x
   | term_name (Free (x, _)) = x
diff -r a0e8efbcf18d -r 8857975b99a9 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/term_items.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -33,6 +33,7 @@
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
   val make_strict: (key * 'a) list -> 'a table
+  val unsynchronized_cache: (key -> 'a) -> key -> 'a
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
@@ -84,6 +85,8 @@
 
 fun make_strict es = Table (Table.make es);
 
+val unsynchronized_cache = Table.unsynchronized_cache;
+
 
 (* set with order of addition *)
 
diff -r a0e8efbcf18d -r 8857975b99a9 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/thm.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -1280,7 +1280,7 @@
     (case prop of
       Const ("Pure.imp", _) $ A $ B =>
         if A aconv propA then
-          Thm (deriv_rule2 (curry Proofterm.%%, curry ZAppP) der derA,
+          Thm (deriv_rule2 (curry Proofterm.%%, curry ZAppp) der derA,
            {cert = join_certificate2 (thAB, thA),
             tags = [],
             maxidx = Int.max (maxidx1, maxidx2),
@@ -1660,16 +1660,22 @@
               val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
                 (*remove trivial tpairs, of the form t \<equiv> t*)
                 |> filter_out (op aconv);
-              val der' = deriv_rule1 (Proofterm.norm_proof_remove_types env, ZTerm.todo_proof) der;
+              val prop' = Envir.norm_term env prop;
               val thy' = Context.certificate_theory cert' handle ERROR msg =>
                 raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
-              val constraints' = insert_constraints_env thy' env constraints;
-              val prop' = Envir.norm_term env prop;
-              val maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop');
-              val shyps = Envir.insert_sorts env shyps;
+
+              fun prf p = Proofterm.norm_proof_remove_types env p;
+              fun zprf p = ZTerm.norm_proof thy' env p;
             in
-              Thm (der', {cert = cert', tags = [], maxidx = maxidx, constraints = constraints',
-                shyps = shyps, hyps = hyps, tpairs = tpairs', prop = prop'})
+              Thm (deriv_rule1 (prf, zprf) der,
+               {cert = cert',
+                tags = [],
+                maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
+                constraints = insert_constraints_env thy' env constraints,
+                shyps = Envir.insert_sorts env shyps,
+                hyps = hyps,
+                tpairs = tpairs',
+                prop = prop'})
             end)
     end);
 
@@ -2043,15 +2049,15 @@
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     fun newth n (env, tpairs) =
       let
-        val normt = Envir.norm_term env;
-        fun assumption_proof prf =
-          Proofterm.assumption_proof (map normt Bs) (normt Bi) n prf;
         val thy' = Context.certificate_theory cert' handle ERROR msg =>
           raise CONTEXT (msg, [], [], [state], Option.map Context.Proof opt_ctxt);
+        val normt = Envir.norm_term env;
+        fun prf p =
+          Proofterm.assumption_proof (map normt Bs) (normt Bi) n p
+          |> not (Envir.is_empty env) ? Proofterm.norm_proof_remove_types env;
+        fun zprf p = ZTerm.assumption_proof thy' env Bs Bi n p;
       in
-        Thm (deriv_rule1
-          (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof_remove_types env,
-            ZTerm.todo_proof) der,
+        Thm (deriv_rule1 (prf, zprf) der,
          {tags = [],
           maxidx = Envir.maxidx_of env,
           constraints = insert_constraints_env thy' env constraints,
@@ -2059,7 +2065,8 @@
           hyps = hyps,
           tpairs = if Envir.is_empty env then tpairs else map (apply2 normt) tpairs,
           prop =
-            if Envir.is_empty env then Logic.list_implies (Bs, C) (*avoid wasted normalizations*)
+            if Envir.is_empty env
+            then Logic.list_implies (Bs, C) (*avoid wasted normalizations*)
             else normt (Logic.list_implies (Bs, C)) (*normalize the new rule fully*),
           cert = cert'})
       end;
@@ -2086,15 +2093,21 @@
     (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
       ~1 => raise THM ("eq_assumption", 0, [state])
     | n =>
-        Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1), ZTerm.todo_proof) der,
-         {cert = cert,
-          tags = [],
-          maxidx = maxidx,
-          constraints = constraints,
-          shyps = shyps,
-          hyps = hyps,
-          tpairs = tpairs,
-          prop = Logic.list_implies (Bs, C)}))
+        let
+          fun prf p = Proofterm.assumption_proof Bs Bi (n + 1) p;
+          fun zprf p =
+            ZTerm.assumption_proof (Context.certificate_theory cert) Envir.init Bs Bi (n + 1) p;
+        in
+          Thm (deriv_rule1 (prf, zprf) der,
+           {cert = cert,
+            tags = [],
+            maxidx = maxidx,
+            constraints = constraints,
+            shyps = shyps,
+            hyps = hyps,
+            tpairs = tpairs,
+            prop = Logic.list_implies (Bs, C)})
+        end)
   end;
 
 
diff -r a0e8efbcf18d -r 8857975b99a9 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Fri Dec 08 19:36:27 2023 +0100
+++ b/src/Pure/zterm.ML	Fri Dec 08 20:56:21 2023 +0100
@@ -135,14 +135,14 @@
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
-  | ZConstP of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
-  | ZBoundP of int
+  | ZConstp of zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table
+  | ZBoundp of int
   | ZHyp of zterm
   | ZAbst of string * ztyp * zproof
-  | ZAbsP of string * zterm * zproof
+  | ZAbsp of string * zterm * zproof
   | ZAppt of zproof * zterm
-  | ZAppP of zproof * zproof
-  | ZClassP of ztyp * class;       (*OFCLASS proof from sorts algebra*)
+  | ZAppp of zproof * zproof
+  | ZClassp of ztyp * class;       (*OFCLASS proof from sorts algebra*)
 
 
 
@@ -158,6 +158,15 @@
   val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
   val ztyp_ord: ztyp * ztyp -> order
   val aconv_zterm: zterm * zterm -> bool
+  val ZAbsts: (string * ztyp) list -> zproof -> zproof
+  val ZAbsps: zterm list -> zproof -> zproof
+  val ZAppts: zproof * zterm list -> zproof
+  val ZAppps: zproof * zproof list -> zproof
+  val fold_proof_terms: (zterm -> 'a -> 'a) -> zproof -> 'a -> 'a
+  val exists_proof_terms: (zterm -> bool) -> zproof -> bool
+  val incr_bv_same: int -> int -> zterm Same.operation
+  val incr_bv: int -> int -> zterm -> zterm
+  val incr_boundvars: int -> zterm -> zterm
   val ztyp_of: typ -> ztyp
   val zterm_cache_consts: Consts.T -> {zterm: term -> zterm, ztyp: typ -> ztyp}
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
@@ -165,6 +174,10 @@
   val typ_of: ztyp -> typ
   val term_of_consts: Consts.T -> zterm -> term
   val term_of: theory -> zterm -> term
+  val could_beta_contract: zterm -> bool
+  val norm_type: Type.tyenv -> ztyp -> ztyp
+  val norm_term: theory -> Envir.env -> zterm -> zterm
+  val norm_proof: theory -> Envir.env -> zproof -> zproof
   val dummy_proof: 'a -> zproof
   val todo_proof: 'a -> zproof
   val axiom_proof:  theory -> string -> term -> zproof
@@ -192,6 +205,7 @@
   val rotate_proof: theory -> term list -> term -> (string * typ) list ->
     term list -> int -> zproof -> zproof
   val permute_prems_proof: theory -> term list -> int -> int -> zproof -> zproof
+  val assumption_proof: theory -> Envir.env -> term list -> term -> int -> zproof -> zproof
 end;
 
 structure ZTerm: ZTERM =
@@ -213,14 +227,68 @@
 
 (* derived operations *)
 
-val mk_ZAbst = fold_rev (fn (x, T) => fn prf => ZAbst (x, T, prf));
-val mk_ZAbsP = fold_rev (fn t => fn prf => ZAbsP ("H", t, prf));
+val ZAbsts = fold_rev (fn (x, T) => fn prf => ZAbst (x, T, prf));
+val ZAbsps = fold_rev (fn t => fn prf => ZAbsp ("H", t, prf));
+
+val ZAppts = Library.foldl ZAppt;
+val ZAppps = Library.foldl ZAppp;
+
+
+(* fold *)
 
-val mk_ZAppt = Library.foldl ZAppt;
-val mk_ZAppP = Library.foldl ZAppP;
+fun fold_proof_terms f =
+  let
+    fun proof (ZConstp (_, _, _, inst)) = ZVars.fold (f o #2) inst
+      | proof (ZHyp t) = f t
+      | proof (ZAbst (_, _, p)) = proof p
+      | proof (ZAbsp (_, t, p)) = f t #> proof p
+      | proof (ZAppt (p, t)) = proof p #> f t
+      | proof (ZAppp (p, q)) = proof p #> proof q
+      | proof _ = I;
+  in proof end;
+
+local exception Found in
+
+fun exists_proof_terms P prf =
+  (fold_proof_terms (fn t => fn () => if P t then raise Found else ()) prf (); true)
+    handle Found => true;
+
+end;
 
 
-(* map structure *)
+(* substitution of bound variables *)
+
+fun incr_bv_same inc =
+  if inc = 0 then fn _ => Same.same
+  else
+    let
+      fun term lev (ZBound i) = if i >= lev then ZBound (i + inc) else raise Same.SAME
+        | term lev (ZAbs (a, T, t)) = ZAbs (a, T, term (lev + 1) t)
+        | term lev (ZApp (t, u)) =
+            (ZApp (term lev t, Same.commit (term lev) u) handle Same.SAME =>
+              ZApp (t, term lev u))
+        | term _ _ = raise Same.SAME;
+    in term end;
+
+fun incr_bv inc lev = Same.commit (incr_bv_same inc lev);
+
+fun incr_boundvars inc = incr_bv inc 0;
+
+fun subst_bound arg body =
+  let
+    fun term lev (ZBound i) =
+          if i < lev then raise Same.SAME   (*var is locally bound*)
+          else if i = lev then incr_boundvars lev arg
+          else ZBound (i - 1)   (*loose: change it*)
+      | term lev (ZAbs (a, T, t)) = ZAbs (a, T, term (lev + 1) t)
+      | term lev (ZApp (t, u)) =
+          (ZApp (term lev t, Same.commit (term lev) u)
+            handle Same.SAME => ZApp (t, term lev u))
+      | term _ _ = raise Same.SAME;
+  in Same.commit (term 0) body end;
+
+
+(* direct substitution *)
 
 fun subst_type_same tvar =
   let
@@ -287,20 +355,20 @@
 fun map_proof_same typ term =
   let
     fun proof ZDummy = raise Same.SAME
-      | proof (ZConstP (a, A, instT, inst)) =
+      | proof (ZConstp (a, A, instT, inst)) =
           let val (instT', inst') = map_insts_same typ term (instT, inst)
-          in ZConstP (a, A, instT', inst') end
-      | proof (ZBoundP _) = raise Same.SAME
+          in ZConstp (a, A, instT', inst') end
+      | proof (ZBoundp _) = raise Same.SAME
       | proof (ZHyp h) = ZHyp (term h)
       | proof (ZAbst (a, T, p)) =
           (ZAbst (a, typ T, Same.commit proof p) handle Same.SAME => ZAbst (a, T, proof p))
-      | proof (ZAbsP (a, t, p)) =
-          (ZAbsP (a, term t, Same.commit proof p) handle Same.SAME => ZAbsP (a, t, proof p))
+      | proof (ZAbsp (a, t, p)) =
+          (ZAbsp (a, term t, Same.commit proof p) handle Same.SAME => ZAbsp (a, t, proof p))
       | proof (ZAppt (p, t)) =
           (ZAppt (proof p, Same.commit term t) handle Same.SAME => ZAppt (p, term t))
-      | proof (ZAppP (p, q)) =
-          (ZAppP (proof p, Same.commit proof q) handle Same.SAME => ZAppP (p, proof q))
-      | proof (ZClassP (T, c)) = ZClassP (typ T, c);
+      | proof (ZAppp (p, q)) =
+          (ZAppp (proof p, Same.commit proof q) handle Same.SAME => ZAppp (p, proof q))
+      | proof (ZClassp (T, c)) = ZClassp (typ T, c);
   in proof end;
 
 fun map_proof_types_same typ =
@@ -352,6 +420,8 @@
   | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
   | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
 
+fun typ_cache () = ZTypes.unsynchronized_cache typ_of;
+
 fun term_of_consts consts =
   let
     val instance = Consts.instance consts;
@@ -370,6 +440,77 @@
 val term_of = term_of_consts o Sign.consts_of;
 
 
+(* beta normalization wrt. environment *)
+
+fun could_beta_contract (ZApp (ZAbs _, _)) = true
+  | could_beta_contract (ZApp (t, u)) = could_beta_contract t orelse could_beta_contract u
+  | could_beta_contract (ZAbs (_, _, b)) = could_beta_contract b
+  | could_beta_contract _ = false;
+
+fun norm_type_same ztyp tyenv =
+  if Vartab.is_empty tyenv then Same.same
+  else
+    let
+      fun norm (ZTVar v) =
+            (case Type.lookup tyenv v of
+              SOME U => Same.commit norm (ztyp U)
+            | NONE => raise Same.SAME)
+        | norm (ZFun (T, U)) =
+            (ZFun (norm T, Same.commit norm U)
+              handle Same.SAME => ZFun (T, norm U))
+        | norm ZProp = raise Same.SAME
+        | norm (ZItself T) = ZItself (norm T)
+        | norm (ZType0 _) = raise Same.SAME
+        | norm (ZType1 (a, T)) = ZType1 (a, norm T)
+        | norm (ZType (a, Ts)) = ZType (a, Same.map norm Ts);
+    in norm end;
+
+fun norm_term_same {ztyp, zterm, typ} (envir as Envir.Envir {tyenv, tenv, ...}) tm =
+  if Envir.is_empty envir andalso not (could_beta_contract tm) then raise Same.SAME
+  else
+    let
+      val lookup =
+        if Vartab.is_empty tenv then K NONE
+        else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm);
+
+      val normT = norm_type_same ztyp tyenv;
+
+      fun norm (ZVar (xi, T)) =
+            (case lookup (xi, T) of
+              SOME u => Same.commit norm u
+            | NONE => ZVar (xi, normT T))
+        | norm (ZBound _) = raise Same.SAME
+        | norm (ZConst0 _) = raise Same.SAME
+        | norm (ZConst1 (a, T)) = ZConst1 (a, normT T)
+        | norm (ZConst (a, Ts)) = ZConst (a, Same.map normT Ts)
+        | norm (ZAbs (a, T, t)) =
+            (ZAbs (a, normT T, Same.commit norm t)
+              handle Same.SAME => ZAbs (a, T, norm t))
+        | norm (ZApp (ZAbs (_, _, body), t)) = Same.commit norm (subst_bound t body)
+        | norm (ZApp (f, t)) =
+            ((case norm f of
+               ZAbs (_, _, body) => Same.commit norm (subst_bound t body)
+             | nf => ZApp (nf, Same.commit norm t))
+            handle Same.SAME => ZApp (f, norm t))
+        | norm _ = raise Same.SAME;
+    in norm tm end;
+
+fun norm_proof_same (cache as {ztyp, ...}) (envir as Envir.Envir {tyenv, ...}) prf =
+  if Envir.is_empty envir andalso not (exists_proof_terms could_beta_contract prf) then
+    raise Same.SAME
+  else map_proof_same (norm_type_same ztyp tyenv) (norm_term_same cache envir) prf;
+
+fun norm_cache thy =
+  let
+    val {ztyp, zterm} = zterm_cache_consts (Sign.consts_of thy);
+    val typ = typ_cache ();
+  in {ztyp = ztyp, zterm = zterm, typ = typ} end;
+
+fun norm_type tyenv = Same.commit (norm_type_same (ztyp_cache ()) tyenv);
+fun norm_term thy envir = Same.commit (norm_term_same (norm_cache thy) envir);
+fun norm_proof thy envir = Same.commit (norm_proof_same (norm_cache thy) envir);
+
+
 
 (** proof construction **)
 
@@ -390,15 +531,15 @@
         (case a of
           ZVar v => if ZVars.defined tab v then tab else ZVars.update (v, a) tab
         | _ => tab)));
-  in ZConstP (a, t, instT, inst) end;
+  in ZConstp (a, t, instT, inst) end;
 
 fun map_const_proof (f, g) prf =
   (case prf of
-    ZConstP (a, A, instT, inst) =>
+    ZConstp (a, A, instT, inst) =>
       let
         val instT' = ZTVars.map (fn ((x, _), _) => fn y => the_default y (try f x)) instT;
         val inst' = ZVars.map (fn ((x, _), _) => fn y => the_default y (try g x)) inst;
-      in ZConstP (a, A, instT', inst') end
+      in ZConstp (a, A, instT', inst') end
   | _ => prf);
 
 
@@ -414,20 +555,20 @@
   ZHyp (zterm_of thy A);
 
 fun trivial_proof thy A =
-  ZAbsP ("H", zterm_of thy A, ZBoundP 0);
+  ZAbsp ("H", zterm_of thy A, ZBoundp 0);
 
 fun implies_intr_proof thy A prf =
   let
     val h = zterm_of thy A;
-    fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundP i else raise Same.SAME
+    fun proof i (ZHyp t) = if aconv_zterm (h, t) then ZBoundp i else raise Same.SAME
       | proof i (ZAbst (x, T, p)) = ZAbst (x, T, proof i p)
-      | proof i (ZAbsP (x, t, p)) = ZAbsP (x, t, proof (i + 1) p)
+      | proof i (ZAbsp (x, t, p)) = ZAbsp (x, t, proof (i + 1) p)
       | proof i (ZAppt (p, t)) = ZAppt (proof i p, t)
-      | proof i (ZAppP (p, q)) =
-          (ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME =>
-            ZAppP (p, proof i q))
+      | proof i (ZAppp (p, q)) =
+          (ZAppp (proof i p, Same.commit (proof i) q) handle Same.SAME =>
+            ZAppp (p, proof i q))
       | proof _ _ = raise Same.SAME;
-  in ZAbsP ("H", h, Same.commit (proof 0) prf) end;
+  in ZAbsp ("H", h, Same.commit (proof 0) prf) end;
 
 fun forall_intr_proof thy T (a, x) prf =
   let
@@ -446,22 +587,22 @@
         | _ => raise Same.SAME);
 
     fun proof i (ZAbst (x, T, prf)) = ZAbst (x, T, proof (i + 1) prf)
-      | proof i (ZAbsP (x, t, prf)) =
-          (ZAbsP (x, term i t, Same.commit (proof i) prf) handle Same.SAME =>
-            ZAbsP (x, t, proof i prf))
+      | proof i (ZAbsp (x, t, prf)) =
+          (ZAbsp (x, term i t, Same.commit (proof i) prf) handle Same.SAME =>
+            ZAbsp (x, t, proof i prf))
       | proof i (ZAppt (p, t)) =
           (ZAppt (proof i p, Same.commit (term i) t) handle Same.SAME =>
             ZAppt (p, term i t))
-      | proof i (ZAppP (p, q)) =
-          (ZAppP (proof i p, Same.commit (proof i) q) handle Same.SAME =>
-            ZAppP (p, proof i q))
+      | proof i (ZAppp (p, q)) =
+          (ZAppp (proof i p, Same.commit (proof i) q) handle Same.SAME =>
+            ZAppp (p, proof i q))
       | proof _ _ = raise Same.SAME;
 
   in ZAbst (a, Z, Same.commit (proof 0) prf) end;
 
 fun forall_elim_proof thy t p = ZAppt (p, zterm_of thy t);
 
-fun of_class_proof (T, c) = ZClassP (ztyp_of T, c);
+fun of_class_proof (T, c) = ZClassp (ztyp_of T, c);
 
 
 (* equality *)
@@ -484,7 +625,7 @@
 in
 
 val is_reflexive_proof =
-  fn ZConstP (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false;
+  fn ZConstp (ZAxiom "Pure.reflexive", _, _, _) => true | _ => false;
 
 fun reflexive_proof thy T t =
   let
@@ -502,7 +643,7 @@
       val x = zterm t;
       val y = zterm u;
       val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y) symmetric_axiom;
-    in ZAppP (ax, prf) end;
+    in ZAppp (ax, prf) end;
 
 fun transitive_proof thy T t u v prf1 prf2 =
   if is_reflexive_proof prf1 then prf2
@@ -515,7 +656,7 @@
       val y = zterm u;
       val z = zterm v;
       val ax = map_const_proof (fn "'a" => A, fn "x" => x | "y" => y | "z" => z) transitive_axiom;
-    in ZAppP (ZAppP (ax, prf1), prf2) end;
+    in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun equal_intr_proof thy t u prf1 prf2 =
   let
@@ -523,7 +664,7 @@
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_intr_axiom;
-  in ZAppP (ZAppP (ax, prf1), prf2) end;
+  in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun equal_elim_proof thy t u prf1 prf2 =
   let
@@ -531,7 +672,7 @@
     val A = zterm t;
     val B = zterm u;
     val ax = map_const_proof (undefined, fn "A" => A | "B" => B) equal_elim_axiom;
-  in ZAppP (ZAppP (ax, prf1), prf2) end;
+  in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 fun abstract_rule_proof thy T U x t u prf =
   let
@@ -543,7 +684,7 @@
     val ax =
       map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f | "g" => g)
         abstract_rule_axiom;
-  in ZAppP (ax, forall_intr_proof thy T x prf) end;
+  in ZAppp (ax, forall_intr_proof thy T x prf) end;
 
 fun combination_proof thy T U f g t u prf1 prf2 =
   let
@@ -557,7 +698,7 @@
     val ax =
       map_const_proof (fn "'a" => A | "'b" => B, fn "f" => f' | "g" => g' | "x" => x | "y" => y)
         combination_axiom;
-  in ZAppP (ZAppP (ax, prf1), prf2) end;
+  in ZAppp (ZAppp (ax, prf1), prf2) end;
 
 end;
 
@@ -627,10 +768,10 @@
     val i = length asms;
     val j = length Bs;
   in
-    mk_ZAbsP (map zterm Bs @ [zterm Bi']) (mk_ZAppP (prf, map ZBoundP
-      (j downto 1) @ [mk_ZAbst (map (apsnd ztyp) params) (mk_ZAbsP (map zterm asms)
-        (mk_ZAppP (mk_ZAppt (ZBoundP i, map ZBound ((length params - 1) downto 0)),
-          map ZBoundP (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
+    ZAbsps (map zterm Bs @ [zterm Bi']) (ZAppps (prf, map ZBoundp
+      (j downto 1) @ [ZAbsts (map (apsnd ztyp) params) (ZAbsps (map zterm asms)
+        (ZAppps (ZAppts (ZBoundp i, map ZBound ((length params - 1) downto 0)),
+          map ZBoundp (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   end;
 
 fun permute_prems_proof thy prems' j k prf =
@@ -638,8 +779,30 @@
     val {zterm, ...} = zterm_cache thy;
     val n = length prems';
   in
-    mk_ZAbsP (map zterm prems')
-      (mk_ZAppP (prf, map ZBoundP ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+    ZAbsps (map zterm prems')
+      (ZAppps (prf, map ZBoundp ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
+  end;
+
+
+(* higher-order resolution *)
+
+fun mk_asm_prf C i m =
+  let
+    fun imp _ i 0 = ZBoundp i
+      | imp (ZApp (ZApp (ZConst0 "Pure.imp", A), B)) i m = ZAbsp ("H", A, imp B (i + 1) (m - 1))
+      | imp _ i _ = ZBoundp i;
+    fun all (ZApp (ZConst1 ("Pure.all", _), ZAbs (a, T, t))) = ZAbst (a, T, all t)
+      | all t = imp t (~ i) m
+  in all C end;
+
+fun assumption_proof thy envir Bs Bi n prf =
+  let
+    val cache as {zterm, ...} = norm_cache thy;
+    val normt = zterm #> Same.commit (norm_term_same cache envir);
+  in
+    ZAbsps (map normt Bs)
+      (ZAppps (prf, map ZBoundp (length Bs - 1 downto 0) @ [mk_asm_prf (normt Bi) n ~1]))
+    |> Same.commit (norm_proof_same cache envir)
   end;
 
 end;