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 <[email protected]> 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. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
