Email Gateway (Aug 19 2022 at 12:15): Email Gateway (Aug 19 2022 at 12:15):From: bnord <bnord01@gmail.com>
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:
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.
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
Email Gateway (Aug 19 2022 at 12:15):From: Lars Noschinski <noschinl@in.tum.de>
On 30.10.2013 11:07, bnord 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:
- 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.
When you are inside a context where some value is marked as (structure),
this value is used to fill in the argument marked with \<index>.
If you are not inside such a context (or you want to override the
argument), you use \<bsub>..\<esub>.
- 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?
What do you mean by "broken"?
signature.asc
Email Gateway (Aug 19 2022 at 12:15):From: bnord <bnord01@gmail.com>
Hi Lars,
thanks, this corresponds to what I assumed.
But what's the influence of this "argument" it looks like it's intended
to hold different instances apart, but how?
Don't display as intended. You get two down arrows with regular size
text in between. If you have a lot of those (like in Algebra/Module for
example) it makes things really hard to read.
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:15):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Benedikt,
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.
They are also used in the archive of formal proofs and in IsaFoR/CeTA, e.g., in the Matrix entry of the AFP and in Linear_Poly...
within IsaFoR.
Perhaps these examples will be help.
Cheers,
René
(IsaFoR/CeTA can be accessed at http://cl-informatik.uibk.ac.at/software/ceta/)
Email Gateway (Aug 19 2022 at 12:17):From: Clemens Ballarin <ballarin@in.tum.de>
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.
Email Gateway (Aug 19 2022 at 12:17):From: bnord <bnord01@gmail.com>
Hi Clemens,
many thanks for these helpful clarifications. I'll look into your
references. Sounds good.
Best
Benedikt
Email Gateway (Aug 19 2022 at 12:48):From: Makarius <makarius@sketis.net>
Depends what you mean by "broken". Isabelle/jEdit still does not make any
attempt to render \<^bsub>...\<^esub> as something that looks like
subscript -- nesting would be difficult anyway. The present rendering is
not particularly pretty, but it is well-defined in what it does and what
not.
In contrast, it has required several years to make block subscripts work
half-way in Proof General / Emacs, and there were really bad incidents on
the way. So the Emacs version is the "broken" one -- it is still possible
crash the font-lock code behind it.
When Isabelle/jEdit was started around 2008, it was unclear if subscripts
would ever work, and I was ready to give up that nice-to-have feature in
exchange for some conceptual advance in prover interaction. Later I did
find some ways to render single symbols in subscript/superscript/bold in
Isabelle/jEdit, but it required so much work that doing this again for
rarely used block-subscripts will not happen so soon.
Clemens Ballarin has already pointed out that this notation is rather
old-fashioned anyway. Which does not mean the concepts behind it are
broken, but used very rarely.
Makarius
Last updated: Apr 26 2024 at 01:06 UTC