# HG changeset patch
# User wenzelm
# Date 1702057231 -3600
# Node ID 35ead2206eb1a9b40aa90b9e21c9e5d9f2325446
# Parent  5ed6f16a5f7c492bb77a952fa0d805a90e08ccf0
more zproofs;

diff -r 5ed6f16a5f7c -r 35ead2206eb1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Dec 08 18:39:58 2023 +0100
+++ b/src/Pure/thm.ML	Fri Dec 08 18:40:31 2023 +0100
@@ -2055,8 +2055,9 @@
         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 (prf, ZTerm.todo_proof) der,
+        Thm (deriv_rule1 (prf, zprf) der,
          {tags = [],
           maxidx = Envir.maxidx_of env,
           constraints = insert_constraints_env thy' env constraints,
@@ -2092,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 5ed6f16a5f7c -r 35ead2206eb1 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Fri Dec 08 18:39:58 2023 +0100
+++ b/src/Pure/zterm.ML	Fri Dec 08 18:40:31 2023 +0100
@@ -198,6 +198,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 =
@@ -755,4 +756,26 @@
       (mk_ZAppP (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
+    mk_ZAbsP (map normt Bs)
+      (mk_ZAppP (prf, map ZBoundP (length Bs - 1 downto 0) @ [mk_asm_prf (normt Bi) n ~1]))
+    |> Same.commit (norm_proof_same cache envir)
+  end;
+
 end;