1 2\appendix 3 4\chapter{Version 2.0}\label{appendix} 5 6This appendix summarizes the differences between \HOL 88 Version 2.0 7and the last major release, which was Version 1.11 (Version 1.12 is 8essentially the Version 2.0 system with the Version 1.10 9documentation). 10 11 12Version 2.0 is primarily a rationalization of Version 1.11. Relics of 13\LCF\ have been deleted and many `internal' \ML\ bindings have been 14made local to the functions that use them. It is hoped that nothing 15useful has been inadvertently removed. 16 17The top-level directory of the \HOL\ distribution sources has been 18reorganized. The details are in Chapter 1 of \TUTORIAL\ (`Getting and 19Installing \HOL'). An important addition is a directory 20{\small\verb%contrib%} containing contributions from the \HOL\ user 21community. The aim of this directory is to make it easy for the 22community to share theories, proofs, examples, tools, documents, and 23other material which may be of general interest. Unlike the library, 24there is no quality control on {\small\verb%contrib%}. 25 26Two major revisions of the theorem-proving tools in Version 2.0 are the 27complete reimplementations, by Tom Melham, of (i) the resolution rules and 28tactics and (ii) the type definition package. 29 30 31The resolution tools have been rewritten so that they are more 32systematic and predictable. Unfortunately, this means that sometimes 33different results are produced, and so code using 34{\small\verb%RES_TAC%}, {\small\verb%IMP_RES_TAC%} \etc\ may need to 35be modified to run in Version 2.0. This is particularly likely if 36tactics have been used that depend on the positions of assumptions in 37goals (this is generally considered `bad style'). The old 38resolution tools are available in the directory 39{\small\verb%contrib/resolve%}. 40 41The type definition package (i.e.\ the \ML\ function 42{\small\verb%define_type%}) has been rewritten to be faster and more 43robust. A number of identifier names have changed and its internal 44workings have been reorganized. A tool for mutually recursive type 45definitions is available in {\small\verb%contrib/mut_rec_types%} (it 46was produced by students at Aarhus University). 47 48Four libraries from Version 1.11 of HOL have been temporarily withdrawn, 49because the Cambridge group have been unable to rebuild them in Version 2.0. 50These are: 51 52\begin{hol}\begin{verbatim} 53 card well_order zet csp 54\end{verbatim}\end{hol} 55 56\noindent The first three are difficult to rebuild because of changes to 57resolution. They rely very heavily on the order in which the 58assumptions of goals appear. The fourth library uses the 59{\small\verb%set%} library, which has been substantially modified. 60These four libraries have been moved to 61{\small\verb%contrib%} until they are updated by their authors. 62 63 64Version 2.0 provides parser and pretty-printer support for restricted 65quantification and set-theoretic notation. 66 67 68The restricted quantification notation allows terms of 69the form 70\con{Q}$x${\small\verb%::%}$p${\small\verb%.%}$t[x]$, where 71\con{Q} is a quantifier and 72if $x:\alpha$ then $p$ can be any term of type $\alpha\fun\bool$; this 73denotes the quantification of $x$ over those values 74satisfying $p$. The qualifier {\small\verb%::%} can be used with 75{\small\verb%\%} and any 76binder, including user defined ones; the appropriate meanings are 77predefined for {\small\verb%\%} and the built-in binders 78{\small\verb%!%}, {\small\verb%?%} and {\small\verb%@%}. This provides a method of 79simulating subtypes and dependent types; the qualifying predicate $p$ can be 80an arbitrary term containing parameters. For example: 81{\small\verb%!%}$w${\small\verb%::%}$\con{Word}(n)${\small\verb%. %}$t[w]$, 82for a suitable constant \con{Word}, simulates a quantification over the 83`type' of $n$-bit words. Experiments are needed to establish how satisfactory 84this approach is. The syntactic mechanism, 85although implemented initially to support restricted quantification, can 86also be used to support better approximations to notations like 87$\sum_{i=1}^{n}x_i$; this could, for example, be represented by 88$\con{Sum}\ i ${\small\verb%::(1,%}$n${\small\verb%).%}$\ x_i$, via a 89suitable definition of the constant $\con{Sum}$. 90 91 92The set notation allows finite sets to be written in the form 93{\small\verb%"{%}$t_1,t_2,\ldots,t_n${\small\verb%}"%}. It also 94supports set abstraction notation of the form 95{\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%}; for example 96{\small\verb%"{2*x|x>0}"%} and {\small\verb%"{(x,y)|x=y}"%}. Both 97these notations can be mounted onto any underlying set theory (or even 98onto theories of lists, bags etc.), although they were initially 99designed for use with the library \ml{sets} (which was previously 100called \ml{all\_sets}). This library has been greatly extended. 101 102 103Version 2.0 has libraries {\small\verb%parser%} and 104{\small\verb%prettyp%}, which provide parser and pretty-printer 105support for embedded languages. These are currently being used to 106provide theorem-proving tools for the hardware description languages 107{\small ELLA}, {\small VHDL} and {\small SILAGE}, and for various 108other special purpose languages. A mechanism called ``syntax blocks'' 109allows user-specified parsers to be invoked from \ML. The development 110of methodologies for embedding application-specific languages in \HOL\ 111is a major topic of research at Cambridge. 112 113A facility is provided to support experiments with user-programmed 114quotation typecheckers for the \HOL\ logic. This enables more type 115inference to be implemented. 116 117Many new conversions are provided. The most useful ones are described 118in Section~\ref{CONVERSIONS} below. 119 120In the sections that follow, those new things in Version 2.0 which 121are likely to be of most general use are described. Section~\ref{adddel} 122list the \ML\ bindings that have ben added and deleted in Version 2.0. 123 124 125\section{Directory reorganization} 126 127The help files and manual have been split apart into two separate directories. 128The top-level of the \HOL\ distribution directory now contains: 129 130\begin{itemize} 131\item \ml{Manual}: directory containing the manual sources; 132\item \ml{help}: directory containing text files for online help, as well 133as for the \REFERENCE\ part of the manual. 134\end{itemize} 135 136\noindent The search path mechanism has been revised in various ways. 137 138 139Library pathnames are now no longer on the default search path, nor 140are they added to the search path when a library is loaded (it is 141the responsibility of the library's load-file to do this, if desired). 142As a consequence, the predefined \ML\ value \ml{Libraries} is no longer used. 143 144The initial search path is now: 145 146\begin{hol}\begin{alltt} 147 [``; `~/`; `\(directory\)/theories/`] 148\end{alltt}\end{hol} 149 150\noindent where $directory$ is the site-specific absolute pathname in which 151the \HOL\ distribution directory (`\ml{hol}') resides. 152 153The \ML\ functions \ml{add\_to\_search\_path} and 154\ml{append\_to\_search\_path} are 155no longer built-in. Users may define them, if required, by: 156 157\begin{hol}\begin{verbatim} 158 let add_to_search_path p = set_search_path(p.search_path()) 159 160 let append_to_search_path p = set_search_path(search_path()@[p]) 161\end{verbatim}\end{hol} 162 163The \ml{install} function now sets the search path to: 164 165\begin{hol}\begin{alltt} 166 [``; `~/`; \(arg\)^`/theories/`] 167\end{alltt}\end{hol} 168 169\noindent where $arg$ is the string argument to install. 170 171\section{Location of libraries} 172 173The function 174 175\begin{holboxed}\index{library_pathname@\ml{library\_pathname}} 176\begin{verbatim} 177 library_pathname : void -> string 178\end{verbatim}\end{holboxed} 179 180\noindent returns the internal pathname used by \HOL\ to 181load libraries. This pathname, which is site-specific and is given an initial 182value when the system is built, should be the absolute pathname of the \HOL\ 183system library directory. This pathname will typically have the form: 184 185\begin{hol}\begin{alltt} 186 `\(directory\)/hol/Library` 187\end{alltt}\end{hol} 188 189\noindent where $directory$ is the site-specific absolute pathname in which the \HOL\ 190distribution directory (`\ml{hol}') resides. The value returned by 191\ml{library\_pathname} can be changed by users only via the \ml{install} function. 192 193The string returned by \ml{library\_pathname} is primarily used in 194library load-files to update the \HOL\ search path and help search 195path. For example, suppose that in a library \ml{lib} there is a 196directory \ml{help} which contains online help files specific to this 197library. The load-file {\small\verb%lib.ml%} can then update the help 198search path as follows: 199 200\begin{hol}\begin{verbatim} 201 let path = library_pathname() ^ `/lib/help/` 202 in 203 set_help_search_path (path . help_search_path()) 204\end{verbatim}\end{hol} 205 206\noindent This will make the help files of the library \ml{lib} 207available for online help 208whenever the library is loaded. 209 210 211 212\section{More flexible help system}\index{help@\ml{help}}\index{help system|(} 213 214 215The help system now uses \ml{cat} rather than \ml{more} as the default for 216displaying help files. This default can be changed with the \ML\ function: 217 218\begin{holboxed}\index{set_help@\ml{set\_help}} 219\begin{verbatim} 220 set_help : string -> string 221\end{verbatim}\end{holboxed} 222 223\noindent This installs a new user-supplied help function, and returns the 224previous one as result. The effect of 225 226\begin{hol}\begin{alltt} 227 help `\(file\)` 228\end{alltt}\end{hol} 229 230\noindent is to pipe the appropriate help file derived from $file${\small\verb%.doc%} 231into the current help function, 232with the top level of \ML\ being the standard output. 233For example, 234 235\begin{hol}\begin{verbatim} 236 set_help `lpr` 237\end{verbatim}\end{hol} 238 239\noindent will cause the help file to be printed instead of being displayed and 240 241\begin{hol}\begin{verbatim} 242 set_help `lpr -Pbarf` 243\end{verbatim}\end{hol} 244 245\noindent will cause it to be printed to the printer \ml{barf}. 246 247 248Two new functions: 249 250\begin{holboxed} 251\index{set_help_search_path@\ml{set\_help\_search\_path}} 252\index{help_search_path@\ml{help\_search\_path}} 253\begin{verbatim} 254 set_help_search_path : string list -> void 255 help_search_path : void -> string list 256\end{verbatim}\end{holboxed} 257 258\noindent have been added to the system for accessing the 259internal search path used by \HOL\ to find online help files. The help 260search path has precisely the same format as the regular search path, 261and these two function are analogous to the \ML\ functions 262\ml{search\_path} and \ml{set\_search\_path}.\index{help system|)} 263 264 265 266\section{Syntax for restricted quantification} 267\index{types, in HOL logic@types, in \HOL\ logic! dependent} 268\index{dependent types in HOL logic@dependent types in \HOL\ logic} 269 270Syntactic support for restricted quantification and abstraction is now 271provided. This follows a suggestion discussed at the Second \HOL\ Users 272Meeting and implements a method of simulating subtypes and dependent 273types with predicates. 274 275Currently no derived rules are provided to support this notation, so 276any inferences will need to work on the underlying semantic 277representation. 278 279The new syntax automatically translates as follows: 280 281\begin{hol} 282{\small\verb% \%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_ABSTRACT %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\ 283{\small\verb% !%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_FORALL %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\ 284{\small\verb% ?%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_EXISTS %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%}\\ 285{\small\verb% @%}$v${\small\verb%::%}$P${\small\verb%.%}$B${\small\verb% <----> RES_SELECT %}$P${\small\verb% (\%}$v${\small\verb%.%}$B${\small\verb%)%} 286\end{hol} 287 288Anything can be written between the binder and `\ml{::}' that could be 289written between the binder and `\ml{.}` in the old notation. See the 290examples below. 291 292The flag \ml{print\_restrict} has default \ml{true}, but if set to 293\ml{false} will 294disable the pretty printing. This is useful for seeing what the 295semantics of particular restricted abstractions are. 296 297The constants \ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and 298\ml{RES\_SELECT} are 299defined in the theory \ml{bool} by: 300 301\begin{hol}\begin{verbatim} 302 RES_ABSTRACT P B = \x:*. (P x => B x | ARB:**) 303 304 RES_FORALL P B = !x:*. P x ==> B x 305 306 RES_EXISTS P B = ?x:*. P x /\ B x 307 308 RES_SELECT P B = @x:*. P x /\ B x 309\end{verbatim}\end{hol} 310 311\noindent where the constant \ml{ARB} is defined in the theory \ml{bool} by: 312 313\begin{hol}\begin{verbatim} 314 ARB = @x:*. T 315\end{verbatim}\end{hol} 316 317User-defined binders can also have restricted forms, which are set up 318with the function: 319 320\begin{holboxed}\index{associate_restriction@\ml{associate\_restriction}} 321\begin{verbatim} 322 associate_restriction : (string # string) -> * 323\end{verbatim}\end{holboxed} 324 325 326\noindent If \m{B} is the name 327of a binder and \ml{RES\_}$B$ is the name of a suitable constant (which 328must be explicitly defined), then executing: 329 330\begin{hol} 331{\small\verb% associate_restriction(`%}\m{B}{\small\verb%`, `RES_%}\m{B}{\small\verb%`)%} 332\end{hol} 333 334\noindent will cause the parser and pretty-printer to support: 335 336\begin{hol} 337{\small\verb% %}$B$ $v${\small\verb%::%}$P${\small\verb%. %}$B${\small\verb% <----> RES_%}$B$ $P${\small\verb% (\%}$v${\small\verb%. %}$B${\small\verb%)%} 338\end{hol} 339 340\noindent Note that associations between user defined binders and their 341restrictions are not stored in theory files, so they have to be set up 342for each \HOL\ session (e.g.\ with a {\small\verb%hol-init.ml%} initialization file). 343 344Here is an example session: 345 346\setcounter{sessioncount}{1} 347\begin{session}\begin{verbatim} 348#"!x y::P. x<y";; 349"!x y :: P. x < y" : term 350 351#set_flag(`print_restrict`, false);; 352true : bool 353 354#"!x y::P. x<y";; 355"RES_FORALL P(\x. RES_FORALL P(\y. x < y))" : term 356 357#"?(x,y) p::(\(m,n).m<n). p=(x,y)";; 358"RES_EXISTS 359 (\(m,n). m < n) 360 (\(x,y). RES_EXISTS(\(m,n). m < n)(\p. p = x,y))" 361: term 362 363#"\x y z::P.[0;x;y;z]";; 364"RES_ABSTRACT P(\x. RES_ABSTRACT P(\y. RES_ABSTRACT P(\z. [0;x;y;z])))" 365: term 366\end{verbatim}\end{session} 367 368A conversion that rewrites away the constants \ml{RES\_ABSTRACT}, 369\ml{RES\_FORALL}, \ml{RES\_EXISTS} and \ml{RES\_SELECT} is: 370 371\begin{hol}\begin{verbatim} 372 let RESTRICT_CONV = 373 (REWRITE_CONV [definition `bool` `RES_ABSTRACT`; 374 definition `bool` `RES_FORALL`; 375 definition `bool` `RES_EXISTS`; 376 definition `bool` `RES_SELECT`]) 377 THENC (DEPTH_CONV BETA_CONV) 378\end{verbatim}\end{hol} 379 380\noindent This is a bit unsatisfactory, as is shown by the artificial 381example below: 382 383\setcounter{sessioncount}{1} 384\begin{session}\begin{verbatim} 385#let t = "!x y::P.?f:num->num::Q. f(@n::R.T) = (x+y)";; 386t = "!x y :: P. ?f :: Q. f(@n :: R. T) = x + y" : term 387 388#RESTRICT_CONV t;; 389|- (!x y :: P. ?f :: Q. f(@n :: R. T) = x + y) = 390 (!x. P x ==> (!x'. P x' ==> (?x. Q x /\ (x(@x. R x /\ T) = x + x')))) 391\end{verbatim}\end{session} 392 393The variable \ml{x} in the definitions of the constants 394\ml{RES\_ABSTRACT}, \ml{RES\_FORALL}, \ml{RES\_EXISTS} and 395\ml{RES\_SELECT} gets confused with the variable in the supplied term. 396This can be avoided by changing \ml{RESTRICT\_CONV} to perform 397explicit alpha-conversion. For example, by implementing a conversion: 398 399\begin{hol} 400{\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%]%} 401\end{hol} 402 403\noindent Dealing with the case when 404$v$ is a variable structure is also desirable. For example: 405 406\begin{session}\begin{verbatim} 407#let t1 = "!(m,n)::P. m<n";; 408t1 = "!(m,n) :: P. m < n" : term 409 410#RESTRICT_CONV t1;; 411|- (!(m,n) :: P. m < n) = (!x. P x ==> (\(m,n). m < n)x) 412 413\end{verbatim}\end{session} 414 415\noindent If anyone writes the desired conversions please let us know! 416 417Here is an example of a user-defined restriction: 418 419\begin{session}\begin{verbatim} 420#new_binder_definition(`DURING`, "DURING(p:num#num->bool) = $!p");; 421|- !p. $DURING p = $! p 422 423#"DURING x::(m,n). p x";; 424no restriction constant associated with DURING 425skipping: x " ;; parse failed 426 427#new_definition 428# (`RES_DURING`, "RES_DURING(m,n)p = !x. m<=x /\ x<=n ==> p x");; 429|- !m n p. RES_DURING(m,n)p = (!x. m <= x /\ x <= n ==> p x) 430 431#associate_restriction(`DURING`,`RES_DURING`);; 432() : void 433 434#"DURING x::(m,n). p x";; 435"DURING x :: (m,n). p x" : term 436 437#set_flag(`print_restrict`,false);; 438true : bool 439 440#"DURING x::(m,n). p x";; 441"RES_DURING(m,n)(\x. p x)" : term 442\end{verbatim}\end{session} 443 444 445\section{Syntax for sets}\index{set theory notation} 446 447The special purpose set-theoretic notations 448{\small\verb%"{%}$t_1,t_2,\ldots,t_n${\small\verb%}"%} and 449{\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} are now available. 450The normal interpretation of the former is the finite set containing 451$t_1,t_2,\ldots, t_n$ and the normal interpretation of the latter 452is the set of all $t$s such that $p$. These interpretations are predefined for 453the library \ml{sets}, but the user can use the syntax for other purposes if 454he or she wishes using the functions: 455 456\begin{holboxed} 457\index{define_finite_set_syntax@\ml{define\_finite\_set\_syntax}} 458\index{define_set_abstraction_syntax@\ml{define\_set\_abstraction\_syntax}} 459\begin{alltt} 460 define_finite_set_syntax : (string # string) -> void 461 define_set_abstraction_syntax : string -> void 462\end{alltt}\end{holboxed} 463 464Executing: 465 466\begin{hol}\begin{alltt} 467 define_finite_set_syntax(`\(\con{c}\sb{1}\)`,`\(\con{c}\sb{2}\)`) 468\end{alltt}\end{hol} 469 470\noindent causes {\small\verb%"{%}$t_1,\ldots,t_n${\small\verb%}"%} 471to parse to: 472 473\begin{hol}\begin{alltt} 474 "\(c\sb{2}\) \(t\sb{1}\) (\(c\sb{2}\) \(t\sb{2}\) \(\cdots\) (\(c\sb{2}\) \(t\sb{n}\) \(c\sb{2}\)) \(\cdots\) ))" 475\end{alltt}\end{hol} 476 477\noindent with failure if either $c_1$ or $c_2$ 478is not the name of a constant. 479 480In the library \ml{sets}, the empty set is \ml{EMPTY} and 481the infixed function \ml{INSERT} adds an element to a set. 482Executing: 483 484\begin{hol}\begin{verbatim} 485 define_finite_set_syntax(`EMPTY`,`INSERT`) 486\end{verbatim}\end{hol} 487 488\noindent will cause 489 490\begin{hol}\begin{verbatim} 491 "{1,2,3,4}" 492\end{verbatim}\end{hol} 493 494\noindent to parse to 495 496\begin{hol}\begin{verbatim} 497 "1 INSERT (2 INSERT (3 INSERT (4 INSERT EMPTY)))" 498\end{verbatim}\end{hol} 499 500 501Executing: 502 503\begin{hol}\begin{alltt} 504 define_set_abstraction_syntax `\(c\)` 505\end{alltt}\end{hol} 506 507\noindent causes {\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} 508to parse to: 509 510\medskip 511 512\noindent{\small 513{\verb% "%}}$c${\small{\verb%(\(%}$x_1${\verb%,%}$\ldots${\verb%,%}$x_n${\verb%).(%}$t${\verb%,%}$p${\verb%))"%} 514} 515 516\medskip 517 518\noindent where $x_1$, $\ldots$ , $x_n$ are the free variables occurring in both $t$ 519and $p$. If there are no such free variables then an error results. 520The order in which the variables are listed in the variable structure 521of the paired abstraction is an unspecified function of the structure 522of $t$ (it is approximately left to right). Failure if $c$ is not the 523name of a constant. 524 525For example, if the library \ml{sets} (i.e.\ what used to be \ml{all\_sets}) 526is loaded, then 527 528\begin{hol}\begin{verbatim} 529 define_set_abstraction_syntax `GSPEC` 530\end{verbatim}\end{hol} 531 532\noindent will cause 533 534\begin{hol}\begin{verbatim} 535 "{x+y | (x < y) /\ (y < z)}" 536\end{verbatim}\end{hol} 537 538\noindent to parse to: 539 540\begin{hol}\begin{verbatim} 541 "GSPEC(\(x,y). ((x+y), (x < y) /\ (y < z)))" 542\end{verbatim}\end{hol} 543 544\noindent where \ml{GSPEC} is defined by: 545 546\begin{hol}\begin{verbatim} 547 |- !f. GSPEC f = SPEC(\x. ?y. x,T = f y) 548\end{verbatim}\end{hol} 549 550\noindent and \ml{SPEC} abstracts a predicate to a set (it is the abstraction 551bijection used in the definition of the type operator \ml{set}). 552Other examples are: 553 554\begin{hol}\begin{verbatim} 555 "{x+y+z | (x < y) /\ (y < z)}" 556\end{verbatim}\end{hol} 557 558\noindent will parse to: 559 560\begin{hol}\begin{verbatim} 561 "GSPEC(\(x,y,z). (x+(y+z), (x < y /\ y < z)))" 562\end{verbatim}\end{hol} 563 564\noindent and 565 566\begin{hol}\begin{verbatim} 567 "{x+y+w | (x < y) /\ (y < z)}" 568\end{verbatim}\end{hol} 569 570\noindent will parse to: 571 572\begin{hol}\begin{verbatim} 573 "GSPEC(\(x,y). (x+(y+w), (x < y /\ y < z)))" 574\end{verbatim}\end{hol} 575 576 577Note that the precedence of comma is increased in the contexts 578``{\small\verb%{%}$\cdots${\small\verb%}%}'' and 579``{\small\verb%{%}$\cdots${\small\verb%|%}''. 580Terms will be printed in set notation if the flag \ml{print\_set} is 581\ml{true}. 582Note that 583 584\medskip 585 586\ml{"}$c${\small\verb%(\(%}$x_1$\ml{,}$\ldots$\ml{,}$x_n$\ml{).(}$t$\ml{,}$p$\ml{))"} 587 588\medskip 589 590\noindent will only print as 591{\small\verb%"{%}$t${\small\verb%|%}$p${\small\verb%}"%} 592if the variables $x_1$, $\ldots$ , 593$x_n$ occur free in both $t$ and $p$ (and \ml{print\_set} is \ml{true}) . 594 595\section{Revised set theory libraries}\label{LIBRARY} 596\index{set theory libraries} 597 598In previous versions of the system, there were three libraries dealing with 599elementary set theory: 600 601\begin{myenumerate} 602\item \ml{sets}: a theory of finite sets (Windley and Leveilley); 603\item \ml{all\_sets}: a theory of infinite and finite sets (Windley and Leveilley); 604\item \ml{set}: a theory of predicates-as-sets (Kalker). 605\end{myenumerate} 606 607Each of these libraries is useful for certain applications, and all three will 608therefore continue to be supported. To better reflect the contents of these 609libraries, they have been renamed as follows: 610 611\begin{myenumerate} 612\item \ml{sets} is now called \ml{finite\_sets}; 613\item \ml{all\_sets} is now called \ml{sets}; 614\item \ml{set} is now called \ml{pred\_sets}. 615\end{myenumerate} 616 617The \ml{sets} library (formerly, \ml{all\_sets}) has been extensively revised and 618extended. The library has been restructured, and several additional built-in 619theorems are available. Parser and pretty-printer support for the notation: 620 621\begin{itemize} 622\item \ml{\{$x_1,\ldots,x_n$\}} denotes a finite set. 623 624\item \ml{\{$x$|$P[x]$\}} denotes the set of all \ml{$x$} such that 625\ml{$P[x]$}. 626 627\item \ml{\{$t[x]$|$P[x]$\}} denotes the set of all \ml{$t[x]$} 628such that \ml{$P[x]$}. 629\end{itemize} 630 631\noindent is now provided by the parser/pretty-printer extension mentioned above. 632 633Proof support is supplied for this notation in the form of a conversion 634 635\begin{holboxed}\index{SET_SPEC_CONV@\ml{SET\_SPEC\_CONV}} 636\begin{verbatim} 637 SET_SPEC_CONV : conv 638\end{verbatim}\end{holboxed} 639 640\noindent which implements the axiom of specification for generalized set 641specifications. 642 643\ml{SET\_SPEC\_CONV} accepts two types of input. 644 645\begin{hol} 646{\small\verb% SET_SPEC_CONV "%}$t${\small\verb% IN {%}$v${\small\verb% | %}$p${\small\verb%[%}$v${\small\verb%]}" %}(where $v$ is a variable) 647\end{hol} 648 649\noindent this returns the theorem: 650 651\begin{hol}\begin{alltt} 652 |- \(t\) IN \{\(v\) | \(p[v]\)\} = \(p[t/v]\) 653\end{alltt}\end{hol} 654 655\noindent Furthermore 656 657\begin{hol}\begin{alltt} 658 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}]\)\}" 659\end{alltt}\end{hol} 660 661\noindent returns the theorem 662 663\medskip 664 665{\small 666\begin{tabular}{ll} 667{\verb%|-%} & $t_1\ \ml{IN}\ ${\verb%{%}$t_2[x_1,\ldots,x_n]${\verb%|%}$p[x_1,\ldots,x_n]${\verb%}%}\\ 668 & \ml{=}\\ 669 & {\verb%?%}$x_1\cdots x_n${\verb%. (%}$t_1 \ml{=} t_2[x_1,\ldots,x_n]${\verb%) /\ %}$p[x_1,\ldots,x_n]$\\ 670\end{tabular} 671} 672 673\medskip 674 675\begin{hol}\begin{verbatim} 676 |- x IN {n | n < m} = x < m 677 678 |- 5 IN {x+y | x < 2 /\ y < 3} = ?x y. (5 = x + y) /\ x < 2 /\ y < 3 679\end{verbatim}\end{hol} 680 681The library \ml{sets} also makes available an induction principle for 682proving properties of finite sets. 683 684\begin{holboxed}\index{SET_INDUCT_TAC@\ml{SET\_INDUCT\_TAC}} 685\begin{verbatim} 686 SET_INDUCT_TAC : tactic 687\end{verbatim}\end{holboxed} 688 689\begin{hol}\begin{alltt} 690 "!\(s\). FINITE \(s\) ==> \(P\)[\(s\)]" 691 ============================= SET_INDUCT_TAC 692 \(P\)[EMPTY] \(P\)[\(x\) INSERT \(t\)] 693 [ "FINITE \(t\)" ] 694 [ "\(P\)[\(s\)]"] 695 [ "~\(x\) IN \(t\)"] 696\end{alltt}\end{hol} 697 698\noindent The file {\small\verb%Libaries/sets/COMPAT.READ.ME%} provides an 699index to theorem names in the new library and other compatibility information. 700This is intended to help users update proof scripts based on the old version of 701the \ml{all\_sets} library. 702 703 704 705\section{Syntax blocks} 706 707\index{syntax blocks|(} 708A syntax block starts with a keyword and ends with a terminator and is 709associated with a function on strings. When such a block is 710encountered in the input stream, all the characters between the start 711keyword and the terminator are made into a string to which the 712associated function is applied. Syntax blocks can be used with the 713parser generator library {\small\verb%parser%} to parse user-specified 714languages into \HOL\ terms. See the documentation of the library for 715details and examples. 716 717The ML function: 718 719\begin{holboxed}\index{new_syntax_block@\ml{new\_syntax\_block}} 720\begin{verbatim} 721 new_syntax_block : string # string # string -> void 722\end{verbatim}\end{holboxed} 723 724 725\noindent declares a new syntax block. The first argument is the start keyword 726of the block, the second argument is the terminator and the third 727argument is the name of a function having a type which is an instance 728of {\small\verb%string->*%}. The effect of 729 730\begin{hol} 731\ml{ new\_syntax\_block(`XXX`, `YYY`, `}$f$\ml{`);;} 732\end{hol} 733 734\noindent is that if subsequently 735 736\begin{hol}\begin{verbatim} 737 XXX ... YYY 738\end{verbatim}\end{hol} 739 740\noindent occurs in the input, then it is as though 741 742\begin{hol} 743\ml{ }$f$\ml{ ` ... `} 744\end{hol} 745 746\noindent were input instead. For example: 747 748\setcounter{sessioncount}{1} 749\begin{session}\begin{verbatim} 750#let foo s = print_string `Hello: `; print_string s; print_newline();; 751foo = - : (string -> void) 752 753#new_syntax_block(`<<`,`>>`, `foo`);; 754() : void 755 756#<< Mike >>;; 757Hello: Mike 758() : void 759 760\end{verbatim}\end{session} 761 762The following function is useful with syntax blocks, because it enables 763backslash ({\small\verb%\%}) to be included in strings. 764 765\begin{holboxed}\index{set_string_escape@\ml{set\_string\_escape}} 766\begin{verbatim} 767 set_string_escape : int -> int 768\end{verbatim}\end{holboxed} 769 770\noindent This changes the escape character in strings to be the character with the 771supplied ascii code (initially this is {\small\verb%92%}, 772viz. `{\small\verb%\%}`). 773The old escape character is returned.\index{syntax blocks|)} 774 775\section{User-programmable quotation typechecker} 776 777The typechecker for \HOL\ quotations contains a number of arbitrary 778design decisions. Several people have suggested changes, e.g.\ that 779full Hindley/Milner type inference be performed. Rather than try to 780create a single new improved typechecker, a facility is now provided 781that enables the user to write his or her own one and then to install 782it in the system. 783 784\index{preterms|(} 785The \ML\ abstract type {\small\verb%preterm%} represents the parse trees of \HOL\ 786terms. A typechecker is a function of type {\small\verb%preterm->term%}. If the flag 787\ml{preterm} is set to \ml{true} (the default is \ml{false}), then \HOL\ will use 788whatever \ML\ function is currently bound to the name 789\ml{preterm\_handler} as 790the quotation typechecker. The way this works is that when 791\ml{preterm} is true the parser produces a preterm rather than a term, 792and then wraps a call of \ml{preterm\_handler} 793around the quotation.\index{type checking, in HOL logic@type checking, 794in \HOL\ logic!user programmed} Other uses of preterms are possible, for example 795as patterns for describing terms. 796 797The definition of the \ML\ type {\small\verb%preterm%} is: 798 799\begin{hol}\index{preterm@\ml{preterm}}\begin{alltt} 800 rectype preterm = 801 preterm_var of string \({\it Variables}\) 802 | preterm_const of string \({\it Constants}\) 803 | preterm_comb of preterm # preterm \({\it Combinations}\) 804 | preterm_abs of preterm # preterm \({\it Abstractions}\) 805 | preterm_typed of preterm # type \({\it Explicit typing}\) 806 | preterm_antiquot of term \({\it Antiquotation}\) 807\end{alltt}\end{hol} 808 809The function: 810 811\begin{holboxed}\index{preterm_to_term@\ml{preterm\_to\_term}} 812\begin{verbatim} 813 preterm_to_term : preterm -> term 814\end{verbatim}\end{holboxed} 815 816\noindent invokes the standard \HOL\ typechecker on a preterm and returns the 817resulting typechecked term (or causes the standard error message).\index{preterms|)} 818 819 820 821The following is a rather contrived example: 822 823\setcounter{sessioncount}{1} 824\begin{session}\index{preterm_handler@\ml{preterm\_handler}} 825\begin{verbatim} 826#letref p_reg = preterm_var `x`;; 827p_reg = preterm_var `x` : preterm 828 829#let preterm_handler p = p_reg:=p; 830 print_string `Typechecking ... `; 831 print_newline(); 832 preterm_to_term p;; 833preterm_handler = - : (preterm -> term) 834\end{verbatim}\end{session} 835 836\begin{session} 837\begin{verbatim} 838#set_flag(`preterm`,true);; 839false : bool 840 841#"x+y";; 842Typechecking ... 843"x + y" : term 844 845#p_reg;; 846preterm_comb((preterm_comb((preterm_const `+`), preterm_var `x`)), 847 preterm_var `y`) 848: preterm 849\end{verbatim}\end{session} 850 851\noindent Different top-level typechecking can be defined by using a 852different definition of the function 853\ml{preterm\_handler}. Note that typechecking 854is purely a `user interface' feature, so changing the typechecker does 855not compromise the logical soundness of \HOL. 856 857 858 859 860\section{New conversions}\label{CONVERSIONS} 861 862 863Many new conversions have been added to the system. Only those likely to be of 864general interest are listed here. 865 866\subsection{Generalized beta-reduction} 867 868A new conversion: 869 870 871\begin{holboxed}\index{PAIRED_BETA_CONV@\ml{PAIRED\_BETA\_CONV}} 872\begin{verbatim} 873 PAIRED_BETA_CONV : conv 874\end{verbatim}\end{holboxed} 875 876\noindent has been added to do 877generalized beta-conversion of tupled lambda abstractions applied to 878tuples. 879 880Given the term: 881 882\begin{hol} 883{\small\verb% "(\(%}$x_1, \ldots ,x_n${\small\verb%).%}$t${\small\verb%) (%}$t_1, \ldots ,t_n${\small\verb%)"%} 884\end{hol} 885 886\noindent \ml{PAIRED\_BETA\_CONV} proves that: 887 888\begin{hol} 889{\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%]%} 890\end{hol} 891 892The conversion works for arbitrarily nested tuples. For example: 893 894\setcounter{sessioncount}{1} 895\begin{session}\begin{verbatim} 896#PAIRED_BETA_CONV "(\((a,b),(c,d)). [a;b;c;d]) ((1,2),(3,4))";; 897|- (\((a,b),c,d). [a;b;c;d])((1,2),3,4) = [1;2;3;4] 898\end{verbatim}\end{session} 899 900\subsection{Arithmetical conversions} 901 902The conversion: 903 904\begin{holboxed}\index{ADD_CONV@\ml{ADD\_CONV}} 905\begin{verbatim} 906 ADD_CONV : conv 907\end{verbatim}\end{holboxed} 908 909\noindent does addition by formal proof. 910If $n$ and $m$ are numerals then 911{\small\verb%ADD_CONV "%}$n\ $\ml{+}$\ m$\ml{"} 912returns the theorem {\small\verb%|- %}$n\ $\ml{+}$\ m\ $\ml{=}$\ s$, 913where $s$ is the numeral denoting the sum of $n$ and $m$. For example: 914 915\setcounter{sessioncount}{1} 916\begin{session}\begin{verbatim} 917#ADD_CONV "1 + 2";; 918|- 1 + 2 = 3 919 920#ADD_CONV "0 + 1000";; 921|- 0 + 1000 = 1000 922 923#ADD_CONV "101 + 102";; 924|- 101 + 102 = 203 925\end{verbatim}\end{session} 926 927 928 929A new conversion has been added for deciding equality of natural number 930constants. 931 932\begin{holboxed}\index{num_EQ_CONV@\ml{num\_EQ\_CONV}} 933\begin{verbatim} 934 num_EQ_CONV : conv 935\end{verbatim}\end{holboxed} 936 937\noindent If $n$ and $m$ are terms constructed from numeral constants 938and the successor function \ml{SUC}, then: 939{\small\verb%num_EQ_CONV "%}$n$\ml{=}$m$\ml{"} 940returns: 941 942\begin{hol} 943\ml{ |- (\(n\)=\(m\)) = T }if \(n\) and \(m\) represent the same number,\\ 944\ml{ |- (\(n\)=\(m\)) = F }if \(n\) and \(m\) represent different numbers. 945\end{hol} 946 947\noindent In addition, {\small\verb%num_EQ_CONV "%}$t\ $\ml{=}$\ t$\ml{"} 948returns: {\small\verb%|- (%}$t$\ml{=}$t${\small\verb%) = T%} 949 950\subsection{List processing conversions} 951 952Two new conversions for lists are now built-in: 953 954\begin{holboxed} 955\index{LENGTH_CONV@\ml{LENGTH\_CONV}} 956\index{list_EQ_CONV@\ml{list\_EQ\_CONV}} 957\begin{verbatim} 958 LENGTH_CONV : conv 959 list_EQ_CONV: conv 960\end{verbatim}\end{holboxed} 961 962\ml{LENGTH\_CONV}: computes the length of a list. 963A call to: 964 965\begin{hol}\begin{alltt} 966 LENGTH_CONV "LENGTH[\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)]" 967\end{alltt}\end{hol} 968 969\noindent generates the theorem: 970 971\begin{hol}\begin{alltt} 972 |- LENGTH [\(t\sb{1}\);\(\ldots\);\(t\sb{n}\)] = n 973\end{alltt}\end{hol} 974 975The other conversion, \ml{list\_EQ\_CONV}, proves or disproves the 976equality of two lists, given 977a conversion for deciding the equality of elements. 978A call to: 979 980\begin{hol}\begin{alltt} 981 list_EQ_CONV \(conv\) "[\(u\sb{1}\);\(\ldots\);\(u\sb{n}\)] = [\(v\sb{1}\);\(\ldots\);\(v\sb{m}\)]" 982\end{alltt}\end{hol} 983 984\noindent returns: {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ F} if: 985 986\begin{myenumerate} 987\item \ml{~($n$=$m$)} or 988\item \ml{$conv$} proves {\small\verb%|- (%}$u_i\ $\ml{=}$\ v_i$\ml{)\ =\ F} 989for any $1\leq i \leq m$. 990\end{myenumerate} 991 992\noindent {\small\verb%|- ([%}$u_1$\m{;}$\ldots$\ml{;}$u_n$\ml{]\ =\ [}$v_1$\ml{;}$\ldots$\ml{;}$v_m$\ml{])\ =\ T} is returned if: 993 994\begin{myenumerate} 995 996\item \ml{($n$=$m$)} and \ml{$u_i$} is syntactically identical to 997\ml{$v_i$} for $1\leq i \leq m$, or 998\item \ml{($n$=$m$)} and \ml{$conv$} proves 999{\small\verb%|- (%}$u_i$\ml{=}$v_i$\ml{)=T} for $1\leq i \leq n$. 1000\end{myenumerate} 1001 1002\subsection{Simplifying {\tt let}-terms} 1003\index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!simplification of} 1004 1005A conversion for reducing {\tt let}-terms is now provided. 1006 1007\begin{holboxed}\index{let_CONV@\ml{let\_CONV}} 1008\begin{verbatim} 1009 let_CONV : conv 1010\end{verbatim}\end{holboxed} 1011 1012\noindent Given a term: 1013 1014\begin{hol}\begin{alltt} 1015 "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}]\)" 1016\end{alltt}\end{hol} 1017 1018\noindent \ml{let\_CONV} proves that: 1019 1020\begin{hol}\begin{alltt} 1021 |- 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}]\) 1022\end{alltt}\end{hol} 1023 1024\noindent The \ml{$v_i$}'s can take any one of the following forms: 1025 1026\begin{myenumerate} 1027\item Variables: \ml{x} etc. 1028\item Tuples: \ml{(x,y)}, \ml{(a,b,c)}, \ml{((a,b),(c,d))} etc. 1029\item Applications: \ml{f (x,y) z}, \ml{f x} etc. 1030\end{myenumerate} 1031 1032\noindent Variables are just substituted for. With tuples, the substitution is 1033done component-wise, and function applications are effectively 1034rewritten in the body of the {\tt let}-term. 1035 1036\setcounter{sessioncount}{1} 1037\begin{session}\begin{verbatim} 1038#let_CONV "let x = 1 in x+y";; 1039|- (let x = 1 in x + y) = 1 + y 1040 1041#let_CONV "let (x,y) = (1,2) in x+y";; 1042|- (let (x,y) = 1,2 in x + y) = 1 + 2 1043 1044#let_CONV "let f x = 1 and f y = 2 in (f 10) + (f 20)";; 1045|- (let f x = 1 and f y = 2 in (f 10) + (f 20)) = 2 + 2 1046 1047#let_CONV "let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))";; 1048|- (let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))) = 1049 (((0 + 2) + 1) + 2) + 1 1050 1051#CONV_RULE(DEPTH_CONV ADD_CONV)it;; 1052|- (let f x = x + 1 and g x = x + 2 in f(g(f(g 0)))) = 6 1053 1054#let_CONV "let f x y = x+y in f 1";; % NB: partial application % 1055|- (let f x y = x + y in f 1) = (\y. 1 + y) 1056\end{verbatim}\end{session} 1057 1058\subsection{Skolemization}\index{Skolemization} 1059 1060Two conversions are provided for a higher-order version of 1061Skolemization (using existentially quantified function variables 1062rather than first-order Skolem constants). 1063 1064The conversion 1065 1066\begin{holboxed}\index{X_SKOLEM_CONV@\ml{X\_SKOLEM\_CONV}} 1067\begin{verbatim} 1068 X_SKOLEM_CONV : term -> conv 1069\end{verbatim}\end{holboxed} 1070 1071\noindent takes a variable parameter, \ml{$f$} say, and 1072proves: 1073 1074\begin{hol}\begin{alltt} 1075 |- (!\(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}]\) 1076\end{alltt}\end{hol} 1077 1078\noindent for any input term 1079\ml{!$x_1\ \ldots\ x_n$.\ ?$y$. $t[x_1,\ldots,x_n,y]$}. 1080Note that when $n=\ml{0}$, this 1081is equivalent to alpha-conversion: 1082 1083\begin{hol}\begin{alltt} 1084 |- (?\(y\). \(t[y]\)) = (?\(f\). \(t[f]\)) 1085\end{alltt}\end{hol} 1086 1087\noindent and that the conversion fails if there is already a free 1088variable \ml{$f$} of the appropriate type in the input term. For example: 1089 1090\begin{hol}\begin{alltt} 1091 X_SKOLEM_CONV "f:num->*" "!n:num. ?x:*. x = (f n)" 1092\end{alltt}\end{hol} 1093 1094\noindent will fail. The conversion \ml{SKOLEM\_CONV} is 1095like \ml{X\_SKOLEM\_CONV}, except that it 1096uses a primed variant of the name of the existentially quantified variable 1097as the name of the skolem function it introduces. For example: 1098 1099\begin{hol}\begin{alltt} 1100 SKOLEM_CONV "!x. ?y. P x y" 1101\end{alltt}\end{hol} 1102 1103\noindent proves that: 1104 1105\begin{hol}\begin{alltt} 1106 |- ?y. !x. P x (y x) 1107\end{alltt}\end{hol} 1108 1109 1110\subsection{Quantifier movement conversions} 1111\index{quantifiers!conversions for} 1112\index{conversions!quantifier movement} 1113 1114A complete and systematically-named set of conversions for moving quantifiers 1115inwards and outwards through the logical connectives {\small\verb%~%}, 1116{\small\verb%/\%}, {\small\verb%\/%}, and {\small\verb%==>%} has 1117been added to the system. The naming scheme is based on the following 1118atoms: 1119 1120\begin{hol}\begin{alltt} 1121 <\(quant\)> := FORALL | EXISTS 1122 <\(conn\)> := NOT | AND | OR | IMP 1123 [\(dir\)] := LEFT | RIGHT \({\it (optional)}\) 1124\end{alltt}\end{hol} 1125 1126 1127 1128The conversions for moving quantifiers inwards are called: 1129 1130\begin{hol}\begin{alltt} 1131 <\(quant\)>_<\(conn\)>_CONV 1132\end{alltt}\end{hol} 1133 1134\noindent where the quantifier \ml{<$quant$>} is to be moved inwards 1135through \ml{<$conn$>}. 1136 1137The conversions for moving quantifiers outwards are called: 1138 1139\begin{hol}\begin{alltt} 1140 [\(dir\)]_<\(conn\)>_<\(quant\)>_CONV 1141\end{alltt}\end{hol} 1142 1143\noindent where \ml{<$quant$>} is to be moved outwards 1144through \ml{<$conn$>}, and the optional 1145\ml{[$dir$]} identifies which operand (left or right) contains the quantifier. 1146The complete set is: 1147 1148\begin{hol}\begin{verbatim} 1149 NOT_FORALL_CONV |- ~(!x.P) = ?x.~P 1150 NOT_EXISTS_CONV |- ~(?x.P) = !x.~P 1151 EXISTS_NOT_CONV |- (?x.~P) = ~!x.P 1152 FORALL_NOT_CONV |- (!x.~P) = ~?x.P 1153\end{verbatim}\end{hol} 1154 1155\begin{hol}\begin{verbatim} 1156 FORALL_AND_CONV |- (!x. P /\ Q) = (!x.P) /\ (!x.Q) 1157 AND_FORALL_CONV |- (!x.P) /\ (!x.Q) = (!x. P /\ Q) 1158 LEFT_AND_FORALL_CONV |- (!x.P) /\ Q = (!x'. P[x'/x] /\ Q) 1159 RIGHT_AND_FORALL_CONV |- P /\ (!x.Q) = (!x'. P /\ Q[x'/x]) 1160\end{verbatim}\end{hol} 1161 1162\begin{hol}\begin{verbatim} 1163 EXISTS_OR_CONV |- (?x. P \/ Q) = (?x.P) \/ (?x.Q) 1164 OR_EXISTS_CONV |- (?x.P) \/ (?x.Q) = (?x. P \/ Q) 1165 LEFT_OR_EXISTS_CONV |- (?x.P) \/ Q = (?x'. P[x'/x] \/ Q) 1166 RIGHT_OR_EXISTS_CONV |- P \/ (?x.Q) = (?x'. P \/ Q[x'/x]) 1167\end{verbatim}\end{hol} 1168 1169\begin{hol}\begin{verbatim} 1170 FORALL_OR_CONV 1171 |- (!x.P \/ Q) = P \/ !x.Q [x not free in P] 1172 |- (!x.P \/ Q) = (!x.P) \/ Q [x not free in Q] 1173 |- (!x.P \/ Q) = (!x.P) \/ (!x.Q) [x not free in P or Q] 1174\end{verbatim}\end{hol} 1175 1176\begin{hol}\begin{verbatim} 1177 OR_FORALL_CONV 1178 |- (!x.P) \/ (!x.Q) = (!x.P \/ Q) [x not free in P or Q] 1179\end{verbatim}\end{hol} 1180 1181\begin{hol}\begin{verbatim} 1182 LEFT_OR_FORALL_CONV |- (!x.P) \/ Q = !x'. P[x'/x] \/ Q 1183 RIGHT_OR_FORALL_CONV |- P \/ (!x.Q) = !x'. P \/ Q[x'/x] 1184\end{verbatim}\end{hol} 1185 1186\begin{hol}\begin{verbatim} 1187 EXISTS_AND_CONV 1188 |- (?x.P /\ Q) = P /\ ?x.Q [x not free in P] 1189 |- (?x.P /\ Q) = (?x.P) /\ Q [x not free in Q] 1190 |- (?x.P /\ Q) = (?x.P) /\ (?x.Q) [x not free in P or Q] 1191\end{verbatim}\end{hol} 1192 1193\begin{hol}\begin{verbatim} 1194 AND_EXISTS_CONV 1195 |- (?x.P) /\ (?x.Q) = (?x.P /\ Q) [x not free in P or Q] 1196\end{verbatim}\end{hol} 1197 1198\begin{hol}\begin{verbatim} 1199 LEFT_AND_EXISTS_CONV |- (?x.P) /\ Q = ?x'. P[x'/x] /\ Q 1200 RIGHT_AND_EXISTS_CONV |- P /\ (?x.Q) = ?x'. P /\ Q[x'/x] 1201\end{verbatim}\end{hol} 1202 1203\begin{hol}\begin{verbatim} 1204 FORALL_IMP_CONV 1205 |- (!x.P ==> Q) = P ==> !x.Q [x not free in P] 1206 |- (!x.P ==> Q) = (?x.P) ==> Q [x not free in Q] 1207 |- (!x.P ==> Q) = (?x.P) ==> (!x.Q) [x not free in P or Q] 1208\end{verbatim}\end{hol} 1209 1210\begin{hol}\begin{verbatim} 1211 LEFT_IMP_FORALL_CONV |- (!x.P) ==> Q = !x'. P[x/'x] ==> Q 1212 RIGHT_IMP_FORALL_CONV |- P ==> (!x.Q) = !x'. P ==> Q[x'/x] 1213\end{verbatim}\end{hol} 1214 1215\begin{hol}\begin{verbatim} 1216 EXISTS_IMP_CONV 1217 |- (?x.P ==> Q) = P ==> ?x.Q [x not free in P] 1218 |- (?x.P ==> Q) = (!x.P) ==> Q [x not free in Q] 1219 |- (?x.P ==> Q) = (!x.P) ==> (?x.Q) [x not free in P or Q] 1220\end{verbatim}\end{hol} 1221 1222\begin{hol}\begin{verbatim} 1223 LEFT_IMP_EXISTS_CONV |- (?x.P) ==> Q = !x'. P[x/'x] ==> Q 1224 RIGHT_IMP_EXISTS_CONV |- P ==> (?x.Q) = ?x'. P ==> Q[x'/x] 1225\end{verbatim}\end{hol} 1226 1227\section{New built-in theorems}\label{THEOREMS} 1228 1229Quite a few new theorems have been added to \HOL. Some are listed 1230below, others can be found in the libraries and in \ml{contrib}. 1231 1232\subsection{New arithmetical theorems} 1233 1234The built-in theory arithmetic has been augmented with a minimal theory of 1235the functions \ml{MOD} and \ml{DIV} on the natural numbers. The old definitions of 1236\ml{MOD} and \ml{DIV}: 1237 1238\begin{hol}\begin{verbatim} 1239 MOD |- MOD k n = @r. ?q. (k = (q * n) + r) /\ r < n 1240 DIV |- DIV k n = @q. (k = (q * n) + (k MOD n)) 1241\end{verbatim}\end{hol} 1242 1243\noindent have been deleted, and replaced by the constant specification: 1244 1245\begin{hol}\begin{verbatim} 1246 DIVISION |- !n. 0 < n ==> 1247 (!k. (k = ((k DIV n) * n) + (k MOD n)) /\ (k MOD n) < n) 1248\end{verbatim}\end{hol} 1249 1250\noindent the validity of which is justified by the division algorithm: 1251 1252\begin{hol}\begin{verbatim} 1253 DA |- !k n. 0 < n ==> (?r q. (k = (q * n) + r) /\ r < n) 1254\end{verbatim}\end{hol} 1255 1256The following theorems are also available: 1257 1258\begin{hol}\begin{verbatim} 1259 MOD_ONE |- !k. k MOD (SUC 0) = 0 1260 DIV_LESS_EQ |- !n. 0 < n ==> (!k. (k DIV n) <= k) 1261 DIV_UNIQUE |- !n k q. (?r. (k = (q * n) + r) /\ r < n) ==> (k DIV n = q) 1262 MOD_UNIQUE |- !n k r. (?q. (k = (q * n) + r) /\ r < n) ==> (k MOD n = r) 1263 DIV_MULT |- !n r. r < n ==> (!q. ((q * n) + r) DIV n = q) 1264 LESS_MOD |- !n k. k < n ==> (k MOD n = k) 1265 MOD_EQ_0 |- !n. 0 < n ==> (!k. (k * n) MOD n = 0) 1266 ZERO_MOD |- !n. 0 < n ==> (0 MOD n = 0) 1267 MOD_MULT |- !n r. r < n ==> (!q. ((q * n) + r) MOD n = r) 1268 MOD_TIMES |- !n. 0 < n ==> (!q r. ((q * n) + r) MOD n = r MOD n) 1269 MOD_PLUS |- !n. 0 < n ==> 1270 (!j k. ((j MOD n) + (k MOD n)) MOD n = (j + k) MOD n) 1271 MOD_MOD |- !n. 0 < n ==> (!k. (k MOD n) MOD n = k MOD n) 1272\end{verbatim}\end{hol} 1273 1274 1275 1276The following miscellaneous arithmetical theorems 1277are now pre-proved. 1278 1279\begin{hol}\begin{verbatim} 1280 ZERO_LESS_EQ |- !n. 0 <= n 1281 LESS_EQ_MONO |- !n m. (SUC n <= SUC m) = (n <= m) 1282 LESS_OR_EQ_ADD |- !n m. n < m \/ ?p. n = p+m 1283 SUC_NOT |- !n. ~(0 = SUC n) 1284 SUB_MONO_EQ |- !n m. (SUC n) - (SUC m) = n - m 1285 SUB_PLUS |- !a b c. a - (b + c) = (a - b) - c 1286 INV_PRE_LESS |- !m n. 0 < m /\ 0 < n ==> ((PRE m)<(PRE n) = m<n) 1287 INV_PRE_LESS_EQ |- !n. 0 < n ==> !m. ((PRE m)<=(PRE n) = m<=n) 1288 SUB_LESS_EQ |- !n m. (n - m) <= n 1289 SUB_EQ_EQ_0 |- !m n. (m - n = m) = (m = 0) \/ (n = 0) 1290 SUB_LESS_0 |- !n m. m < n = 0 < (n - m) 1291 SUB_LESS_OR |- !m n. n < m ==> n <= (m - 1) 1292 LESS_SUB_ADD_LESS |- !n m i. i < (n - m) ==> (i + m) < n 1293 TIMES2 |- !n. 2 * n = n + n 1294 LESS_MULT_MONO |- !m i n. ((SUC n) * m) < ((SUC n) * i) = m < i 1295 MULT_MONO_EQ |- !m i n. ((SUC n) * m = (SUC n) * i) = (m = i) 1296 ADD_SUB |- !a c. (a + c) - c = a 1297 LESS_EQ_ADD_SUB |- !c b. c <= b ==> (!a. (a + b) - c = a + (b - c)) 1298 SUB_EQUAL_0 |- !c. c - c = 0 1299 LESS_EQ_SUB_LESS |- !a b. b <= a ==> (!c. (a - b) < c = a < (b + c)) 1300 NOT_SUC_LESS_EQ |- !n m. ~(SUC n) <= m = m <= n 1301 SUB_SUB |- !b c. c <= b ==> (!a. a - (b - c) = (a + c) - b) 1302 LESS_IMP_LESS_ADD |- !n m. n < m ==> (!p. n < (m + p)) 1303 LESS_EQ_IMP_LESS_SUC |- !n m. n <= m ==> n < (SUC m) 1304\end{verbatim}\end{hol} 1305\begin{hol}\begin{verbatim} 1306 SUB_LESS_EQ_ADD |- !m p. m <= p ==> (!n. (p - m) <= n = p <= (m + n)) 1307 SUB_CANCEL |- !p n m. n <= p /\ m <= p ==> 1308 ((p - n = p - m) = (n = m)) 1309 CANCEL_SUB |- !p n m. p <= n /\ p <= m ==> 1310 ((n - p = m - p) = (n = m)) 1311 NOT_EXP_0 |- !m n. ~((SUC n) EXP m = 0) 1312 ZERO_LESS_EXP |- !m n. 0 < ((SUC n) EXP m) 1313 ODD_OR_EVEN |- !n. ?m. (n = (SUC(SUC 0)) * m) \/ 1314 (n = ((SUC(SUC 0)) * m) + 1) 1315 LESS_EXP_SUC_MONO |- !n m. 1316 ((SUC(SUC m)) EXP n)<((SUC(SUC m)) EXP (SUC n)) 1317 LESS_EQUAL_ANTISYM |- !n m. n <= m /\ m <= n ==> (n = m) 1318 LESS_ADD_SUC |- !m n. m < (m + (SUC n)) 1319 1320\end{verbatim}\end{hol} 1321 1322 1323\subsection{New theorems about lists} 1324 1325\begin{hol}\begin{verbatim} 1326 LIST_NOT_EQ: |- !l1 l2. ~(l1 = l2) ==> (!h1 h2. ~(CONS h1 l1 = CONS h2 l2)) 1327 NOT_EQ_LIST: |- !h1 h2. ~(h1 = h2) ==> (!l1 l2. ~(CONS h1 l1 = CONS h2 l2)) 1328 EQ_LIST |- !h1 h2. (h1 = h2) ==> 1329 (!l1 l2. (l1 = l2) ==> (CONS h1 l1 = CONS h2 l2)) 1330\end{verbatim}\end{hol} 1331 1332\subsection{New propositional theorems} 1333 1334\begin{hol}\begin{verbatim} 1335 LEFT_AND_OVER_OR |- !t1 t2 t3. t1 /\ (t2 \/ t3) = t1 /\ t2 \/ t1 /\ t3 1336 RIGHT_AND_OVER_OR |- !t1 t2 t3. (t2 \/ t3) /\ t1 = t2 /\ t1 \/ t3 /\ t1 1337 LEFT_OR_OVER_AND |- !t1 t2 t3. t1 \/ t2 /\ t3 = (t1 \/ t2) /\ (t1 \/ t3) 1338 RIGHT_OR_OVER_AND |- !t1 t2 t3. t2 /\ t3 \/ t1 = (t2 \/ t1) /\ (t3 \/ t1) 1339\end{verbatim}\end{hol} 1340\begin{hol}\begin{verbatim} 1341 OR_IMP_THM |- !t1 t2. (t1 = t2 \/ t1) = t2 ==> t1 1342 NOT_IMP |- !t1 t2. ~(t1 ==> t2) = t1 /\ ~t2 1343 COND_ID |- !b t. (b => t | t) = t 1344 DISJ_ASSOC |- !t1 t2 t3. t1 \/ t2 \/ t3 = (t1 \/ t2) \/ t3 1345\end{verbatim}\end{hol} 1346 1347 1348\section{Additions and deletions}\label{adddel} 1349 1350The \ML\ identifiers that have been added and deleted in Version 2.0 1351are listed here. The reasons for the changes are given in the files: 1352 1353\begin{hol}\begin{verbatim} 1354 hol/Version.2.0 1355 hol/Versions/Version.1.12 1356 hol/Versions/Versions.pre.1.12 1357\end{verbatim}\end{hol} 1358 1359\noindent The file \ml{Version.$m$.$n$} (in the sources) documents \HOL\ 1360Version \ml{$m$.$n$} and may contain details not in \DESCRIPTION\ or 1361\REFERENCE. 1362 1363\subsection{Additions} 1364 1365Here is a list of all the new functions in Version 2.0, the ones that 1366are not described in this appendix or earlier in \DESCRIPTION\ should be 1367documented in \REFERENCE. 1368 1369\begin{hol}\begin{verbatim} 1370 get_const_type parity is_type 1371 mk_let dest_let is_let 1372 bndvar body is_axiom 1373\end{verbatim}\end{hol} 1374\begin{hol}\begin{verbatim} 1375 mk_cons dest_cons is_cons 1376 mk_list dest_list is_list 1377 list_mk_pair strip_mk_pair 1378\end{verbatim}\end{hol} 1379\begin{hol}\begin{verbatim} 1380 ancestors ancestry 1381\end{verbatim}\end{hol} 1382\begin{hol}\begin{verbatim} 1383 prove_rep_fn_one_one prove_rep_fn_onto 1384 prove_abs_fn_one_one prove_abs_fn_onto 1385\end{verbatim}\end{hol} 1386\begin{hol}\begin{verbatim} 1387 define_finite_set_syntax define_set_abstraction_syntax 1388 associate_restriction 1389\end{verbatim}\end{hol} 1390\begin{hol}\begin{verbatim} 1391 X_FUN_EQ_CONV COND_CONV PAIRED_BETA_CONV 1392 BOOL_EQ_CONV ADD_CONV LENGTH_CONV 1393 list_EQ_CONV num_EQ_CONV let_CONV 1394 EXISTS_LEAST_CONV X_SKOLEM_CONV SKOLEM_CONV 1395 NOT_FORALL_CONV NOT_EXISTS_CONV 1396 EXISTS_NOT_CONV FORALL_NOT_CONV 1397 FORALL_AND_CONV AND_FORALL_CONV 1398 LEFT_AND_FORALL_CONV RIGHT_AND_FORALL_CONV 1399 EXISTS_OR_CONV OR_EXISTS_CONV 1400 LEFT_OR_EXISTS_CONV RIGHT_OR_EXISTS_CONV 1401 FORALL_OR_CONV OR_FORALL_CONV 1402 LEFT_OR_FORALL_CONV RIGHT_OR_FORALL_CONV 1403 EXISTS_AND_CONV AND_EXISTS_CONV 1404 LEFT_AND_EXISTS_CONV RIGHT_AND_EXISTS_CONV 1405 FORALL_IMP_CONV EXISTS_IMP_CONV 1406 LEFT_IMP_FORALL_CONV RIGHT_IMP_FORALL_CONV 1407 LEFT_IMP_EXISTS_CONV RIGHT_IMP_EXISTS_CONV 1408\end{verbatim}\end{hol} 1409\begin{hol}\begin{verbatim} 1410 last butlast 1411\end{verbatim}\end{hol} 1412\begin{hol}\begin{verbatim} 1413 getenv library_pathname is_ml_infix 1414 set_help_search_path help_search_path 1415\end{verbatim}\end{hol} 1416\begin{hol}\begin{verbatim} 1417 EQF_INTRO ISPEC ISPECL 1418 EQF_ELIM EXISTENCE IMP_CONJ 1419 EXIST_IMP 1420\end{verbatim}\end{hol} 1421\begin{hol}\begin{verbatim} 1422 REPEAT_GTCL AP_THM_TAC 1423\end{verbatim}\end{hol} 1424 1425 1426\subsection{Deletions} 1427 1428The large number of deletions listed below are mostly the result of a ``spring 1429cleaning'' of the \HOL\ sources. It is hoped that nothing in use has been 1430deleted by mistake---please let us know if you want anything back. 1431 1432\begin{hol}\begin{verbatim} 1433 abbrev_ty_def EXPAND_TY_DEFINITION 1434 pp_constants pp_axioms pp_theorem 1435 pp_delete_theorem pp_theorems 1436 new_pp_theory close_pp_theory 1437 load_pp_theory extend_pp_theory new_pp_predicate 1438 mk_quant mk_bool_comb space ascii_ize 1439 dest_quant dest_bool_comb truth 1440 mk_iff dest_iff is_iff 1441\end{verbatim}\end{hol} 1442\begin{hol}\begin{verbatim} 1443 TOTALLY_AD_HOC_LEMMA 1444\end{verbatim}\end{hol} 1445\begin{hol}\begin{verbatim} 1446 AND_CLAUSE1 AND_CLAUSE2 AND_CLAUSE3 1447 AND_CLAUSE4 AND_CLAUSE5 1448 OR_CLAUSE1 OR_CLAUSE2 OR_CLAUSE3 1449 OR_CLAUSE4 OR_CLAUSE5 1450 IMP_CLAUSE1 IMP_CLAUSE2 IMP_CLAUSE3 1451 IMP_CLAUSE4 IMP_CLAUSE5 1452 EQ_CLAUSE1 EQ_CLAUSE2 EQ_CLAUSE3 1453 EQ_CLAUSE4 1454 COND_CLAUSE1 COND_CLAUSE2 1455\end{verbatim}\end{hol} 1456\begin{hol}\begin{verbatim} 1457 paired_mem paired_tryfind paired_aconv_term 1458 paired_map paired_filter paired_subst_term 1459 paired_forall paired_mapfilter paired_subst_occs_term 1460 paired_exists paired_rev_itlist paired_term_freein_term 1461 paired_find paired_term_match paired_type_in_term 1462 paired_type_in_type paired_set_left paired_axiom 1463 paired_inst_type paired_set_right paired_inst_term 1464 paired_cons paired_variant paired_eq 1465 paired_form_match paired_aconv_form paired_subst_form 1466 paired_subst_occs_form paired_term_freein_form paired_term_freein_form 1467 paired_type_in_form paired_inst_form 1468\end{verbatim}\end{hol} 1469\begin{hol}\begin{verbatim} 1470 new_curried_infix curried_infixes paired_infixes 1471\end{verbatim}\end{hol} 1472\begin{hol}\begin{verbatim} 1473 rename_form rename_term print_form 1474 mk_inequiv dest_inequiv is_inequiv 1475 is_equiv dest_equiv mk_equiv 1476 gen_all new_predicate 1477 make_tuple list_variant nil 1478 diagonal eqfst eqsnd 1479 flip mk_tuple dest_tuple 1480\end{verbatim}\end{hol} 1481\begin{hol}\begin{verbatim} 1482 OLD_IMP_RES_TAC HOL_IMP_RES_THEN HOL_STRIP_THM_THEN 1483 OLD_RES_TAC HOL_RES_THEN HOL_STRIP_ASSUME_TAC 1484 OLD_IMP_RES_THEN RES_CANON_FUN HOL_MATCH_MP 1485 OLD_RES_THEN MULTI_MP HOL_RESOLVE_THEN 1486 MP_CHAIN REDEPTH_CHAIN SUB_CHAIN 1487 ONCE_DEPTH_CHAIN DSPEC DSPECL 1488\end{verbatim}\end{hol} 1489\begin{hol}\begin{verbatim} 1490 print_tok_ty print_tok_thm apply_type_op 1491 print_all_tok_thm 1492 int_of_tok (replaced by int_of_string) 1493 tok_of_int (replaced by string_of_int) 1494 int_to_term term_to_int 1495 form_class form_frees 1496 form_vars form_tyvars 1497 term_frees (equivalent to frees) 1498 term_vars (equivalent to vars) 1499 term_tyvars (equivalent to tyvars) 1500 term_class 1501\end{verbatim}\end{hol} 1502\begin{hol}\begin{verbatim} 1503 seg (now in library `eval`) 1504 word_seg (now in library `eval`) 1505 word_el (now in library `eval`) 1506 truncate (now in library `eval`) 1507 upto 1508 keyword 1509\end{verbatim}\end{hol} 1510\begin{hol}\begin{verbatim} 1511 LESS_OR (replaced by LESS_SUC_EQ) 1512 GSUBS 1513\end{verbatim}\end{hol} 1514\begin{hol}\begin{verbatim} 1515 DEPTH_EXISTS_CONV DISJS_CONV BINOP_CONV 1516 ANTE_FORALL_CONV 1517 BOOL_EQ_CONV (renamed bool_EQ_CONV) 1518 MOVE_EXISTS_OUT_CONV (replaced by RIGHT_AND_EXISTS_CONV) 1519\end{verbatim}\end{hol} 1520\begin{hol}\begin{verbatim} 1521 is_string is_int is_cons 1522 obj_of_string obj_of_int cons 1523 string_of_obj int_of_obj 1524 left right 1525 set_left set_right 1526 eq lisp_eval 1527 make_set (renamed to setify) 1528 thenf orelsef all_fun 1529 no_fun first_fun every_fun 1530 repeatf mapshape 1531 \end{verbatim}\end{hol} 1532\begin{hol}\begin{verbatim} 1533 BETA_RED_CONV LENGTH_MAP_CONV make_definitions 1534 BINDER_CONV LEN_SIMP_CONV mk_def 1535 CHOOSE_RULE LHS_CONV mk_defs 1536 COND_F MAP_ELIM mk_fn_ty 1537 COND_T MOVE_FORALL_IN mk_fun_test 1538 CONJS_CONV OR_ELIM_CONV mk_funct 1539 DEPTH_FORALL_CONV OR_IMP mk_injs 1540 DO_ASM PROJ mk_new_vars 1541 ELIM_ANTE_EQNS_CONV RM_LEN_CONV mk_subset_pred 1542 ELIM_ANTE_EQN_CONV SIMP_CONV mk_sum_ty 1543 ELIM_LEN_CONV SIMP_ISL1 mk_test 1544 ELIM_MAP_CONV SIMP_ISL2 mk_tl_spec 1545 EQ_ANTE_ELIM SIMP_RHS mk_tuple_ty 1546 EXISTS_RULE TEST_CONV pars_ty 1547\end{verbatim}\end{hol} 1548\begin{hol}\begin{verbatim} 1549 E_I_CONV clean parse_type 1550 FN_BETA cleanup proj 1551 FN_CASES_SIMP do_abs prove_existence_thm 1552 FN_CASE_SIMP extract_list strip_cases 1553 FORALL_AND_CONV extract_tuple strip_tok 1554 FORALL_CONJ_CONV gen_names strip_val 1555 FOUR_BINDER_CONV infix_ty strip_vty_tok 1556 FST_SND_SIMP is_char sub_conv 1557 HD_TL_SIMP list_gen_alpha ty_case 1558 variant_tyvar rotate_left rotate_right 1559 derive_existence_thm instantiate_existence_thm 1560 mk_fn closeup 1561\end{verbatim}\end{hol} 1562\begin{hol}\begin{verbatim} 1563 CLOSE_UP save_open_thm 1564 HOLdir set_hol_lib_dir 1565 load_from_lib loadt_from_lib loadf_from_lib 1566 loadx theories_dir_pathname 1567\end{verbatim}\end{hol} 1568\begin{hol}\begin{verbatim} 1569 IFF_DEF I FF_EQ_THM1 IFF_EQ_THM2 1570 IFF_EQ IFF_EQ_RULE CONJ_IFF 1571 IFF_CONJ IFF_THEN2 IFF_THEN 1572 IFF_TAC EXISTS_REFL_TAC 1573\end{verbatim}\end{hol} 1574\begin{hol}\begin{verbatim} 1575 define_new_type_isomorphisms (renamed define_new_type_bijections) 1576\end{verbatim}\end{hol} 1577\begin{hol}\begin{verbatim} 1578 mk_rewrites mk_rewritesl REWRITE_CONV 1579\end{verbatim}\end{hol} 1580 1581 1582