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

[Manuel Eberl]

Yes, but the underlying reason for that is that complex numbers are
isomorphic to pairs of real numbers, and binary product types are
"degenerate" (I would rather say very basic) co-algebraic datatypes.

So my point (and I would guess Andrei's as well) is that this really has
nothing to do with complex numbers, it is a general observation about
types that are isomorphic to product types. In particular, any algebraic
datatype with only one constructor can be rewritten into a corresponding
codatatype, allowing you to use primcorec for it.

Manuel

On 13/05/14 13:39, Lawrence Paulson wrote:
> it's not just about syntactic sugar. It seems to me that the complex
> numbers are an elegant (if degenerative) example of a co-algebraic
> datatype. The co-recursive definitions look absolutely natural to me.
> Larry
>
> On 11 May 2014, at 12:55, Andrei Popescu <uuomul at yahoo.com
> <mailto:uuomul at yahoo.com>> wrote:
>
>> 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.  
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140513/65127d37/attachment-0002.html>