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

[Johannes Hölzl]

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.
> 
> >> Makarius wrote:
> >> That is indeed very nice.  Is that a new invention or an old trick
> that every category theorist knows?

I do not count myself a category theorist (I don't know what a functor
adjunction is). As Manuel pointed out, the change was mostly a
bureaucratic one.
It boils down to the fact that the Re/Im rules should match more often.

For example assume one wants to proof:

  "Complex a b + cis x + Complex c d = cis x + Complex (c + a) (b + d)"

(where "cis x = cos x + i * sin x")

With complex_eq_iff and the Re/Im rules this can be proved by
field_simps, even without giving Re/Im rules for cis. When we only have
the Complex rules, this does not work, we need either to do a case-split
on "cis x", or unfold cis_def. 

 - Johannes