*To*: Dmitriy Traytel <traytel at in.tum.de>, usr Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Binders and (product) patterns*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 28 Aug 2014 18:17:26 +0200*In-reply-to*: <53FB08B4.30104@in.tum.de>*Organization*: TU Munich*References*: <53F8CD96.6030009@informatik.tu-muenchen.de> <53FB08B4.30104@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.0

Hi Dmitriy, >> 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])? >> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-April/004091.html thanks for explaining this. The matter has many facets, and I'll attempt to structure it a little: 1. The mentioned syntax fiddling in Product_Type.thy is inoperative and obsolete. A restored version should plugin into the check/uncheck phases. 2. It is a fact of the Isabelle system »as it is« that »spontaneous η-expansion« may occur any time while conducting proofs. IMHO, these two aspects are facts. 3. There should be an effective device to retain product patterns for binders despite (2) for the sake of readability (what (1) was originally supposed to be). I. e. lemma "(∑(a, b)∈R. f a (∑(c, d)∈Q. g d c)) = s" apply simp -- ‹ at {prop "(∑x∈R. case x of (a, b) ⇒ f a (∑x∈Q. case x of (c, d) ⇒ g d c)) = s"}› reveals a considerable decline in readability, particularly when the newly introduced variable names shadow previously essential names. 4. Accepting this yields further questions how to deal with patterns in general. E. g. in the current state of affairs it is not desirable to η-contract expressions at binding positions unconditionally, i.e. "(∑p∈P. case p of Ident x ⇒ x) = s" which is internally just "setsum (λp. case_ident (λx. x) p) P = s" under eta-contraction would collapse to "setsum (case_ident (λx. x)) P = s" which seems not desired here. When the syntax »λC x ⇒ … | D y ⇒ …« has been introduced, I suggested that any surjective constructor (like »Ident« above) should be treated like »Pair«, allow patterns like "(∑(Ident x∈P). x) = s" which would again perfectly be apt to η-contraction again. If 3. is generally accepted, I am willing to undertake an implementation at the current state of the art (check/uncheck and local everything (!)). Any opinion concerning (4)? Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Isabelle2014-RC4: Eta-contraction of expression over paired patterns***From:*Florian Haftmann

**Re: [isabelle] Isabelle2014-RC4: Eta-contraction of expression over paired patterns***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed
- Next by Date: [isabelle] "rewrite_cterm: bad background theory"
- Previous by Thread: Re: [isabelle] Isabelle2014-RC4: Eta-contraction of expression over paired patterns
- Next by Thread: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed
- Cl-isabelle-users August 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list