[isabelle-dev] Problems with more rigorous check of simplifier context

[Makarius]

On Sat, 20 Jul 2013, Florian Haftmann wrote:

> I stumbled over a problem with
> http://isabelle.in.tum.de/repos/isabelle/rev/9ec2d47de6a7 and static
> code conversions.
>
> In static code conversions, it happens routinely that the cterm to which
> the conversion is applied to stems from a different (but subsequent)
> theory than the theory from the context of its construction.  See the
> attached theory for a minimal example which actually only invokes pre-
> and postprocessor.
>
> This breaks in #9ec2d47de6a7 with »rewrite_cterm: bad background theory«.

That change belongs to the full localization of the Simplifier that I did 
some weeks ago.  There is no longer anything special about type simpset 
from the past -- you just invoke the Simplifier with "the" context, i.e. 
the one you have at run-time of a certain tool.  So it should be a context 
from a super-theory of everything involved in the process.

I was half expecting problems with codegen side-entries to the Simplifier, 
but it should work out nonetheless.  You need to avoid hard-wired 
(Simplifier.global_context thy) -- it would have to transferred to the 
run-time theory before invoking simplification.

Instead of transfer, it is usually easier not to store such a Simplifier 
context at all, but only its inner data content, which is accessible via 
simpset_of and put_simpset.  E.g. see this example here:

http://isabelle.in.tum.de/repos/isabelle/annotate/06653152ea8b/src/HOL/HOL.thy#l1997


The idea is as follows:

   * use the compile-time @{context} to build up a certain simpset
     (the full context is required for operations like addsimps to work);

   * store its simpset_of;

   * at tool run-time put_simpset that into "the" context;


 	Makarius