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-9 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--> 15</style> 16 17</head> 18 19<body> 20<h1>Notes on HOL 4, Kananaskis-9 release</h1> 21 22<p>We are pleased to announce the Kananaskis-9 release of HOL 4.</p> 23 24<h2 id="contents">Contents</h2> 25<ul> 26 <li> <a href="#new-features">New features</a> </li> 27 <li> <a href="#bugs-fixed">Bugs fixed</a> </li> 28 <li> <a href="#new-theories">New theories</a> </li> 29 <li> <a href="#new-tools">New tools</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<li><p>The <code>Define</code> function for making function definitions now treats each clause (each conjunct) of the definition as independent when assessing the types of the new functions��� parameters. 38For example, the following now works as a definition (termination still has to be proved manually): 39<pre> 40 (f x = x + 1 + g (x > 4)) ��� 41 (g x = if x then f 0 else 1) 42</pre> 43<p> In earlier releases, the parser would have rejected this because the two <code>x</code> parameters would have been required to have the same types (in the clause for <code>f</code>, the author wants <code>x</code> to have type <code>:num</code>, and in the clause for <code>g</code>, type <code>:bool</code>). 44 45<p>This feature is most useful when dealing with algebraic types with numerous constructors, where it can be a pain to keep the names of parameters under constructors apart. 46 47<p>Thanks to Scott Owens for the <a href="http://github.com/mn200/HOL/issues/112">feature suggestion</a>. 48</li> 49 50<li><p>The compilation of pattern-matching in function definitions now attempts to be cleverer about organising its nested case-splits. 51This should result in less complicated definitions (and accompanying induction principles). 52 53<p>Thanks to Thomas T��rk for the implementation of this feature. 54 55</ul> 56 57<h2 id="bugs-fixed">Bugs fixed:</h2> 58 59<ul> 60<li><p> Type abbreviations involving array types (of the form <code>ty1[ty2]</code>) weren���t being pretty-printed. 61Thanks to Hamed Nemati for the bug report. 62(<a href="http://github.com/mn200/HOL/issues/106">GitHub issue</a>) 63 64<li><p> 65It was possible to prove a theorem which caused an unexportable theory. 66Thanks to Joseph Chan for the bug report. 67(<a href="http://github.com/mn200/HOL/issues/115">GitHub issue</a>) 68 69<li><p> 70The error messages printed by, and the documentation for, <code>new_type_definition</code> have been improved. 71Thanks to Rob Arthan for the bug report. 72(<a href="http://github.com/mn200/HOL/issues/128">GitHub issue</a>) 73 74<li><p> 75<code>Holmake</code>���s parsing of nested conditional directives (<code>ifdef</code>, <code>ifeq</code>, <code>ifndef</code> <i>etc.</i>) was incorrect. 76 77<li><p> 78Evaluation and simplification were not correctly handling (real valued) terms such as <code>``0 * 1/2``</code> and <code>``1/2 * 0``</code>. 79 80<li><p> 81Parsing code for tracking the way overloaded constants should be printed stored information in a data structure that grew unreasonably when theories were loaded. 82Thanks to Scott Owens for the bug report. 83 84<li><p> 85The emacs mode got confused when called on to <code>open</code> a theory whose name included the substring <code>_fun_</code>. 86Thanks to Magnus Myreen for the bug report. 87 88</ul> 89 90<h2 id="new-theories">New theories:</h2> 91 92<h2 id="new-tools">New tools:</h2> 93 94<ul> 95<li><p>There is a new tactic <code>HINT_EXISTS_TAC</code> designed to instantiate existential goals. 96If the goal is of the form 97<pre> 98 ���x. P(x) ��� Q(x) ��� R(x) 99</pre> 100<p>and there is an assumption of the form <code>Q(t)</code> (say), then <code>HINT_EXISTS_TAC</code> applied to this goal will instantiate the existential with the term <code>t</code>. 101 102<p>Thanks to Vincent Aravantinos for the <a href="http://github.com/mn200/HOL/commit/e5e35f623cbdb19e1331b119fc5dd3d11f019016">implementation</a> of this tactic. 103 104<li><p>A new tactic, <code>suffices_by</code>, an infix, taking two arguments, a quotation and a tactic. 105When <code>`some term` suffices_by tac</code> is executed, the system attempts to prove that <code>some term</code> implies the current goal by applying <code>tac</code>. 106The sub-goal(s) resulting from the application of <code>tac</code> will be presented to the user, along with <code>some term</code>. 107(<a href="http://github.com/mn200/HOL/issues/116">GitHub issue</a>) 108</p> 109</ul> 110 111<h2 id="new-examples">New examples:</h2> 112 113<ul> 114<li> <p> Theories in <code>examples/parsing</code> to do with context-free languages, their properties and Parsing Expression Grammars. The material not to do with PEGs is derived from Aditi Barthwal���s PhD thesis, with more still to be updated and brought across. 115 116<li> <p> 117Theories in <code>examples/ARM_security_properties</code> provide proofs of several security lemmas for the ARM Instruction Set Architecture. 118To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. 119A proof tool is included, which assists the verification of relational state predicates semi-automatically. 120 121<p> The work has been done as part of the PROSPER project by members from KTH Royal Institute of Technology and SICS Swedish ICT. 122Some of the obtained theorems are tied to that project (but can be adopted for others), while some guarantees are generally applicable. 123 124</ul> 125 126<h2 id="incompatibilities">Incompatibilities:</h2> 127 128<ul> 129 130<li><p>The <code>MEM</code> constant has been replaced with an abbreviation that maps that string to <code>��e l. e ��� set l</code>. 131In other words, if you enter <code>``MEM x mylist``</code>, the underlying term would be <code>x ��� set mylist</code> (recall also that <code>set</code> is another name for <code>LIST_TO_SET</code>). 132The pretty-printer will reverse this transformation so that the same term will print as <code>``MEM e l``</code>. 133The entry-points for making <code>MEM</code>-terms in <code>listSyntax</code> do the right thing. 134Similarly, exporting code with <code>EmitML</code> will continue to work. 135 136<p>Thus, SML code that takes <code>MEM</code>-terms apart using functions like <code>rand</code> and <code>rator</code> will likely need to be adjusted. 137If the SML code uses <code>listSyntax.{dest,mk,is}_mem</code>, it will be fine. 138(<a href="http://github.com/mn200/HOL/issues/52">GitHub issue</a>) 139 140<li><p>The case-constants generated for algebraic data types now have different types. 141The value that is ���switched on��� is now the first argument of the constant rather than the last. 142The names of these constants have also changed, emphasising the change. 143For example, the old constant for natural numbers, <code>num_case</code> had type 144<pre> 145 �� ��� (num ��� ��) ��� num ��� �� 146</pre> 147<p> Now the case constant for the natural numbers is called <code>num_CASE</code> and has type 148<pre> 149 num ��� �� ��� (num ��� ��) ��� �� 150</pre> 151 152<p>This change is invisible if the ���<code>case</code>-<code>of</code>��� syntax is used. 153 154<p>This change makes more efficient evaluation (with <code>EVAL</code>) of expressions with case constants possible. 155 156<p>In addition, the <code>bool_case</code> constant has been deleted entirely: when the arguments are flipped as above it becomes identical to <code>COND</code> (<code>if</code>-<code>then</code>-<code>else</code>). 157This means that simple case-expressions over booleans will print as <code>if</code>-<code>then</code>-<code>else</code> forms. 158Thus 159<pre> 160 > ``case b of T => 1 | F => 3``; 161 val it = ``if b then 1 else 3``: term 162</pre> 163<p>More complicated case expressions involving booleans will still print with the <code>case</code> form: 164<pre> 165 > ``case p of (x,T) => 3 | (y,F) => y``; 166 val it = 167 ``case p of (x,T) => 3 | (x,F) => x``: term 168</pre> 169 170<p>At the ML level, we have tried to retain a degree of backwards compatibility. 171For example, the automatically defined case constants for algebraic types will still be saved in their home-theories with the name ���<i>type</i><code>_case_def</code>���. 172In addition, case terms for the core types of the system (options, lists, numbers, pairs, sums, etc) can still be constructed and destructed through functions in the relevant <i>type</i><code>Syntax</code> modules in the same way. 173For example, <code>numSyntax.mk_num_case</code> still has the type 174<pre> 175 term * term * term -> term 176</pre> 177<p> and the returned term-triple still corresponds to the 0-case, the successor-case and the number-argument (in that order), as before. 178This is despite the fact that the underlying term has those sub-terms in a different order (the number-argument comes first). 179(<a href="http://github.com/mn200/HOL/issues/97">GitHub issue</a>) 180 181 182<li><p> 183The various printing traces in the <code>Goalstack</code> module have been renamed to all be of the form <code>"Goalstack.<some_name>"</code>. 184For example, what was the trace <code>"goalstack print goal at top"</code> is now <code>"Goalstack.print_goal_at_top"</code>. 185This change collects all the goalstack-related traces together when the traces are listed (<i>e.g.</i>, with the <code>traces()</code> command). 186There is also a new trace, <code>"Goalstack.show_stack_subgoal_count"</code>, which, if true (the default), includes the number of sub-goals currently under consideration when a goalstack is printed.</li> 187 188<li><p>The <code>-r</code> command-line option to <code>Holmake</code> now forces recursive behaviour (even with cleaning targets, which is a new feature), rather than being a shorter form of the <code>--rebuild_deps</code> flag. 189 190</ul> 191<hr> 192<div class="footer"> 193<p><em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-9</a></em></p> 194<p>(<a href="kananaskis-8.release.html">Release notes for previous version</a>)</p> 195</div> 196 197</body> </html> 198