[isabelle-dev] Raw_Simplifier.rewrite: repeated ad-hoc construction of simpset

[Makarius]

On Thu, 5 Sep 2013, Florian Haftmann wrote:

> There is a subtle issue with the simplifier concerning the recent proper
> distinction between simpsets and context.
>
> To understand, watch the following examples from axclass.ML:
>
>> fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
>> fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));
>
> The expectation was that by having e.g. … let val conv = unoverlad_conv
> thy in … end you obtain once a fully set-up rewriter.
>
> However the current implementation of Raw_Simplifier.rewrite (see patch
> below) awaits a concrete application to a cterm before actually building
> the corresponding simpset in »the« context.

I see the same dynamic building of the simpset in Isabelle2013.  But you 
are right that the full absorption of the simpset into the context has 
lead to situations that are a bit more dynamic than before, i.e. the 
simpset is produced later when the tool is applied.

In the past few months I've had several incidents of unexpected runtime 
warnings of "Ignoring duplicate rewrite rule". Often there was a genuine 
confusion of the rule lists given to certain simplifier operations, which 
I have then cleaned up to avoid duplicates.  In other situations I have 
made the building of the simpset static, such that inevitable warnings 
appear only once at compile time.


> Technically this has the bizarre consequence that if you switch on 
> tracing of the simplifier, you get a bunch of »Adding rewrite rule …« on 
> *every* invocation of (un)overload_conv.  The issue would also stay the 
> same if unoverload_conv would take a proof context as argument rather 
> than a background theory.

Is this really different from Isabelle2013?  There is a general problem of 
certain options for tracing: they tend to be "global" in the sense of tool 
composition, i.e. just spam (or even) bomb the session when switched on.

In principle one could use Context_Position.is_visible in more situations, 
but one needs to answer delicate questions about how such options for 
"invisible", "trace", "verbose" etc. should be composed.


> From studying the sources, it is obvious why Raw_Simplifier.rewrite is
> implemented like this: it needs a proper context to build a simpset on
> it, and this is most conveniently derived from the incoming cterm.
>
> I have two answers to that:
> a) The attached pragmatic patch which would build the simpset initially
> against a context derived from the theory certificate of the first
> rewrite rule and throwing that away immediately.

I have made an attempt to build simpsets for Raw_Simplifier.rewrite etc. 
in a static manner.  The standard way to guess at the corresponding global 
context is to merge all back ground theories of the theorems involved. 
This basically worked, but lead into situations where tools are not very 
precise about the background theories, and would require additional 
Thm.transfer in user-space, which is unrobust.

So I have given up that attempt for now.

Note that in some sense Raw_Simplifier.rewrite is not properly localized 
yet.  So we should definitely make another round at some point.


 	Makarius