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

[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
> 

-- 

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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150922/96e901e6/attachment.sig>