Email Gateway (Aug 22 2022 at 20:29): Email Gateway (Aug 22 2022 at 20:29):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Consider the following code, which is essentially a copy of the
definition of set-comprehension syntax from HOL.Set:
consts C :: "('a ⇒ bool) ⇒ 'a set"
syntax
"_C" :: "pttrn ⇒ bool ⇒ 'a set"
("(1⟨_./ _⟩)")
translations
"⟨x. P⟩" ⇌ "CONST C (λx. P)"
The command term "⟨x. x = x⟩" outputs ⟨x. x = x⟩, which is what I’d
expect. However, term "⟨x. P x⟩ outputs C P instead of ⟨x. P x⟩.
My guess is that Isabelle applies η-conversion, turning C (λx. P x)
into C P, which then doesn’t match the right-hand side of the
translation equality. The peculiar thing is that I do get output with
syntactic sugar when using actual set comprehensions: term "{x. P x}"
yields {x. P x}.
Why does Isabelle use syntactic sugar when outputting {x. P x} but not
when outputting ⟨x. P x⟩? Both notations are defined in essentially
the same way.
I’m using Isabelle2018.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:29):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
Hi,
I hope that registering the syntactic constant in the signature is not the
problem!
Because I spent the last few days investigating the syntax translation
package with
the intention of making it better! Namely, making it generate correctly
markup strings for syntax constant!
And I still do not find where the syntax introduced by syntax translation
package is registered in Isabelle!
The usual place is the signature! However it is not there, and my hope is
not because of this!
I am using Isabelle 2019!
Best wishes,
Yakoub.
Email Gateway (Aug 22 2022 at 20:30):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Anyone being able to answer this question?
This issue is not severe, but it would nevertheless be nice to have a
solution for it. Furthermore, it feels awkward to me that Isabelle seems
to treat my own declarations different from library declarations; so
having an explanation for this apparent mismatch would be great.
Thanks in advance for any clarifications. :smile:
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:34):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hello, again!
With the help of responses from several Isabellers (both on- and off-
list), I found a solution to this issue, namely adding the following
declaration:
print_translation ‹[
Syntax_Trans.preserve_binder_abs_tr'
@{const_syntax C}
@{syntax_const "_C"}
]›
It seems to work, but I have to admit that I don’t fully understand
what’s going on internally. So if someone sees a problem with this
solution, I’d be glad to hear about that.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:36):From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Hi Wolfgang,
I'm not knowledgeable enough to answer, but could investigate that also
in Set.thy, term "{x. P x}" initially prints "Collect P", but after the
"print_translation" with line
in [(\<^const_syntax>‹Collect›, setcompr_tr')] end
it becomes "{x. P x}". So you might want to learn what
"print_translation" does (I can't help there).
Best regards,
Akihisa
Last updated: Apr 25 2024 at 12:23 UTC