[isabelle-dev] Factorial ring

[Manuel Eberl]

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
>