author | wenzelm |
Thu, 02 Sep 2010 00:48:07 +0200 | |
changeset 38980 | af73cf0dc31f |
parent 36747 | 7361d5dde9ce |
child 39050 | 600de0485859 |
permissions | -rw-r--r-- |
28762 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Inner{\isacharunderscore}Syntax}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Inner{\isacharunderscore}Syntax\isanewline |
|
12 |
\isakeyword{imports}\ Main\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Inner syntax --- the term language \label{ch:inner-syntax}% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\isamarkupsection{Printing logical entities% |
|
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
29 |
\isamarkupsubsection{Diagnostic commands% |
|
30 |
} |
|
31 |
\isamarkuptrue% |
|
32 |
% |
|
33 |
\begin{isamarkuptext}% |
|
34 |
\begin{matharray}{rcl} |
|
35 |
\indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
36 |
\indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
37 |
\indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
38 |
\indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
39 |
\indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
40 |
\indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
41 |
\indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
42 |
\end{matharray} |
|
43 |
||
44 |
These diagnostic commands assist interactive development by printing |
|
45 |
internal logical entities in a human-readable fashion. |
|
46 |
||
47 |
\begin{rail} |
|
48 |
'typ' modes? type |
|
49 |
; |
|
50 |
'term' modes? term |
|
51 |
; |
|
52 |
'prop' modes? prop |
|
53 |
; |
|
54 |
'thm' modes? thmrefs |
|
55 |
; |
|
56 |
( 'prf' | 'full\_prf' ) modes? thmrefs? |
|
57 |
; |
|
58 |
'pr' modes? nat? (',' nat)? |
|
59 |
; |
|
60 |
||
61 |
modes: '(' (name + ) ')' |
|
62 |
; |
|
63 |
\end{rail} |
|
64 |
||
65 |
\begin{description} |
|
66 |
||
67 |
\item \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}} reads and prints types of the |
|
68 |
meta-logic according to the current theory or proof context. |
|
69 |
||
70 |
\item \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}} |
|
71 |
read, type-check and print terms or propositions according to the |
|
72 |
current theory or proof context; the inferred type of \isa{t} is |
|
73 |
output as well. Note that these commands are also useful in |
|
74 |
inspecting the current environment of term abbreviations. |
|
75 |
||
76 |
\item \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} retrieves |
|
77 |
theorems from the current theory or proof context. Note that any |
|
78 |
attributes included in the theorem specifications are applied to a |
|
79 |
temporary context derived from the current theory or proof; the |
|
80 |
result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect. |
|
81 |
||
82 |
\item \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}} displays the (compact) proof term of the |
|
83 |
current proof state (if present), or of the given theorems. Note |
|
84 |
that this requires proof terms to be switched on for the current |
|
85 |
object logic (see the ``Proof terms'' section of the Isabelle |
|
86 |
reference manual for information on how to do this). |
|
87 |
||
88 |
\item \hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}} is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays |
|
89 |
the full proof term, i.e.\ also displays information omitted in the |
|
90 |
compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders |
|
91 |
there. |
|
92 |
||
93 |
\item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} prints the current |
|
94 |
proof state (if present), including the proof context, current facts |
|
95 |
and goals. The optional limit arguments affect the number of goals |
|
96 |
and premises to be displayed, which is initially 10 for both. |
|
97 |
Omitting limit values leaves the current setting unchanged. |
|
98 |
||
99 |
\end{description} |
|
100 |
||
101 |
All of the diagnostic commands above admit a list of \isa{modes} |
|
102 |
to be specified, which is appended to the current print mode (see |
|
103 |
also \cite{isabelle-ref}). Thus the output behavior may be modified |
|
104 |
according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols{\isacharparenright}{\isachardoublequote}} would print the current proof state |
|
105 |
with mathematical symbols and special characters represented in |
|
106 |
{\LaTeX} source, according to the Isabelle style |
|
107 |
\cite{isabelle-sys}. |
|
108 |
||
109 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
|
110 |
systematic way to include formal items into the printed text |
|
111 |
document.% |
|
112 |
\end{isamarkuptext}% |
|
113 |
\isamarkuptrue% |
|
114 |
% |
|
115 |
\isamarkupsubsection{Details of printed content% |
|
116 |
} |
|
117 |
\isamarkuptrue% |
|
118 |
% |
|
119 |
\begin{isamarkuptext}% |
|
120 |
\begin{mldecls} |
|
32836 | 121 |
\indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\ |
122 |
\indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\ |
|
123 |
\indexdef{}{ML}{show\_consts}\verb|show_consts: bool Unsynchronized.ref| & default \verb|false| \\ |
|
124 |
\indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\ |
|
125 |
\indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\ |
|
126 |
\indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\ |
|
127 |
\indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\ |
|
128 |
\indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Unsynchronized.ref| & default \verb|true| \\ |
|
129 |
\indexdef{}{ML}{goals\_limit}\verb|goals_limit: int Unsynchronized.ref| & default \verb|10| \\ |
|
130 |
\indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\ |
|
131 |
\indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\ |
|
132 |
\indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\ |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
36747
diff
changeset
|
133 |
\indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\ |
28762 | 134 |
\end{mldecls} |
135 |
||
136 |
These global ML variables control the detail of information that is |
|
137 |
displayed for types, terms, theorems, goals etc. |
|
138 |
||
139 |
In interactive sessions, the user interface usually manages these |
|
140 |
global parameters of the Isabelle process, even with some concept of |
|
141 |
persistence. Nonetheless it is occasionally useful to manipulate ML |
|
142 |
variables directly, e.g.\ using \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} or \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}. |
|
143 |
||
144 |
Batch-mode logic sessions may be configured by putting appropriate |
|
145 |
ML text directly into the \verb|ROOT.ML| file. |
|
146 |
||
147 |
\begin{description} |
|
148 |
||
149 |
\item \verb|show_types| and \verb|show_sorts| control printing of type |
|
150 |
constraints for term variables, and sort constraints for type |
|
151 |
variables. By default, neither of these are shown in output. If |
|
152 |
\verb|show_sorts| is set to \verb|true|, types are always shown as |
|
153 |
well. |
|
154 |
||
155 |
Note that displaying types and sorts may explain why a polymorphic |
|
156 |
inference rule fails to resolve with some goal, or why a rewrite |
|
157 |
rule does not apply as expected. |
|
158 |
||
159 |
\item \verb|show_consts| controls printing of types of constants when |
|
160 |
displaying a goal state. |
|
161 |
||
162 |
Note that the output can be enormous, because polymorphic constants |
|
163 |
often occur at several different type instances. |
|
164 |
||
165 |
\item \verb|long_names|, \verb|short_names|, and \verb|unique_names| |
|
166 |
control the way of printing fully qualified internal names in |
|
167 |
external form. See also \secref{sec:antiq} for the document |
|
168 |
antiquotation options of the same names. |
|
169 |
||
170 |
\item \verb|show_brackets| controls bracketing in pretty printed |
|
171 |
output. If set to \verb|true|, all sub-expressions of the pretty |
|
172 |
printing tree will be parenthesized, even if this produces malformed |
|
173 |
term syntax! This crude way of showing the internal structure of |
|
174 |
pretty printed entities may occasionally help to diagnose problems |
|
175 |
with operator priorities, for example. |
|
176 |
||
177 |
\item \verb|eta_contract| controls \isa{{\isachardoublequote}{\isasymeta}{\isachardoublequote}}-contracted printing of |
|
178 |
terms. |
|
179 |
||
180 |
The \isa{{\isasymeta}}-contraction law asserts \isa{{\isachardoublequote}{\isacharparenleft}{\isasymlambda}x{\isachardot}\ f\ x{\isacharparenright}\ {\isasymequiv}\ f{\isachardoublequote}}, |
|
181 |
provided \isa{x} is not free in \isa{f}. It asserts |
|
182 |
\emph{extensionality} of functions: \isa{{\isachardoublequote}f\ {\isasymequiv}\ g{\isachardoublequote}} if \isa{{\isachardoublequote}f\ x\ {\isasymequiv}\ g\ x{\isachardoublequote}} for all \isa{x}. Higher-order unification frequently puts |
|
183 |
terms into a fully \isa{{\isasymeta}}-expanded form. For example, if \isa{F} has type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymtau}\ {\isasymRightarrow}\ {\isasymtau}{\isacharparenright}\ {\isasymRightarrow}\ {\isasymtau}{\isachardoublequote}} then its expanded form is \isa{{\isachardoublequote}{\isasymlambda}h{\isachardot}\ F\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ h\ x{\isacharparenright}{\isachardoublequote}}. |
|
184 |
||
185 |
Setting \verb|eta_contract| makes Isabelle perform \isa{{\isasymeta}}-contractions before printing, so that \isa{{\isachardoublequote}{\isasymlambda}h{\isachardot}\ F\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ h\ x{\isacharparenright}{\isachardoublequote}} |
|
186 |
appears simply as \isa{F}. |
|
187 |
||
188 |
Note that the distinction between a term and its \isa{{\isasymeta}}-expanded |
|
189 |
form occasionally matters. While higher-order resolution and |
|
190 |
rewriting operate modulo \isa{{\isachardoublequote}{\isasymalpha}{\isasymbeta}{\isasymeta}{\isachardoublequote}}-conversion, some other tools |
|
191 |
might look at terms more discretely. |
|
192 |
||
193 |
\item \verb|goals_limit| controls the maximum number of subgoals to |
|
194 |
be shown in goal output. |
|
195 |
||
196 |
\item \verb|Proof.show_main_goal| controls whether the main result to |
|
197 |
be proven should be displayed. This information might be relevant |
|
198 |
for schematic goals, to inspect the current claim that has been |
|
199 |
synthesized so far. |
|
200 |
||
201 |
\item \verb|show_hyps| controls printing of implicit hypotheses of |
|
202 |
local facts. Normally, only those hypotheses are displayed that are |
|
203 |
\emph{not} covered by the assumptions of the current context: this |
|
204 |
situation indicates a fault in some tool being used. |
|
205 |
||
206 |
By setting \verb|show_hyps| to \verb|true|, output of \emph{all} |
|
207 |
hypotheses can be enforced, which is occasionally useful for |
|
208 |
diagnostic purposes. |
|
209 |
||
210 |
\item \verb|show_tags| controls printing of extra annotations within |
|
211 |
theorems, such as internal position information, or the case names |
|
212 |
being attached by the attribute \hyperlink{attribute.case-names}{\mbox{\isa{case{\isacharunderscore}names}}}. |
|
213 |
||
214 |
Note that the \hyperlink{attribute.tagged}{\mbox{\isa{tagged}}} and \hyperlink{attribute.untagged}{\mbox{\isa{untagged}}} |
|
215 |
attributes provide low-level access to the collection of tags |
|
216 |
associated with a theorem. |
|
217 |
||
218 |
\item \verb|show_question_marks| controls printing of question marks |
|
219 |
for schematic variables, such as \isa{{\isacharquery}x}. Only the leading |
|
220 |
question mark is affected, the remaining text is unchanged |
|
221 |
(including proper markup for schematic variables that might be |
|
222 |
relevant for user interfaces). |
|
223 |
||
224 |
\end{description}% |
|
225 |
\end{isamarkuptext}% |
|
226 |
\isamarkuptrue% |
|
227 |
% |
|
228 |
\isamarkupsubsection{Printing limits% |
|
229 |
} |
|
230 |
\isamarkuptrue% |
|
231 |
% |
|
232 |
\begin{isamarkuptext}% |
|
233 |
\begin{mldecls} |
|
36745 | 234 |
\indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\ |
30121 | 235 |
\indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\ |
28762 | 236 |
\end{mldecls} |
237 |
||
238 |
These ML functions set limits for pretty printed text. |
|
239 |
||
240 |
\begin{description} |
|
241 |
||
36745 | 242 |
\item \verb|Pretty.margin_default| indicates the global default for |
243 |
the right margin of the built-in pretty printer, with initial value |
|
244 |
76. Note that user-interfaces typically control margins |
|
245 |
automatically when resizing windows, or even bypass the formatting |
|
246 |
engine of Isabelle/ML altogether and do it within the front end via |
|
247 |
Isabelle/Scala. |
|
28762 | 248 |
|
249 |
\item \verb|print_depth|~\isa{n} limits the printing depth of the |
|
250 |
ML toplevel pretty printer; the precise effect depends on the ML |
|
251 |
compiler and run-time system. Typically \isa{n} should be less |
|
252 |
than 10. Bigger values such as 100--1000 are useful for debugging. |
|
253 |
||
254 |
\end{description}% |
|
255 |
\end{isamarkuptext}% |
|
256 |
\isamarkuptrue% |
|
257 |
% |
|
258 |
\isamarkupsection{Mixfix annotations% |
|
259 |
} |
|
260 |
\isamarkuptrue% |
|
261 |
% |
|
262 |
\begin{isamarkuptext}% |
|
263 |
Mixfix annotations specify concrete \emph{inner syntax} of |
|
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32836
diff
changeset
|
264 |
Isabelle types and terms. Locally fixed parameters in toplevel |
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32836
diff
changeset
|
265 |
theorem statements, locale specifications etc.\ also admit mixfix |
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
32836
diff
changeset
|
266 |
annotations. |
28762 | 267 |
|
268 |
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix} |
|
269 |
\begin{rail} |
|
270 |
infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')' |
|
271 |
; |
|
272 |
mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')' |
|
273 |
; |
|
274 |
structmixfix: mixfix | '(' 'structure' ')' |
|
275 |
; |
|
276 |
||
277 |
prios: '[' (nat + ',') ']' |
|
278 |
; |
|
279 |
\end{rail} |
|
280 |
||
281 |
Here the \railtok{string} specifications refer to the actual mixfix |
|
282 |
template, which may include literal text, spacing, blocks, and |
|
283 |
arguments (denoted by ``\isa{{\isacharunderscore}}''); the special symbol |
|
284 |
``\verb|\<index>|'' (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}'') represents an index |
|
285 |
argument that specifies an implicit structure reference (see also |
|
286 |
\secref{sec:locale}). Infix and binder declarations provide common |
|
287 |
abbreviations for particular mixfix declarations. So in practice, |
|
288 |
mixfix templates mostly degenerate to literal text for concrete |
|
289 |
syntax, such as ``\verb|++|'' for an infix symbol. |
|
290 |
||
291 |
\medskip In full generality, mixfix declarations work as follows. |
|
292 |
Suppose a constant \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymtau}\isactrlsub n\ {\isasymRightarrow}\ {\isasymtau}{\isachardoublequote}} is |
|
293 |
annotated by \isa{{\isachardoublequote}{\isacharparenleft}mixfix\ {\isacharbrackleft}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isacharbrackright}\ p{\isacharparenright}{\isachardoublequote}}, where \isa{{\isachardoublequote}mixfix{\isachardoublequote}} is a string \isa{{\isachardoublequote}d\isactrlsub {\isadigit{0}}\ {\isacharunderscore}\ d\isactrlsub {\isadigit{1}}\ {\isacharunderscore}\ {\isasymdots}\ {\isacharunderscore}\ d\isactrlsub n{\isachardoublequote}} consisting of |
|
294 |
delimiters that surround argument positions as indicated by |
|
295 |
underscores. |
|
296 |
||
297 |
Altogether this determines a production for a context-free priority |
|
298 |
grammar, where for each argument \isa{{\isachardoublequote}i{\isachardoublequote}} the syntactic category |
|
299 |
is determined by \isa{{\isachardoublequote}{\isasymtau}\isactrlsub i{\isachardoublequote}} (with priority \isa{{\isachardoublequote}p\isactrlsub i{\isachardoublequote}}), and |
|
300 |
the result category is determined from \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} (with |
|
301 |
priority \isa{{\isachardoublequote}p{\isachardoublequote}}). Priority specifications are optional, with |
|
302 |
default 0 for arguments and 1000 for the result. |
|
303 |
||
304 |
Since \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} may be again a function type, the constant |
|
305 |
type scheme may have more argument positions than the mixfix |
|
306 |
pattern. Printing a nested application \isa{{\isachardoublequote}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}} for |
|
307 |
\isa{{\isachardoublequote}m\ {\isachargreater}\ n{\isachardoublequote}} works by attaching concrete notation only to the |
|
308 |
innermost part, essentially by printing \isa{{\isachardoublequote}{\isacharparenleft}c\ t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isacharparenright}\ {\isasymdots}\ t\isactrlsub m{\isachardoublequote}} |
|
309 |
instead. If a term has fewer arguments than specified in the mixfix |
|
310 |
template, the concrete syntax is ignored. |
|
311 |
||
312 |
\medskip A mixfix template may also contain additional directives |
|
313 |
for pretty printing, notably spaces, blocks, and breaks. The |
|
314 |
general template format is a sequence over any of the following |
|
315 |
entities. |
|
316 |
||
317 |
\begin{description} |
|
318 |
||
319 |
\item \isa{{\isachardoublequote}d{\isachardoublequote}} is a delimiter, namely a non-empty sequence of |
|
320 |
characters other than the following special characters: |
|
321 |
||
322 |
\smallskip |
|
323 |
\begin{tabular}{ll} |
|
324 |
\verb|'| & single quote \\ |
|
325 |
\verb|_| & underscore \\ |
|
326 |
\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} & index symbol \\ |
|
327 |
\verb|(| & open parenthesis \\ |
|
328 |
\verb|)| & close parenthesis \\ |
|
329 |
\verb|/| & slash \\ |
|
330 |
\end{tabular} |
|
331 |
\medskip |
|
332 |
||
333 |
\item \verb|'| escapes the special meaning of these |
|
334 |
meta-characters, producing a literal version of the following |
|
335 |
character, unless that is a blank. |
|
336 |
||
337 |
A single quote followed by a blank separates delimiters, without |
|
338 |
affecting printing, but input tokens may have additional white space |
|
339 |
here. |
|
340 |
||
341 |
\item \verb|_| is an argument position, which stands for a |
|
342 |
certain syntactic category in the underlying grammar. |
|
343 |
||
344 |
\item \isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}} is an indexed argument position; this is the place |
|
345 |
where implicit structure arguments can be attached. |
|
346 |
||
347 |
\item \isa{{\isachardoublequote}s{\isachardoublequote}} is a non-empty sequence of spaces for printing. |
|
348 |
This and the following specifications do not affect parsing at all. |
|
349 |
||
350 |
\item \verb|(|\isa{n} opens a pretty printing block. The |
|
351 |
optional number specifies how much indentation to add when a line |
|
352 |
break occurs within the block. If the parenthesis is not followed |
|
353 |
by digits, the indentation defaults to 0. A block specified via |
|
354 |
\verb|(00| is unbreakable. |
|
355 |
||
356 |
\item \verb|)| closes a pretty printing block. |
|
357 |
||
358 |
\item \verb|//| forces a line break. |
|
359 |
||
360 |
\item \verb|/|\isa{s} allows a line break. Here \isa{s} |
|
361 |
stands for the string of spaces (zero or more) right after the |
|
362 |
slash. These spaces are printed if the break is \emph{not} taken. |
|
363 |
||
364 |
\end{description} |
|
365 |
||
366 |
For example, the template \verb|(_ +/ _)| specifies an infix |
|
367 |
operator. There are two argument positions; the delimiter |
|
368 |
\verb|+| is preceded by a space and followed by a space or |
|
369 |
line break; the entire phrase is a pretty printing block. |
|
370 |
||
371 |
The general idea of pretty printing with blocks and breaks is also |
|
372 |
described in \cite{paulson-ml2}.% |
|
373 |
\end{isamarkuptext}% |
|
374 |
\isamarkuptrue% |
|
375 |
% |
|
35414 | 376 |
\isamarkupsection{Explicit notation% |
28762 | 377 |
} |
378 |
\isamarkuptrue% |
|
379 |
% |
|
380 |
\begin{isamarkuptext}% |
|
381 |
\begin{matharray}{rcll} |
|
35414 | 382 |
\indexdef{}{command}{type\_notation}\hypertarget{command.type-notation}{\hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
383 |
\indexdef{}{command}{no\_type\_notation}\hypertarget{command.no-type-notation}{\hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
28762 | 384 |
\indexdef{}{command}{notation}\hypertarget{command.notation}{\hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
385 |
\indexdef{}{command}{no\_notation}\hypertarget{command.no-notation}{\hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
36508
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
386 |
\indexdef{}{command}{write}\hypertarget{command.write}{\hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\ |
28762 | 387 |
\end{matharray} |
388 |
||
389 |
\begin{rail} |
|
35414 | 390 |
('type\_notation' | 'no\_type\_notation') target? mode? \\ (nameref mixfix + 'and') |
391 |
; |
|
29746 | 392 |
('notation' | 'no\_notation') target? mode? \\ (nameref structmixfix + 'and') |
28762 | 393 |
; |
36508
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
394 |
'write' mode? (nameref structmixfix + 'and') |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
395 |
; |
28762 | 396 |
\end{rail} |
397 |
||
398 |
\begin{description} |
|
399 |
||
35414 | 400 |
\item \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix |
401 |
syntax with an existing type constructor. The arity of the |
|
402 |
constructor is retrieved from the context. |
|
403 |
||
404 |
\item \hyperlink{command.no-type-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}type{\isacharunderscore}notation}}}} is similar to \hyperlink{command.type-notation}{\mbox{\isa{\isacommand{type{\isacharunderscore}notation}}}}, but removes the specified syntax annotation from |
|
405 |
the present context. |
|
406 |
||
28762 | 407 |
\item \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} associates mixfix |
35414 | 408 |
syntax with an existing constant or fixed variable. The type |
409 |
declaration of the given entity is retrieved from the context. |
|
28762 | 410 |
|
411 |
\item \hyperlink{command.no-notation}{\mbox{\isa{\isacommand{no{\isacharunderscore}notation}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, |
|
412 |
but removes the specified syntax annotation from the present |
|
413 |
context. |
|
414 |
||
36508
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
415 |
\item \hyperlink{command.write}{\mbox{\isa{\isacommand{write}}}} is similar to \hyperlink{command.notation}{\mbox{\isa{\isacommand{notation}}}}, but |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
416 |
works within an Isar proof body. |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
417 |
|
35414 | 418 |
\end{description} |
419 |
||
36508
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
420 |
Note that the more primitive commands \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} and |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
421 |
\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}} (\secref{sec:syn-trans}) provide raw access |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
35414
diff
changeset
|
422 |
to the syntax tables of a global theory.% |
28762 | 423 |
\end{isamarkuptext}% |
424 |
\isamarkuptrue% |
|
425 |
% |
|
426 |
\isamarkupsection{The Pure syntax \label{sec:pure-syntax}% |
|
427 |
} |
|
428 |
\isamarkuptrue% |
|
429 |
% |
|
430 |
\isamarkupsubsection{Priority grammars \label{sec:priority-grammar}% |
|
431 |
} |
|
432 |
\isamarkuptrue% |
|
433 |
% |
|
434 |
\begin{isamarkuptext}% |
|
435 |
A context-free grammar consists of a set of \emph{terminal |
|
436 |
symbols}, a set of \emph{nonterminal symbols} and a set of |
|
437 |
\emph{productions}. Productions have the form \isa{{\isachardoublequote}A\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}}, |
|
438 |
where \isa{A} is a nonterminal and \isa{{\isasymgamma}} is a string of |
|
439 |
terminals and nonterminals. One designated nonterminal is called |
|
440 |
the \emph{root symbol}. The language defined by the grammar |
|
441 |
consists of all strings of terminals that can be derived from the |
|
442 |
root symbol by applying productions as rewrite rules. |
|
443 |
||
444 |
The standard Isabelle parser for inner syntax uses a \emph{priority |
|
445 |
grammar}. Each nonterminal is decorated by an integer priority: |
|
446 |
\isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}}. In a derivation, \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}} may be rewritten |
|
447 |
using a production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup q\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}} only if \isa{{\isachardoublequote}p\ {\isasymle}\ q{\isachardoublequote}}. Any |
|
448 |
priority grammar can be translated into a normal context-free |
|
449 |
grammar by introducing new nonterminals and productions. |
|
450 |
||
451 |
\medskip Formally, a set of context free productions \isa{G} |
|
452 |
induces a derivation relation \isa{{\isachardoublequote}{\isasymlongrightarrow}\isactrlsub G{\isachardoublequote}} as follows. Let \isa{{\isasymalpha}} and \isa{{\isasymbeta}} denote strings of terminal or nonterminal symbols. |
|
453 |
Then \isa{{\isachardoublequote}{\isasymalpha}\ A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}\ {\isasymbeta}\ {\isasymlongrightarrow}\isactrlsub G\ {\isasymalpha}\ {\isasymgamma}\ {\isasymbeta}{\isachardoublequote}} holds if and only if \isa{G} |
|
454 |
contains some production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup q\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymgamma}{\isachardoublequote}} for \isa{{\isachardoublequote}p\ {\isasymle}\ q{\isachardoublequote}}. |
|
455 |
||
456 |
\medskip The following grammar for arithmetic expressions |
|
457 |
demonstrates how binding power and associativity of operators can be |
|
458 |
enforced by priorities. |
|
459 |
||
460 |
\begin{center} |
|
461 |
\begin{tabular}{rclr} |
|
462 |
\isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|(| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|)| \\ |
|
463 |
\isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|0| \\ |
|
464 |
\isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|+| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\ |
|
465 |
\isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|*| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\ |
|
466 |
\isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|-| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \\ |
|
467 |
\end{tabular} |
|
468 |
\end{center} |
|
469 |
The choice of priorities determines that \verb|-| binds |
|
470 |
tighter than \verb|*|, which binds tighter than \verb|+|. Furthermore \verb|+| associates to the left and |
|
471 |
\verb|*| to the right. |
|
472 |
||
473 |
\medskip For clarity, grammars obey these conventions: |
|
474 |
\begin{itemize} |
|
475 |
||
476 |
\item All priorities must lie between 0 and 1000. |
|
477 |
||
478 |
\item Priority 0 on the right-hand side and priority 1000 on the |
|
479 |
left-hand side may be omitted. |
|
480 |
||
481 |
\item The production \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}\ {\isacharequal}\ {\isasymalpha}{\isachardoublequote}} is written as \isa{{\isachardoublequote}A\ {\isacharequal}\ {\isasymalpha}\ {\isacharparenleft}p{\isacharparenright}{\isachardoublequote}}, i.e.\ the priority of the left-hand side actually appears in |
|
482 |
a column on the far right. |
|
483 |
||
484 |
\item Alternatives are separated by \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}}. |
|
485 |
||
486 |
\item Repetition is indicated by dots \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}{\isacharparenright}{\isachardoublequote}} in an informal |
|
487 |
but obvious way. |
|
488 |
||
489 |
\end{itemize} |
|
490 |
||
491 |
Using these conventions, the example grammar specification above |
|
492 |
takes the form: |
|
493 |
\begin{center} |
|
494 |
\begin{tabular}{rclc} |
|
495 |
\isa{A} & \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}} & \verb|(| \isa{A} \verb|)| \\ |
|
496 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|0| & \qquad\qquad \\ |
|
497 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{A} \verb|+| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ |
|
498 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|*| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ |
|
499 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|-| \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ |
|
500 |
\end{tabular} |
|
501 |
\end{center}% |
|
502 |
\end{isamarkuptext}% |
|
503 |
\isamarkuptrue% |
|
504 |
% |
|
505 |
\isamarkupsubsection{The Pure grammar% |
|
506 |
} |
|
507 |
\isamarkuptrue% |
|
508 |
% |
|
509 |
\begin{isamarkuptext}% |
|
510 |
The priority grammar of the \isa{{\isachardoublequote}Pure{\isachardoublequote}} theory is defined as follows: |
|
511 |
||
512 |
%FIXME syntax for "index" (?) |
|
513 |
%FIXME "op" versions of ==> etc. (?) |
|
514 |
||
515 |
\begin{center} |
|
516 |
\begin{supertabular}{rclr} |
|
517 |
||
518 |
\indexdef{inner}{syntax}{any}\hypertarget{syntax.inner.any}{\hyperlink{syntax.inner.any}{\mbox{\isa{any}}}} & = & \isa{{\isachardoublequote}prop\ \ {\isacharbar}\ \ logic{\isachardoublequote}} \\\\ |
|
519 |
||
520 |
\indexdef{inner}{syntax}{prop}\hypertarget{syntax.inner.prop}{\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}} & = & \verb|(| \isa{prop} \verb|)| \\ |
|
521 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{4}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ |
|
522 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=?=| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ |
|
523 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ |
|
524 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ |
|
28857 | 525 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|&&&| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}{\isacharparenright}{\isachardoublequote}} \\ |
28762 | 526 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ |
527 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{2}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ |
|
528 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[|\verb,|,\verb|| \isa{prop} \verb|;| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|;| \isa{prop} \verb||\verb,|,\verb|]| \verb|==>| \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ |
|
529 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlbrakk}{\isachardoublequote}} \isa{prop} \verb|;| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|;| \isa{prop} \isa{{\isachardoublequote}{\isasymrbrakk}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} \isa{{\isachardoublequote}prop\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}} \\ |
|
530 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|!!| \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ |
|
531 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}} \isa{idts} \verb|.| \isa{prop} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ |
|
532 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|OFCLASS| \verb|(| \isa{type} \verb|,| \isa{logic} \verb|)| \\ |
|
533 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|SORT_CONSTRAINT| \verb|(| \isa{type} \verb|)| \\ |
|
28857 | 534 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TERM| \isa{logic} \\ |
28762 | 535 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|PROP| \isa{aprop} \\\\ |
536 |
||
28857 | 537 |
\indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \verb|(| \isa{aprop} \verb|)| \\ |
538 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\ |
|
539 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\ |
|
28762 | 540 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\\\ |
541 |
||
542 |
\indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\ |
|
543 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{4}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ |
|
544 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ var\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|...| \\ |
|
28857 | 545 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|CONST| \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|CONST| \isa{{\isachardoublequote}longid{\isachardoublequote}} \\ |
28762 | 546 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}logic\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ \ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ {\isasymdots}\ any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}{\isachardoublequote}} \\ |
547 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|%| \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ |
|
548 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isasymlambda}} \isa{pttrns} \verb|.| \isa{{\isachardoublequote}any\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{3}}\isactrlsup {\isacharparenright}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{3}}{\isacharparenright}{\isachardoublequote}} \\ |
|
549 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\ |
|
550 |
||
551 |
\indexdef{inner}{syntax}{idt}\hypertarget{syntax.inner.idt}{\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}} & = & \verb|(| \isa{idt} \verb|)|\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\ |
|
552 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{id} \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ |
|
553 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|_| \verb|::| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ |
|
554 |
||
555 |
\indexdef{inner}{syntax}{idts}\hypertarget{syntax.inner.idts}{\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}} & = & \isa{{\isachardoublequote}idt\ \ {\isacharbar}\ \ idt\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}\ idts{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ |
|
556 |
||
557 |
\indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\ |
|
558 |
||
559 |
\indexdef{inner}{syntax}{pttrns}\hypertarget{syntax.inner.pttrns}{\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}}} & = & \isa{{\isachardoublequote}pttrn\ \ {\isacharbar}\ \ pttrn\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}\ pttrns{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ |
|
560 |
||
561 |
\indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\ |
|
562 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid\ \ {\isacharbar}\ \ tvar\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \\ |
|
563 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}tid{\isachardoublequote}} \verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ tvar\ \ {\isachardoublequote}}\verb|::| \isa{{\isachardoublequote}sort\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|_| \verb|::| \isa{{\isachardoublequote}sort{\isachardoublequote}} \\ |
|
564 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ id\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{id} \\ |
|
29746 | 565 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}longid\ \ {\isacharbar}\ \ type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isadigit{0}}\isactrlsup {\isacharparenright}\ longid{\isachardoublequote}} \\ |
566 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|(| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|)| \isa{longid} \\ |
|
28762 | 567 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ |
568 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}type\isactrlsup {\isacharparenleft}\isactrlsup {\isadigit{1}}\isactrlsup {\isacharparenright}{\isachardoublequote}} \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ |
|
569 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\ |
|
570 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|[| \isa{type} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{type} \verb|]| \isa{{\isachardoublequote}{\isasymRightarrow}{\isachardoublequote}} \isa{type} & \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{0}}{\isacharparenright}{\isachardoublequote}} \\\\ |
|
571 |
||
29746 | 572 |
\indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isachardoublequote}id\ \ {\isacharbar}\ \ longid\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|{}| \\ |
573 |
& \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \verb|{| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|,| \isa{{\isachardoublequote}{\isacharparenleft}id\ {\isacharbar}\ longid{\isacharparenright}{\isachardoublequote}} \verb|}| \\ |
|
28762 | 574 |
\end{supertabular} |
575 |
\end{center} |
|
576 |
||
577 |
\medskip Here literal terminals are printed \verb|verbatim|; |
|
578 |
see also \secref{sec:inner-lex} for further token categories of the |
|
579 |
inner syntax. The meaning of the nonterminals defined by the above |
|
580 |
grammar is as follows: |
|
581 |
||
582 |
\begin{description} |
|
583 |
||
584 |
\item \indexref{inner}{syntax}{any}\hyperlink{syntax.inner.any}{\mbox{\isa{any}}} denotes any term. |
|
585 |
||
586 |
\item \indexref{inner}{syntax}{prop}\hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} denotes meta-level propositions, |
|
587 |
which are terms of type \isa{prop}. The syntax of such formulae of |
|
588 |
the meta-logic is carefully distinguished from usual conventions for |
|
589 |
object-logics. In particular, plain \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-term notation is |
|
590 |
\emph{not} recognized as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}. |
|
591 |
||
592 |
\item \indexref{inner}{syntax}{aprop}\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}} denotes atomic propositions, which |
|
593 |
are embedded into regular \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}} by means of an |
|
594 |
explicit \verb|PROP| token. |
|
595 |
||
596 |
Terms of type \isa{prop} with non-constant head, e.g.\ a plain |
|
597 |
variable, are printed in this form. Constants that yield type \isa{prop} are expected to provide their own concrete syntax; otherwise |
|
598 |
the printed version will appear like \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} and |
|
599 |
cannot be parsed again as \hyperlink{syntax.inner.prop}{\mbox{\isa{prop}}}. |
|
600 |
||
601 |
\item \indexref{inner}{syntax}{logic}\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}} denotes arbitrary terms of a |
|
602 |
logical type, excluding type \isa{prop}. This is the main |
|
603 |
syntactic category of object-logic entities, covering plain \isa{{\isasymlambda}}-term notation (variables, abstraction, application), plus |
|
604 |
anything defined by the user. |
|
605 |
||
606 |
When specifying notation for logical entities, all logical types |
|
607 |
(excluding \isa{prop}) are \emph{collapsed} to this single category |
|
608 |
of \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}. |
|
609 |
||
610 |
\item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly |
|
611 |
constrained by types. |
|
612 |
||
613 |
\item \indexref{inner}{syntax}{idts}\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}} denotes a sequence of \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}. This is the most basic category for variables in |
|
614 |
iterated binders, such as \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}} or \isa{{\isachardoublequote}{\isasymAnd}{\isachardoublequote}}. |
|
615 |
||
616 |
\item \indexref{inner}{syntax}{pttrn}\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}} and \indexref{inner}{syntax}{pttrns}\hyperlink{syntax.inner.pttrns}{\mbox{\isa{pttrns}}} |
|
617 |
denote patterns for abstraction, cases bindings etc. In Pure, these |
|
618 |
categories start as a merely copy of \hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} and |
|
619 |
\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, respectively. Object-logics may add |
|
620 |
additional productions for binding forms. |
|
621 |
||
622 |
\item \indexref{inner}{syntax}{type}\hyperlink{syntax.inner.type}{\mbox{\isa{type}}} denotes types of the meta-logic. |
|
623 |
||
624 |
\item \indexref{inner}{syntax}{sort}\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}} denotes meta-level sorts. |
|
625 |
||
626 |
\end{description} |
|
627 |
||
628 |
Here are some further explanations of certain syntax features. |
|
629 |
||
630 |
\begin{itemize} |
|
631 |
||
632 |
\item In \hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}, note that \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ nat\ y{\isachardoublequote}} is |
|
633 |
parsed as \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}nat\ y{\isacharparenright}{\isachardoublequote}}, treating \isa{y} like a type |
|
634 |
constructor applied to \isa{nat}. To avoid this interpretation, |
|
635 |
write \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ y{\isachardoublequote}} with explicit parentheses. |
|
636 |
||
637 |
\item Similarly, \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ nat\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} is parsed as \isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}nat\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}. The correct form is \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}, or \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} if \isa{y} is last in the |
|
638 |
sequence of identifiers. |
|
639 |
||
640 |
\item Type constraints for terms bind very weakly. For example, |
|
641 |
\isa{{\isachardoublequote}x\ {\isacharless}\ y\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}} is normally parsed as \isa{{\isachardoublequote}{\isacharparenleft}x\ {\isacharless}\ y{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ nat{\isachardoublequote}}, unless \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}} has a very low priority, in which case the |
|
642 |
input is likely to be ambiguous. The correct form is \isa{{\isachardoublequote}x\ {\isacharless}\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ nat{\isacharparenright}{\isachardoublequote}}. |
|
643 |
||
644 |
\item Constraints may be either written with two literal colons |
|
645 |
``\verb|::|'' or the double-colon symbol \verb|\<Colon>|, |
|
646 |
which actually looks exactly the same in some {\LaTeX} styles. |
|
647 |
||
648 |
\item Dummy variables (written as underscore) may occur in different |
|
649 |
roles. |
|
650 |
||
651 |
\begin{description} |
|
652 |
||
653 |
\item A type ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}{\isacharunderscore}\ {\isacharcolon}{\isacharcolon}\ sort{\isachardoublequote}}'' acts like an |
|
654 |
anonymous inference parameter, which is filled-in according to the |
|
655 |
most general type produced by the type-checking phase. |
|
656 |
||
657 |
\item A bound ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to a vacuous abstraction, where |
|
658 |
the body does not refer to the binding introduced here. As in the |
|
659 |
term \isa{{\isachardoublequote}{\isasymlambda}x\ {\isacharunderscore}{\isachardot}\ x{\isachardoublequote}}, which is \isa{{\isachardoublequote}{\isasymalpha}{\isachardoublequote}}-equivalent to \isa{{\isachardoublequote}{\isasymlambda}x\ y{\isachardot}\ x{\isachardoublequote}}. |
|
660 |
||
661 |
\item A free ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' refers to an implicit outer binding. |
|
662 |
Higher definitional packages usually allow forms like \isa{{\isachardoublequote}f\ x\ {\isacharunderscore}\ {\isacharequal}\ x{\isachardoublequote}}. |
|
663 |
||
664 |
\item A schematic ``\isa{{\isachardoublequote}{\isacharunderscore}{\isachardoublequote}}'' (within a term pattern, see |
|
665 |
\secref{sec:term-decls}) refers to an anonymous variable that is |
|
666 |
implicitly abstracted over its context of locally bound variables. |
|
667 |
For example, this allows pattern matching of \isa{{\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ f\ x\ {\isacharequal}\ g\ x{\isacharbraceright}{\isachardoublequote}} against \isa{{\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharunderscore}{\isacharbraceright}{\isachardoublequote}}, or even \isa{{\isachardoublequote}{\isacharbraceleft}{\isacharunderscore}{\isachardot}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharunderscore}{\isacharbraceright}{\isachardoublequote}} by |
|
668 |
using both bound and schematic dummies. |
|
669 |
||
670 |
\end{description} |
|
671 |
||
672 |
\item The three literal dots ``\verb|...|'' may be also |
|
673 |
written as ellipsis symbol \verb|\<dots>|. In both cases this |
|
674 |
refers to a special schematic variable, which is bound in the |
|
675 |
context. This special term abbreviation works nicely with |
|
676 |
calculational reasoning (\secref{sec:calculation}). |
|
677 |
||
678 |
\end{itemize}% |
|
679 |
\end{isamarkuptext}% |
|
680 |
\isamarkuptrue% |
|
681 |
% |
|
682 |
\isamarkupsection{Lexical matters \label{sec:inner-lex}% |
|
683 |
} |
|
684 |
\isamarkuptrue% |
|
685 |
% |
|
686 |
\begin{isamarkuptext}% |
|
687 |
The inner lexical syntax vaguely resembles the outer one |
|
688 |
(\secref{sec:outer-lex}), but some details are different. There are |
|
689 |
two main categories of inner syntax tokens: |
|
690 |
||
691 |
\begin{enumerate} |
|
692 |
||
693 |
\item \emph{delimiters} --- the literal tokens occurring in |
|
694 |
productions of the given priority grammar (cf.\ |
|
695 |
\secref{sec:priority-grammar}); |
|
696 |
||
697 |
\item \emph{named tokens} --- various categories of identifiers etc. |
|
698 |
||
699 |
\end{enumerate} |
|
700 |
||
701 |
Delimiters override named tokens and may thus render certain |
|
702 |
identifiers inaccessible. Sometimes the logical context admits |
|
703 |
alternative ways to refer to the same entity, potentially via |
|
704 |
qualified names. |
|
705 |
||
706 |
\medskip The categories for named tokens are defined once and for |
|
707 |
all as follows, reusing some categories of the outer token syntax |
|
708 |
(\secref{sec:outer-lex}). |
|
709 |
||
710 |
\begin{center} |
|
711 |
\begin{supertabular}{rcl} |
|
712 |
\indexdef{inner}{syntax}{id}\hypertarget{syntax.inner.id}{\hyperlink{syntax.inner.id}{\mbox{\isa{id}}}} & = & \indexref{}{syntax}{ident}\hyperlink{syntax.ident}{\mbox{\isa{ident}}} \\ |
|
713 |
\indexdef{inner}{syntax}{longid}\hypertarget{syntax.inner.longid}{\hyperlink{syntax.inner.longid}{\mbox{\isa{longid}}}} & = & \indexref{}{syntax}{longident}\hyperlink{syntax.longident}{\mbox{\isa{longident}}} \\ |
|
714 |
\indexdef{inner}{syntax}{var}\hypertarget{syntax.inner.var}{\hyperlink{syntax.inner.var}{\mbox{\isa{var}}}} & = & \indexref{}{syntax}{var}\hyperlink{syntax.var}{\mbox{\isa{var}}} \\ |
|
715 |
\indexdef{inner}{syntax}{tid}\hypertarget{syntax.inner.tid}{\hyperlink{syntax.inner.tid}{\mbox{\isa{tid}}}} & = & \indexref{}{syntax}{typefree}\hyperlink{syntax.typefree}{\mbox{\isa{typefree}}} \\ |
|
716 |
\indexdef{inner}{syntax}{tvar}\hypertarget{syntax.inner.tvar}{\hyperlink{syntax.inner.tvar}{\mbox{\isa{tvar}}}} & = & \indexref{}{syntax}{typevar}\hyperlink{syntax.typevar}{\mbox{\isa{typevar}}} \\ |
|
717 |
\indexdef{inner}{syntax}{num}\hypertarget{syntax.inner.num}{\hyperlink{syntax.inner.num}{\mbox{\isa{num}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ |
|
29158 | 718 |
\indexdef{inner}{syntax}{float\_token}\hypertarget{syntax.inner.float-token}{\hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}} & = & \indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\verb|.|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ |
28762 | 719 |
\indexdef{inner}{syntax}{xnum}\hypertarget{syntax.inner.xnum}{\hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}} & = & \verb|#|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}}\isa{{\isachardoublequote}\ \ {\isacharbar}\ \ {\isachardoublequote}}\verb|#-|\indexref{}{syntax}{nat}\hyperlink{syntax.nat}{\mbox{\isa{nat}}} \\ |
720 |
||
721 |
\indexdef{inner}{syntax}{xstr}\hypertarget{syntax.inner.xstr}{\hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}}} & = & \verb|''| \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}} \verb|''| \\ |
|
722 |
\end{supertabular} |
|
723 |
\end{center} |
|
724 |
||
29158 | 725 |
The token categories \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, \hyperlink{syntax.inner.xnum}{\mbox{\isa{xnum}}}, and \hyperlink{syntax.inner.xstr}{\mbox{\isa{xstr}}} are |
726 |
not used in Pure. Object-logics may implement numerals and string |
|
727 |
constants by adding appropriate syntax declarations, together with |
|
728 |
some translation functions (e.g.\ see Isabelle/HOL). |
|
729 |
||
730 |
The derived categories \indexdef{inner}{syntax}{num\_const}\hypertarget{syntax.inner.num-const}{\hyperlink{syntax.inner.num-const}{\mbox{\isa{num{\isacharunderscore}const}}}} and |
|
731 |
\indexdef{inner}{syntax}{float\_const}\hypertarget{syntax.inner.float-const}{\hyperlink{syntax.inner.float-const}{\mbox{\isa{float{\isacharunderscore}const}}}} provide robust access to \hyperlink{syntax.inner.num}{\mbox{\isa{num}}}, and \hyperlink{syntax.inner.float-token}{\mbox{\isa{float{\isacharunderscore}token}}}, respectively: the |
|
732 |
syntax tree holds a syntactic constant instead of a free variable.% |
|
28762 | 733 |
\end{isamarkuptext}% |
734 |
\isamarkuptrue% |
|
735 |
% |
|
736 |
\isamarkupsection{Syntax and translations \label{sec:syn-trans}% |
|
737 |
} |
|
738 |
\isamarkuptrue% |
|
739 |
% |
|
740 |
\begin{isamarkuptext}% |
|
741 |
\begin{matharray}{rcl} |
|
742 |
\indexdef{}{command}{nonterminals}\hypertarget{command.nonterminals}{\hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
743 |
\indexdef{}{command}{syntax}\hypertarget{command.syntax}{\hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
744 |
\indexdef{}{command}{no\_syntax}\hypertarget{command.no-syntax}{\hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
745 |
\indexdef{}{command}{translations}\hypertarget{command.translations}{\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
746 |
\indexdef{}{command}{no\_translations}\hypertarget{command.no-translations}{\hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
747 |
\end{matharray} |
|
748 |
||
749 |
\begin{rail} |
|
750 |
'nonterminals' (name +) |
|
751 |
; |
|
752 |
('syntax' | 'no\_syntax') mode? (constdecl +) |
|
753 |
; |
|
754 |
('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) |
|
755 |
; |
|
756 |
||
757 |
mode: ('(' ( name | 'output' | name 'output' ) ')') |
|
758 |
; |
|
759 |
transpat: ('(' nameref ')')? string |
|
760 |
; |
|
761 |
\end{rail} |
|
762 |
||
763 |
\begin{description} |
|
764 |
||
765 |
\item \hyperlink{command.nonterminals}{\mbox{\isa{\isacommand{nonterminals}}}}~\isa{c} declares a type |
|
766 |
constructor \isa{c} (without arguments) to act as purely syntactic |
|
767 |
type: a nonterminal symbol of the inner syntax. |
|
768 |
||
769 |
\item \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} is similar to |
|
770 |
\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{decls}, except that the actual logical |
|
771 |
signature extension is omitted. Thus the context free grammar of |
|
772 |
Isabelle's inner syntax may be augmented in arbitrary ways, |
|
773 |
independently of the logic. The \isa{mode} argument refers to the |
|
774 |
print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}} indicator is given, all productions are added both to the |
|
775 |
input and output grammar. |
|
776 |
||
777 |
\item \hyperlink{command.no-syntax}{\mbox{\isa{\isacommand{no{\isacharunderscore}syntax}}}}~\isa{{\isachardoublequote}{\isacharparenleft}mode{\isacharparenright}\ decls{\isachardoublequote}} removes grammar |
|
778 |
declarations (and translations) resulting from \isa{decls}, which |
|
779 |
are interpreted in the same manner as for \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} above. |
|
780 |
||
781 |
\item \hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}}~\isa{rules} specifies syntactic |
|
782 |
translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isachardoublequote}{\isasymrightleftharpoons}{\isachardoublequote}}), |
|
783 |
parse rules (\isa{{\isachardoublequote}{\isasymrightharpoonup}{\isachardoublequote}}), or print rules (\isa{{\isachardoublequote}{\isasymleftharpoondown}{\isachardoublequote}}). |
|
784 |
Translation patterns may be prefixed by the syntactic category to be |
|
785 |
used for parsing; the default is \isa{logic}. |
|
786 |
||
787 |
\item \hyperlink{command.no-translations}{\mbox{\isa{\isacommand{no{\isacharunderscore}translations}}}}~\isa{rules} removes syntactic |
|
788 |
translation rules, which are interpreted in the same manner as for |
|
789 |
\hyperlink{command.translations}{\mbox{\isa{\isacommand{translations}}}} above. |
|
790 |
||
791 |
\end{description}% |
|
792 |
\end{isamarkuptext}% |
|
793 |
\isamarkuptrue% |
|
794 |
% |
|
795 |
\isamarkupsection{Syntax translation functions \label{sec:tr-funs}% |
|
796 |
} |
|
797 |
\isamarkuptrue% |
|
798 |
% |
|
799 |
\begin{isamarkuptext}% |
|
800 |
\begin{matharray}{rcl} |
|
801 |
\indexdef{}{command}{parse\_ast\_translation}\hypertarget{command.parse-ast-translation}{\hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
802 |
\indexdef{}{command}{parse\_translation}\hypertarget{command.parse-translation}{\hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
803 |
\indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
804 |
\indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
805 |
\indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
806 |
\end{matharray} |
|
807 |
||
808 |
\begin{rail} |
|
809 |
( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | |
|
810 |
'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text |
|
811 |
; |
|
812 |
\end{rail} |
|
813 |
||
814 |
Syntax translation functions written in ML admit almost arbitrary |
|
815 |
manipulations of Isabelle's inner syntax. Any of the above commands |
|
816 |
have a single \railqtok{text} argument that refers to an ML |
|
817 |
expression of appropriate type, which are as follows by default: |
|
818 |
||
819 |
%FIXME proper antiquotations |
|
820 |
\begin{ttbox} |
|
821 |
val parse_ast_translation : (string * (ast list -> ast)) list |
|
822 |
val parse_translation : (string * (term list -> term)) list |
|
823 |
val print_translation : (string * (term list -> term)) list |
|
824 |
val typed_print_translation : |
|
825 |
(string * (bool -> typ -> term list -> term)) list |
|
826 |
val print_ast_translation : (string * (ast list -> ast)) list |
|
827 |
\end{ttbox} |
|
828 |
||
829 |
If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding |
|
830 |
translation functions may depend on the current theory or proof |
|
831 |
context. This allows to implement advanced syntax mechanisms, as |
|
832 |
translations functions may refer to specific theory declarations or |
|
833 |
auxiliary proof data. |
|
834 |
||
30397 | 835 |
See also \cite{isabelle-ref} for more information on the general |
836 |
concept of syntax transformations in Isabelle. |
|
28762 | 837 |
|
838 |
%FIXME proper antiquotations |
|
839 |
\begin{ttbox} |
|
840 |
val parse_ast_translation: |
|
841 |
(string * (Proof.context -> ast list -> ast)) list |
|
842 |
val parse_translation: |
|
843 |
(string * (Proof.context -> term list -> term)) list |
|
844 |
val print_translation: |
|
845 |
(string * (Proof.context -> term list -> term)) list |
|
846 |
val typed_print_translation: |
|
847 |
(string * (Proof.context -> bool -> typ -> term list -> term)) list |
|
848 |
val print_ast_translation: |
|
849 |
(string * (Proof.context -> ast list -> ast)) list |
|
850 |
\end{ttbox}% |
|
851 |
\end{isamarkuptext}% |
|
852 |
\isamarkuptrue% |
|
853 |
% |
|
854 |
\isamarkupsection{Inspecting the syntax% |
|
855 |
} |
|
856 |
\isamarkuptrue% |
|
857 |
% |
|
858 |
\begin{isamarkuptext}% |
|
859 |
\begin{matharray}{rcl} |
|
860 |
\indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
861 |
\end{matharray} |
|
862 |
||
863 |
\begin{description} |
|
864 |
||
865 |
\item \hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}} prints the inner syntax of the |
|
866 |
current context. The output can be quite large; the most important |
|
867 |
sections are explained below. |
|
868 |
||
869 |
\begin{description} |
|
870 |
||
871 |
\item \isa{{\isachardoublequote}lexicon{\isachardoublequote}} lists the delimiters of the inner token |
|
872 |
language; see \secref{sec:inner-lex}. |
|
873 |
||
874 |
\item \isa{{\isachardoublequote}prods{\isachardoublequote}} lists the productions of the underlying |
|
875 |
priority grammar; see \secref{sec:priority-grammar}. |
|
876 |
||
877 |
The nonterminal \isa{{\isachardoublequote}A\isactrlsup {\isacharparenleft}\isactrlsup p\isactrlsup {\isacharparenright}{\isachardoublequote}} is rendered in plain text as \isa{{\isachardoublequote}A{\isacharbrackleft}p{\isacharbrackright}{\isachardoublequote}}; delimiters are quoted. Many productions have an extra |
|
878 |
\isa{{\isachardoublequote}{\isasymdots}\ {\isacharequal}{\isachargreater}\ name{\isachardoublequote}}. These names later become the heads of parse |
|
879 |
trees; they also guide the pretty printer. |
|
880 |
||
881 |
Productions without such parse tree names are called \emph{copy |
|
882 |
productions}. Their right-hand side must have exactly one |
|
883 |
nonterminal symbol (or named token). The parser does not create a |
|
884 |
new parse tree node for copy productions, but simply returns the |
|
885 |
parse tree of the right-hand symbol. |
|
886 |
||
887 |
If the right-hand side of a copy production consists of a single |
|
888 |
nonterminal without any delimiters, then it is called a \emph{chain |
|
889 |
production}. Chain productions act as abbreviations: conceptually, |
|
890 |
they are removed from the grammar by adding new productions. |
|
891 |
Priority information attached to chain productions is ignored; only |
|
892 |
the dummy value \isa{{\isachardoublequote}{\isacharminus}{\isadigit{1}}{\isachardoublequote}} is displayed. |
|
893 |
||
28857 | 894 |
\item \isa{{\isachardoublequote}print\ modes{\isachardoublequote}} lists the alternative print modes |
28762 | 895 |
provided by this grammar; see \secref{sec:print-modes}. |
896 |
||
897 |
\item \isa{{\isachardoublequote}parse{\isacharunderscore}rules{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}rules{\isachardoublequote}} relate to |
|
898 |
syntax translations (macros); see \secref{sec:syn-trans}. |
|
899 |
||
900 |
\item \isa{{\isachardoublequote}parse{\isacharunderscore}ast{\isacharunderscore}translation{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}ast{\isacharunderscore}translation{\isachardoublequote}} list sets of constants that invoke |
|
901 |
translation functions for abstract syntax trees, which are only |
|
902 |
required in very special situations; see \secref{sec:tr-funs}. |
|
903 |
||
904 |
\item \isa{{\isachardoublequote}parse{\isacharunderscore}translation{\isachardoublequote}} and \isa{{\isachardoublequote}print{\isacharunderscore}translation{\isachardoublequote}} |
|
905 |
list the sets of constants that invoke regular translation |
|
906 |
functions; see \secref{sec:tr-funs}. |
|
907 |
||
908 |
\end{description} |
|
909 |
||
910 |
\end{description}% |
|
911 |
\end{isamarkuptext}% |
|
912 |
\isamarkuptrue% |
|
913 |
% |
|
914 |
\isadelimtheory |
|
915 |
% |
|
916 |
\endisadelimtheory |
|
917 |
% |
|
918 |
\isatagtheory |
|
919 |
\isacommand{end}\isamarkupfalse% |
|
920 |
% |
|
921 |
\endisatagtheory |
|
922 |
{\isafoldtheory}% |
|
923 |
% |
|
924 |
\isadelimtheory |
|
925 |
% |
|
926 |
\endisadelimtheory |
|
927 |
\isanewline |
|
928 |
\end{isabellebody}% |
|
929 |
%%% Local Variables: |
|
930 |
%%% mode: latex |
|
931 |
%%% TeX-master: "root" |
|
932 |
%%% End: |