Manual/Description/version2.tex

12 Version 2.0 is primarily a rationalization of Version 1.11. Relics of
17 The top-level directory of the \HOL\ distribution sources has been
18 reorganized.  The details are in Chapter 1 of \TUTORIAL\ (`Getting and
21 community.  The aim of this directory is to make it easy for the
23 other material which may be of general interest. Unlike the library,
26 Two major revisions of the theorem-proving tools in Version 2.0 are the
27 complete reimplementations, by Tom Melham, of (i) the resolution rules and
36 tactics have been used that depend on the positions of assumptions in
43 robust. A number of identifier names have changed and its internal
48 Four libraries from Version 1.11 of HOL have been temporarily withdrawn,
56 \noindent The first three are difficult to rebuild because of changes to
58 assumptions of goals appear.  The fourth library uses the
68 The restricted quantification notation allows terms of
72 if $x:\alpha$ then $p$ can be any term of type $\alpha\fun\bool$; this
73 denotes the quantification of $x$ over those values
78 {\small\verb%!%}, {\small\verb%?%} and {\small\verb%@%}.  This provides a method of
83 `type' of $n$-bit words. Experiments are needed to establish how satisfactory
89 suitable definition of the constant $\con{Sum}$.
94 supports set abstraction notation of the form
98 onto theories of lists, bags etc.), although they were initially
110 of methodologies for embedding application-specific languages in \HOL\
111 is a major topic of research at Cambridge.
121 are likely to be of most general use are described. Section~\ref{adddel}
128 The top-level of the \HOL\ distribution directory now contains:
133 as for the \REFERENCE\ part of the manual.
141 the responsibility of the library's load-file to do this, if desired).
171 \section{Location of libraries}
182 value when the system is built, should be the absolute pathname of the \HOL\
206 \noindent This will make the help files of the library \ml{lib}
224 previous one as result. The effect of
232 with the top level of \ML\ being the standard output.
239 \noindent will cause the help file to be printed instead of being displayed and
272 Meeting and implements a method of simulating subtypes and dependent
295 semantics of particular restricted abstractions are.
327 of a binder and \ml{RES\_}$B$ is the name of a suitable constant (which
393 The variable \ml{x} in the definitions of the constants
417 Here is an example of a user-defined restriction:
450 The 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
452 is the set of all $t$s such that $p$. These interpretations are predefined for
478 is not the name of a constant.
521 of the paired abstraction is an unspecified function of the structure
522 of $t$ (it is approximately left to right). Failure if $c$ is not the
523 name of a constant.
551 bijection used in the definition of the type operator \ml{set}).
577 Note that the precedence of comma is increased in the contexts
598 In previous versions of the system, there were three libraries dealing with
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).
607 Each of these libraries is useful for certain applications, and all three will
608 therefore continue to be supported.  To better reflect the contents of these
624 \item  \ml{\{$x$|$P[x]$\}}      denotes the set of all \ml{$x$} such that
627 \item \ml{\{$t[x]$|$P[x]$\}}   denotes the set of all \ml{$t[x]$}
633 Proof support is supplied for this notation in the form of a conversion
640 \noindent which implements the axiom of specification for generalized set
643 \ml{SET\_SPEC\_CONV} accepts two types of input.
682 proving properties of finite sets.
700 This is intended to help users update proof scripts based on the old version of
714 languages into \HOL\ terms. See the documentation of the library for
726 of the block, the second argument is the terminator and the third
727 argument is the name of a function having a type which is an instance
728 of {\small\verb%string->*%}. The effect of
777 The typechecker for \HOL\ quotations contains a number of arbitrary
785 The \ML\ abstract type {\small\verb%preterm%} represents the parse trees of \HOL\
786 terms. A typechecker is a function of type {\small\verb%preterm->term%}. If the flag
792 and then wraps a call of \ml{preterm\_handler}
794 in \HOL\ logic!user programmed} Other uses of preterms are possible, for example
797 The definition of the \ML\ type {\small\verb%preterm%} is:
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}\)
852 different definition of the function
855 not compromise the logical soundness of \HOL.
863 Many new conversions have been added to the system. Only those likely to be of
877 generalized beta-conversion of tupled lambda abstractions applied to
913 where $s$ is the numeral denoting the sum of $n$ and $m$.  For example:
929 A new conversion has been added for deciding equality of natural number
962 \ml{LENGTH\_CONV}: computes the length of a list.
976 equality of two lists, given
977 a conversion for deciding the equality of elements.
1003 \index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!simplification of}
1024 \noindent The \ml{$v_i$}'s can take any one of the following forms:
1034 rewritten in the body of the {\tt let}-term.
1060 Two conversions are provided for a higher-order version of
1088 variable \ml{$f$} of the appropriate type in the input term. For example:
1096 uses a primed variant of the name of the existentially quantified variable
1097 as the name of the skolem function it introduces.  For example:
1114 A complete and systematically-named set of conversions for moving quantifiers
1234 The built-in theory arithmetic has been augmented with a minimal theory of
1235 the functions \ml{MOD} and \ml{DIV} on the natural numbers.  The old definitions of
1250 \noindent the validity of which is justified by the division algorithm:
1365 Here is a list of all the new functions in Version 2.0, the ones that
1428 The large number of deletions listed below are mostly the result of a ``spring
1429 cleaning'' of the \HOL\ sources. It is hoped that nothing in use has been