Email Gateway (Aug 19 2022 at 15:39): Email Gateway (Aug 19 2022 at 15:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dmitriy,
thanks for explaining this.
The matter has many facets, and I'll attempt to structure it a little:
The mentioned syntax fiddling in Product_Type.thy is inoperative and
obsolete. A restored version should plugin into the check/uncheck phases.
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.
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 --
‹@{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.
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
signature.asc
Email Gateway (Aug 19 2022 at 15:50):From: Dmitriy Traytel <traytel@in.tum.de>
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:
- The mentioned syntax fiddling in Product_Type.thy is inoperative and
obsolete. A restored version should plugin into the check/uncheck phases.[...]
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 --
‹@{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.
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".
Dmitriy
Last updated: Apr 25 2024 at 12:23 UTC