Email Gateway (Aug 19 2022 at 15:34): Email Gateway (Aug 19 2022 at 15:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
It is maybe too late to do any work on the following issue which I have
stumbled over today.
In Product_Type.thy there is some syntax fiddling to print binders over
product values conveniently, as in the following statements:
lemma "∀(a, b) ∈ A. P b a"
apply simp -- {* and this is what we get *}
oops
lemma Collect_Pair_syntax:
"{(x, y). P x y} = {p. (case p of (x, y) ⇒ P x y)}"
-- {* and this is what we get for Collect *}
oops
This works only if those expressions are proper eta-contracted. For
this sake there are print translations in Product_Type.thy. Alas, as
the examples above demonstrate, they seem to be inoperative. A
superficial analysis is presented in the attached theory: the print
translations try to match against @{const_syntax case_prod}, but this
never occurs in the terms to be translated!
I did not attempt to do a bisection so far.
Maybe something got broken during refinements of the case pattern
syntax. Any suspicions?
Cheers,
Florian
Patterns.thy
signature.asc
Email Gateway (Aug 19 2022 at 15:34):From: Dmitriy Traytel <traytel@in.tum.de>
Hi Florian,
indeed the observed behaviour is due to the changes from early 2013 in
how the case syntax is handled. This is also related to the discussion
on isabelle-dev [1], where the consensus seemed to be that the
simplified behaviour of the pretty printer is desirable (such that I
didn't attempt to integrate the print translations from Product_Type).
So one should either drop the inoperative translation altogether or
transform it into a proper syntax uncheck phase (where one operates on
the real constant case_prod, not its syntactic representation). Any
opinion (different from the one in [1])?
Dmitriy
[1]
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-April/004091.html
Last updated: Nov 21 2024 at 12:39 UTC