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

[Florian Haftmann]

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.  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.

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.
b) I have the strong feeling that every conversion (including
Raw_Simplifier.rewrite) involving the simplifier should take an explicit
context as argument.

b) is maybe nothing to attempt before a release.  a) cannot be a final
solution but is maybe worth thinkg about.

	Florian

--

diff -r 84166a7d51bc -r 90a81561205a src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Sep 05 15:53:52 2013 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Sep 05 16:41:25 2013 +0200
@@ -1323,10 +1323,12 @@
 val simple_prover =
   SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));

-fun rewrite _ [] ct = Thm.reflexive ct
-  | rewrite full thms ct =
-      rewrite_cterm (full, false, false) simple_prover
-        (global_context (Thm.theory_of_cterm ct) empty_ss addsimps
thms) ct;
+fun with_simpset f ss ct = f (global_context (Thm.theory_of_cterm ct)
ss) ct;
+
+fun rewrite _ [] = Thm.reflexive
+  | rewrite full (thms as thm :: _) =
+      with_simpset (rewrite_cterm (full, false, false) simple_prover)
+        (empty_ss |> global_context (Thm.theory_of_thm thm) |> fold
add_simp thms |> simpset_of);

 val rewrite_rule = Conv.fconv_rule o rewrite true;

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130905/7136c874/attachment-0001.asc>