Re: [isabelle] locales and 'types'



On Tue, 13 Jul 2010, Peter Gammie wrote:

theory t
imports Main
begin

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

(* This is fine *)
types 'b Type = "'b set"

(* This should be fine too *)
types 'a Type = "'a set"

*** Locally fixed type arguments "'a" in type declaration "Type"
*** At command "types" ...

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"?


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.


BTW, you can see the same effect as above here for term parameters:

  locale foo = fixes x :: 'a
  begin

  lemma fixes x shows "x = x" ..

  *** Duplicate fixed variable(s): "x"


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


	Makarius





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