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

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 *}

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 *}

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?



PGP available:

Attachment: Patterns.thy
Description: application/extension-thy

Attachment: signature.asc
Description: OpenPGP digital signature

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