A common style of hol90 interaction is for the user to work with the SML top-level loop. This loop reads input until a complete phrase has been found, then evaluates the phrase, then prints out the result before resuming its wait for input. Let us start our proof work with a classic example:
All men are mortal; Socrates is a man; therefore, Socrates is mortal.
How might this argument be represented in hol90? We start by entering our terms. In order to make the interaction more clear, we are going to first turn off some specialized printing support:
term_pp_prefix := ""; term_pp_suffix := "";In the following, the dash (-) is the SML/NJ system prompt. Everything that follows on that line is user input, ending with the semicolon.
- val men_are_mortal = string_to_term "!(x:ind). Man x ==> Mortal x"; val men_are_mortal = `!x. Man x ==> Mortal x` : termThe contents of the second line is what SML has printed back as the value of the input phrase. Let's look at the input phrase: it binds the name men_are_mortal with the value of invoking the term parser (string_to_term) on the string "!(x:ind). Man x ==> Mortal x". This may be read aloud as For all x of type individual, Man x implies Mortal x. The exclamation mark (!) stands for the universal quantifier, and the ==> symbol stands for the material implication. The identifiers Man and Mortal stand for predicates. HOL is a typed logic; the type ind of individuals is one of its primitive types.
SML prints out the binding and tells us that is has type term. The second term in our argument is introduced in much the same way as the first:
- val socrates_is_a_man = string_to_term "(Man:ind->bool) Socrates"; val socrates_is_a_man = `Man Socrates` : termThe subexpression (Man :ind -> bool) constrains the predicate Man to belong to a certain type; the expression is read as Man has type individual to bool. Now we can make the argument. It goes in three steps: we assume our terms, and then make use of a version of modus ponens that uses matching to find the correct instantiation.
- val th1 = ASSUME men_are_mortal; val th1 = . |- !x. Man x ==> Mortal x : thm - val th2 = ASSUME socrates_is_a_man; val th2 = . |- Man Socrates : thm - MATCH_MP th1 th2; val it = .. |- Mortal Socrates : thmNotice that the bindings th1, th2, and it are all of type thm. This means that they represent theorems of the HOL logic. When these values are printed out, there are "dots" to the left of the turnstile (|-): these are the assumptions. We can discharge these:
- DISCH_ALL it; val it = |- Man Socrates ==> (!x. Man x ==> Mortal x) ==> Mortal Socrates : thmUsing SML, we can package all this work up into one phrase and evaluate it (incidentally, without adding any new top-level bindings, except for the final theorem):
- MATCH_MP (ASSUME (Parse.string_to_term "!x:ind. Man x ==> Mortal x")) (ASSUME (Parse.string_to_term "(Man:ind->bool) Socrates")); val it = .. |- Mortal Socrates : thm
Note. Ending a session with SML/NJ, and hence hol90, is done by entering the end-of-file character (^D).
This example was a trivial example of reasoning in HOL. However, the essence of the system has been demonstrated: theorems of the HOL logic are proved by applying rules of inference, which are ML functions. Theorem proving is just functional programming!
The technology in HOL scales up remarkably well: some of the largest proofs performed to date have been done in hol90. Such efforts make common use of quite sophisticated reasoning tools, but these tools are always composed from simple inference rules such as those we have demonstrated here.