--- a/src/Pure/proofterm.ML Sat Jan 06 13:13:48 2024 +0100
+++ b/src/Pure/proofterm.ML Sat Jan 06 15:31:41 2024 +0100
@@ -182,10 +182,10 @@
val export_proof_boxes_required: theory -> bool
val export_proof_boxes: proof_body list -> unit
val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
- val thm_proof: theory -> ZTerm.sorts_zproof -> sorts_proof -> string * Position.T -> sort list ->
- term list -> term -> (serial * proof_body future) list -> proof_body -> proof_body
- val unconstrain_thm_proof: theory -> ZTerm.sorts_zproof -> sorts_proof ->
- sort list -> term -> (serial * proof_body future) list -> proof_body -> term * proof_body
+ val thm_proof: theory -> sorts_proof -> string * Position.T -> sort list -> term list ->
+ term -> (serial * proof_body future) list -> proof_body -> proof_body
+ val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
+ term -> (serial * proof_body future) list -> proof_body -> term * proof_body
val get_identity: sort list -> term list -> term -> proof ->
{serial: serial, theory_name: string, name: string} option
val get_approximative_name: sort list -> term list -> term -> proof -> string
@@ -2173,7 +2173,7 @@
strict = false} xml
end;
-fun prepare_thm_proof unconstrain thy sorts_zproof sorts_proof
+fun prepare_thm_proof unconstrain thy sorts_proof
(name, pos) shyps hyps concl promises
(PBody {oracles = oracles0, thms = thms0, zboxes = zboxes0, zproof = zproof0, proof = proof0}) =
let
@@ -2186,7 +2186,8 @@
val proofs = get_proofs_level ();
val (zproof1, zboxes1) =
- if zproof_enabled proofs then ZTerm.add_box_proof thy hyps concl zproof0 zboxes0
+ if zproof_enabled proofs then
+ ZTerm.add_box_proof {unconstrain = unconstrain} thy hyps concl zproof0 zboxes0
else (ZDummy, []);
val proof1 =
if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0
@@ -2246,20 +2247,16 @@
else map PClass (#outer_constraints ucontext) @ map Hyp hyps;
val proof2 = proof_combP (proof_combt' (head, argst), argsP);
- val (zboxes2, zproof2) =
- if unconstrain then (zboxes1, zproof1) (* FIXME proper zproof *)
- else (zboxes1, zproof1);
-
- val body2 = {oracles = [], thms = [thm], zboxes = zboxes2, zproof = zproof2, proof = proof2};
+ val body2 = {oracles = [], thms = [thm], zboxes = zboxes1, zproof = zproof1, proof = proof2};
in (prop1, PBody body2) end;
in
-fun thm_proof thy sorts_zproof sorts_proof name shyps hyps concl promises =
- prepare_thm_proof false thy sorts_zproof sorts_proof name shyps hyps concl promises #> #2;
+fun thm_proof thy sorts_proof name shyps hyps concl promises =
+ prepare_thm_proof false thy sorts_proof name shyps hyps concl promises #> #2;
-fun unconstrain_thm_proof thy sorts_zproof sorts_proof shyps concl promises body =
- prepare_thm_proof true thy sorts_zproof sorts_proof ("", Position.none)
+fun unconstrain_thm_proof thy sorts_proof shyps concl promises body =
+ prepare_thm_proof true thy sorts_proof ("", Position.none)
shyps [] concl promises body;
end;
--- a/src/Pure/thm.ML Sat Jan 06 13:13:48 2024 +0100
+++ b/src/Pure/thm.ML Sat Jan 06 15:31:41 2024 +0100
@@ -133,7 +133,7 @@
(*type classes*)
val the_classrel: theory -> class * class -> thm
val the_arity: theory -> string * sort list * class -> thm
- val sorts_zproof: theory -> ZTerm.sorts_zproof
+ val sorts_zproof: theory -> ZTerm.sorts_proof
val sorts_proof: theory -> Proofterm.sorts_proof
(*oracles*)
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
@@ -1157,9 +1157,7 @@
val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
val ps = map (apsnd (Future.map fulfill_body)) promises;
- val body' =
- Proofterm.thm_proof thy (sorts_zproof thy) (sorts_proof thy)
- name_pos shyps hyps prop ps body;
+ val body' = Proofterm.thm_proof thy (sorts_proof thy) name_pos shyps hyps prop ps body;
in Thm (make_deriv0 [] body', args) end);
fun close_derivation pos =
@@ -2020,9 +2018,7 @@
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
val ps = map (apsnd (Future.map fulfill_body)) promises;
- val (prop', body') =
- Proofterm.unconstrain_thm_proof thy (sorts_zproof thy) (sorts_proof thy)
- shyps prop ps body;
+ val (prop', body') = Proofterm.unconstrain_thm_proof thy (sorts_proof thy) shyps prop ps body;
in
Thm (make_deriv0 [] body',
{cert = cert,
--- a/src/Pure/zterm.ML Sat Jan 06 13:13:48 2024 +0100
+++ b/src/Pure/zterm.ML Sat Jan 06 15:31:41 2024 +0100
@@ -266,7 +266,8 @@
type zboxes = zbox Ord_List.T
val union_zboxes: zboxes -> zboxes -> zboxes
val unions_zboxes: zboxes list -> zboxes
- val add_box_proof: theory -> term list -> term -> zproof -> zboxes -> zproof * zboxes
+ val add_box_proof: {unconstrain: bool} -> theory ->
+ term list -> term -> zproof -> zboxes -> zproof * zboxes
val thm_proof: theory -> Thm_Name.T * Position.T -> term list -> term -> zproof -> zbox * zproof
val axiom_proof: theory -> string -> term -> zproof
val oracle_proof: theory -> string -> term -> zproof
@@ -299,10 +300,10 @@
zproof -> zproof
val bicompose_proof: theory -> Envir.env -> int -> bool -> term list -> term list ->
term option -> term list -> int -> int -> term list -> zproof -> zproof -> zproof
- type sorts_zproof = (class * class -> zproof) * (string * class list list * class -> zproof)
- val of_sort_proof: Sorts.algebra -> sorts_zproof -> (typ * class -> zproof) ->
+ type sorts_proof = (class * class -> zproof) * (string * class list list * class -> zproof)
+ val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> zproof) ->
typ * sort -> zproof list
- val unconstrainT_proof: theory -> sorts_zproof -> Logic.unconstrain_context -> zproof -> zproof
+ val unconstrainT_proof: theory -> sorts_proof -> Logic.unconstrain_context -> zproof -> zproof
end;
structure ZTerm: ZTERM =
@@ -880,8 +881,9 @@
fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i};
in box_proof zproof_name thy end;
-fun add_box_proof thy hyps concl prf zboxes =
+fun add_box_proof {unconstrain} thy hyps concl prf zboxes =
let
+ (* FIXME unconstrain *)
val (zbox, prf') = box_proof ZBox thy hyps concl prf;
val zboxes' = add_zboxes zbox zboxes;
in (prf', zboxes') end;
@@ -1251,7 +1253,7 @@
(* sort constraints within the logic *)
-type sorts_zproof = (class * class -> zproof) * (string * class list list * class -> zproof);
+type sorts_proof = (class * class -> zproof) * (string * class list list * class -> zproof);
fun of_sort_proof algebra (classrel_proof, arity_proof) hyps =
Sorts.of_sort_derivation algebra