This page will likely evolve.
The HOL system currently doesn't allow for this model of work very well. Part of the reason for this is that script files for HOL inter-mingle ML (which is the theorem-prover's implementation language) and embedded bits of logic. We would like to check the logic without having to be able to parse (and execute) ML as well.
Therefore, the aim of this project is to design a simple file format in which users could write ``ML-less HOL'', and to then implement at least two tools for manipulating this format. The first tool would be the type-checker. It would make sure that the definitions and other logical material in the file actually made sense at the level of types. The second tool would do all this and also produce a genuine HOL theory, using the various facilities already present in HOL.
If this all went well, there would be ample opportunity to extend this project so that it also included a declarative proof (as opposed to just definition) element.
FACT(SUC n) = (SUC n) * FACT(n)(i.e., that the factorial of a number greater than zero is equal to
that number multiplied by the factorial of the number one less), then
we can rewrite a term such as FACT(SUC 6) to SUC 6
* FACT(6). However, at this point, the rewriter can't make any
more progress, because it doesn't recognise 6 as an instance of
SUC n for some variable n. (The representation
of the numeral 6 is not just a chain of SUCs applied to
0; this representation would be very inefficient.) In order to be
able to make progress, we need to prove that there exists a number
m such that 6 = SUC m.
Similarly, if we know that
for some functions f and g, then we would have to prove that a number was even before we could apply the rewrite. Note also that this procedure would ideally work with more than just numerals. If we have as context that x > 10, then we could do quite a bit of rewriting with x!, maybe all the way to
A project to investigate this idea would probably proceed by first implementing a simple rewriting system over arithmetic terms. This system would then need to be extended with access to an arithmetic decision procedure that could figure out the various supporting theorems. I can provide one of these. If you can find your own arithmetic decision procedure, this project could be done in any language. My d.p. is in SML, and you would almost certainly have to write the rest of the project in SML too.
Alternatively, and for extra kudos, the whole project could be done in HOL. Here the basic rewriting system is already provided, but there would be quite a bit (probably even, a lot) of hard work involved in learning the HOL system.