Hing Lun Chan’s thesis (linked to in the notes below) provides pretty good documentation of the approach taken, as do the various papers arising from the work.
The short version of the story is that the “obvious” approach of working with a polymorphic type-variable to represent the type of group elements doesn’t make the task of proving the required results too arduous. Michael On 4 Feb 2021, at 01:13, Ken Kubota <m...@kenkubota.de<mailto:m...@kenkubota.de>> wrote: Is there any documentation on how abstract algebra is implemented in HOL4? Usually the HOL type system is considered too weak. Freek Wiedijk: “The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra.” John Harrison, Josef Urban, and Freek Wiedijk: “Another limitation of the simple HOL type system is that there is no explicit quantifier over polymorphic type variables, which can make many standard results [...] awkward to express [...]. [...] For example, in one of the most impressive formalization efforts to date [Gonthier et al., 2013] the entire group theory framework is developed in terms of subsets of a single universe group, apparently to avoid the complications from groups with general and possibly heterogeneous types.” https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-July/msg00074.html Kind regards, Ken Kubota ____________________________________________________ Ken Kubota https://doi.org/10.4444/100 Am 03.02.2021 um 03:47 schrieb Norrish, Michael (Data61, Acton) <michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>: Release notes for HOL4, Kananaskis-14 (Released: 3 February 2021) We are pleased to announce the Kananaskis-14 release of HOL4. New examples: * algebra: an abstract algebra library for HOL4. The algebraic types are generic, so the library is useful in general. The algebraic structures consist of monoidTheory for monoids with identity, groupTheory for groups, ringTheory for commutative rings, fieldTheory for fields, polynomialTheory for polynomials with coefficients from rings or fields, linearTheory for vector spaces, including linear independence, and finitefieldTheory for finite fields, including existence and uniqueness.
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
