[isabelle] Type variable names in inherited locales



Hi all,

When deriving a locale, say locale B = A + something, the type variables of A will be renamed to 'a,'b, ... for use in B. Can this behaviour be changed to keep the names of the type variables unless there are name clashes, or is there a good reason for this renaming ? The current behaviour makes referring to type variables of imported locales not really readable. Currently, I'm inserting constrains-statements as a workaround, but this may get tedious with many types or locales.

Example:

 locale DPN =
   fixes D :: "('Q\<times>'\<Gamma> list) set"
 begin
   (* Everything fine:
   locale DPN =
     fixes D :: "'Q \<times> '\<Gamma> list \<Rightarrow> bool"
   *)
 end

 locale DPN1 = DPN
 begin
   (* Types renamed to 'a and 'b:
   locale DPN1 =
     fixes D :: "'a \<times> 'b list \<Rightarrow> bool"
   *)
 end

 (* Workaround: *)
 locale DPN2 = DPN +
   constrains D :: "('Q\<times>'\<Gamma> list) set"
 begin
   (* Everything fine again:
   locale DPN2 =
     fixes D :: "'Q \<times> '\<Gamma> list \<Rightarrow> bool"
   *)
 end






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