[isabelle] 'where'-clause for defining locales

Dear all,

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. In general such a thing is
possible with:

locale bar = foo +
    fixes param_b1 :: "'v => 's"
    and param_b2 :: "'v => 's => 's"

But, if I want to unify the types of foo and bar, I get a problem:

locale bar = foo param_f1 param_f2
     for param_f1 and param_f2 :: "'s => 'v" +
     fixes param_b1 :: "'v => 's"
     and param_b2 :: "'v => 's => 's"

This now has a different order of parameters:
params_f3 … param_fn param_f1 param_f2 param_b1 param_b2

The only way to keep the order is to list all n parameters in the
import-part -- which quickly gets nasty, especially if you have a larger
locale hierarchy.

Are there any means to specify type signatures without changing the
order of arguments? Something along the lines of:

locale bar = foo where param_f2 :: "'v => 's" +
       fixes ...

(or, as 'where' is used for equations, other keywords like 'constraining')

or using the record-way (though then the question arises on how to
specify the order of the types in the annotation):

locale bar = ('v,'s) foo +
     fixes ...

Any hints are very much appreciated.


P.S.: The same problem arises, when the only parameter using all
relevant type variables is the very last one of the imported locale.

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.