[isabelle-dev] "set_comprehension_pointfree" simproc losing bounds

[Lukas Bulwahn]

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.


Lukas
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121022/fbfa7fa8/attachment-0002.html>