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

Reply via email to