[isabelle-dev] Redefinition of group.ord in 042ae6ca2c40

[Lawrence Paulson]

I did this, incorporating the HOL Light definition.

The purpose of old_ord is simply to ease the transition. I’m hoping to get rid of it soon.

Algebra needs a huge amount of tidying up. In particular, we have both comm_group and abelian_group, but the latter is about rings!

Larry

> On 6 Apr 2019, at 14:23, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
> I see that the definition of the order of a group element was re-defined
> in 042ae6ca2c40. This change is good; something like that has been on my
> to-do list. But: if we are changing it now, we should also think about
> what to return for elements that have infinite order. At the moment,
> this case is simply underspecified.
> 
> I think it would make sense to simply return 0. This is also the choice
> that is made in Pocklington.ord in HOL-Number_Theory, which is a kind of
> specialised instance of group.ord. Since no element can ever "really"
> have otder 0, this choice does not clash with anything else.
> 
> By the way, a perhaps simpler way to write the definition would be to
> use GCD, i.e. "ord a = Gcd {n | n > 0 /\ a [^] n = 1}". If the set is
> empty, the result is automatically 0. Not sure if this actually saves
> any work when proving the derived properites of "ord" (it might), but
> it's certainly a nicer definition than using Hilbert choice.
> 
> I also noticed that an "old_ord" constant was introduced. I must lobby
> to get rid of this before the release. Such things (in German we would
> say "Altlasten") have a tendency to accumulate, become half-forgotten,
> and annoy people for years to come (remember Old_Number-Theory? ;) )
> 
> I wish I could do more than just complain and actually help with
> cleaning this up, but I am currently in hospital and cannot really work
> on anything of this magnitude.