Email Gateway (Aug 18 2022 at 15:38): Email Gateway (Aug 18 2022 at 15:38):From: Peter Gammie <peteg42@gmail.com>
Hello,
This doesn't work as one might hope:
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...
cheers
peter
Email Gateway (Aug 18 2022 at 15:38):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 15:38):From: Makarius <makarius@sketis.net>
On Tue, 13 Jul 2010, Peter Gammie wrote:
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"
begintypes Type = "'a set"
It is not a construct that copes with things that are already fixed in a
context.
You can consider this limitation as an accidental feature of the current
implementation. Trying a bit harder in the internal structures, one could
support type parameters on the RHS one day. It is a very important
principle to base a system on assumptions that are as weak as possible, to
leave room for continued unfolding of the concepts behind it. Exploiting
the inability for type parameters on the RHS now would limit the future
growth of the system.
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?
I promise to mention something like that in the next tutorial on Isar that
should come forward this year.
On the other hand we have a bit too many manuals that are often in an
inconsistent state, while many things that I find myself explaining again
and again are written in the "reference manuals" collection -- these 3 are
in fact mostly up to date: isar-ref, implementation, system.
Maybe the next generation of user interfaces needs to tell users directly
about thing that are better avoided, or point to relevant sections of the
manuals via formal references in the text.
Makarius
Email Gateway (Aug 18 2022 at 15:39):From: Peter Gammie <peteg42@gmail.com>
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
Last updated: Apr 26 2024 at 12:28 UTC