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

Makarius makarius at sketis.net
Wed Sep 5 15:35:26 CEST 2012


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


More information about the isabelle-dev mailing list