[isabelle-dev] Highlighting of locale variables
makarius at sketis.net
Fri Apr 12 16:50:28 CEST 2013
On Fri, 12 Apr 2013, Lars Noschinski wrote:
> On 12.04.2013 15:24, Makarius wrote:
>> On Fri, 12 Apr 2013, Lars Noschinski wrote:
>>> Rationale: In the locale context, these locale variables are morally
>>> constants. Somebody suggested to highlight locale variables like
>>> constants, but personally I'd prefer a highlighting similar to
>>> variables obtained or fixed in a proof (maybe a non-bold orange?).
>> Can you point to situations where this is still treated differently?
>> Such incidents are mostly coming from the depths of time, as Larry
>> usually calls this.
> I was referring to variable fixed by a locale. In the example below, "F" is
> always rendered like a free variable (i.e. blue); although it's scope is not
> the lemma, but the locale.
> locale dummy = fixes F :: 'a
> lemma "P F"
The locale is not so special here, it is just one way to start with a
context that has fixed variables already. Another one is the more recent
"context begin". As a consequence, the "F" in the lemma statement is not
treated as auto-fixable, but just as a reference to the already fixed F of
the context. Similar effects happen for structured specifications (locale
body, inductive, function etc.) and 'for' parameters.
Tools and packages are normally built in a way to have a fully official
notation that evades this implicitness of scopes, and produces a more
explicit error, i.e. like this:
lemma fixes F shows "P F"
An I agree that all this needs proper color schemes -- conforming to the
already established nuances of scoping in the bottom of the system -- and
the outcome will probably surprise many users concerning the fine points.
One reason why I did not tackle it so far is that "blueness" of variables
occurs in further situations in the local theory infrastructure that needs
>> There are certain intermediate states, like undeclared frees that are
>> implicitly fixed by the system infrastructure via "auto fix", but that
>> is slightly different.
> An oddity related to this is the let command. In the example below, "a"
> is rendered as an undeclared free. This feels wrong as writing such a
> statement seems perfectly fine, because constants and variables on the
> left hand side are generalized anyway.
> notepad begin
> let "?X a" = "1 + a"
According to the "autofix" policy, the system wrongly accepts something
that is not within proper Isar. So the hilighting gives a hint that it
should be actually rejected. The reason why undeclared frees within Isar
proof bodies are not rejected outright is to facilitate experimentation,
and explanation of proof patterns. Mizar is very difficult to convince
here -- you normally have to work with more concrete expressions, rather
than arbitrary things.
I am aware of the 'let' (and similar 'is') problem for many years, but the
traditional approach is to have a more liberal system and expect users to
know what it right (cf. "abuses non tollit usus" quoted in my PhD thesis.)
The correct way is this:
let "?X" = "%x. 1 + a"
Since the system has become so complex in the last 10 years, it seems to
require more efforts now to pin-down error situations more rigidly.
More information about the isabelle-dev