[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural Re/Im view
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