7046
|
1 |
|
|
2 |
\chapter{Common Isar elements}
|
|
3 |
|
7134
|
4 |
FIXME $*$ indicates \emph{improper commands}
|
|
5 |
|
|
6 |
\section{Theory commands}
|
|
7 |
|
|
8 |
\subsection{Defining theories}
|
|
9 |
|
|
10 |
\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
|
|
11 |
\begin{matharray}{rcl}
|
|
12 |
\isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
|
|
13 |
\isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
|
|
14 |
\isarcmd{end} & : & \isartrans{theory}{\cdot} \\
|
|
15 |
\end{matharray}
|
|
16 |
|
|
17 |
Isabelle/Isar ``new-style'' theories are either defined via theory files or
|
|
18 |
interactively.\footnote{In contrast, ``old-style'' Isabelle theories support
|
|
19 |
batch processing only, with only the ML proof script part suitable for
|
|
20 |
interaction.}
|
|
21 |
|
|
22 |
The first command of any theory has to be $\THEORY$, starting a new theory
|
|
23 |
based on the merge of existing ones. In interactive experiments, the theory
|
|
24 |
context may be changed by $\CONTEXT$ without creating a new theory. In both
|
|
25 |
cases the concluding command is $\END$, which has to be the very last one of
|
|
26 |
any proper theory file.
|
|
27 |
|
|
28 |
\begin{rail}
|
|
29 |
'theory' name '=' (name + '+') filespecs? ':'
|
|
30 |
;
|
|
31 |
'context' name
|
|
32 |
;
|
|
33 |
'end'
|
|
34 |
;;
|
|
35 |
|
|
36 |
filespecs : 'files' ((name | '(' name ')') +);
|
|
37 |
\end{rail}
|
|
38 |
|
|
39 |
\begin{description}
|
|
40 |
\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
|
|
41 |
existing ones $B@1 + \cdots + B@n$. Note that Isabelle's theory loader
|
|
42 |
system ensures that any of the base theories are properly loaded (and fully
|
|
43 |
up-to-date when $\THEORY$ is executed interactively).
|
|
44 |
|
|
45 |
\item [$\CONTEXT~B$] enters existing theory context $B$, basically in
|
|
46 |
read-only mode, so only a limited set of commands may be performed. Just as
|
|
47 |
for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
|
|
48 |
|
|
49 |
\item [$\END$] concludes the current theory definition of context switch.
|
|
50 |
\end{description}
|
|
51 |
|
|
52 |
|
|
53 |
\subsection{Formal comments}
|
|
54 |
|
|
55 |
\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{subsection}\indexisarcmd{subsubsection}
|
|
56 |
\indexisarcmd{text}\indexisarcmd{txt}
|
|
57 |
\begin{matharray}{rcl}
|
|
58 |
\isarcmd{title} & : & \isartrans{theory}{theory} \\
|
|
59 |
\isarcmd{chapter} & : & \isartrans{theory}{theory} \\
|
|
60 |
\isarcmd{subsection} & : & \isartrans{theory}{theory} \\
|
|
61 |
\isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
|
|
62 |
\isarcmd{text} & : & \isartrans{theory}{theory} \\
|
|
63 |
\isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
64 |
\end{matharray}
|
|
65 |
|
|
66 |
There are several commands to include \emph{formal comments} in theory and
|
|
67 |
proof specification. In contrast to source-level comments
|
|
68 |
\verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text
|
|
69 |
given as formal comment is meant to be part of the actual document.
|
|
70 |
Consequently, it would be included in the final printed version.
|
|
71 |
|
|
72 |
Apart from plain prose, formal comments may also refer to logical entities of
|
|
73 |
the current theory context (types, terms, theorems etc.). Proper processing
|
|
74 |
of the text would then include some further consistency checks with the items
|
|
75 |
declared in the current theory, e.g.\ type-checking of included terms.
|
|
76 |
\footnote{The current version of Isabelle/Isar does not process formal
|
|
77 |
comments in any such way. This will be available as part of the automatic
|
|
78 |
theory and proof document preparation system (via (PDF)LaTeX) that is
|
|
79 |
planned for the near future.}
|
|
80 |
|
|
81 |
\begin{rail}
|
|
82 |
'title' text text? text?
|
|
83 |
;
|
|
84 |
'chapter' text
|
|
85 |
;
|
|
86 |
'subsection' text
|
|
87 |
;
|
|
88 |
'subsubsection' text
|
|
89 |
;
|
|
90 |
'text' text
|
|
91 |
;
|
|
92 |
'txt' text
|
|
93 |
;
|
|
94 |
\end{rail}
|
|
95 |
|
|
96 |
\begin{description}
|
|
97 |
\item [$\isarkeyword{title}~title~author~date$] specifies the document title
|
|
98 |
just as in typical LaTeX documents.
|
|
99 |
\item [$\isarkeyword{chapter}~text$, $\isarkeyword{subsection}~text$,
|
|
100 |
$\isarkeyword{subsubsection}~text$] specify chapter and subsection headings.
|
|
101 |
\item [$\TEXT~text$] specifies an actual body of prose text, including
|
|
102 |
references to formal entities.\footnote{The latter feature is not yet
|
|
103 |
exploited in any way.}
|
|
104 |
\item [$\TXT~text$] is similar to $\TEXT$, but may appear within proofs.
|
|
105 |
\end{description}
|
|
106 |
|
|
107 |
|
7135
|
108 |
\subsection{Type classes and sorts}\label{sec:classes}
|
7134
|
109 |
|
|
110 |
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
|
|
111 |
\begin{matharray}{rcl}
|
|
112 |
\isarcmd{classes} & : & \isartrans{theory}{theory} \\
|
|
113 |
\isarcmd{classrel} & : & \isartrans{theory}{theory} \\
|
|
114 |
\isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
|
|
115 |
\end{matharray}
|
|
116 |
|
|
117 |
\begin{rail}
|
7135
|
118 |
'classes' (classdecl +)
|
7134
|
119 |
;
|
|
120 |
'classrel' nameref '<' nameref comment?
|
|
121 |
;
|
|
122 |
'defaultsort' sort comment?
|
|
123 |
;
|
|
124 |
\end{rail}
|
|
125 |
|
|
126 |
\begin{description}
|
|
127 |
\item [$\isarkeyword{classes}~c<cs ~\dots$] declares class $c$ to be a
|
|
128 |
subclass of existing classes $cs$. Cyclic class structures are ruled out.
|
|
129 |
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
|
|
130 |
existing classes $c@1$ and $c@2$. This is done axiomatically! The
|
|
131 |
$\isarkeyword{instance}$ command provides a way introduce proven class
|
|
132 |
relations (see \S\ref{sec:axclass}).
|
|
133 |
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
|
|
134 |
any type variables input without sort constraints. Typically, the default
|
|
135 |
sort would be only changed when defining new logics.
|
|
136 |
\end{description}
|
|
137 |
|
|
138 |
|
7141
|
139 |
\subsection{Types}\label{sec:types-pure}
|
7134
|
140 |
|
|
141 |
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
|
|
142 |
\begin{matharray}{rcl}
|
|
143 |
\isarcmd{types} & : & \isartrans{theory}{theory} \\
|
|
144 |
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
|
|
145 |
\isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
|
|
146 |
\isarcmd{arities} & : & \isartrans{theory}{theory} \\
|
|
147 |
\end{matharray}
|
|
148 |
|
|
149 |
\begin{rail}
|
|
150 |
'types' (typespec '=' type infix? comment? +)
|
|
151 |
;
|
|
152 |
'typedecl' typespec infix? comment?
|
|
153 |
;
|
|
154 |
'nonterminals' (name +) comment?
|
|
155 |
;
|
|
156 |
'arities' (nameref '::' arity comment? +)
|
|
157 |
;
|
|
158 |
\end{rail}
|
|
159 |
|
|
160 |
\begin{description}
|
|
161 |
\item [$\TYPES~(\vec\alpha)t = \tau~\dots$] introduces \emph{type synonym}
|
|
162 |
$(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions,
|
|
163 |
as are available in Isabelle/HOL for example, type synonyms are just purely
|
|
164 |
syntactic abbreviations, without any logical significance. Internally, type
|
|
165 |
synonyms are fully expanded, as may be observed when printing terms or
|
|
166 |
theorems.
|
|
167 |
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
|
|
168 |
$t$, intended as an actual logical type. Note that some logics such as
|
|
169 |
Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.
|
|
170 |
\item [$\isarkeyword{nonterminals}~c~\dots$] declares $0$-ary type
|
|
171 |
constructors $c$ to act as purely syntactic types, i.e.\ nonterminal symbols
|
|
172 |
of Isabelle's inner syntax of terms or types.
|
|
173 |
\item [$\isarkeyword{arities}~t::(\vec s)s~\dots$] augments Isabelle's
|
|
174 |
order-sorted signature of types by new type constructor arities. This is
|
|
175 |
done axiomatically! The $\isarkeyword{instance}$ command provides a way
|
|
176 |
introduce proven type arities (see \S\ref{sec:axclass}).
|
|
177 |
\end{description}
|
|
178 |
|
|
179 |
|
|
180 |
\subsection{Constants and simple definitions}
|
|
181 |
|
|
182 |
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}
|
|
183 |
\begin{matharray}{rcl}
|
|
184 |
\isarcmd{consts} & : & \isartrans{theory}{theory} \\
|
|
185 |
\isarcmd{defs} & : & \isartrans{theory}{theory} \\
|
|
186 |
\isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
|
|
187 |
\end{matharray}
|
|
188 |
|
|
189 |
\begin{rail}
|
|
190 |
'consts' (constdecl +)
|
|
191 |
;
|
|
192 |
'defs' (thmdecl? prop comment? +)
|
|
193 |
;
|
|
194 |
'constdefs' (constdecl prop comment? +)
|
|
195 |
;
|
|
196 |
|
|
197 |
constdecl: name '::' type mixfix? comment?
|
|
198 |
;
|
|
199 |
\end{rail}
|
|
200 |
|
|
201 |
\begin{description}
|
|
202 |
\item [$\CONSTS~c::\tau~\dots$] declares constant $c$ to have any instance of
|
|
203 |
type scheme $\tau$. The optional mixfix annotations may attach concrete
|
|
204 |
syntax to the constant.
|
|
205 |
\item [$\DEFS~name: eqn~\dots$] introduces $eqn$ as a definitional axiom for
|
|
206 |
some existing constant. See \cite[\S6]{isabelle-ref} for more details on
|
|
207 |
the form of equations admitted as constant definitions.
|
|
208 |
\item [$\isarkeyword{constdefs}~c::\tau~eqn~\dots$] combines constant
|
|
209 |
declarations and definitions, using canonical name $c_def$ for the
|
|
210 |
definitional axiom.
|
|
211 |
\end{description}
|
|
212 |
|
|
213 |
|
|
214 |
\subsection{Concrete syntax}
|
|
215 |
|
|
216 |
\indexisarcmd{syntax}\indexisarcmd{translations}
|
|
217 |
\begin{matharray}{rcl}
|
|
218 |
\isarcmd{syntax} & : & \isartrans{theory}{theory} \\
|
|
219 |
\isarcmd{translations} & : & \isartrans{theory}{theory} \\
|
|
220 |
\end{matharray}
|
|
221 |
|
|
222 |
\begin{rail}
|
|
223 |
'syntax' ('(' name 'output'? ')')? (constdecl +)
|
|
224 |
;
|
|
225 |
'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
|
|
226 |
;
|
|
227 |
transpat: ('(' nameref ')')? string
|
|
228 |
;
|
|
229 |
\end{rail}
|
|
230 |
|
|
231 |
\begin{description}
|
|
232 |
\item [$\isarkeyword{syntax}~mode~decls$] is similar to $\CONSTS~decls$,
|
|
233 |
except the actual logical signature extension. Thus the context free
|
|
234 |
grammar of Isabelle's inner syntax may be augmented in arbitrary ways. The
|
|
235 |
$mode$ argument refers to the print mode that the grammar rules belong;
|
|
236 |
unless there is the \texttt{output} flag given, all productions are added
|
|
237 |
both to the input and output grammar.
|
|
238 |
\item [$\isarkeyword{translations}~rule~\dots$] specifies syntactic
|
|
239 |
translation rules (macros): parse/print rules (\texttt{==}), parse rules
|
|
240 |
(\texttt{=>}), print rules (\texttt{<=}). Translation patterns may be
|
|
241 |
prefixed by the syntactic category to be used for parsing; the default is
|
|
242 |
\texttt{logic}.
|
|
243 |
\end{description}
|
|
244 |
|
|
245 |
|
|
246 |
\subsection{Axioms and theorems}
|
|
247 |
|
|
248 |
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
|
|
249 |
\begin{matharray}{rcl}
|
|
250 |
\isarcmd{axioms} & : & \isartrans{theory}{theory} \\
|
|
251 |
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\
|
|
252 |
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
|
|
253 |
\end{matharray}
|
|
254 |
|
|
255 |
\begin{rail}
|
7135
|
256 |
'axioms' (axmdecl prop comment? +)
|
7134
|
257 |
;
|
|
258 |
('theorems' | 'lemmas') thmdef? thmrefs
|
|
259 |
;
|
|
260 |
\end{rail}
|
|
261 |
|
|
262 |
\begin{description}
|
|
263 |
\item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary
|
|
264 |
statements as logical axioms. In fact, axioms are ``axiomatic theorems'',
|
|
265 |
and may be referred as any other theorems later.
|
|
266 |
|
|
267 |
Axioms are usually only introduced when declaring new logical systems.
|
|
268 |
Everyday work is normally done the hard way, with proper definitions and
|
|
269 |
actual theorems.
|
|
270 |
\item [$\isarkeyword{theorems}~name = thms$] stores lists of existing theorems
|
|
271 |
as $name$. Typical applications would also involve attributes to augment
|
|
272 |
the default simpset, for example.
|
|
273 |
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
|
|
274 |
tags the results as ``lemma''.
|
|
275 |
\end{description}
|
|
276 |
|
|
277 |
|
|
278 |
\subsection{Manipulating name spaces}
|
|
279 |
|
|
280 |
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{path}
|
|
281 |
\begin{matharray}{rcl}
|
|
282 |
\isarcmd{global} & : & \isartrans{theory}{theory} \\
|
|
283 |
\isarcmd{local} & : & \isartrans{theory}{theory} \\
|
|
284 |
\isarcmd{path} & : & \isartrans{theory}{theory} \\
|
|
285 |
\end{matharray}
|
|
286 |
|
|
287 |
\begin{rail}
|
|
288 |
'global'
|
|
289 |
;
|
|
290 |
'local'
|
|
291 |
;
|
|
292 |
'path' nameref
|
|
293 |
;
|
|
294 |
\end{rail}
|
|
295 |
|
|
296 |
\begin{description}
|
|
297 |
\item [$\isarkeyword{global}$] FIXME
|
|
298 |
\item [$\isarkeyword{local}$] FIXME
|
|
299 |
\item [$\isarkeyword{path}~name$] FIXME
|
|
300 |
\end{description}
|
|
301 |
|
|
302 |
|
|
303 |
\subsection{Incorporating ML code}
|
|
304 |
|
|
305 |
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}
|
|
306 |
\begin{matharray}{rcl}
|
|
307 |
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
|
|
308 |
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
|
|
309 |
\isarcmd{setup} & : & \isartrans{\cdot}{\cdot} \\
|
|
310 |
\end{matharray}
|
|
311 |
|
|
312 |
\begin{rail}
|
|
313 |
'use' name
|
|
314 |
;
|
|
315 |
'ML' text
|
|
316 |
;
|
|
317 |
'setup' text
|
|
318 |
;
|
|
319 |
\end{rail}
|
|
320 |
|
|
321 |
\begin{description}
|
|
322 |
\item [$\isarkeyword{use}~file$] FIXME
|
|
323 |
\item [$\isarkeyword{ML}~text$] FIXME
|
|
324 |
\item [$\isarkeyword{setup}~text$] FIXME
|
|
325 |
\end{description}
|
|
326 |
|
|
327 |
|
|
328 |
\subsection{ML translation functions}
|
|
329 |
|
7141
|
330 |
\indexisarcmd{parse\_ast\_translation}\indexisarcmd{parse\_translation}
|
|
331 |
\indexisarcmd{print\_translation}\indexisarcmd{typed\_print\_translation}
|
|
332 |
\indexisarcmd{print\_ast\_translation}\indexisarcmd{token\_translation}
|
7134
|
333 |
\begin{matharray}{rcl}
|
|
334 |
\isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
|
|
335 |
\isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
|
|
336 |
\isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
|
|
337 |
\isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
|
|
338 |
\isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
|
|
339 |
\isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
|
|
340 |
\end{matharray}
|
|
341 |
|
|
342 |
Syntax translation functions written in ML admit almost arbitrary
|
|
343 |
manipulations of Isabelle's inner syntax. Any of the above commands have a
|
|
344 |
single \railqtoken{text} argument that refers to an ML expression of
|
|
345 |
appropriate type. See \cite[\S8]{isabelle-ref} for more information on syntax
|
|
346 |
transformations.
|
|
347 |
|
|
348 |
|
|
349 |
\subsection{Oracles}
|
|
350 |
|
|
351 |
\indexisarcmd{oracle}
|
|
352 |
\begin{matharray}{rcl}
|
|
353 |
\isarcmd{oracle} & : & \isartrans{theory}{theory} \\
|
|
354 |
\end{matharray}
|
|
355 |
|
|
356 |
\begin{rail}
|
|
357 |
'oracle' name '=' text comment?
|
|
358 |
;
|
|
359 |
\end{rail}
|
|
360 |
|
|
361 |
\begin{description}
|
|
362 |
\item [$\isarkeyword{oracle}~name=text$] FIXME
|
|
363 |
\end{description}
|
|
364 |
|
|
365 |
|
|
366 |
\section{Proof commands}
|
|
367 |
|
|
368 |
\subsection{Goal statements}
|
|
369 |
|
7141
|
370 |
\indexisarcmd{theorem}\indexisarcmd{lemma}
|
|
371 |
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
|
7134
|
372 |
\begin{matharray}{rcl}
|
|
373 |
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
|
|
374 |
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
|
|
375 |
\isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
376 |
\isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
377 |
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
378 |
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
379 |
\end{matharray}
|
|
380 |
|
|
381 |
\begin{rail}
|
|
382 |
('theorem' | 'lemma') goal
|
|
383 |
;
|
|
384 |
('have' | 'show' | 'hence' | 'thus') goal
|
|
385 |
;
|
|
386 |
|
|
387 |
goal: thmdecl? proppat comment?
|
|
388 |
;
|
|
389 |
\end{rail}
|
|
390 |
|
|
391 |
\begin{description}
|
|
392 |
\item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal,
|
|
393 |
eventually resulting in some theorem $\turn \phi$, which stored in the
|
|
394 |
theory.
|
|
395 |
\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
|
|
396 |
``lemma''.
|
|
397 |
\item [$\HAVE{name}{\phi}$] FIXME
|
|
398 |
\item [$\SHOW{name}{\phi}$] FIXME
|
|
399 |
\item [$\HENCE{name}{\phi}$] FIXME
|
|
400 |
\item [$\THUS{name}{\phi}$] FIXME
|
|
401 |
\end{description}
|
|
402 |
|
|
403 |
|
|
404 |
\subsection{Initial and terminal proof steps}
|
|
405 |
|
|
406 |
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
|
|
407 |
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
|
|
408 |
\begin{matharray}{rcl}
|
|
409 |
\isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
|
|
410 |
\isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
|
|
411 |
\isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
412 |
\isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
413 |
\isarcmd{..} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
414 |
\isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
415 |
\end{matharray}
|
|
416 |
|
|
417 |
\begin{rail}
|
|
418 |
'proof' interest? meth? comment?
|
|
419 |
;
|
|
420 |
'qed' meth? comment?
|
|
421 |
;
|
|
422 |
'by' meth meth? comment?
|
|
423 |
;
|
|
424 |
('.' | '..' | 'sorry') comment?
|
|
425 |
;
|
|
426 |
|
|
427 |
meth: method interest?
|
|
428 |
;
|
|
429 |
\end{rail}
|
|
430 |
|
|
431 |
\begin{description}
|
|
432 |
\item [$ $] FIXME
|
|
433 |
\end{description}
|
|
434 |
|
|
435 |
|
|
436 |
\subsection{Facts and forward chaining}
|
|
437 |
|
|
438 |
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
|
|
439 |
\begin{matharray}{rcl}
|
|
440 |
\isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
441 |
\isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
442 |
\isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
443 |
\isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
444 |
\end{matharray}
|
|
445 |
|
|
446 |
\begin{rail}
|
|
447 |
'note' thmdef? thmrefs comment?
|
|
448 |
;
|
|
449 |
'then' comment?
|
|
450 |
;
|
|
451 |
('from' | 'with') thmrefs comment?
|
|
452 |
;
|
|
453 |
\end{rail}
|
|
454 |
|
|
455 |
\begin{description}
|
|
456 |
\item [$ $] FIXME
|
|
457 |
\end{description}
|
|
458 |
|
|
459 |
|
|
460 |
\subsection{Proof context}
|
|
461 |
|
|
462 |
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let}
|
|
463 |
\begin{matharray}{rcl}
|
|
464 |
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
465 |
\isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
466 |
\isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
467 |
\isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
468 |
\isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
469 |
\end{matharray}
|
|
470 |
|
|
471 |
\begin{rail}
|
|
472 |
'fix' (var +) comment?
|
|
473 |
;
|
|
474 |
('assume' | 'presume') thmdecl? (proppat +) comment?
|
|
475 |
;
|
|
476 |
'def' thmdecl? var '==' termpat comment?
|
|
477 |
;
|
|
478 |
'let' ((term + 'as') '=' term comment? + 'and')
|
|
479 |
;
|
|
480 |
|
|
481 |
var: name ('::' type)?
|
|
482 |
;
|
|
483 |
\end{rail}
|
|
484 |
|
|
485 |
\begin{description}
|
|
486 |
\item [$ $] FIXME
|
|
487 |
\end{description}
|
|
488 |
|
|
489 |
|
|
490 |
\subsection{Block structure}
|
|
491 |
|
|
492 |
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
|
|
493 |
\begin{matharray}{rcl}
|
|
494 |
\isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
495 |
\isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
496 |
\isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
497 |
\end{matharray}
|
|
498 |
|
|
499 |
\begin{description}
|
|
500 |
\item [$ $] FIXME
|
|
501 |
\end{description}
|
|
502 |
|
|
503 |
|
|
504 |
\subsection{Calculational proof}
|
|
505 |
|
|
506 |
\indexisarcmd{also}\indexisarcmd{finally}
|
|
507 |
\begin{matharray}{rcl}
|
|
508 |
\isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
509 |
\isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
510 |
\end{matharray}
|
|
511 |
|
|
512 |
\begin{rail}
|
|
513 |
('also' | 'finally') transrules? comment?
|
|
514 |
;
|
|
515 |
|
|
516 |
transrules: '(' thmrefs ')' interest?
|
|
517 |
;
|
|
518 |
\end{rail}
|
|
519 |
|
|
520 |
\begin{description}
|
|
521 |
\item [$ $] FIXME
|
|
522 |
\end{description}
|
|
523 |
|
|
524 |
|
|
525 |
|
|
526 |
\subsection{Improper proof steps}
|
|
527 |
|
7141
|
528 |
\indexisarcmd{apply}\indexisarcmd{then\_apply}\indexisarcmd{back}
|
7134
|
529 |
\begin{matharray}{rcl}
|
|
530 |
\isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
|
|
531 |
\isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
|
|
532 |
\isarcmd{back}^* & : & \isartrans{proof}{proof} \\
|
|
533 |
\end{matharray}
|
|
534 |
|
|
535 |
\railalias{thenapply}{then\_apply}
|
|
536 |
\railterm{thenapply}
|
|
537 |
|
|
538 |
\begin{rail}
|
|
539 |
'apply' method
|
|
540 |
;
|
|
541 |
thenapply method
|
|
542 |
;
|
|
543 |
'back'
|
|
544 |
;
|
|
545 |
\end{rail}
|
|
546 |
|
|
547 |
\begin{description}
|
|
548 |
\item [$ $] FIXME
|
|
549 |
\end{description}
|
|
550 |
|
|
551 |
|
|
552 |
\section{Other commands}
|
|
553 |
|
|
554 |
\subsection{Diagnostics}
|
|
555 |
|
|
556 |
\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
|
|
557 |
\begin{matharray}{rcl}
|
|
558 |
\isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
|
|
559 |
\isarcmd{term} & : & \isarkeep{theory~|~proof} \\
|
|
560 |
\isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
|
|
561 |
\isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
|
|
562 |
\end{matharray}
|
|
563 |
|
|
564 |
\begin{rail}
|
|
565 |
'typ' type
|
|
566 |
;
|
|
567 |
'term' term
|
|
568 |
;
|
|
569 |
'prop' prop
|
|
570 |
;
|
|
571 |
'thm' thmrefs
|
|
572 |
;
|
|
573 |
\end{rail}
|
|
574 |
|
|
575 |
\begin{description}
|
|
576 |
\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,
|
|
577 |
$\isarkeyword{prop}~\phi$] read and print types / terms / propositions
|
|
578 |
according to the current theory or proof context.
|
|
579 |
\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
|
|
580 |
theory or proof context. Note that any attributes included in the theorem
|
|
581 |
specifications are applied to a temporary proof context derived from the
|
|
582 |
current theory or proof; the resulting context is discarded.
|
|
583 |
\end{description}
|
|
584 |
|
|
585 |
|
|
586 |
\subsection{System operations}
|
|
587 |
|
7141
|
588 |
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use\_thy}\indexisarcmd{use\_thy\_only}
|
|
589 |
\indexisarcmd{update\_thy}\indexisarcmd{update\_thy\_only}
|
7134
|
590 |
\begin{matharray}{rcl}
|
|
591 |
\isarcmd{cd} & : & \isarkeep{\cdot} \\
|
|
592 |
\isarcmd{pwd} & : & \isarkeep{\cdot} \\
|
|
593 |
\isarcmd{use_thy} & : & \isarkeep{\cdot} \\
|
|
594 |
\isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
|
|
595 |
\isarcmd{update_thy} & : & \isarkeep{\cdot} \\
|
|
596 |
\isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
|
|
597 |
\end{matharray}
|
|
598 |
|
|
599 |
\begin{description}
|
|
600 |
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
|
|
601 |
process.
|
|
602 |
\item [$\isarkeyword{pwd}~$] prints the current working directory.
|
|
603 |
\item [$\isarkeyword{use_thy}~name$, $\isarkeyword{use_thy_only}~name$,
|
|
604 |
$\isarkeyword{update_thy}~name$, $\isarkeyword{update_thy_only}~name$] load
|
|
605 |
theory files. These commands are exactly the same as the corresponding ML
|
|
606 |
functions (see also \cite[\S1 and \S6]{isabelle-ref}).
|
|
607 |
\end{description}
|
|
608 |
|
|
609 |
|
7046
|
610 |
%%% Local Variables:
|
|
611 |
%%% mode: latex
|
|
612 |
%%% TeX-master: "isar-ref"
|
|
613 |
%%% End:
|