--- a/src/Pure/Proof/extraction.ML Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Dec 02 19:57:57 2023 +0100
@@ -184,6 +184,7 @@
PBody
{oracles = Ord_List.make Proofterm.oracle_ord oracles,
thms = Ord_List.make Proofterm.thm_ord thms,
+ zboxes = Proofterm.empty_zboxes,
proof = (prf, ZDummy)};
in Proofterm.thm_body body end;
--- a/src/Pure/proofterm.ML Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/proofterm.ML Sat Dec 02 19:57:57 2023 +0100
@@ -13,6 +13,7 @@
prop: term, types: typ list option}
type thm_body
type thm_node
+ type zboxes = (zterm * zproof future) Inttab.table
datatype proof =
MinProof
| PBound of int
@@ -28,6 +29,7 @@
and proof_body = PBody of
{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
type oracle = (string * Position.T) * term option
@@ -60,6 +62,8 @@
val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
val union_thms: thm Ord_List.T -> thm Ord_List.T -> thm Ord_List.T
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_thm_names: proof -> proof
@@ -213,6 +217,8 @@
{serial: serial, pos: Position.T list, theory_name: string, name: string,
prop: term, types: typ list option};
+type zboxes = (zterm * zproof future) Inttab.table;
+
datatype proof =
MinProof
| PBound of int
@@ -228,6 +234,7 @@
and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
+ zboxes: zboxes,
proof: proof * zproof}
and thm_body =
Thm_Body of {open_proof: proof -> proof, body: proof_body future}
@@ -252,8 +259,8 @@
val zproof_of = snd o proofs_of;
val join_proof = Future.join #> proof_of;
-fun map_proofs_of f (PBody {oracles, thms, proof}) =
- PBody {oracles = oracles, thms = thms, proof = f proof};
+fun map_proofs_of f (PBody {oracles, thms, zboxes, proof}) =
+ PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = f proof};
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};
@@ -335,8 +342,11 @@
val union_thms = Ord_List.union thm_ord;
val unions_thms = Ord_List.unions thm_ord;
+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 = [], proof = proof};
+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_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf)
@@ -391,7 +401,7 @@
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, proof = (prf, _)}) =
+and proof_body consts (PBody {oracles, thms, zboxes = _, 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) =
@@ -459,7 +469,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, proof = (c, ZDummy)} end
+ in PBody {oracles = a, thms = b, zboxes = empty_zboxes, proof = (c, ZDummy)} end
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
@@ -2012,14 +2022,17 @@
fun fulfill_norm_proof thy ps body0 =
let
val _ = consolidate_bodies (map #2 ps @ [body0]);
- val PBody {oracles = oracles0, thms = thms0, proof = (proof0, zproof)} = body0;
+ val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (proof0, zproof)} = body0;
val oracles =
unions_oracles
(fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
val thms =
unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
+ val zboxes = fold (fn (_, PBody {zboxes, ...}) => union_zboxes zboxes) ps zboxes0;
val proof = rew_proof thy proof0;
- in PBody {oracles = oracles, thms = thms, proof = (proof, zproof)} end;
+ in
+ PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = (proof, zproof)}
+ end;
fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
let
@@ -2227,12 +2240,11 @@
val (ucontext, prop1) = Logic.unconstrainT shyps prop;
- val PBody {oracles = oracles0, thms = thms0, proof = (prf, zprf)} = body;
+ val PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf, zprf)} = body;
val proofs = ! proofs;
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 = Future.value (PBody {oracles = oracles0, thms = thms0, proof = (prf', zprf')});
+ val body0 = PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, proof = (prf', zprf')};
fun new_prf () =
let
@@ -2240,7 +2252,7 @@
val unconstrainT =
unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
val postproc = map_proofs_of (apfst (unconstrainT #> named ? rew_proof thy));
- in (i, fulfill_proof_future thy promises postproc body0) end;
+ in (i, fulfill_proof_future thy promises postproc (Future.value body0)) end;
val (i, body') =
(*somewhat non-deterministic proof boxes!*)
--- a/src/Pure/thm.ML Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/thm.ML Sat Dec 02 19:57:57 2023 +0100
@@ -744,10 +744,11 @@
(** derivations and promised proofs **)
-fun make_deriv promises oracles thms proof =
- Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
+fun make_deriv promises oracles thms zboxes proof =
+ Deriv {promises = promises,
+ body = PBody {oracles = oracles, thms = thms, zboxes = zboxes, proof = proof}};
-val empty_deriv = make_deriv [] [] [] Proofterm.no_proof;
+val empty_deriv = make_deriv [] [] [] Proofterm.empty_zboxes Proofterm.no_proof;
(* inference rules *)
@@ -758,14 +759,16 @@
error ("Illegal level of detail for proof objects: " ^ string_of_int i);
fun deriv_rule2 (f, g)
- (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = proof1}})
- (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = proof2}}) =
+ (Deriv {promises = ps1, body = body1}) (Deriv {promises = ps2, body = 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 = Proofterm.union_oracles oracles1 oracles2;
val thms = Proofterm.union_thms thms1 thms2;
- val (prf1, zprf1) = proof1;
- val (prf2, zprf2) = proof2;
+ val zboxes = Proofterm.union_zboxes zboxes1 zboxes2;
val proof =
(case ! Proofterm.proofs of
0 => Proofterm.no_proof
@@ -775,22 +778,22 @@
| 5 => (MinProof, g zprf1 zprf2)
| 6 => (f prf1 prf2, g zprf1 zprf2)
| i => bad_proofs i);
- in make_deriv ps oracles thms proof end;
+ in make_deriv ps oracles thms zboxes proof end;
fun deriv_rule1 (f, g) = deriv_rule2 (K f, K g) empty_deriv;
fun deriv_rule0 (f, g) =
let val proofs = ! Proofterm.proofs in
if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then
- deriv_rule1 (I, I) (make_deriv [] [] []
+ 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))
else empty_deriv
end;
fun deriv_rule_unconditional (f, g)
- (Deriv {promises, body = PBody {oracles, thms, proof = (prf, zprf)}}) =
- make_deriv promises oracles thms (f prf, g zprf);
+ (Deriv {promises, body = PBody {oracles, thms, zboxes, proof = (prf, zprf)}}) =
+ make_deriv promises oracles thms zboxes (f prf, g zprf);
(* fulfilled proofs *)
@@ -850,7 +853,7 @@
val i = serial ();
val future = future_thm |> Future.map (future_result i cert sorts prop);
in
- Thm (make_deriv [(i, future)] [] [] Proofterm.no_proof,
+ Thm (make_deriv [(i, future)] [] [] Proofterm.empty_zboxes Proofterm.no_proof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -990,20 +993,24 @@
local
-fun union_digest (oracles1, thms1) (oracles2, thms2) =
- (Proofterm.union_oracles oracles1 oracles2, Proofterm.union_thms thms1 thms2);
+val empty_digest = ([], [], Proofterm.empty_zboxes);
-fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, ...}, ...}, _)) =
- (oracles, thms);
+fun union_digest (oracles1, thms1, zboxes1) (oracles2, thms2, zboxes2) =
+ (Proofterm.union_oracles oracles1 oracles2,
+ Proofterm.union_thms thms1 thms2,
+ Proofterm.union_zboxes zboxes1 zboxes2);
+
+fun thm_digest (Thm (Deriv {body = PBody {oracles, thms, zboxes, ...}, ...}, _)) =
+ (oracles, thms, zboxes);
fun constraint_digest ({theory = thy, typ, sort, ...}: constraint) =
Sorts.of_sort_derivation (Sign.classes_of thy)
{class_relation = fn _ => fn _ => fn (digest, c1) => fn c2 =>
- if c1 = c2 then ([], []) else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
+ if c1 = c2 then empty_digest else union_digest digest (thm_digest (the_classrel thy (c1, c2))),
type_constructor = fn (a, _) => fn dom => fn c =>
let val arity_digest = thm_digest (the_arity thy (a, (map o map) #2 dom, c))
in (fold o fold) (union_digest o #1) dom arity_digest end,
- type_variable = fn T => map (pair ([], [])) (Type.sort_of_atyp T)}
+ type_variable = fn T => map (pair empty_digest) (Type.sort_of_atyp T)}
(typ, sort);
in
@@ -1024,10 +1031,10 @@
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, proof}} = der;
- val (oracles', thms') = (oracles, thms)
+ val Deriv {promises, body = PBody {oracles, thms, zboxes, proof}} = der;
+ val (oracles', thms', zboxes') = (oracles, thms, zboxes)
|> fold (fold union_digest o constraint_digest) constraints;
- val body' = PBody {oracles = oracles', thms = thms', proof = proof};
+ val body' = PBody {oracles = oracles', thms = thms', zboxes = zboxes', proof = proof};
in
Thm (Deriv {promises = promises, body = body'},
{constraints = [], cert = cert, tags = tags, maxidx = maxidx,
@@ -1132,7 +1139,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] (prf, zprf);
+ val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
in Thm (der', args) end);
fun close_derivation pos =
@@ -1168,7 +1175,7 @@
| 6 => (make_oracle (), (Proofterm.oracle_proof name prop, ZTerm.todo_proof ()))
| i => bad_proofs i);
in
- Thm (make_deriv [] [oracle] [] proof,
+ Thm (make_deriv [] [oracle] [] Proofterm.empty_zboxes proof,
{cert = Context.join_certificate (Context.Certificate thy', cert2),
tags = [],
maxidx = maxidx,
@@ -1832,7 +1839,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] (prf, zprf);
+ val der' = make_deriv [] [] [pthm] Proofterm.empty_zboxes (prf, zprf);
val prop' = Proofterm.thm_node_prop (#2 pthm);
in
Thm (der',
--- a/src/Pure/zterm.ML Sat Dec 02 15:42:50 2023 +0100
+++ b/src/Pure/zterm.ML Sat Dec 02 19:57:57 2023 +0100
@@ -38,11 +38,6 @@
| ZAppP of zproof * zproof
| ZClassP of ztyp * class (*OFCLASS proof from sorts algebra*)
| ZOracle of serial * zterm * ztyp list
-and zproof_body = ZPBody of
- {boxes: (zterm * zproof future) Inttab.table,
- consts: serial Ord_List.T,
- oracles: ((string * Position.T) * zterm option) Ord_List.T,
- proof: zproof}
signature ZTERM =