Recently I’ve been doing actual theorem proving using HOL. This is a real eye-opener. Here is a summary of my first experience:
- Simple theorems can be proved just by using definitions.
- It’s not good to prove everything from definition — this makes the proof tedious.
- Some fundamental results should first be established by definition — they become theorems for proving more complex results.
This corresponds to the working mode of mathematicians. To build a theory one starts from definitions, properties, lemma, then theorems. There are many proof techniques, called tactics in HOL, and choosing the most efficient one needs a lot of experience.
Meanwhile, HOL upon loading includes some basic theories, and there is mechanism to load in more specific theories if required. Users of HOL can write up the proofs in scripts, and the Holmake utility can compile the script and generate the theory file and binary files, ready for loading so that the theorems will be available in other HOL sessions.
HOL is a very useful too, and I’m learning the basics of the tool. The HOL documentations are a big help here. I alway learn a lot by following the theory scripts provided in the source and examples.