I agree in principle, but putting up a hierarchy of algebraic structures within the constraints of Isabelle's type class system is tricky. Additionally, sometimes adjustments have to be made since some things that are natural in ‘regular’ mathematics are awkward to express in a theorem prover.

For instance, Florian explained to me that working with an equivalence relation like associatedness (i.e. two elements divide each other) is tedious in Isabelle, whereas working with equations is easy. Therefore, introducing a "normalisation" operation that essentially picks one distinguished representative from that equivalence class (e.g. the non-negative one in case of integers, the monic one in case of polynomials) and expressing associatedness as "normalize x = normalize y" makes things a lot easier.


In principle, what I would like is to have a full stack of algebraic structures in HOL-Algebra and a full stack of algebraic structures as type classes built on top of that, but I don't think that's going to happen.

I think the best approach at the moment is to gradually flesh out the existing hierarchy (like Florian and I have already done with Euclidean rings) in a way that works well in practice and see where that leads us.


Manuel


On 11/03/16 13:39, Tjark Weber wrote:
Florian,

On Thu, 2016-03-10 at 14:01 +0100, Manuel Eberl wrote:
"multiplicity" is definitely interesting [...]
I don't see why is_prime should require an algebraic_semidom [...]
Factorial rings (also known as unique factorisation domains) usually
[...]
[...] (somewhat non-standard) normalization_semidom.
My general impression is that it would be good if the algebraic
hierarchy that is part of standard Isabelle/HOL could follow standard
mathematical definitions and nomenclature more closely.

Best,
Tjark


_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to