[isabelle-dev] Factorial ring
Manuel Eberl
eberlm at in.tum.de
Fri Mar 11 13:48:16 CET 2016
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
>
More information about the isabelle-dev
mailing list