HOL Light version 2.20 now available
 John Harrison
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060520 (18:16) 
From:  John Harrison <John.Harrison@c...> 
Subject:  HOL Light version 2.20 now available 
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/hollight/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/hollight/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 [destismk]_intconst > [destismk]_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 2variable 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.