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