1<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/x 2html1/DTD/xhtml1-strict.dtd"> 3<html xmlns="http://www.w3.org/1999/xhtml"> 4<head> 5<meta http-equiv="content-type" 6 content="text/html ; charset=US-ASCII" /> 7<title>Release Notes for Kananaskis-4 version of HOL 4</title> 8</head> 9 10<body> 11<h1>Notes on HOL 4, Kananaskis-4 release</h1> 12 13<h2 id="contents">Contents</h2> 14<ul> 15 <li> <a href="#new-features">New features</a> </li> 16 <li> <a href="#bugs-fixed">Bugs fixed</a> </li> 17 <li> <a href="#new-theories">New theories</a> </li> 18 <li> <a href="#new-tools">New tools</a> </li> 19 <li> <a href="#new-examples">New examples</a> </li> 20 <li> <a href="#incompatibilities">Incompatibilities</a> </li> 21</ul> 22 23 24 25<h2 id="new-features">New features:</h2> 26 27<ul> 28 <li> There is a new unambiguous notation for set comprehensions that 29 allows one to specify exactly what variables can “vary” 30 to generate the set. For example, the current notation interprets 31<pre> 32 { x + y | x < y } 33</pre> 34 as the set that takes all pairs of numbers such that the first 35 component is less than the other, and then sums them (generating 36 the set of all non-zero numbers). The new notation allows one 37 to specify that only the <code>x</code> should vary by writing 38<pre> 39 { x + y | x | x < y } 40</pre> 41 This denotes the set of numbers from <code>y</code> up to but not 42 including <code>2 * y</code>. To express the first set 43 in the new notation, one would write 44<pre> 45 { x + y | x,y | x < y } 46</pre> 47 The parser accepts both notations. The pretty-printer prefers 48 the old notation unless it can not express the set being 49 printed. Further details are in the Description. Thanks to 50 John Harrison for discussion leading to the adoption of this 51 syntax. </li> 52 53 <li> <p> The syntax of string and character literals is now the same as 54 that accepted by SML. This means that escapes such as 55 <code>\n</code> (for the linefeed character) and 56 <code>\^E</code> (for ASCII character no. 5) can be used 57 inside string and character literals.</p> 58 59 <p> The SML syntax which allows strings to be broken over 60 new-lines by using back-slashes is also supported. This means 61 that one can write </p> 62<pre> 63 ``mystring = "the quick brown fox jumps over \ 64 \the lazy dog"`` 65</pre> 66 <p> and have the actual string value generated exclude the 67 white-space appearing between the back-slashes.</p> 68 </li> 69 70 71 <li> <p> It is possible to include both <code>^</code> (caret) and 72 <code>`</code> back-tick characters inside quotations. Usually 73 these characters have special meaning inside quotations: caret 74 is used to introduce an antiquotation, and the back-tick is used 75 to end a quotation (singly or doubly, depending on the sort of 76 quotation). The caret character can be used <em>as is</em> if a 77 sequence of them is followed by white-space. Otherwise, it 78 needs to be “escaped” by preceding it with another 79 caret character. Similarly, the backquote character can be 80 written by escaping it with a caret. For example, writing</p> 81<pre> 82 ``s1 ^ s2`` 83</pre> 84 <p> will result in the string <code>s1 ^ s2</code> being passed 85 to the HOL parser. This string will then be treated in the 86 standard fashion. E.g., if <code>^</code> is an infix, a 87 function application with it as the head operator will be 88 created. If one wrote <code>``s1 ^^ s2``</code> this would also 89 pass through unchanged. However, if one wrote </p> 90<pre> 91 ``s1 ^s2`` 92</pre> 93 <p> this would be taken as an anti-quotation of SML variable 94 <code>s2</code>. One should write </p> 95<pre> 96 ``s1 ^^s2`` 97</pre> 98 <p> to get the single caret passed to the underlying lexer.</p> 99 100 <p> Note that the back-quote character always needs to be 101 escaped by a caret, and that caret-escapes need to be applied 102 even within string literals and comments that occur inside 103 quotations.</p></li> 104 105 106 <li> <p> The XEmacs editor is now supported, in addition to Emacs, 107 by the <code>tools/hol98-mode.el</code> file of Emacs 108 extensions.</p> 109 </li> 110 111 112 <li> <p> Case expressions may now include literals as patterns, 113 in addition to constructor expressions as in the past. These 114 literals may be for example of types <code>num</code>, 115 <code>char</code>, or <code>string</code>; 116 or they may be of any other type as well, even function types. 117 Literals need not be constants, but they must not contain 118 any free variables.</p> 119<pre> 120 case n of 121 0 -> "none" 122 || 1 -> "one" 123 || 2 -> "two" 124 || _ -> "many" 125</pre> 126 <p>Patterns in case expressions are similar to the patterns used 127 in the definition of recursive functions by <code>Define</code>. 128 Thus they may be deeply nested within larger patterns. 129 As before, in case of overlapping patterns, the earliest 130 listed pattern is matched.</p> 131 132 <p>If the set of patterns specified is sparse, there may be new 133 rows generated automatically to fill it out, and possibly some new 134 or renamed variables or the <code>ARB</code> constant to properly 135 represent the case expression. </p> 136<pre> 137 - ``case a of 138 (1, y, z) -> y + z 139 || (x, 2, z) -> x - z 140 || (x, y, 3) -> x * y``; 141 > val it = 142 ``case a of 143 (1,2,3) -> 2 + 3 144 || (1,2,z) -> 2 + z 145 || (1,y,3) -> y + 3 146 || (1,y,z) -> y + z 147 || (x,2,3) -> x - 3 148 || (x,2,z') -> x - z' 149 || (x,y',3) -> x * y' 150 || (x,y',z') -> ARB`` : term 151</pre> 152 <p>A complex pattern with several components may include 153 both literals and constructor expressions as subpatterns. 154 However, a set of patterns specified in a case expression 155 may not have both literals and constructor expressions as 156 alternatives to each other, except insofar as a pattern 157 may be both a literal and a (0-ary) constructor, such as 158 the literal <code>0</code>. See the Description for more 159 information and examples of case expressions. </p> 160 161 </li> 162 163 164 <li> <p> Inductive definitions are now made with respect to a 165 varying “<code>monoset</code>”: a list of theorems 166 specifying that boolean operators are monotone in their 167 arguments. These are used to justify recursions that may occur 168 underneath new operators that users introduce. </p> 169 170 <p> Initially, this set includes results for the standard 171 boolean operators (such as existential quantification and 172 conjunction), and is augmented as later theories are loaded. For 173 example, the constant <code>EVERY</code> in the theory of lists, 174 has a monotonicity result</p> 175<pre> 176 |- (!x:'a. P x ==> Q x) ==> (EVERY P l ==> EVERY Q l) 177</pre> 178<p> and this is incorporated into the global <code>monoset</code> when 179the theory of lists is loaded. This then allows the easy definition 180of relations that recurse under <code>EVERY</code>, as in this rule 181</p> 182<pre> 183 !x. EVERY newrel (somelist_of x) ==> newrel x 184</pre> 185 186 187 <p> Theorems can be declared as monotonicity results using the 188 <code>export_mono</code> function. See the Description for the 189 exact form that monotonicity theorems must take. </p> 190 191 </li> 192 193 194 <li> <p>Types that are instances of abbreviation patterns (made with 195 <code>type_abbrev</code>) now print in abbreviated form by 196 default. For example, if one writes</p> 197<pre> 198 type_abbrev("set", ``:'a -> bool``); 199</pre> 200 201 <p> Then, as before, one can write <code>``:num set``</code> and 202 have this understood by the type parser. Now, in addition, when 203 types are printed, this is reversed, so that the following 204 works: </p> 205<pre> 206 - type_of ``(UNION)``; 207 > val it = ``:'a set -> 'a set -> 'a set`` : hol_type 208</pre> 209 210 <p> Unfortunately, with this particular example, one also 211 gets</p> 212<pre> 213 - type_of ``(/\)``; 214 > val it = ``:bool -> bool set`` : hol_type 215</pre> 216 217 <p> which is more confusing than it is illuminating. For this 218 reason, it is possible to turn abbreviation printing off 219 globally (using a <code>trace</code> variable, 220 <code>print_tyabbrevs</code>), or on an 221 abbreviation-by-abbreviation basis. The latter is done with the 222 function</p> 223 224<pre> 225 disable_tyabbrev_printing : string -> unit 226</pre> 227 228 <p> Calls to this function are made in the <code>pred_set</code> 229 and <code>bag</code> theories so that those theories’ 230 abbreviations (<code>set</code>, <code>bag</code> and 231 <code>multiset</code>) are not printed. </p> 232 </li> 233 234 235 236 <li> <p> There is a new polymorphic type, 237 <code>``:'a itself``</code> containing just one value for 238 all possible instantiations of <code>``:'a``</code>. This value 239 is supported by special syntax, and can be written</p> 240<pre> 241 (:tyname) 242</pre> 243 244 <p> This type provides a convenient method for defining values 245 that are dependent on just the type, and not on any values 246 within that type. For example, within the <a 247 href="#wordsTheory">new theory of words</a>, the constant 248 <code>dimindex</code> has type 249 <code>:'a itself -> num</code>, and returns the 250 cardinality of the universe of the type <code>'a</code> if the 251 universe is finite, or one otherwise. The syntax support means 252 one can write terms such as </p> 253<pre> 254 dimindex(:bool) 255</pre> 256 <p> and </p> 257<pre> 258 dimindex(:'a -> bool) 259</pre> 260 <p> This type is inspired by a similar one in Isabelle/HOL.</p> 261 </li> 262 263</ul> 264 265<h2 id="bugs-fixed">Bugs fixed:</h2> 266 267<ul> 268 <li> <p> The <code>muddyC/muddy.c</code> file would not build with 269 <code>gcc-4</code>. </p> 270 </li> 271 272 <li> <p> The implementation of <code>Q.EXISTS</code> was incorrect 273 (would only work with witnesses of type <code>:bool</code>). 274 Thanks to Eunsuk Kang for the report of this bug. </p> </li> 275 276 <li> <p> The natural number and integer decision procedures were not 277 normalising multiplicative expressions as much as they should, 278 causing obvious goals to not get proved. Thanks to Alexey 279 Gotsman for the report of this bug. </p> </li> 280 281 <li> <p> The theory and identifier indexes in the help pages were 282 generated with bogus links. Thanks to Hasan Amjad for the 283 report of this bug. </p> </li> 284 285 <li> <p> Expressions using <code>case</code>-expressions with 286 function-types and applied to arguments failed to parse 287 correctly. </p> </li> 288 289 <li> <p> The implementation of <code>Holmake</code>’s 290 <code>--rebuild_deps</code> (or <code>-r</code>) option was 291 faulty. Thanks to Tom Ridge for the report of this bug. </p> 292 </li> 293 294 <li> <p> The implementation of <code>stringLib.string_EQ_CONV</code> 295 failed if one of the string arguments was the empty string. 296 Thanks to Mike Gordon for the report of this bug. </p> </li> 297 298 <li> <p> The derivation of “strong” induction principles 299 in the inductive definitions library has been improved to cope 300 with multiple (mutually recursive) inductively-defined 301 relations. Such relations could always be defined using 302 <code>Hol_reln</code>, but their strong induction principles 303 couldn’t be derived. (See below for a change in the type 304 and home of this function.) </p></li> 305 306</ul> 307 308 309<h2 id="new-theories">New theories:</h2> 310<ul> 311 <li> <p> A theory of the rational numbers, thanks to Jens 312 Brandt. This is used in the <a href="#acl2">embedding of ACL2 in 313 HOL</a>.</p> </li> 314 315 <li id="wordsTheory"> <p> A new polymorphic theory of fixed-width 316 words, called <code>words</code>. This is now our recommended way 317 of using types such as <code>word32</code>, <code>word16</code> etc. 318 This builds on John Harrison’s “Finite cartesian 319 products” from <cite>A HOL theory of Euclidean space</cite> in 320 TPHOLs 2005. </p> 321 322 <p> There is now no need to use the word functor 323 approach introduced in Kananaskis-3 (though this code is still 324 available). Instead, when <code>wordsTheory</code> is loaded, one 325 set of polymorphic constants is defined, and these can be used for 326 all the word types. Words are polymorphic in one argument (thus 327 there is a type <code>``:'a word``</code>) and types such as 328 <code>word32</code> and <code>word16</code> instantiate the type 329 parameter to different concrete type arguments. (The cardinality of 330 the parameter’s universe indicates the number of bits in the 331 word.) For more, see the Description.</p></li> 332 333</ul> 334 335<h2 id="new-tools">New tools:</h2> 336 337<ul><li>None this time!</li></ul> 338 339<h2 id="new-examples">New examples:</h2> 340 341<ul> 342 <li id="acl2"> A deep embedding 343 of the entire ACL2 logic in HOL has been defined via a theory 344 <code>sexp</code> of S-expressions. All 78 ACL2 axioms have been 345 verified in HOL. A suite of tools is available to translate HOL 346 datatypes into S-expressions and HOL functions to functions on 347 S-expressions. Scripts are provided to print S-expressions defined 348 inside HOL to defuns and defthms for processing by the ACL2 system, 349 and for slurping ACL2 defuns and defthms into HOL. This work is a 350 collaboration between Mike Gordon and James Reynolds at the 351 University of Cambridge and Warren Hunt and Matt Kaufmann at the 352 University of Texas. The goal is to provide a robust and scalable 353 link between the HOL4 and ACL2 systems suitable for use on 354 substantial industrial-scale verification projects. </li> 355 356<li id="temporal_deep">The example <code>temporal_deep</code> contains deep embeddings of temporal logics and other formalisms related to model checking. Amongst others there are deep embeddings of 357<ul> 358 <li>LTL</li> 359 <li>CTL*</li> 360 <li>nondeterministic and universal omega-automata</li> 361 <li>alternating automata.</li> 362</ul> 363Additionally, there is an automated translation from LTL to omega-automata. Together with the interface to SMV from <code>temporalLib</code> this allows LTL model checking. Moreover, there is a translation of a subset of the FL of the PSL example into LTL. Thus, this example allows model checking for a subset of PSL. 364</li> 365 366</ul> 367 368<h2 id="incompatibilities">Incompatibilities:</h2> 369 370<ul> 371 372 <li> <p> The <code>std_ss</code> simpset has become more powerful, 373 picking up a set of “obvious” rewrites that used to 374 be in <code>arith_ss</code>. Now the latter simpset adds just 375 the decision procedure for Presburger arithmetic.</p> </li> 376 377 <li> <p> Functions such as <code>induction_of</code> in the 378 <code>TypeBase</code> structure that used to take a string (the 379 name of a type operator), now take a type. Thus, instead of</p> 380<pre> 381 TypeBase.induction_of "num" 382</pre> use 383<pre> 384 TypeBase.induction_of ``:num`` 385</pre> 386</li> 387 388 <li> <p> The normalisation of arithmetic terms performed by 389 the <code>ARITH_ss</code> simpset fragment (and thus, the 390 simpset <code>bossLib.arith_ss</code>) is more aggressive. This 391 can break proofs. The <code>bossLib</code> library now exports 392 <code>old_arith_ss</code> and <code>old_ARITH_ss</code> 393 entry-points if users wish to avoid having to adjust their 394 proofs. </p> </li> 395 396 <li> <p> The <code>derive_strong_induction</code> function has 397 changed type, and location. It is now an entry-point in 398 <code>IndDefLib</code>, and has type </p> 399<pre> 400 thm * thm -> thm 401</pre> 402 <p> rather than </p> 403<pre> 404 thm list * thm -> thm 405</pre> 406 <p> The first argument should now be the “rules” 407 theorem returned by a call to <code>Hol_reln</code>. </p> </li> 408 409<li> <p> In order to avoid certain misleading scenarios, the type of 410 <code>mk_oracle_thm</code> has changed so that it takes a string 411 as its first argument rather than a <code>tag</code>. The 412 implementation of <code>mk_oracle_thm</code> turns the given 413 string into a tag value using the function 414 <code>Tag.read</code>. There is also a new function, 415 <code>Thm.add_tag</code>, that allows arbitrary tags to be added 416 to existing theorems. Thanks to Mark Adams for discussion leading 417 to this change. </p> </li> 418 419 420</ul> 421 422 423 424 425<hr /> 426 427<p> <em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-4</a></em> </p> 428 429</body> </html> 430