Stream: Isabelle/ML

Topic: Sorts in proof export

Antoine Gontard (Jun 23 2026 at 07:47):

Hi everyone,
What is the expected behavior of sorts in proof export?
When looking at the exported version (in Isabelle/Scala) of some subpart of the HOL session, I noticed that sorts (in type variables, in propositions' type arguments) are always empty (at least in the few theories I looked) in places I would expect them not to be (definitions/propositions in a typeclass context).
However, in the type arguments of a theory's Spec_Rules, they are present as I would expect them to be.
Is that normal?

Antoine Gontard (Jun 26 2026 at 14:35):

I've been staring at the code for a few days and could not find where that comes from. All I found is that, when I ran a test on a session with Pure + theory HOL.Groups, in every call to Export_theory.encode_thm, the typargs in standard_prop_of thm (Some proof0) are always of empty sort. It looks like Zterm.standard_vars does not remove sorts, so from what I understand, a theories' thms are already void of sorts when the export happens. Is that normal ?

Antoine Gontard (Jul 07 2026 at 11:13):

What I found to get the sorts:

• In src/Pure/Build/export_theory.ML:
  • For const export: Use U instead of U0; add a list string in encode const for the sort and remove the #1 from the definition of args.
  • In encode_thm: compute the typargs with raw_thm first (using ZTerm.standard_vars), and use these instead of the ones computed in standard_prop_of thm.
  • I did not do it for axioms as I did not do it, but the same is doable.
• in src/Pure/proofterm.ML
  • In prepare_thm_proof, same trick, compute typargs first then pass them to export_proof.
  • In export_proof, glue together the newly computed typargs' names (which may have changed) with the precomputed typargs' sorts.

Doing this (and changing src/Pure/Build/export_theory.scala to read the sorts of consts) I indeed got sorts when I needed them most in consts, theorems, and intermediary proofs. Other important sorts can be found in the theories' arities (in particular instantiations' constants' internal names contain enough information to find the associated arity and extract its typargs)

Yutaka Nagashima (Aug 14 2026 at 23:29):

@Antoine Gontard ,

Sorry for the late reply. I'm unsure whether proof term.ML is still actively maintained as of 2026. I'd recommend checking the maintainer's activity level and overall confidence in that portion of the Isabelle source code before investing significant effort or conducting a deep investigation.

Regards, Yutaka

Last updated: Aug 26 2026 at 04:41 UTC