Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
To: info-hol@edu.uidaho.cs.ted
Subject: **** RELEASE OF HOL 2.01 ****
Date: Mon, 07 Dec 92 18:33:03 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"nene.cl.ca.133:07.12.92.18.33.08"@cl.cam.ac.uk>


This is to announce the release of HOL88 Version 2.01 ("classic" HOL).

The version incorporates a number of bugfixes and new features, but changes in
the proof system from 2.0 are relatively few in number. However the new release
includes several major new libraries. There is also a lot of new stuff in
"contrib"; a separate message concerning "contrib" will be posted shortly.

The changes felt most likely to affect users' proofs are:

o Renaming of REWRITE_CONV to REWR_CONV (see below); there is an entry "newrw"
  in "contrib" to update code with respect to this change.

o Changes to MATCH_MP so it may add quantifiers and pick variants which did not
  appear before.

o Changes to functions underlying STRIP_TAC and relatives may cause different
  variable-priming behaviour.

From a practical point of view, your attention is drawn to the following two
directories in "contrib":

o AKCL-mods - this contains a hol-init.ml file to improve the garbage
  collection performance of HOL when built under AKCL, by increasing certain
  allocations. (John Van Tassel).

o non-unix - contains files to build HOL on PCs and Macs. (John Carroll)

HOL 2.01 may be obtained by FTP from Cambridge or Idaho as before:

  ftp.cl.cam.ac.uk [128.232.0.56] in directory "hvg/hol"

  ted.cs.uidaho.edu [129.101.100.20] in directory "pub/hol"

The two main files are "holsys.tar.Z" and "holdoc.tar.Z", which are
compressed tarfiles of, respectively, the hol system (i.e. code, theories)
and the hol documentation (help files and stuff to build the manuals).
There are other odds and ends available too, mostly concerned with
particular LISPs.

More details of changes in this version are appended below.

Answers to queries and requests for more information, or help with problems in
getting hold of HOL, may be received by emailing:

  hol-support@cl.cam.ac.uk

or by contacting me personally (see details below). Delivery of HOL on magnetic
tape can be arranged for users without FTP access.

Regards,

  John Harrison (jrh@cl.cam.ac.uk)

  Hardware Verification Group
  University of Cambridge Computer Laboratory
  New Museums Site
  Pembroke Street
  Cambridge CB2 3QG
  England.

  Phone: +44 223 334760
  Fax:   +44 223 334678

=============================================================================
New theorems include the following:

* Theorems about ordering and multiplication

   LESS_LESS_CASES =    |- !m n. (m = n) \/ m < n \/ n < m
   GREATER_EQ =         |- !n m. n >= m = m <= n
   LESS_EQ_CASES =      |- !m n. m <= n \/ n <= m
   LESS_EQUAL_ADD =     |- !m n. m <= n ==> (?p. n = m + p)
   LESS_EQ_EXISTS =     |- !m n. m <= n = (?p. n = m + p)
   NOT_LESS_EQUAL =     |- !m n. ~m <= n = n < m
   LESS_EQ_0 =          |- !n. n <= 0 = (n = 0)
   MULT_EQ_0 =          |- !m n. (m * n = 0) = (m = 0) \/ (n = 0)
   LESS_MULT2 =         |- !m n. 0 < m /\ 0 < n ==> 0 < (m * n)
   LESS_EQ_LESS_TRANS = |- !m n p. m <= n /\ n < p ==> m < p
   LESS_LESS_EQ_TRANS = |- !m n p. m < n /\ n <= p ==> m < p

* Theorems about division

   ZERO_DIV = |- !n. 0 < n ==> (0 DIV n = 0)

* Theorems about the factorial function

   FACT =               |- (FACT 0 = 1) /\
                           (!n. FACT(SUC n) = (SUC n) * (FACT n))
   FACT_LESS =          |- !n. 0 < (FACT n)

* Theorems about evenness and oddity

   EVEN =               |- (EVEN 0 = T) /\ (!n. EVEN(SUC n) = ~EVEN n)
   ODD =                |- (ODD 0 = F) /\ (!n. ODD(SUC n) = ~ODD n)
   EVEN_ODD =           |- !n. EVEN n = ~ODD n
   ODD_EVEN =           |- !n. ODD n = ~EVEN n
   EVEN_OR_ODD =        |- !n. EVEN n \/ ODD n
   EVEN_AND_ODD =       |- !n. ~(EVEN n /\ ODD n)
   EVEN_ADD =           |- !m n. EVEN(m + n) = (EVEN m = EVEN n)
   EVEN_MULT =          |- !m n. EVEN(m * n) = EVEN m \/ EVEN n
   ODD_ADD =            |- !m n. ODD(m + n) = ~(ODD m = ODD n)
   ODD_MULT =           |- !m n. ODD(m * n) = ODD m /\ ODD n
   EVEN_DOUBLE =        |- !n. EVEN(2 * n)
   ODD_DOUBLE =         |- !n. ODD(SUC(2 * n))
   EVEN_ODD_EXISTS =    |- !n. (EVEN n ==> (?m. n = 2 * m)) /\
                               (ODD n ==> (?m. n = SUC(2 * m)))
   EVEN_EXISTS =        |- !n. EVEN n = (?m. n = 2 * m)
   ODD_EXISTS =         |- !n. ODD n = (?m. n = SUC(2 * m))

Strengthening of existing theorems

* The theorem INV_PRE_LESS was

   |- !m n. 0 < m /\ 0 < n ==> ((PRE m) < (PRE n) = m < n)

  and has now been strengthened to

   |- !m. 0 < m ==> (!n. (PRE m) < (PRE n) = m < n)

New general functions and facilities

* MAP2: maps a curried binary function down a pair of lists

* The environment variable HOLPATH allows simple communication with other
  programs

* Libraries may now be divided into sections which can be loaded separately

* Functions are provided to print terms and types without surrounding quotes.

New proof functions

* APPEND_CONV: conversion to append lists

* GSYM: version of SYM which works within quantifiers etc.

* MAP_CONV: conversion to map function over a list

* A consistent set of filtered rewriting rules and tactics, e.g.
  FILTER_PURE_ASM_REWRITE_TAC.

* A collection of rewriting conversions consistent with the rules and tactics
  (the former REWRITE_CONV has been renamed REWR_CONV).

Changes and bugfixes to existing functions

* install now sets the help search path correctly

* RES_CANON now avoids capture when dealing with bound variables of the
  same name.

* The set_goal and g functions check the terms they are given are
  booleans.

* EXT now works if the quantified variable is free in the assumptions

* MATCH_MP will rearrange quantifiers and pick variants

Changes to existing libraries

* Library sets fully documented

* Library pred_sets substantially rewritten and documented

* Some new theorems added to the set libraries

New libraries

* wellorder: versions of the Axiom Of Choice, including the Well-ordering
  theorem. (John Harrison)

* latex-hol: tools for incorporating HOL output in Latex. (Wai Wong)

* abs_theory: implementation of abstract theories. (Phil Windley)

* reals: definitional theory of real numbers. (John Harrison)

* arith: decision procedure for subset of linear arithmetic. (Richard Boulton)

* UNITY: theory from "Parallel Program Design - A Foundation" (Flemming
  Andersen)

* pair: functions for dealing with paired quantification, abstraction
  etc. (Jim Grundy)
=============================================================================