From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id C81F0BB84 for ; Sat, 20 May 2006 20:16:20 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k4KIGJbP021377 for ; Sat, 20 May 2006 20:16:19 +0200 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA10843 for ; Sat, 20 May 2006 20:16:18 +0200 (MET DST) Received: from mta1.cl.cam.ac.uk (mta1.cl.cam.ac.uk [128.232.0.15]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k4KIGIbC007327 for ; Sat, 20 May 2006 20:16:18 +0200 Received: from ivatt.cl.cam.ac.uk ([128.232.8.11] helo=cl.cam.ac.uk) by mta1.cl.cam.ac.uk with esmtp (Exim 3.092 #1) id 1FhVzm-0002mS-00; Sat, 20 May 2006 19:16:10 +0100 X-Uri: To: hol-info@lists.sourceforge.net, caml-list@inria.fr Cc: John.Harrison@cl.cam.ac.uk Subject: HOL Light version 2.20 now available Date: Sat, 20 May 2006 19:16:09 +0100 From: John Harrison Message-Id: X-Miltered: at nez-perce with ID 446F5CF3.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 446F5CF2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; inference:01 bugfixes:01 integers:01 arith:01 subtraction:01 rewrites:01 abbrev:01 binary:01 indexing:01 beq:01 iterated:01 syntax:01 syntax:01 integers:01 existential:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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.