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

[Alexander Krauss]

Hi Brian,

Here are my thoughts:

- The termination prover uses the global simpset (clasimpset actually), 
since I explicitly want it to pick up lemmas from the user. In practice, 
I have never seen a termination proof break because of a bad simp rule 
declared by the user. However, there is alse the possibility to declare 
rules [termination_simp] that should be used *only* in termination 
proofs. So the termination prover uses a superset.

- The core of the function package should never use the global simpset, 
since it should be completely deterministic, and the user cannot declare 
extra rules (The problem with the warning that you pointed out is 
actually a violation of this rule, which I think should not be there).

- I think one should be particularly careful when the actual result of 
some package (like the format of some rules) and not just success or 
failure is influenced by declarations. [fundef_cong] is such a case. In 
this case, it should really be a separate declaration, because otherwise 
the dependencies get really strange.

What proofs are you considering?


> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev