Printing of dummy terms in syntax translations
Lukas Stevens
lukas.stevens+isabelle-users at in.tum.de
Fri Jul 10 17:11:30 CEST 2026
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, 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
>
>
>
-------------- next part --------------
diff -r 333ffbe82f5f src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy Mon Jul 06 15:47:01 2026 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Jul 10 14:22:56 2026 +0200
@@ -300,9 +300,11 @@
end
| go pattern elem (Abs abs) =
let
- val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' ctxt abs
+ val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
in
- go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
+ case x of
+ _ $ tx => go ((x, 0) :: pattern) (tx :: elem) t
+ | _ => raise Match
end
| go pattern elem (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t) =
go
diff -r 333ffbe82f5f src/HOL/Set.thy
--- a/src/HOL/Set.thy Mon Jul 06 15:47:01 2026 +0200
+++ b/src/HOL/Set.thy Fri Jul 10 14:22:56 2026 +0200
@@ -353,14 +353,15 @@
if check (P, 0) then tr' P
else
let
- val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
+ val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
val M = Syntax.const \<^syntax_const>\<open>_Coll\<close> $ x $ t;
in
- case t of
- Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
- (Const (\<^const_syntax>\<open>Set.member\<close>, _) $
- (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P =>
- if xN = yN then Syntax.const \<^syntax_const>\<open>_Collect\<close> $ x $ A $ P else M
+ case (x, t) of
+ (_ $ Free(xN, _),
+ Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
+ (Const (\<^const_syntax>\<open>Set.member\<close>, _) $
+ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P) =>
+ if xN = yN then Syntax.const \<^syntax_const>\<open>_Collect\<close> $ x $ A $ P else M
| _ => M
end
end;
diff -r 333ffbe82f5f src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML Mon Jul 06 15:47:01 2026 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Fri Jul 10 14:22:56 2026 +0200
@@ -345,8 +345,11 @@
(strip_abss ctxt strip_abs_vars strip_abs_body (eta_contr ctxt tm));
fun atomic_abs_tr' ctxt (x, T, t) =
- let val xT = singleton (variant_bounds ctxt t) (x, T)
- in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
+ if Name.is_internal x andalso not (Term.is_dependent t) then
+ (Const ("_idtdummy", T), incr_boundvars ~1 t)
+ else
+ let val xT = singleton (variant_bounds ctxt t) (x, T)
+ in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
fun abs_ast_tr' asts =
(case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
-------------- next part --------------
diff -r dd0ea2723c32 thys/Regular_Tree_Relations/Util/FSet_Utils.thy
--- a/thys/Regular_Tree_Relations/Util/FSet_Utils.thy Mon Jul 06 15:47:06 2026 +0200
+++ b/thys/Regular_Tree_Relations/Util/FSet_Utils.thy Fri Jul 10 14:09:57 2026 +0200
@@ -92,14 +92,15 @@
if check (P, 0) then tr' P
else
let
- val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
+ val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
val M = Syntax.const \<^syntax_const>\<open>_fColl\<close> $ x $ t;
in
- case t of
- Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
- (Const (\<^const_syntax>\<open>fmember\<close>, _) $
- (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P =>
- if xN = yN then Syntax.const \<^syntax_const>\<open>_fCollect\<close> $ x $ A $ P else M
+ case (x, t) of
+ (_ $ Free(xN, _),
+ Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
+ (Const (\<^const_syntax>\<open>fmember\<close>, _) $
+ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P) =>
+ if xN = yN then Syntax.const \<^syntax_const>\<open>_fCollect\<close> $ x $ A $ P else M
| _ => M
end
end;
diff -r dd0ea2723c32 thys/Zippy/Zippy/Instances/Zip/Examples/Benchmarks/Set.thy
--- a/thys/Zippy/Zippy/Instances/Zip/Examples/Benchmarks/Set.thy Mon Jul 06 15:47:06 2026 +0200
+++ b/thys/Zippy/Zippy/Instances/Zip/Examples/Benchmarks/Set.thy Fri Jul 10 14:09:57 2026 +0200
@@ -350,14 +350,15 @@
if check (P, 0) then tr' P
else
let
- val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
+ val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
val M = Syntax.const \<^syntax_const>\<open>_Coll\<close> $ x $ t;
in
- case t of
- Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
- (Const (\<^const_syntax>\<open>Set.member\<close>, _) $
- (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P =>
- if xN = yN then Syntax.const \<^syntax_const>\<open>_Collect\<close> $ x $ A $ P else M
+ case (x, t) of
+ (_ $ Free(xN, _),
+ Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
+ (Const (\<^const_syntax>\<open>Set.member\<close>, _) $
+ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (yN, _)) $ A) $ P) =>
+ if xN = yN then Syntax.const \<^syntax_const>\<open>_Collect\<close> $ x $ A $ P else M
| _ => M
end
end;
More information about the isabelle-dev
mailing list