[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural Re/Im view

Makarius makarius at sketis.net
Wed May 7 16:50:39 CEST 2014

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 primcorec!

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

In mathematics books / lectures there is usually some handwaving only, to 
justify why it is possible to define functions on complex by specifying 
the observation of Re/Im.


More information about the isabelle-dev mailing list