New OCaml version of HOL Light theorem prover

New OCaml version of HOL Light theorem prover

[John Harrison]

I'm pleased to announce the availability of the HOL Light theorem prover
version 2.0, based on Objective Caml. The system and its documentation,
including a new draft tutorial, can be downloaded from the following Web
page:

  http://www.cl.cam.ac.uk/users/jrh/hol-light

HOL Light proves theorems in classical higher-order logic. It is intended
as an interactive proof assistant, but offers automated support for
proofs in some domains (arithmetic, algebra, pure logic...) and has a
significant library of pre-proved mathematics, particularly elementary
analysis. The system is designed to be fully programmable; not only is
OCaml the implementation language but the OCaml toplevel is the "shell"
from which the user directs proofs. Here are the proofs of a few
extremely simple theorems in the system, just to show you what it looks
like.

1. The sum of squares of the first n natural numbers, by induction and
   arithmetic:

   let SUM_OF_SQUARES = prove
    (`!n:num. nsum(1..n) (\i. i * i) = (n * (n + 1) * (2 * n + 1)) DIV 6`,
     INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;

2. Vector version of Pythagoras's theorem, using algebra on vectors and real
   numbers:

   needs "Multivariate/vectors.ml";;

   let PYTHAGORAS = prove
    (`!A B C:real^2.
           orthogonal (A - B) (C - B)
           ==> dist(A,C) pow 2 = dist(B,A) pow 2 + dist(B,C) pow 2`,
     SIMP_TAC[dist; NORM_POW_2; orthogonal; DOT_LSUB; DOT_RSUB; DOT_SYM] THEN
     CONV_TAC REAL_RING);;

3. Los's "non-obvious" theorem of predicate calculus, using pure
   first-order reasoning.

   let LOS = prove
    (`(!x y z. P x y /\ P y z ==> P x z) /\
      (!x y z. Q x y /\ Q y z ==> Q x z) /\
      (!x y. P x y ==> P y x) /\
      (!x y. P x y \/ Q x y)
      ==> (!x y. P x y) \/ (!x y. Q x y)`,
     MESON_TAC[]);;

The ASCIIfied logical symbols used above include:

 !x.    for all x
 /\     and
 \/     or
 ==>    implies
 \x.    lambda x (like "fun x ->" in OCaml)

John.