## File: entries.tex

package info (click to toggle)
hol88 2.02.19940316-35
 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128 \chapter{ML Functions in the string Library}\input{entries-intro}\DOC{ascii\_EQ\_CONV} \TYPE {\small\verb%ascii_EQ_CONV : conv%}\egroup \SYNOPSIS Decision-procedure for equality of ascii character constants. \DESCRIBE The conversion {\small\verb%ascii_EQ_CONV%} implements a decision procedure for the equality of ascii character constants built up from boolean constants {\small\verb%T%} and {\small\verb%F%} using the constructor {\small\verb%ASCII%}. The conversion expects its term argument to be an equation of the form: {\par\samepage\setseps\small \begin{verbatim} "ASCII a1 a2 a3 a4 a5 a6 a7 a8 = ASCII b1 b2 b3 b4 b5 b6 b7 b8" \end{verbatim} } \noindent where each of {\small\verb%a1%}, ..., {\small\verb%a8%}, {\small\verb%b1%}, ..., {\small\verb%b8%} is either the constant {\small\verb%T%} or the constant {\small\verb%F%}. Given such a term, the conversion returns: {\par\samepage\setseps\small \begin{verbatim} |- (ASCII a1 a2 a3 a4 a5 a6 a7 a8 = ASCII b1 b2 b3 b4 b5 b6 b7 b8) = T \end{verbatim} } \noindent if {\small\verb%ai%} is identical to {\small\verb%bi%} for i from 1 to 8. Otherwise, the conversion returns: {\par\samepage\setseps\small \begin{verbatim} |- (ASCII a1 a2 a3 a4 a5 a6 a7 a8 = ASCII b1 b2 b3 b4 b5 b6 b7 b8) = F \end{verbatim} } \FAILURE Fails if applied to a term that is not of the form shown above. \SEEALSO string_EQ_CONV. \ENDDOC \DOC{load\_string} \TYPE {\small\verb%load_string : (void -> void)%}\egroup \SYNOPSIS Loads ML functions in the string library and sets up autoloading of theorems in the library. \DESCRIBE If the user is not in draft mode, or the current theory is not an ancestor of the library theory {\small\verb%string%}, then the contents of the string library cannot immediately be made available when the library is loaded, since the theory {\small\verb%string%} can neither be made a parent of the current theory nor loaded using {\small\verb%load_theory%}. In this case, the library load sequence defines the function {\small\verb%load_string%}. Calling this function when the library theory {\small\verb%string%} is an ancestor of the current theory completes the library load sequence for the string library, making available the ML functions in the library and activating autoloading of theorems. \FAILURE Fails if the theory {\small\verb%string%} is not an ancestor of the current theory. \ENDDOC \DOC{string\_CONV} \TYPE {\small\verb%string_CONV : conv%}\egroup \SYNOPSIS Axiom-scheme for character string constants. \DESCRIBE The conversion {\small\verb%string_CONV%} expects its term argument to be a non-empty ascii character string constant (for example: {\small\verb%"a"%}, {\small\verb%"b"%}, {\small\verb%"abc"%}). Given such a term, for example the term {\small\verb%"abc"%}, the conversion returns a theorem that defines this constant in terms of a shorter string: {\par\samepage\setseps\small \begin{verbatim} |- abc = STRING(ASCII F T T F F F F T)bc \end{verbatim} } \noindent where {\small\verb%(ASCII F T T F F F F T)%} is the ascii character code for the first character in the supplied string (in this case {\small\verb%a%}). \FAILURE Fails if applied to a term that is not of the form shown above or if applied to the empty string {\small\verb%""%}. \SEEALSO string_EQ_CONV. \ENDDOC \DOC{string\_EQ\_CONV} \TYPE {\small\verb%string_EQ_CONV : conv%}\egroup \SYNOPSIS Decision-procedure for equality of string constants. \DESCRIBE The conversion {\small\verb%string_EQ_CONV%} expects its term argument to be an equation between character string constants (for example: {\small\verb%"a"%}, {\small\verb%"b"%}, {\small\verb%"abc"%}, etc). Given such a term, the conversion {\small\verb%string_EQ_CONV%} returns: {\par\samepage\setseps\small \begin{verbatim} |- (lhs = rhs) = T \end{verbatim} } \noindent if {\small\verb%lhs%} and {\small\verb%rhs%} are identical character strings. Otherwise, the conversion returns: {\par\samepage\setseps\small \begin{verbatim} |- (lhs = rhs) = F \end{verbatim} } \FAILURE Fails if applied to a term that is not of the form specified above. \EXAMPLE {\par\samepage\setseps\small \begin{verbatim} #string_EQ_CONV "aax = aay";; |- (aax = aay) = F \end{verbatim} } \SEEALSO ascii_EQ_CONV. \ENDDOC