Email Gateway (Apr 04 2025 at 11:06): Email Gateway (Apr 04 2025 at 11:06):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
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.
Larry
Email Gateway (Apr 23 2025 at 19:43):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Apr 25 2025 at 11:26):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
On 23 Apr 2025, at 20:42, Makarius <makarius@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
Last updated: May 18 2025 at 04:27 UTC