[isabelle-dev] [OT] Checked "assume" command

[Makarius]

On Wed, 5 Sep 2012, Lawrence Paulson wrote:

> I'm only talking about cases where “show" must inevitably fail. 
> Fortunately, such situations are rare, but if they can easily be 
> detected, they should be. Larry
>
> On 5 Sep 2012, at 14:20, Lars Noschinski <noschinl at in.tum.de> wrote:
>
>> On 05.09.2012 15:13, Lawrence Paulson wrote:
>>> Fixing a variable that ought to be free is an error.
>>>
>>> Highlighting is useful, but you have to be quite alert to notice it. I 
>>> seldom notice it except in really blatant situations, like the same 
>>> variable highlighted in two different ways. If the context is simply 
>>> wrong, the highlighting should be absolutely unmissable.
>>
>> Indeed, a variable shadowed by mistake is quite hard to detect. But is there a clear rule whether a variable "ought to be free"? Shadowing has its legitimate use cases (e.g. I usually shadow the "n" in induction proofs on the naturals).

With the "case that must fail" we are getting back to the tendencies of 
this thread: 
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-May/002736.html
where I failed to explain basic observations how warnings and errors get a 
slightly different meaning in the Prover IDE model.

Concerning fixes (and implicit type abstractions) you know my basic plan 
already: highlight the situation in the source text in a way that tells 
the user what is there, and the user can then see by himself if it is what 
he had in mind or should have in mind.


 	Makarius