*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Natural expression of group theory – Re: abelian_group*From*: Ken Kubota <mail at kenkubota.de>*Date*: Sat, 13 Apr 2019 13:53:14 +0200*Cc*: Manuel Eberl <eberlm at in.tum.de>*In-reply-to*: <cab8db41-0746-f1c2-f5bf-d6f7a5bae524@in.tum.de>*References*: <A80C58ED-7E98-4574-9A67-7CA0259B6885@cam.ac.uk> <cab8db41-0746-f1c2-f5bf-d6f7a5bae524@in.tum.de>

For a natural expression of group theory type abstraction should be implemented, as suggested by Mike Gordon: "[…] 'second order' λ-terms like λ𝛼. λx:𝛼. x, perhaps such terms should be included in the HOL logic." [Gordon, 2001, p. 22] With type abstraction the mechanism of lambda notation can be used to _syntactically_ express the dependencies (here between the term and the type level), which follows the very idea of type theory. See also: http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/ https://sourceforge.net/p/hol/mailman/message/35458077/ (section 5) For a demonstration of an implementation (PDF) run make group.r0.out.pdf && open -a Preview $_ make xor_group.r0.out.pdf && open -a Preview $_ For a demonstration of an implementation (HTML) run make group.r0.out.html && open -a Safari $_ make xor_group.r0.out.html && open -a Safari $_ on a Mac after downloading the software (license restrictions apply) at http://doi.org/10.4444/100.10.3 PDF generation requires Pandoc with LaTeX installed, and HTML view will cause a call to mathjax.org as the JavaScript display engine for mathematics. Kind regards, Ken Kubota ____________________________________________________ Ken Kubota http://doi.org/10.4444/100 > Am 12.04.2019 um 18:20 schrieb Manuel Eberl <eberlm at in.tum.de>: > > HOL-Algebra is a bit messy. A big part of that, I think, comes from > quirks of Isabelle/HOL itself. > > My guess would be that one can write groups either additively (G, +, 0) > or multiplicatively (G, *, 1). Of course, more abstract syntax (G, ∘, e) > is also possible. There are various conventions about when to use which > notation – in particular, I think the convention is that if you use "+", > the group is always commutative (i.e. abelian). > > In HOL-Algebra, groups are /always/ written multiplicatively. There is > no other way. When you have a ring, you can write "+" for addition, but > that is not formally associated to any group. The additive group of the > ring has all its properties stated w.r.t. the "*" of "add_monoid R". > > "abelian_group" is apparently some kind of attempt to have an abelian > group that is written additively. Due to the fact that the "+" operator > is defined for the ring record, this requires us to use a ring record > even though there is (in general) no multiplication operation. We also > don't have any locale assumption that this "ring record" is an actual > ring (i.e. fulfils the ring axioms). Just the addition operation in it > is required to form an abelian group. > > As for why this strange "abelian_group" locale exists, I cannot say. One > would have to examine where it is used and what for. > > I agree that it's all very confusing. Maybe it is simply the case that > this ad-hoc "single-inheritance record" "locale with structure > parameters" is just fraught with problems. But as far as I know, it's > the only way we have in Isabelle to do abstract algebra, and I don't > know of a better one. Unless we can find a way to emulate the more > modular typeclass/implicit parameter approach and elaborators that > systems like Coq and Lean have. > > Manuel > > > On 12/04/2019 17:01, Lawrence Paulson wrote: >> A notable peculiarity of Algebra is its locale abelian_group, which is based on comm_group (groups with commutative multiplication) but with the weird twist of requiring a ring; it appears to be, in reality, the specification that a ring’s addition operator is commutative. Except that all rings have this property, and the very existence of this locale is confusing. Does anybody know any more about this? >> >> Larry >> >> record 'a ring = "'a monoid" + >> zero :: 'a ("𝟬ı") >> add :: "['a, 'a] ⇒ 'a" (infixl "⊕ı" 65) >> >> abbreviation >> add_monoid :: "('a, 'm) ring_scheme ⇒ ('a, 'm) monoid_scheme" >> where "add_monoid R ≡ ⦇ carrier = carrier R, mult = add R, one = zero R, … = (undefined :: 'm) ⦈" >> >> locale abelian_monoid = >> fixes G (structure) >> assumes a_comm_monoid: >> "comm_monoid (add_monoid G)" >> >> locale abelian_group = abelian_monoid + >> assumes a_comm_group: >> "comm_group (add_monoid G)" >> >> >

**References**:**[isabelle] abelian_group***From:*Lawrence Paulson

**Re: [isabelle] abelian_group***From:*Manuel Eberl

- Previous by Date: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)
- Next by Date: [isabelle] Algebraic rule collections
- Previous by Thread: Re: [isabelle] abelian_group
- Next by Thread: Re: [isabelle] abelian_group
- Cl-isabelle-users April 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list