legacy_Complex_simps

[Lawrence Paulson]

> On 23 Apr 2025, at 20:42, Makarius <makarius at sketis.net> wrote:
> 
> On 04/04/2025 13:06, Lawrence Paulson via isabelle-dev wrote:
>> Can anybody explain why all of the lemmas about the complex constructor “Complex" have been shoved into this lemma list, legacy_Complex_simps?
>> There is seemingly a view to push users into writing complex expressions in the form x + iy, which looks nice in a mathematics textbook but is certain to complicate reasoning where the real and imaginary parts are dealt with separately.
> 
> The Isabelle sources follow the principle that "the history is the proof for the state of the text". Here is the relevant changeset from 07-May-2014 by Johannes Hölzl: https://isabelle-dev.sketis.net/rISABELLE48a745e1bde7
> 
> Maybe you can make sense from that.

This looks like a massive and mostly positive change, namely to express the complex numbers as a codatatype. It also quite sensibly removes the default simprule going from x + iy to Complex x y. Nevertheless, when doing algebraic calculations, the Complex x y form is the practical choice.

The commit msg is "avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex”. 

Larry