--- a/src/Pure/proofterm.ML Sat Dec 09 17:31:10 2023 +0100
+++ b/src/Pure/proofterm.ML Sat Dec 09 20:05:13 2023 +0100
@@ -30,16 +30,15 @@
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
zboxes: zboxes,
- proof: proof * zproof}
- type proofs = proof * zproof
+ zproof: zproof,
+ proof: proof}
type oracle = (string * Position.T) * term option
type thm = serial * thm_node
exception MIN_PROOF of unit
- val proofs_of: proof_body -> proofs
+ val zproof_of: proof_body -> zproof
val proof_of: proof_body -> proof
- val zproof_of: proof_body -> zproof
val join_proof: proof_body future -> proof
- val map_proofs_of: (proofs -> proofs) -> proof_body -> proof_body
+ val map_proof_of: (proof -> proof) -> proof_body -> proof_body
val thm_header: serial -> Position.T list -> string -> string -> term -> typ list option ->
thm_header
val thm_body: proof_body -> thm_body
@@ -64,8 +63,7 @@
val unions_thms: thm Ord_List.T list -> thm Ord_List.T
val empty_zboxes: zboxes
val union_zboxes: zboxes -> zboxes -> zboxes
- val no_proof: proofs
- val no_proof_body: proofs -> proof_body
+ val no_proof_body: zproof -> proof -> proof_body
val no_thm_names: proof -> proof
val no_thm_proofs: proof -> proof
val no_body_proofs: proof -> proof
@@ -237,15 +235,14 @@
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
zboxes: zboxes,
- proof: proof * zproof}
+ zproof: zproof,
+ proof: proof}
and thm_body =
Thm_Body of {open_proof: proof -> proof, body: proof_body future}
and thm_node =
Thm_Node of {theory_name: string, name: string, prop: term,
body: proof_body future, export: unit lazy, consolidate: unit lazy};
-type proofs = proof * zproof;
-
type oracle = (string * Position.T) * term option;
val oracle_ord: oracle ord =
prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord);
@@ -256,13 +253,15 @@
exception MIN_PROOF of unit;
-fun proofs_of (PBody {proof, ...}) = proof;
-val proof_of = fst o proofs_of;
-val zproof_of = snd o proofs_of;
+fun proof_of (PBody {proof, ...}) = proof;
+fun zproof_of (PBody {zproof, ...}) = zproof;
val join_proof = Future.join #> proof_of;
-fun map_proofs_of f (PBody {oracles, thms, zboxes, proof}) =
- PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = f proof};
+fun map_proof_of f (PBody {oracles, thms, zboxes, zproof, proof}) =
+ PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = f proof};
+
+fun no_proofs (PBody {oracles, thms, zboxes, ...}) =
+ PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = MinProof, zproof = ZDummy};
fun thm_header serial pos theory_name name prop types : thm_header =
{serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types};
@@ -347,9 +346,9 @@
val empty_zboxes: zboxes = Inttab.empty;
val union_zboxes = curry (Inttab.merge (fn (_: (zterm * zproof future), _) => true));
-val no_proof = (MinProof, ZDummy);
-fun no_proof_body proof = PBody {oracles = [], thms = [], zboxes = empty_zboxes, proof = proof};
-val no_thm_body = thm_body (no_proof_body no_proof);
+fun no_proof_body zproof proof =
+ PBody {oracles = [], thms = [], zboxes = empty_zboxes, zproof = zproof, proof = proof};
+val no_thm_body = thm_body (no_proof_body ZDummy MinProof);
fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
| no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
@@ -372,7 +371,8 @@
| no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2
| no_body_proofs (PThm (header, Thm_Body {open_proof, body})) =
let
- val body' = Future.value (no_proof_body (proofs_of (Future.join body)));
+ val PBody {zproof, proof, ...} = Future.join body;
+ val body' = Future.value (no_proof_body zproof proof);
val thm_body' = Thm_Body {open_proof = open_proof, body = body'};
in PThm (header, thm_body') end
| no_body_proofs a = a;
@@ -402,8 +402,8 @@
([int_atom serial, theory_name, name],
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
(map Position.properties_of pos,
- (prop, (types, map_proofs_of (apfst open_proof) (Future.join body)))))]
-and proof_body consts (PBody {oracles, thms, zboxes = _, proof = (prf, _)}) =
+ (prop, (types, map_proof_of open_proof (Future.join body)))))]
+and proof_body consts (PBody {oracles, thms, zboxes = _, zproof = _, proof = prf}) =
triple (list (pair (pair string (properties o Position.properties_of))
(option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
and thm consts (a, thm_node) =
@@ -471,7 +471,7 @@
val (a, b, c) =
triple (list (pair (pair string (Position.of_properties o properties))
(option (term consts)))) (list (thm consts)) (proof consts) x;
- in PBody {oracles = a, thms = b, zboxes = empty_zboxes, proof = (c, ZDummy)} end
+ in PBody {oracles = a, thms = b, zboxes = empty_zboxes, zproof = ZDummy, proof = c} end
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
@@ -533,7 +533,7 @@
| stripc x = x
in stripc (prf, []) end;
-fun strip_thm_body (body as PBody {proof = (proof, _), ...}) =
+fun strip_thm_body (body as PBody {proof, ...}) =
(case fst (strip_combt (fst (strip_combP proof))) of
PThm (_, Thm_Body {body = body', ...}) => Future.join body'
| _ => body);
@@ -1982,7 +1982,7 @@
fun fulfill_norm_proof thy ps body0 =
let
val _ = consolidate_bodies (map #2 ps @ [body0]);
- val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (proof0, zproof)} = body0;
+ val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof, proof = proof0} = body0;
val oracles =
unions_oracles
(fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
@@ -1991,7 +1991,7 @@
val zboxes = fold (fn (_, PBody {zboxes, ...}) => union_zboxes zboxes) ps zboxes0;
val proof = rew_proof thy proof0;
in
- PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = (proof, zproof)}
+ PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}
end;
fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
@@ -2122,7 +2122,7 @@
fun prune_body body =
if Options.default_bool "prune_proofs"
- then (Future.map o map_proofs_of) (K no_proof) body
+ then Future.map no_proofs body
else body;
fun export_enabled () = Options.default_bool "export_proofs";
@@ -2200,18 +2200,19 @@
val (ucontext, prop1) = Logic.unconstrainT shyps prop;
- val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf, zprf)} = body;
+ val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zprf, proof = prf} = body;
val proofs = get_proofs_level ();
val prf' = if proof_enabled proofs then fold_rev implies_intr_proof hyps prf else MinProof;
val zprf' = if zproof_enabled proofs then ZTerm.todo_proof zprf else ZDummy;
- val body0 = PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf', zprf')};
+ val body0 =
+ PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zprf', proof = prf'};
fun new_prf () =
let
val i = serial ();
val unconstrainT =
unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
- val postproc = map_proofs_of (apfst (unconstrainT #> named ? rew_proof thy));
+ val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
in (i, fulfill_proof_future thy promises postproc (Future.value body0)) end;
val (i, body') =
@@ -2224,7 +2225,7 @@
let
val Thm_Body {body = body', ...} = thm_body';
val i = if a = "" andalso named then serial () else ser;
- in (i, body' |> ser <> i ? Future.map (map_proofs_of (apfst (rew_proof thy)))) end
+ in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
else new_prf ()
| _ => new_prf ());
--- a/src/Pure/thm.ML Sat Dec 09 17:31:10 2023 +0100
+++ b/src/Pure/thm.ML Sat Dec 09 20:05:13 2023 +0100
@@ -744,11 +744,11 @@
(** derivations and promised proofs **)
-fun make_deriv promises oracles thms zboxes proof =
+fun make_deriv promises oracles thms zboxes zproof proof =
Deriv {promises = promises,
- body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = proof}};
+ body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}};
-val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes Proofterm.no_proof;
+val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes ZDummy MinProof;
(* inference rules *)
@@ -756,12 +756,12 @@
val promise_ord: (serial * thm future) ord = fn ((i, _), (j, _)) => int_ord (j, i);
fun deriv_rule2 (f, g)
- (Deriv {promises = ps1, body = body1}) (Deriv {promises = ps2, body = body2}) =
+ (Deriv {promises = ps1, body = PBody body1}) (Deriv {promises = ps2, body = PBody body2}) =
let
val ps = Ord_List.union promise_ord ps1 ps2;
- val PBody {oracles = oracles1, thms = thms1, zboxes = zboxes1, proof = (prf1, zprf1)} = body1;
- val PBody {oracles = oracles2, thms = thms2, zboxes = zboxes2, proof = (prf2, zprf2)} = body2;
+ 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;
@@ -770,7 +770,7 @@
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 (prf, zprf) end;
+ in make_deriv ps oracles thms zboxes zprf prf end;
fun deriv_rule1 (f, g) = deriv_rule2 (K f, K g) empty_deriv;
@@ -778,14 +778,14 @@
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.proof_enabled proofs then f () else MinProof,
- if Proofterm.zproof_enabled proofs then g () else ZDummy))
+ (if Proofterm.zproof_enabled proofs then g () else ZDummy)
+ (if Proofterm.proof_enabled proofs then f () else MinProof))
else empty_deriv
end;
fun deriv_rule_unconditional (f, g)
- (Deriv {promises, body = PBody {oracles, thms, zboxes, proof = (prf, zprf)}}) =
- make_deriv promises oracles thms zboxes (f prf, g zprf);
+ (Deriv {promises, body = PBody {oracles, thms, zboxes, zproof = zprf, proof = prf}}) =
+ make_deriv promises oracles thms zboxes (g zprf) (f prf);
(* fulfilled proofs *)
@@ -845,7 +845,7 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i cert sorts prop);
in
- Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes Proofterm.no_proof,
+ Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes ZDummy MinProof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1026,10 +1026,11 @@
raise THEORY ("solve_constraints: bad theories for theorem\n" ^
Syntax.string_of_term_global thy (prop_of thm), thy :: bad_thys);
- val Deriv {promises, body = PBody {oracles, thms, zboxes, proof}} = der;
+ val Deriv {promises, body = PBody {oracles, thms, zboxes, zproof, proof}} = der;
val (oracles', thms', zboxes') = (oracles, thms, zboxes)
|> fold (fold union_digest o constraint_digest) constraints;
- val body' = PBody {oracles = oracles', thms = thms', zboxes = zboxes', proof = proof};
+ val body' =
+ PBody {oracles = oracles', thms = thms', zboxes = zboxes', zproof = zproof, proof = proof};
in
Thm (Deriv {promises = promises, body = body'},
{constraints = [], cert = cert, tags = tags, maxidx = maxidx,
@@ -1134,7 +1135,7 @@
Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
name_pos shyps hyps prop ps body;
val zprf = ZTerm.todo_proof (Proofterm.zproof_of body);
- val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
+ val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes zprf prf;
in Thm (der', args) end);
fun close_derivation pos =
@@ -1173,7 +1174,7 @@
then ZTerm.oracle_proof (Context.certificate_theory cert) name prop
else ZDummy;
in
- Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes (proof, zproof),
+ Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes zproof proof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1916,7 +1917,7 @@
Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
shyps prop ps body;
val zprf = ZTerm.todo_proof body;
- val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
+ val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes zprf prf;
val prop' = Proofterm.thm_node_prop (#2 pthm);
in
Thm (der',