Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2014-RC4: Eta-contraction of expressio...


view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC