A useful inductive data type ty with negative occurrences like ty -> bool in the arguments of its constructors can have a set-theoretic interpretation when the negative occurrence models only finite sets. The HOL code proves the necesarry theorems we need in order to be able to add such a data types manually to HOL using equivalence sets. More specifically, the data type added to HOL:

ty = SET ty -> bool 
| NUM num 
| LIST (ty)list 
| TREE (ty)ltree

Code Download:

• For Taupo 6
• For HOL90.7

Documentation/papers:

T.E.J. Vos and S.D. Swierstra, Inductive data types with negative occurences in HOL, Workshop on Thirty Five years of Automath, Edinburgh, UK, April 2002.