HOL4/doc/kananaskis-5.release.html

<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<meta http-equiv="content-type"
      content="text/html ; charset=UTF-8">
<title>Release Notes for Kananaskis-5 version of HOL 4</title>
<style type="text/css">
<!--
  body {color: #333333; background: #FFFFFF;
        margin-left: 1em; margin-right: 1em }
  code, pre {color: #660066; font-weight: bold; /* font-size: smaller */}
-->
</style>

</head>

<body>
<h1>Notes on HOL 4, Kananaskis-5 release</h1>

<p> We are pleased to announce the release of the latest HOL4 system.  We
believe there are a number of exciting new features (runs on Poly/ML,
looks prettier thanks to Unicode support), as well as the usual bug
fixes.</p>

<!-- maybe announce HOL-�� here -->
<p> A new version of the HOL4 theorem prover is also now available,
called HOL-Omega (or HOL<sub>��</sub>).  While backwards compatible,
the HOL-Omega theorem prover implements a more powerful logic, capable
of modelling concepts not expressible in normal higher order logic,
such as monads and concepts from category theory.  See
the <a href="#new-versions">New versions</a> section below for more.
</p>

<h2 id="contents">Contents</h2>
<ul>
  <li> <a href="#new-features">New features</a> </li>
  <li> <a href="#bugs-fixed">Bugs fixed</a> </li>
  <li> <a href="#new-theories">New theories</a> </li>
  <li> <a href="#new-tools">New tools</a> </li>
  <li> <a href="#new-examples">New examples</a> </li>
  <li> <a href="#new-versions">New versions</a> </li>
  <li> <a href="#incompatibilities">Incompatibilities</a> </li>
</ul>


<h2 id="new-features">New features:</h2>

<ul>
<li> <p> There is now a <a href="http://polyml.org">Poly/ML</a>
implementation of HOL4 available for users on platforms other than
Windows. Users should build from the same source-tree, and have
version 5.2 of Poly/ML installed.  The build process is similar.
Start with </p>
<pre>
         poly &lt; tools/smart-configure.sml
</pre>
<p> Continue with </p>
<pre>
         bin/build
</pre>
<p>Most of the features of the Moscow ML implementation should work in
the Poly/ML version, but as it is still rather young, users may
encounter some rough edges.  The advantage of the Poly/ML
implementation is that it is considerably quicker than the Moscow ML
implementation. Many thanks to Scott Owens for doing most of the work
on this port.</p></li>

<li id="syntactic-patterns"><p>Overloading can now target ���syntactic
patterns���, which are terms other than just constants.  Typically a
pattern will be a lambda-abstraction.  For example, one can overload
the symbol <code>&lt;&gt;</code> (meant to represent ���not equal to���)
to the term <code>(\x y. ~(x = y))</code>.  The call would be </p>
<pre>
         overload_on ("&lt;&gt;", ``\x y. ~(x = y)``)
</pre>
<p> It is then possible to write terms such
as <code>``&lt;&gt;&nbsp;a&nbsp;3``</code>.  This will actually
translate to the term <code>``~(a&nbsp;=&nbsp;3)``</code> internally.
Pretty-printing will reverse the transformation so that what was typed
will also be printed.  (One can check that the term really has been
translated as desired with calls to term destructors
like <code>dest_term</code> and <code>strip_comb</code>.)  </p>

<p>Of course, in the case of <code>&lt;&gt;</code>, one would want
this as an infix.  To do this one would use <code>set_fixity</code> as
usual.  In this case, </p>
<pre>
         set_fixity "&lt;&gt;" (Infix(NONASSOC, 450))
</pre>
<p> would be appropriate.  (See
the <a href="#incompatibilities">Incompatibilities section</a> below
on the change to the associativity of grammar level 450.)</p>

<p>Finally, overloading can be type-specific.  In this way, the
default system now overloads the ASCII <code>&lt;=&gt;</code> to
equality over the booleans.  Various operators over strings now use
the same technology as well (see
<a href="#strings-as-charlists">below</a>). </p>

<p>The system has syntactic patterns built-in for not-equal (as
above), iff (the <code>&lt;=&gt;</code> symbol), not-iff
(<code>&lt;=/=&gt;</code>), and not-an-element-of
(<code>NOTIN</code>).  The Unicode variants
(see <a href="#unicode">later item</a>) for these
are <code>���</code>, <code>���</code>, <code>���</code>,
and <code>���</code>. </p></li>

<li id="strings-as-charlists"><p>The <code>:string</code> type is now
an alias for <code>:char list</code>, meaning that strings inherit all
of the list operations ���for free���.  Existing string operators that are
effectively duplicates of operations on lists
(like <code>STRLEN</code> and <code>STRCAT</code>) are now
type-specific overloads of the list constants.</p>

<p>Note that this means that the <code>IMPLODE</code>
and <code>EXPLODE</code> functions are now identities, and that
theorems that used to print as </p>
<pre>
         ��� STRLEN s = LENGTH (EXPLODE s)
</pre>
<p> are still true, but are now looping rewrites.
(The <code>STRLEN</code> in the theorem is the same term as
the <code>LENGTH</code>, and in fact the theorem (now
called <code>STRLEN_EXPLODE_THM</code>) prints
with <code>STRLEN</code> in both positions.)</p>

<p>The <code>EXPLODE</code> and <code>IMPLODE</code> constants are
still useful if theorems are to be exported to ML, where strings are
not the same type as lists of characters.</p>
</li>

<li> <p> Types can now be numerals, as long as <code>fcpTheory</code>
(the theory of finite cartesian products) is loaded.  A numeral type
has no interesting properties except that the cardinality of its
universe has exactly the size given by the numeral.  This implies that
negative number types and the type :0 do not exist.  The
pretty-printing of numeral types can be turned off with the trace
flag <code>pp_num_types</code>. </p>

<p> This removes the need for type abbreviations <code>i32</code> and
others, and also the function <code>fcpLib.mk_index_type</code>, which
has been removed. </p></li>

<li> <p> The finite cartesian product &ldquo;array&rdquo; type can now
be written with square brackets rather than with the
infix <code>**</code> operator.  This combines well with the numeric
types above.  For example, <code>:bool[32]</code> is a type of 32
booleans, and indeed is now the type used for what had been previously
called <code>word32</code>. The pretty-printing of array types can be
turned off with the trace flag <code>pp_array_types</code>. </p>

<p> Unfortunately, because of lists, at the term level one can not
index arrays with square brackets.  Instead, we recommend the
infix <code>'</code> operator (that���s an apostrophe, ASCII character
#39).  For example, <code>array ' 3</code> is the value of the fourth
element of <code>array</code> (indexing starts at zero!)</p>
</li>

<li> <p> Errors in inductive relation definitions (made
with <code>Hol_reln</code>) are now accompanied by better location
information. </p></li>

<li> <p> Errors in quotient type definitions (made with entry-points
in <code>quotientLib</code>) are now accompanied by better
diagnostics about problems like missing respectfulness results.</p></li>

<li><p> If HOL is started in a directory with
<code>INCLUDES</code> specified in a <code>Holmakefile</code>, then
those same includes are put onto the <code>loadPath</code> that is
used interactively.  This should help interactive debugging of
multiple-directory developments.</p>

<p>If <code>Holmake</code> is run in a directory
with <code>INCLUDES</code> specified in a <code>Holmakefile</code>,
then it will call itself recursively in those directories before
working in the current directory.  This behaviour can be prevented by
using the <code>--no_prereqs</code> option on the command-line, or by
including <code>NO_PREREQS</code> as an <code>OPTION</code> in
the <code>Holmakefile</code>.</p>
</li>

<li> <p> The <code>tautLib</code> decision procedure for propositional
    logic now uses external SAT solvers (through
the <code>HolSatLib</code> code) for all but the smallest goals,
translating proofs back through the HOL kernel.</p></li>

<li> <p> In the Emacs mode: provide a new option to the
work-horse <code>M-h&nbsp;M-r</code> command: if you precede it by
hitting <code>C-u</code> twice, it will
toggle <code>quietdec</code> around what is to be pasted into the HOL
session.  This can be useful if you���re opening a whole slew of big
theories and don���t want to have to watch grammar guff scroll
by.</p></li>

<li> <p> The termination prover under <code>Define</code> is now
smarter.  It now does a better job of guessing termination relations,
using a relevance criterion to cut down the number of lexicographic
combinations that are tried.  It can handle <code>DIV</code>
and <code>MOD</code> now, through the <code>termination_simps</code>
variable, which can be added to in order to support other destructor
functions.</p>

<p> Termination proofs for functions defined recursively over words
are also supported.  The system knows about subtracting 1 and also
right-shifting. </p></li>

<li> <p> Post processing for word parsing is supported with the function:</p>
<pre>
         wordsLib.inst_word_lengths : term -> term
</pre>
<p>
When possible, word lengths are guessed for the extract and
concatenate functions.  That is, <code>``(a&nbsp;&gt;&lt;&nbsp;b)&nbsp;w``</code> is given
type <code>``:(a+1-b)&nbsp;word``</code> and <code>``(a:&nbsp;a&nbsp;word) @@ (b:&nbsp;b&nbsp;word)``</code> is
given type <code>``:(a&nbsp;+&nbsp;b)&nbsp;word``</code>.</p>

<p>For example:</p>
<pre>
         - val _ = Parse.post_process_term := wordsLib.inst_word_lengths;
         - ``(3 &gt;&lt; 0) a @@ (7 &gt;&lt; 4) a @@ (16 &gt;&lt; 8) a``;
         &lt;&lt;HOL message: inventing new type variable names: 'a, 'b, 'c, 'd, 'e, 'f&gt;&gt;
         &lt;&lt;HOL message: assigning word length(s): 'a &lt;- 4, 'b &lt;- 13, 'c &lt;- 17, 'e &lt;- 4 and 'f &lt;- 9&gt;&gt;
         > val it = ``(3 &gt;&lt; 0) a @@ (7 &gt;&lt; 4) a @@ (16 &gt;&lt; 8) a`` : term
</pre>
<p>
The assignment message is controlled by the trace variable
<code>"notify word length guesses"</code>.</p>
</li>

<li>
<p> <code>wordsLib</code> now supports evaluation over non-standard
word-sizes:</p>
<pre>
         - load "wordsLib";
         > val it = () : unit
         - EVAL ``123w + 321w:bool[56]``;
         > val it = |- 123w + 321w = 444w : thm
</pre>
<p>Non-standard word sizes will evaluate more slowly when first used.
However, size theorems are then added to the compset, so subsequent
evaluations will be quicker.
</p></li>

<li id="unicode">
<p> HOL now supports Unicode symbols as part of its parsing and
printing.  In addition, there are now appropriate Unicode symbols,
such as <code>���</code> and <code>���</code> built in to the system.  To
enable their printing and parsing, you must set the trace
variable <code>Unicode</code>.  If this is done, you will see, for
example</p>
<pre>
         - FORALL_DEF;
         > val it = |- $��� = (��P. P = (��x. T)) : thm
</pre>
<p> If you turn Unicode on, and see gibberish when you print terms and
theorems, your fonts and system are not Unicode and UTF-8 compatible.
Emacs versions past 22 can be made to work, as can normal shells on
MacOS and Linux.  The latest versions of Emacs on Windows support
UTF-8, and so running HOL inside Emacs on Windows gives a pleasant
Unicode experience there too. </p>

<p>The <code>Unicode</code> trace controls the use of Unicode symbols
that are set up as explicit alternatives for ASCII equivalents.  To
set up such an aliasing, use the function</p>
<pre>
         Unicode.unicode_version : {u:string,tmnm:string} -> unit
</pre>
<p> where the string <code>u</code> is the Unicode, and
where <code>tmnm</code> is the name of the term being aliased.  Note
that you can also alias the names of syntactic patterns
(<a href="#syntactic-patterns">see above</a>). </p>
<p> You are also free to use the standard grammar manipulation
functions to define pretty Unicode syntax that has no ASCII equivalent
if you wish, and this can be done whether or not
the <code>Unicode</code> trace is set.</p>
</li>

<li>
  <p> A new function <code>limit</code>:</p>
<pre>
         limit : int -> simpset -> simpset
</pre>
  <p> can be used to limit the number of rewrites a simpset applies.
  By default a simpset will allow the simplifier to apply as many
  rewrites as match, possibly going into an infinite loop thereby.
  The <code>limit</code> function puts a numeric limit on this,
  usually guaranteeing the simplifier���s termination (it will still
  loop if a user-provided conversion or decision procedure loops).</p>
</li>

<li id="unary-minus">
<p> Operators (<i>e.g.</i> <code>&amp;</code> and <code>-</code>) can
now be both prefix and infix operators simultaneously.  In particular,
the subtraction operator (<code>-</code>) is now also a prefix in all
theories descended from <code>arithmetic</code>.  In order to use this
as a negation, you must overload the
string <code>"numeric_negate"</code>, which is the abstract syntax
name of the unary minus.  Thus, in <code>integerTheory</code>, the
line </p>
<pre>
         val _ = overload_on("numeric_negate", ``int_neg``)
</pre>
<p>sets up unary minus as a symbol for negation over the integers.</p>

<p>This change allows one to input terms such
as <code>``-x&nbsp;+&nbsp;y``</code> even in the theory of natural
numbers.  In this context, the unary negation maps to a variable
called <code>numeric_negate</code>, which is unlikely to be helpful.
Luckily, the variable will likely be polymorphic and the warning about
invention of type variables will serve as a clue that something
dubious is being attempted.</p>

<p>In the existing numeric theories, we have kept <code>~</code> as a
unary negation symbol as well (following SML���s example), but the
unary minus is now the preferred printing form.</p>

<p>If you wish to add an existing binary operator as a prefix, it is
important that you <em>not</em> use the <code>set_fixity</code>
command to do it.  This command will clear the grammar of your binary
operator before adding the unary one.  Better to
use <code>add_rule</code> (for which, see the Reference Manual).  This
will also allow you to map the unary form to a different name.  With
subtraction, for example, the binary operator maps to the
name <code>"-"</code>, and the unary operator maps
to <code>"numeric_negate"</code>.</p>

<p>Finally, note that in the HOL language, unary minus and binary
minus are inherently ambiguous.  Is <code>x-y</code> the application
of binary minus to arguments <code>x</code> and <code>y</code>, or is
it the application of function <code>x</code> to
argument <code>-y</code>?  In this situation, the implementation of
this feature treats these dual-purpose operators as infixes by
default.  In order to obtain the second reading above, one has to
write <code>x(-y)</code>. </p>

<p>(<a href="#unary-minus-incompat">See below</a> for discussion of
the backwards incompatibility this causes to users of
the <code>words</code> theory.)</p>
</li>

<li>
<p>It is now possible to use the simplifier to rewrite terms with
respect to arbitrary pre-orders.  The entry-point is the function</p>
<pre>
         simpLib.add_relsimp :
            {trans: thm, refl: thm, subsets: thm list,
             rewrs: thm list, weakenings: thm list} ->
            simpset -> simpset
</pre>
<p>where the <code>trans</code> and <code>refl</code> fields are the
theorems stating that some relation is a pre-order.
The <code>weakenings</code> field is a list of congruences justifying
the switch from equality reasoning to reasoning over the pre-order.
For example, all equivalences (<code>���</code>, say) will have the
following be true
</p>
<pre>
         |- (M1 ��� M2) ==> (N1 ��� N2) ==> ((M1 ��� N1) <=> (M2 ��� N2))
</pre>
<p>With the above installed, when the simplifier sees a term of the
form <code>M1&nbsp;���&nbsp;N1</code> it will rewrite both sides using
the relation <code>���</code>.</p>
<p>See the Description manual���s section on the simplifier for more.</p>

</li>

</ul>

<h2 id="bugs-fixed">Bugs fixed:</h2>

<ul>
<li> <code>EVAL ``BIGUNION {}``</code> now works.</li>

<li> <p> Fixed a subtle bug in termination condition extraction,
whereby multiple <code>let</code>-bindings for a variable would
cause <code>Define</code> to be unpredictable and sometimes broken.
Now variables get renamed in order to make the definition process
succeed. </p></li>

<li> <p> <code>ASM_MESON_TAC</code> (which lives
beneath <code>PROVE_TAC</code>) now properly pays attention to the
controlling reference variable <code>max_depth</code>.</p></li>

<li><p> Fixed an error in the build process when
building <code>mlyacc</code> from sources on Windows.</p></li>

</ul>


<h2 id="new-theories">New theories:</h2>
<ul>
<li>A theory of Patricia trees, due to Anthony Fox.</li>
</ul>

<h2 id="new-tools">New tools:</h2>

<ul>
<li>A new library <code>HolSmtLib</code> provides an oracle interface
to external SMT solvers.
</li>

<li><p>There are a number of new facilities in <code>wordsLib</code>.
The main additions are:</p>

<dl>
<dt><code>WORD_ss</code>:</dt> <dd> Does some basic simplification,
evaluation and AC rewriting
(over <code>*</code>, <code>+</code>, <code>&amp;&amp;</code>
and <code>!!</code>).  For example,
<pre>
         ``a * 3w + a``  --&gt;  ``4w * a``
</pre>
and
<pre>
         ``a &amp;&amp; 3w !! a &amp;&amp; 2w``  --&gt;  ``3w &amp;&amp; a``
</pre></dd>

<dt><code>BIT_ss</code>:</dt> <dd>For example, <code>``BIT&nbsp;n&nbsp;3``&nbsp;--&gt;&nbsp;``n&nbsp;IN&nbsp;{0;&nbsp;1}``</code></dd>

<dt><code>WORD_MUL_LSL_ss</code>:</dt>
<dd>Converts multiplications to left-shifts e.g.
  <code>``2w * a`` --> ``a&nbsp;&lt;&lt;&nbsp;1``</code></dd>

<dt><code>WORD_BIT_EQ_ss</code>:</dt>
<dd>Can be used to establish bit-wise (in)equality <i>e.g.</i>
  <code>``a &amp;&amp; ~a = 0w``&nbsp;--&gt;&nbsp;``T``</code>
Does not work with <code>*</code>, <code>+</code> <i>etc.</i></dd>

<dt><code>WORD_ARITH_EQ_ss</code>:</dt>
<dd> Can be used to establish arithmetic (in)equality <i>e.g.</i>
  <code>``~(b + 1w = b + 4294967295w:word32)`` --&gt; ``T``</code>
</dd>

<dt><code>WORD_EXTRACT_ss</code>:</dt>
<dd>
Simplification for shifts and bit extraction.
Simplifies <code>--</code>, <code>w2w</code>, <code>sw2sw</code>, <code>#>></code>, <code>@@</code> <i>etc.</i> and expresses operations
  using <code>&gt;&lt;</code>, <code>&lt;&lt;</code> and <code>!!</code>.</dd>

<dt><code>WORD_DECIDE</code>:</dt>
<dd>A decision procedure.  Will solve Boolean (bitwise) problems
  and some problems over &lt;, &lt;+ etc.</dd>
</dl>
</li>
</ul>

<h2 id="new-versions">New versions:</h2>

<ul>
<li>
<p>
The HOL-Omega or HOL<sub>��</sub> system presents a more powerful version
of the widely used HOL theorem prover.  This system implements a new logic,
which is an extension of the existing higher order logic of HOL4. The logic
is extended to three levels, adding kinds to the existing levels of types
and terms.  New types include type operator variables and universal types
as in System F.  Impredicativity is avoided through the stratification of
types by ranks according to the depth of universal types.  The HOL-Omega
system is a merging of HOL4, HOL2P by V&ouml;lker, and major aspects of
System F<sub>��</sub> from chapter 30 of
<i>Types and Programming Languages</i> by Pierce.
As in HOL4, HOL-Omega was constructed according to the design principles
of the LCF approach, for the highest degree of soundness.
</p>

<p>
The HOL-Omega system is described in the paper
<a href="http://www.trustworthytools.com/holw/holw-lncs5674.pdf"><i>The HOL-Omega Logic</i></a>,
by Homeier, P.V., in Proceedings of TPHOLs 2009, LNCS vol. 5674, pp. 244-259.
The paper presents the abstract syntax and semantics for the ranks, kinds,
types, and terms of the logic, as well as the new fundamental axioms
and rules of inference.  It also presents examples of using the HOL-Omega
system to model monads and concepts from category theory such as functors
and natural transformations.  As an example,
here is the definition of functors, as a type abbreviation and a term predicate:
</p>

<pre>
   (*---------------------------------------------------------------------------
               Functor type abbreviation
    ---------------------------------------------------------------------------*)

   val _ = type_abbrev ("functor", Type `: \'F. !'a 'b. ('a -> 'b) -> 'a 'F -> 'b 'F`);

   (*---------------------------------------------------------------------------
               Functor predicate
    ---------------------------------------------------------------------------*)

   val functor_def = new_definition("functor_def", Term
      `functor (F': 'F functor) =
         (* Identity *)
             (!:'a. F' (I:'a->'a) = I) /\
         (* Composition *)
             (!:'a 'b 'c. !(f:'a -> 'b) (g:'b -> 'c).
                    F' (g o f) = F' g o F' f)
      `);
</pre>

<p>
The HOL-Omega implementation may be downloaded by the command</p>
<pre>
   svn checkout https://hol.svn.sf.net/svnroot/hol/branches/HOL-Omega
</pre>
<p>Installation instructions are in the top directory.
HOL-Omega may be built using either the standard or the experimental kernel,
and either Moscow ML or Poly/ML, by the same process as for HOL4.
This implementation is still in development but is currently useful.
This provides a practical workbench for developments in the HOL-Omega
logic, integrated in a natural and consistent manner with the existing HOL4
tools and libraries that have been refined and extended over many years.
Examples using the new features of HOL-Omega may be found in the directory
<code>examples/HolOmega</code>.
</p>

<p>
This implementation was designed with particular concern for backward
compatibility with HOL4.  This was almost entirely achieved, which was
possible only because the fundamental data types representing types and
terms were originally encapsulated.  This meant that the underlying
representation could be changed without affecting the abstract view of
types and terms by the rest of the system.  Virtually all existing HOL4
code will build correctly, including the extensive libraries.
The simplifiers have been upgraded, including higher-order matching of
the new types and terms and automatic type beta-reduction.  Algebraic
types with higher kinds and ranks may be constructed using the familiar
<code>Hol_datatype</code> tool.  Not all of the tools will work as
expected on the new terms and types, as the revision process is ongoing,
but they will function identically on the classic terms and types.
So nothing of HOL4���s existing power has been lost.
</p>

<p>
More information may be found at
<a href="http://www.trustworthytools.com">http://www.trustworthytools.com</a>.
</li>
</ul>

<h2 id="new-examples">New examples:</h2>

<ul>
<li><p><code>examples/machine-code</code> contains a development of
verified Lisp implementations on top of formal models of hardware
instruction sets for the ARM, PowerPC and x86 chips.  This is work
done by Magnus Myreen.  <strong>Note:</strong> This
example <em>must</em> be built with Poly/ML. </p></li>


<li> <p> <code>examples/hol_dpllScript.sml</code> contains a very
simplistic HOL implementation of DPLL with unit propagation, with
proofs of termination, completeness and soundness. </p> </li>

<li><p><code>examples/misc/PropLogicScript.sml</code> contains
soundness and completeness results for a classical propositional
logic.</p></li>

<li><p>A formalisation of Symbolic Trajectory Evaluation, contributed
by Ashish Darbari.</p></li>

</ul>

<h2 id="incompatibilities">Incompatibilities:</h2>

<ul>

<li><p> The <code>emacs</code> mode is now found in the
  file <code>tools/hol-mode.el</code> (rather
  than <code>hol98-mode.el</code>) and all of the occurrences of the
  string <code>hol98</code> there have been replaced
  by <code>hol</code>.</p> </li>

<li> <p> The <code>muddy</code> code, and the packages that depend on it
(<code>HolBdd</code> and <code>HolCheck</code>) have moved from
the <code>src</code> directory into <code>examples</code>.  If you
wish to use any of these packages, you will now have to both build
them (see below), and then explicitly include the directories in
your <code>Holmakefile</code>s.  For example, the following line at
the top of a <code>Holmakefile</code> will give access
to <code>HolBdd</code> (and its dependency, <code>muddy</code>):</p>
<pre>
         INCLUDES = $(protect $(HOLDIR)/examples/muddy) $(protect $(HOLDIR)/examples/HolBdd)
</pre>
<p> To build these libraries: </p>
<ol>
<li> On Windows, copy <code>tools\win-binaries\muddy.so</code>
to <code>examples\muddy\muddyC</code>.  On other platforms,
type <code>make</code> in <code>examples/muddy/muddyC</code>.</li>
<li> Do <code>Holmake</code> in <code>examples/muddy</code>.</li>
<li> Do <code>Holmake</code> in <code>examples/HolBdd</code>.</li>
<li> Do <code>Holmake</code> in <code>examples/HolCheck</code>.</li>
</ol>

<p> On 64-bit Unices, users report having to add
the <code>-fPIC</code> option to the <code>CFLAGS</code> variable
at</p>
<ul>
<li> <code>src/muddy/muddyC/Makefile</code>
     <li> <code>src/muddy/muddyC/buddy/config</code>
</ul>


</li>

<li> <p>The <code>FIRSTN</code> and <code>BUTFIRSTN</code> constants from
the theory <code>rich_list</code> are now defined in the
theory <code>list</code>, with names <code>TAKE</code>
and <code>DROP</code>.  If you load <code>rich_listTheory</code>, then
the old names are overloaded so that parsing existing theories should
continue to work.  The change may cause pain if you have code that
expects the constants to have their old names (for a call
to <code>mk_const</code> say), or if you have variables or constants
of your own using the names <code>TAKE</code>
and <code>DROP</code>.</p>

<p>Similarly, the <code>IS_PREFIX</code> constant
from <code>rich_listTheory</code> is now actually an overload to a
pattern referring to the constant <code>isPREFIX</code>
in <code>listTheory</code> (this was the name of the corresponding
constant in <code>stringTheory</code>
(see <a href="#strings-as-charlists">above</a>).  The new constant
takes its arguments in the reverse order (smaller list first), and
prints with the infix symbol <code>&lt;&lt;=</code>.  The
quotation <code>`IS_PREFIX&nbsp;l1&nbsp;l2`</code> will produce a term
that prints as <code>``l2&nbsp;&lt;&lt;=&nbsp;l1``</code>, preserving the
appropriate semantics.  (The Unicode symbol for this infix
is <code>���</code>.)</p>
</li>

<li> <p> The <code>SET_TO_LIST</code> constant is now defined
in <code>listTheory</code> (moved from <code>containerTheory</code>),
which now depends on the theory of sets (<code>pred_setTheory</code>).
The <code>LIST_TO_SET</code> constant is now also overloaded to the
easier-to-type name <code>set</code>.  A number of theorems about both
functions are now in <code>listTheory</code>, and because the theory
of lists depends on that of sets, so too does the standard HOL
environment loaded by <code>bossLib</code>.  All of the theorems
from <code>containerTheory</code> are still accessible in the same
place, even though they are now just copies of theorems proved
in <code>listTheory</code>.</p>

<p>If the presence of a constant called <code>set</code> causes pain
because you have used the same string as a variable name and don���t
wish to change it, the constant can be hidden, and the interference
halted, by using <code>hide</code>:</p>
<pre>
         hide "set";
</pre>
</li>

<li><p>The <code>parse_in_context</code> function (used heavily in
the <code>Q</code> structure) is now pickier about its parses.  Now
any use of a free variable in a quotation that is parsed must be
consistent with its type in the provided context.</p></li>

<li><p>The user-specified pretty-printing functions that can be added
to customise printing of terms (using <code>add_user_printer</code>),
now key off term patterns rather than types.  Previously, if a term
was of a the type specified by the user, the user���s function would be
called.  Now, if the term matches the provided pattern, the function
is called.  The old behaviour can be emulated by simply giving as the
pattern a variable of the desired type.</p>

<p>Additionally, the user���s function now gets access to a richer
context of arguments when the system printer calls it.</p>

</li>

<li> <p>Precedence level 450 in the standard term grammar is now
non-associative, and suggested as an appropriate level for binary
relations, such as <code>=</code>, <code>&lt;</code>
and <code>���</code>.  The list cons operators <code>::</code> has moved
out of this level to level 490, and the <code>++</code> operator used
as a shorthand for list concatenation (<code>APPEND</code>) has moved
to 480.  (This preserves their relative positioning.)
</p></li>

<li id="unary-minus-incompat">
<p> The <a href="#unary-minus">new feature allowing unary minus</a>
causes the way unary minus was handled in <code>wordsTheory</code> to
fail.  There the unary minus (���twos complement��� in fact) could be
accessed by writing things like <code>``$-&nbsp;3w&nbsp;+&nbsp;x``</code>.  One
should now write <code>``-3w&nbsp;+&nbsp;x``</code>.  If converting
one���s script files is going to be too arduous, the old behaviour can
be achieved by including the line</p>
<pre>
         val _ = temp_overload_on ("-", ``word_2comp``)
</pre>
<p>at the top of the given script file. </p>
</li>

</ul>


<hr>

<p> <em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-5</a></em> </p>

</body> </html>