# HG changeset patch
# User wenzelm
# Date 1704031744 -3600
# Node ID f4fdf5eebcac247e928948c0dbb759e980bfe135
# Parent  cb19148c0b958beeb0a3f61925243f8c8d6e5843
pro-forma support for ZTerm.sorts_zproof;

diff -r cb19148c0b95 -r f4fdf5eebcac src/Pure/Proof/proof_rewrite_rules.ML
--- 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;
 
diff -r cb19148c0b95 -r f4fdf5eebcac src/Pure/proofterm.ML
--- 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;
diff -r cb19148c0b95 -r f4fdf5eebcac src/Pure/thm.ML
--- 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',
diff -r cb19148c0b95 -r f4fdf5eebcac src/Pure/zterm.ML
--- 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;