Re: [isabelle] locales and 'types'



On 13/07/2010, at 7:03 PM, Makarius wrote:

>> Can the implementation be tweaked to account for variable shadowing? I have too many type variables not to use them conventionally...
> 
> What do you mean by "not to use them conventionally"?

Oh, just what you mean below.

> When introducing locally fixed parameters (either for types or terms) the outcome needs to be unique, i.e. something that is fixed already in the context cannot be fixed again.  There are two different context policies to achieve this: (1) within a proof body parameters are implicitly renamed, (2) for toplevel specifications and statements non-unique names are rejected.
> 
> Renaming at the toplevel is ruled out for general simplicity and sanity reasons, otherwise we would reintroduce very strange effects that we had before the current infrstructure of specifications within a local context was introduced.

OK.

I find this reasoning a bit confusing for "types" as 'a cannot be used in the RHS anyway, i.e. this is illegal too:

locale X =
  fixes a :: "'a"
begin

types Type = "'a set"

It is not a construct that copes with things that are already fixed in a context.

> One more note on the example above.  In order to avoid unnecessary confusion and unexpected problems, it is important to stick to established Isabelle naming conventions:
> 
>  * Theory names: capitalized words, typically describing the main concept
>    in singular, e.g. "theory Foo_Bar_Concept"
> 
>  * Almost everything else in lower case, especially locale and type
>    names.
> 
>  * Exceptions: capitalized datatype constructors, also some term
>    constructions according to typical mathematical usage (e.g. capital
>    singleton letters A, B, C, or occasional Foo for "sets" etc.)

Could I humbly suggest that these and other style rules be put in a document that accompanies the distribution?

Thanks!

cheers
peter

-- 
http://peteg.org/






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