[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural

[Andrei Popescu]

> Johannes wrote:

> Theorems about complex numbers are now stated only using Re and Im, the Complex
>  constructor is not used anymore. It is possible to use primcorec to defined the behaviour of a complex-valued function.

>> Makarius wrote:
>> That is indeed very nice.  Is that a new invention or an old trick that every category theorist knows?

The fact that one can use primcorec to obtain the Re/Im view is simply a consequence of the syntactic sugar for the top 
"sum of products" layer of (co)datatypes and the associated convenience for the (co)recursor.  

IMO, the proximate genus of this Re/Im species is not codatatype, but functor adjunction.
Consider the functor Duplicate : Set --> Set * Set that sends each set A to the pair (A,A) and similarly each function 
f : A -> B to (f,f).  Then the product functor _*_ : Set * Set -> Set is its right adjoint, 
whereas the sum functor _+_ : Set * Set -> Set is its left adjoint.  These mean:

(1) Giving a function from A to B * C is equivalent to giving a morphism in Set * Set from (A,A) to (B,C), i.e., two functions: 
one from A to B and one from A to C -- this is the case for Re/Im

(2) Giving a function from A + B to C is equivalent to giving a morphism in Set * Set from (A,B) to C, i.e., two functions: 
one from A to C and one from B to C.  

Andrei 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140511/8501e17d/attachment.html>