\appendix \chapter{Version 2.0}\label{appendix} This appendix summarizes the differences between \HOL 88 Version 2.0 and the last major release, which was Version 1.11 (Version 1.12 is essentially the Version 2.0 system with the Version 1.10 documentation). Version 2.0 is primarily a rationalization of Version 1.11. Relics of \LCF\ have been deleted and many `internal' \ML\ bindings have been made local to the functions that use them. It is hoped that nothing useful has been inadvertently removed. The top-level directory of the \HOL\ distribution sources has been reorganized. The details are in Chapter 1 of \TUTORIAL\ (`Getting and Installing \HOL'). An important addition is a directory {\small\verb%contrib%} containing contributions from the \HOL\ user community. The aim of this directory is to make it easy for the community to share theories, proofs, examples, tools, documents, and other material which may be of general interest. Unlike the library, there is no quality control on {\small\verb%contrib%}. Two major revisions of the theorem-proving tools in Version 2.0 are the complete reimplementations, by Tom Melham, of (i) the resolution rules and tactics and (ii) the type definition package. The resolution tools have been rewritten so that they are more systematic and predictable. Unfortunately, this means that sometimes different results are produced, and so code using {\small\verb%RES_TAC%}, {\small\verb%IMP_RES_TAC%} \etc\ may need to be modified to run in Version 2.0. This is particularly likely if tactics have been used that depend on the positions of assumptions in goals (this is generally considered `bad style'). The old resolution tools are available in the directory {\small\verb%contrib/resolve%}. The type definition package (i.e. the \ML\ function {\small\verb%define_type%}) has been rewritten to be faster and more robust. A number of identifier names have changed and its internal workings have been reorganized. A tool for mutually recursive type definitions is available in {\small\verb%contrib/mut_rec_types%} (it was produced by students at Aarhus University). Four libraries from Version 1.11 of HOL have been temporarily withdrawn, because the Cambridge group have been unable to rebuild them in Version 2.0. These are: \begin{hol}\begin{verbatim} card well_order zet csp \end{verbatim}\end{hol} \noindent The first three are difficult to rebuild because of changes to resolution. They rely very heavily on the order in which the assumptions of goals appear. The fourth library uses the {\small\verb%set%} library, which has been substantially modified. These four libraries have been moved to {\small\verb%contrib%} until they are updated by their authors. Version 2.0 provides parser and pretty-printer support for restricted quantification and set-theoretic notation. The restricted quantification notation allows terms of the form \con{Q}$x${\small\verb%::%}$p${\small\verb%.%}$t[x]$, where \con{Q} is a quantifier and if $x:\alpha$ then $p$ can be any term of type $\alpha\fun\bool$; this denotes the quantification of $x$ over those values satisfying $p$. The qualifier {\small\verb%::%} can be used with {\small\verb%\%} and any binder, including user defined ones; the appropriate meanings are predefined for {\small\verb%\%} and the built-in binders {\small\verb%!%}, {\small\verb%?%} and {\small\verb%@%}. This provides a method of simulating subtypes and dependent types; the qualifying predicate $p$ can be an arbitrary term containing parameters. For example: {\small\verb%!%}$w${\small\verb%::%}$\con{Word}(n)${\small\verb%. %}$t[w]$, for a suitable constant \con{Word}, simulates a quantification over the `type' of $n$-bit words. Experiments are needed to establish how satisfactory this approach is. The syntactic mechanism, although implemented initially to support restricted quantification, can also be used to support better approximations to notations like $\sum_{i=1}^{n}x_i$; this could, for example, be represented by $\con{Sum}\ i ${\small\verb%::(1,%}$n${\small\verb%).%}$\ x_i$, via a suitable definition of the constant $\con{Sum}$. The set notation allows finite sets to be written in the form {\small\verb%"{%}$t_1,t_2,\ldots,t_n${\small\verb%}"%}. It also supports set abstraction notation of the form {\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%}; for example {\small\verb%"{2*x|x>0}"%} and {\small\verb%"{(x,y)|x=y}"%}. Both these notations can be mounted onto any underlying set theory (or even onto theories of lists, bags etc.), although they were initially designed for use with the library \ml{sets} (which was previously called \ml{all\_sets}). This library has been greatly extended. Version 2.0 has libraries {\small\verb%parser%} and {\small\verb%prettyp%}, which provide parser and pretty-printer support for embedded languages. These are currently being used to provide theorem-proving tools for the hardware description languages {\small ELLA}, {\small VHDL} and {\small SILAGE}, and for various other special purpose languages. A mechanism called ``syntax blocks'' allows user-specified parsers to be invoked from \ML. The development of methodologies for embedding application-specific languages in \HOL\ is a major topic of research at Cambridge. A facility is provided to support experiments with user-programmed quotation typecheckers for the \HOL\ logic. This enables more type inference to be implemented. Many new conversions are provided. The most useful ones are described in Section~\ref{CONVERSIONS} below. In the sections that follow, those new things in Version 2.0 which are likely to be of most general use are described. Section~\ref{adddel} list the \ML\ bindings that have ben added and deleted in Version 2.0. \section{Directory reorganization} The help files and manual have been split apart into two separate directories. The top-level of the \HOL\ distribution directory now contains: \begin{itemize} \item \ml{Manual}: directory containing the manual sources; \item \ml{help}: directory containing text files for online help, as well as for the \REFERENCE\ part of the manual. \end{itemize} \noindent The search path mechanism has been revised in various ways. Library pathnames are now no longer on the default search path, nor are they added to the search path when a library is loaded (it is the responsibility of the library's load-file to do this, if desired). As a consequence, the predefined \ML\ value \ml{Libraries} is no longer used. The initial search path is now: \begin{hol}\begin{alltt} [``; `~/`; `\(directory\)/theories/`] \end{alltt}\end{hol} \noindent where $directory$ is the site-specific absolute pathname in which the \HOL\ distribution directory (`\ml{hol}') resides. The \ML\ functions \ml{add\_to\_search\_path} and \ml{append\_to\_search\_path} are no longer built-in. Users may define them, if required, by: \begin{hol}\begin{verbatim} let add_to_search_path p = set_search_path(p.search_path()) let append_to_search_path p = set_search_path(search_path()@[p]) \end{verbatim}\end{hol} The \ml{install} function now sets the search path to: \begin{hol}\begin{alltt} [``; `~/`; \(arg\)^`/theories/`] \end{alltt}\end{hol} \noindent where $arg$ is the string argument to install. \section{Location of libraries} The function \begin{holboxed}\index{library_pathname@\ml{library\_pathname}} \begin{verbatim} library_pathname : void -> string \end{verbatim}\end{holboxed} \noindent returns the internal pathname used by \HOL\ to load libraries. This pathname, which is site-specific and is given an initial value when the system is built, should be the absolute pathname of the \HOL\ system library directory. This pathname will typically have the form: \begin{hol}\begin{alltt} `\(directory\)/hol/Library` \end{alltt}\end{hol} \noindent where $directory$ is the site-specific absolute pathname in which the \HOL\ distribution directory (`\ml{hol}') resides. The value returned by \ml{library\_pathname} can be changed by users only via the \ml{install} function. The string returned by \ml{library\_pathname} is primarily used in library load-files to update the \HOL\ search path and help search path. For example, suppose that in a library \ml{lib} there is a directory \ml{help} which contains online help files specific to this library. The load-file {\small\verb%lib.ml%} can then update the help search path as follows: \begin{hol}\begin{verbatim} let path = library_pathname() ^ `/lib/help/` in set_help_search_path (path . help_search_path()) \end{verbatim}\end{hol} \noindent This will make the help files of the library \ml{lib} available for online help whenever the library is loaded. \section{More flexible help system}\index{help@\ml{help}}\index{help system|(} The help system now uses \ml{cat} rather than \ml{more} as the default for displaying help files. This default can be changed with the \ML\ function: \begin{holboxed}\index{set_help@\ml{set\_help}} \begin{verbatim} set_help : string -> string \end{verbatim}\end{holboxed} \noindent This installs a new user-supplied help function, and returns the previous one as result. The effect of \begin{hol}\begin{alltt} help `\(file\)` \end{alltt}\end{hol} \noindent is to pipe the appropriate help file derived from $file${\small\verb%.doc%} into the current help function, with the top level of \ML\ being the standard output. For example, \begin{hol}\begin{verbatim} set_help `lpr` \end{verbatim}\end{hol} \noindent will cause the help file to be printed instead of being displayed and \begin{hol}\begin{verbatim} set_help `lpr -Pbarf` \end{verbatim}\end{hol} \noindent will cause it to be printed to the printer \ml{barf}. Two new functions: \begin{holboxed} \index{set_help_search_path@\ml{set\_help\_search\_path}} \index{help_search_path@\ml{help\_search\_path}} \begin{verbatim} set_help_search_path : string list -> void help_search_path : void -> string list \end{verbatim}\end{holboxed} \noindent have been added to the system for accessing the internal search path used by \HOL\ to find online help files. The help search path has precisely the same format as the regular search path, and these two function are analogous to the \ML\ functions \ml{search\_path} and \ml{set\_search\_path}.\index{help system|)} \section{Syntax for restricted quantification} \index{types, in HOL logic@types, in \HOL\ logic! dependent} \index{dependent types in HOL logic@dependent types in \HOL\ logic} Syntactic support for restricted quantification and abstraction is now provided. This follows a suggestion discussed at the Second \HOL\ Users Meeting and implements a method of simulating subtypes and dependent types with predicates. Currently no derived rules are provided to support this notation, so any inferences will need to work on the underlying semantic representation. The new syntax automatically translates as follows: \begin{hol} {\small\verb% \%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_ABSTRACT %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\ {\small\verb% !%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_FORALL %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\ {\small\verb% ?%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_EXISTS %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\ {\small\verb% @%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_SELECT %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%} \end{hol} Anything can be written between the binder and `\ml{::}' that could be written between the binder and `\ml{.}` in the old notation. See the examples below. The flag \ml{print\_restrict} has default \ml{true}, but if set to \ml{false} will disable the pretty printing. This is useful for seeing what the semantics of particular restricted abstractions are. The constants \ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and \ml{RES\_SELECT} are defined in the theory \ml{bool} by: \begin{hol}\begin{verbatim} RES_ABSTRACT P B = \x:*. (P x => B x | ARB:**) RES_FORALL P B = !x:*. P x ==> B x RES_EXISTS P B = ?x:*. P x /\ B x RES_SELECT P B = @x:*. P x /\ B x \end{verbatim}\end{hol} \noindent where the constant \ml{ARB} is defined in the theory \ml{bool} by: \begin{hol}\begin{verbatim} ARB = @x:*. T \end{verbatim}\end{hol} User-defined binders can also have restricted forms, which are set up with the function: \begin{holboxed}\index{associate_restriction@\ml{associate\_restriction}} \begin{verbatim} associate_restriction : (string # string) -> * \end{verbatim}\end{holboxed} \noindent If \m{B} is the name of a binder and \ml{RES\_}$B$ is the name of a suitable constant (which must be explicitly defined), then executing: \begin{hol} {\small\verb% associate_restriction(`%}\m{B}{\small\verb%`, `RES_%}\m{B}{\small\verb%`)%} \end{hol} \noindent will cause the parser and pretty-printer to support: \begin{hol} {\small\verb% %}$B$ $v${\small\verb%::%}$P${\small\verb%. %}$B${\small\verb% <----> RES_%}$B$ $P${\small\verb% (\%}$v${\small\verb%. %}$B${\small\verb%)%} \end{hol} \noindent Note that associations between user defined binders and their restrictions are not stored in theory files, so they have to be set up for each \HOL\ session (e.g. with a {\small\verb%hol-init.ml%} initialization file). Here is an example session: \setcounter{sessioncount}{1} \begin{session}\begin{verbatim} #"!x y::P. x (!x'. P x' ==> (?x. Q x /\ (x(@x. R x /\ T) = x + x')))) \end{verbatim}\end{session} The variable \ml{x} in the definitions of the constants \ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and \ml{RES\_SELECT} gets confused with the variable in the supplied term. This can be avoided by changing \ml{RESTRICT\_CONV} to perform explicit alpha-conversion. For example, by implementing a conversion: \begin{hol} {\small\verb% RES_FORALL %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%[%}$v${\small\verb%]) ----> !%}$v${\small\verb%. %}$P$ $v${\small\verb% ==> %}$B${\small\verb%[%}$v${\small\verb%]%} \end{hol} \noindent Dealing with the case when $v$ is a variable structure is also desirable. For example: \begin{session}\begin{verbatim} #let t1 = "!(m,n)::P. m (\(m,n). m < n)x) \end{verbatim}\end{session} \noindent If anyone writes the desired conversions please let us know! Here is an example of a user-defined restriction: \begin{session}\begin{verbatim} #new_binder_definition(`DURING`, "DURING(p:num#num->bool) = $!p");; |- !p. $DURING p = $! p #"DURING x::(m,n). p x";; no restriction constant associated with DURING skipping: x " ;; parse failed #new_definition # (`RES_DURING`, "RES_DURING(m,n)p = !x. m<=x /\ x<=n ==> p x");; |- !m n p. RES_DURING(m,n)p = (!x. m <= x /\ x <= n ==> p x) #associate_restriction(`DURING`,`RES_DURING`);; () : void #"DURING x::(m,n). p x";; "DURING x :: (m,n). p x" : term #set_flag(`print_restrict`,false);; true : bool #"DURING x::(m,n). p x";; "RES_DURING(m,n)(\x. p x)" : term \end{verbatim}\end{session} \section{Syntax for sets}\index{set theory notation} The special purpose set-theoretic notations {\small\verb%"{%}$t_1,t_2,\ldots,t_n${\small\verb%}"%} and {\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} are now available. The normal interpretation of the former is the finite set containing $t_1,t_2,\ldots, t_n$ and the normal interpretation of the latter is the set of all $t$s such that $p$. These interpretations are predefined for the library \ml{sets}, but the user can use the syntax for other purposes if he or she wishes using the functions: \begin{holboxed} \index{define_finite_set_syntax@\ml{define\_finite\_set\_syntax}} \index{define_set_abstraction_syntax@\ml{define\_set\_abstraction\_syntax}} \begin{alltt} define_finite_set_syntax : (string # string) -> void define_set_abstraction_syntax : string -> void \end{alltt}\end{holboxed} Executing: \begin{hol}\begin{alltt} define_finite_set_syntax(`\(\con{c}\sb{1}\)`,`\(\con{c}\sb{2}\)`) \end{alltt}\end{hol} \noindent causes {\small\verb%"{%}$t_1,\ldots,t_n${\small\verb%}"%} to parse to: \begin{hol}\begin{alltt} "\(c\sb{2}\) \(t\sb{1}\) (\(c\sb{2}\) \(t\sb{2}\) \(\cdots\) (\(c\sb{2}\) \(t\sb{n}\) \(c\sb{2}\)) \(\cdots\) ))" \end{alltt}\end{hol} \noindent with failure if either $c_1$ or $c_2$ is not the name of a constant. In the library \ml{sets}, the empty set is \ml{EMPTY} and the infixed function \ml{INSERT} adds an element to a set. Executing: \begin{hol}\begin{verbatim} define_finite_set_syntax(`EMPTY`,`INSERT`) \end{verbatim}\end{hol} \noindent will cause \begin{hol}\begin{verbatim} "{1,2,3,4}" \end{verbatim}\end{hol} \noindent to parse to \begin{hol}\begin{verbatim} "1 INSERT (2 INSERT (3 INSERT (4 INSERT EMPTY)))" \end{verbatim}\end{hol} Executing: \begin{hol}\begin{alltt} define_set_abstraction_syntax `\(c\)` \end{alltt}\end{hol} \noindent causes {\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} to parse to: \medskip \noindent{\small {\verb% "%}}$c${\small{\verb%(\(%}$x_1${\verb%,%}$\ldots${\verb%,%}$x_n${\verb%).(%}$t${\verb%,%}$p${\verb%))"%} } \medskip \noindent where $x_1$, $\ldots$ , $x_n$ are the free variables occurring in both $t$ and $p$. If there are no such free variables then an error results. The order in which the variables are listed in the variable structure of the paired abstraction is an unspecified function of the structure of $t$ (it is approximately left to right). Failure if $c$ is not the name of a constant. For example, if the library \ml{sets} (i.e. what used to be \ml{all\_sets}) is loaded, then \begin{hol}\begin{verbatim} define_set_abstraction_syntax `GSPEC` \end{verbatim}\end{hol} \noindent will cause \begin{hol}\begin{verbatim} "{x+y | (x < y) /\ (y < z)}" \end{verbatim}\end{hol} \noindent to parse to: \begin{hol}\begin{verbatim} "GSPEC(\(x,y). ((x+y), (x < y) /\ (y < z)))" \end{verbatim}\end{hol} \noindent where \ml{GSPEC} is defined by: \begin{hol}\begin{verbatim} |- !f. GSPEC f = SPEC(\x. ?y. x,T = f y) \end{verbatim}\end{hol} \noindent and \ml{SPEC} abstracts a predicate to a set (it is the abstraction bijection used in the definition of the type operator \ml{set}). Other examples are: \begin{hol}\begin{verbatim} "{x+y+z | (x < y) /\ (y < z)}" \end{verbatim}\end{hol} \noindent will parse to: \begin{hol}\begin{verbatim} "GSPEC(\(x,y,z). (x+(y+z), (x < y /\ y < z)))" \end{verbatim}\end{hol} \noindent and \begin{hol}\begin{verbatim} "{x+y+w | (x < y) /\ (y < z)}" \end{verbatim}\end{hol} \noindent will parse to: \begin{hol}\begin{verbatim} "GSPEC(\(x,y). (x+(y+w), (x < y /\ y < z)))" \end{verbatim}\end{hol} Note that the precedence of comma is increased in the contexts ``{\small\verb%{%}$\cdots${\small\verb%}%}'' and ``{\small\verb%{%}$\cdots${\small\verb%|%}''. Terms will be printed in set notation if the flag \ml{print\_set} is \ml{true}. Note that \medskip \ml{"}$c${\small\verb%(\(%}$x_1$\ml{,}$\ldots$\ml{,}$x_n$\ml{).(}$t$\ml{,}$p$\ml{))"} \medskip \noindent will only print as {\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} if the variables $x_1$, $\ldots$ , $x_n$ occur free in both $t$ and $p$ (and \ml{print\_set} is \ml{true}) . \section{Revised set theory libraries}\label{LIBRARY} \index{set theory libraries} In previous versions of the system, there were three libraries dealing with elementary set theory: \begin{myenumerate} \item \ml{sets}: a theory of finite sets (Windley and Leveilley); \item \ml{all\_sets}: a theory of infinite and finite sets (Windley and Leveilley); \item \ml{set}: a theory of predicates-as-sets (Kalker). \end{myenumerate} Each of these libraries is useful for certain applications, and all three will therefore continue to be supported. To better reflect the contents of these libraries, they have been renamed as follows: \begin{myenumerate} \item \ml{sets} is now called \ml{finite\_sets}; \item \ml{all\_sets} is now called \ml{sets}; \item \ml{set} is now called \ml{pred\_sets}. \end{myenumerate} The \ml{sets} library (formerly, \ml{all\_sets}) has been extensively revised and extended. The library has been restructured, and several additional built-in theorems are available. Parser and pretty-printer support for the notation: \begin{itemize} \item \ml{\{$x_1,\ldots,x_n$\}} denotes a finite set. \item \ml{\{$x$|$P[x]$\}} denotes the set of all \ml{$x$} such that \ml{$P[x]$}. \item \ml{\{$t[x]$|$P[x]$\}} denotes the set of all \ml{$t[x]$} such that \ml{$P[x]$}. \end{itemize} \noindent is now provided by the parser/pretty-printer extension mentioned above. Proof support is supplied for this notation in the form of a conversion \begin{holboxed}\index{SET_SPEC_CONV@\ml{SET\_SPEC\_CONV}} \begin{verbatim} SET_SPEC_CONV : conv \end{verbatim}\end{holboxed} \noindent which implements the axiom of specification for generalized set specifications. \ml{SET\_SPEC\_CONV} accepts two types of input. \begin{hol} {\small\verb% SET_SPEC_CONV "%}$t${\small\verb% IN {%}$v${\small\verb% | %}$p${\small\verb%[%}$v${\small\verb%]}" %}(where $v$ is a variable) \end{hol} \noindent this returns the theorem: \begin{hol}\begin{alltt} |- \(t\) IN \{\(v\) | \(p[v]\)\} = \(p[t/v]\) \end{alltt}\end{hol} \noindent Furthermore \begin{hol}\begin{alltt} SET_SPEC_CONV "\(t\sb{1}\) IN \{\(t\sb{2}[x\sb{1},\ldots,x\sb{n}]\) | \(p[x\sb{1}\ldots,x\sb{n}]\)\}" \end{alltt}\end{hol} \noindent returns the theorem \medskip {\small \begin{tabular}{ll} {\verb%|-%} & $t_1\ \ml{IN}\ ${\verb%{%}$t_2[x_1,\ldots,x_n]${\verb%|%}$p[x_1,\ldots,x_n]${\verb%}%}\\ & \ml{=}\\ & {\verb%?%}$x_1\cdots x_n${\verb%. (%}$t_1 \ml{=} t_2[x_1,\ldots,x_n]${\verb%) /\ %}$p[x_1,\ldots,x_n]$\\ \end{tabular} } \medskip \begin{hol}\begin{verbatim} |- x IN {n | n < m} = x < m |- 5 IN {x+y | x < 2 /\ y < 3} = ?x y. (5 = x + y) /\ x < 2 /\ y < 3 \end{verbatim}\end{hol} The library \ml{sets} also makes available an induction principle for proving properties of finite sets. \begin{holboxed}\index{SET_INDUCT_TAC@\ml{SET\_INDUCT\_TAC}} \begin{verbatim} SET_INDUCT_TAC : tactic \end{verbatim}\end{holboxed} \begin{hol}\begin{alltt} "!\(s\). FINITE \(s\) ==> \(P\)[\(s\)]" ============================= SET_INDUCT_TAC \(P\)[EMPTY] \(P\)[\(x\) INSERT \(t\)] [ "FINITE \(t\)" ] [ "\(P\)[\(s\)]"] [ "~\(x\) IN \(t\)"] \end{alltt}\end{hol} \noindent The file {\small\verb%Libaries/sets/COMPAT.READ.ME%} provides an index to theorem names in the new library and other compatibility information. This is intended to help users update proof scripts based on the old version of the \ml{all\_sets} library. \section{Syntax blocks} \index{syntax blocks|(} A syntax block starts with a keyword and ends with a terminator and is associated with a function on strings. When such a block is encountered in the input stream, all the characters between the start keyword and the terminator are made into a string to which the associated function is applied. Syntax blocks can be used with the parser generator library {\small\verb%parser%} to parse user-specified languages into \HOL\ terms. See the documentation of the library for details and examples. The ML function: \begin{holboxed}\index{new_syntax_block@\ml{new\_syntax\_block}} \begin{verbatim} new_syntax_block : string # string # string -> void \end{verbatim}\end{holboxed} \noindent declares a new syntax block. The first argument is the start keyword of the block, the second argument is the terminator and the third argument is the name of a function having a type which is an instance of {\small\verb%string->*%}. The effect of \begin{hol} \ml{ new\_syntax\_block(`XXX`, `YYY`, `}$f$\ml{`);;} \end{hol} \noindent is that if subsequently \begin{hol}\begin{verbatim} XXX ... YYY \end{verbatim}\end{hol} \noindent occurs in the input, then it is as though \begin{hol} \ml{ }$f$\ml{ ` ... `} \end{hol} \noindent were input instead. For example: \setcounter{sessioncount}{1} \begin{session}\begin{verbatim} #let foo s = print_string `Hello: `; print_string s; print_newline();; foo = - : (string -> void) #new_syntax_block(`<<`,`>>`, `foo`);; () : void #<< Mike >>;; Hello: Mike () : void \end{verbatim}\end{session} The following function is useful with syntax blocks, because it enables backslash ({\small\verb%\%}) to be included in strings. \begin{holboxed}\index{set_string_escape@\ml{set\_string\_escape}} \begin{verbatim} set_string_escape : int -> int \end{verbatim}\end{holboxed} \noindent This changes the escape character in strings to be the character with the supplied ascii code (initially this is {\small\verb%92%}, viz. `{\small\verb%\%}`). The old escape character is returned.\index{syntax blocks|)} \section{User-programmable quotation typechecker} The typechecker for \HOL\ quotations contains a number of arbitrary design decisions. Several people have suggested changes, e.g. that full Hindley/Milner type inference be performed. Rather than try to create a single new improved typechecker, a facility is now provided that enables the user to write his or her own one and then to install it in the system. \index{preterms|(} The \ML\ abstract type {\small\verb%preterm%} represents the parse trees of \HOL\ terms. A typechecker is a function of type {\small\verb%preterm->term%}. If the flag \ml{preterm} is set to \ml{true} (the default is \ml{false}), then \HOL\ will use whatever \ML\ function is currently bound to the name \ml{preterm\_handler} as the quotation typechecker. The way this works is that when \ml{preterm} is true the parser produces a preterm rather than a term, and then wraps a call of \ml{preterm\_handler} around the quotation.\index{type checking, in HOL logic@type checking, in \HOL\ logic!user programmed} Other uses of preterms are possible, for example as patterns for describing terms. The definition of the \ML\ type {\small\verb%preterm%} is: \begin{hol}\index{preterm@\ml{preterm}}\begin{alltt} rectype preterm = preterm_var of string \({\it Variables}\) | preterm_const of string \({\it Constants}\) | preterm_comb of preterm # preterm \({\it Combinations}\) | preterm_abs of preterm # preterm \({\it Abstractions}\) | preterm_typed of preterm # type \({\it Explicit typing}\) | preterm_antiquot of term \({\it Antiquotation}\) \end{alltt}\end{hol} The function: \begin{holboxed}\index{preterm_to_term@\ml{preterm\_to\_term}} \begin{verbatim} preterm_to_term : preterm -> term \end{verbatim}\end{holboxed} \noindent invokes the standard \HOL\ typechecker on a preterm and returns the resulting typechecked term (or causes the standard error message).\index{preterms|)} The following is a rather contrived example: \setcounter{sessioncount}{1} \begin{session}\index{preterm_handler@\ml{preterm\_handler}} \begin{verbatim} #letref p_reg = preterm_var `x`;; p_reg = preterm_var `x` : preterm #let preterm_handler p = p_reg:=p; print_string `Typechecking ... `; print_newline(); preterm_to_term p;; preterm_handler = - : (preterm -> term) \end{verbatim}\end{session} \begin{session} \begin{verbatim} #set_flag(`preterm`,true);; false : bool #"x+y";; Typechecking ... "x + y" : term #p_reg;; preterm_comb((preterm_comb((preterm_const `+`), preterm_var `x`)), preterm_var `y`) : preterm \end{verbatim}\end{session} \noindent Different top-level typechecking can be defined by using a different definition of the function \ml{preterm\_handler}. Note that typechecking is purely a `user interface' feature, so changing the typechecker does not compromise the logical soundness of \HOL. \section{New conversions}\label{CONVERSIONS} Many new conversions have been added to the system. Only those likely to be of general interest are listed here. \subsection{Generalized beta-reduction} A new conversion: \begin{holboxed}\index{PAIRED_BETA_CONV@\ml{PAIRED\_BETA\_CONV}} \begin{verbatim} PAIRED_BETA_CONV : conv \end{verbatim}\end{holboxed} \noindent has been added to do generalized beta-conversion of tupled lambda abstractions applied to tuples. Given the term: \begin{hol} {\small\verb% "(\(%}$x_1, \ldots ,x_n${\small\verb%).%}$t${\small\verb%) (%}$t_1, \ldots ,t_n${\small\verb%)"%} \end{hol} \noindent \ml{PAIRED\_BETA\_CONV} proves that: \begin{hol} {\small\verb% |- (\(%}$x_1, \ldots ,x_n${\small\verb%). %}$t${\small\verb%[%}$x_1,\ldots,x_n${\small\verb%]) (%}$t_1, \ldots ,t_n${\small\verb%) = %}$t${\small\verb%[%}$t_1, \ldots ,t_n${\small\verb%]%} \end{hol} The conversion works for arbitrarily nested tuples. For example: \setcounter{sessioncount}{1} \begin{session}\begin{verbatim} #PAIRED_BETA_CONV "(\((a,b),(c,d)). [a;b;c;d]) ((1,2),(3,4))";; |- (\((a,b),c,d). [a;b;c;d])((1,2),3,4) = [1;2;3;4] \end{verbatim}\end{session} \subsection{Arithmetical conversions} The conversion: \begin{holboxed}\index{ADD_CONV@\ml{ADD\_CONV}} \begin{verbatim} ADD_CONV : conv \end{verbatim}\end{holboxed} \noindent does addition by formal proof. If $n$ and $m$ are numerals then {\small\verb%ADD_CONV "%}$n\ $\ml{+}$\ m$\ml{"} returns the theorem {\small\verb%|- %}$n\ $\ml{+}$\ m\ $\ml{=}$\ s$, where $s$ is the numeral denoting the sum of $n$ and $m$. For example: \setcounter{sessioncount}{1} \begin{session}\begin{verbatim} #ADD_CONV "1 + 2";; |- 1 + 2 = 3 #ADD_CONV "0 + 1000";; |- 0 + 1000 = 1000 #ADD_CONV "101 + 102";; |- 101 + 102 = 203 \end{verbatim}\end{session} A new conversion has been added for deciding equality of natural number constants. \begin{holboxed}\index{num_EQ_CONV@\ml{num\_EQ\_CONV}} \begin{verbatim} num_EQ_CONV : conv \end{verbatim}\end{holboxed} \noindent If $n$ and $m$ are terms constructed from numeral constants and the successor function \ml{SUC}, then: {\small\verb%num_EQ_CONV "%}$n$\ml{=}$m$\ml{"} returns: \begin{hol} \ml{ |- (\(n\)=\(m\)) = T }if \(n\) and \(m\) represent the same number,\\ \ml{ |- (\(n\)=\(m\)) = F }if \(n\) and \(m\) represent different numbers. \end{hol} \noindent In addition, {\small\verb%num_EQ_CONV "%}$t\ $\ml{=}$\ t$\ml{"} returns: {\small\verb%|- (%}$t$\ml{=}$t${\small\verb%) = T%} \subsection{List processing conversions} Two new conversions for lists are now built-in: \begin{holboxed} \index{LENGTH_CONV@\ml{LENGTH\_CONV}} \index{list_EQ_CONV@\ml{list\_EQ\_CONV}} \begin{verbatim} LENGTH_CONV : conv list_EQ_CONV: conv \end{verbatim}\end{holboxed} \ml{LENGTH\_CONV}: computes the length of a list. A call to: \begin{hol}\begin{alltt} LENGTH_CONV "LENGTH[\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)]" \end{alltt}\end{hol} \noindent generates the theorem: \begin{hol}\begin{alltt} |- LENGTH [\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)] = n \end{alltt}\end{hol} The other conversion, \ml{list\_EQ\_CONV}, proves or disproves the equality of two lists, given a conversion for deciding the equality of elements. A call to: \begin{hol}\begin{alltt} list_EQ_CONV \(conv\) "[\(u\sb{1}\);\(\ldots\);\(u\sb{n}\)] = [\(v\sb{1}\);\(\ldots\);\(v\sb{m}\)]" \end{alltt}\end{hol} \noindent returns: {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ F} if: \begin{myenumerate} \item \ml{~($n$=$m$)} or \item \ml{$conv$} proves {\small\verb%|- (%}$u_i\ $\ml{=}$\ v_i$\ml{)\ =\ F} for any $1\leq i \leq m$. \end{myenumerate} \noindent {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ T} is returned if: \begin{myenumerate} \item \ml{($n$=$m$)} and \ml{$u_i$} is syntactically identical to \ml{$v_i$} for $1\leq i \leq m$, or \item \ml{($n$=$m$)} and \ml{$conv$} proves {\small\verb%|- (%}$u_i$\ml{=}$v_i$\ml{)=T} for $1\leq i \leq n$. \end{myenumerate} \subsection{Simplifying {\tt let}-terms} \index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!simplification of} A conversion for reducing {\tt let}-terms is now provided. \begin{holboxed}\index{let_CONV@\ml{let\_CONV}} \begin{verbatim} let_CONV : conv \end{verbatim}\end{holboxed} \noindent Given a term: \begin{hol}\begin{alltt} "let \(v\sb{1}\) = \(t\sb{1}\) and \(\cdots\) and \(v\sb{n}\) = \(t\sb{n}\) in \(t[v\sb{1},\ldots,v\sb{n}]\)" \end{alltt}\end{hol} \noindent \ml{let\_CONV} proves that: \begin{hol}\begin{alltt} |- let \(v\sb{1}\) = \(t\sb{1}\) and \(\cdots\) and \(v\sb{n}\) = \(t\sb{n}\) in \(t[v\sb{1},\ldots,v\sb{n}]\) = \(t[t\sb{1},\ldots,t\sb{n}]\) \end{alltt}\end{hol} \noindent The \ml{$v_i$}'s can take any one of the following forms: \begin{myenumerate} \item Variables: \ml{x} etc. \item Tuples: \ml{(x,y)}, \ml{(a,b,c)}, \ml{((a,b),(c,d))} etc. \item Applications: \ml{f (x,y) z}, \ml{f x} etc. \end{myenumerate} \noindent Variables are just substituted for. With tuples, the substitution is done component-wise, and function applications are effectively rewritten in the body of the {\tt let}-term. \setcounter{sessioncount}{1} \begin{session}\begin{verbatim} #let_CONV "let x = 1 in x+y";; |- (let x = 1 in x + y) = 1 + y #let_CONV "let (x,y) = (1,2) in x+y";; |- (let (x,y) = 1,2 in x + y) = 1 + 2 #let_CONV "let f x = 1 and f y = 2 in (f 10) + (f 20)";; |- (let f x = 1 and f y = 2 in (f 10) + (f 20)) = 2 + 2 #let_CONV "let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))";; |- (let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))) = (((0 + 2) + 1) + 2) + 1 #CONV_RULE(DEPTH_CONV ADD_CONV)it;; |- (let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))) = 6 #let_CONV "let f x y = x+y in f 1";; % NB: partial application % |- (let f x y = x + y in f 1) = (\y. 1 + y) \end{verbatim}\end{session} \subsection{Skolemization}\index{Skolemization} Two conversions are provided for a higher-order version of Skolemization (using existentially quantified function variables rather than first-order Skolem constants). The conversion \begin{holboxed}\index{X_SKOLEM_CONV@\ml{X\_SKOLEM\_CONV}} \begin{verbatim} X_SKOLEM_CONV : term -> conv \end{verbatim}\end{holboxed} \noindent takes a variable parameter, \ml{$f$} say, and proves: \begin{hol}\begin{alltt} |- (!\(x\sb{1}\) \(\ldots\) \(x\sb{n}\). ?\(y\). \(t[x\sb{1},\ldots,x\sb{n},y]\) = (?\(f\). !\(x\sb{1}\) \(\ldots\) \(x\sb{n}\). \(t[x\sb{1},\ldots,x\sb{n},f x\sb{1}\ldots x\sb{n}]\) \end{alltt}\end{hol} \noindent for any input term \ml{!$x_1\ \ldots\ x_n$.\ ?$y$. $t[x_1,\ldots,x_n,y]$}. Note that when $n=\ml{0}$, this is equivalent to alpha-conversion: \begin{hol}\begin{alltt} |- (?\(y\). \(t[y]\)) = (?\(f\). \(t[f]\)) \end{alltt}\end{hol} \noindent and that the conversion fails if there is already a free variable \ml{$f$} of the appropriate type in the input term. For example: \begin{hol}\begin{alltt} X_SKOLEM_CONV "f:num->*" "!n:num. ?x:*. x = (f n)" \end{alltt}\end{hol} \noindent will fail. The conversion \ml{SKOLEM\_CONV} is like \ml{X\_SKOLEM\_CONV}, except that it uses a primed variant of the name of the existentially quantified variable as the name of the skolem function it introduces. For example: \begin{hol}\begin{alltt} SKOLEM_CONV "!x. ?y. P x y" \end{alltt}\end{hol} \noindent proves that: \begin{hol}\begin{alltt} |- ?y. !x. P x (y x) \end{alltt}\end{hol} \subsection{Quantifier movement conversions} \index{quantifiers!conversions for} \index{conversions!quantifier movement} A complete and systematically-named set of conversions for moving quantifiers inwards and outwards through the logical connectives {\small\verb%~%}, {\small\verb%/\%}, {\small\verb%\/%}, and {\small\verb%==>%} has been added to the system. The naming scheme is based on the following atoms: \begin{hol}\begin{alltt} <\(quant\)> := FORALL | EXISTS <\(conn\)> := NOT | AND | OR | IMP [\(dir\)] := LEFT | RIGHT \({\it (optional)}\) \end{alltt}\end{hol} The conversions for moving quantifiers inwards are called: \begin{hol}\begin{alltt} <\(quant\)>_<\(conn\)>_CONV \end{alltt}\end{hol} \noindent where the quantifier \ml{<$quant$>} is to be moved inwards through \ml{<$conn$>}. The conversions for moving quantifiers outwards are called: \begin{hol}\begin{alltt} [\(dir\)]_<\(conn\)>_<\(quant\)>_CONV \end{alltt}\end{hol} \noindent where \ml{<$quant$>} is to be moved outwards through \ml{<$conn$>}, and the optional \ml{[$dir$]} identifies which operand (left or right) contains the quantifier. The complete set is: \begin{hol}\begin{verbatim} NOT_FORALL_CONV |- ~(!x.P) = ?x.~P NOT_EXISTS_CONV |- ~(?x.P) = !x.~P EXISTS_NOT_CONV |- (?x.~P) = ~!x.P FORALL_NOT_CONV |- (!x.~P) = ~?x.P \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} FORALL_AND_CONV |- (!x. P /\ Q) = (!x.P) /\ (!x.Q) AND_FORALL_CONV |- (!x.P) /\ (!x.Q) = (!x. P /\ Q) LEFT_AND_FORALL_CONV |- (!x.P) /\ Q = (!x'. P[x'/x] /\ Q) RIGHT_AND_FORALL_CONV |- P /\ (!x.Q) = (!x'. P /\ Q[x'/x]) \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} EXISTS_OR_CONV |- (?x. P \/ Q) = (?x.P) \/ (?x.Q) OR_EXISTS_CONV |- (?x.P) \/ (?x.Q) = (?x. P \/ Q) LEFT_OR_EXISTS_CONV |- (?x.P) \/ Q = (?x'. P[x'/x] \/ Q) RIGHT_OR_EXISTS_CONV |- P \/ (?x.Q) = (?x'. P \/ Q[x'/x]) \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} FORALL_OR_CONV |- (!x.P \/ Q) = P \/ !x.Q [x not free in P] |- (!x.P \/ Q) = (!x.P) \/ Q [x not free in Q] |- (!x.P \/ Q) = (!x.P) \/ (!x.Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} OR_FORALL_CONV |- (!x.P) \/ (!x.Q) = (!x.P \/ Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} LEFT_OR_FORALL_CONV |- (!x.P) \/ Q = !x'. P[x'/x] \/ Q RIGHT_OR_FORALL_CONV |- P \/ (!x.Q) = !x'. P \/ Q[x'/x] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} EXISTS_AND_CONV |- (?x.P /\ Q) = P /\ ?x.Q [x not free in P] |- (?x.P /\ Q) = (?x.P) /\ Q [x not free in Q] |- (?x.P /\ Q) = (?x.P) /\ (?x.Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} AND_EXISTS_CONV |- (?x.P) /\ (?x.Q) = (?x.P /\ Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} LEFT_AND_EXISTS_CONV |- (?x.P) /\ Q = ?x'. P[x'/x] /\ Q RIGHT_AND_EXISTS_CONV |- P /\ (?x.Q) = ?x'. P /\ Q[x'/x] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} FORALL_IMP_CONV |- (!x.P ==> Q) = P ==> !x.Q [x not free in P] |- (!x.P ==> Q) = (?x.P) ==> Q [x not free in Q] |- (!x.P ==> Q) = (?x.P) ==> (!x.Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} LEFT_IMP_FORALL_CONV |- (!x.P) ==> Q = !x'. P[x/'x] ==> Q RIGHT_IMP_FORALL_CONV |- P ==> (!x.Q) = !x'. P ==> Q[x'/x] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} EXISTS_IMP_CONV |- (?x.P ==> Q) = P ==> ?x.Q [x not free in P] |- (?x.P ==> Q) = (!x.P) ==> Q [x not free in Q] |- (?x.P ==> Q) = (!x.P) ==> (?x.Q) [x not free in P or Q] \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} LEFT_IMP_EXISTS_CONV |- (?x.P) ==> Q = !x'. P[x/'x] ==> Q RIGHT_IMP_EXISTS_CONV |- P ==> (?x.Q) = ?x'. P ==> Q[x'/x] \end{verbatim}\end{hol} \section{New built-in theorems}\label{THEOREMS} Quite a few new theorems have been added to \HOL. Some are listed below, others can be found in the libraries and in \ml{contrib}. \subsection{New arithmetical theorems} The built-in theory arithmetic has been augmented with a minimal theory of the functions \ml{MOD} and \ml{DIV} on the natural numbers. The old definitions of \ml{MOD} and \ml{DIV}: \begin{hol}\begin{verbatim} MOD |- MOD k n = @r. ?q. (k = (q * n) + r) /\ r < n DIV |- DIV k n = @q. (k = (q * n) + (k MOD n)) \end{verbatim}\end{hol} \noindent have been deleted, and replaced by the constant specification: \begin{hol}\begin{verbatim} DIVISION |- !n. 0 < n ==> (!k. (k = ((k DIV n) * n) + (k MOD n)) /\ (k MOD n) < n) \end{verbatim}\end{hol} \noindent the validity of which is justified by the division algorithm: \begin{hol}\begin{verbatim} DA |- !k n. 0 < n ==> (?r q. (k = (q * n) + r) /\ r < n) \end{verbatim}\end{hol} The following theorems are also available: \begin{hol}\begin{verbatim} MOD_ONE |- !k. k MOD (SUC 0) = 0 DIV_LESS_EQ |- !n. 0 < n ==> (!k. (k DIV n) <= k) DIV_UNIQUE |- !n k q. (?r. (k = (q * n) + r) /\ r < n) ==> (k DIV n = q) MOD_UNIQUE |- !n k r. (?q. (k = (q * n) + r) /\ r < n) ==> (k MOD n = r) DIV_MULT |- !n r. r < n ==> (!q. ((q * n) + r) DIV n = q) LESS_MOD |- !n k. k < n ==> (k MOD n = k) MOD_EQ_0 |- !n. 0 < n ==> (!k. (k * n) MOD n = 0) ZERO_MOD |- !n. 0 < n ==> (0 MOD n = 0) MOD_MULT |- !n r. r < n ==> (!q. ((q * n) + r) MOD n = r) MOD_TIMES |- !n. 0 < n ==> (!q r. ((q * n) + r) MOD n = r MOD n) MOD_PLUS |- !n. 0 < n ==> (!j k. ((j MOD n) + (k MOD n)) MOD n = (j + k) MOD n) MOD_MOD |- !n. 0 < n ==> (!k. (k MOD n) MOD n = k MOD n) \end{verbatim}\end{hol} The following miscellaneous arithmetical theorems are now pre-proved. \begin{hol}\begin{verbatim} ZERO_LESS_EQ |- !n. 0 <= n LESS_EQ_MONO |- !n m. (SUC n <= SUC m) = (n <= m) LESS_OR_EQ_ADD |- !n m. n < m \/ ?p. n = p+m SUC_NOT |- !n. ~(0 = SUC n) SUB_MONO_EQ |- !n m. (SUC n) - (SUC m) = n - m SUB_PLUS |- !a b c. a - (b + c) = (a - b) - c INV_PRE_LESS |- !m n. 0 < m /\ 0 < n ==> ((PRE m)<(PRE n) = m !m. ((PRE m)<=(PRE n) = m<=n) SUB_LESS_EQ |- !n m. (n - m) <= n SUB_EQ_EQ_0 |- !m n. (m - n = m) = (m = 0) \/ (n = 0) SUB_LESS_0 |- !n m. m < n = 0 < (n - m) SUB_LESS_OR |- !m n. n < m ==> n <= (m - 1) LESS_SUB_ADD_LESS |- !n m i. i < (n - m) ==> (i + m) < n TIMES2 |- !n. 2 * n = n + n LESS_MULT_MONO |- !m i n. ((SUC n) * m) < ((SUC n) * i) = m < i MULT_MONO_EQ |- !m i n. ((SUC n) * m = (SUC n) * i) = (m = i) ADD_SUB |- !a c. (a + c) - c = a LESS_EQ_ADD_SUB |- !c b. c <= b ==> (!a. (a + b) - c = a + (b - c)) SUB_EQUAL_0 |- !c. c - c = 0 LESS_EQ_SUB_LESS |- !a b. b <= a ==> (!c. (a - b) < c = a < (b + c)) NOT_SUC_LESS_EQ |- !n m. ~(SUC n) <= m = m <= n SUB_SUB |- !b c. c <= b ==> (!a. a - (b - c) = (a + c) - b) LESS_IMP_LESS_ADD |- !n m. n < m ==> (!p. n < (m + p)) LESS_EQ_IMP_LESS_SUC |- !n m. n <= m ==> n < (SUC m) \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} SUB_LESS_EQ_ADD |- !m p. m <= p ==> (!n. (p - m) <= n = p <= (m + n)) SUB_CANCEL |- !p n m. n <= p /\ m <= p ==> ((p - n = p - m) = (n = m)) CANCEL_SUB |- !p n m. p <= n /\ p <= m ==> ((n - p = m - p) = (n = m)) NOT_EXP_0 |- !m n. ~((SUC n) EXP m = 0) ZERO_LESS_EXP |- !m n. 0 < ((SUC n) EXP m) ODD_OR_EVEN |- !n. ?m. (n = (SUC(SUC 0)) * m) \/ (n = ((SUC(SUC 0)) * m) + 1) LESS_EXP_SUC_MONO |- !n m. ((SUC(SUC m)) EXP n)<((SUC(SUC m)) EXP (SUC n)) LESS_EQUAL_ANTISYM |- !n m. n <= m /\ m <= n ==> (n = m) LESS_ADD_SUC |- !m n. m < (m + (SUC n)) \end{verbatim}\end{hol} \subsection{New theorems about lists} \begin{hol}\begin{verbatim} LIST_NOT_EQ: |- !l1 l2. ~(l1 = l2) ==> (!h1 h2. ~(CONS h1 l1 = CONS h2 l2)) NOT_EQ_LIST: |- !h1 h2. ~(h1 = h2) ==> (!l1 l2. ~(CONS h1 l1 = CONS h2 l2)) EQ_LIST |- !h1 h2. (h1 = h2) ==> (!l1 l2. (l1 = l2) ==> (CONS h1 l1 = CONS h2 l2)) \end{verbatim}\end{hol} \subsection{New propositional theorems} \begin{hol}\begin{verbatim} LEFT_AND_OVER_OR |- !t1 t2 t3. t1 /\ (t2 \/ t3) = t1 /\ t2 \/ t1 /\ t3 RIGHT_AND_OVER_OR |- !t1 t2 t3. (t2 \/ t3) /\ t1 = t2 /\ t1 \/ t3 /\ t1 LEFT_OR_OVER_AND |- !t1 t2 t3. t1 \/ t2 /\ t3 = (t1 \/ t2) /\ (t1 \/ t3) RIGHT_OR_OVER_AND |- !t1 t2 t3. t2 /\ t3 \/ t1 = (t2 \/ t1) /\ (t3 \/ t1) \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} OR_IMP_THM |- !t1 t2. (t1 = t2 \/ t1) = t2 ==> t1 NOT_IMP |- !t1 t2. ~(t1 ==> t2) = t1 /\ ~t2 COND_ID |- !b t. (b => t | t) = t DISJ_ASSOC |- !t1 t2 t3. t1 \/ t2 \/ t3 = (t1 \/ t2) \/ t3 \end{verbatim}\end{hol} \section{Additions and deletions}\label{adddel} The \ML\ identifiers that have been added and deleted in Version 2.0 are listed here. The reasons for the changes are given in the files: \begin{hol}\begin{verbatim} hol/Version.2.0 hol/Versions/Version.1.12 hol/Versions/Versions.pre.1.12 \end{verbatim}\end{hol} \noindent The file \ml{Version.$m$.$n$} (in the sources) documents \HOL\ Version \ml{$m$.$n$} and may contain details not in \DESCRIPTION\ or \REFERENCE. \subsection{Additions} Here is a list of all the new functions in Version 2.0, the ones that are not described in this appendix or earlier in \DESCRIPTION\ should be documented in \REFERENCE. \begin{hol}\begin{verbatim} get_const_type parity is_type mk_let dest_let is_let bndvar body is_axiom \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} mk_cons dest_cons is_cons mk_list dest_list is_list list_mk_pair strip_mk_pair \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} ancestors ancestry \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} prove_rep_fn_one_one prove_rep_fn_onto prove_abs_fn_one_one prove_abs_fn_onto \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} define_finite_set_syntax define_set_abstraction_syntax associate_restriction \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} X_FUN_EQ_CONV COND_CONV PAIRED_BETA_CONV BOOL_EQ_CONV ADD_CONV LENGTH_CONV list_EQ_CONV num_EQ_CONV let_CONV EXISTS_LEAST_CONV X_SKOLEM_CONV SKOLEM_CONV NOT_FORALL_CONV NOT_EXISTS_CONV EXISTS_NOT_CONV FORALL_NOT_CONV FORALL_AND_CONV AND_FORALL_CONV LEFT_AND_FORALL_CONV RIGHT_AND_FORALL_CONV EXISTS_OR_CONV OR_EXISTS_CONV LEFT_OR_EXISTS_CONV RIGHT_OR_EXISTS_CONV FORALL_OR_CONV OR_FORALL_CONV LEFT_OR_FORALL_CONV RIGHT_OR_FORALL_CONV EXISTS_AND_CONV AND_EXISTS_CONV LEFT_AND_EXISTS_CONV RIGHT_AND_EXISTS_CONV FORALL_IMP_CONV EXISTS_IMP_CONV LEFT_IMP_FORALL_CONV RIGHT_IMP_FORALL_CONV LEFT_IMP_EXISTS_CONV RIGHT_IMP_EXISTS_CONV \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} last butlast \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} getenv library_pathname is_ml_infix set_help_search_path help_search_path \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} EQF_INTRO ISPEC ISPECL EQF_ELIM EXISTENCE IMP_CONJ EXIST_IMP \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} REPEAT_GTCL AP_THM_TAC \end{verbatim}\end{hol} \subsection{Deletions} The large number of deletions listed below are mostly the result of a ``spring cleaning'' of the \HOL\ sources. It is hoped that nothing in use has been deleted by mistake---please let us know if you want anything back. \begin{hol}\begin{verbatim} abbrev_ty_def EXPAND_TY_DEFINITION pp_constants pp_axioms pp_theorem pp_delete_theorem pp_theorems new_pp_theory close_pp_theory load_pp_theory extend_pp_theory new_pp_predicate mk_quant mk_bool_comb space ascii_ize dest_quant dest_bool_comb truth mk_iff dest_iff is_iff \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} TOTALLY_AD_HOC_LEMMA \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} AND_CLAUSE1 AND_CLAUSE2 AND_CLAUSE3 AND_CLAUSE4 AND_CLAUSE5 OR_CLAUSE1 OR_CLAUSE2 OR_CLAUSE3 OR_CLAUSE4 OR_CLAUSE5 IMP_CLAUSE1 IMP_CLAUSE2 IMP_CLAUSE3 IMP_CLAUSE4 IMP_CLAUSE5 EQ_CLAUSE1 EQ_CLAUSE2 EQ_CLAUSE3 EQ_CLAUSE4 COND_CLAUSE1 COND_CLAUSE2 \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} paired_mem paired_tryfind paired_aconv_term paired_map paired_filter paired_subst_term paired_forall paired_mapfilter paired_subst_occs_term paired_exists paired_rev_itlist paired_term_freein_term paired_find paired_term_match paired_type_in_term paired_type_in_type paired_set_left paired_axiom paired_inst_type paired_set_right paired_inst_term paired_cons paired_variant paired_eq paired_form_match paired_aconv_form paired_subst_form paired_subst_occs_form paired_term_freein_form paired_term_freein_form paired_type_in_form paired_inst_form \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} new_curried_infix curried_infixes paired_infixes \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} rename_form rename_term print_form mk_inequiv dest_inequiv is_inequiv is_equiv dest_equiv mk_equiv gen_all new_predicate make_tuple list_variant nil diagonal eqfst eqsnd flip mk_tuple dest_tuple \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} OLD_IMP_RES_TAC HOL_IMP_RES_THEN HOL_STRIP_THM_THEN OLD_RES_TAC HOL_RES_THEN HOL_STRIP_ASSUME_TAC OLD_IMP_RES_THEN RES_CANON_FUN HOL_MATCH_MP OLD_RES_THEN MULTI_MP HOL_RESOLVE_THEN MP_CHAIN REDEPTH_CHAIN SUB_CHAIN ONCE_DEPTH_CHAIN DSPEC DSPECL \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} print_tok_ty print_tok_thm apply_type_op print_all_tok_thm int_of_tok (replaced by int_of_string) tok_of_int (replaced by string_of_int) int_to_term term_to_int form_class form_frees form_vars form_tyvars term_frees (equivalent to frees) term_vars (equivalent to vars) term_tyvars (equivalent to tyvars) term_class \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} seg (now in library `eval`) word_seg (now in library `eval`) word_el (now in library `eval`) truncate (now in library `eval`) upto keyword \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} LESS_OR (replaced by LESS_SUC_EQ) GSUBS \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} DEPTH_EXISTS_CONV DISJS_CONV BINOP_CONV ANTE_FORALL_CONV BOOL_EQ_CONV (renamed bool_EQ_CONV) MOVE_EXISTS_OUT_CONV (replaced by RIGHT_AND_EXISTS_CONV) \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} is_string is_int is_cons obj_of_string obj_of_int cons string_of_obj int_of_obj left right set_left set_right eq lisp_eval make_set (renamed to setify) thenf orelsef all_fun no_fun first_fun every_fun repeatf mapshape \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} BETA_RED_CONV LENGTH_MAP_CONV make_definitions BINDER_CONV LEN_SIMP_CONV mk_def CHOOSE_RULE LHS_CONV mk_defs COND_F MAP_ELIM mk_fn_ty COND_T MOVE_FORALL_IN mk_fun_test CONJS_CONV OR_ELIM_CONV mk_funct DEPTH_FORALL_CONV OR_IMP mk_injs DO_ASM PROJ mk_new_vars ELIM_ANTE_EQNS_CONV RM_LEN_CONV mk_subset_pred ELIM_ANTE_EQN_CONV SIMP_CONV mk_sum_ty ELIM_LEN_CONV SIMP_ISL1 mk_test ELIM_MAP_CONV SIMP_ISL2 mk_tl_spec EQ_ANTE_ELIM SIMP_RHS mk_tuple_ty EXISTS_RULE TEST_CONV pars_ty \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} E_I_CONV clean parse_type FN_BETA cleanup proj FN_CASES_SIMP do_abs prove_existence_thm FN_CASE_SIMP extract_list strip_cases FORALL_AND_CONV extract_tuple strip_tok FORALL_CONJ_CONV gen_names strip_val FOUR_BINDER_CONV infix_ty strip_vty_tok FST_SND_SIMP is_char sub_conv HD_TL_SIMP list_gen_alpha ty_case variant_tyvar rotate_left rotate_right derive_existence_thm instantiate_existence_thm mk_fn closeup \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} CLOSE_UP save_open_thm HOLdir set_hol_lib_dir load_from_lib loadt_from_lib loadf_from_lib loadx theories_dir_pathname \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} IFF_DEF I FF_EQ_THM1 IFF_EQ_THM2 IFF_EQ IFF_EQ_RULE CONJ_IFF IFF_CONJ IFF_THEN2 IFF_THEN IFF_TAC EXISTS_REFL_TAC \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} define_new_type_isomorphisms (renamed define_new_type_bijections) \end{verbatim}\end{hol} \begin{hol}\begin{verbatim} mk_rewrites mk_rewritesl REWRITE_CONV \end{verbatim}\end{hol}