[isabelle-dev] Warning "Simplifier: renamed bound variable" (was "set_comprehension_pointfree" simproc losing bounds

[Lukas Bulwahn]

On 10/22/2012 08:22 AM, Lukas Bulwahn wrote:
> On 10/19/2012 04:35 PM, Makarius wrote:
>> On Fri, 19 Oct 2012, Lukas Bulwahn wrote:
>>
>>>> Operations like Simplifier.context, Simplifier.inherit_context 
>>>> should help here.  Once that is repaired, I will see if the warning 
>>>> can now be made an error that is more explicit about the reasons.
>>>>
>>> I am certainly in favour of this. First, tool developers mainly 
>>> react on errors with test runs, but do not see the warnings. 
>>> Secondly, users do not know who to report those warnings and do not 
>>> know if they are caused by their scripts or the tools.
>>
>> Historically, the weak warning was a necessity due to too many 
>> simprocs still not working with the context.
>>
>> Let's hope that it can be easily switched to an explicit error after 
>> so many years now.
>>
> On the weekend, I had a look at this issue in the 
> set_comprehension_pointfree simproc (cf. changeset 6250121bfffb) and 
> already noticed what could make things difficult turning this into an 
> error.
>
> Two examples:
> - the hypsubst_tac internally uses the simplifier, but the interface 
> does not allow to pass the current simpset to this tactic.
> - An implementer has to avoid certain functions, such 
> asRaw_Simplifier.rewrite, that assume to be used only in a non-nested 
> context.
>
>
I had a further look at the issue with the "Simplifier: renamed bound 
variable" to repair the set_comprehension_pointfree simproc and to turn 
the warning into an error for the future.

However, I was very surprised that the warning occurs even if I pass 
around the context following typical Isabelle programming idioms.
To state my expectation more formally:
For every simpset ss and ss', I would expect

Simplifier.context (Simplifier.the_context ss) ss' == 
Simplifier.inherit_context ss ss'

Attached, there is an simple example that shows a warning for 
"Simplifier.context (Simplifier.the_context ss)", but it does not for 
Simplifier.inherit_context ss.

Looking at the code of the simplifier, I did understand my misunderstanding:
It is NOT ONLY "working with the context" correctly, but also "passing 
around the simpset" correctly---a programming paradigm that I (and 
probably many others) are not aware of.


Lukas

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121108/7657d83f/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Scratch.thy
Type: application/isabelle-theory
Size: 1759 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121108/7657d83f/attachment.bin>