[isabelle] Binders and (product) patterns



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
Description: OpenPGP digital signature



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