Re: [isabelle] 'where'-clause for defining locales

Am 30.06.2014 20:35, schrieb Florian Haftmann:
> Hi René,
>> given I have some locale foo with a myriad of parameters. Now I
>> want to extend this into a locale bar, which should add some
>> parameters. Also (for convenience) the new parameters should go
>> to the end and the old order of parameters should not change.
> IMHO you should consider one of these: a) What is the matter of
> your order?  To have uniform appearance of locale expressions?  In
> that case, you might consider specification of parameters by
> *name*.  See the Isar reference manual for the syntactic details.

Ah, I wasn't aware that I can also use the where-clause in locale
specifications. This actually turns out to be (nearly) what I want: If
one specifies the _last_ parameter with a 'where'-clause, also the
order is kept the same (of course, this is only useful when all
necessary type variables are part of it):

locale bar = foo
    where param_fn = param_fn
    for param_fn :: "..." +

> b) If you really want to have structural control, consider grouping
> your parameters to records.  HOL-Algebra is a nice example how this
> is accomplished in practice.

Our "problem" arose from the fact that we had to abolish our setup
with records, as this gave rise to other problems with multiple
inheritance (if locale A specifies record rA
and locale B has record rB = rA + B_ext
and locale C has record rC = rA + C_ext
and I now want to have a locale BC which implements both B and C, I am
stuck, as I can't have a record rBC = rB + rC)

> Hope this helps,

It did, thanks!

- René

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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