--- a/src/Pure/Proof/proof_rewrite_rules.ML Sun Dec 31 12:40:10 2023 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sun Dec 31 15:09:04 2023 +0100
@@ -374,7 +374,7 @@
Same.commit (Proofterm.map_proof_same Same.same Same.same of_class_index);
in
map2 reconstruct (Logic.mk_of_sort (T, S))
- (Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.classrel_proof thy) (Thm.arity_proof thy)
+ (Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.sorts_proof thy)
(PClass o apfst Type.strip_sorts) (subst T, S))
end;
--- a/src/Pure/proofterm.ML Sun Dec 31 12:40:10 2023 +0100
+++ b/src/Pure/proofterm.ML Sun Dec 31 15:09:04 2023 +0100
@@ -145,10 +145,8 @@
val abstract_rule_proof: string * term -> proof -> proof
val combination_proof: term -> term -> term -> term -> proof -> proof -> proof
val could_unify: proof * proof -> bool
- val of_sort_proof: Sorts.algebra ->
- (class * class -> proof) ->
- (string * class list list * class -> proof) ->
- (typ * class -> proof) -> typ * sort -> proof list
+ type sorts_proof = (class * class -> proof) * (string * class list list * class -> proof)
+ val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> proof) -> typ * sort -> proof list
val axm_proof: string -> term -> proof
val oracle_proof: string -> term -> proof
val shrink_proof: proof -> proof
@@ -184,12 +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 -> (class * class -> proof) ->
- (string * class list list * class -> proof) -> string * Position.T -> sort list ->
+ 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 -> (class * class -> proof) ->
- (string * class list list * class -> proof) -> sort list -> term ->
- (serial * proof_body future) list -> proof_body -> term * 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 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
@@ -1097,7 +1093,9 @@
(** sort constraints within the logic **)
-fun of_sort_proof algebra classrel_proof arity_proof hyps =
+type sorts_proof = (class * class -> proof) * (string * class list list * class -> proof);
+
+fun of_sort_proof algebra (classrel_proof, arity_proof) hyps =
Sorts.of_sort_derivation algebra
{class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 =>
if c1 = c2 then prf else classrel_proof (c1, c2) %% prf,
@@ -1106,7 +1104,7 @@
in proof_combP (arity_proof (a, Ss, c), prfs) end,
type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
-fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
+fun unconstrainT_proof algebra sorts_proof (ucontext: Logic.unconstrain_context) =
let
fun hyp_map hyp =
(case AList.lookup (op =) (#constraints ucontext) hyp of
@@ -1119,7 +1117,7 @@
fun ofclass (T, c) =
let
val T' = Same.commit typ_sort T;
- val [p] = of_sort_proof algebra classrel_proof arity_proof hyp_map (T', [c])
+ val [p] = of_sort_proof algebra sorts_proof hyp_map (T', [c])
in p end;
in
Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
@@ -2177,7 +2175,7 @@
strict = false} xml
end;
-fun prepare_thm_proof unconstrain thy classrel_proof arity_proof
+fun prepare_thm_proof unconstrain thy sorts_zproof sorts_proof
(name, pos) shyps hyps concl promises (PBody body0) =
let
val named = name <> "";
@@ -2199,8 +2197,7 @@
fun new_prf () =
let
val i = serial ();
- val unconstrainT =
- unconstrainT_proof (Sign.classes_of thy) classrel_proof arity_proof ucontext;
+ val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext;
val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
val body1 =
{oracles = #oracles body0, thms = #thms body0,
@@ -2259,11 +2256,11 @@
in
-fun thm_proof thy classrel_proof arity_proof name shyps hyps concl promises =
- prepare_thm_proof false thy classrel_proof arity_proof name shyps hyps concl promises #> #2;
+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 unconstrain_thm_proof thy classrel_proof arity_proof shyps concl promises body =
- prepare_thm_proof true thy classrel_proof arity_proof ("", Position.none)
+fun unconstrain_thm_proof thy sorts_zproof sorts_proof shyps concl promises body =
+ prepare_thm_proof true thy sorts_zproof sorts_proof ("", Position.none)
shyps [] concl promises body;
end;
--- a/src/Pure/thm.ML Sun Dec 31 12:40:10 2023 +0100
+++ b/src/Pure/thm.ML Sun Dec 31 15:09:04 2023 +0100
@@ -133,8 +133,8 @@
(*type classes*)
val the_classrel: theory -> class * class -> thm
val the_arity: theory -> string * sort list * class -> thm
- val classrel_proof: theory -> class * class -> proof
- val arity_proof: theory -> string * sort list * class -> proof
+ val sorts_zproof: theory -> ZTerm.sorts_zproof
+ val sorts_proof: theory -> Proofterm.sorts_proof
(*oracles*)
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
val oracle_space: theory -> Name_Space.T
@@ -805,6 +805,8 @@
fun proof_bodies_of thms = (join_promises_of thms; map fulfill_body thms);
val proof_body_of = singleton proof_bodies_of;
+
+val zproof_of = Proofterm.zproof_of o proof_body_of;
val proof_of = Proofterm.proof_of o proof_body_of;
fun reconstruct_proof_of thm =
@@ -993,8 +995,8 @@
| NONE => error ("Unproven type arity " ^
Syntax.string_of_arity (Proof_Context.init_global thy) (a, Ss, [c])));
-val classrel_proof = proof_of oo the_classrel;
-val arity_proof = proof_of oo the_arity;
+fun sorts_zproof thy = (zproof_of o the_classrel thy, zproof_of o the_arity thy);
+fun sorts_proof thy = (proof_of o the_classrel thy, proof_of o the_arity thy);
(* solve sort constraints by pro-forma proof *)
@@ -1157,7 +1159,7 @@
val ps = map (apsnd (Future.map fulfill_body)) promises;
val body' =
- Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
+ Proofterm.thm_proof thy (sorts_zproof thy) (sorts_proof thy)
name_pos shyps hyps prop ps body;
in Thm (make_deriv0 [] body', args) end);
@@ -2020,7 +2022,7 @@
val ps = map (apsnd (Future.map fulfill_body)) promises;
val (prop', body') =
- Proofterm.unconstrain_thm_proof thy (classrel_proof thy) (arity_proof thy)
+ Proofterm.unconstrain_thm_proof thy (sorts_zproof thy) (sorts_proof thy)
shyps prop ps body;
in
Thm (make_deriv0 [] body',
--- a/src/Pure/zterm.ML Sun Dec 31 12:40:10 2023 +0100
+++ b/src/Pure/zterm.ML Sun Dec 31 15:09:04 2023 +0100
@@ -301,6 +301,9 @@
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) ->
+ typ * sort -> zproof list
end;
structure ZTerm: ZTERM =
@@ -1191,4 +1194,18 @@
else proof (normp rprf) (if Envir.above env smax then sprf else normp sprf)
end;
+
+(* sort constraints within the logic *)
+
+type sorts_zproof = (class * class -> zproof) * (string * class list list * class -> zproof);
+
+fun of_sort_proof algebra (classrel_proof, arity_proof) hyps =
+ Sorts.of_sort_derivation algebra
+ {class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 =>
+ if c1 = c2 then prf else ZAppp (classrel_proof (c1, c2), prf),
+ type_constructor = fn (a, _) => fn dom => fn c =>
+ let val Ss = map (map snd) dom and prfs = maps (map fst) dom
+ in ZAppps (arity_proof (a, Ss, c), prfs) end,
+ type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
+
end;