Email Gateway (Jul 07 2026 at 11:18): Email Gateway (Jul 07 2026 at 11:18):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Dear Isabelle developers,
I am working on the type annotation algorithm in
~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML that is used
by some interactive tools, e.g., Sledgehammer and Sketch and Explore.
The algorithm places type annotations in terms such that printing and
then parsing them again yields a term with the same type as the original
term. This is crucial when trying to output well-formed Isar proofs.
While testing the algorithm, I ran into some unfortunate behavior that
results from the interaction of Syntax_Trans.atomic_abs_tr' and the
syntax translation case_prod_tr'/case_prod_guess_names_tr' in
Product_Type.thy. You can observe this behavior in
Isabelle/333ffbe82f5f, where
term "λ_. 1 :: nat"
yields "λ_. 1" :: "'a ⇒ nat" while
term "λ(x, _). 1 :: nat"
gives "λ(x, uu_). 1" :: "'a × 'b ⇒ nat", which contains an internal
variable uu_. The latter term cannot be parsed after printing it due to
the internal variable. Note that the same behavior surfaces for other
users of Syntax_Trans.atomic_abs_tr' such as the translations for SOME
and set comprehensions.
The reason for the first term being printed without internal variables
is the changeset Isabelle/41986849fee0 that adds support for the syntax
constant _idtdummy (printed as _) to Syntax_Trans.abs_tr'/mk_binder_tr';
however, case_prod_tr'/case_prod_guess_names_tr' internally uses
Syntax_Trans.atomic_abs_tr', which has no support for _idtdummy. This
could be changed by a 4-line modification of Syntax_Trans.atomic_abs_tr'
(see attached diff), which produces the right result on the surface,
although I am not sure if there is any collateral.
Anecdotally, I know that users of Sketch and Explore have stumbled over
this behavior.
Cheers,
Lukas
Email Gateway (Jul 10 2026 at 15:19):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
After consulting with Tobias and Larry, I have now inspected all users
of Syntax_Trans.atomic_abs_tr' in the distribution and the AFP and
propose the attached changes. Except for a change in
HOL-Probability.Probability_Measure all changes are concerned with the
print_translation of Collect in HOL.Set and its clones. The change to
the print translation of Collect is necessary, since
Syntax_Trans.atomic_abs_tr' now might return _idtdummy instead of always
a variable. This changes the behavior of
term "{_. True}"
from outputting "{uu_. True}" to "{_. True}", which is arguably nicer.
The change to HOL-Probability.Probability_Measure is perhaps overly
defensive because the translation only works on bounded set
comprehensions: e.g., for a bounded set comprehension {x. x ∈ A ∧ True}
the bound variable x is always used, so it can never be replaced by a
dummy. Allowing dummies in bounded set comprehensions would therefore
require significant refinements. I have checked all other users of
Syntax_Trans.atomic_abs_tr' and convinced myself that no changes are
necessary. The AFP builds successfully with these changes:
https://build.proof.cit.tum.de/build?id=38dc54fc-0a32-4755-a0b3-496107c8d016.
Tobias has pointed out that he is the original author of the file, but
judging from the more recent history Makarius is the current owner of
the file. Makarius, can you comment on how to proceed?
Cheers,
Lukas
On 07.07.26 13:09, Lukas Stevens wrote:
Dear Isabelle developers,
I am working on the type annotation algorithm in
~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML that is
used by some interactive tools, e.g., Sledgehammer and Sketch and
Explore. The algorithm places type annotations in terms such that
printing and then parsing them again yields a term with the same type
as the original term. This is crucial when trying to output
well-formed Isar proofs.While testing the algorithm, I ran into some unfortunate behavior that
results from the interaction of Syntax_Trans.atomic_abs_tr' and the
syntax translation case_prod_tr'/case_prod_guess_names_tr' in
Product_Type.thy. You can observe this behavior in
Isabelle/333ffbe82f5f, whereterm "λ_. 1 :: nat"
yields "λ_. 1" :: "'a ⇒ nat" while
term "λ(x, _). 1 :: nat"
gives "λ(x, uu_). 1" :: "'a × 'b ⇒ nat", which contains an internal
variable uu_. The latter term cannot be parsed after printing it due
to the internal variable. Note that the same behavior surfaces for
other users of Syntax_Trans.atomic_abs_tr' such as the translations
for SOME and set comprehensions.The reason for the first term being printed without internal variables
is the changeset Isabelle/41986849fee0 that adds support for the
syntax constant _idtdummy (printed as _) to
Syntax_Trans.abs_tr'/mk_binder_tr'; however,
case_prod_tr'/case_prod_guess_names_tr' internally uses
Syntax_Trans.atomic_abs_tr', which has no support for _idtdummy. This
could be changed by a 4-line modification of
Syntax_Trans.atomic_abs_tr' (see attached diff), which produces the
right result on the surface, although I am not sure if there is any
collateral.Anecdotally, I know that users of Sketch and Explore have stumbled
over this behavior.Cheers,
Lukas
atomic_abs_tr.diff
atomic_abs_tr_AFP.diff
Email Gateway (Jul 10 2026 at 18:15):From: Makarius <makarius@sketis.net>
On 10/07/2026 17:11, Lukas Stevens wrote:
Tobias has pointed out that he is the original author of the file, but judging
from the more recent history Makarius is the current owner of the file.
Makarius, can you comment on how to proceed?
Tobias started the inner syntax engine > 30 years ago. I have reworked it so
many times since then that I don't remember how often it has changed.
In Isabelle development, we don't have "owners" of anything, but individuals
who are personally responsible for certain parts of the system.
I am personally responsible for everything around inner syntax.
I am presently busy elsewhere, and my mail folder is lagging behind several
months.
Re-openening a thread just after a few days of inactivity is a waste of time
--- it slows down the development process for no particular reason.
Makarius
Last updated: Jul 13 2026 at 06:55 UTC