The HOL Light theorem prover (moved from Google code)
Standard ML OCaml Makefile TeX C Shell
Switch branches/tags
Nothing to show
Clone or download
jrh13 Called out more explicitly the carefully chosen defaults for DIV/MOD …
…with

zero (DIV_ZERO and MOD_ZERO) and using those streamlined quite a number
of DIV, MOD and congruence theorems to remove nonzeroness hypotheses:

        CONG
        CONG_LMOD
        CONG_MOD
        CONG_RMOD
        COPRIME_MOD
        DIVIDES_MOD
        DIVISION_SIMP
        DIV_0
        DIV_DIV
        DIV_LE
        DIV_MOD
        MOD_0
        MOD_ADD_MOD
        MOD_EQ_0
        MOD_EXP_MOD
        MOD_LE
        MOD_MOD
        MOD_MOD_REFL
        MOD_MULT
        MOD_MULT2
        MOD_MULT_CONG
        MOD_MULT_LMOD
        MOD_MULT_MOD2
        MOD_MULT_RMOD
        MOD_NSUM_MOD
        MOD_NSUM_MOD_NUMSEG
        MOD_REFL
        MULT_DIV_LE

sharpening the hypothesis of these

        DIV_MULT2
        DIV_MONO

and indicdentally adding missing quantifiers to

        DIV_EQ_EXCLUSION

On the other hand simply removed DIVIDES_DIV which is now even more
clearly subsumed by DIVIDES_MOD. Also added a few more theorems in
this area as well as more topology (NORMAL_SPACE_DISJOINT_CLOSURES
etc.) and basic results about the notion of polar dual in convexity.
New definition:

        polar_dual

and theorems:

        CLOSED_IN_CONNECTED_COMPONENTS_OF
        CLOSED_IN_CONNECTED_COMPONENT_OF
        CLOSED_POLAR_DUAL
        CONG_DIV
        CONG_SOLVE_EQ
        CONG_SOLVE_LT_EQ
        CONNECTED_COMPONENT_OF_MONO
        CONVEX_POLAR_DUAL
        DIV_ZERO
        EL_MAP2
        EXISTS_CONNECTED_COMPONENT_OF_SUPERSET
        EXISTS_PATH_COMPONENT_OF_SUPERSET
        HOMEOMORPHIC_MAP_CLOSURE_OF
        HOMEOMORPHIC_MAP_DERIVED_SET_OF
        HOMEOMORPHIC_MAP_FRONTIER_OF
        HOMEOMORPHIC_MAP_INTERIOR_OF
        HOMEOMORPHIC_MAP_SEPARATION
        MOD_LE_TWICE
        MOD_UNIQUE
        MOD_ZERO
        NORMAL_SPACE_DISJOINT_CLOSURES
        PATH_COMPONENT_OF_MONO
        POLAR_DUAL
        POLAR_DUAL_0
        POLAR_DUAL_ANTIMONO
        POLAR_DUAL_CBALL
        POLAR_DUAL_EMPTY
        POLAR_DUAL_POLAR_DUAL
        POLAR_DUAL_POLAR_DUAL_EQ
        POLAR_DUAL_POLAR_DUAL_GEN
        POLAR_DUAL_SCALING
        POLAR_DUAL_SING
        POLAR_DUAL_UNION
        POLAR_DUAL_UNIT_CBALL
        POLAR_DUAL_UNIV
        num_INDUCTION_DOWN
Latest commit 92e0cff Jul 16, 2018
Permalink
Failed to load latest commit information.
100 Added a new file "Library/grouptheory.ml" with a basic development of Sep 11, 2017
Arithmetic Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
Boyer_Moore Proved the excision property for singular homology, including the Oct 30, 2017
Complex Made a small recoding of a phrase that OCaml has started treating as Jan 16, 2017
Examples Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
Formal_ineqs copyright info for Formal_ineqs Oct 5, 2017
Functionspaces Made a radical spring-clean of the general topology and other areas. Mar 17, 2017
Help Added two new functions contributed by Michael Faerber: "type_unify" May 14, 2018
IEEE Eliminated a number of duplicated theorems (often exact duplicates, Aug 28, 2017
IsabelleLight copyright and license for IsabelleLight Oct 9, 2017
Jordan Eliminated a number of duplicated theorems (often exact duplicates, Aug 28, 2017
LP_arith Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
Library Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
Minisat Added a number of Multivariate theorems, including a definition of Mar 26, 2017
Mizarlight Fixed two remaining compatibility issues with OCaml 4.00, namely Sep 10, 2012
Model Made changes essentially corresponding to the steps of hol-online's Mar 25, 2010
Multivariate Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
Ntrie Added a complete revision from Marco Maggesi of the "Ntrie" library Sep 25, 2017
Permutation Removed the still extant files from the old logical kernel (type.ml, Feb 22, 2016
Proofrecording Defined the notion of relative boundary (hom_relboundary) and hence Mar 26, 2018
QBF Added Ondrej Kuncar's code for constructing proofs of quantified May 27, 2012
Quaternions Eliminated a number of duplicated theorems (often exact duplicates, Aug 28, 2017
RichterHilbertAxiomGeometry clear executable bits on non-executable files Sep 27, 2017
Rqe Eliminated a number of duplicated theorems (often exact duplicates, Aug 28, 2017
Tutorial Made a small recoding of a phrase that OCaml has started treating as Jan 16, 2017
Unity Added a few additional theorems: Apr 23, 2012
miz3 Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
CHANGES Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
LICENSE Added a few additional theorems: Apr 23, 2012
Makefile Incorporated Michael Faerber's improved "update_database.ml" file Nov 20, 2017
QUICK_REFERENCE.txt Initial checkin Feb 13, 2010
README Updated the build instructions; John O'Leary pointed out that OCaml Dec 4, 2017
VERYQUICK_REFERENCE.txt Initial checkin Feb 13, 2010
arith.ml Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
basics.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
bool.ml Improved REAL_FIELD and COMPLEX_FIELD so they do a somewhat better job Oct 9, 2016
calc_int.ml Made a small recoding of a phrase that OCaml has started treating as Jan 16, 2017
calc_num.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
calc_rat.ml Added a miscellany of new theorems, finishing off the suite of Jun 12, 2017
canon.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
cart.ml Added quite a few theorems, all fairly straightforward and many in Apr 17, 2017
class.ml Made a small recoding of a phrase that OCaml has started treating as Jan 16, 2017
database.ml Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
define.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
doc-to-help.sed Initial checkin Feb 13, 2010
drule.ml Added two new functions contributed by Michael Faerber: "type_unify" May 14, 2018
equal.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
fusion.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
grobner.ml Added a definition and suite of basic theorems for yet another topolo… Jun 19, 2017
help.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
hol.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
holtest Added two new functions contributed by Michael Faerber: "type_unify" May 14, 2018
holtest.mk Added two new functions contributed by Michael Faerber: "type_unify" May 14, 2018
holtest_parallel Added a new parallel version of holtest from Hendrik Tews, which is Jan 12, 2014
impconv.ml Added a couple of generic "iterate" versions of theorems already Jan 8, 2017
ind_defs.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
ind_types.ml Made a small recoding of a phrase that OCaml has started treating as Jan 16, 2017
int.ml Finally integrated the singular homology material into the main Mar 19, 2018
itab.ml Moved more hol-online changes upstream, adding explicit "needs" Mar 8, 2010
iterate.ml Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
lib.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
lists.ml Called out more explicitly the carefully chosen defaults for DIV/MOD … Jul 16, 2018
make.ml Initial checkin Feb 13, 2010
meson.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
metis.ml Added a couple of generic "iterate" versions of theorems already Jan 8, 2017
nets.ml Moved more hol-online changes upstream, adding explicit "needs" Mar 8, 2010
normalizer.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
nums.ml Eliminated a number of duplicated theorems (often exact duplicates, Aug 28, 2017
pa_j_3.07.ml Initial checkin Feb 13, 2010
pa_j_3.08.ml Initial checkin Feb 13, 2010
pa_j_3.09.ml Initial checkin Feb 13, 2010
pa_j_3.1x_5.xx.ml Ondrej Kuncar pointed out that the system doesn't build with the new Dec 3, 2010
pa_j_3.1x_6.02.1.ml Added (directly from Ondrej Kuncar) an updated version of pa_j for the Feb 9, 2011
pa_j_3.1x_6.02.2.ml Kevin S. Van Horn reported in "Issue 2" another problem with the Apr 2, 2011
pa_j_3.1x_6.11.ml Made some changes suggested by Randy Pollack so that HOL Light makes use Nov 7, 2015
pa_j_3.1x_6.xx.ml Ondrej Kuncar pointed out that the system doesn't build with the new Dec 3, 2010
pa_j_4.xx_7.xx.ml Made some changes suggested by Hendrik Tews to support the new Aug 4, 2017
pair.ml Eliminated a number of duplicated theorems (often exact duplicates, Aug 28, 2017
parser.ml Further developed the singular homology theory, actually introducing Oct 9, 2017
preterm.ml Improved REAL_FIELD and COMPLEX_FIELD so they do a somewhat better job Oct 9, 2016
printer.ml Added a patch to the prettyprinter from Marco Maggesi that ensures May 15, 2017
quot.ml Moved more hol-online changes upstream, adding explicit "needs" Mar 8, 2010
real.ml Updated the build instructions; John O'Leary pointed out that OCaml Dec 4, 2017
realarith.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
realax.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
recursion.ml Based on an idea discussed with Mark Adams, changed Oct 23, 2011
sets.ml Added some new material about groups, including a definition of the Jan 29, 2018
simp.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
system.ml Added a new library by Mohamed Yousri Mahmoud and Vincent Aravantinos Oct 6, 2014
tactics.ml Made a small recoding of a phrase that OCaml has started treating as Jan 16, 2017
theorems.ml Systematically renamed instances of "&" to "&&" and "or" to "||" to a… Sep 12, 2016
trivia.ml Moved more hol-online changes upstream, adding explicit "needs" Mar 8, 2010
update_database_3.ml Incorporated Michael Faerber's improved "update_database.ml" file Nov 20, 2017
update_database_4.ml Incorporated Michael Faerber's improved "update_database.ml" file Nov 20, 2017
wf.ml Added an actual topological "dimension" function for Euclidean space … Oct 31, 2016

README

                             HOL LIGHT

HOL Light is an interactive theorem prover / proof checker. It is
written in Objective CAML (OCaml) and uses the toplevel from OCaml as
its front end. This is the HOL Light homepage:

        http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html

and this is the root of the Github code repository:

        https://github.com/jrh13/hol-light

Basic installation instructions are below. For more detailed information
on usage, see the Tutorial:

        http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf

Refer to the reference manual for more details of individual functions:

        http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.html (HTML files)
        http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf (one PDF file)

        *       *       *       *       *       *       *       *

                             INSTALLATION

If you use Debian Linux or some other Debian-based Linux distribution
(Knoppix, Mint, Ubuntu, etc.), there is actually a "hol-light" package,
thanks to Hendrik Tews, so installation of HOL Light and all its
prerequisites is as simple as

  sudo apt-get install hol-light

For other OSs, more work is involved. The Objective CAML (OCaml)
implementation is a prerequisite for running HOL Light. HOL Light
should work with any recent version of OCaml; I've tried it on at
least 3.04, 3.06, 3.07+2, 3.08.1, 3.09.3, 3.10.0, 3.11.2 and 4.00.
However, for versions >= 3.10 (in 3.10 there was an incompatible
change in the camlp4 preprocessor) you will also need to get camlp5
(version >= 4.07). Installing both items of software should not be too
difficult, depending on the platform.

 1. OCaml: there are packages for many Linux distributions. For
    example, on a debian derivative like Ubuntu, you may just need
    to do the following:

        sudo apt-get install ocaml

    Alternatively you can download binaries directly, or get sources
    and build them (which in my experience is usually trouble-free).
    See the OCaml Web page for downloads and other information.

        http://caml.inria.fr/ocaml/index.en.html

    The HOL Light system uses the OCaml "Num" library for rational
    arithmetic. As of OCaml 4.06, this is no longer included in
    the core system and will need to be added separately. You can
    do this using the OCaml package manager "opam" if you use it by

        opam install num

    Alternatively you can download the sources from here

        https://github.com/ocaml/num

    and build and install them following the instructions on that
    page, for example

        git clone https://github.com/ocaml/num mynums
        cd mynums
        make all
        sudo make install [assuming no earlier errors]

 2. camlp5: this is needed to run HOL Light under any OCaml >= 3.10.
    Somtimes you need a recent version of camlp5 to be compatible with
    your OCaml. I recommend downloading the sources for a recent
    version from

        https://camlp5.github.io/

    and building it in "strict" mode before installing it, thus:

        cd software/camlp5-rel701 [or wherever you unpacked sources to]
        ./configure --strict
        make
        sudo make install       [assuming no earlier errors]

    There are also packages for camlp5, so you may be able to get away
    with just something like

        sudo apt-get install camlp5

    However, you may get a version in "transitional" instead of
    "strict" mode (do "camlp5 -pmode" to check which you have).

Now for HOL Light itself. The instructions below assume a Unix-like
environment such as Linux [or Cygwin (see www.cygwin.com) under
Windows], but the steps automated by the Makefile are easy enough to
invoke manually. There's more detail on doing that in the Tutorial.

(0) You can download the HOL Light sources from the Github site.
    For example, the following will copy the code from the trunk of the
    Github repository into a new directory 'hol-light':

        git clone https://github.com/jrh13/hol-light.git

    The above is now the recommended way of getting HOL Light. There
    are also gzipped tar files on the HOL Light Web page, but they are
    only for quite old versions and will probably be difficult to use
    with recent versions of OCaml.

    You should next enter the 'hol-light' directory that has been
     created:

        cd ./hol-light

There are now two alternatives: launch the OCaml toplevel and directly
load the HOL Light source files into it, or create a standalone image
with all the HOL Light sources pre-loaded. The latter is more
convenient, but requires a separate checkpointing program, which may not
be available for some platforms. First the basic approach:

(1) Do 'make'. This ought to build the appropriate syntax extension
    file ('pa_j.cmo') for the version of OCaml that you're using. If you
    have the camlp4 or camlp5 libraries in a non-standard place rather
    than /usr/local/lib/ocaml/camlp4 or /usr/local/lib/ocaml/camlp5
    then you may get an error like this

      Error while loading "pa_extend.cmo": file not found in path.

    in which case you should add the right directory to CAMLP4LIB or
    CAMLP5LIB, e.g.

      export CAMLP5LIB=$HOME/mylib/ocaml/camlp5

(2) Do 'ocaml'. (Actually for OCaml >= 4.02 I prefer 'ocaml -safe-string'
    to avoid mutable strings, while you may need something else like
    'ocamlnum' on some platforms --- see [*] below.) You should see a
    prompt, something like:

                Objective Caml version 4.01.0

        #

(3) At the OCaml prompt '#', do '#use "hol.ml";;' (the '#' is part of the
    command, not the prompt) followed by a newline. This should rebuild
    all the core HOL Light theories, and terminate after a few minutes
    with the usual OCaml prompt, something like:

        val search : term list -> (string * thm) list = <fun>
        - : unit = ()
        File "help.ml" already loaded
        - : unit = ()
        - : unit = ()
        - : unit = ()
                Camlp5 parsing version 7.03

        #

    HOL Light is now ready for the user to start proving theorems. You
    can also use the load process (2) and (3) in other directories, but
    you should either set the environment variable HOLLIGHT_DIR to point
    to the directory containing the HOL source files, or change the
    first line of "hol.ml" to give that explicitly, from

        let hol_dir = ref (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;

    to, for example

        let hol_dir = "/home/johnh/hol-light";;

    or

        let hol_dir = "/usr/share/hol";;

Now for the alternative approach of building a standalone image.
The level of convenience depends on the checkpointing program you
have installed. The earlier checkpointing programs in this list
are more convenient to use but seem less easy to get going on
recent Linux kernel/libc combinations.

(1) If you have the 'ckpt' program installed, then the Makefile will
    conveniently create a HOL Light binary. You can get 'ckpt' here:

        http://www.cs.wisc.edu/~zandy/ckpt/

    Once 'ckpt' is installed, simply type

        make hol

    in the 'hol-light' directory, and a standalone HOL Light image
    called 'hol' should be created. If desired you can move or copy
    this to some other place such as '~/bin' or '/usr/local/bin'. You
    then simply type 'hol' (or './hol') to start the system up and
    start proving theorems.

    Note that although the HOL binary will work on its own, it
    does not pre-load all the source files. You will probably want
    to keep the sources available to be loaded later as needed (if
    you need additional mathematical theories or tools), so it's
    better to unpack the HOL distribution somewhere permanent
    before doing 'make hol'.

    If you later develop a large body of proofs or tools, you can
    save the augmented system using the command "self_destruct"
    (this is the same approach as in the Makefile) rather than
    re-load each time. For example, the following will create a
    HOL Light binary (always called 'hol.snapshot'):

        self_destruct "My version of HOL Light";;

(2) Another checkpointing option is CryoPID, which you can get
    here:

        http://cryopid.berlios.de/

    In this case, the Makefile doesn't have a convenient way of
    making HOL binaries, but you can make one yourself once HOL
    Light is loaded and you are sitting in its toplevel loop.
    (This also works if you have your own extensions loaded, and
    indeed this is when it's most useful.) Instead of the
    'self_destruct' command, use 'checkpoint', which is similar
    except that the current process is not terminated once the
    binary (again called hol.snapshot) is created:

        checkpoint "My version of HOL Light";;

(3) A third option which seems to work with recent Linuxes is
    DMTCP, which you can download from here:

      http://dmtcp.sourceforge.net/

    You may try installing from the packages (e.g.
    'sudo dpkg -i dmtcp.deb'), but I found it was better to
    compile from source. HOL Light does not have convenient
    commands or scripts to exploit DMTCP, but you can proceed
    as follows:

        1. Start ocaml running under the DMTCP coordinator:

              dmtcp_checkpoint -n ocaml

        2. Use ocaml to load HOL Light as usual, for example:

              #use "hol.ml";;

        3. From another terminal, issue the checkpoint command:

             dmtcp_command --checkpoint

        4. (Don't forget this!) Kill the original ocaml process,
           e.g. by just typing control-d to the Ocaml prompt.

        5. Step 3 created a checkpoint of the OCaml process and
           a shell script to invoke it, both in the directory in
           which ocaml was started. Running that should restore
           the OCaml process with all your state and bindings:

             ./dmtcp_restart_script.sh

(4) If none of these options work, you may find some others on the
    following Web page. Unfortunately I don't know of any such
    checkpointing program for either Windows or Mac OS X; I would
    be glad to hear of one.

        http://checkpointing.org

The directories "Library" and "Examples" may give an idea of the
kind of thing that might be done, or may be useful in further work.

Thanks to Carl Witty for help with Camlp4 porting and advice on
checkpointing programs.

        *       *       *       *       *       *       *       *

[*] HOL Light uses the OCaml 'num' library for multiple-precision
rationals. On many platforms, including Linux and native Windows, this
will be loaded automatically by the HOL root file 'hol.ml'. However,
OCaml on some platforms (notably Cygwin) does not support dynamic
loading, hence the need to use 'ocamlnum', a toplevel with the 'num'
library already installed. You can make your own with:

    ocamlmktop -o ocamlnum nums.cma