[isabelle-dev] NEWS: avoid the Complex constructor, use the more natural
hoelzl at in.tum.de
Tue May 13 11:33:54 CEST 2014
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
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.
More information about the isabelle-dev