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

Makarius makarius at sketis.net
Mon May 10 10:39:04 CEST 2010

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.


More information about the isabelle-dev mailing list