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