--- a/src/Pure/proofterm.ML Fri Dec 01 18:12:18 2023 +0100
+++ b/src/Pure/proofterm.ML Sat Dec 02 15:42:50 2023 +0100
@@ -28,13 +28,16 @@
and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
- proof: proof}
+ proof: proof * zproof}
+ type proofs = proof * zproof
type oracle = (string * Position.T) * term option
type thm = serial * thm_node
exception MIN_PROOF of unit
+ val proofs_of: proof_body -> proofs
val proof_of: proof_body -> proof
+ val zproof_of: proof_body -> zproof
val join_proof: proof_body future -> proof
- val map_proof_of: (proof -> proof) -> proof_body -> proof_body
+ val map_proofs_of: (proofs -> proofs) -> 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
@@ -57,7 +60,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 no_proof_body: proof -> proof_body
+ val no_proof: proofs
+ val no_proof_body: proofs -> proof_body
val no_thm_names: proof -> proof
val no_thm_proofs: proof -> proof
val no_body_proofs: proof -> proof
@@ -72,8 +76,10 @@
val %> : proof * term -> proof
(*primitive operations*)
+ val proof_enabled: int -> bool
+ val zproof_enabled: int -> bool
val proofs: int Unsynchronized.ref
- val proofs_enabled: unit -> bool
+ val any_proofs_enabled: unit -> bool
val atomic_proof: proof -> bool
val compact_proof: proof -> bool
val proof_combt: proof * term list -> proof
@@ -222,13 +228,15 @@
and proof_body = PBody of
{oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
- proof: proof}
+ proof: proof * zproof}
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);
@@ -239,10 +247,12 @@
exception MIN_PROOF of unit;
-fun proof_of (PBody {proof, ...}) = proof;
+fun proofs_of (PBody {proof, ...}) = proof;
+val proof_of = fst o proofs_of;
+val zproof_of = snd o proofs_of;
val join_proof = Future.join #> proof_of;
-fun map_proof_of f (PBody {oracles, thms, proof}) =
+fun map_proofs_of f (PBody {oracles, thms, proof}) =
PBody {oracles = oracles, thms = thms, proof = f proof};
fun thm_header serial pos theory_name name prop types : thm_header =
@@ -325,8 +335,9 @@
val union_thms = Ord_List.union thm_ord;
val unions_thms = Ord_List.unions thm_ord;
+val no_proof = (MinProof, ZDummy);
fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof};
-val no_thm_body = thm_body (no_proof_body MinProof);
+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)
| no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
@@ -349,7 +360,7 @@
| 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 (join_proof body));
+ val body' = Future.value (no_proof_body (proofs_of (Future.join body)));
val thm_body' = Thm_Body {open_proof = open_proof, body = body'};
in PThm (header, thm_body') end
| no_body_proofs a = a;
@@ -378,8 +389,9 @@
fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) =>
([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_proof_of open_proof (Future.join body)))))]
-and proof_body consts (PBody {oracles, thms, proof = prf}) =
+ (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, _)}) =
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) =
@@ -447,7 +459,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} end
+ in PBody {oracles = a, thms = b, proof = (c, ZDummy)} end
and thm consts x =
let
val (a, (b, (c, (d, e)))) =
@@ -464,8 +476,14 @@
(** proof objects with different levels of detail **)
-val proofs = Unsynchronized.ref 2;
-fun proofs_enabled () = ! proofs >= 2;
+fun proof_enabled proofs = Word.andb (Word.fromInt proofs, 0w2) <> 0w0;
+fun zproof_enabled proofs = Word.andb (Word.fromInt proofs, 0w4) <> 0w0;
+
+val proofs = Unsynchronized.ref 6;
+
+fun any_proofs_enabled () =
+ let val proofs = ! proofs
+ in proof_enabled proofs orelse zproof_enabled proofs end;
fun atomic_proof prf =
(case prf of
@@ -496,7 +514,7 @@
| stripc x = x
in stripc (prf, []) end;
-fun strip_thm_body (body as PBody {proof, ...}) =
+fun strip_thm_body (body as PBody {proof = (proof, _), ...}) =
(case fst (strip_combt (fst (strip_combP proof))) of
PThm (_, Thm_Body {body = body', ...}) => Future.join body'
| _ => body);
@@ -1605,7 +1623,7 @@
let val (rules, procs) = #1 (Data.get thy)
in (map #2 rules, map #2 procs) end;
-fun rew_proof thy = rewrite_prf fst (get_rew_data thy);
+fun rew_proof thy prf = rewrite_prf fst (get_rew_data thy) prf;
fun add_prf_rrule r = (Data.map o apfst o apfst) (cons (stamp (), r));
fun add_prf_rproc p = (Data.map o apfst o apsnd) (cons (stamp (), p));
@@ -1994,14 +2012,14 @@
fun fulfill_norm_proof thy ps body0 =
let
val _ = consolidate_bodies (map #2 ps @ [body0]);
- val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
+ val PBody {oracles = oracles0, thms = thms0, 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 proof = rew_proof thy proof0;
- in PBody {oracles = oracles, thms = thms, proof = proof} end;
+ in PBody {oracles = oracles, thms = thms, proof = (proof, zproof)} end;
fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
let
@@ -2131,7 +2149,7 @@
fun prune_body body =
if Options.default_bool "prune_proofs"
- then (Future.map o map_proof_of) (K MinProof) body
+ then (Future.map o map_proofs_of) (K no_proof) body
else body;
fun export_enabled () = Options.default_bool "export_proofs";
@@ -2209,18 +2227,19 @@
val (ucontext, prop1) = Logic.unconstrainT shyps prop;
- val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
- val body0 =
- Future.value
- (PBody {oracles = oracles0, thms = thms0,
- proof = if proofs_enabled () then fold_rev implies_intr_proof hyps prf else MinProof});
+ val PBody {oracles = oracles0, thms = thms0, 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')});
fun new_prf () =
let
val i = serial ();
val unconstrainT =
unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
- val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
+ val postproc = map_proofs_of (apfst (unconstrainT #> named ? rew_proof thy));
in (i, fulfill_proof_future thy promises postproc body0) end;
val (i, body') =
@@ -2233,7 +2252,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_proof_of (rew_proof thy))) end
+ in (i, body' |> ser <> i ? Future.map (map_proofs_of (apfst (rew_proof thy)))) end
else new_prf ()
| _ => new_prf ());
--- a/src/Pure/thm.ML Fri Dec 01 18:12:18 2023 +0100
+++ b/src/Pure/thm.ML Sat Dec 02 15:42:50 2023 +0100
@@ -747,7 +747,7 @@
fun make_deriv promises oracles thms proof =
Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
-val empty_deriv = make_deriv [] [] [] MinProof;
+val empty_deriv = make_deriv [] [] [] Proofterm.no_proof;
(* inference rules *)
@@ -757,29 +757,40 @@
fun bad_proofs i =
error ("Illegal level of detail for proof objects: " ^ string_of_int i);
-fun deriv_rule2 f
- (Deriv {promises = ps1, body = PBody {oracles = oracles1, thms = thms1, proof = prf1}})
- (Deriv {promises = ps2, body = PBody {oracles = oracles2, thms = thms2, proof = prf2}}) =
+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}}) =
let
val ps = Ord_List.union promise_ord ps1 ps2;
val oracles = Proofterm.union_oracles oracles1 oracles2;
val thms = Proofterm.union_thms thms1 thms2;
- val prf =
+ val (prf1, zprf1) = proof1;
+ val (prf2, zprf2) = proof2;
+ val proof =
(case ! Proofterm.proofs of
- 2 => f prf1 prf2
- | 1 => MinProof
- | 0 => MinProof
+ 0 => Proofterm.no_proof
+ | 1 => Proofterm.no_proof
+ | 2 => (f prf1 prf2, ZDummy)
+ | 4 => (MinProof, g zprf1 zprf2)
+ | 5 => (MinProof, g zprf1 zprf2)
+ | 6 => (f prf1 prf2, g zprf1 zprf2)
| i => bad_proofs i);
- in make_deriv ps oracles thms prf end;
+ in make_deriv ps oracles thms proof end;
-fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
+fun deriv_rule1 (f, g) = deriv_rule2 (K f, K g) empty_deriv;
-fun deriv_rule0 make_prf =
- if ! Proofterm.proofs <= 1 then empty_deriv
- else deriv_rule1 I (make_deriv [] [] [] (make_prf ()));
+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 [] [] []
+ (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 (Deriv {promises, body = PBody {oracles, thms, proof}}) =
- make_deriv promises oracles thms (f proof);
+fun deriv_rule_unconditional (f, g)
+ (Deriv {promises, body = PBody {oracles, thms, proof = (prf, zprf)}}) =
+ make_deriv promises oracles thms (f prf, g zprf);
(* fulfilled proofs *)
@@ -833,13 +844,13 @@
val Cterm {cert = cert, t = prop, T, maxidx, sorts} = ct;
val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
val _ =
- if Proofterm.proofs_enabled ()
+ if Proofterm.any_proofs_enabled ()
then raise CTERM ("future: proof terms enabled", [ct]) else ();
val i = serial ();
val future = future_thm |> Future.map (future_result i cert sorts prop);
in
- Thm (make_deriv [(i, future)] [] [] MinProof,
+ Thm (make_deriv [(i, future)] [] [] Proofterm.no_proof,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -858,7 +869,7 @@
(case Name_Space.lookup (Theory.axiom_table thy) name of
SOME prop =>
let
- val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop);
+ val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop, ZTerm.todo_proof);
val cert = Context.Certificate thy;
val maxidx = maxidx_of_term prop;
val shyps = Sorts.insert_term prop [];
@@ -885,7 +896,7 @@
(* technical adjustments *)
fun norm_proof (th as Thm (der, args)) =
- Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th)) der, args);
+ Thm (deriv_rule1 (Proofterm.rew_proof (theory_of_thm th), I) der, args);
fun adjust_maxidx_thm i
(th as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) =
@@ -1063,7 +1074,7 @@
val shyps' = fold (Sorts.insert_sort o #2) present extra';
in
Thm (deriv_rule_unconditional
- (Proofterm.strip_shyps_proof algebra present witnessed extra') der,
+ (Proofterm.strip_shyps_proof algebra present witnessed extra', I) der,
{cert = cert, tags = tags, maxidx = maxidx, constraints = constraints',
shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop})
end)
@@ -1117,10 +1128,11 @@
val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
val ps = map (apsnd (Future.map fulfill_body)) promises;
- val (pthm, proof) =
+ val (pthm, prf) =
Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
name_pos shyps hyps prop ps body;
- val der' = make_deriv [] [] [pthm] proof;
+ val zprf = ZTerm.todo_proof (Proofterm.zproof_of body);
+ val der' = make_deriv [] [] [pthm] (prf, zprf);
in Thm (der', args) end);
fun close_derivation pos =
@@ -1144,14 +1156,19 @@
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
let
- val (oracle, prf) =
+ fun no_oracle () = ((name, Position.none), NONE);
+ fun make_oracle () = ((name, Position.thread_data ()), SOME prop);
+ val (oracle, proof) =
(case ! Proofterm.proofs of
- 2 => (((name, Position.thread_data ()), SOME prop), Proofterm.oracle_proof name prop)
- | 1 => (((name, Position.thread_data ()), SOME prop), MinProof)
- | 0 => (((name, Position.none), NONE), MinProof)
+ 0 => (no_oracle (), Proofterm.no_proof)
+ | 1 => (make_oracle (), Proofterm.no_proof)
+ | 2 => (make_oracle (), (Proofterm.oracle_proof name prop, ZDummy))
+ | 4 => (no_oracle (), (MinProof, ZTerm.todo_proof ()))
+ | 5 => (make_oracle (), (MinProof, ZTerm.todo_proof ()))
+ | 6 => (make_oracle (), (Proofterm.oracle_proof name prop, ZTerm.todo_proof ()))
| i => bad_proofs i);
in
- Thm (make_deriv [] [oracle] [] prf,
+ Thm (make_deriv [] [oracle] [] proof,
{cert = Context.join_certificate (Context.Certificate thy', cert2),
tags = [],
maxidx = maxidx,
@@ -1188,7 +1205,7 @@
raise THM ("assume: prop", 0, [])
else if maxidx <> ~1 then
raise THM ("assume: variables", maxidx, [])
- else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop),
+ else Thm (deriv_rule0 (fn () => Proofterm.Hyp prop, ZTerm.todo_proof),
{cert = cert,
tags = [],
maxidx = ~1,
@@ -1212,7 +1229,7 @@
if T <> propT then
raise THM ("implies_intr: assumptions must have type prop", 0, [th])
else
- Thm (deriv_rule1 (Proofterm.implies_intr_proof A) der,
+ Thm (deriv_rule1 (Proofterm.implies_intr_proof A, ZTerm.todo_proof) der,
{cert = join_certificate1 (ct, th),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1239,7 +1256,7 @@
(case prop of
Const ("Pure.imp", _) $ A $ B =>
if A aconv propA then
- Thm (deriv_rule2 (curry Proofterm.%%) der derA,
+ Thm (deriv_rule2 (curry Proofterm.%%, K ZTerm.todo_proof) der derA,
{cert = join_certificate2 (thAB, thA),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1271,7 +1288,7 @@
if occs x ts tpairs then
raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
else
- Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE) der,
+ Thm (deriv_rule1 (Proofterm.forall_intr_proof (a, x) NONE, ZTerm.todo_proof) der,
{cert = join_certificate1 (ct, th),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1300,7 +1317,7 @@
if T <> qary then
raise THM ("forall_elim: type mismatch", 0, [th])
else
- Thm (deriv_rule1 (Proofterm.% o rpair (SOME t)) der,
+ Thm (deriv_rule1 (Proofterm.% o rpair (SOME t), ZTerm.todo_proof) der,
{cert = join_certificate1 (ct, th),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1318,7 +1335,7 @@
t \<equiv> t
*)
fun reflexive (Cterm {cert, t, T = _, maxidx, sorts}) =
- Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1336,7 +1353,7 @@
fun symmetric (th as Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
(case prop of
(eq as Const ("Pure.eq", _)) $ t $ u =>
- Thm (deriv_rule1 Proofterm.symmetric_proof der,
+ Thm (deriv_rule1 (Proofterm.symmetric_proof, ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1364,7 +1381,7 @@
((eq as Const ("Pure.eq", Type (_, [U, _]))) $ t1 $ u, Const ("Pure.eq", _) $ u' $ t2) =>
if not (u aconv u') then err "middle term"
else
- Thm (deriv_rule2 (Proofterm.transitive_proof U u) der1 der2,
+ Thm (deriv_rule2 (Proofterm.transitive_proof U u, K ZTerm.todo_proof) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1387,7 +1404,7 @@
(case t of Abs (_, _, bodt) $ u => subst_bound (u, bodt)
| _ => raise THM ("beta_conversion: not a redex", 0, []));
in
- Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1399,7 +1416,7 @@
end;
fun eta_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
- Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1410,7 +1427,7 @@
prop = Logic.mk_equals (t, Envir.eta_contract t)});
fun eta_long_conversion (Cterm {cert, t, T = _, maxidx, sorts}) =
- Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof),
+ Thm (deriv_rule0 (fn () => Proofterm.reflexive_proof, ZTerm.todo_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1436,7 +1453,7 @@
if occs x ts tpairs then
raise THM ("abstract_rule: variable " ^ quote a ^ " free in assumptions", 0, [th])
else
- Thm (deriv_rule1 (Proofterm.abstract_rule_proof (b, x)) der,
+ Thm (deriv_rule1 (Proofterm.abstract_rule_proof (b, x), ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1476,7 +1493,7 @@
(Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
(chktypes fT tT;
- Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2,
+ Thm (deriv_rule2 (Proofterm.combination_proof f g t u, K ZTerm.todo_proof) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1504,7 +1521,7 @@
(case (prop1, prop2) of
(Const("Pure.imp", _) $ A $ B, Const("Pure.imp", _) $ B' $ A') =>
if A aconv A' andalso B aconv B' then
- Thm (deriv_rule2 (Proofterm.equal_intr_proof A B) der1 der2,
+ Thm (deriv_rule2 (Proofterm.equal_intr_proof A B, K ZTerm.todo_proof) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1533,7 +1550,7 @@
(case prop1 of
Const ("Pure.eq", _) $ A $ B =>
if prop2 aconv A then
- Thm (deriv_rule2 (Proofterm.equal_elim_proof A B) der1 der2,
+ Thm (deriv_rule2 (Proofterm.equal_elim_proof A B, K ZTerm.todo_proof) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),
@@ -1568,7 +1585,7 @@
val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
(*remove trivial tpairs, of the form t \<equiv> t*)
|> filter_out (op aconv);
- val der' = deriv_rule1 (Proofterm.norm_proof' env) der;
+ val der' = deriv_rule1 (Proofterm.norm_proof' env, ZTerm.todo_proof) der;
val thy' = Context.certificate_theory cert' handle ERROR msg =>
raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
val constraints' = insert_constraints_env thy' env constraints;
@@ -1612,7 +1629,7 @@
val tpairs' = map (apply2 generalize) tpairs;
val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
in
- Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop) der,
+ Thm (deriv_rule1 (Proofterm.generalize_proof (tfrees, frees) idx prop, ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx',
@@ -1718,7 +1735,8 @@
instT' constraints;
in
Thm (deriv_rule1
- (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d) der,
+ (fn d => Proofterm.instantiate (TVars.map (K #1) instT', Vars.map (K #1) inst') d,
+ ZTerm.todo_proof) der,
{cert = cert',
tags = [],
maxidx = maxidx',
@@ -1759,7 +1777,7 @@
if T <> propT then
raise THM ("trivial: the term must have type prop", 0, [])
else
- Thm (deriv_rule0 (fn () => Proofterm.trivial_proof),
+ Thm (deriv_rule0 (fn () => Proofterm.trivial_proof, ZTerm.todo_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1783,7 +1801,7 @@
val Cterm {t = prop, maxidx, sorts, ...} = global_cterm_of thy (Logic.mk_of_class (T, c));
in
if Sign.of_sort thy (T, [c]) then
- Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c)),
+ Thm (deriv_rule0 (fn () => Proofterm.PClass (T, c), ZTerm.todo_proof),
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -1810,10 +1828,11 @@
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
val ps = map (apsnd (Future.map fulfill_body)) promises;
- val (pthm, proof) =
+ val (pthm, prf) =
Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
shyps prop ps body;
- val der' = make_deriv [] [] [pthm] proof;
+ val zprf = ZTerm.todo_proof body;
+ val der' = make_deriv [] [] [pthm] (prf, zprf);
val prop' = Proofterm.thm_node_prop (#2 pthm);
in
Thm (der',
@@ -1835,7 +1854,7 @@
val (al, prop2) = Type.varify_global tfrees prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
in
- (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees) der,
+ (al, Thm (deriv_rule1 (Proofterm.varify_proof prop tfrees, ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = Int.max (0, maxidx),
@@ -1855,7 +1874,7 @@
val prop2 = Type.legacy_freeze prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
in
- Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1) der,
+ Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1, ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx_of_term prop2,
@@ -1904,7 +1923,7 @@
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) der,
+ Thm (deriv_rule1 (Proofterm.lift_proof gprop inc prop, ZTerm.todo_proof) der,
{cert = join_certificate1 (goal, orule),
tags = [],
maxidx = maxidx + inc,
@@ -1919,7 +1938,7 @@
if i < 0 then raise THM ("negative increment", 0, [thm])
else if i = 0 then thm
else
- Thm (deriv_rule1 (Proofterm.incr_indexes i) der,
+ Thm (deriv_rule1 (Proofterm.incr_indexes i, ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx + i,
@@ -1944,7 +1963,8 @@
raise CONTEXT (msg, [], [], [state], Option.map Context.Proof opt_ctxt);
in
Thm (deriv_rule1
- (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env) der,
+ (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env,
+ ZTerm.todo_proof) der,
{tags = [],
maxidx = Envir.maxidx_of env,
constraints = insert_constraints_env thy' env constraints,
@@ -1979,7 +1999,7 @@
(case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
~1 => raise THM ("eq_assumption", 0, [state])
| n =>
- Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
+ Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1), ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -2009,7 +2029,7 @@
in Logic.list_all (params, Logic.list_implies (qs @ ps, concl)) end
else raise THM ("rotate_rule", k, [state]);
in
- Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m) der,
+ Thm (deriv_rule1 (Proofterm.rotate_proof Bs Bi' params asms m, ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -2043,7 +2063,7 @@
in (prems', Logic.list_implies (prems', concl)) end
else raise THM ("permute_prems: k", k, [rl]);
in
- Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m) der,
+ Thm (deriv_rule1 (Proofterm.permute_prems_proof prems' j m, ZTerm.todo_proof) der,
{cert = cert,
tags = [],
maxidx = maxidx,
@@ -2201,7 +2221,8 @@
Thm (deriv_rule2
(if Envir.is_empty env then bicompose_proof
else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env
- else Proofterm.norm_proof' env oo bicompose_proof) rder' sder,
+ else Proofterm.norm_proof' env oo bicompose_proof,
+ K ZTerm.todo_proof) rder' sder,
{tags = [],
maxidx = Envir.maxidx_of env,
constraints = constraints',
@@ -2220,7 +2241,7 @@
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) rder)
+ deriv_rule1 (Proofterm.map_proof_terms (rename K) I, ZTerm.todo_proof) rder)
end;
in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
handle TERM _ =>