wenzelm@11648
|
1 |
%
|
wenzelm@11648
|
2 |
\begin{isabellebody}%
|
wenzelm@11648
|
3 |
\def\isabellecontext{Documents}%
|
wenzelm@11866
|
4 |
\isamarkupfalse%
|
wenzelm@12627
|
5 |
%
|
wenzelm@12647
|
6 |
\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
|
wenzelm@12627
|
7 |
}
|
wenzelm@12627
|
8 |
\isamarkuptrue%
|
wenzelm@12627
|
9 |
%
|
wenzelm@12627
|
10 |
\begin{isamarkuptext}%
|
wenzelm@12627
|
11 |
Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate infrastructure
|
wenzelm@12644
|
12 |
for concrete syntax is that of general \bfindex{mixfix annotations}.
|
wenzelm@12644
|
13 |
Associated with any kind of name and type declaration, mixfixes give
|
wenzelm@12644
|
14 |
rise both to grammar productions for the parser and output templates
|
wenzelm@12644
|
15 |
for the pretty printer.
|
wenzelm@12627
|
16 |
|
wenzelm@12627
|
17 |
In full generality, the whole affair of parser and pretty printer
|
wenzelm@12627
|
18 |
configuration is rather subtle. Any syntax specifications given by
|
wenzelm@12627
|
19 |
end-users need to interact properly with the existing setup of
|
wenzelm@12627
|
20 |
Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further
|
wenzelm@12627
|
21 |
details. It is particularly important to get the precedence of new
|
wenzelm@12627
|
22 |
syntactic constructs right, avoiding ambiguities with existing
|
wenzelm@12627
|
23 |
elements.
|
wenzelm@12627
|
24 |
|
wenzelm@12627
|
25 |
\medskip Subsequently we introduce a few simple declaration forms
|
wenzelm@12627
|
26 |
that already cover the most common situations fairly well.%
|
wenzelm@12627
|
27 |
\end{isamarkuptext}%
|
wenzelm@12627
|
28 |
\isamarkuptrue%
|
wenzelm@12627
|
29 |
%
|
wenzelm@12647
|
30 |
\isamarkupsubsection{Infix Annotations%
|
wenzelm@12627
|
31 |
}
|
wenzelm@12627
|
32 |
\isamarkuptrue%
|
wenzelm@12627
|
33 |
%
|
wenzelm@12627
|
34 |
\begin{isamarkuptext}%
|
wenzelm@12627
|
35 |
Syntax annotations may be included wherever constants are declared
|
wenzelm@12627
|
36 |
directly or indirectly, including \isacommand{consts},
|
wenzelm@12627
|
37 |
\isacommand{constdefs}, or \isacommand{datatype} (for the
|
wenzelm@12627
|
38 |
constructor operations). Type-constructors may be annotated as
|
wenzelm@12627
|
39 |
well, although this is less frequently encountered in practice
|
wenzelm@12627
|
40 |
(\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
|
wenzelm@12627
|
41 |
|
wenzelm@12644
|
42 |
Infix declarations\index{infix annotations} provide a useful special
|
wenzelm@12644
|
43 |
case of mixfixes, where users need not care about the full details
|
wenzelm@12644
|
44 |
of priorities, nesting, spacing, etc. The subsequent example of the
|
wenzelm@12644
|
45 |
exclusive-or operation on boolean values illustrates typical infix
|
wenzelm@12644
|
46 |
declarations.%
|
wenzelm@12627
|
47 |
\end{isamarkuptext}%
|
wenzelm@12627
|
48 |
\isamarkuptrue%
|
wenzelm@12627
|
49 |
\isacommand{constdefs}\isanewline
|
wenzelm@12627
|
50 |
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
|
wenzelm@12627
|
51 |
\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
wenzelm@12627
|
52 |
%
|
wenzelm@12627
|
53 |
\begin{isamarkuptext}%
|
wenzelm@12627
|
54 |
Any curried function with at least two arguments may be associated
|
wenzelm@12627
|
55 |
with infix syntax: \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to
|
wenzelm@12627
|
56 |
the same expression internally. In partial applications with less
|
wenzelm@12627
|
57 |
than two operands there is a special notation with \isa{op} prefix:
|
wenzelm@12627
|
58 |
\isa{xor} without arguments is represented as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}};
|
wenzelm@12627
|
59 |
combined with plain prefix application this turns \isa{xor\ A}
|
wenzelm@12627
|
60 |
into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
|
wenzelm@12627
|
61 |
|
wenzelm@12627
|
62 |
\medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above declaration
|
wenzelm@12627
|
63 |
refers to the bit of concrete syntax to represent the operator,
|
wenzelm@12627
|
64 |
while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the whole
|
wenzelm@12627
|
65 |
construct.
|
wenzelm@12627
|
66 |
|
wenzelm@12627
|
67 |
As it happens, Isabelle/HOL already spends many popular combinations
|
wenzelm@12627
|
68 |
of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
|
wenzelm@12627
|
69 |
\isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present
|
wenzelm@12627
|
70 |
\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current
|
wenzelm@12627
|
71 |
arrangement of inner syntax may be inspected via
|
wenzelm@12627
|
72 |
\commdx{print\protect\_syntax}, albeit its output is enormous.
|
wenzelm@12627
|
73 |
|
wenzelm@12627
|
74 |
Operator precedence also needs some special considerations. The
|
wenzelm@12627
|
75 |
admissible range is 0--1000. Very low or high priorities are
|
wenzelm@12627
|
76 |
basically reserved for the meta-logic. Syntax of Isabelle/HOL
|
wenzelm@12627
|
77 |
mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
|
wenzelm@12627
|
78 |
centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common
|
wenzelm@12627
|
79 |
HOL forms, or use the mostly unused range 100--900.
|
wenzelm@12627
|
80 |
|
wenzelm@12627
|
81 |
\medskip The keyword \isakeyword{infixl} specifies an operator that
|
wenzelm@12627
|
82 |
is nested to the \emph{left}: in iterated applications the more
|
wenzelm@12627
|
83 |
complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly,
|
wenzelm@12635
|
84 |
\isakeyword{infixr} refers to nesting to the \emph{right}, reading
|
wenzelm@12635
|
85 |
\isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In contrast,
|
wenzelm@12635
|
86 |
a \emph{non-oriented} declaration via \isakeyword{infix} would
|
wenzelm@12635
|
87 |
always demand explicit parentheses.
|
wenzelm@12647
|
88 |
|
wenzelm@12627
|
89 |
Many binary operations observe the associative law, so the exact
|
wenzelm@12627
|
90 |
grouping does not matter. Nevertheless, formal statements need be
|
wenzelm@12627
|
91 |
given in a particular format, associativity needs to be treated
|
wenzelm@12627
|
92 |
explicitly within the logic. Exclusive-or is happens to be
|
wenzelm@12627
|
93 |
associative, as shown below.%
|
wenzelm@12627
|
94 |
\end{isamarkuptext}%
|
wenzelm@12627
|
95 |
\isamarkuptrue%
|
wenzelm@12627
|
96 |
\isacommand{lemma}\ xor{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}{\isachardoublequote}\isanewline
|
wenzelm@12627
|
97 |
\ \ \isamarkupfalse%
|
wenzelm@12627
|
98 |
\isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
|
wenzelm@12627
|
99 |
%
|
wenzelm@12627
|
100 |
\begin{isamarkuptext}%
|
wenzelm@12627
|
101 |
Such rules may be used in simplification to regroup nested
|
wenzelm@12627
|
102 |
expressions as required. Note that the system would actually print
|
wenzelm@12627
|
103 |
the above statement as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}
|
wenzelm@12627
|
104 |
(due to nesting to the left). We have preferred to give the fully
|
wenzelm@12635
|
105 |
parenthesized form in the text for clarity. Only in rare situations
|
wenzelm@12635
|
106 |
one may consider to force parentheses by use of non-oriented infix
|
wenzelm@12635
|
107 |
syntax; equality would probably be a typical candidate.%
|
wenzelm@12627
|
108 |
\end{isamarkuptext}%
|
wenzelm@12627
|
109 |
\isamarkuptrue%
|
wenzelm@12635
|
110 |
%
|
wenzelm@12647
|
111 |
\isamarkupsubsection{Mathematical Symbols \label{sec:thy-present-symbols}%
|
wenzelm@12635
|
112 |
}
|
wenzelm@12627
|
113 |
\isamarkuptrue%
|
wenzelm@12635
|
114 |
%
|
wenzelm@12635
|
115 |
\begin{isamarkuptext}%
|
wenzelm@12635
|
116 |
Concrete syntax based on plain ASCII characters has its inherent
|
wenzelm@12635
|
117 |
limitations. Rich mathematical notation demands a larger repertoire
|
wenzelm@12635
|
118 |
of symbols. Several standards of extended character sets have been
|
wenzelm@12635
|
119 |
proposed over decades, but none has become universally available so
|
wenzelm@12635
|
120 |
far, not even Unicode\index{Unicode}.
|
wenzelm@12635
|
121 |
|
wenzelm@12644
|
122 |
Isabelle supports a generic notion of \bfindex{symbols} as the
|
wenzelm@12644
|
123 |
smallest entities of source text, without referring to internal
|
wenzelm@12644
|
124 |
encodings. Such ``generalized characters'' may be of one of the
|
wenzelm@12644
|
125 |
following three kinds:
|
wenzelm@12635
|
126 |
|
wenzelm@12635
|
127 |
\begin{enumerate}
|
wenzelm@12635
|
128 |
|
wenzelm@12635
|
129 |
\item Traditional 7-bit ASCII characters.
|
wenzelm@12635
|
130 |
|
wenzelm@12635
|
131 |
\item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
|
wenzelm@12635
|
132 |
\verb,\\,\verb,<,$ident$\verb,>,).
|
wenzelm@12635
|
133 |
|
wenzelm@12635
|
134 |
\item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
|
wenzelm@12635
|
135 |
\verb,\\,\verb,<^,$ident$\verb,>,).
|
wenzelm@12635
|
136 |
|
wenzelm@12635
|
137 |
\end{enumerate}
|
wenzelm@12635
|
138 |
|
wenzelm@12635
|
139 |
Here $ident$ may be any identifier according to the usual Isabelle
|
wenzelm@12635
|
140 |
conventions. This results in an infinite store of symbols, whose
|
wenzelm@12635
|
141 |
interpretation is left to further front-end tools. For example, the
|
wenzelm@12635
|
142 |
\verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
|
wenzelm@12635
|
143 |
$\forall$ --- both by the user-interface of Proof~General + X-Symbol
|
wenzelm@12635
|
144 |
and the Isabelle document processor (see \S\ref{FIXME}).
|
wenzelm@12635
|
145 |
|
wenzelm@12635
|
146 |
A list of standard Isabelle symbols is given in
|
wenzelm@12635
|
147 |
\cite[appendix~A]{isabelle-sys}. Users may introduce their own
|
wenzelm@12635
|
148 |
interpretation of further symbols by configuring the appropriate
|
wenzelm@12635
|
149 |
front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
|
wenzelm@12635
|
150 |
macros for document preparation. There are also a few predefined
|
wenzelm@12635
|
151 |
control symbols, such as \verb,\,\verb,<^sub>, and
|
wenzelm@12635
|
152 |
\verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
|
wenzelm@12635
|
153 |
(printable) symbol, respectively.
|
wenzelm@12635
|
154 |
|
wenzelm@12635
|
155 |
\medskip The following version of our \isa{xor} definition uses a
|
wenzelm@12635
|
156 |
standard Isabelle symbol to achieve typographically pleasing output.%
|
wenzelm@12635
|
157 |
\end{isamarkuptext}%
|
wenzelm@12627
|
158 |
\isamarkuptrue%
|
wenzelm@12627
|
159 |
\isamarkupfalse%
|
wenzelm@12627
|
160 |
\isamarkupfalse%
|
wenzelm@12635
|
161 |
\isacommand{constdefs}\isanewline
|
wenzelm@12635
|
162 |
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
|
wenzelm@12635
|
163 |
\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
wenzelm@12627
|
164 |
\isamarkupfalse%
|
wenzelm@12635
|
165 |
%
|
wenzelm@12635
|
166 |
\begin{isamarkuptext}%
|
wenzelm@12635
|
167 |
The X-Symbol package within Proof~General provides several input
|
wenzelm@12635
|
168 |
methods to enter \isa{{\isasymoplus}} in the text. If all fails one may just
|
wenzelm@12635
|
169 |
type \verb,\,\verb,<oplus>, by hand; the display is adapted
|
wenzelm@12635
|
170 |
immediately after continuing further input.
|
wenzelm@12635
|
171 |
|
wenzelm@12635
|
172 |
\medskip A slightly more refined scheme is to provide alternative
|
wenzelm@12644
|
173 |
syntax via the \bfindex{print mode} concept of Isabelle (see also
|
wenzelm@12644
|
174 |
\cite{isabelle-ref}). By convention, the mode ``$xsymbols$'' is
|
wenzelm@12644
|
175 |
enabled whenever X-Symbol is active. Consider the following hybrid
|
wenzelm@12644
|
176 |
declaration of \isa{xor}.%
|
wenzelm@12635
|
177 |
\end{isamarkuptext}%
|
wenzelm@12627
|
178 |
\isamarkuptrue%
|
wenzelm@12627
|
179 |
\isamarkupfalse%
|
wenzelm@12635
|
180 |
\isamarkupfalse%
|
wenzelm@12635
|
181 |
\isacommand{constdefs}\isanewline
|
wenzelm@12635
|
182 |
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
|
wenzelm@12635
|
183 |
\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
|
wenzelm@12635
|
184 |
\isanewline
|
wenzelm@12635
|
185 |
\isamarkupfalse%
|
wenzelm@12635
|
186 |
\isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
|
wenzelm@12635
|
187 |
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
|
wenzelm@12635
|
188 |
\isamarkupfalse%
|
wenzelm@12635
|
189 |
%
|
wenzelm@12635
|
190 |
\begin{isamarkuptext}%
|
wenzelm@12635
|
191 |
Here the \commdx{syntax} command acts like \isakeyword{consts}, but
|
wenzelm@12635
|
192 |
without declaring a logical constant, and with an optional print
|
wenzelm@12635
|
193 |
mode specification. Note that the type declaration given here
|
wenzelm@12635
|
194 |
merely serves for syntactic purposes, and is not checked for
|
wenzelm@12635
|
195 |
consistency with the real constant.
|
wenzelm@12635
|
196 |
|
wenzelm@12635
|
197 |
\medskip Now we may write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
|
wenzelm@12635
|
198 |
input, while output uses the nicer syntax of $xsymbols$, provided
|
wenzelm@12635
|
199 |
that print mode is presently active. This scheme is particularly
|
wenzelm@12635
|
200 |
useful for interactive development, with the user typing plain ASCII
|
wenzelm@12635
|
201 |
text, but gaining improved visual feedback from the system (say in
|
wenzelm@12635
|
202 |
current goal output).
|
wenzelm@12635
|
203 |
|
wenzelm@12635
|
204 |
\begin{warn}
|
wenzelm@12635
|
205 |
Using alternative syntax declarations easily results in varying
|
wenzelm@12635
|
206 |
versions of input sources. Isabelle provides no systematic way to
|
wenzelm@12635
|
207 |
convert alternative expressions back and forth. Print modes only
|
wenzelm@12635
|
208 |
affect situations where formal entities are pretty printed by the
|
wenzelm@12635
|
209 |
Isabelle process (e.g.\ output of terms and types), but not the
|
wenzelm@12635
|
210 |
original theory text.
|
wenzelm@12635
|
211 |
\end{warn}
|
wenzelm@12635
|
212 |
|
wenzelm@12635
|
213 |
\medskip The following variant makes the alternative \isa{{\isasymoplus}}
|
wenzelm@12635
|
214 |
notation only available for output. Thus we may enforce input
|
wenzelm@12635
|
215 |
sources to refer to plain ASCII only.%
|
wenzelm@12635
|
216 |
\end{isamarkuptext}%
|
wenzelm@12627
|
217 |
\isamarkuptrue%
|
wenzelm@12635
|
218 |
\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
|
wenzelm@12635
|
219 |
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
|
wenzelm@12635
|
220 |
%
|
wenzelm@12647
|
221 |
\isamarkupsubsection{Prefix Annotations%
|
wenzelm@12635
|
222 |
}
|
wenzelm@12627
|
223 |
\isamarkuptrue%
|
wenzelm@12635
|
224 |
%
|
wenzelm@12635
|
225 |
\begin{isamarkuptext}%
|
wenzelm@12644
|
226 |
Prefix syntax annotations\index{prefix annotation} are just a very
|
wenzelm@12644
|
227 |
degenerate of the general mixfix form \cite{isabelle-ref}, without
|
wenzelm@12644
|
228 |
any template arguments or priorities --- just some piece of literal
|
wenzelm@12644
|
229 |
syntax.
|
wenzelm@12635
|
230 |
|
wenzelm@12635
|
231 |
The following example illustrates this idea idea by associating
|
wenzelm@12635
|
232 |
common symbols with the constructors of a currency datatype.%
|
wenzelm@12635
|
233 |
\end{isamarkuptext}%
|
wenzelm@12627
|
234 |
\isamarkuptrue%
|
wenzelm@12635
|
235 |
\isacommand{datatype}\ currency\ {\isacharequal}\isanewline
|
wenzelm@12635
|
236 |
\ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
|
wenzelm@12635
|
237 |
\ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
|
wenzelm@12635
|
238 |
\ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
|
wenzelm@12635
|
239 |
\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
|
wenzelm@12635
|
240 |
%
|
wenzelm@12635
|
241 |
\begin{isamarkuptext}%
|
wenzelm@12635
|
242 |
Here the degenerate mixfix annotations on the rightmost column
|
wenzelm@12635
|
243 |
happen to consist of a single Isabelle symbol each:
|
wenzelm@12635
|
244 |
\verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
|
wenzelm@12644
|
245 |
\verb,\,\verb,<yen>,, \verb,$,.
|
wenzelm@12635
|
246 |
|
wenzelm@12635
|
247 |
Recall that a constructor like \isa{Euro} actually is a function
|
wenzelm@12635
|
248 |
\isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will
|
wenzelm@12644
|
249 |
be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}. Only the head of the application is
|
wenzelm@12644
|
250 |
subject to our concrete syntax; this simple form already achieves
|
wenzelm@12644
|
251 |
conformance with notational standards of the European Commission.
|
wenzelm@12635
|
252 |
|
wenzelm@12635
|
253 |
\medskip Certainly, the same idea of prefix syntax also works for
|
wenzelm@12635
|
254 |
\isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
|
wenzelm@12635
|
255 |
might introduce a (slightly unrealistic) function to calculate an
|
wenzelm@12635
|
256 |
abstract currency value, by cases on the datatype constructors and
|
wenzelm@12644
|
257 |
fixed exchange rates. The funny symbol used here is that of
|
wenzelm@12644
|
258 |
\verb,\<currency>,.%
|
wenzelm@12635
|
259 |
\end{isamarkuptext}%
|
wenzelm@12627
|
260 |
\isamarkuptrue%
|
wenzelm@12635
|
261 |
\isacommand{consts}\isanewline
|
wenzelm@12635
|
262 |
\ \ currency\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}currency\ {\isasymRightarrow}\ nat{\isachardoublequote}\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
|
wenzelm@12635
|
263 |
%
|
wenzelm@12647
|
264 |
\isamarkupsubsection{Syntax Translations \label{sec:def-translations}%
|
wenzelm@12635
|
265 |
}
|
wenzelm@12627
|
266 |
\isamarkuptrue%
|
wenzelm@12635
|
267 |
%
|
wenzelm@12635
|
268 |
\begin{isamarkuptext}%
|
wenzelm@12635
|
269 |
FIXME
|
wenzelm@12635
|
270 |
|
wenzelm@12635
|
271 |
\index{syntax translations|(}%
|
wenzelm@12635
|
272 |
\index{translations@\isacommand {translations} (command)|(}
|
wenzelm@12635
|
273 |
Isabelle offers an additional definitional facility,
|
wenzelm@12635
|
274 |
\textbf{syntax translations}.
|
wenzelm@12635
|
275 |
They resemble macros: upon parsing, the defined concept is immediately
|
wenzelm@12635
|
276 |
replaced by its definition. This effect is reversed upon printing. For example,
|
wenzelm@12635
|
277 |
the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
|
wenzelm@12635
|
278 |
\end{isamarkuptext}%
|
wenzelm@12627
|
279 |
\isamarkuptrue%
|
wenzelm@12635
|
280 |
\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
|
wenzelm@12635
|
281 |
%
|
wenzelm@12635
|
282 |
\begin{isamarkuptext}%
|
wenzelm@12635
|
283 |
\index{$IsaEqTrans@\isasymrightleftharpoons}
|
wenzelm@12635
|
284 |
\noindent
|
wenzelm@12635
|
285 |
Internally, \isa{{\isasymnoteq}} never appears.
|
wenzelm@12635
|
286 |
|
wenzelm@12635
|
287 |
In addition to \isa{{\isasymrightleftharpoons}} there are
|
wenzelm@12635
|
288 |
\isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup}
|
wenzelm@12635
|
289 |
and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown}
|
wenzelm@12635
|
290 |
for uni-directional translations, which only affect
|
wenzelm@12635
|
291 |
parsing or printing. This tutorial will not cover the details of
|
wenzelm@12635
|
292 |
translations. We have mentioned the concept merely because it
|
wenzelm@12635
|
293 |
crops up occasionally; a number of HOL's built-in constructs are defined
|
wenzelm@12647
|
294 |
via translations. Translations are preferable to definitions when the new
|
wenzelm@12635
|
295 |
concept is a trivial variation on an existing one. For example, we
|
wenzelm@12635
|
296 |
don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
|
wenzelm@12635
|
297 |
about \isa{{\isacharequal}} still apply.%
|
wenzelm@12635
|
298 |
\index{syntax translations|)}%
|
wenzelm@12635
|
299 |
\index{translations@\isacommand {translations} (command)|)}%
|
wenzelm@12635
|
300 |
\end{isamarkuptext}%
|
wenzelm@12627
|
301 |
\isamarkuptrue%
|
wenzelm@12635
|
302 |
%
|
wenzelm@12647
|
303 |
\isamarkupsection{Document Preparation%
|
wenzelm@12635
|
304 |
}
|
wenzelm@12627
|
305 |
\isamarkuptrue%
|
wenzelm@12635
|
306 |
%
|
wenzelm@12644
|
307 |
\begin{isamarkuptext}%
|
wenzelm@12644
|
308 |
Isabelle/Isar is centered around a certain notion of \bfindex{formal
|
wenzelm@12644
|
309 |
proof documents}\index{documents|bold}: ultimately the result of the
|
wenzelm@12644
|
310 |
user's theory development efforts is a human-readable record --- as
|
wenzelm@12644
|
311 |
a browsable PDF file or printed on paper. The overall document
|
wenzelm@12644
|
312 |
structure follows traditional mathematical articles, with
|
wenzelm@12644
|
313 |
sectioning, explanations, definitions, theorem statements, and
|
wenzelm@12644
|
314 |
proofs.
|
wenzelm@12644
|
315 |
|
wenzelm@12644
|
316 |
The Isar proof language \cite{Wenzel-PhD}, which is not covered in
|
wenzelm@12644
|
317 |
this book, admits to write formal proof texts that are acceptable
|
wenzelm@12644
|
318 |
both to the machine and human readers at the same time. Thus
|
wenzelm@12644
|
319 |
marginal comments and explanations may be kept at a minimum.
|
wenzelm@12644
|
320 |
Nevertheless, Isabelle document output is still useful without
|
wenzelm@12644
|
321 |
actual Isar proof texts; formal specifications usually deserve their
|
wenzelm@12644
|
322 |
own coverage in the text, while unstructured proof scripts may be
|
wenzelm@12644
|
323 |
just ignore by readers (or intentionally suppressed from the text).
|
wenzelm@12644
|
324 |
|
wenzelm@12644
|
325 |
\medskip The Isabelle document preparation system essentially acts
|
wenzelm@12644
|
326 |
like a formal front-end for {\LaTeX}. After checking definitions
|
wenzelm@12644
|
327 |
and proofs the theory sources are turned into typesetting
|
wenzelm@12644
|
328 |
instructions, so the final document is known to observe quite strong
|
wenzelm@12644
|
329 |
``soundness'' properties. This enables users to write authentic
|
wenzelm@12644
|
330 |
reports on formal theory developments with little additional effort,
|
wenzelm@12644
|
331 |
the most tedious consistency checks are handled by the system.%
|
wenzelm@12644
|
332 |
\end{isamarkuptext}%
|
wenzelm@12635
|
333 |
\isamarkuptrue%
|
wenzelm@12635
|
334 |
%
|
wenzelm@12647
|
335 |
\isamarkupsubsection{Isabelle Sessions%
|
wenzelm@12635
|
336 |
}
|
wenzelm@12635
|
337 |
\isamarkuptrue%
|
wenzelm@12635
|
338 |
%
|
wenzelm@12635
|
339 |
\begin{isamarkuptext}%
|
wenzelm@12644
|
340 |
In contrast to the highly interactive mode of the formal parts of
|
wenzelm@12644
|
341 |
Isabelle/Isar theory development, the document preparation stage
|
wenzelm@12644
|
342 |
essentially works in batch-mode. This revolves around the concept
|
wenzelm@12644
|
343 |
of a \bfindex{session}, which essentially consists of a collection
|
wenzelm@12644
|
344 |
of theory source files that contribute to a single output document.
|
wenzelm@12644
|
345 |
Each session is derived from a parent one (usually an object-logic
|
wenzelm@12644
|
346 |
image such as \texttt{HOL}); this results in an overall tree
|
wenzelm@12644
|
347 |
structure of Isabelle sessions.
|
wenzelm@12644
|
348 |
|
wenzelm@12644
|
349 |
The canonical arrangement of source files of a session called
|
wenzelm@12644
|
350 |
\texttt{MySession} is as follows:
|
wenzelm@12644
|
351 |
|
wenzelm@12644
|
352 |
\begin{itemize}
|
wenzelm@12644
|
353 |
|
wenzelm@12644
|
354 |
\item Directory \texttt{MySession} contains the required theory
|
wenzelm@12644
|
355 |
files, say $A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}.
|
wenzelm@12644
|
356 |
|
wenzelm@12644
|
357 |
\item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
|
wenzelm@12644
|
358 |
for loading all wanted theories, usually just
|
wenzelm@12644
|
359 |
\texttt{use_thy~"$A@i$"} for any $A@i$ in leaf position of the
|
wenzelm@12644
|
360 |
theory dependency graph.
|
wenzelm@12644
|
361 |
|
wenzelm@12644
|
362 |
\item Directory \texttt{MySession/document} contains everything
|
wenzelm@12644
|
363 |
required for the {\LaTeX} stage, but only \texttt{root.tex} needs to
|
wenzelm@12644
|
364 |
be provided initially. The latter file holds appropriate {\LaTeX}
|
wenzelm@12644
|
365 |
code to commence a document (\verb,\documentclass, etc.), and to
|
wenzelm@12644
|
366 |
include the generated files $A@i$\texttt{.tex} for each theory. The
|
wenzelm@12644
|
367 |
generated file \texttt{session.tex} holds {\LaTeX} commands to
|
wenzelm@12644
|
368 |
include \emph{all} theory output files in topologically sorted
|
wenzelm@12644
|
369 |
order.
|
wenzelm@12644
|
370 |
|
wenzelm@12644
|
371 |
\item In addition an \texttt{IsaMakefile} outside of directory
|
wenzelm@12644
|
372 |
\texttt{MySession} holds appropriate dependencies and invocations of
|
wenzelm@12644
|
373 |
Isabelle tools to control the batch job. The details are covered in
|
wenzelm@12644
|
374 |
\cite{isabelle-sys}; \texttt{isatool usedir} is the most important
|
wenzelm@12644
|
375 |
entry point.
|
wenzelm@12644
|
376 |
|
wenzelm@12644
|
377 |
\end{itemize}
|
wenzelm@12644
|
378 |
|
wenzelm@12644
|
379 |
With everything put in its proper place, \texttt{isatool make}
|
wenzelm@12644
|
380 |
should be sufficient to process the Isabelle session completely,
|
wenzelm@12644
|
381 |
with the generated document appearing in its proper place (within
|
wenzelm@12644
|
382 |
\verb,~/isabelle/browser_info,).
|
wenzelm@12644
|
383 |
|
wenzelm@12647
|
384 |
In practice, users may want to have \texttt{isatool mkdir} generate
|
wenzelm@12644
|
385 |
an initial working setup without further ado. For example, an empty
|
wenzelm@12644
|
386 |
session \texttt{MySession} derived from \texttt{HOL} may be produced
|
wenzelm@12644
|
387 |
as follows:
|
wenzelm@12644
|
388 |
|
wenzelm@12644
|
389 |
\begin{verbatim}
|
wenzelm@12644
|
390 |
isatool mkdir HOL MySession
|
wenzelm@12644
|
391 |
isatool make
|
wenzelm@12644
|
392 |
\end{verbatim}
|
wenzelm@12644
|
393 |
|
wenzelm@12644
|
394 |
This runs the session with sensible default options, including
|
wenzelm@12644
|
395 |
verbose mode to tell the user where the result will appear. The
|
wenzelm@12644
|
396 |
above dry run should produce should produce a single page of output
|
wenzelm@12644
|
397 |
(with a dummy title, empty table of contents etc.). Any failure at
|
wenzelm@12644
|
398 |
that stage is likely to indicate some technical problems with your
|
wenzelm@12644
|
399 |
{\LaTeX} installation.\footnote{Especially make sure that
|
wenzelm@12644
|
400 |
\texttt{pdflatex} is present.}
|
wenzelm@12644
|
401 |
|
wenzelm@12644
|
402 |
\medskip Users may now start to populate the directory
|
wenzelm@12644
|
403 |
\texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
|
wenzelm@12644
|
404 |
accordingly. \texttt{MySession/document/root.tex} should be also
|
wenzelm@12644
|
405 |
adapted at some point; the generated version is mostly
|
wenzelm@12647
|
406 |
self-explanatory. The default versions includes the
|
wenzelm@12647
|
407 |
\texttt{isabelle} (mandatory) and \texttt{isabellesym} (required for
|
wenzelm@12647
|
408 |
mathematical symbols); further packages may required, e.g.\ for
|
wenzelm@12647
|
409 |
unusual Isabelle symbols.
|
wenzelm@12644
|
410 |
|
wenzelm@12644
|
411 |
Realistic applications may demand additional files in
|
wenzelm@12644
|
412 |
\texttt{MySession/document} for the {\LaTeX} stage, such as
|
wenzelm@12644
|
413 |
\texttt{root.bib} for the bibliographic database.\footnote{Using
|
wenzelm@12644
|
414 |
that particular name of \texttt{root.bib}, the Isabelle document
|
wenzelm@12644
|
415 |
processor (actually \texttt{isatool document} \cite{isabelle-sys})
|
wenzelm@12644
|
416 |
will be smart enough to invoke \texttt{bibtex} accordingly.}
|
wenzelm@12644
|
417 |
|
wenzelm@12644
|
418 |
\medskip Failure of the document preparation phase in an Isabelle
|
wenzelm@12644
|
419 |
batch session leaves the generated sources in there target location
|
wenzelm@12644
|
420 |
(as pointed out by the accompanied error message). In case of
|
wenzelm@12644
|
421 |
{\LaTeX} errors, users may trace error messages at the file position
|
wenzelm@12644
|
422 |
of the generated text.%
|
wenzelm@12644
|
423 |
\end{isamarkuptext}%
|
wenzelm@12644
|
424 |
\isamarkuptrue%
|
wenzelm@12644
|
425 |
%
|
wenzelm@12647
|
426 |
\isamarkupsubsection{Structure Markup%
|
wenzelm@12644
|
427 |
}
|
wenzelm@12644
|
428 |
\isamarkuptrue%
|
wenzelm@12644
|
429 |
%
|
wenzelm@12644
|
430 |
\isamarkupsubsubsection{Sections%
|
wenzelm@12644
|
431 |
}
|
wenzelm@12644
|
432 |
\isamarkuptrue%
|
wenzelm@12644
|
433 |
%
|
wenzelm@12644
|
434 |
\begin{isamarkuptext}%
|
wenzelm@12647
|
435 |
FIXME \verb,\label, within sections;
|
wenzelm@12647
|
436 |
|
wenzelm@12647
|
437 |
The large-scale structure of Isabelle documents closely follows
|
wenzelm@12644
|
438 |
{\LaTeX} convention, with chapters, sections, subsubsections etc.
|
wenzelm@12644
|
439 |
The formal Isar language includes separate structure \bfindex{markup
|
wenzelm@12644
|
440 |
commands}, which do not effect the formal content of a theory (or
|
wenzelm@12644
|
441 |
proof), but results in corresponding {\LaTeX} elements issued to the
|
wenzelm@12644
|
442 |
output.
|
wenzelm@12644
|
443 |
|
wenzelm@12644
|
444 |
There are different markup commands for different formal contexts:
|
wenzelm@12644
|
445 |
in header position (just before a \isakeyword{theory} command),
|
wenzelm@12644
|
446 |
within the theory body, or within a proof. Note that the header
|
wenzelm@12644
|
447 |
needs to be treated specially, since ordinary theory and proof
|
wenzelm@12644
|
448 |
commands may only occur \emph{after} the initial \isakeyword{theory}
|
wenzelm@12644
|
449 |
specification.
|
wenzelm@12644
|
450 |
|
wenzelm@12644
|
451 |
\smallskip
|
wenzelm@12644
|
452 |
|
wenzelm@12644
|
453 |
\begin{tabular}{llll}
|
wenzelm@12644
|
454 |
header & theory & proof & default meaning \\\hline
|
wenzelm@12644
|
455 |
& \commdx{chapter} & & \verb,\chapter, \\
|
wenzelm@12644
|
456 |
\commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
|
wenzelm@12644
|
457 |
& \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
|
wenzelm@12644
|
458 |
& \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
|
wenzelm@12644
|
459 |
\end{tabular}
|
wenzelm@12644
|
460 |
|
wenzelm@12644
|
461 |
\medskip
|
wenzelm@12644
|
462 |
|
wenzelm@12644
|
463 |
From the Isabelle perspective, each markup command takes a single
|
wenzelm@12644
|
464 |
text argument (delimited by \verb,",\dots\verb,", or
|
wenzelm@12644
|
465 |
\verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping
|
wenzelm@12644
|
466 |
surrounding white space, the argument is passed to a {\LaTeX} macro
|
wenzelm@12644
|
467 |
\verb,\isamarkupXXX, for any command \isakeyword{XXX}. The latter
|
wenzelm@12644
|
468 |
are defined in \verb,isabelle.sty, according to the rightmost column
|
wenzelm@12644
|
469 |
above.
|
wenzelm@12644
|
470 |
|
wenzelm@12644
|
471 |
\medskip The following source fragment illustrates structure markup
|
wenzelm@12647
|
472 |
of a theory. Note that {\LaTeX} labels may well be included inside
|
wenzelm@12647
|
473 |
of section headings as well.
|
wenzelm@12644
|
474 |
|
wenzelm@12644
|
475 |
\begin{ttbox}
|
wenzelm@12644
|
476 |
header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
|
wenzelm@12644
|
477 |
|
wenzelm@12644
|
478 |
theory Foo_Bar = Main:
|
wenzelm@12644
|
479 |
|
wenzelm@12644
|
480 |
subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
|
wenzelm@12644
|
481 |
|
wenzelm@12644
|
482 |
consts
|
wenzelm@12644
|
483 |
foo :: \dots
|
wenzelm@12644
|
484 |
bar :: \dots
|
wenzelm@12647
|
485 |
|
wenzelm@12644
|
486 |
defs \dots
|
wenzelm@12647
|
487 |
|
wenzelm@12644
|
488 |
subsection {\ttlbrace}* Derived rules *{\ttrbrace}
|
wenzelm@12644
|
489 |
|
wenzelm@12644
|
490 |
lemma fooI: \dots
|
wenzelm@12644
|
491 |
lemma fooE: \dots
|
wenzelm@12644
|
492 |
|
wenzelm@12647
|
493 |
subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
|
wenzelm@12644
|
494 |
|
wenzelm@12644
|
495 |
theorem main: \dots
|
wenzelm@12644
|
496 |
|
wenzelm@12644
|
497 |
end
|
wenzelm@12644
|
498 |
\end{ttbox}
|
wenzelm@12644
|
499 |
|
wenzelm@12647
|
500 |
Users may occasionally want to change the meaning of some markup
|
wenzelm@12647
|
501 |
commands, typically via appropriate use of \verb,\renewcommand, in
|
wenzelm@12647
|
502 |
\texttt{root.tex}. The \verb,\isamarkupheader, is a good candidate
|
wenzelm@12647
|
503 |
for some adaption, e.g.\ moving it up in the hierarchy to become
|
wenzelm@12647
|
504 |
\verb,\chapter,.
|
wenzelm@12644
|
505 |
|
wenzelm@12644
|
506 |
\begin{verbatim}
|
wenzelm@12644
|
507 |
\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
|
wenzelm@12644
|
508 |
\end{verbatim}
|
wenzelm@12644
|
509 |
|
wenzelm@12644
|
510 |
Certainly, this requires to change the default
|
wenzelm@12644
|
511 |
\verb,\documentclass{article}, in \texttt{root.tex} to something
|
wenzelm@12644
|
512 |
that supports the notion of chapters in the first place, e.g.\
|
wenzelm@12647
|
513 |
\verb,\documentclass{report},.
|
wenzelm@12644
|
514 |
|
wenzelm@12647
|
515 |
\medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
|
wenzelm@12647
|
516 |
hold the name of the current theory context. This is particularly
|
wenzelm@12647
|
517 |
useful for document headings or footings, e.g.\ like this:
|
wenzelm@12644
|
518 |
|
wenzelm@12644
|
519 |
\begin{verbatim}
|
wenzelm@12644
|
520 |
\renewcommand{\isamarkupheader}[1]%
|
wenzelm@12644
|
521 |
{\chapter{#1}\markright{THEORY~\isabellecontext}}
|
wenzelm@12644
|
522 |
\end{verbatim}
|
wenzelm@12644
|
523 |
|
wenzelm@12644
|
524 |
\noindent Make sure to include something like
|
wenzelm@12647
|
525 |
\verb,\pagestyle{headings}, in \texttt{root.tex}; the document
|
wenzelm@12647
|
526 |
should have more than 2 pages to show the effect.%
|
wenzelm@12644
|
527 |
\end{isamarkuptext}%
|
wenzelm@12644
|
528 |
\isamarkuptrue%
|
wenzelm@12644
|
529 |
%
|
wenzelm@12647
|
530 |
\isamarkupsubsection{Formal Comments and Antiquotations%
|
wenzelm@12644
|
531 |
}
|
wenzelm@12644
|
532 |
\isamarkuptrue%
|
wenzelm@12644
|
533 |
%
|
wenzelm@12644
|
534 |
\begin{isamarkuptext}%
|
wenzelm@12647
|
535 |
Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),%
|
wenzelm@12644
|
536 |
\end{isamarkuptext}%
|
wenzelm@12644
|
537 |
\isamarkuptrue%
|
wenzelm@12644
|
538 |
%
|
wenzelm@12647
|
539 |
\isamarkupsubsection{Symbols and Characters%
|
wenzelm@12644
|
540 |
}
|
wenzelm@12644
|
541 |
\isamarkuptrue%
|
wenzelm@12644
|
542 |
%
|
wenzelm@12644
|
543 |
\begin{isamarkuptext}%
|
wenzelm@12644
|
544 |
FIXME \verb,\isabellestyle,%
|
wenzelm@12644
|
545 |
\end{isamarkuptext}%
|
wenzelm@12644
|
546 |
\isamarkuptrue%
|
wenzelm@12644
|
547 |
%
|
wenzelm@12647
|
548 |
\isamarkupsubsection{Suppressing Output%
|
wenzelm@12644
|
549 |
}
|
wenzelm@12644
|
550 |
\isamarkuptrue%
|
wenzelm@12644
|
551 |
%
|
wenzelm@12644
|
552 |
\begin{isamarkuptext}%
|
wenzelm@12647
|
553 |
By default Isabelle's document system generates a {\LaTeX} source
|
wenzelm@12647
|
554 |
file for each theory that happens to get loaded during the session.
|
wenzelm@12647
|
555 |
The generated \texttt{session.tex} file will include all of these in
|
wenzelm@12647
|
556 |
order of appearance, which in turn gets included by the standard
|
wenzelm@12647
|
557 |
\texttt{root.tex} file. Certainly one may change the order of
|
wenzelm@12647
|
558 |
appearance or suppress unwanted theories by ignoring
|
wenzelm@12647
|
559 |
\texttt{session.tex} and include individual files in
|
wenzelm@12647
|
560 |
\texttt{root.tex} by hand. On the other hand, such an arrangement
|
wenzelm@12647
|
561 |
requires additional efforts for maintenance.
|
wenzelm@12644
|
562 |
|
wenzelm@12647
|
563 |
Alternatively, one may tune the theory loading process in
|
wenzelm@12647
|
564 |
\texttt{ROOT.ML}: traversal of the theory dependency graph may be
|
wenzelm@12647
|
565 |
fine-tuned by adding further \verb,use_thy, invocations, although
|
wenzelm@12647
|
566 |
topological sorting needs to be preserved. Moreover, the ML
|
wenzelm@12647
|
567 |
operator \verb,no_document, temporarily disables document generation
|
wenzelm@12647
|
568 |
while executing a theory loader command; the usage is like this:
|
wenzelm@12647
|
569 |
|
wenzelm@12647
|
570 |
\begin{verbatim}
|
wenzelm@12647
|
571 |
no_document use_thy "Aux";
|
wenzelm@12647
|
572 |
\end{verbatim}
|
wenzelm@12647
|
573 |
|
wenzelm@12647
|
574 |
Theory output may be also suppressed \emph{partially} as well.
|
wenzelm@12647
|
575 |
Typical applications include research papers or slides based on
|
wenzelm@12647
|
576 |
formal developments --- these usually do not show the full formal
|
wenzelm@12647
|
577 |
content. The special source comments
|
wenzelm@12647
|
578 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
|
wenzelm@12647
|
579 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), are interpreted by the
|
wenzelm@12647
|
580 |
document generator as open and close parenthesis for
|
wenzelm@12647
|
581 |
\bfindex{ignored material}. Any text inside of (potentially nested)
|
wenzelm@12647
|
582 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\dots~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
|
wenzelm@12647
|
583 |
parentheses is just ignored from the output --- after correct formal
|
wenzelm@12647
|
584 |
checking.
|
wenzelm@12647
|
585 |
|
wenzelm@12647
|
586 |
In the following example we suppress the slightly formalistic
|
wenzelm@12647
|
587 |
\isakeyword{theory} and \isakeyword{end} part of a theory text.
|
wenzelm@12647
|
588 |
|
wenzelm@12647
|
589 |
\medskip
|
wenzelm@12647
|
590 |
|
wenzelm@12647
|
591 |
\begin{tabular}{l}
|
wenzelm@12647
|
592 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
|
wenzelm@12647
|
593 |
\texttt{theory A = Main:} \\
|
wenzelm@12647
|
594 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
|
wenzelm@12647
|
595 |
~~$\vdots$ \\
|
wenzelm@12647
|
596 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
|
wenzelm@12647
|
597 |
\texttt{end} \\
|
wenzelm@12647
|
598 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
|
wenzelm@12647
|
599 |
\end{tabular}
|
wenzelm@12647
|
600 |
|
wenzelm@12647
|
601 |
\medskip
|
wenzelm@12647
|
602 |
|
wenzelm@12647
|
603 |
Ignoring portions of printed text like this demands some special
|
wenzelm@12647
|
604 |
care. FIXME%
|
wenzelm@12635
|
605 |
\end{isamarkuptext}%
|
wenzelm@12627
|
606 |
\isamarkuptrue%
|
wenzelm@11866
|
607 |
\isamarkupfalse%
|
wenzelm@11648
|
608 |
\end{isabellebody}%
|
wenzelm@11648
|
609 |
%%% Local Variables:
|
wenzelm@11648
|
610 |
%%% mode: latex
|
wenzelm@11648
|
611 |
%%% TeX-master: "root"
|
wenzelm@11648
|
612 |
%%% End:
|