1<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN"> 2<html> 3<head> 4<meta http-equiv="content-type" 5 content="text/html ; charset=UTF-8"> 6<title>Release Notes for Kananaskis-6 version of HOL 4</title> 7<style type="text/css"> 8<!-- 9 body {color: #333333; background: #FFFFFF; 10 margin-left: 1em; margin-right: 1em } 11 code, pre {color: #006400; font-weight: bold; font-family: "Andale Mono", "Lucida Console", monospace; } 12 div.footer { font-size: small; display: flex; justify-content: space-between; } 13--> 14</style> 15 16</head> 17 18<body> 19<h1>Notes on HOL 4, Kananaskis-6 release</h1> 20 21<p>We are pleased to announce the Kananaskis-6 release of HOL 4.</p> 22 23<h2 id="contents">Contents</h2> 24<ul> 25 <li> <a href="#new-features">New features</a> </li> 26 <li> <a href="#bugs-fixed">Bugs fixed</a> </li> 27 <li> <a href="#new-theories">New theories</a> </li> 28 <li> <a href="#new-tools">New tools</a> </li> 29 <li> <a href="#new-versions">New versions</a> </li> 30 <li> <a href="#new-examples">New examples</a> </li> 31 <li> <a href="#incompatibilities">Incompatibilities</a> </li> 32</ul> 33 34<h2 id="new-features">New features:</h2> 35 36<ul> 37 38<li><p>The <code>HolSmtLib</code> library now supports proof 39 reconstruction for the 40 <abbrev title="Satisfiability Modulo Theories">SMT</abbrev> solver 41 <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/">Z3</a>. 42 (Several other SMT solvers continue to be supported as 43 oracles.)</p></li> 44 45<li><p>The pretty-printer now uses colours to convey extra information 46 about terms and types as they are printed. For example, bound 47 term variables are printed in green, and free variables are 48 printed in blue. This colouring will happen on colour terminals 49 such as Unix <code>xterm</code> (also the standard MacOS Terminal 50 application), as well as inside Emacs.</p> 51 52 <p> If you are using the 53 Emacs mode, then the types of both sorts of variables are also 54 available in a mouse-over tooltip. Moreover, the colours and 55 printing-styles used in the Emacs mode for things like bound 56 variables can be customised, 57 using <code>M-x customize</code>. </p> 58 59 <p>Besides this automatic colored pretty-printing depending on 60 the term structure, it is now possible to define syntax highlighting 61 in userprinters.</p></li> 62 63<li><p>Many type variables can now be parsed and printed as lower-case 64 Greek letters. For example, you can input <code>``:'a``</code>, 65 and will get back <code>``:��``</code>. You can also input type 66 variables using the Greek letters (except for the letter ��). 67 Underneath, the type variable still has the name with the 68 apostrophe: this is a purely presentational change.</p></li> 69 70<li><p>Bounded rewrites work better (a few bugs were fixed here), and 71there is now also an easy way to specify that a rewrite should only 72occur on the left or right side of a term. For example, to apply the 73theorem <code>th</code> twice, and on the left-hand side on an equality, 74use</p> 75<pre> 76 SIMP_TAC bool_ss [Ntimes th 2, SimpLHS] 77</pre> 78<p>To rewrite on the right-hand side:</p> 79<pre> 80 SIMP_TAC bool_ss [Ntimes th 2, SimpRHS] 81</pre> 82<p>It is also possible to rewrite on the left or right sides of 83operators other than equality. See the Description manual for 84details. </p> 85</li> 86 87<li><p>If the block of universally quantified variables at the head of 88a clause in the definition of an inductive relation contains duplicate 89names, <code>Hol_reln</code> detects this and provides an informative 90error message. </p></li> 91 92<li><p>There are two new ���document-level��� modes for using HOL���s 93LaTeX-pretty-printing technology (originally due to Ramana Kumar and 94Thomas T��rk). In both, terms, types and theorems become 95straightforward to embed in LaTeX documents. For example, one might 96write something like</p> 97<pre> 98 The term \HOLtm{p1 /\ q2} is a typical conjunction. 99</pre> 100<p> and have this turned into </p> 101<pre> 102 The term <i>p���</i> ��� <i>q���</i> is a typical conjunction. 103</pre> 104<p> after LaTeX has been run. The ASCII conjunction has turned into a 105nice LaTeX maths symbol, and the term has been parsed, allowing 106variables to be printed in italic font, and with trailing digits 107sub-scripted. </p> 108 109<p>See the Description manual for more detailed documentation. 110 111</li> 112 113<li> <p> Simplification of terms involving the <code>EL</code> operator 114(calculates the <i>n</i><sup>th</sup> element of a list) is better. 115 116<li><p> Some new syntax for various bag operations, including arithmetic 117symbols <code>+</code>, <code>-</code>, <code><</code>, <code>���</code> 118for the notions on bags that are just point-wise lifts of those 119operators on numbers 120(<code>BAG_UNION</code>, <code>BAG_DIFF</code>, <code>PSUB_BAG</code>, <code>SUB_BAG</code>).</li> 121 122<li><p> New syntax for universal sets 123(in <code>pred_setTheory</code>). In ASCII 124mode, <code>univ(:'a)</code> is the universal set with elements drawn 125from type <code>:'a</code>. Another example: <code>univ(:num)</code> 126is the set of all natural numbers. With Unicode on, the first example 127prints as <code>𝕌(:��)</code>. The Unicode character used here 128(U+1D54C, a cute uppercase ���U���) is beyond the BMP (Basic Multilingual Plane) 129and may not appear in many fonts. Rather than have to give up all of 130Unicode to get around this, there is an additional trace variable 131(<code>"Unicode Univ printing"</code>) to turn off the use of this 132character, making the syntax use <code>univ</code> once more. 133 134<p>Of course, the old syntax (<code>UNIV:'a -> bool</code>, 135or <code>UNIV:'a set</code>) continues to work. 136 137<li><p> A new ���vim mode��� for controlling a HOL session from within the 138vim editor. This mimicks most of the important features of the Emacs 139mode. See <code>tools/vim</code> for a README file about this 140feature. Thanks to Ramana Kumar for the implementation of this tool. 141 142<li> <p> If syntax that involves non-ASCII characters is added 143using <code>add_rule</code>, <code>set_fixity</code> 144or <code>overload_on</code>, it is only used if the Unicode flag is 145set. If the Unicode flag is toggled off and then on again, the 146Unicode syntax will disappear and reappear appropriately. 147 148 149<li> <p> The persistent simpset (<code>srw_ss()</code>, also used 150in <code>SRW_TAC</code>) can now have named simpset fragments removed from 151it using the function <code>diminish_srw_ss</code>. 152 153<li> <p> <code>bin/build</code> uses earlier (cached) options when not 154explicitly overridden. 155 156In particular, kernel specifications (<code>-expk</code>, and the new <code>-stdknl</code>), and 157build-sequence file specifications are cached in 158<code>tools/lastbuildoptions</code> so that one can subsequently do 159just <code>bin/build</code> to build again with those same options. 160To override a <code>-seq foo</code> option, you can use 161the <code>-fullbuild</code> option. 162 163<p> Other options (<code>-symlink</code>, <code>-selftest</code>) are 164not cached. 165 166<li> <p>Users can configure their interactive sessions (setting output 167pretty-printing options with <code>set_trace</code> commands for 168example), by writing SML code into a <code>.hol-config.sml</code> file 169in their HOME directory. In fact, all of the following are acceptable 170names for the file: <code>hol-config.sml</code>, <code>hol-config.ML</code>, <code>.hol-config</code>, <code>.hol-config.sml</code>, 171and <code>.hol-config.ML</code>. The first of these that is found is 172used. 173 174<p> (The meaning of ���the user���s home 175directory��� is clear on Unix systems. On Windows, the environment 176variables <code>HOMEPATH</code> and <code>APPDATA</code> are consulted 177to determine where to look.) 178 179<p> The file, if it exists, is <code>use</code>-d into the interactive 180session, when it begins. A message is printed saying as much also. 181</ul> 182 183<h2 id="bugs-fixed">Bugs fixed:</h2> 184 185<ul> 186<li><p>Type abbreviations used to be able to be applied to more type 187arguments than they were expecting. E.g.,</p> 188<pre> 189 type_abbrev("foo", ``:bool``) 190</pre> 191<p>followed by</p> 192<pre> 193 ``:'a foo`` 194</pre> 195<p>used to work. No more!</p> 196</li> 197 198<li><p> <code>Hol_reln</code> now correctly accepts inductive 199definitions where type variables appear only in schematic 200variables.</p></li> 201 202<li><p><code>Hol_reln</code> now correctly accepts inductive 203definitions defining multiple (presumably multiply recursive) 204relations with schematic variables. Note that for a variable to be 205detected as schematic in this situation, it needs to be a parameter to 206all relations, even if it may not be used in all of them. 207 208<li><p>The syntax <code>num$0</code> failed to parse. Thanks to 209Behzad Akbarpour for the report of this bug.</p></li> 210 211<li><p>In <code>Hol_datatype</code>, nested recursion in record data 212types where the new type was also polymorphic failed. Thanks to Ramana 213Kumar for the report of this bug. </p> 214 215<li><p>In <code>Hol_datatype</code>, nested recursion involving 216the <code>itself</code> type constructor could fail. Thanks to Ramana 217Kumar for the report of and fix for this bug. </p> 218 219<li><p>The <code>TypeNet</code> data structure for indexing 220information by types could get confused if the ���same��� type was 221redefined (in the one interactive session) with different arities. 222Thanks to Ramana Kumar for the bug report that led to the isolation of 223this problem.</p> 224 225</ul> 226 227 228 229<h2 id="new-theories">New theories:</h2> 230 231<ul> 232<li> <p> A very simple theory <code>string_numTheory</code> demonstrating 233that strings and natural numbers are in bijection (with 234functions <code>n2s</code> and <code>s2n</code> constructively 235demonstrating this bijection). 236 237<li> <p>A theory of trie-like trees that recurse under a finite 238map, <code>fmaptreeTheory</code>. This type can be used to represent 239recursive namespace-like environments. 240</ul> 241 242<h2 id="new-tools">New tools:</h2> 243 244<ul> 245<li><p> A new library <code>HolQbfLib</code> provides an interface to 246external Quantified Boolean Formulae (QBF) solvers. It can check 247certificates of invalidity generated by the QBF solver Squolem.</li> 248 249<li><p>A bit-blasting conversion for operations on fixed-width 250words: <code>BBLAST_CONV</code>. This goes beyond the capabilities 251of <code>WORD_BIT_EQ_CONV</code> by expanding out additions and 252subtractions. This allows the new conversion to automatically handle 253small but tricky bit vector goals. For example: 254<pre> 255 (x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w) 256</pre> 257<p> and 258<pre> 259 !a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w 260</pre> 261<p> 262(These aren���t provable with <code>wordsLib.WORD_DECIDE</code>.) 263 264<p> Obviously bit-blasting is a brute force approach, so the new 265conversion should be used with care. It will only work well for 266smallish word sizes and when there is only and handful of additions 267around. It is also ���eager������additions are expanded out even when 268not strictly necessary. For example, in 269<pre> 270 (a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32 271</pre> 272<p> 273the sum <code>a + b</code> is expanded. Users may be able to achieve 274speed-ups by first introducing abbreviations and then proving general 275forms, <i>e.g.</i> 276<pre> 277 x <+ c /\ c <+ d ==> x <+ d:word32 278</pre> 279<p> The conversion handles most operators, however, the following are 280not covered or interpreted: 281<ul> 282 <li> Type variables for word lengths, <i>i.e.</i> terms of type <code>``:'a word``</code> 283 284 <li> General multiplication, i.e. <code>``w1 * w2``</code>. 285 Multiplication by a literal is 286 okay, although this may introduce many additions. 287 288 <li> Bit field selections with non-literal bounds, e.g. <code>``(exp1 -- exp2) w``</code>. 289 290 <li> Shifting by non-literal amounts, <i>e.g.</i> <code>``w << exp``</code>. 291 292 <li> <code>``n2w exp``</code> and <code>``w2n w``</code>. Also <code>w2s</code>, <code>s2w</code>, <code>w2l</code> and <code>l2w</code>. 293 294 <li> <code>word_div</code>, <code>word_sdiv</code>, <code>word_mod</code> 295 and <code>word_log2</code>. 296 297</ul> 298 299 300 301 302</ul> 303 304<h2 id="new-versions">New versions:</h2> 305 306<h2 id="new-examples">New examples:</h2> 307 308<ul> 309<li> A development of some basic computability theory: 310<ul> 311 <li> a development of ��-terms as computable functions, showing that 312 things like Church-numerals are as powerful as one would like, and 313 that ��-terms can indeed be set up to evaluate suitably encoded 314 ��-terms (thereby providing a Universal Machine); 315 316 <li> a development of primitive recursive and recursive 317 functions doing much the same; 318 319 <li> a demonstration that both models can emulate each other; 320 321 <li> definition of concepts of recursive, and 322 recursively-enumerable sets; and 323 324 <li> some standard results, including: the Halting Problem, Rice's 325 Theorem, the Recursion theorem, that recursive sets are closed under 326 union and complementation, that r.e. sets are closed under union and 327 intersection but not complement, and that if a set and its 328 complement are both r.e. then they are both recursive. 329</ul> 330</ul> 331 332<h2 id="incompatibilities">Incompatibilities:</h2> 333 334<ul> 335 336<li><p><code>Drule.CONJUNCTS_CONV</code> (proving equivalence of 337 conjunctions under associativity, commutativity and idempotence) has 338 been renamed to <code>Drule.CONJUNCTS_AC</code>.</p></li> 339 340<li><p><code>Drule.CONJ_SET_CONV</code> 341 and <code>Drule.FRONT_CONJ_CONV</code> have been removed. Their 342 functionality can easily be derived 343 from <code>Drule.CONJUNCTS_AC</code>.</p></li> 344 345<li><p>The overload <code><></code> on <code>words$word_slice</code> 346 has been removed and replaced with <code>''</code>.</p></li> 347 348<li><p>The interface of <code>userprinter</code> (user defined pretty 349 printers) changed. Instead of getting just two 350 functions <code>add_string</code> and <code>add_break</code>, it now 351 gets a record of type <code>term_pp_types.ppstream_funs</code> that 352 contains these functions as well as several others.</p></li> 353 354<li><p>The type of the <code>filter</code> field of 355the <code>SSFRAG</code> function for constructing simpset fragment 356values has changed 357from <code>(thm -> thm list) option</code> 358to <code>(controlled_thm -> controlled_thm list) option</code>, 359where a <q>controlled theorem</q> value is a pair of a theorem and a 360control indicating how many times the rewrite is allowed to be 361applied. See the REFERENCE and the <code>BoundedRewrites</code> 362module for details.</p> 363 364<li><p>The <code>Unicode</code> structure is now a sub-structure 365of <code>Parse</code>, due to some significant code-reorganisation. 366This means that a line such as 367<pre> 368 open Parse boolLib Unicode 369</pre> 370<p>will fail. Instead it must be 371<pre> 372 open Parse boolLib 373 open Unicode 374</pre> 375 376<li><p>The constant <code>INFINITE</code> 377in <code>pred_setTheory</code> has been replaced by an abbreviation. 378Thus, if one types <code>``INFINITE s``</code>, the underlying term is 379really <code>��FINITE s</code>. All instances of this pattern 380will print as <code>INFINITE s</code>. The 381functions <code>mk_infinite</code>, <code>dest_infinite</code> 382and <code>is_infinite</code> in <code>pred_setSyntax</code> continue 383to work and do the ���right thing���, the 384entrypoint <code>infinite_tm</code> in the same module has been removed.</p> 385 386</ul> 387 388<hr> 389<div class="footer"> 390<p><em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-6</a></em></p> 391<p>(<a href="kananaskis-5.release.html">Release notes for previous version</a>)</p> 392</div> 393 394</body> </html> 395