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