HOL Light version 2.20 now available

HOL Light version 2.20 now available

[John Harrison]

I'm pleased to announce the release of version 2.20 of the HOL
Light theorem prover, available now from the HOL Light homepage:

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

Since the last release, the system has been cleaned up, with many
"internal" functions deleted or hidden. There is now a reference
manual, available as crosslinked HTML or as a single PDF file, that
documents all the inference rules, conversions, tactics and utility
functions defined in the system:

  http://www.cl.cam.ac.uk/users/jrh13/hol-light/reference.html

Besides this consolidation and documentation, there are several new
features, improvements and bugfixes. Those I consider most important
are listed below.

John.

MOST SIGNIFICANT CHANGES
------------------------

 * Better infrastructure for the integers including automation
   of divisibility properties (more details below).

 * Much improved performance of ARITH_RULE on problems with many
   instances of cutoff subtraction.

 * Much improved performance of the ring and field functions on
   large problems.

 * Generalized beta conversion (e.g. (\(x,y). x + y) (1,2) = 1 + 2)
   is now built into the default "rewrites"

 * Online help is available (do ``help "ident";;'')

 * Type abbreviations are supported (see "new_type_abbrev")

 * Binary numerals are also accepted ("0b101010")

 * "define_finite_type", for defining indexing types, has been
   added.

MOST ANNOYING INCOMPATIBLE CHANGES
----------------------------------

Two constant name changes:

  dest_int -> real_of_int
  mk_int   -> int_of_real

the renaming of these utility functions:

  is_beq                -> is_iff
  [dest|is|mk]_intconst -> [dest|is|mk]_realintconst
  upto                  -> --
  gather                -> filter

and the following theorem renamings (some others about iterated
operations had a few redundant hypotheses removed)

 [N]SUM_CMUL -> [N]SUM_LMUL (and there's an _RMUL version too)


NEW INTEGER SUPPORT
-------------------

The type `:int` was formerly a poor relation of `:num` and `:real`, with
rather less in the way of syntax operations and automated support. This
has mostly changed. There are now syntax operations like "mk_intconst",
arithmetic conversions like "INT_ADD_CONV" and "INT_REDUCE_CONV" and an
instantiation of the ring procedure, "INT_RING".

The most basic divisibility notions "divides", "coprime" and "gcd" have
been defined on both integers and natural numbers in the core. Few
lemmas about them have been provided, but there are some very useful
(though hacky and brittle) automated proof procedures that can
generate many routine lemmas about divisibility notions automatically:
NUMBER_RULE and NUMBER_TAC (over the natural numbers) and INTEGER_RULE
and INTEGER_TAC (over the integers). For example, over the natural
numbers:

  NUMBER_RULE `coprime(x * y,x EXP 2 + y EXP 2) <=> coprime(x,y)`;;

  NUMBER_RULE `!d a b:num. d divides (a * b) /\ coprime(d,a) ==> d divides b`;;

  NUMBER_RULE `~(gcd(a,b) = 0) /\ a = a' * gcd(a,b) /\ b = b' * gcd(a,b)
               ==> coprime(a',b')`

  NUMBER_RULE `!a x y:num.
         coprime(a,n) ==> ((x * a == y * a) (mod n) <=> (x == y) (mod n))`;;

Over the integers, even some existential goals can be solved, e.g. the
2-variable Chinese remainder theorem. This works less well over the
natural numbers because of the positivity constraints, though I plan to
fix this eventually:

  INTEGER_RULE
   `!a b u v:int. coprime(a,b) ==> ?x. (x == u) (mod a) /\ (x == v) (mod b)`;;

  INTEGER_RULE
   `gcd(a,n) divides b ==> ?x:int. (a * x == b) (mod n)`;;

NEW EXAMPLES/LIBRARIES
----------------------

  Examples/binary.ml       --- binary expansion of numbers
  Examples/combin.ml       --- combinatory logic (port of old HOL88 example)
  Examples/ste.ml          --- basic Symbolic Trajectory Evaluation theory
  Multivariate/clifford.ml --- multivectors with outer and geometric product
  100/*.ml                 --- Some of the "great 100 theorems"

The last bunch of examples are HOL Light formalizations of some of the
theorems from the following list:

  http://www.cs.ru.nl/~freek/100/

I believe that all the ones done in HOL Light are either in this
directory or somewhere in the standard core or libraries.