1<HTML> 2<HEAD> 3<TITLE>Release Notes for Kananaskis-1 version of HOL 4</TITLE> 4</HEAD> 5 6<BODY bgcolor=white> 7<H1>Notes on HOL 4, Kananaskis-1 release</H1> 8 9It has been a long time since our last major release. Progress has 10been made on many fronts. The HOL system has become easier to use, 11and it has grown a lot as well. Our goal continues to be the provision 12of a leading-edge research platform suitable for 13 14<UL> 15<LI> formalizing mathematics, 16<LI> verifying hardware and software, and 17<LI> constructing custom proof tools. 18</UL> 19 20And now the news. 21<P> 22<HR> 23 24<H2>Change of Base</H2> 25 26We have moved our base of operations to SourceForge. 27<PRE> 28 http://sourceforge.net/projects/hol/ 29</PRE> 30The (very nice) facilities available at SourceForge have enabled the HOL 31developers, who are currently scattered over three countries, to keep 32reasonable control over a continually changing system. SourceForge also 33provides a convenient place from which to distribute the system. Ordinary 34users can even grab incremental updates and bugfixes, rather than 35waiting for upcoming releases. 36<P> 37 HOL is an open system, and we welcome those keen to play a role in its 38continuing evolution. There are many ways in which one might take part 39in HOL development. It is <EM>not</EM> necessary to have a deep knowledge of 40HOL (or even logic) in order to make a contribution. If you are 41interested, please send us an email. 42 43<P><HR> 44 45<H2>Documentation Improved</H2> 46 47 Much new documentation has been written, especially for heavily 48used proof tools. Existing documentation has been spruced up, and there 49is a new interface to it. The HOL Reference Page, located in the distribution 50at 51<PRE> 52 <holdir>/help/HOLindex.html 53</PRE> 54gives organized access to 55 56<UL> 57<LI> libraries (source) 58<LI> theories (proved theorems, scripts, and theory map) 59<LI> proof support (documentation and links to source) 60<LI> an index of all identifiers in the system, with links to sources 61</UL> 62 63<P><HR> 64<H2>New Examples</H2> 65 66 67<UL> 68<LI> <strong>ARM6</strong> -- 69 Anthony Fox has formalized version 6 of the Acorn Risc 70 Machine and completed a proof of its correctness. 71<P> 72 73<LI><strong>Sugar2</strong> -- 74 Mike Gordon has deeply embedded Sugar 2.0, the Accellera 75 standard property language. 76 77<P> 78<LI> <strong>miller</strong> -- 79 Joe Hurd has completely formalized an argument for the 80 correctness of the Miller-Rabin probabilistic primality 81 test. Also included are some cute smaller examples using 82 probability. 83<P> 84 85<LI> <strong>Rijndael</strong> -- 86 Konrad Slind has formalized and proved the functional 87 correctness of Rijndael, the new AES crypto algorithm. 88 89<P> 90<LI> <strong>root2</strong> -- 91 A short introductory example showing that the square root 92 of 2 is irrational. Adapted from a proof of John Harrison. 93</UL> 94 95 96<P><HR> 97<H2>New and improved proof tools</H2> 98 99<UL> 100<LI> Another complete decision procedure for full Presburger arithmetic 101 over the integers and natural numbers, the <em>Omega Test</em>, has been 102 implemented. It is usually faster than Cooper's algorithm, but 103 problems that require significant work in converting the input to 104 DNF can cause it to take much longer. The Omega Test is available 105 in <kbd>intLib</kbd> as <kd>intLib.ARITH_CONV</kbd>. 106<P> 107<LI> Induct and Induct_on have been improved to deal with mutually 108 recursive datatypes, thanks to code written by Peter Homeier. 109<P> 110<LI> Hol_datatype's definition of large "enumerated types" (data types 111 with only nullary constructors) is now much more efficient than 112 it used to be. 113<P> 114 115<LI> There is a new (simple) interface provided to the "call-by-value" 116 rewriter. bossLib.EVAL and bossLib.EVAL_TAC "evaluate" terms and 117 goals respectively using a global set of rewrite theorems. This 118 set is updated as theories load, so that running "functional 119 programs" in the logic should often be as simple a matter as 120 writing (for example) 121<PRE> 122 EVAL ``FACT 6`` 123</PRE> 124 and getting back 125<PRE> 126 > val it = |- FACT 6 = 720 : thm 127</PRE> 128 Definitions made with Define also automatically update this global 129 set of rewrites. There is support for monitoring EVAL and its kin, 130 and for controlling the depth of its expansions. 131<P> 132 133<LI> The system now maintains a "stateful" simpset that is updated 134 automatically as theories and libraries load, and as new types are 135 defined. It can be accessed in the module BasicProvers or 136 bossLib, with the function 137<PRE> 138 srw_ss : unit -> simpset 139</PRE> 140 The access to type information (constructor injectivity and 141 disjointness) duplicates the functionality provided by RW_TAC, but 142 use of srw_ss has the advantage that other theorems and behaviours 143 are also available automatically. For example, when pred_setLib 144 is loaded, the srw_ss() simpset is extended with all 145 pred_setTheory's "obvious rewrites", things like 146<PRE> 147 |- FINITE (P UNION Q) = FINITE P /\ FINITE Q 148</PRE> 149 as well as the SET_SPEC_CONV conversion which does the right thing 150 with 151<PRE> 152 x IN { ... | ... } 153</PRE> 154 terms. There is also an RW_TAC equivalent, SRW_TAC which uses 155 this simpset and also implements RW_TAC's aggressive stripping and 156 normalisation strategies. 157<P> 158 159<LI> Permutative rewriting now has a kinder interface. Previously the 160 simplifier cared about the order of the submitted (A,C) theorems, 161 and required them to be fully specialized. No longer! Permutative 162 rewrite sets can now be easily built with simpLib.ac_ss. 163<P> 164 165<LI> Much attention has been paid to efficiency problems arising from big 166 terms (ranging to those with hundreds of thousands or millions of 167 connectives and bound variables). We have not solved the problem of 168 scale, but we have been able to remedy some serious bottlenecks. These 169 improvements have generally been backwards compatible, but have also 170 required some new (experimental) primitives. Consult the 171 hol-developers discussion list at SourceForge for further 172 information. 173</UL> 174 175<P><HR> 176<H2>New libraries</H2> 177 178<UL> 179<LI> The library HolSatLib (http://www.cl.cam.ac.uk/~mjcg/HolSatLib/) 180 provides a very simple harness for invoking SAT solvers on HOL 181 terms. Currently SATO, GRASP and ZCHAFF are supported. HolSatLib has 182 only been tested under Linux, though it should be possible to run it 183 under Windows. 184<P> 185 186<LI> The library word32Lib comprises a functor (called "wordFunctor") 187 for creating word theories. It also provides word32Theory (see below), 188 plus an evaluation conversion "WORD32_CONV". 189</UL> 190 191<P><HR> 192<H2>New and improved theories</H2> 193 194<UL> 195<LI> Laurent Thery's theories of divisibility, primality, and gcd are 196 now part of the distribution, under the name dividesTheory, 197 primeTheory and gcdTheory. 198<P> 199 200<LI> A theory of 32-bit machine arithmetic, due to Anthony Fox, 201 available under the name word32Theory. The theory defines many 202 of the `integer' operations found in computer architectures. It 203 was developed in modelling the ARM instruction set. The operations 204 can be grouped as follows: 205 206<UL> 207<LI> Bit-field testing and extraction; 208<LI> Arithmetic: Addition, Subtraction, Multiplication and Two's 209 Complement; 210<LI> Logical: One's Complement, Bitwise And, Or and Exclusive Or; 211<LI> Shifts: Logical Right, Arithmetic Right, Rotate Right, and 212 Rotate Right One Place with Carry Extension. 213</UL> 214<P> 215 Theorems are provided for reasoning about bit-fields, as well as 216 arithmetic (Commutative Ring properties) and the logical 217 operations (Boolean Algebra properties). A number of rewrite 218 rules are also provided, and these support fairly efficient term 219 evaluation using WORD32_CONV (or EVAL). 220<P> 221 The functor <strong>wordFunctor</strong> can be used to create 222 bespoke word theories. For example, a theory of 8-bit words can be 223 obtained by the invocation 224<PRE> 225 structure word8Theory = wordFunctor (val bits = 8) 226</PRE> 227 228<LI> A replacement theory of strings over an alphabet of 256 characters 229 has been provided. String literals are no longer implemented as an 230 infinite set of constants, given meaning by mk_thm; instead, they 231 are constructed terms. This removes the last use of mk_thm in the 232 HOL system. Note however, that this new theory is not backwards 233 compatible: it will break code that treats string literals as 234 constants. 235<P> 236 237<LI> A small theory of set-theoretic fixpoints, due to Michael Norrish. 238 239<P> 240<LI> A small theory supporting relatively efficient definitional CNF, due 241 to Joe Hurd. 242<P> 243 244<LI> A small theory of container types, offering maps between lists, 245 finite sets, and multisets (bags). 246<P> 247 248<LI> relationTheory now defines the constants RTC and RC (reflexive and 249 transitive closure, and reflexive closure) and proves a variety of 250 properties about them. 251<P> 252 253<LI> Restricted quantification now uses predicate sets, so the meaning of 254 the term 255<PRE> 256 !x::P. Q x 257</PRE> 258 is 259<PRE> 260 !x. x IN P ==> Q x. 261</PRE> 262 The restricted quantification library has been updated to reflect 263 this change, and also shrunk down: in the course of use it was found 264 that more powerful proof tools like the simplifier have removed the 265 need for many of the lower-level tactics. 266</UL> 267 268<P><HR> 269<H2>Improved support for large formalizations</H2> 270 271<UL> 272<LI> Holmake will now read and act under the supervision of make-files 273 (usually named <strong>Holmakefile</strong>). These files can be 274 used to control construction of object files in languages other than 275 SML, and also have a number of other convenient functions. The 276 basic format of the make-files read by Holmake is very much like 277 that of standard make-files, but there is no support for patterns. 278 For more documentation, see the <strong>Holmake</strong> section of 279 the <strong>DESCRIPTION</strong>. 280</UL> 281 282<P><HR> 283<H2>New syntax support</H2> 284 285<UL> 286<LI> Term and type constants in the logic now enjoy per-theory 287 name-spaces. This means that multiple theories can share 288 constants with the same names. If two term constants of the same 289 name are part of the logical context, the parser treats that name 290 as if it were overloaded to both constants. Constants can be 291 unambigously specified by prepending the theory name and "$". 292 Thus 293<PRE> 294 bool$/\ 295</PRE> 296 is the conjunction operator in boolTheory, and 297<PRE> 298 :num$num 299</PRE> 300 is the num type from numTheory. There are also new functions in 301 the kernel's ML API for building and pulling apart constants with 302 theory information included. For example, the function 303 mk_thy_const has the following type 304<PRE> 305 {Name:string, Thy:string, Ty:hol_type} -> term 306</PRE> 307 and the function <kbd>dest_thy_const</kbd> inverts this. 308 <kbd>mk_const</kbd> remains in the system, but its behaviour is 309 unspecified when two or more constants have the same name. 310<P> 311 312<LI> Type abbreviations can now be introduced using the function 313 <kbd>Parse.type_abbrev</kbd>. When a type abbreviation is made, both the 314 abbreviation and the abbreviation's RHS can be used to specify 315 types. Variables that occur in the RHS become parameters of the 316 "new" type operator. Thus 317<PRE> 318 type_abbrev("set", ``:'a -> bool``) 319</PRE> 320 is used in <kbd>pred_setTheory</kbd> to establish ``:'a set`` as an 321 abbreviation for functions of type ``'a -> bool``. After issuing 322 this command, one can write ``NS:num set`` and ``:'b set``. When 323 printed, types do not include abbreviations. 324 325<P> 326<LI> Syntax for ML-style case expressions is now supported. The same 327 patterns supported by <kbd>Define</kbd> are allowed. Some examples 328 of the syntax: 329<PRE> 330 case n of 0 -> x || SUC n -> n + 1 331</PRE> 332 and 333<PRE> 334 case p of (x, []) -> x + 1 335 || (y, h::t) -> y + h 336</PRE> 337</UL> 338 339<P><HR> 340<H2>Modified syntax support</H2> 341 342<UL> 343<LI> The system now compiles files with common HOL infix declarations 344 already in scope. This means that one need no longer write 345<PRE> 346 infix THEN THENL ... 347</PRE> 348 at the top of one's files. Doing so is not an error however. If 349 this behaviour leads to problems, recall that ML infix declarations 350 can be cancelled with the "nonfix" directive. 351 352<P> 353<LI> We have rationalised the ML API. By default, just about all 354 functions use "paired" syntax, rather than "record" syntax. So, 355 mk_var has type 356<PRE> 357 string * hol_type -> term 358</PRE> 359 rather than 360<PRE> 361 {Name : string, Ty : hol_type} -> term 362</PRE> 363 A consistently "record-ised" view of the world is still available 364 by opening the structure Rsyntax. Even in the default view of 365 the world, some functions still take records. These exceptions 366 are for functions where we feel that the order of arguments of the 367 same type is not always obvious. This is exemplified by the 368 universal adoption of the {redex,residue} datatype for 369 substitutions and instantiations. (Remember also that the infix 370 |-> function can be used to construct such records.) 371 372<P> 373<LI> Overloading now works slightly differently. Constants are 374 automatically overloaded to "themselves". Thus, if you define a 375 constant called "foo", and then another called "bar", and want to 376 have "bar" overload to "foo", then you need only call 377<PRE> 378 overload_on ("foo", ``bar``); 379</PRE> 380<P> 381 382<LI> The names of record fields are not now overloaded to the accessor 383 function. This function needs to be accessed as the constant 384<PRE> 385 <rcd-type-name>_<fldname> 386</PRE> 387 E.g., "rcd_fld". If you really like the 'dot' syntax, you can 388 always write 389<PRE> 390 \r. r.fld 391</PRE> 392 which eta-converts to the above. 393<P> 394 395<LI> An easier way of augmenting the built-in pretty-printer is now 396 possible. Previously we allowed for the built-in printer to be 397 completely replaced by a new function. Now, users can also 398 specify new functions to augment the existing code, with the new 399 functions called on terms of specified types. For more details, 400 see the documentation for Parse.add_user_printer in the REFERENCE. 401<P> 402 403<LI> The parser now lets you create an ambiguous grammar. In doing so, it 404 will issue a warning, but will otherwise attempt to do its best to 405 parse inputs. The system's parsing and printing behaviour may become 406 unpredictable, but generous uses of parentheses should allow most 407 reasonable uses of the parser. 408</UL> 409 410<P><HR> 411 412<H2>"Gratuitous" and probably irritating incompatibilities</H2> 413 414<UL> 415<LI> There is no longer any module called basicHol90Lib. Instead, 416 proof scripts should open boolLib. 417 418<P> 419<LI> The orientation of the theorems INTER_ASSOC and UNION_ASSOC from 420 pred_setTheory has been flipped. This brings these theorems into 421 line with all of the other associativity theorems in the system, 422 which are of the form "right-associated" = "left associated", 423 (e.g. x + (y + z) = (x + y) + z). This form is that expected by 424 the AC_CONV procedure. 425 426 If you want to flip them back to make a now-broken proof go 427 through, use something like 428<PRE> 429 val INTER_ASSOC = GSYM INTER_ASSOC 430 val UNION_ASSOC = GSYM UNION_ASSOC 431</PRE> 432 before the references to these theorems occur. 433<P> 434 435<LI> Quotations vs. terms. New tactics from bossLib and definitional 436 principles take quotations (i.e., use `...`). This allows tactics 437 to parse the quotations in the context of the current goal, and 438 allows definitional principles to cope with the fact that you may 439 be redefining a new version of an existing constant with the same 440 name. Other functions take terms, or types (i.e., use ``...``, or 441 (Term`...`)). For example, this means that bossLib.DECIDE now takes 442 a term, not a quotation. 443 444<P> 445<LI> We have removed setLib (including set_Theory) from the core 446 distribution, though the source code is still present in the 447 src/retired/set directory. With the "set" type abbreviation, 448 pred_setLib (including pred_setTheory) should be a "drop-in" 449 replacement for set. 450 451<P> 452<LI> Similarly, the inductive definition packages from Melham and 453 Harrison have been merged into one. Please consult the 454 examples/ind_def directory to see what syntactic changes are 455 necessary. 456<P> 457 458<LI> Eta-conversion used to be part of std_ss, but it has been removed. 459 This may break some proofs. 460 461<P> 462<LI> The functions "theorems", "definitions" and "axioms" have gained a 463 theory-segment parameter. These functions take the name of the 464 theory segment from which the theorems/definitions/axioms are to 465 be retrieved. A call to 466<PRE> 467 theorems () 468</PRE> 469 should thus be replaced with 470<PRE> 471 theorems "-" 472</PRE> 473</UL> 474 475<P><HR> 476 477<H2>Miscellaneous</H2> 478 479<UL> 480<LI> There are now four (4!) hol executables. They are: 481<PRE> 482 hol, hol.bare, hol.unquote, and hol.bare.unquote 483</PRE> 484 all found in the bin/ directory. We recommend hol.unquote as the 485 standard starting point. 486<P> 487 In more detail, the ".unquote" suffix means that the ``...`` 488 preprocessor is enabled. The ".bare" indicates that the 489 executable starts up with a minimal logical context (just 490 boolTheory, the goal-stack and the 'standard' tactics and 491 conversions loaded). This is like the old behaviour of the hol 492 and hol.unquote executables. The absence of the ".bare" indicates 493 an executable that loads "bossLib" as it starts. This provides a 494 much richer logical environment (lists, natural numbers, pairs, 495 options, disjoint sums), with additional tools too (arithmetic 496 decision procedure, high-level definition principles). 497 498<P> 499<LI> The unquote filter is also better at handling Control-C 500 interruptions. If in the middle of entering a input line that 501 includes a delimiter (such as parentheses, various quotes etc), 502 control-C causes the filter to completely forget that this has 503 happened. This mimics the behaviour of Moscow ML's "native" 504 interactive loop. 505 506<P> 507<LI> The installation procedure has been somewhat simplified. In 508 particular, installation on Windows is easier. 509 510<P> 511<LI> Muddy wouldn't build on Linux if the binary distribution of Moscow 512 ML was being used because of a lack of header files in an expected 513 place. Thanks to Hasan Amjad for reporting this bug, which has been 514 fixed. 515</UL> 516 517<P><HR> 518 519<H2>A final note</H2> 520 521 We have retroactively decided to number HOL implementations in the 522following way: 523<OL> 524 525<LI> <strong>HOL88</strong> and earlier: implementations based on a Lisp 526 substrate, with Classic ML. 527 528<LI> <strong>HOL90</strong>: implementations in Standard ML, principally 529 using the SML/NJ implementation. 530 531<LI> <strong>HOL98</strong> (Athabasca and Taupo releases): 532 implementations using Moscow ML, and with a new library and theory 533 mechanism. 534<LI> HOL (Kananaskis releases and beyond) 535 536</OL> 537 With HOL 4, we do away with the habit of associating implementations 538with their year of origin. Individual releases within HOL 4 will 539retain the <em>lake</em>-<em>number</em> naming scheme. 540</BODY></HTML> 541<P> 542<HR> 543<EM><A HREF="http://hol.sourceforge.net/"> 544 HOL 4, Kananaskis-1 545</EM> 546</BODY> 547</HTML> 548