[isabelle-dev] Highlighting of locale variables

[Makarius]

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
> begin
>
> lemma "P F"
> oops
> -----------

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 
further looking.


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

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.


 	Makarius