[isabelle-dev] Raw_Simplifier.rewrite: repeated ad-hoc construction of simpset
florian.haftmann at informatik.tu-muenchen.de
Mon Sep 16 19:08:27 CEST 2013
>> 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.
>> 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.
Generally, I did not undertake a thorough comparision with Isabelle2013,
just an »as it is« analysis.
> Note that in some sense Raw_Simplifier.rewrite is not properly localized
> yet. So we should definitely make another round at some point.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 261 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev