# 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;