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

[Brian Huffman]

Hello all,

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

As I recall, the old recdef package maintained its own special simpset
of recdef_simp rules for doing termination proofs. The current design
of fixrec is modeled after this style. I guess the advantage is that
the result of a "fixrec" command is more predictable, and its success
or failure is not so sensitive to changes in [simp] declarations in
other theories.

On the other hand, if I understand correctly it seems that the
function package makes a different design choice, and uses the
standard simpset for some things (like termination proofs).

So now I'm not so sure which way is better. Maybe maintaining a
separate simpset (and requiring users to know about the fixrec_simp
attribute) is more trouble than it's worth. Using the standard simpset
might introduce some extra hidden dependencies between [simp]
declarations and later fixrec definitions, but changing the simpset
does not change the theorems produced by fixrec, so maybe this is not
much of a drawback.

What do you all think?

- Brian