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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
