Re: [isabelle] locales and 'types'
On Tue, 13 Jul 2010, Peter Gammie wrote:
locale X =
fixes a :: "'a"
(* 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
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
BTW, you can see the same effect as above here for term parameters:
locale foo = fixes x :: 'a
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
* 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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and