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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
