author | wenzelm |
Wed, 21 Nov 2001 00:34:38 +0100 | |
changeset 12260 | 4898247d0102 |
parent 11549 | e7265e70fd7c |
child 12618 | 43a97a2155d0 |
permissions | -rw-r--r-- |
7046 | 1 |
|
7895 | 2 |
\chapter{Basic Isar Language Elements}\label{ch:pure-syntax} |
7167 | 3 |
|
8515 | 4 |
Subsequently, we introduce the main part of Pure Isar theory and proof |
8547 | 5 |
commands, together with fundamental proof methods and attributes. |
8515 | 6 |
Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic |
7 |
tools and packages (such as the Simplifier) that are either part of Pure |
|
8 |
Isabelle or pre-installed by most object logics. Chapter~\ref{ch:hol-tools} |
|
9 |
refers to actual object-logic specific elements of Isabelle/HOL. |
|
7046 | 10 |
|
7167 | 11 |
\medskip |
12 |
||
13 |
Isar commands may be either \emph{proper} document constructors, or |
|
7466 | 14 |
\emph{improper commands}. Some proof methods and attributes introduced later |
15 |
are classified as improper as well. Improper Isar language elements, which |
|
16 |
are subsequently marked by $^*$, are often helpful when developing proof |
|
7981 | 17 |
documents, while their use is discouraged for the final outcome. Typical |
18 |
examples are diagnostic commands that print terms or theorems according to the |
|
19 |
current context; other commands even emulate old-style tactical theorem |
|
8547 | 20 |
proving. |
7167 | 21 |
|
7134 | 22 |
|
23 |
\section{Theory commands} |
|
24 |
||
7167 | 25 |
\subsection{Defining theories}\label{sec:begin-thy} |
7134 | 26 |
|
7895 | 27 |
\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context} |
7134 | 28 |
\begin{matharray}{rcl} |
7895 | 29 |
\isarcmd{header} & : & \isarkeep{toplevel} \\ |
8510 | 30 |
\isarcmd{theory} & : & \isartrans{toplevel}{theory} \\ |
31 |
\isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\ |
|
32 |
\isarcmd{end} & : & \isartrans{theory}{toplevel} \\ |
|
7134 | 33 |
\end{matharray} |
34 |
||
35 |
Isabelle/Isar ``new-style'' theories are either defined via theory files or |
|
7981 | 36 |
interactively. Both theory-level specifications and proofs are handled |
7335 | 37 |
uniformly --- occasionally definitional mechanisms even require some explicit |
38 |
proof as well. In contrast, ``old-style'' Isabelle theories support batch |
|
39 |
processing only, with the proof scripts collected in separate ML files. |
|
7134 | 40 |
|
7895 | 41 |
The first actual command of any theory has to be $\THEORY$, starting a new |
42 |
theory based on the merge of existing ones. Just preceding $\THEORY$, there |
|
43 |
may be an optional $\isarkeyword{header}$ declaration, which is relevant to |
|
44 |
document preparation only; it acts very much like a special pre-theory markup |
|
45 |
command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory |
|
46 |
context may be also changed by $\CONTEXT$ without creating a new theory. In |
|
47 |
both cases, $\END$ concludes the theory development; it has to be the very |
|
8547 | 48 |
last command of any theory file. |
7134 | 49 |
|
50 |
\begin{rail} |
|
7895 | 51 |
'header' text |
52 |
; |
|
7134 | 53 |
'theory' name '=' (name + '+') filespecs? ':' |
54 |
; |
|
55 |
'context' name |
|
56 |
; |
|
57 |
'end' |
|
58 |
;; |
|
59 |
||
7167 | 60 |
filespecs: 'files' ((name | parname) +); |
7134 | 61 |
\end{rail} |
62 |
||
7167 | 63 |
\begin{descr} |
7895 | 64 |
\item [$\isarkeyword{header}~text$] provides plain text markup just preceding |
8547 | 65 |
the formal beginning of a theory. In actual document preparation the |
7895 | 66 |
corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to |
67 |
produce chapter or section headings. See also \S\ref{sec:markup-thy} and |
|
68 |
\S\ref{sec:markup-prf} for further markup commands. |
|
69 |
||
7981 | 70 |
\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$ |
71 |
based on existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader |
|
72 |
system ensures that any of the base theories are properly loaded (and fully |
|
73 |
up-to-date when $\THEORY$ is executed interactively). The optional |
|
74 |
$\isarkeyword{files}$ specification declares additional dependencies on ML |
|
75 |
files. Unless put in parentheses, any file will be loaded immediately via |
|
76 |
$\isarcmd{use}$ (see also \S\ref{sec:ML}). The optional ML file |
|
77 |
\texttt{$A$.ML} that may be associated with any theory should \emph{not} be |
|
78 |
included in $\isarkeyword{files}$, though. |
|
7134 | 79 |
|
7895 | 80 |
\item [$\CONTEXT~B$] enters an existing theory context, basically in read-only |
7981 | 81 |
mode, so only a limited set of commands may be performed without destroying |
82 |
the theory. Just as for $\THEORY$, the theory loader ensures that $B$ is |
|
83 |
loaded and up-to-date. |
|
7175 | 84 |
|
7167 | 85 |
\item [$\END$] concludes the current theory definition or context switch. |
7981 | 86 |
Note that this command cannot be undone, but the whole theory definition has |
87 |
to be retracted. |
|
7167 | 88 |
\end{descr} |
7134 | 89 |
|
90 |
||
7895 | 91 |
\subsection{Theory markup commands}\label{sec:markup-thy} |
7134 | 92 |
|
7895 | 93 |
\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection} |
94 |
\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw} |
|
7134 | 95 |
\begin{matharray}{rcl} |
96 |
\isarcmd{chapter} & : & \isartrans{theory}{theory} \\ |
|
7167 | 97 |
\isarcmd{section} & : & \isartrans{theory}{theory} \\ |
7134 | 98 |
\isarcmd{subsection} & : & \isartrans{theory}{theory} \\ |
99 |
\isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\ |
|
100 |
\isarcmd{text} & : & \isartrans{theory}{theory} \\ |
|
7895 | 101 |
\isarcmd{text_raw} & : & \isartrans{theory}{theory} \\ |
7134 | 102 |
\end{matharray} |
103 |
||
7895 | 104 |
Apart from formal comments (see \S\ref{sec:comments}), markup commands provide |
7981 | 105 |
a structured way to insert text into the document generated from a theory (see |
7895 | 106 |
\cite{isabelle-sys} for more information on Isabelle's document preparation |
107 |
tools). |
|
7134 | 108 |
|
7895 | 109 |
\railalias{textraw}{text\_raw} |
110 |
\railterm{textraw} |
|
7134 | 111 |
|
112 |
\begin{rail} |
|
7895 | 113 |
('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text |
7134 | 114 |
; |
115 |
\end{rail} |
|
116 |
||
7167 | 117 |
\begin{descr} |
7335 | 118 |
\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, |
119 |
$\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter |
|
120 |
and section headings. |
|
7895 | 121 |
\item [$\TEXT$] specifies paragraphs of plain text, including references to |
122 |
formal entities.\footnote{The latter feature is not yet supported. |
|
123 |
Nevertheless, any source text of the form |
|
124 |
``\texttt{\at\ttlbrace$\dots$\ttrbrace}'' should be considered as reserved |
|
125 |
for future use.} |
|
126 |
\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output, |
|
127 |
without additional markup. Thus the full range of document manipulations |
|
128 |
becomes available. A typical application would be to emit |
|
129 |
\verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain |
|
130 |
parts from the final document.\footnote{This requires the \texttt{comment} |
|
8547 | 131 |
package to be included in {\LaTeX}, of course.} |
7167 | 132 |
\end{descr} |
7134 | 133 |
|
8684 | 134 |
Any of these markup elements corresponds to a {\LaTeX} command with the name |
135 |
prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain |
|
136 |
macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for |
|
137 |
$\isarkeyword{chapter}$. The $\isarkeyword{text}$ markup results in a |
|
138 |
{\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots} |
|
139 |
\verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text |
|
140 |
to be inserted directly into the {\LaTeX} source. |
|
7895 | 141 |
|
8485 | 142 |
\medskip |
143 |
||
144 |
Additional markup commands are available for proofs (see |
|
7895 | 145 |
\S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$ |
8684 | 146 |
declaration (see \S\ref{sec:begin-thy}) admits to insert section markup just |
147 |
preceding the actual theory definition. |
|
7895 | 148 |
|
7134 | 149 |
|
7135 | 150 |
\subsection{Type classes and sorts}\label{sec:classes} |
7134 | 151 |
|
152 |
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} |
|
153 |
\begin{matharray}{rcl} |
|
154 |
\isarcmd{classes} & : & \isartrans{theory}{theory} \\ |
|
155 |
\isarcmd{classrel} & : & \isartrans{theory}{theory} \\ |
|
156 |
\isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\ |
|
157 |
\end{matharray} |
|
158 |
||
159 |
\begin{rail} |
|
7167 | 160 |
'classes' (classdecl comment? +) |
7134 | 161 |
; |
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset
|
162 |
'classrel' nameref ('<' | subseteq) nameref comment? |
7134 | 163 |
; |
164 |
'defaultsort' sort comment? |
|
165 |
; |
|
166 |
\end{rail} |
|
167 |
||
7167 | 168 |
\begin{descr} |
11100
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset
|
169 |
\item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a |
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset
|
170 |
subclass of existing classes $\vec c$. Cyclic class structures are ruled |
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset
|
171 |
out. |
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset
|
172 |
\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states a subclass relation |
34d58b1818f4
\<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents:
11017
diff
changeset
|
173 |
between existing classes $c@1$ and $c@2$. This is done axiomatically! The |
10223 | 174 |
$\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce |
175 |
proven class relations. |
|
7134 | 176 |
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for |
7895 | 177 |
any type variables given without sort constraints. Usually, the default |
8547 | 178 |
sort would be only changed when defining new object-logics. |
7167 | 179 |
\end{descr} |
7134 | 180 |
|
181 |
||
7315 | 182 |
\subsection{Primitive types and type abbreviations}\label{sec:types-pure} |
7134 | 183 |
|
184 |
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities} |
|
185 |
\begin{matharray}{rcl} |
|
186 |
\isarcmd{types} & : & \isartrans{theory}{theory} \\ |
|
187 |
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ |
|
188 |
\isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\ |
|
189 |
\isarcmd{arities} & : & \isartrans{theory}{theory} \\ |
|
190 |
\end{matharray} |
|
191 |
||
192 |
\begin{rail} |
|
193 |
'types' (typespec '=' type infix? comment? +) |
|
194 |
; |
|
195 |
'typedecl' typespec infix? comment? |
|
196 |
; |
|
197 |
'nonterminals' (name +) comment? |
|
198 |
; |
|
199 |
'arities' (nameref '::' arity comment? +) |
|
200 |
; |
|
201 |
\end{rail} |
|
202 |
||
7167 | 203 |
\begin{descr} |
7335 | 204 |
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym} |
7134 | 205 |
$(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions, |
206 |
as are available in Isabelle/HOL for example, type synonyms are just purely |
|
7895 | 207 |
syntactic abbreviations without any logical significance. Internally, type |
7981 | 208 |
synonyms are fully expanded. |
7134 | 209 |
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor |
7895 | 210 |
$t$, intended as an actual logical type. Note that object-logics such as |
211 |
Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version. |
|
7175 | 212 |
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors |
213 |
$\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of |
|
214 |
Isabelle's inner syntax of terms or types. |
|
7335 | 215 |
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted |
216 |
signature of types by new type constructor arities. This is done |
|
10223 | 217 |
axiomatically! The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a |
218 |
way to introduce proven type arities. |
|
7167 | 219 |
\end{descr} |
7134 | 220 |
|
221 |
||
7981 | 222 |
\subsection{Constants and simple definitions}\label{sec:consts} |
7134 | 223 |
|
7175 | 224 |
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl} |
7134 | 225 |
\begin{matharray}{rcl} |
226 |
\isarcmd{consts} & : & \isartrans{theory}{theory} \\ |
|
227 |
\isarcmd{defs} & : & \isartrans{theory}{theory} \\ |
|
228 |
\isarcmd{constdefs} & : & \isartrans{theory}{theory} \\ |
|
229 |
\end{matharray} |
|
230 |
||
231 |
\begin{rail} |
|
232 |
'consts' (constdecl +) |
|
233 |
; |
|
9308 | 234 |
'defs' ('(overloaded)')? (axmdecl prop comment? +) |
7134 | 235 |
; |
236 |
'constdefs' (constdecl prop comment? +) |
|
237 |
; |
|
238 |
||
239 |
constdecl: name '::' type mixfix? comment? |
|
240 |
; |
|
241 |
\end{rail} |
|
242 |
||
7167 | 243 |
\begin{descr} |
7335 | 244 |
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type |
245 |
scheme $\sigma$. The optional mixfix annotations may attach concrete syntax |
|
7895 | 246 |
to the constants declared. |
9308 | 247 |
|
7335 | 248 |
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some |
249 |
existing constant. See \cite[\S6]{isabelle-ref} for more details on the |
|
250 |
form of equations admitted as constant definitions. |
|
9308 | 251 |
|
252 |
The $overloaded$ option declares definitions to be potentially overloaded. |
|
253 |
Unless this option is given, a warning message would be issued for any |
|
254 |
definitional equation with a more special type than that of the |
|
255 |
corresponding constant declaration. |
|
256 |
||
7335 | 257 |
\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and |
8547 | 258 |
definitions of constants, using the canonical name $c_def$ for the |
259 |
definitional axiom. |
|
7167 | 260 |
\end{descr} |
7134 | 261 |
|
262 |
||
7981 | 263 |
\subsection{Syntax and translations}\label{sec:syn-trans} |
7134 | 264 |
|
265 |
\indexisarcmd{syntax}\indexisarcmd{translations} |
|
266 |
\begin{matharray}{rcl} |
|
267 |
\isarcmd{syntax} & : & \isartrans{theory}{theory} \\ |
|
268 |
\isarcmd{translations} & : & \isartrans{theory}{theory} \\ |
|
269 |
\end{matharray} |
|
270 |
||
10640 | 271 |
\railalias{rightleftharpoons}{\isasymrightleftharpoons} |
272 |
\railterm{rightleftharpoons} |
|
273 |
||
274 |
\railalias{rightharpoonup}{\isasymrightharpoonup} |
|
275 |
\railterm{rightharpoonup} |
|
276 |
||
277 |
\railalias{leftharpoondown}{\isasymleftharpoondown} |
|
278 |
\railterm{leftharpoondown} |
|
279 |
||
7134 | 280 |
\begin{rail} |
9727 | 281 |
'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +) |
7134 | 282 |
; |
10640 | 283 |
'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat comment? +) |
7134 | 284 |
; |
285 |
transpat: ('(' nameref ')')? string |
|
286 |
; |
|
287 |
\end{rail} |
|
288 |
||
7167 | 289 |
\begin{descr} |
7175 | 290 |
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, |
291 |
except that the actual logical signature extension is omitted. Thus the |
|
292 |
context free grammar of Isabelle's inner syntax may be augmented in |
|
7335 | 293 |
arbitrary ways, independently of the logic. The $mode$ argument refers to |
8547 | 294 |
the print mode that the grammar rules belong; unless the \texttt{output} |
295 |
flag is given, all productions are added both to the input and output |
|
296 |
grammar. |
|
7175 | 297 |
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation |
10640 | 298 |
rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==} or |
299 |
\isasymrightleftharpoons), parse rules (\texttt{=>} or |
|
300 |
\isasymrightharpoonup), or print rules (\texttt{<=} or |
|
301 |
\isasymleftharpoondown). Translation patterns may be prefixed by the |
|
302 |
syntactic category to be used for parsing; the default is \texttt{logic}. |
|
7167 | 303 |
\end{descr} |
7134 | 304 |
|
305 |
||
9605 | 306 |
\subsection{Axioms and theorems}\label{sec:axms-thms} |
7134 | 307 |
|
308 |
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas} |
|
309 |
\begin{matharray}{rcl} |
|
310 |
\isarcmd{axioms} & : & \isartrans{theory}{theory} \\ |
|
311 |
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\ |
|
312 |
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ |
|
313 |
\end{matharray} |
|
314 |
||
315 |
\begin{rail} |
|
7135 | 316 |
'axioms' (axmdecl prop comment? +) |
7134 | 317 |
; |
9199 | 318 |
('theorems' | 'lemmas') (thmdef? thmrefs comment? + 'and') |
7134 | 319 |
; |
320 |
\end{rail} |
|
321 |
||
7167 | 322 |
\begin{descr} |
7335 | 323 |
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as |
7895 | 324 |
axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and |
325 |
may be referred later just as any other theorem. |
|
7134 | 326 |
|
327 |
Axioms are usually only introduced when declaring new logical systems. |
|
7175 | 328 |
Everyday work is typically done the hard way, with proper definitions and |
8547 | 329 |
actual proven theorems. |
7335 | 330 |
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems. |
8547 | 331 |
Typical applications would also involve attributes, to declare Simplifier |
332 |
rules, for example. |
|
7134 | 333 |
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but |
334 |
tags the results as ``lemma''. |
|
7167 | 335 |
\end{descr} |
7134 | 336 |
|
337 |
||
7167 | 338 |
\subsection{Name spaces} |
7134 | 339 |
|
8726 | 340 |
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide} |
7134 | 341 |
\begin{matharray}{rcl} |
342 |
\isarcmd{global} & : & \isartrans{theory}{theory} \\ |
|
343 |
\isarcmd{local} & : & \isartrans{theory}{theory} \\ |
|
8726 | 344 |
\isarcmd{hide} & : & \isartrans{theory}{theory} \\ |
7134 | 345 |
\end{matharray} |
346 |
||
8726 | 347 |
\begin{rail} |
348 |
'global' comment? |
|
349 |
; |
|
350 |
'local' comment? |
|
351 |
; |
|
352 |
'hide' name (nameref + ) comment? |
|
353 |
; |
|
354 |
\end{rail} |
|
355 |
||
7895 | 356 |
Isabelle organizes any kind of name declarations (of types, constants, |
8547 | 357 |
theorems etc.) by separate hierarchically structured name spaces. Normally |
8726 | 358 |
the user does not have to control the behavior of name spaces by hand, yet the |
359 |
following commands provide some way to do so. |
|
7175 | 360 |
|
7167 | 361 |
\begin{descr} |
362 |
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current |
|
363 |
name declaration mode. Initially, theories start in $\isarkeyword{local}$ |
|
364 |
mode, causing all names to be automatically qualified by the theory name. |
|
7895 | 365 |
Changing this to $\isarkeyword{global}$ causes all names to be declared |
366 |
without the theory prefix, until $\isarkeyword{local}$ is declared again. |
|
8726 | 367 |
|
368 |
Note that global names are prone to get hidden accidently later, when |
|
369 |
qualified names of the same base name are introduced. |
|
370 |
||
371 |
\item [$\isarkeyword{hide}~space~names$] removes declarations from a given |
|
372 |
name space (which may be $class$, $type$, or $const$). Hidden objects |
|
373 |
remain valid within the logic, but are inaccessible from user input. In |
|
374 |
output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the |
|
375 |
full internal name. |
|
376 |
||
377 |
Unqualified (global) names may not be hidden deliberately. |
|
7167 | 378 |
\end{descr} |
7134 | 379 |
|
380 |
||
7167 | 381 |
\subsection{Incorporating ML code}\label{sec:ML} |
7134 | 382 |
|
8682 | 383 |
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-command} |
384 |
\indexisarcmd{ML-setup}\indexisarcmd{setup} |
|
9199 | 385 |
\indexisarcmd{method-setup} |
7134 | 386 |
\begin{matharray}{rcl} |
387 |
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\ |
|
388 |
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\ |
|
8682 | 389 |
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ |
7895 | 390 |
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\ |
7175 | 391 |
\isarcmd{setup} & : & \isartrans{theory}{theory} \\ |
9199 | 392 |
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ |
7134 | 393 |
\end{matharray} |
394 |
||
7895 | 395 |
\railalias{MLsetup}{ML\_setup} |
396 |
\railterm{MLsetup} |
|
397 |
||
9199 | 398 |
\railalias{methodsetup}{method\_setup} |
399 |
\railterm{methodsetup} |
|
400 |
||
8682 | 401 |
\railalias{MLcommand}{ML\_command} |
402 |
\railterm{MLcommand} |
|
403 |
||
7134 | 404 |
\begin{rail} |
9273 | 405 |
'use' name comment? |
7134 | 406 |
; |
9273 | 407 |
('ML' | MLcommand | MLsetup | 'setup') text comment? |
7134 | 408 |
; |
9199 | 409 |
methodsetup name '=' text text comment? |
410 |
; |
|
7134 | 411 |
\end{rail} |
412 |
||
7167 | 413 |
\begin{descr} |
7175 | 414 |
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$. |
7466 | 415 |
The current theory context (if present) is passed down to the ML session, |
7981 | 416 |
but may not be modified. Furthermore, the file name is checked with the |
7466 | 417 |
$\isarkeyword{files}$ dependency declaration given in the theory header (see |
418 |
also \S\ref{sec:begin-thy}). |
|
419 |
||
8682 | 420 |
\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML |
421 |
commands from $text$. The theory context is passed in the same way as for |
|
10858 | 422 |
$\isarkeyword{use}$, but may not be changed. Note that the output of |
8682 | 423 |
$\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$. |
7895 | 424 |
|
425 |
\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The |
|
426 |
theory context is passed down to the ML session, and fetched back |
|
427 |
afterwards. Thus $text$ may actually change the theory as a side effect. |
|
428 |
||
7167 | 429 |
\item [$\isarkeyword{setup}~text$] changes the current theory context by |
8379 | 430 |
applying $text$, which refers to an ML expression of type |
431 |
\texttt{(theory~->~theory)~list}. The $\isarkeyword{setup}$ command is the |
|
8547 | 432 |
canonical way to initialize any object-logic specific tools and packages |
433 |
written in ML. |
|
9199 | 434 |
|
435 |
\item [$\isarkeyword{method_setup}~name = text~description$] defines a proof |
|
436 |
method in the current theory. The given $text$ has to be an ML expression |
|
437 |
of type \texttt{Args.src -> Proof.context -> Proof.method}. Parsing |
|
438 |
concrete method syntax from \texttt{Args.src} input can be quite tedious in |
|
439 |
general. The following simple examples are for methods without any explicit |
|
440 |
arguments, or a list of theorems, respectively. |
|
441 |
||
442 |
{\footnotesize |
|
443 |
\begin{verbatim} |
|
9605 | 444 |
Method.no_args (Method.METHOD (fn facts => foobar_tac)) |
445 |
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) |
|
10899 | 446 |
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) |
447 |
Method.thms_ctxt_args (fn thms => fn ctxt => Method.METHOD (fn facts => foobar_tac)) |
|
9199 | 448 |
\end{verbatim} |
449 |
} |
|
450 |
||
451 |
Note that mere tactic emulations may ignore the \texttt{facts} parameter |
|
452 |
above. Proper proof methods would do something ``appropriate'' with the list |
|
453 |
of current facts, though. Single-rule methods usually do strict |
|
454 |
forward-chaining (e.g.\ by using \texttt{Method.multi_resolves}), while |
|
455 |
automatic ones just insert the facts using \texttt{Method.insert_tac} before |
|
456 |
applying the main tactic. |
|
7167 | 457 |
\end{descr} |
7134 | 458 |
|
459 |
||
8250 | 460 |
\subsection{Syntax translation functions} |
7134 | 461 |
|
8250 | 462 |
\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation} |
463 |
\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation} |
|
464 |
\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation} |
|
465 |
\begin{matharray}{rcl} |
|
466 |
\isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\ |
|
467 |
\isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\ |
|
468 |
\isarcmd{print_translation} & : & \isartrans{theory}{theory} \\ |
|
469 |
\isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\ |
|
470 |
\isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\ |
|
471 |
\isarcmd{token_translation} & : & \isartrans{theory}{theory} \\ |
|
472 |
\end{matharray} |
|
7134 | 473 |
|
9273 | 474 |
\railalias{parseasttranslation}{parse\_ast\_translation} |
475 |
\railterm{parseasttranslation} |
|
476 |
||
477 |
\railalias{parsetranslation}{parse\_translation} |
|
478 |
\railterm{parsetranslation} |
|
479 |
||
480 |
\railalias{printtranslation}{print\_translation} |
|
481 |
\railterm{printtranslation} |
|
482 |
||
483 |
\railalias{typedprinttranslation}{typed\_print\_translation} |
|
484 |
\railterm{typedprinttranslation} |
|
485 |
||
486 |
\railalias{printasttranslation}{print\_ast\_translation} |
|
487 |
\railterm{printasttranslation} |
|
488 |
||
489 |
\railalias{tokentranslation}{token\_translation} |
|
490 |
\railterm{tokentranslation} |
|
491 |
||
492 |
\begin{rail} |
|
493 |
( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation | |
|
494 |
printasttranslation | tokentranslation ) text comment? |
|
495 |
\end{rail} |
|
496 |
||
8250 | 497 |
Syntax translation functions written in ML admit almost arbitrary |
498 |
manipulations of Isabelle's inner syntax. Any of the above commands have a |
|
499 |
single \railqtoken{text} argument that refers to an ML expression of |
|
8379 | 500 |
appropriate type. |
501 |
||
502 |
\begin{ttbox} |
|
503 |
val parse_ast_translation : (string * (ast list -> ast)) list |
|
504 |
val parse_translation : (string * (term list -> term)) list |
|
505 |
val print_translation : (string * (term list -> term)) list |
|
506 |
val typed_print_translation : |
|
507 |
(string * (bool -> typ -> term list -> term)) list |
|
508 |
val print_ast_translation : (string * (ast list -> ast)) list |
|
509 |
val token_translation : |
|
510 |
(string * string * (string -> string * real)) list |
|
511 |
\end{ttbox} |
|
512 |
See \cite[\S8]{isabelle-ref} for more information on syntax transformations. |
|
7134 | 513 |
|
514 |
||
515 |
\subsection{Oracles} |
|
516 |
||
517 |
\indexisarcmd{oracle} |
|
518 |
\begin{matharray}{rcl} |
|
519 |
\isarcmd{oracle} & : & \isartrans{theory}{theory} \\ |
|
520 |
\end{matharray} |
|
521 |
||
7175 | 522 |
Oracles provide an interface to external reasoning systems, without giving up |
523 |
control completely --- each theorem carries a derivation object recording any |
|
524 |
oracle invocation. See \cite[\S6]{isabelle-ref} for more information. |
|
525 |
||
7134 | 526 |
\begin{rail} |
527 |
'oracle' name '=' text comment? |
|
528 |
; |
|
529 |
\end{rail} |
|
530 |
||
7167 | 531 |
\begin{descr} |
7175 | 532 |
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML |
8379 | 533 |
function $text$, which has to be of type |
534 |
\texttt{Sign.sg~*~Object.T~->~term}. |
|
7167 | 535 |
\end{descr} |
7134 | 536 |
|
537 |
||
538 |
\section{Proof commands} |
|
539 |
||
7987 | 540 |
Proof commands perform transitions of Isar/VM machine configurations, which |
7315 | 541 |
are block-structured, consisting of a stack of nodes with three main |
7335 | 542 |
components: logical proof context, current facts, and open goals. Isar/VM |
8547 | 543 |
transitions are \emph{typed} according to the following three different modes |
544 |
of operation: |
|
7167 | 545 |
\begin{descr} |
546 |
\item [$proof(prove)$] means that a new goal has just been stated that is now |
|
8547 | 547 |
to be \emph{proven}; the next command may refine it by some proof method, |
548 |
and enter a sub-proof to establish the actual result. |
|
10858 | 549 |
\item [$proof(state)$] is like a nested theory mode: the context may be |
7987 | 550 |
augmented by \emph{stating} additional assumptions, intermediate results |
551 |
etc. |
|
7895 | 552 |
\item [$proof(chain)$] is intermediate between $proof(state)$ and |
7987 | 553 |
$proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$'' |
554 |
register) have been just picked up in order to be used when refining the |
|
555 |
goal claimed next. |
|
7167 | 556 |
\end{descr} |
7134 | 557 |
|
7167 | 558 |
|
7895 | 559 |
\subsection{Proof markup commands}\label{sec:markup-prf} |
7167 | 560 |
|
7987 | 561 |
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} |
7895 | 562 |
\indexisarcmd{txt}\indexisarcmd{txt-raw} |
7134 | 563 |
\begin{matharray}{rcl} |
8101 | 564 |
\isarcmd{sect} & : & \isartrans{proof}{proof} \\ |
565 |
\isarcmd{subsect} & : & \isartrans{proof}{proof} \\ |
|
566 |
\isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\ |
|
567 |
\isarcmd{txt} & : & \isartrans{proof}{proof} \\ |
|
568 |
\isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\ |
|
7134 | 569 |
\end{matharray} |
570 |
||
7895 | 571 |
These markup commands for proof mode closely correspond to the ones of theory |
8684 | 572 |
mode (see \S\ref{sec:markup-thy}). |
7895 | 573 |
|
574 |
\railalias{txtraw}{txt\_raw} |
|
575 |
\railterm{txtraw} |
|
7175 | 576 |
|
7134 | 577 |
\begin{rail} |
7895 | 578 |
('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text |
7134 | 579 |
; |
580 |
\end{rail} |
|
581 |
||
582 |
||
7315 | 583 |
\subsection{Proof context}\label{sec:proof-context} |
7134 | 584 |
|
7315 | 585 |
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} |
7134 | 586 |
\begin{matharray}{rcl} |
587 |
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
588 |
\isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
589 |
\isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
590 |
\isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
591 |
\end{matharray} |
|
592 |
||
7315 | 593 |
The logical proof context consists of fixed variables and assumptions. The |
594 |
former closely correspond to Skolem constants, or meta-level universal |
|
595 |
quantification as provided by the Isabelle/Pure logical framework. |
|
596 |
Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in |
|
7987 | 597 |
a local value that may be used in the subsequent proof as any other variable |
7895 | 598 |
or constant. Furthermore, any result $\edrv \phi[x]$ exported from the |
7987 | 599 |
context will be universally closed wrt.\ $x$ at the outermost level: $\edrv |
600 |
\All x \phi$ (this is expressed using Isabelle's meta-variables). |
|
7315 | 601 |
|
602 |
Similarly, introducing some assumption $\chi$ has two effects. On the one |
|
603 |
hand, a local theorem is created that may be used as a fact in subsequent |
|
7895 | 604 |
proof steps. On the other hand, any result $\chi \drv \phi$ exported from the |
605 |
context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$. |
|
606 |
Thus, solving an enclosing goal using such a result would basically introduce |
|
607 |
a new subgoal stemming from the assumption. How this situation is handled |
|
608 |
depends on the actual version of assumption command used: while $\ASSUMENAME$ |
|
609 |
insists on solving the subgoal by unification with some premise of the goal, |
|
610 |
$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the |
|
611 |
user. |
|
7315 | 612 |
|
7319 | 613 |
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by |
7987 | 614 |
combining $\FIX x$ with another version of assumption that causes any |
615 |
hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. |
|
616 |
Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. |
|
7175 | 617 |
|
10686 | 618 |
\railalias{equiv}{\isasymequiv} |
619 |
\railterm{equiv} |
|
620 |
||
7134 | 621 |
\begin{rail} |
7431 | 622 |
'fix' (vars + 'and') comment? |
7134 | 623 |
; |
7315 | 624 |
('assume' | 'presume') (assm comment? + 'and') |
7134 | 625 |
; |
10686 | 626 |
'def' thmdecl? \\ name ('==' | equiv) term termpat? comment? |
7134 | 627 |
; |
628 |
||
629 |
var: name ('::' type)? |
|
630 |
; |
|
7458 | 631 |
vars: (name+) ('::' type)? |
7431 | 632 |
; |
7315 | 633 |
assm: thmdecl? (prop proppat? +) |
634 |
; |
|
7134 | 635 |
\end{rail} |
636 |
||
7167 | 637 |
\begin{descr} |
8547 | 638 |
\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables |
639 |
$\vec x$. |
|
8515 | 640 |
\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local |
641 |
theorems $\vec\phi$ by assumption. Subsequent results applied to an |
|
642 |
enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ |
|
643 |
expects to be able to unify with existing premises in the goal, while |
|
644 |
$\PRESUMENAME$ leaves $\vec\phi$ as new subgoals. |
|
7335 | 645 |
|
646 |
Several lists of assumptions may be given (separated by |
|
7895 | 647 |
$\isarkeyword{and}$); the resulting list of current facts consists of all of |
648 |
these concatenated. |
|
7315 | 649 |
\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition. |
650 |
In results exported from the context, $x$ is replaced by $t$. Basically, |
|
7987 | 651 |
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\ASSUME{}{x \equiv t}$, with the |
7335 | 652 |
resulting hypothetical equation solved by reflexivity. |
7431 | 653 |
|
654 |
The default name for the definitional equation is $x_def$. |
|
7167 | 655 |
\end{descr} |
656 |
||
7895 | 657 |
The special name $prems$\indexisarthm{prems} refers to all assumptions of the |
658 |
current context as a list of theorems. |
|
7315 | 659 |
|
7167 | 660 |
|
661 |
\subsection{Facts and forward chaining} |
|
662 |
||
663 |
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with} |
|
664 |
\begin{matharray}{rcl} |
|
665 |
\isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
666 |
\isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
667 |
\isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
668 |
\isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\ |
|
669 |
\end{matharray} |
|
670 |
||
7319 | 671 |
New facts are established either by assumption or proof of local statements. |
7335 | 672 |
Any fact will usually be involved in further proofs, either as explicit |
8547 | 673 |
arguments of proof methods, or when forward chaining towards the next goal via |
7335 | 674 |
$\THEN$ (and variants). Note that the special theorem name |
7987 | 675 |
$this$\indexisarthm{this} refers to the most recently established facts. |
7167 | 676 |
\begin{rail} |
9199 | 677 |
'note' (thmdef? thmrefs comment? + 'and') |
7167 | 678 |
; |
679 |
'then' comment? |
|
680 |
; |
|
9199 | 681 |
('from' | 'with') (thmrefs comment? + 'and') |
7167 | 682 |
; |
683 |
\end{rail} |
|
684 |
||
685 |
\begin{descr} |
|
7175 | 686 |
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result |
687 |
as $a$. Note that attributes may be involved as well, both on the left and |
|
688 |
right hand sides. |
|
7167 | 689 |
\item [$\THEN$] indicates forward chaining by the current facts in order to |
7895 | 690 |
establish the goal to be claimed next. The initial proof method invoked to |
691 |
refine that will be offered the facts to do ``anything appropriate'' (cf.\ |
|
692 |
also \S\ref{sec:proof-steps}). For example, method $rule$ (see |
|
8515 | 693 |
\S\ref{sec:pure-meth-att}) would typically do an elimination rather than an |
7895 | 694 |
introduction. Automatic methods usually insert the facts into the goal |
8547 | 695 |
state before operation. This provides a simple scheme to control relevance |
696 |
of facts in automated proof search. |
|
7335 | 697 |
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is |
7458 | 698 |
equivalent to $\FROM{this}$. |
10858 | 699 |
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward |
7175 | 700 |
chaining is from earlier facts together with the current ones. |
7167 | 701 |
\end{descr} |
702 |
||
8515 | 703 |
Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect |
7895 | 704 |
multiple facts to be given in their proper order, corresponding to a prefix of |
705 |
the premises of the rule involved. Note that positions may be easily skipped |
|
9695 | 706 |
using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example. This |
8547 | 707 |
involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be |
708 |
bound in Isabelle/Pure as ``\texttt{_}'' |
|
709 |
(underscore).\indexisarthm{_@\texttt{_}} |
|
7389 | 710 |
|
9238 | 711 |
Forward chaining with an empty list of theorems is the same as not chaining. |
712 |
Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode, |
|
713 |
since $nothing$\indexisarthm{nothing} is bound to the empty list of facts. |
|
714 |
||
7167 | 715 |
|
716 |
\subsection{Goal statements} |
|
717 |
||
718 |
\indexisarcmd{theorem}\indexisarcmd{lemma} |
|
719 |
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} |
|
720 |
\begin{matharray}{rcl} |
|
721 |
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\ |
|
722 |
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\ |
|
7987 | 723 |
\isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
724 |
\isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ |
|
7167 | 725 |
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ |
726 |
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ |
|
727 |
\end{matharray} |
|
728 |
||
7175 | 729 |
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$ |
7895 | 730 |
and $\LEMMANAME$. New local goals may be claimed within proof mode as well. |
731 |
Four variants are available, indicating whether the result is meant to solve |
|
8547 | 732 |
some pending goal or whether forward chaining is indicated. |
7175 | 733 |
|
7167 | 734 |
\begin{rail} |
735 |
('theorem' | 'lemma') goal |
|
736 |
; |
|
737 |
('have' | 'show' | 'hence' | 'thus') goal |
|
738 |
; |
|
739 |
||
8632 | 740 |
goal: thmdecl? prop proppat? comment? |
7167 | 741 |
; |
742 |
\end{rail} |
|
743 |
||
744 |
\begin{descr} |
|
7335 | 745 |
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal, |
8547 | 746 |
eventually resulting in some theorem $\turn \phi$ to be put back into the |
747 |
theory. |
|
7987 | 748 |
\item [$\LEMMA{a}{\phi}$] is similar to $\THEOREMNAME$, but tags the result as |
7167 | 749 |
``lemma''. |
7335 | 750 |
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a |
7167 | 751 |
theorem with the current assumption context as hypotheses. |
7335 | 752 |
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some |
7895 | 753 |
pending goal with the result \emph{exported} into the corresponding context |
754 |
(cf.\ \S\ref{sec:proof-context}). |
|
755 |
\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal |
|
756 |
to be proven by forward chaining the current facts. Note that $\HENCENAME$ |
|
757 |
is also equivalent to $\FROM{this}~\HAVENAME$. |
|
758 |
\item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$. Note that $\THUSNAME$ is |
|
759 |
also equivalent to $\FROM{this}~\SHOWNAME$. |
|
7167 | 760 |
\end{descr} |
761 |
||
10550 | 762 |
Any goal statement causes some term abbreviations (such as $\Var{thesis}$, |
763 |
$\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}. |
|
11549 | 764 |
Furthermore, the local context of a (non-atomic) goal is provided via the |
765 |
$rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}. |
|
10550 | 766 |
|
767 |
\medskip |
|
768 |
||
769 |
\begin{warn} |
|
770 |
Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound |
|
771 |
schematic variables}, although this does not conform to the aim of |
|
772 |
human-readable proof documents! The main problem with schematic goals is |
|
773 |
that the actual outcome is usually hard to predict, depending on the |
|
774 |
behavior of the actual proof methods applied during the reasoning. Note |
|
775 |
that most semi-automated methods heavily depend on several kinds of implicit |
|
776 |
rule declarations within the current theory context. As this would also |
|
777 |
result in non-compositional checking of sub-proofs, \emph{local goals} are |
|
778 |
not allowed to be schematic at all. |
|
779 |
||
780 |
Nevertheless, schematic goals do have their use in Prolog-style interactive |
|
781 |
synthesis of proven results, usually by stepwise refinement via emulation of |
|
782 |
traditional Isabelle tactic scripts (see also \S\ref{sec:tactic-commands}). |
|
783 |
In any case, users should know what they are doing! |
|
784 |
\end{warn} |
|
8991 | 785 |
|
7167 | 786 |
|
787 |
\subsection{Initial and terminal proof steps}\label{sec:proof-steps} |
|
788 |
||
7175 | 789 |
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} |
790 |
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} |
|
791 |
\begin{matharray}{rcl} |
|
792 |
\isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\ |
|
793 |
\isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\ |
|
794 |
\isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
|
795 |
\isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
|
796 |
\isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
|
797 |
\isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ |
|
798 |
\end{matharray} |
|
799 |
||
8547 | 800 |
Arbitrary goal refinement via tactics is considered harmful. Properly, the |
7335 | 801 |
Isar framework admits proof methods to be invoked in two places only. |
7167 | 802 |
\begin{enumerate} |
7175 | 803 |
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated |
7335 | 804 |
goal to a number of sub-goals that are to be solved later. Facts are passed |
7895 | 805 |
to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode. |
7167 | 806 |
|
7987 | 807 |
\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve |
808 |
remaining goals. No facts are passed to $m@2$. |
|
7167 | 809 |
\end{enumerate} |
810 |
||
8547 | 811 |
The only other proper way to affect pending goals is by $\SHOWNAME$, which |
812 |
involves an explicit statement of what is to be solved. |
|
7167 | 813 |
|
7175 | 814 |
\medskip |
815 |
||
7167 | 816 |
Also note that initial proof methods should either solve the goal completely, |
7895 | 817 |
or constitute some well-understood reduction to new sub-goals. Arbitrary |
818 |
automatic proof tools that are prone leave a large number of badly structured |
|
819 |
sub-goals are no help in continuing the proof document in any intelligible |
|
7987 | 820 |
way. |
7167 | 821 |
|
7175 | 822 |
\medskip |
823 |
||
8547 | 824 |
Unless given explicitly by the user, the default initial method is ``$rule$'', |
825 |
which applies a single standard elimination or introduction rule according to |
|
826 |
the topmost symbol involved. There is no separate default terminal method. |
|
827 |
Any remaining goals are always solved by assumption in the very last step. |
|
7167 | 828 |
|
829 |
\begin{rail} |
|
830 |
'proof' interest? meth? comment? |
|
831 |
; |
|
832 |
'qed' meth? comment? |
|
833 |
; |
|
834 |
'by' meth meth? comment? |
|
835 |
; |
|
836 |
('.' | '..' | 'sorry') comment? |
|
837 |
; |
|
838 |
||
839 |
meth: method interest? |
|
840 |
; |
|
841 |
\end{rail} |
|
842 |
||
843 |
\begin{descr} |
|
7335 | 844 |
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for |
845 |
forward chaining are passed if so indicated by $proof(chain)$ mode. |
|
846 |
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and |
|
7895 | 847 |
concludes the sub-proof by assumption. If the goal had been $\SHOWNAME$ (or |
848 |
$\THUSNAME$), some pending sub-goal is solved as well by the rule resulting |
|
849 |
from the result \emph{exported} into the enclosing goal context. Thus |
|
850 |
$\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting |
|
851 |
rule does not fit to any pending goal\footnote{This includes any additional |
|
852 |
``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing |
|
853 |
context. Debugging such a situation might involve temporarily changing |
|
854 |
$\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing |
|
855 |
some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$. |
|
856 |
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it |
|
7987 | 857 |
abbreviates $\PROOF{m@1}~\QED{m@2}$, with backtracking across both methods, |
858 |
though. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done |
|
7895 | 859 |
by expanding its definition; in many cases $\PROOF{m@1}$ is already |
7175 | 860 |
sufficient to see what is going wrong. |
7895 | 861 |
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it |
8515 | 862 |
abbreviates $\BY{rule}$. |
7895 | 863 |
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it |
8195 | 864 |
abbreviates $\BY{this}$. |
8379 | 865 |
\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake}; provided that the |
866 |
\texttt{quick_and_dirty} flag is enabled, $\SORRY$ pretends to solve the |
|
8515 | 867 |
goal without further ado. Of course, the result would be a fake theorem |
868 |
only, involving some oracle in its internal derivation object (this is |
|
869 |
indicated as ``$[!]$'' in the printed result). The main application of |
|
870 |
$\SORRY$ is to support experimentation and top-down proof development. |
|
871 |
\end{descr} |
|
872 |
||
873 |
||
874 |
\subsection{Fundamental methods and attributes}\label{sec:pure-meth-att} |
|
875 |
||
8547 | 876 |
The following proof methods and attributes refer to basic logical operations |
877 |
of Isar. Further methods and attributes are provided by several generic and |
|
878 |
object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and |
|
879 |
\ref{ch:hol-tools}). |
|
8515 | 880 |
|
881 |
\indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$} |
|
9936 | 882 |
\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule} |
8515 | 883 |
\indexisaratt{OF}\indexisaratt{of} |
884 |
\begin{matharray}{rcl} |
|
885 |
assumption & : & \isarmeth \\ |
|
886 |
this & : & \isarmeth \\ |
|
887 |
rule & : & \isarmeth \\ |
|
888 |
- & : & \isarmeth \\ |
|
889 |
OF & : & \isaratt \\ |
|
890 |
of & : & \isaratt \\ |
|
891 |
intro & : & \isaratt \\ |
|
892 |
elim & : & \isaratt \\ |
|
893 |
dest & : & \isaratt \\ |
|
9936 | 894 |
rule & : & \isaratt \\ |
8515 | 895 |
\end{matharray} |
896 |
||
897 |
\begin{rail} |
|
8547 | 898 |
'rule' thmrefs? |
8515 | 899 |
; |
900 |
'OF' thmrefs |
|
901 |
; |
|
8693 | 902 |
'of' insts ('concl' ':' insts)? |
8515 | 903 |
; |
9936 | 904 |
'rule' 'del' |
905 |
; |
|
8515 | 906 |
\end{rail} |
907 |
||
908 |
\begin{descr} |
|
909 |
\item [$assumption$] solves some goal by a single assumption step. Any facts |
|
910 |
given (${} \le 1$) are guaranteed to participate in the refinement. Recall |
|
911 |
that $\QEDNAME$ (see \S\ref{sec:proof-steps}) already concludes any |
|
912 |
remaining sub-goals by assumption. |
|
913 |
\item [$this$] applies all of the current facts directly as rules. Recall |
|
914 |
that ``$\DOT$'' (dot) abbreviates $\BY{this}$. |
|
8547 | 915 |
\item [$rule~\vec a$] applies some rule given as argument in backward manner; |
8515 | 916 |
facts are used to reduce the rule before applying it to the goal. Thus |
917 |
$rule$ without facts is plain \emph{introduction}, while with facts it |
|
918 |
becomes \emph{elimination}. |
|
919 |
||
8547 | 920 |
When no arguments are given, the $rule$ method tries to pick appropriate |
921 |
rules automatically, as declared in the current context using the $intro$, |
|
922 |
$elim$, $dest$ attributes (see below). This is the default behavior of |
|
923 |
$\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see |
|
8515 | 924 |
\S\ref{sec:proof-steps}). |
925 |
\item [``$-$''] does nothing but insert the forward chaining facts as premises |
|
926 |
into the goal. Note that command $\PROOFNAME$ without any method actually |
|
927 |
performs a single reduction step using the $rule$ method; thus a plain |
|
928 |
\emph{do-nothing} proof step would be $\PROOF{-}$ rather than $\PROOFNAME$ |
|
929 |
alone. |
|
8547 | 930 |
\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in |
931 |
parallel). This corresponds to the \texttt{MRS} operator in ML |
|
932 |
\cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be |
|
933 |
skipped by including ``$\_$'' (underscore) as argument. |
|
934 |
\item [$of~\vec t$] performs positional instantiation. The terms $\vec t$ are |
|
8515 | 935 |
substituted for any schematic variables occurring in a theorem from left to |
936 |
right; ``\texttt{_}'' (underscore) indicates to skip a position. Arguments |
|
937 |
following a ``$concl\colon$'' specification refer to positions of the |
|
938 |
conclusion of a rule. |
|
939 |
\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and |
|
940 |
destruct rules, respectively. Note that the classical reasoner (see |
|
941 |
\S\ref{sec:classical-basic}) introduces different versions of these |
|
942 |
attributes, and the $rule$ method, too. In object-logics with classical |
|
943 |
reasoning enabled, the latter version should be used all the time to avoid |
|
944 |
confusion! |
|
9936 | 945 |
\item [$rule~del$] undeclares introduction, elimination, or destruct rules. |
7315 | 946 |
\end{descr} |
947 |
||
948 |
||
949 |
\subsection{Term abbreviations}\label{sec:term-abbrev} |
|
950 |
||
951 |
\indexisarcmd{let} |
|
952 |
\begin{matharray}{rcl} |
|
953 |
\isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\ |
|
954 |
\isarkeyword{is} & : & syntax \\ |
|
955 |
\end{matharray} |
|
956 |
||
957 |
Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements, |
|
7987 | 958 |
or by annotating assumptions or goal statements with a list of patterns |
959 |
$\ISS{p@1\;\dots}{p@n}$. In both cases, higher-order matching is invoked to |
|
960 |
bind extra-logical term variables, which may be either named schematic |
|
961 |
variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}'' |
|
962 |
(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the |
|
963 |
patterns occur on the left-hand side, while the $\ISNAME$ patterns are in |
|
964 |
postfix position. |
|
7315 | 965 |
|
8620
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
966 |
Polymorphism of term bindings is handled in Hindley-Milner style, as in ML. |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
967 |
Type variables referring to local assumptions or open goal statements are |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
968 |
\emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
969 |
in \emph{arbitrary} instances later. Even though actual polymorphism should |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
970 |
be rarely used in practice, this mechanism is essential to achieve proper |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
971 |
incremental type-inference, as the user proceeds to build up the Isar proof |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
972 |
text. |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
973 |
|
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
974 |
\medskip |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
975 |
|
7319 | 976 |
Term abbreviations are quite different from actual local definitions as |
977 |
introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are |
|
7315 | 978 |
visible within the logic as actual equations, while abbreviations disappear |
8620
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
979 |
during the input process just after type checking. Also note that $\DEFNAME$ |
3786d47f5570
support Hindley-Milner polymorphisms in results and bindings;
wenzelm
parents:
8547
diff
changeset
|
980 |
does not support polymorphism. |
7315 | 981 |
|
982 |
\begin{rail} |
|
8664 | 983 |
'let' ((term + 'and') '=' term comment? + 'and') |
7315 | 984 |
; |
985 |
\end{rail} |
|
986 |
||
987 |
The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or |
|
988 |
\railnonterm{proppat} (see \S\ref{sec:term-pats}). |
|
989 |
||
990 |
\begin{descr} |
|
991 |
\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$ |
|
992 |
by simultaneous higher-order matching against terms $\vec t$. |
|
993 |
\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the |
|
994 |
preceding statement. Also note that $\ISNAME$ is not a separate command, |
|
995 |
but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). |
|
996 |
\end{descr} |
|
997 |
||
10160 | 998 |
Some \emph{automatic} term abbreviations\index{term abbreviations} for goals |
7988 | 999 |
and facts are available as well. For any open goal, |
10160 | 1000 |
$\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement, |
1001 |
abstracted over any meta-level parameters (if present). Likewise, |
|
1002 |
$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from |
|
1003 |
assumptions or finished goals. In case $\Var{this}$ refers to an object-logic |
|
1004 |
statement that is an application $f(t)$, then $t$ is bound to the special text |
|
1005 |
variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical |
|
1006 |
application of the latter are calculational proofs (see |
|
1007 |
\S\ref{sec:calculation}). |
|
1008 |
||
1009 |
%FIXME !? |
|
7315 | 1010 |
|
10160 | 1011 |
% A few \emph{automatic} term abbreviations\index{term abbreviations} for goals |
1012 |
% and facts are available as well. For any open goal, |
|
1013 |
% $\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition |
|
1014 |
% (which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its |
|
1015 |
% (atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its |
|
1016 |
% object-level statement. The latter two abstract over any meta-level |
|
1017 |
% parameters. |
|
1018 |
||
1019 |
% Fact statements resulting from assumptions or finished goals are bound as |
|
1020 |
% $\Var{this_prop}$\indexisarvar{this-prop}, |
|
1021 |
% $\Var{this_concl}$\indexisarvar{this-concl}, and |
|
1022 |
% $\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above. In case |
|
1023 |
% $\Var{this}$ refers to an object-logic statement that is an application |
|
1024 |
% $f(t)$, then $t$ is bound to the special text variable |
|
1025 |
% ``$\dots$''\indexisarvar{\dots} (three dots). The canonical application of |
|
1026 |
% the latter are calculational proofs (see \S\ref{sec:calculation}). |
|
7315 | 1027 |
|
1028 |
||
7134 | 1029 |
\subsection{Block structure} |
1030 |
||
8896 | 1031 |
\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} |
7397 | 1032 |
\begin{matharray}{rcl} |
8448 | 1033 |
\NEXT & : & \isartrans{proof(state)}{proof(state)} \\ |
7974 | 1034 |
\BG & : & \isartrans{proof(state)}{proof(state)} \\ |
1035 |
\EN & : & \isartrans{proof(state)}{proof(state)} \\ |
|
7397 | 1036 |
\end{matharray} |
1037 |
||
9030 | 1038 |
\railalias{lbrace}{\ttlbrace} |
1039 |
\railterm{lbrace} |
|
1040 |
||
1041 |
\railalias{rbrace}{\ttrbrace} |
|
1042 |
\railterm{rbrace} |
|
1043 |
||
1044 |
\begin{rail} |
|
1045 |
'next' comment? |
|
1046 |
; |
|
1047 |
lbrace comment? |
|
1048 |
; |
|
1049 |
rbrace comment? |
|
1050 |
; |
|
1051 |
\end{rail} |
|
1052 |
||
7167 | 1053 |
While Isar is inherently block-structured, opening and closing blocks is |
1054 |
mostly handled rather casually, with little explicit user-intervention. Any |
|
1055 |
local goal statement automatically opens \emph{two} blocks, which are closed |
|
1056 |
again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of |
|
8448 | 1057 |
different context within a sub-proof may be switched via $\NEXT$, which is |
1058 |
just a single block-close followed by block-open again. Thus the effect of |
|
1059 |
$\NEXT$ to reset the local proof context. There is no goal focus involved |
|
1060 |
here! |
|
7167 | 1061 |
|
7175 | 1062 |
For slightly more advanced applications, there are explicit block parentheses |
7895 | 1063 |
as well. These typically achieve a stronger forward style of reasoning. |
7167 | 1064 |
|
1065 |
\begin{descr} |
|
8448 | 1066 |
\item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the |
1067 |
local context to the initial one. |
|
8896 | 1068 |
\item [$\BG$ and $\EN$] explicitly open and close blocks. Any current facts |
1069 |
pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be |
|
7895 | 1070 |
\emph{exported} into the enclosing context. Thus fixed variables are |
1071 |
generalized, assumptions discharged, and local definitions unfolded (cf.\ |
|
1072 |
\S\ref{sec:proof-context}). There is no difference of $\ASSUMENAME$ and |
|
1073 |
$\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain |
|
1074 |
backward reasoning with the result exported at $\SHOWNAME$ time. |
|
7167 | 1075 |
\end{descr} |
7134 | 1076 |
|
1077 |
||
9605 | 1078 |
\subsection{Emulating tactic scripts}\label{sec:tactic-commands} |
8515 | 1079 |
|
9605 | 1080 |
The Isar provides separate commands to accommodate tactic-style proof scripts |
1081 |
within the same system. While being outside the orthodox Isar proof language, |
|
1082 |
these might come in handy for interactive exploration and debugging, or even |
|
1083 |
actual tactical proof within new-style theories (to benefit from document |
|
1084 |
preparation, for example). See also \S\ref{sec:tactics} for actual tactics, |
|
1085 |
that have been encapsulated as proof methods. Proper proof methods may be |
|
1086 |
used in scripts, too. |
|
8515 | 1087 |
|
9605 | 1088 |
\indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done} |
8515 | 1089 |
\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} |
9605 | 1090 |
\indexisarcmd{declare} |
8515 | 1091 |
\begin{matharray}{rcl} |
8533 | 1092 |
\isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ |
9605 | 1093 |
\isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ |
8946 | 1094 |
\isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ |
8533 | 1095 |
\isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ |
1096 |
\isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ |
|
1097 |
\isarcmd{back}^* & : & \isartrans{proof}{proof} \\ |
|
9605 | 1098 |
\isarcmd{declare}^* & : & \isartrans{theory}{theory} \\ |
8515 | 1099 |
\end{matharray} |
1100 |
||
1101 |
\railalias{applyend}{apply\_end} |
|
1102 |
\railterm{applyend} |
|
1103 |
||
1104 |
\begin{rail} |
|
9605 | 1105 |
( 'apply' | applyend ) method comment? |
8515 | 1106 |
; |
8946 | 1107 |
'done' comment? |
1108 |
; |
|
8682 | 1109 |
'defer' nat? comment? |
8515 | 1110 |
; |
8682 | 1111 |
'prefer' nat comment? |
8515 | 1112 |
; |
9273 | 1113 |
'back' comment? |
1114 |
; |
|
9605 | 1115 |
'declare' thmrefs comment? |
1116 |
; |
|
8515 | 1117 |
\end{rail} |
1118 |
||
1119 |
\begin{descr} |
|
10223 | 1120 |
\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike |
1121 |
$\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method |
|
1122 |
applications may be given just as in tactic scripts. |
|
8515 | 1123 |
|
8881 | 1124 |
Facts are passed to $m$ as indicated by the goal's forward-chain mode, and |
10223 | 1125 |
are \emph{consumed} afterwards. Thus any further $\APPLYNAME$ command would |
1126 |
always work in a purely backward manner. |
|
8946 | 1127 |
|
8515 | 1128 |
\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in |
1129 |
terminal position. Basically, this simulates a multi-step tactic script for |
|
1130 |
$\QEDNAME$, but may be given anywhere within the proof body. |
|
1131 |
||
1132 |
No facts are passed to $m$. Furthermore, the static context is that of the |
|
1133 |
enclosing goal (as for actual $\QEDNAME$). Thus the proof method may not |
|
1134 |
refer to any assumptions introduced in the current body, for example. |
|
9605 | 1135 |
|
1136 |
\item [$\isarkeyword{done}$] completes a proof script, provided that the |
|
1137 |
current goal state is already solved completely. Note that actual |
|
1138 |
structured proof commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to |
|
1139 |
conclude proof scripts as well. |
|
1140 |
||
8515 | 1141 |
\item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list |
1142 |
of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$ |
|
1143 |
by default), while $prefer$ brings goal $n$ to the top. |
|
9605 | 1144 |
|
8515 | 1145 |
\item [$\isarkeyword{back}$] does back-tracking over the result sequence of |
1146 |
the latest proof command.\footnote{Unlike the ML function \texttt{back} |
|
1147 |
\cite{isabelle-ref}, the Isar command does not search upwards for further |
|
1148 |
branch points.} Basically, any proof command may return multiple results. |
|
9605 | 1149 |
|
1150 |
\item [$\isarkeyword{declare}~thms$] declares theorems to the current theory |
|
1151 |
context. No theorem binding is involved here, unlike |
|
1152 |
$\isarkeyword{theorems}$ or $\isarkeyword{lemmas}$ (cf.\ |
|
1153 |
\S\ref{sec:axms-thms}). So $\isarkeyword{declare}$ only has the effect of |
|
1154 |
applying attributes as included in the theorem specification. |
|
9006 | 1155 |
\end{descr} |
1156 |
||
1157 |
Any proper Isar proof method may be used with tactic script commands such as |
|
10223 | 1158 |
$\APPLYNAME$. A few additional emulations of actual tactics are provided as |
1159 |
well; these would be never used in actual structured proofs, of course. |
|
9006 | 1160 |
|
8515 | 1161 |
|
1162 |
\subsection{Meta-linguistic features} |
|
1163 |
||
1164 |
\indexisarcmd{oops} |
|
1165 |
\begin{matharray}{rcl} |
|
1166 |
\isarcmd{oops} & : & \isartrans{proof}{theory} \\ |
|
1167 |
\end{matharray} |
|
1168 |
||
1169 |
The $\OOPS$ command discontinues the current proof attempt, while considering |
|
1170 |
the partial proof text as properly processed. This is conceptually quite |
|
1171 |
different from ``faking'' actual proofs via $\SORRY$ (see |
|
1172 |
\S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all, |
|
1173 |
but goes back right to the theory level. Furthermore, $\OOPS$ does not |
|
1174 |
produce any result theorem --- there is no claim to be able to complete the |
|
1175 |
proof anyhow. |
|
1176 |
||
1177 |
A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the |
|
1178 |
system itself, in conjunction with the document preparation tools of Isabelle |
|
1179 |
described in \cite{isabelle-sys}. Thus partial or even wrong proof attempts |
|
1180 |
can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} |
|
1181 |
macros can be easily adapted to print something like ``$\dots$'' instead of an |
|
1182 |
``$\OOPS$'' keyword. |
|
1183 |
||
8547 | 1184 |
\medskip The $\OOPS$ command is undoable, unlike $\isarkeyword{kill}$ (see |
1185 |
\S\ref{sec:history}). The effect is to get back to the theory \emph{before} |
|
1186 |
the opening of the proof. |
|
8515 | 1187 |
|
1188 |
||
7134 | 1189 |
\section{Other commands} |
1190 |
||
9605 | 1191 |
\subsection{Diagnostics} |
7134 | 1192 |
|
10858 | 1193 |
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term} |
1194 |
\indexisarcmd{prop}\indexisarcmd{typ} |
|
7134 | 1195 |
\begin{matharray}{rcl} |
8515 | 1196 |
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\ |
1197 |
\isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\ |
|
1198 |
\isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\ |
|
1199 |
\isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\ |
|
1200 |
\isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\ |
|
7134 | 1201 |
\end{matharray} |
1202 |
||
9605 | 1203 |
These diagnostic commands assist interactive development. Note that $undo$ |
1204 |
does not apply here, the theory or proof configuration is not changed. |
|
7335 | 1205 |
|
7134 | 1206 |
\begin{rail} |
9727 | 1207 |
'pr' modes? nat? (',' nat)? |
7134 | 1208 |
; |
10584 | 1209 |
'thm' modes? thmrefs comment? |
8485 | 1210 |
; |
10584 | 1211 |
'term' modes? term comment? |
7134 | 1212 |
; |
10584 | 1213 |
'prop' modes? prop comment? |
7134 | 1214 |
; |
10584 | 1215 |
'typ' modes? type comment? |
8485 | 1216 |
; |
1217 |
||
1218 |
modes: '(' (name + ) ')' |
|
7134 | 1219 |
; |
1220 |
\end{rail} |
|
1221 |
||
7167 | 1222 |
\begin{descr} |
9727 | 1223 |
\item [$\isarkeyword{pr}~goals, prems$] prints the current proof state (if |
1224 |
present), including the proof context, current facts and goals. The |
|
1225 |
optional limit arguments affect the number of goals and premises to be |
|
1226 |
displayed, which is initially 10 for both. Omitting limit values leaves the |
|
1227 |
current setting unchanged. |
|
8547 | 1228 |
\item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory |
1229 |
or proof context. Note that any attributes included in the theorem |
|
7974 | 1230 |
specifications are applied to a temporary context derived from the current |
8547 | 1231 |
theory or proof; the result is discarded, i.e.\ attributes involved in $\vec |
1232 |
a$ do not have any permanent effect. |
|
9727 | 1233 |
\item [$\isarkeyword{term}~t$ and $\isarkeyword{prop}~\phi$] read, type-check |
1234 |
and print terms or propositions according to the current theory or proof |
|
7895 | 1235 |
context; the inferred type of $t$ is output as well. Note that these |
1236 |
commands are also useful in inspecting the current environment of term |
|
1237 |
abbreviations. |
|
7974 | 1238 |
\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic |
1239 |
according to the current theory or proof context. |
|
9605 | 1240 |
\end{descr} |
1241 |
||
1242 |
All of the diagnostic commands above admit a list of $modes$ to be specified, |
|
1243 |
which is appended to the current print mode (see also \cite{isabelle-ref}). |
|
1244 |
Thus the output behavior may be modified according particular print mode |
|
1245 |
features. For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would |
|
1246 |
print the current proof state with mathematical symbols and special characters |
|
1247 |
represented in {\LaTeX} source, according to the Isabelle style |
|
1248 |
\cite{isabelle-sys}. |
|
1249 |
||
1250 |
Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic |
|
1251 |
way to include formal items into the printed text document. |
|
1252 |
||
1253 |
||
1254 |
\subsection{Inspecting the context} |
|
1255 |
||
1256 |
\indexisarcmd{print-facts}\indexisarcmd{print-binds} |
|
1257 |
\indexisarcmd{print-commands}\indexisarcmd{print-syntax} |
|
1258 |
\indexisarcmd{print-methods}\indexisarcmd{print-attributes} |
|
10858 | 1259 |
\indexisarcmd{thms-containing}\indexisarcmd{thm-deps} |
1260 |
\indexisarcmd{print-theorems} |
|
9605 | 1261 |
\begin{matharray}{rcl} |
1262 |
\isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\ |
|
1263 |
\isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\ |
|
1264 |
\isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\ |
|
1265 |
\isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\ |
|
10858 | 1266 |
\isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\ |
1267 |
\isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\ |
|
1268 |
\isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\ |
|
9605 | 1269 |
\isarcmd{print_facts}^* & : & \isarkeep{proof} \\ |
1270 |
\isarcmd{print_binds}^* & : & \isarkeep{proof} \\ |
|
1271 |
\end{matharray} |
|
1272 |
||
10858 | 1273 |
\railalias{thmscontaining}{thms\_containing} |
1274 |
\railterm{thmscontaining} |
|
1275 |
||
1276 |
\railalias{thmdeps}{thm\_deps} |
|
1277 |
\railterm{thmdeps} |
|
1278 |
||
1279 |
\begin{rail} |
|
11017 | 1280 |
thmscontaining (term * ) |
10858 | 1281 |
; |
1282 |
thmdeps thmrefs |
|
1283 |
; |
|
1284 |
\end{rail} |
|
1285 |
||
1286 |
These commands print certain parts of the theory and proof context. Note that |
|
1287 |
there are some further ones available, such as for the set of rules declared |
|
1288 |
for simplifications. |
|
9605 | 1289 |
|
1290 |
\begin{descr} |
|
1291 |
\item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax, |
|
1292 |
including keywords and command. |
|
1293 |
\item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and |
|
1294 |
terms, depending on the current context. The output can be very verbose, |
|
1295 |
including grammar tables and syntax translation rules. See \cite[\S7, |
|
1296 |
\S8]{isabelle-ref} for further information on Isabelle's inner syntax. |
|
10858 | 1297 |
\item [$\isarkeyword{print_methods}$] prints all proof methods available in |
1298 |
the current theory context. |
|
1299 |
\item [$\isarkeyword{print_attributes}$] prints all attributes available in |
|
1300 |
the current theory context. |
|
1301 |
\item [$\isarkeyword{print_theorems}$] prints theorems available in the |
|
1302 |
current theory context. In interactive mode this actually refers to the |
|
1303 |
theorems left by the last transaction; this allows to inspect the result of |
|
1304 |
advanced definitional packages, such as $\isarkeyword{datatype}$. |
|
11017 | 1305 |
\item [$\isarkeyword{thms_containing}~\vec t$] retrieves theorems from the |
1306 |
theory context containing all of the constants occurring in the terms $\vec |
|
1307 |
t$. Note that giving the empty list yields \emph{all} theorems of the |
|
1308 |
current theory. |
|
10858 | 1309 |
\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of theorems |
1310 |
and lemmas, using Isabelle's graph browser tool (see also |
|
1311 |
\cite{isabelle-sys}). |
|
8379 | 1312 |
\item [$\isarkeyword{print_facts}$] prints any named facts of the current |
1313 |
context, including assumptions and local results. |
|
1314 |
\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in |
|
1315 |
the context. |
|
8485 | 1316 |
\end{descr} |
1317 |
||
1318 |
||
1319 |
\subsection{History commands}\label{sec:history} |
|
1320 |
||
1321 |
\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill} |
|
1322 |
\begin{matharray}{rcl} |
|
1323 |
\isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\ |
|
1324 |
\isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\ |
|
1325 |
\isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\ |
|
1326 |
\end{matharray} |
|
1327 |
||
1328 |
The Isabelle/Isar top-level maintains a two-stage history, for theory and |
|
1329 |
proof state transformation. Basically, any command can be undone using |
|
1330 |
$\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be |
|
10858 | 1331 |
revoked via $\isarkeyword{redo}$, unless the corresponding |
8485 | 1332 |
$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The |
1333 |
$\isarkeyword{kill}$ command aborts the current history node altogether, |
|
1334 |
discontinuing a proof or even the whole theory. This operation is \emph{not} |
|
1335 |
undoable. |
|
1336 |
||
1337 |
\begin{warn} |
|
8547 | 1338 |
History commands should never be used with user interfaces such as |
1339 |
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of |
|
1340 |
stepping forth and back itself. Interfering by manual $\isarkeyword{undo}$, |
|
8510 | 1341 |
$\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly |
1342 |
result in utter confusion. |
|
8485 | 1343 |
\end{warn} |
1344 |
||
8379 | 1345 |
|
7134 | 1346 |
\subsection{System operations} |
1347 |
||
7167 | 1348 |
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only} |
1349 |
\indexisarcmd{update-thy}\indexisarcmd{update-thy-only} |
|
7134 | 1350 |
\begin{matharray}{rcl} |
8515 | 1351 |
\isarcmd{cd}^* & : & \isarkeep{\cdot} \\ |
1352 |
\isarcmd{pwd}^* & : & \isarkeep{\cdot} \\ |
|
1353 |
\isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\ |
|
1354 |
\isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\ |
|
1355 |
\isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\ |
|
1356 |
\isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\ |
|
7134 | 1357 |
\end{matharray} |
1358 |
||
7167 | 1359 |
\begin{descr} |
7134 | 1360 |
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle |
1361 |
process. |
|
1362 |
\item [$\isarkeyword{pwd}~$] prints the current working directory. |
|
7175 | 1363 |
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$, |
7987 | 1364 |
$\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some |
7895 | 1365 |
theory given as $name$ argument. These commands are basically the same as |
7987 | 1366 |
the corresponding ML functions\footnote{The ML versions also change the |
1367 |
implicit theory context to that of the theory loaded.} (see also |
|
1368 |
\cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may |
|
1369 |
load new- and old-style theories alike. |
|
7167 | 1370 |
\end{descr} |
7134 | 1371 |
|
7987 | 1372 |
These system commands are scarcely used when working with the Proof~General |
1373 |
interface, since loading of theories is done fully transparently. |
|
7134 | 1374 |
|
8379 | 1375 |
|
7046 | 1376 |
%%% Local Variables: |
1377 |
%%% mode: latex |
|
1378 |
%%% TeX-master: "isar-ref" |
|
1379 |
%%% End: |