--- a/src/Pure/thm.ML Wed Dec 06 19:54:38 2023 +0100
+++ b/src/Pure/thm.ML Wed Dec 06 20:16:23 2023 +0100
@@ -2115,8 +2115,11 @@
let val (ps, qs) = chop m asms
in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
else raise THM ("rotate_rule", k, [state]);
+
+ fun prf p = Proofterm.rotate_proof Bs Bi' params asms m p;
+ fun zprf p = ZTerm.rotate_proof (Context.certificate_theory cert) Bs Bi' params asms m p;
in
- Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m, ZTerm.todo_proof) der,
+ Thm (deriv_rule1 (prf, zprf) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -2149,8 +2152,11 @@
val prems' = fixed_prems @ qs @ ps;
in (prems', Logic.list_implies (prems', concl)) end
else raise THM ("permute_prems: k", k, [rl]);
+
+ fun prf p = Proofterm.permute_prems_proof prems' j m p;
+ fun zprf p = ZTerm.permute_prems_proof (Context.certificate_theory cert) prems' j m p;
in
- Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m, ZTerm.todo_proof) der,
+ Thm (deriv_rule1 (prf, zprf) der,
{cert = cert,
tags = [],
maxidx = maxidx,
--- a/src/Pure/zterm.ML Wed Dec 06 19:54:38 2023 +0100
+++ b/src/Pure/zterm.ML Wed Dec 06 20:16:23 2023 +0100
@@ -186,6 +186,9 @@
val varifyT_proof: ((string * sort) * (indexname * sort)) list -> zproof -> zproof
val legacy_freezeT_proof: term -> zproof -> zproof
val incr_indexes_proof: int -> zproof -> zproof
+ 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
end;
structure ZTerm: ZTERM =
@@ -205,6 +208,15 @@
| (a1, a2) => a1 = a2);
+(* 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 mk_ZAppt = Library.foldl ZAppt;
+val mk_ZAppP = Library.foldl ZAppP;
+
+
(* map structure *)
fun subst_type_same tvar =
@@ -571,4 +583,30 @@
val term = subst_term_same typ var;
in Same.commit (map_proof_same typ term) prf end;
+
+(* permutations *)
+
+fun rotate_proof thy Bs Bi' params asms m prf =
+ let
+ val ztyp = ztyp_of;
+ val zterm = global_zterm_of thy;
+
+ 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))))))]))
+ end;
+
+fun permute_prems_proof thy prems' j k prf =
+ let
+ val zterm = global_zterm_of 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))))
+ end;
+
end;