[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.

Thanks,
René

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.