[isabelle-dev] types and locales

[ballarin at in.tum.de]

Quoting Makarius <makarius at sketis.net>:

> Looks like their is still a problem with implicitly fixed variables in
> locale expressions.

No.  The problem here is that in

> locale r1 =
>  r0 "init :: 'buffer \<Rightarrow> ('buffer \<times> 'value) set =>   
> 'value" +  fixes d2i :: "('buffer \<times> 'buffer) \<Rightarrow>   
> 'buffer"

init is lost as a parameter of the locale!  This is immediate from
Isabelle's output after the declaration:

    locale r1 =
     fixes immediate :: "'buffer * 'buffer => bool"
       and d2i :: "'buffer * 'buffer => 'buffer"

Technically speaking,

    r0 "init :: 'buffer \<Rightarrow> ('buffer \<times> 'value) set => 'value"

is an instantiation of r0 (even if the instantiation term is just a
type constraint).  If the variable init occuring in the instantiation
term is to be a locale parameter, this needs to be declared.
Makarius' solution does just the right thing:

> locale r1 =
>   r0 "init :: 'buffer => ('buffer \<times> 'value) set => 'value" for init
>   + fixes d2i :: "('buffer \<times> 'buffer) => 'buffer"

Now the parameter is restored (as is visible in Isabelle's output):

    locale r1 =
      fixes immediate :: "'buffer * 'buffer => bool"
        and init :: "'buffer => ('buffer * 'value => bool) => 'value"
        and d2i :: "'buffer * 'buffer => 'buffer"
      assumes "r1 immediate"

In order to retain the original order of the parameters, try

    locale r1 = r0 _ "immediate :: 'buffer * 'buffer => bool" for immediate +
      fixes d2i :: "('buffer \<times> 'buffer) \<Rightarrow> 'buffer"

In this context, cf the relevant NEWS entry:

   - In locale expressions, instantiation replaces renaming.  Parameters
   must be declared in a for clause.  To aid compatibility with previous
   parameter inheritance, in locale declarations, parameters that are not
   'touched' (instantiation position "_" or omitted) are implicitly added
   with their syntax at the beginning of the for clause.

Clemens