Re: [isabelle] (structure) and \<index>



Hi Benedikt,

The structure mechanism was designed for use with algebraic structures represented by record types.  It has come out of fashion because records make it hard to compose structures from other structures.  For example, the construction of ring from additive and multiplicative monoid in HOL-Algebra is painful: the set of theorems for the additive monoid is duplicated manually.

The structure mechanism works as follows: an operation of a structure, such as multiplication in a group G, takes the structure record as an argument: mult G x y.  The \<index> token marks parameters implicit.  In the context of a locale the structure parameter is inserted for the \<index> parameter of the operation (if it is omitted).  That is, in locale group with parameter G (structure), mult x y is expanded to mult G x y.  This allows for concise syntax.

At the time, the structure mechanism also provided a convenient means for adding derived operations to structures.  In the meantime, definitions in locale contexts have become available, making an approach without records (and structure parameters) feasible.  For examples, see my recent paper on the semantics of locales [1] and a study on formalising groups and rings [2].  Either approach may be suitable.  If you end up having algebraic structures with many parameters, records may be of advantage.  Otherwise, the additional flexibility gained by avoiding records is a plus.

Clemens


[1] Clemens Ballarin. Locales: a module system for mathematical theories. Journal of Automated Reasoning, 2013.
[2] Clemens Ballarin. Reading an Algebra Textbook. In C. Lange et al., editors, MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, Bath UK, CEUR Workshop Proceedings 1010, 2013.
 

On 30 October, 2013 11:07 CET, bnord <bnord01 at gmail.com> wrote: 
 
> Hi all,
> 
> I was looking into the Isabelle HOL/Algebra library, as I've a student 
> who wants to do similar stuff (maybe on top of this).
> I am little bit confused about the (structure) keyword and the related 
> \<index>. They only seem to be used in this Library and the Isar 
> reference is rather brief about them also, the locales tutorial doesn't 
> mention them at all.
> 
> I have two questions about this:
> 
> 1. What is the precise semantics of these constructs? Is there some 
> documentation I've missed? The isar reference only mentions that it is 
> used for some kind of implicit references.
> 
> 2. Assuming their use is still advised and appropriate for this setting: 
> They still seem work only using the \<bsub>..\<esub> syntax which is 
> broken in the JEdit interface, is there a way to move away from this?
> 
> Best
> Benedikt
 
 
 
 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.