Re: [isabelle] Binders and (product) patterns

Hi Florian,

On 28.08.2014 18:17, Florian Haftmann wrote:
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.


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.

     "(∑(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.


If 3. is generally accepted, I am willing to undertake an implementation
at the current state of the art (check/uncheck and local everything (!)).
No objections, of course.

You would base your implementation on the code from Product_Type mentioned in 1. and plug it in before the "case"-uncheck-phase, right?

Why are you also mentioning check? I think the parse translations are good enough here.

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.
How often does this situation occur with constructors different from Pair? Also using the selectors (as provided by datatype_new) might be the better way to express "case p of Ident x => x".


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