.
Andrei
On Tue, 5/13/14, Lawrence Paulson wrote:
Subject: Re: [isabelle-dev] NEWS: avoid the Complex constructor, use the more
natural
To: "Andrei Popescu"
Cc: "isabelle-dev@mailbroy.informatik.tu-muenchen.de"
Date: Tuesday, M
Am 13.05.2014 um 14:11 schrieb Manuel Eberl :
> In particular, any algebraic datatype with only one constructor can be
> rewritten into a corresponding codatatype, allowing you to use primcorec for
> it.
In fact, even (nonrecursive) datatypes with several constructors can be
rewritten into a c
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 com
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 wrote:
> The fact that one can use primco
Am Sonntag, den 11.05.2014, 04:55 -0700 schrieb 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.
>
> 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 invent
Hallo,
I stumbled across this just now and thought about it for a bit. I don't
know much about category theory, but I would say the intuitive “reason”
why complex numbers can be represented this way is the following:
1. ℂ is a field extension of ℝ with degree 2 (since it is constructed
from the ℝ
On Wed, 7 May 2014, Johannes Hölzl 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.
This is also a surprising application of primcor
* 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.
Removed theorems about the Complex constructor from the simpset, they are
available as
