I make quite a lot of use of recursion theorems to enable
various kinds of recursive definitions to be proven
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
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.
Proofpower mailing list