[isabelle-dev] NEWS

[Florian Haftmann]

Hi Dmitriy,

> 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].

the other two are mere input abbreviations, which could disappear some
time in the future.

Where we have a real mess are the lemma names which follow different
conventions, depending on their origin in the »split« or »case« world.

This is now the first time when there is perspective to converge against
one name.  I do not insist that »uncurry« must be the last word on that,
but I deem that expressions like

  »map (uncurry f) xs«
  »(uncurry o curry) = id«

are much more intuitive to read (and write) than

  »map (split f) xs«
  »(split o curry) = id«
  »map (prod_case f) xs«
  »(prod_case o curry) = id«

> Clearly, case_prod is the "right" name from the perspective of the
> (co)datatype package.

Which I hope is name-ignorant ;-).  The point is that case expressions
are always fully expanded and so an »uncurry« will never show up there.

The situation is similar to inj_on / inj, SIGMA / _ x _, coprime / gcd,
dvd / even where syntax decides how to present logically similar
constructs in a specific fashion but keep them unified internally.

	Florian

> 
> 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/20150910/c25d0537/attachment.sig>