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

[Manuel Eberl]

Hello,

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.

Cheers,

Manuel