Re: [isabelle] Isabelle2014-RC4: Eta-contraction of expression over paired patterns



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

On 23.08.2014 19:21, Florian Haftmann wrote:
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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.