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-7 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-7 release</h1> 20 21<p>We are pleased to announce the Kananaskis-7 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-examples">New examples</a> </li> 30 <li> <a href="#incompatibilities">Incompatibilities</a> </li> 31</ul> 32 33<h2 id="new-features">New features:</h2> 34 35<ul> 36 37<li><p><code>HolSmtLib</code> 38supports <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/">Z3</a> 39proof reconstruction also for goals that involve fixed-width words, 40based on bit-blasting (cf. <code>blastLib</code>) and other word 41decision procedures.<p></li> 42 43<li><p><code>HolSmtLib</code> provides a translation from HOL into 44<a href="http://combination.cs.uiowa.edu/smtlib/">SMT-LIB</a> 2 45format. (Support for SMT-LIB 1.2 has been 46discontinued. <b>Incompatibility</b>.)<p></li> 47 48<li><p><code>HolQbfLib</code> supports checking both validity and 49invalidity certificates for Squolem 2.02. (Support for Squolem 1.x has 50been discontinued. <b>Incompatibility</b>.)</p></li> 51 52<li><p><code>wordsSyntax.mk_word_replicate</code> computes the width 53of the resulting word when applied to a numeral and a fixed-width 54word. Minor <b>incompatibility</b>.</p></li> 55 56<li><p>The new <code>numLib.MOD_ss</code> simpset fragment simplifies a number of expressions involving natural number modulus (<code>MOD</code>). 57For example, <code>(7*x + 3) MOD 2</code> will automatically simplify to <code>(x + 1) MOD 2</code>. 58 59 60<li><p>User pretty-printers now have to be of a different type. 61This <b>incompatibility</b> affects the function <code>add_user_printer</code>. 62Users have to write their pretty-printers in a monadic style, where pretty-printing components are linked with an infix <code>>></code> connective. 63The advantage of the new system is that it gives pretty-printers access to information about which variables are bound and free, and the ability to change this status when making recursive calls to the built-in printer. 64It will also be easier to extend the system with new functionality along the same lines. 65 66<li><p>The system supports syntax for decimal fractions (<em>e.g.</em>, <code>3.021</code>). 67This syntax maps to division terms of the form <em>n</em> / 10<em><sup>m</sup></em>. 68Thus <code>3.012</code> maps to the term <code>3012 / 1000</code>. 69This transformation is reversed by the pretty-printer. 70In the core system, this syntax is enabled for the real, rational and <a href=" 71#complex">complex</a> theories. 72 73</ul> 74 75<h2 id="bugs-fixed">Bugs fixed:</h2> 76 77<ul> 78 79<li><p><code>numSimps.REDUCE_ss</code> no longer diverges on certain 80terms.</p></li> 81 82<li><p>There is now LaTeX notation for the operation of cross-product on sets (written <em>A �� B</em>), and for the numeric pairing function (written <em>n ��� m</em>).</p></li> 83 84<li><p>The lexer now tokenizes the input <code>``"(*"``</code> correctly.</p> 85<p>Also handle occurrences of such strings in <code>Theory.sig</code> files, which can cause them to become invalid SML.</p> 86</li> 87 88<li><p>When making definitions with <code>Define</code> (and <code>Hol_defn</code>, and others), one can now use the boolean equivalence syntax (<code><=></code> or <code>���</code>), not just <code>=</code>.</p> 89</li> 90 91<li><p>The <code>SimpL</code> and <code>SimpR</code> directives for controlling the position of simplification were only working with binary relations, not functions (such as <code>+</code>, say). 92Thanks to Ramana Kumar for the report of the bug. 93 94<li><p>Fix type-parsing bug when array suffixes and normal suffixes (such as <code>list</code>) interact. Now, both <code>:bool[32] list</code> and <code>:bool list[32]</code> parse correctly. 95 96</ul> 97 98<h2 id="new-theories">New theories:</h2> 99 100<ul> 101<li><p>The theory of transcendental functions (<code>transcTheory</code>) 102has been extended with a treatment of exponentiation where exponents 103can be of type <code>:real</code>. This is implemented by the (infix) 104function <code>rpow</code>. (The existing function <code>pow</code> 105requires a natural number as the exponent.) Thanks to Umair Siddique 106for the definition and theorems. 107 108 109<li id="complex"><p> 110A formalisation of the complex numbers (<code>complexTheory</code>) by Yong Guan, Liming Li, Minhua Wu and Zhiping Shi. 111The authors referred to the HOL Light theory by John Harrison and the theory in PVS. 112It includes treatments of the complex numbers in the real pair form, the polar form and the exponential form, with basic arithmetic results and some other theorems. 113 114<li><p>A theory of relations based on sets of pairs (<code>set_relationTheory</code>). 115Most of the theorems are about orders, including Zorn���s lemma, and a lemma stating that ���stream-like��� partial orders can be extended to ���stream-like��� linear orders. 116Also add a theorem to <code>llist</code> that ���stream-like��� linear orders can be converted into lazy lists. 117Thanks to Scott Owens for this development. 118 119</ul> 120 121<h2 id="new-tools">New tools:</h2> 122 123<ul> 124<li> 125<p>A few extra tools in <code>wordsLib</code>: 126<dl> 127 <dt> <code>WORD_SUB_CONV</code> / <code>WORD_SUB_ss</code> 128<dd> 129<p> These can be used to simplify applications of unary/binary minus, introducing or eliminating subtractions where possible. 130These must <em>not</em> be used simulataneously with <code>srw_ss</code>, <code>WORD_ARITH_ss</code> or <code>WORD_ss</code> (as this will likely result in non-termination). 131However, can be used to good effect afterwards. 132For example: 133<pre> 134 wordsLib.WORD_SUB_CONV ``a + -1w * b`` 135 |- a + -1w * b = a - b 136 137 wordsLib.WORD_SUB_CONV ``-(a - b)`` 138 |- -(a - b) = b - a 139 140 wordsLib.WORD_SUB_CONV ``a + b * 3w : word2`` 141 |- a + b * 3w = a - b 142 143 wordsLib.WORD_SUB_CONV ``192w * a + b : word8`` 144 |- 192w * a + b = b - 64w * a 145</pre> 146 147<dt><code>WORD_DIV_LSR_CONV</code> 148<dd><p> 149 Convert division by a power of two into a right shift. For example: 150<pre> 151 wordsLib.WORD_DIV_LSR_CONV ``(a:word8) // 8w`` 152 |- a // 8w = a >>> 3 153</pre> 154 155<dt><code>BITS_INTRO_CONV</code> / <code>BITS_INTRO_ss</code> 156<dd> 157 <p> These convert <code>DIV</code> and <code>MOD</code> by powers of two into application of BITS. 158 For example: 159<pre> 160 wordsLib.BITS_INTRO_CONV ``(a DIV 4) MOD 8``; 161 |- (a DIV 4) MOD 8 = BITS 4 2 a 162 163 wordsLib.BITS_INTRO_CONV ``(a MOD 32) DIV 8``; 164 |- a MOD 32 DIV 8 = BITS 4 3 a 165 166 wordsLib.BITS_INTRO_CONV ``a MOD 2 ** 4``; 167 |- a MOD 2 ** 4 = BITS 3 0 a 168 169 wordsLib.BITS_INTRO_CONV ``a MOD dimword (:'a)``; 170 |- a MOD dimword (:'a) = BITS (dimindex (:'a) - 1) 0 a 171</pre> 172 173<dt><code>n2w_INTRO_TAC <<em>int</em>></code> 174<dd><p> Attempts to convert goals of the form <code>``a = b``</code>, <code>``a < b``</code> and <code>``a <= b``</code> into goals of the form <code>``n2w a = n2w b``</code>, <code>``n2w a <+ n2w b``</code> and <code>``n2w a <=+ n2w b``</code>. 175The integer argument denotes the required word size. 176This enables some bounded problems (over the naturals) to be proved using bit-vector tactics. 177For example, the goal: 178<pre> 179 `((11 >< 8) (imm12:word16) : word12) <> 0w ==> 180 ((31 + 2 * w2n ((11 >< 8) imm12 : word12)) MOD 32 = 181 w2n (2w * (11 >< 8) imm12 + -1w : word32))` 182</pre> 183<p> can be solved with 184<pre> 185 STRIP_TAC THEN n2w_INTRO_TAC 32 THEN FULL_BBLAST_TAC 186</pre> 187</dl> 188 189 190 191</ul> 192 193<h2 id="new-examples">New examples:</h2> 194 195<ul> 196<li> <p> A mechanisation of first-order and nominal unification done in an accumulator-passing style with <q>triangular</q> substitutions. 197In <code>examples/unification/triangular</code>. 198<li><p> Some basic category theory (up to the Yoneda lemma), including two categories of <q>sets</q>: one using HOL sets (predicates) and one using the axiomatically introduced type from <code>zfsetTheory</code>. 199In <code>examples/category</code>. 200</ul> 201 202<h2 id="incompatibilities">Incompatibilities:</h2> 203 204<ul> 205 206<li><p><code>Lib.itotal</code> removed; use <code>Lib.total</code> 207instead. Note that <code>handle _</code> is harmful: 208exception <code>Interrupt</code> should never be handled without being 209re-raised.</p></li> 210 211<li><p><code>Lib.gather</code> removed; 212use <code>{Lib,List}.filter</code> instead.</p></li> 213 214<li><p>The ugly situation whereby we had fixities called <code>Prefix</code> and <code>TruePrefix</code>, but <code>Prefix</code> really encoded an absence of fixity, has been done away with. 215Now the fixity <code>Prefix</code> codes for what used to be <code>TruePrefix</code>, and in relevant situations where a <code>fixity</code> value was required, a <code>fixity option</code> can be provided instead. 216In this situation <code>NONE</code> is used to indicate the absence of a fixity. 217 218<p>The function <code>set_fixity</code> takes a <code>fixity</code>, not a <code>fixity option</code>, so its old ability to remove fixities has disappeared. 219If you wish to do this, you should use the function <code>remove_rules_for_term</code>. 220 221</ul> 222 223<hr> 224<div class="footer"> 225<p><em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-7</a></em></p> 226<p>(<a href="kananaskis-6.release.html">Release notes for previous version</a>)</p> 227</div> 228 229</body> </html> 230