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

Manuel Eberl eberlm at in.tum.de
Tue May 13 14:11:48 CEST 2014

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.


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>

More information about the isabelle-dev mailing list