I make quite a lot of use of recursion theorems to enable various kinds of recursive definitions to be proven consistent automatically.
The facilities provided in ProofPower are designed to support recursive definitions over recursive datatypes, in which every element of the type is obtained using some constructor and functions are defined using pattern matching. Because I work in set theory (in HOL) there are recursion principles I use for defining functions over arbitrary sets not obtained using any constructor. If I produce a corresponding recursion theorem, in the required format except for the lack of a constructor, this is accepted by the system (by add_%exists%_cd_thms, and by evaluate_%exists%_cd_thm) without complaint, but the consistency proofs for corresponding recursive definitions don't happen. This can be fixed by putting in a fake constructor, CombI will do, so the definitions then go though so long as you put CombI in the definition. I'm curious to know whether this is the intended behaviour (I don't remember anything about this at the time it was being implemented) and if there is any obvious way I can avoid having to put "CombI" in my recursive definitions. Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
