1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
\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
|
