# HG changeset patch
# User wenzelm
# Date 1701890183 -3600
# Node ID 53288743c2f00329d5f7ccc3ea633865a0848b6a
# Parent  e47db1e15a2215f46ae6427c55beda982639dfb1
more zproofs;

diff -r e47db1e15a22 -r 53288743c2f0 src/Pure/thm.ML
--- 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,
diff -r e47db1e15a22 -r 53288743c2f0 src/Pure/zterm.ML
--- 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;