[isabelle-dev] Use of global simpset by definition packages

[Makarius]

On Fri, 7 May 2010, Brian Huffman wrote:

> I am looking for some advice on a design decision for the HOLCF fixrec 
> package.
>
> Fixrec uses the simplifier when doing its internal proofs of the 
> defining equations for a function. Currently it maintains its own 
> special simpset for this purpose, which users can extend by declaring 
> theorems with the [fixrec_simp] attribute. The alternative would be to 
> get rid of [fixrec_simp] and just use the main simpset from the theory 
> context (i.e. theorems declared with [simp]).

Just a technical note on this: the "main simpset" is the one from a 
regular local context, which can be retrieved via the regular Operation 
simpset_of: Proof.context -> simpset

The non-standard variant global_simpset_of: theory -> simpset is there for 
old tools that do not have a proper context available. There is also some 
system infrastructure that needs such global operations to initialize a 
certain context.

Tools and packages that have already been localized, and fixrec appears to 
be one of them, should never refer to "global" stuff from the raw 
background theory.


 	Makarius