# HG changeset patch # User wenzelm # Date 1702150656 -3600 # Node ID 582dfbe9980e3ac53c3f78e3c8798766e8b71de4 # Parent f9d972b464c11b9dbf7143688557344cf7b9899b clarified signature: fewer tuples; diff -r f9d972b464c1 -r 582dfbe9980e src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Dec 09 20:05:13 2023 +0100 +++ b/src/Pure/thm.ML Sat Dec 09 20:37:36 2023 +0100 @@ -755,31 +755,32 @@ val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i); -fun deriv_rule2 (f, g) - (Deriv {promises = ps1, body = PBody body1}) (Deriv {promises = ps2, body = PBody body2}) = +fun deriv_rule2 zproof proof + (Deriv {promises = ps1, body = PBody body1}) + (Deriv {promises = ps2, body = PBody body2}) = let - val ps = Ord_List.union promise_ord ps1 ps2; + val ps' = Ord_List.union promise_ord ps1 ps2; val {oracles = oracles1, thms = thms1, zboxes = zboxes1, zproof = zprf1, proof = prf1} = body1; val {oracles = oracles2, thms = thms2, zboxes = zboxes2, zproof = zprf2, proof = prf2} = body2; - val oracles = Proofterm.union_oracles oracles1 oracles2; - val thms = Proofterm.union_thms thms1 thms2; - val zboxes = Proofterm.union_zboxes zboxes1 zboxes2; + val oracles' = Proofterm.union_oracles oracles1 oracles2; + val thms' = Proofterm.union_thms thms1 thms2; + val zboxes' = Proofterm.union_zboxes zboxes1 zboxes2; val proofs = Proofterm.get_proofs_level (); - val prf = if Proofterm.proof_enabled proofs then f prf1 prf2 else MinProof; - val zprf = if Proofterm.zproof_enabled proofs then g zprf1 zprf2 else ZDummy; - in make_deriv ps oracles thms zboxes zprf prf end; + val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZDummy; + val proof' = if Proofterm.proof_enabled proofs then proof prf1 prf2 else MinProof; + in make_deriv ps' oracles' thms' zboxes' zproof' proof' end; -fun deriv_rule1 (f, g) = deriv_rule2 (K f, K g) empty_deriv; +fun deriv_rule1 zproof proof = deriv_rule2 (K zproof) (K proof) empty_deriv; -fun deriv_rule0 (f, g) = +fun deriv_rule0 zproof proof = let val proofs = Proofterm.get_proofs_level () in if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then - deriv_rule1 (I, I) (make_deriv [] [] [] Proofterm.empty_zboxes - (if Proofterm.zproof_enabled proofs then g () else ZDummy) - (if Proofterm.proof_enabled proofs then f () else MinProof)) + deriv_rule1 I I (make_deriv [] [] [] Proofterm.empty_zboxes + (if Proofterm.zproof_enabled proofs then zproof () else ZDummy) + (if Proofterm.proof_enabled proofs then proof () else MinProof)) else empty_deriv end; @@ -864,15 +865,13 @@ (case Name_Space.lookup (Theory.axiom_table thy) name of SOME prop => let - val der = - deriv_rule0 - (fn () => Proofterm.axm_proof name prop, - fn () => ZTerm.axiom_proof thy name prop); + fun zproof () = ZTerm.axiom_proof thy name prop; + fun proof () = Proofterm.axm_proof name prop; val cert = Context.Certificate thy; val maxidx = maxidx_of_term prop; val shyps = Sorts.insert_term prop []; in - Thm (der, + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = maxidx, constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) end @@ -894,7 +893,7 @@ (* technical adjustments *) fun norm_proof (th as Thm (der, args)) = - Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th), I) der, args); + Thm (deriv_rule1 I (Proofterm.rew_proof (theory_of_thm th)) der, args); fun adjust_maxidx_thm i (th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = @@ -1213,10 +1212,10 @@ raise THM ("assume: variables", maxidx, []) else let - fun prf () = Proofterm.Hyp prop; - fun zprf () = ZTerm.assume_proof (Context.certificate_theory cert) prop; + fun zproof () = ZTerm.assume_proof (Context.certificate_theory cert) prop; + fun proof () = Proofterm.Hyp prop; in - Thm (deriv_rule0 (prf, zprf), + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = ~1, @@ -1243,10 +1242,10 @@ else let val cert = join_certificate1 (ct, th); - val prf = Proofterm.implies_intr_proof A; - fun zprf b = ZTerm.implies_intr_proof (Context.certificate_theory cert) A b; + fun zproof p = ZTerm.implies_intr_proof (Context.certificate_theory cert) A p; + fun proof p = Proofterm.implies_intr_proof A p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1274,7 +1273,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 ZAppp) (curry Proofterm.%%) der derA, {cert = join_certificate2 (thAB, thA), tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1308,10 +1307,10 @@ else let val cert = join_certificate1 (ct, th); - val prf = Proofterm.forall_intr_proof (a, x) NONE; - fun zprf p = ZTerm.forall_intr_proof (Context.certificate_theory cert) T (a, x) p; + fun zproof p = ZTerm.forall_intr_proof (Context.certificate_theory cert) T (a, x) p; + fun proof p = Proofterm.forall_intr_proof (a, x) NONE p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1343,9 +1342,10 @@ else let val cert = join_certificate1 (ct, th); - fun zprf p = ZTerm.forall_elim_proof (Context.certificate_theory cert) t p; + fun zproof p = ZTerm.forall_elim_proof (Context.certificate_theory cert) t p; + fun proof p = p % SOME t; in - Thm (deriv_rule1 (Proofterm.% o rpair (SOME t), zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1364,8 +1364,11 @@ t \ t *) fun reflexive (Cterm {cert, t, T, maxidx, sorts}) = - let fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t in - Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf), + let + fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t; + fun proof () = Proofterm.reflexive_proof; + in + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = maxidx, @@ -1384,8 +1387,8 @@ fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = (case prop of (eq as Const ("Pure.eq", Type ("fun", [T, _]))) $ t $ u => - let fun zprf prf = ZTerm.symmetric_proof (Context.certificate_theory cert) T t u prf in - Thm (deriv_rule1 (Proofterm.symmetric_proof, zprf) der, + let fun zproof p = ZTerm.symmetric_proof (Context.certificate_theory cert) T t u p in + Thm (deriv_rule1 zproof Proofterm.symmetric_proof der, {cert = cert, tags = [], maxidx = maxidx, @@ -1416,10 +1419,10 @@ else let val cert = join_certificate2 (th1, th2); - fun zprf prf1 prf2 = - ZTerm.transitive_proof (Context.certificate_theory cert) T t1 u t2 prf1 prf2; + fun zproof p q = ZTerm.transitive_proof (Context.certificate_theory cert) T t1 u t2 p q; + fun proof p = Proofterm.transitive_proof T u p; in - Thm (deriv_rule2 (Proofterm.transitive_proof T u, zprf) der1 der2, + Thm (deriv_rule2 zproof proof der1 der2, {cert = cert, tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1443,9 +1446,10 @@ else (case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt) | _ => raise THM ("beta_conversion: not a redex", 0, [])); - fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t; + fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t; + fun proof () = Proofterm.reflexive_proof; in - Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf), + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = maxidx, @@ -1457,8 +1461,11 @@ end; fun eta_conversion (Cterm {cert, t, T, maxidx, sorts}) = - let fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t in - Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf), + let + fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t; + fun proof () = Proofterm.reflexive_proof; + in + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = maxidx, @@ -1470,8 +1477,11 @@ end; fun eta_long_conversion (Cterm {cert, t, T, maxidx, sorts}) = - let fun zprf () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t in - Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, zprf), + let + fun zproof () = ZTerm.reflexive_proof (Context.certificate_theory cert) T t; + fun proof () = Proofterm.reflexive_proof; + in + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = maxidx, @@ -1503,10 +1513,11 @@ let val f = Abs (b, T, abstract_over (x, t)); val g = Abs (b, T, abstract_over (x, u)); - fun zprf prf = - ZTerm.abstract_rule_proof (Context.certificate_theory cert) T U (b, x) f g prf; + fun zproof p = + ZTerm.abstract_rule_proof (Context.certificate_theory cert) T U (b, x) f g p; + fun proof p = Proofterm.abstract_rule_proof (b, x) p in - Thm (deriv_rule1 (Proofterm.abstract_rule_proof (b, x), zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = maxidx, @@ -1546,10 +1557,11 @@ else raise THM ("combination: types", 0, [th1, th2]) | _ => raise THM ("combination: not function type", 0, [th1, th2])); val cert = join_certificate2 (th1, th2); - fun zprf prf1 prf2 = - ZTerm.combination_proof (Context.certificate_theory cert) fT U f g t u prf1 prf2; + fun zproof p q = + ZTerm.combination_proof (Context.certificate_theory cert) fT U f g t u p q; + fun proof p q = Proofterm.combination_proof f g t u p q; in - Thm (deriv_rule2 (Proofterm.combination_proof f g t u, zprf) der1 der2, + Thm (deriv_rule2 zproof proof der1 der2, {cert = cert, tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1580,10 +1592,10 @@ if A aconv A' andalso B aconv B' then let val cert = join_certificate2 (th1, th2); - fun zprf prf1 prf2 = - ZTerm.equal_intr_proof (Context.certificate_theory cert) A B prf1 prf2; + fun proof p q = Proofterm.equal_intr_proof A B p q; + fun zproof p q = ZTerm.equal_intr_proof (Context.certificate_theory cert) A B p q; in - Thm (deriv_rule2 (Proofterm.equal_intr_proof A B, zprf) der1 der2, + Thm (deriv_rule2 zproof proof der1 der2, {cert = cert, tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1615,10 +1627,10 @@ if prop2 aconv A then let val cert = join_certificate2 (th1, th2); - fun zprf prf1 prf2 = - ZTerm.equal_elim_proof (Context.certificate_theory cert) A B prf1 prf2; + fun proof p q = Proofterm.equal_elim_proof A B p q; + fun zproof p q = ZTerm.equal_elim_proof (Context.certificate_theory cert) A B p q; in - Thm (deriv_rule2 (Proofterm.equal_elim_proof A B, zprf) der1 der2, + Thm (deriv_rule2 zproof proof der1 der2, {cert = cert, tags = [], maxidx = Int.max (maxidx1, maxidx2), @@ -1658,10 +1670,10 @@ val thy' = Context.certificate_theory cert' handle ERROR msg => raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt); - fun prf p = Proofterm.norm_proof_remove_types env p; - fun zprf p = ZTerm.norm_proof thy' env p; + fun zproof p = ZTerm.norm_proof thy' env p; + fun proof p = Proofterm.norm_proof_remove_types env p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert', tags = [], maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'), @@ -1704,10 +1716,10 @@ val tpairs' = map (apply2 generalize) tpairs; val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop'); - val prf = Proofterm.generalize_proof (tfrees, frees) idx prop; - val zprf = ZTerm.generalize_proof (tfrees, frees) idx; + val zproof = ZTerm.generalize_proof (tfrees, frees) idx; + val proof = Proofterm.generalize_proof (tfrees, frees) idx prop; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = maxidx', @@ -1812,14 +1824,14 @@ TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints; - fun prf p = - Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') p; - fun zprf p = + fun zproof p = ZTerm.instantiate_proof thy' (TVars.fold (fn (v, (T, _)) => cons (v, T)) instT' [], Vars.fold (fn (v, (t, _)) => cons (v, t)) inst' []) p; + fun proof p = + Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert', tags = [], maxidx = maxidx', @@ -1860,8 +1872,11 @@ if T <> propT then raise THM ("trivial: the term must have type prop", 0, []) else - let fun zprf () = ZTerm.trivial_proof (Context.certificate_theory cert) A in - Thm (deriv_rule0 (fn () => Proofterm.trivial_proof, zprf), + let + fun zproof () = ZTerm.trivial_proof (Context.certificate_theory cert) A; + fun proof () = Proofterm.trivial_proof; + in + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = maxidx, @@ -1884,9 +1899,12 @@ handle ERROR msg => raise CONTEXT (msg, [cT], [], [], NONE); val c = Sign.certify_class thy raw_c; val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c)); + + fun zproof () = ZTerm.of_class_proof (T, c); + fun proof () = Proofterm.PClass (T, c); in if Sign.of_sort thy (T, [c]) then - Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c), fn () => ZTerm.of_class_proof (T, c)), + Thm (deriv_rule0 zproof proof, {cert = cert, tags = [], maxidx = maxidx, @@ -1938,8 +1956,10 @@ val prop1 = attach_tpairs tpairs prop; val (al, prop2) = Type.varify_global tfrees prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); + fun zproof p = ZTerm.varifyT_proof al p; + fun proof p = Proofterm.varifyT_proof al p; in - (al, Thm (deriv_rule1 (Proofterm.varifyT_proof al, ZTerm.varifyT_proof al) der, + (al, Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = Int.max (0, maxidx), @@ -1958,10 +1978,10 @@ val prop1 = attach_tpairs tpairs prop; val prop2 = Type.legacy_freeze prop1; val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); - fun prf p = Proofterm.legacy_freezeT prop1 p; - fun zprf p = ZTerm.legacy_freezeT_proof prop1 p; + fun zproof p = ZTerm.legacy_freezeT_proof prop1 p; + fun proof p = Proofterm.legacy_freezeT prop1 p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = maxidx_of_term prop2, @@ -2010,30 +2030,40 @@ in if T <> propT then raise THM ("lift_rule: the term must have type prop", 0, []) else - Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop, ZTerm.todo_proof) der, - {cert = join_certificate1 (goal, orule), - tags = [], - maxidx = maxidx + inc, - constraints = constraints, - shyps = Sorts.union shyps sorts, (*sic!*) - hyps = hyps, - tpairs = map (apply2 lift_abs) tpairs, - prop = Logic.list_implies (map lift_all As, lift_all B)}) + let + fun zproof p = ZTerm.todo_proof p; + fun proof p = Proofterm.lift_proof gprop inc prop p; + in + Thm (deriv_rule1 zproof proof der, + {cert = join_certificate1 (goal, orule), + tags = [], + maxidx = maxidx + inc, + constraints = constraints, + shyps = Sorts.union shyps sorts, (*sic!*) + hyps = hyps, + tpairs = map (apply2 lift_abs) tpairs, + prop = Logic.list_implies (map lift_all As, lift_all B)}) + end end; fun incr_indexes i (thm as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) = if i < 0 then raise THM ("negative increment", 0, [thm]) else if i = 0 then thm else - Thm (deriv_rule1 (Proofterm.incr_indexes i, ZTerm.incr_indexes_proof i) der, - {cert = cert, - tags = [], - maxidx = maxidx + i, - constraints = constraints, - shyps = shyps, - hyps = hyps, - tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs, - prop = Logic.incr_indexes ([], [], i) prop}); + let + fun zproof p = ZTerm.incr_indexes_proof i p; + fun proof p = Proofterm.incr_indexes i p; + in + Thm (deriv_rule1 zproof proof der, + {cert = cert, + tags = [], + maxidx = maxidx + i, + constraints = constraints, + shyps = shyps, + hyps = hyps, + tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs, + prop = Logic.incr_indexes ([], [], i) prop}) + end; (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) fun assumption opt_ctxt i state = @@ -2046,12 +2076,12 @@ 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 = + fun zproof p = ZTerm.assumption_proof thy' env Bs Bi n p; + fun proof 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, zprf) der, + Thm (deriv_rule1 zproof proof der, {tags = [], maxidx = Envir.maxidx_of env, constraints = insert_constraints_env thy' env constraints, @@ -2088,11 +2118,11 @@ ~1 => raise THM ("eq_assumption", 0, [state]) | n => let - fun prf p = Proofterm.assumption_proof Bs Bi (n + 1) p; - fun zprf p = + fun zproof p = ZTerm.assumption_proof (Context.certificate_theory cert) Envir.init Bs Bi (n + 1) p; + fun proof p = Proofterm.assumption_proof Bs Bi (n + 1) p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = maxidx, @@ -2123,10 +2153,10 @@ 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; + fun zproof p = ZTerm.rotate_proof (Context.certificate_theory cert) Bs Bi' params asms m p; + fun proof p = Proofterm.rotate_proof Bs Bi' params asms m p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = maxidx, @@ -2160,10 +2190,10 @@ 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; + fun zproof p = ZTerm.permute_prems_proof (Context.certificate_theory cert) prems' j m p; + fun proof p = Proofterm.permute_prems_proof prems' j m p; in - Thm (deriv_rule1 (prf, zprf) der, + Thm (deriv_rule1 zproof proof der, {cert = cert, tags = [], maxidx = maxidx, @@ -2314,16 +2344,16 @@ val constraints' = union_constraints constraints1 constraints2 |> insert_constraints_env thy' env; - fun bicompose_proof prf1 prf2 = - Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) - prf1 prf2 + fun zproof p q = ZTerm.todo_proof p; + fun bicompose_proof p q = + Proofterm.bicompose_proof flatten (map normt Bs) (map normt As) A oldAs n (nlift+1) p q; + val proof = + if Envir.is_empty env then bicompose_proof + else if Envir.above env smax + then bicompose_proof o Proofterm.norm_proof_remove_types env + else Proofterm.norm_proof_remove_types env oo bicompose_proof; val th = - Thm (deriv_rule2 - (if Envir.is_empty env then bicompose_proof - else if Envir.above env smax - then bicompose_proof o Proofterm.norm_proof_remove_types env - else Proofterm.norm_proof_remove_types env oo bicompose_proof, - K ZTerm.todo_proof) rder' sder, + Thm (deriv_rule2 zproof proof rder' sder, {tags = [], maxidx = Envir.maxidx_of env, constraints = constraints', @@ -2340,10 +2370,11 @@ let val (As1, rder') = if not lifted then (As0, rder) else - let val rename = rename_bvars dpairs tpairs B As0 - in (map (rename strip_apply) As0, - deriv_rule1 (Proofterm.map_proof_terms (rename K) I, ZTerm.todo_proof) rder) - end; + let + val rename = rename_bvars dpairs tpairs B As0; + fun proof p = Proofterm.map_proof_terms (rename K) I p; + fun zproof p = ZTerm.todo_proof p; + in (map (rename strip_apply) As0, deriv_rule1 zproof proof rder) end; in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n) handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule])