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

[Florian Haftmann]

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

Agree.

	Florian

-- 

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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130916/eeeea04e/attachment.sig>