[isabelle-dev] Definite name for case combinator on products [was: NEWS]

[Florian Haftmann]

In fb95d06fb21f, find my attempt to reach a stable status again after
opening too many loose ends.
* The combinator is named »case_prod« uniformly; no aliasses remain, in
order not to obfuscate the now reached state of uniformity.
* The most popular theorem names with »split« are retained (see end of
HOL/Product_Type.thy); there could be room for further cleanup there, e.
g. getting rid of the alias »split« and reducing the variants regarding
eta-contraction further. But I did not attempt this at this moment.
* Some discontinuities introduced unconsciously in the past (e. g. wrong
trigger terms for simprocs) have been repaired silently.
* I encountered a borderline case of printing and just reinstallated a
print translation believed to be totally obsolete; my conclusion at the
moment is that it is not feasible to refine anything regarding the
parsing / printing of products without reconsidering / remoulding the
eta-expansion issue.

This is the state of affairs. Please report any remaning suspicious
behaviour.

	Florian

Am 22.09.2015 um 16:20 schrieb Florian Haftmann:
> So, the direction is going towards prod_case.
> 
> If this is settled, the consequences are:
> * Abbreviation »uncurry« will disappear again.
> * Abbreviation »split« will disappear finally (using the distribution
> and AFP as indicator whether this is »now« or »later«).
> * Theorem names contain »prod_case« instead of »split«; the latter are
> retained as aliasses, but documentation etc. is updated to prefer the
> first version.
> * There is no way to have something like »curry (uncurry f) = f«
> printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f
> x y) = f« by default.
> 
> Any headache with this?
> 
> 	Florian
> 
> Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel:
>> Hi Florian,
>>
>> while I very much welcome the simplified printing rules and your effort
>> of unifying case_prod/split, I am not sure if adding a third alternative
>> name is the way to go. The situation reminds me of the one depicted in [1].
>>
>> Clearly, case_prod is the "right" name from the perspective of the
>> (co)datatype package.
>>
>> Dmitriy
>>
>> [1] https://xkcd.com/927/
>>
>> On 10.09.2015 12:02, Florian Haftmann wrote:
>>> * Combinator to represent case distinction on products is named
>>> "uncurry", with "split" and "prod_case" retained as input abbreviations.
>>>
>>> Partially applied occurences of "uncurry" with eta-contracted body
>>> terms are not printed with special syntax, to provide a compact
>>> notation and getting rid of a special-case print translation.
>>>
>>> Hence, the "uncurry"-expressions are printed the following way:
>>>
>>> a) fully applied "uncurry f p": explicit case-expression;
>>>
>>> b) partially applied with explicit double lambda abstraction in
>>> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;
>>>
>>> c) partially applied with eta-contracted body term "uncurry f":
>>> no special syntax, plain "uncurry" combinator.
>>> This aims for maximum readability in a given subterm.
>>> INCOMPATIBILITY.
>>>
>>> This refers to e6b1236f9b3d.
>>>
>>> This schema emerged after some experimentation and seems to be a
>>> convenient compromise. The longer perspective is to overcome the
>>> case_prod/split schism eventually and consolidate theorem names accordingly.
>>>
>>> The next step after this initial cleanup is to tackle the »let (a, b) =
>>> … in …« issue.
>>>
>>> 	Florian
>>>
>>>
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151013/c9fca71c/attachment.asc>