26767
|
1 |
(* $Id$ *)
|
|
2 |
|
|
3 |
theory pure
|
|
4 |
imports CPure
|
|
5 |
begin
|
|
6 |
|
|
7 |
chapter {* Basic language elements \label{ch:pure-syntax} *}
|
|
8 |
|
|
9 |
text {*
|
|
10 |
Subsequently, we introduce the main part of Pure theory and proof
|
|
11 |
commands, together with fundamental proof methods and attributes.
|
|
12 |
\Chref{ch:gen-tools} describes further Isar elements provided by
|
|
13 |
generic tools and packages (such as the Simplifier) that are either
|
|
14 |
part of Pure Isabelle or pre-installed in most object logics.
|
26852
|
15 |
Specific language elements introduced by the major object-logics are
|
|
16 |
described in \chref{ch:hol} (Isabelle/HOL), \chref{ch:holcf}
|
|
17 |
(Isabelle/HOLCF), and \chref{ch:zf} (Isabelle/ZF). Nevertheless,
|
|
18 |
examples given in the generic parts will usually refer to
|
|
19 |
Isabelle/HOL as well.
|
26767
|
20 |
|
|
21 |
\medskip Isar commands may be either \emph{proper} document
|
|
22 |
constructors, or \emph{improper commands}. Some proof methods and
|
|
23 |
attributes introduced later are classified as improper as well.
|
|
24 |
Improper Isar language elements, which are subsequently marked by
|
|
25 |
``@{text "\<^sup>*"}'', are often helpful when developing proof
|
|
26 |
documents, while their use is discouraged for the final
|
|
27 |
human-readable outcome. Typical examples are diagnostic commands
|
|
28 |
that print terms or theorems according to the current context; other
|
|
29 |
commands emulate old-style tactical theorem proving.
|
|
30 |
*}
|
|
31 |
|
|
32 |
|
|
33 |
section {* Theory commands *}
|
|
34 |
|
|
35 |
subsection {* Defining theories \label{sec:begin-thy} *}
|
|
36 |
|
|
37 |
text {*
|
|
38 |
\begin{matharray}{rcl}
|
|
39 |
@{command_def "header"} & : & \isarkeep{toplevel} \\
|
|
40 |
@{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
|
|
41 |
@{command_def "end"} & : & \isartrans{theory}{toplevel} \\
|
|
42 |
\end{matharray}
|
|
43 |
|
|
44 |
Isabelle/Isar theories are defined via theory, which contain both
|
|
45 |
specifications and proofs; occasionally definitional mechanisms also
|
|
46 |
require some explicit proof.
|
|
47 |
|
|
48 |
The first ``real'' command of any theory has to be @{command
|
|
49 |
"theory"}, which starts a new theory based on the merge of existing
|
|
50 |
ones. Just preceding the @{command "theory"} keyword, there may be
|
|
51 |
an optional @{command "header"} declaration, which is relevant to
|
|
52 |
document preparation only; it acts very much like a special
|
|
53 |
pre-theory markup command (cf.\ \secref{sec:markup-thy} and
|
|
54 |
\secref{sec:markup-thy}). The @{command "end"} command concludes a
|
|
55 |
theory development; it has to be the very last command of any theory
|
|
56 |
file loaded in batch-mode.
|
|
57 |
|
|
58 |
\begin{rail}
|
|
59 |
'header' text
|
|
60 |
;
|
|
61 |
'theory' name 'imports' (name +) uses? 'begin'
|
|
62 |
;
|
|
63 |
|
|
64 |
uses: 'uses' ((name | parname) +);
|
|
65 |
\end{rail}
|
|
66 |
|
|
67 |
\begin{descr}
|
|
68 |
|
|
69 |
\item [@{command "header"}~@{text "text"}] provides plain text
|
|
70 |
markup just preceding the formal beginning of a theory. In actual
|
|
71 |
document preparation the corresponding {\LaTeX} macro @{verbatim
|
|
72 |
"\\isamarkupheader"} may be redefined to produce chapter or section
|
|
73 |
headings. See also \secref{sec:markup-thy} and
|
|
74 |
\secref{sec:markup-prf} for further markup commands.
|
|
75 |
|
|
76 |
\item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
|
|
77 |
B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
|
|
78 |
merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
|
|
79 |
|
|
80 |
Due to inclusion of several ancestors, the overall theory structure
|
|
81 |
emerging in an Isabelle session forms a directed acyclic graph
|
|
82 |
(DAG). Isabelle's theory loader ensures that the sources
|
|
83 |
contributing to the development graph are always up-to-date.
|
|
84 |
Changed files are automatically reloaded when processing theory
|
|
85 |
headers.
|
|
86 |
|
|
87 |
The optional @{keyword_def "uses"} specification declares additional
|
|
88 |
dependencies on extra files (usually ML sources). Files will be
|
|
89 |
loaded immediately (as ML), unless the name is put in parentheses,
|
|
90 |
which merely documents the dependency to be resolved later in the
|
|
91 |
text (typically via explicit @{command_ref "use"} in the body text,
|
|
92 |
see \secref{sec:ML}).
|
|
93 |
|
|
94 |
\item [@{command "end"}] concludes the current theory definition or
|
|
95 |
context switch.
|
|
96 |
|
|
97 |
\end{descr}
|
|
98 |
*}
|
|
99 |
|
|
100 |
|
|
101 |
subsection {* Markup commands \label{sec:markup-thy} *}
|
|
102 |
|
|
103 |
text {*
|
|
104 |
\begin{matharray}{rcl}
|
|
105 |
@{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\
|
|
106 |
@{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\
|
|
107 |
@{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\
|
|
108 |
@{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\
|
|
109 |
@{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\
|
|
110 |
@{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\
|
|
111 |
\end{matharray}
|
|
112 |
|
|
113 |
Apart from formal comments (see \secref{sec:comments}), markup
|
|
114 |
commands provide a structured way to insert text into the document
|
|
115 |
generated from a theory (see \cite{isabelle-sys} for more
|
|
116 |
information on Isabelle's document preparation tools).
|
|
117 |
|
|
118 |
\begin{rail}
|
|
119 |
('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text
|
|
120 |
;
|
|
121 |
'text\_raw' text
|
|
122 |
;
|
|
123 |
\end{rail}
|
|
124 |
|
|
125 |
\begin{descr}
|
|
126 |
|
|
127 |
\item [@{command "chapter"}, @{command "section"}, @{command
|
|
128 |
"subsection"}, and @{command "subsubsection"}] mark chapter and
|
|
129 |
section headings.
|
|
130 |
|
|
131 |
\item [@{command "text"}] specifies paragraphs of plain text.
|
|
132 |
|
|
133 |
\item [@{command "text_raw"}] inserts {\LaTeX} source into the
|
|
134 |
output, without additional markup. Thus the full range of document
|
|
135 |
manipulations becomes available.
|
|
136 |
|
|
137 |
\end{descr}
|
|
138 |
|
|
139 |
The @{text "text"} argument of these markup commands (except for
|
|
140 |
@{command "text_raw"}) may contain references to formal entities
|
|
141 |
(``antiquotations'', see also \secref{sec:antiq}). These are
|
|
142 |
interpreted in the present theory context, or the named @{text
|
|
143 |
"target"}.
|
|
144 |
|
|
145 |
Any of these markup elements corresponds to a {\LaTeX} command with
|
|
146 |
the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning
|
|
147 |
commands this is a plain macro with a single argument, e.g.\
|
|
148 |
@{verbatim "\\isamarkupchapter{"}@{text "\<dots>"}@{verbatim "}"} for
|
|
149 |
@{command "chapter"}. The @{command "text"} markup results in a
|
26777
|
150 |
{\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"} @{text
|
|
151 |
"\<dots>"} @{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"}
|
26767
|
152 |
causes the text to be inserted directly into the {\LaTeX} source.
|
|
153 |
|
|
154 |
\medskip Additional markup commands are available for proofs (see
|
|
155 |
\secref{sec:markup-prf}). Also note that the @{command_ref
|
|
156 |
"header"} declaration (see \secref{sec:begin-thy}) admits to insert
|
|
157 |
section markup just preceding the actual theory definition.
|
|
158 |
*}
|
|
159 |
|
|
160 |
|
|
161 |
subsection {* Type classes and sorts \label{sec:classes} *}
|
|
162 |
|
|
163 |
text {*
|
|
164 |
\begin{matharray}{rcll}
|
|
165 |
@{command_def "classes"} & : & \isartrans{theory}{theory} \\
|
|
166 |
@{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
|
|
167 |
@{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\
|
|
168 |
@{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\
|
|
169 |
\end{matharray}
|
|
170 |
|
|
171 |
\begin{rail}
|
|
172 |
'classes' (classdecl +)
|
|
173 |
;
|
|
174 |
'classrel' (nameref ('<' | subseteq) nameref + 'and')
|
|
175 |
;
|
|
176 |
'defaultsort' sort
|
|
177 |
;
|
|
178 |
\end{rail}
|
|
179 |
|
|
180 |
\begin{descr}
|
|
181 |
|
|
182 |
\item [@{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"}]
|
|
183 |
declares class @{text c} to be a subclass of existing classes @{text
|
|
184 |
"c\<^sub>1, \<dots>, c\<^sub>n"}. Cyclic class structures are not permitted.
|
|
185 |
|
|
186 |
\item [@{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"}] states
|
|
187 |
subclass relations between existing classes @{text "c\<^sub>1"} and
|
|
188 |
@{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref
|
|
189 |
"instance"} command (see \secref{sec:axclass}) provides a way to
|
|
190 |
introduce proven class relations.
|
|
191 |
|
|
192 |
\item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the
|
|
193 |
new default sort for any type variables given without sort
|
|
194 |
constraints. Usually, the default sort would be only changed when
|
|
195 |
defining a new object-logic.
|
|
196 |
|
|
197 |
\item [@{command "class_deps"}] visualizes the subclass relation,
|
|
198 |
using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
|
|
199 |
|
|
200 |
\end{descr}
|
|
201 |
*}
|
|
202 |
|
|
203 |
|
|
204 |
subsection {* Primitive types and type abbreviations \label{sec:types-pure} *}
|
|
205 |
|
|
206 |
text {*
|
|
207 |
\begin{matharray}{rcll}
|
|
208 |
@{command_def "types"} & : & \isartrans{theory}{theory} \\
|
|
209 |
@{command_def "typedecl"} & : & \isartrans{theory}{theory} \\
|
|
210 |
@{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\
|
|
211 |
@{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
|
|
212 |
\end{matharray}
|
|
213 |
|
|
214 |
\begin{rail}
|
|
215 |
'types' (typespec '=' type infix? +)
|
|
216 |
;
|
|
217 |
'typedecl' typespec infix?
|
|
218 |
;
|
|
219 |
'nonterminals' (name +)
|
|
220 |
;
|
|
221 |
'arities' (nameref '::' arity +)
|
|
222 |
;
|
|
223 |
\end{rail}
|
|
224 |
|
|
225 |
\begin{descr}
|
|
226 |
|
|
227 |
\item [@{command "types"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>"}]
|
|
228 |
introduces \emph{type synonym} @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}
|
|
229 |
for existing type @{text "\<tau>"}. Unlike actual type definitions, as
|
|
230 |
are available in Isabelle/HOL for example, type synonyms are just
|
|
231 |
purely syntactic abbreviations without any logical significance.
|
|
232 |
Internally, type synonyms are fully expanded.
|
|
233 |
|
|
234 |
\item [@{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"}]
|
|
235 |
declares a new type constructor @{text t}, intended as an actual
|
|
236 |
logical type (of the object-logic, if available).
|
|
237 |
|
|
238 |
\item [@{command "nonterminals"}~@{text c}] declares type
|
|
239 |
constructors @{text c} (without arguments) to act as purely
|
|
240 |
syntactic types, i.e.\ nonterminal symbols of Isabelle's inner
|
|
241 |
syntax of terms or types.
|
|
242 |
|
|
243 |
\item [@{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)
|
|
244 |
s"}] augments Isabelle's order-sorted signature of types by new type
|
|
245 |
constructor arities. This is done axiomatically! The @{command_ref
|
|
246 |
"instance"} command (see \S\ref{sec:axclass}) provides a way to
|
|
247 |
introduce proven type arities.
|
|
248 |
|
|
249 |
\end{descr}
|
|
250 |
*}
|
|
251 |
|
|
252 |
|
|
253 |
subsection {* Primitive constants and definitions \label{sec:consts} *}
|
|
254 |
|
|
255 |
text {*
|
|
256 |
Definitions essentially express abbreviations within the logic. The
|
|
257 |
simplest form of a definition is @{text "c :: \<sigma> \<equiv> t"}, where @{text
|
|
258 |
c} is a newly declared constant. Isabelle also allows derived forms
|
|
259 |
where the arguments of @{text c} appear on the left, abbreviating a
|
|
260 |
prefix of @{text \<lambda>}-abstractions, e.g.\ @{text "c \<equiv> \<lambda>x y. t"} may be
|
|
261 |
written more conveniently as @{text "c x y \<equiv> t"}. Moreover,
|
|
262 |
definitions may be weakened by adding arbitrary pre-conditions:
|
|
263 |
@{text "A \<Longrightarrow> c x y \<equiv> t"}.
|
|
264 |
|
|
265 |
\medskip The built-in well-formedness conditions for definitional
|
|
266 |
specifications are:
|
|
267 |
|
|
268 |
\begin{itemize}
|
|
269 |
|
|
270 |
\item Arguments (on the left-hand side) must be distinct variables.
|
|
271 |
|
|
272 |
\item All variables on the right-hand side must also appear on the
|
|
273 |
left-hand side.
|
|
274 |
|
|
275 |
\item All type variables on the right-hand side must also appear on
|
|
276 |
the left-hand side; this prohibits @{text "0 :: nat \<equiv> length ([] ::
|
|
277 |
\<alpha> list)"} for example.
|
|
278 |
|
|
279 |
\item The definition must not be recursive. Most object-logics
|
|
280 |
provide definitional principles that can be used to express
|
|
281 |
recursion safely.
|
|
282 |
|
|
283 |
\end{itemize}
|
|
284 |
|
|
285 |
Overloading means that a constant being declared as @{text "c :: \<alpha>
|
|
286 |
decl"} may be defined separately on type instances @{text "c ::
|
|
287 |
(\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t decl"} for each type constructor @{text
|
|
288 |
t}. The right-hand side may mention overloaded constants
|
|
289 |
recursively at type instances corresponding to the immediate
|
|
290 |
argument types @{text "\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n"}. Incomplete
|
|
291 |
specification patterns impose global constraints on all occurrences,
|
|
292 |
e.g.\ @{text "d :: \<alpha> \<times> \<alpha>"} on the left-hand side means that all
|
|
293 |
corresponding occurrences on some right-hand side need to be an
|
|
294 |
instance of this, general @{text "d :: \<alpha> \<times> \<beta>"} will be disallowed.
|
|
295 |
|
|
296 |
\begin{matharray}{rcl}
|
|
297 |
@{command_def "consts"} & : & \isartrans{theory}{theory} \\
|
|
298 |
@{command_def "defs"} & : & \isartrans{theory}{theory} \\
|
|
299 |
@{command_def "constdefs"} & : & \isartrans{theory}{theory} \\
|
|
300 |
\end{matharray}
|
|
301 |
|
|
302 |
\begin{rail}
|
|
303 |
'consts' ((name '::' type mixfix?) +)
|
|
304 |
;
|
|
305 |
'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +)
|
|
306 |
;
|
|
307 |
\end{rail}
|
|
308 |
|
|
309 |
\begin{rail}
|
|
310 |
'constdefs' structs? (constdecl? constdef +)
|
|
311 |
;
|
|
312 |
|
|
313 |
structs: '(' 'structure' (vars + 'and') ')'
|
|
314 |
;
|
|
315 |
constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where'
|
|
316 |
;
|
|
317 |
constdef: thmdecl? prop
|
|
318 |
;
|
|
319 |
\end{rail}
|
|
320 |
|
|
321 |
\begin{descr}
|
|
322 |
|
|
323 |
\item [@{command "consts"}~@{text "c :: \<sigma>"}] declares constant
|
|
324 |
@{text c} to have any instance of type scheme @{text \<sigma>}. The
|
|
325 |
optional mixfix annotations may attach concrete syntax to the
|
|
326 |
constants declared.
|
|
327 |
|
|
328 |
\item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn}
|
|
329 |
as a definitional axiom for some existing constant.
|
|
330 |
|
|
331 |
The @{text "(unchecked)"} option disables global dependency checks
|
|
332 |
for this definition, which is occasionally useful for exotic
|
|
333 |
overloading. It is at the discretion of the user to avoid malformed
|
|
334 |
theory specifications!
|
|
335 |
|
|
336 |
The @{text "(overloaded)"} option declares definitions to be
|
|
337 |
potentially overloaded. Unless this option is given, a warning
|
|
338 |
message would be issued for any definitional equation with a more
|
|
339 |
special type than that of the corresponding constant declaration.
|
|
340 |
|
|
341 |
\item [@{command "constdefs"}] provides a streamlined combination of
|
|
342 |
constants declarations and definitions: type-inference takes care of
|
|
343 |
the most general typing of the given specification (the optional
|
26777
|
344 |
type constraint may refer to type-inference dummies ``@{text
|
26767
|
345 |
_}'' as usual). The resulting type declaration needs to agree with
|
|
346 |
that of the specification; overloading is \emph{not} supported here!
|
|
347 |
|
|
348 |
The constant name may be omitted altogether, if neither type nor
|
|
349 |
syntax declarations are given. The canonical name of the
|
|
350 |
definitional axiom for constant @{text c} will be @{text c_def},
|
|
351 |
unless specified otherwise. Also note that the given list of
|
|
352 |
specifications is processed in a strictly sequential manner, with
|
|
353 |
type-checking being performed independently.
|
|
354 |
|
|
355 |
An optional initial context of @{text "(structure)"} declarations
|
|
356 |
admits use of indexed syntax, using the special symbol @{verbatim
|
|
357 |
"\<index>"} (printed as ``@{text "\<index>"}''). The latter concept is
|
|
358 |
particularly useful with locales (see also \S\ref{sec:locale}).
|
|
359 |
|
|
360 |
\end{descr}
|
|
361 |
*}
|
|
362 |
|
|
363 |
|
|
364 |
subsection {* Syntax and translations \label{sec:syn-trans} *}
|
|
365 |
|
|
366 |
text {*
|
|
367 |
\begin{matharray}{rcl}
|
|
368 |
@{command_def "syntax"} & : & \isartrans{theory}{theory} \\
|
|
369 |
@{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\
|
|
370 |
@{command_def "translations"} & : & \isartrans{theory}{theory} \\
|
|
371 |
@{command_def "no_translations"} & : & \isartrans{theory}{theory} \\
|
|
372 |
\end{matharray}
|
|
373 |
|
|
374 |
\begin{rail}
|
|
375 |
('syntax' | 'no\_syntax') mode? (constdecl +)
|
|
376 |
;
|
|
377 |
('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
|
|
378 |
;
|
|
379 |
|
|
380 |
mode: ('(' ( name | 'output' | name 'output' ) ')')
|
|
381 |
;
|
|
382 |
transpat: ('(' nameref ')')? string
|
|
383 |
;
|
|
384 |
\end{rail}
|
|
385 |
|
|
386 |
\begin{descr}
|
|
387 |
|
|
388 |
\item [@{command "syntax"}~@{text "(mode) decls"}] is similar to
|
|
389 |
@{command "consts"}~@{text decls}, except that the actual logical
|
|
390 |
signature extension is omitted. Thus the context free grammar of
|
|
391 |
Isabelle's inner syntax may be augmented in arbitrary ways,
|
|
392 |
independently of the logic. The @{text mode} argument refers to the
|
|
393 |
print mode that the grammar rules belong; unless the @{keyword_ref
|
|
394 |
"output"} indicator is given, all productions are added both to the
|
|
395 |
input and output grammar.
|
|
396 |
|
|
397 |
\item [@{command "no_syntax"}~@{text "(mode) decls"}] removes
|
|
398 |
grammar declarations (and translations) resulting from @{text
|
|
399 |
decls}, which are interpreted in the same manner as for @{command
|
|
400 |
"syntax"} above.
|
|
401 |
|
|
402 |
\item [@{command "translations"}~@{text rules}] specifies syntactic
|
|
403 |
translation rules (i.e.\ macros): parse~/ print rules (@{text "\<rightleftharpoons>"}),
|
|
404 |
parse rules (@{text "\<rightharpoonup>"}), or print rules (@{text "\<leftharpoondown>"}).
|
|
405 |
Translation patterns may be prefixed by the syntactic category to be
|
|
406 |
used for parsing; the default is @{text logic}.
|
|
407 |
|
|
408 |
\item [@{command "no_translations"}~@{text rules}] removes syntactic
|
|
409 |
translation rules, which are interpreted in the same manner as for
|
|
410 |
@{command "translations"} above.
|
|
411 |
|
|
412 |
\end{descr}
|
|
413 |
*}
|
|
414 |
|
|
415 |
|
|
416 |
subsection {* Axioms and theorems \label{sec:axms-thms} *}
|
|
417 |
|
|
418 |
text {*
|
|
419 |
\begin{matharray}{rcll}
|
|
420 |
@{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
|
|
421 |
@{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
|
|
422 |
@{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\
|
|
423 |
\end{matharray}
|
|
424 |
|
|
425 |
\begin{rail}
|
|
426 |
'axioms' (axmdecl prop +)
|
|
427 |
;
|
|
428 |
('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and')
|
|
429 |
;
|
|
430 |
\end{rail}
|
|
431 |
|
|
432 |
\begin{descr}
|
|
433 |
|
|
434 |
\item [@{command "axioms"}~@{text "a: \<phi>"}] introduces arbitrary
|
|
435 |
statements as axioms of the meta-logic. In fact, axioms are
|
|
436 |
``axiomatic theorems'', and may be referred later just as any other
|
|
437 |
theorem.
|
|
438 |
|
|
439 |
Axioms are usually only introduced when declaring new logical
|
|
440 |
systems. Everyday work is typically done the hard way, with proper
|
|
441 |
definitions and proven theorems.
|
|
442 |
|
|
443 |
\item [@{command "lemmas"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
|
|
444 |
retrieves and stores existing facts in the theory context, or the
|
|
445 |
specified target context (see also \secref{sec:target}). Typical
|
|
446 |
applications would also involve attributes, to declare Simplifier
|
|
447 |
rules, for example.
|
|
448 |
|
|
449 |
\item [@{command "theorems"}] is essentially the same as @{command
|
|
450 |
"lemmas"}, but marks the result as a different kind of facts.
|
|
451 |
|
|
452 |
\end{descr}
|
|
453 |
*}
|
|
454 |
|
|
455 |
|
|
456 |
subsection {* Name spaces *}
|
|
457 |
|
|
458 |
text {*
|
|
459 |
\begin{matharray}{rcl}
|
|
460 |
@{command_def "global"} & : & \isartrans{theory}{theory} \\
|
|
461 |
@{command_def "local"} & : & \isartrans{theory}{theory} \\
|
|
462 |
@{command_def "hide"} & : & \isartrans{theory}{theory} \\
|
|
463 |
\end{matharray}
|
|
464 |
|
|
465 |
\begin{rail}
|
|
466 |
'hide' ('(open)')? name (nameref + )
|
|
467 |
;
|
|
468 |
\end{rail}
|
|
469 |
|
|
470 |
Isabelle organizes any kind of name declarations (of types,
|
|
471 |
constants, theorems etc.) by separate hierarchically structured name
|
|
472 |
spaces. Normally the user does not have to control the behavior of
|
|
473 |
name spaces by hand, yet the following commands provide some way to
|
|
474 |
do so.
|
|
475 |
|
|
476 |
\begin{descr}
|
|
477 |
|
|
478 |
\item [@{command "global"} and @{command "local"}] change the
|
|
479 |
current name declaration mode. Initially, theories start in
|
|
480 |
@{command "local"} mode, causing all names to be automatically
|
|
481 |
qualified by the theory name. Changing this to @{command "global"}
|
|
482 |
causes all names to be declared without the theory prefix, until
|
|
483 |
@{command "local"} is declared again.
|
|
484 |
|
|
485 |
Note that global names are prone to get hidden accidently later,
|
|
486 |
when qualified names of the same base name are introduced.
|
|
487 |
|
|
488 |
\item [@{command "hide"}~@{text "space names"}] fully removes
|
|
489 |
declarations from a given name space (which may be @{text "class"},
|
|
490 |
@{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text
|
|
491 |
"(open)"} option, only the base name is hidden. Global
|
|
492 |
(unqualified) names may never be hidden.
|
|
493 |
|
|
494 |
Note that hiding name space accesses has no impact on logical
|
|
495 |
declarations -- they remain valid internally. Entities that are no
|
|
496 |
longer accessible to the user are printed with the special qualifier
|
|
497 |
``@{text "??"}'' prefixed to the full internal name.
|
|
498 |
|
|
499 |
\end{descr}
|
|
500 |
*}
|
|
501 |
|
|
502 |
|
|
503 |
subsection {* Incorporating ML code \label{sec:ML} *}
|
|
504 |
|
|
505 |
text {*
|
|
506 |
\begin{matharray}{rcl}
|
|
507 |
@{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
|
|
508 |
@{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
|
|
509 |
@{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
|
|
510 |
@{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
|
|
511 |
@{command_def "setup"} & : & \isartrans{theory}{theory} \\
|
|
512 |
@{command_def "method_setup"} & : & \isartrans{theory}{theory} \\
|
|
513 |
\end{matharray}
|
|
514 |
|
|
515 |
\begin{rail}
|
|
516 |
'use' name
|
|
517 |
;
|
|
518 |
('ML' | 'ML\_val' | 'ML\_command' | 'setup') text
|
|
519 |
;
|
|
520 |
'method\_setup' name '=' text text
|
|
521 |
;
|
|
522 |
\end{rail}
|
|
523 |
|
|
524 |
\begin{descr}
|
|
525 |
|
|
526 |
\item [@{command "use"}~@{text "file"}] reads and executes ML
|
|
527 |
commands from @{text "file"}. The current theory context is passed
|
|
528 |
down to the ML toplevel and may be modified, using @{ML
|
|
529 |
"Context.>>"} or derived ML commands. The file name is checked with
|
|
530 |
the @{keyword_ref "uses"} dependency declaration given in the theory
|
|
531 |
header (see also \secref{sec:begin-thy}).
|
|
532 |
|
|
533 |
\item [@{command "ML"}~@{text "text"}] is similar to @{command
|
|
534 |
"use"}, but executes ML commands directly from the given @{text
|
|
535 |
"text"}.
|
|
536 |
|
|
537 |
\item [@{command "ML_val"} and @{command "ML_command"}] are
|
|
538 |
diagnostic versions of @{command "ML"}, which means that the context
|
|
539 |
may not be updated. @{command "ML_val"} echos the bindings produced
|
|
540 |
at the ML toplevel, but @{command "ML_command"} is silent.
|
|
541 |
|
|
542 |
\item [@{command "setup"}~@{text "text"}] changes the current theory
|
|
543 |
context by applying @{text "text"}, which refers to an ML expression
|
|
544 |
of type @{ML_type "theory -> theory"}. This enables to initialize
|
|
545 |
any object-logic specific tools and packages written in ML, for
|
|
546 |
example.
|
|
547 |
|
|
548 |
\item [@{command "method_setup"}~@{text "name = text description"}]
|
|
549 |
defines a proof method in the current theory. The given @{text
|
|
550 |
"text"} has to be an ML expression of type @{ML_type "Args.src ->
|
|
551 |
Proof.context -> Proof.method"}. Parsing concrete method syntax
|
|
552 |
from @{ML_type Args.src} input can be quite tedious in general. The
|
|
553 |
following simple examples are for methods without any explicit
|
|
554 |
arguments, or a list of theorems, respectively.
|
|
555 |
|
|
556 |
%FIXME proper antiquotations
|
|
557 |
{\footnotesize
|
|
558 |
\begin{verbatim}
|
|
559 |
Method.no_args (Method.METHOD (fn facts => foobar_tac))
|
|
560 |
Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
|
|
561 |
Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
|
|
562 |
Method.thms_ctxt_args (fn thms => fn ctxt =>
|
|
563 |
Method.METHOD (fn facts => foobar_tac))
|
|
564 |
\end{verbatim}
|
|
565 |
}
|
|
566 |
|
|
567 |
Note that mere tactic emulations may ignore the @{text facts}
|
|
568 |
parameter above. Proper proof methods would do something
|
|
569 |
appropriate with the list of current facts, though. Single-rule
|
|
570 |
methods usually do strict forward-chaining (e.g.\ by using @{ML
|
|
571 |
Drule.multi_resolves}), while automatic ones just insert the facts
|
|
572 |
using @{ML Method.insert_tac} before applying the main tactic.
|
|
573 |
|
|
574 |
\end{descr}
|
|
575 |
*}
|
|
576 |
|
|
577 |
|
|
578 |
subsection {* Syntax translation functions *}
|
|
579 |
|
|
580 |
text {*
|
|
581 |
\begin{matharray}{rcl}
|
|
582 |
@{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\
|
|
583 |
@{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\
|
|
584 |
@{command_def "print_translation"} & : & \isartrans{theory}{theory} \\
|
|
585 |
@{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\
|
|
586 |
@{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\
|
|
587 |
@{command_def "token_translation"} & : & \isartrans{theory}{theory} \\
|
|
588 |
\end{matharray}
|
|
589 |
|
|
590 |
\begin{rail}
|
|
591 |
( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
|
|
592 |
'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
|
|
593 |
;
|
|
594 |
|
|
595 |
'token\_translation' text
|
|
596 |
;
|
|
597 |
\end{rail}
|
|
598 |
|
|
599 |
Syntax translation functions written in ML admit almost arbitrary
|
|
600 |
manipulations of Isabelle's inner syntax. Any of the above commands
|
|
601 |
have a single \railqtok{text} argument that refers to an ML
|
|
602 |
expression of appropriate type, which are as follows by default:
|
|
603 |
|
|
604 |
%FIXME proper antiquotations
|
|
605 |
\begin{ttbox}
|
|
606 |
val parse_ast_translation : (string * (ast list -> ast)) list
|
|
607 |
val parse_translation : (string * (term list -> term)) list
|
|
608 |
val print_translation : (string * (term list -> term)) list
|
|
609 |
val typed_print_translation :
|
|
610 |
(string * (bool -> typ -> term list -> term)) list
|
|
611 |
val print_ast_translation : (string * (ast list -> ast)) list
|
|
612 |
val token_translation :
|
|
613 |
(string * string * (string -> string * real)) list
|
|
614 |
\end{ttbox}
|
|
615 |
|
|
616 |
If the @{text "(advanced)"} option is given, the corresponding
|
|
617 |
translation functions may depend on the current theory or proof
|
|
618 |
context. This allows to implement advanced syntax mechanisms, as
|
|
619 |
translations functions may refer to specific theory declarations or
|
|
620 |
auxiliary proof data.
|
|
621 |
|
|
622 |
See also \cite[\S8]{isabelle-ref} for more information on the
|
|
623 |
general concept of syntax transformations in Isabelle.
|
|
624 |
|
|
625 |
%FIXME proper antiquotations
|
|
626 |
\begin{ttbox}
|
|
627 |
val parse_ast_translation:
|
|
628 |
(string * (Context.generic -> ast list -> ast)) list
|
|
629 |
val parse_translation:
|
|
630 |
(string * (Context.generic -> term list -> term)) list
|
|
631 |
val print_translation:
|
|
632 |
(string * (Context.generic -> term list -> term)) list
|
|
633 |
val typed_print_translation:
|
|
634 |
(string * (Context.generic -> bool -> typ -> term list -> term)) list
|
|
635 |
val print_ast_translation:
|
|
636 |
(string * (Context.generic -> ast list -> ast)) list
|
|
637 |
\end{ttbox}
|
|
638 |
*}
|
|
639 |
|
|
640 |
|
|
641 |
subsection {* Oracles *}
|
|
642 |
|
|
643 |
text {*
|
|
644 |
\begin{matharray}{rcl}
|
|
645 |
@{command_def "oracle"} & : & \isartrans{theory}{theory} \\
|
|
646 |
\end{matharray}
|
|
647 |
|
|
648 |
The oracle interface promotes a given ML function @{ML_text
|
26777
|
649 |
"theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some
|
|
650 |
type @{ML_text T} given by the user. This acts like an infinitary
|
26767
|
651 |
specification of axioms -- there is no internal check of the
|
|
652 |
correctness of the results! The inference kernel records oracle
|
|
653 |
invocations within the internal derivation object of theorems, and
|
|
654 |
the pretty printer attaches ``@{text "[!]"}'' to indicate results
|
|
655 |
that are not fully checked by Isabelle inferences.
|
|
656 |
|
|
657 |
\begin{rail}
|
|
658 |
'oracle' name '(' type ')' '=' text
|
|
659 |
;
|
|
660 |
\end{rail}
|
|
661 |
|
|
662 |
\begin{descr}
|
|
663 |
|
|
664 |
\item [@{command "oracle"}~@{text "name (type) = text"}] turns the
|
26777
|
665 |
given ML expression @{text "text"} of type
|
|
666 |
@{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> term"} into an
|
|
667 |
ML function of type
|
|
668 |
@{ML_text "theory ->"}~@{text "type"}~@{ML_text "-> thm"}, which is
|
|
669 |
bound to the global identifier @{ML_text name}.
|
26767
|
670 |
|
|
671 |
\end{descr}
|
|
672 |
*}
|
|
673 |
|
|
674 |
|
|
675 |
section {* Proof commands *}
|
|
676 |
|
|
677 |
text {*
|
|
678 |
Proof commands perform transitions of Isar/VM machine
|
|
679 |
configurations, which are block-structured, consisting of a stack of
|
|
680 |
nodes with three main components: logical proof context, current
|
|
681 |
facts, and open goals. Isar/VM transitions are \emph{typed}
|
|
682 |
according to the following three different modes of operation:
|
|
683 |
|
|
684 |
\begin{descr}
|
|
685 |
|
|
686 |
\item [@{text "proof(prove)"}] means that a new goal has just been
|
|
687 |
stated that is now to be \emph{proven}; the next command may refine
|
|
688 |
it by some proof method, and enter a sub-proof to establish the
|
|
689 |
actual result.
|
|
690 |
|
|
691 |
\item [@{text "proof(state)"}] is like a nested theory mode: the
|
|
692 |
context may be augmented by \emph{stating} additional assumptions,
|
|
693 |
intermediate results etc.
|
|
694 |
|
|
695 |
\item [@{text "proof(chain)"}] is intermediate between @{text
|
|
696 |
"proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
|
|
697 |
the contents of the special ``@{fact_ref this}'' register) have been
|
|
698 |
just picked up in order to be used when refining the goal claimed
|
|
699 |
next.
|
|
700 |
|
|
701 |
\end{descr}
|
|
702 |
|
|
703 |
The proof mode indicator may be read as a verb telling the writer
|
|
704 |
what kind of operation may be performed next. The corresponding
|
|
705 |
typings of proof commands restricts the shape of well-formed proof
|
|
706 |
texts to particular command sequences. So dynamic arrangements of
|
|
707 |
commands eventually turn out as static texts of a certain structure.
|
|
708 |
\Appref{ap:refcard} gives a simplified grammar of the overall
|
|
709 |
(extensible) language emerging that way.
|
|
710 |
*}
|
|
711 |
|
|
712 |
|
|
713 |
subsection {* Markup commands \label{sec:markup-prf} *}
|
|
714 |
|
|
715 |
text {*
|
|
716 |
\begin{matharray}{rcl}
|
|
717 |
@{command_def "sect"} & : & \isartrans{proof}{proof} \\
|
|
718 |
@{command_def "subsect"} & : & \isartrans{proof}{proof} \\
|
|
719 |
@{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\
|
|
720 |
@{command_def "txt"} & : & \isartrans{proof}{proof} \\
|
|
721 |
@{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\
|
|
722 |
\end{matharray}
|
|
723 |
|
|
724 |
These markup commands for proof mode closely correspond to the ones
|
|
725 |
of theory mode (see \S\ref{sec:markup-thy}).
|
|
726 |
|
|
727 |
\begin{rail}
|
|
728 |
('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text
|
|
729 |
;
|
|
730 |
\end{rail}
|
|
731 |
*}
|
|
732 |
|
|
733 |
|
|
734 |
subsection {* Context elements \label{sec:proof-context} *}
|
|
735 |
|
|
736 |
text {*
|
|
737 |
\begin{matharray}{rcl}
|
|
738 |
@{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
739 |
@{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
740 |
@{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
741 |
@{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
742 |
\end{matharray}
|
|
743 |
|
|
744 |
The logical proof context consists of fixed variables and
|
|
745 |
assumptions. The former closely correspond to Skolem constants, or
|
|
746 |
meta-level universal quantification as provided by the Isabelle/Pure
|
|
747 |
logical framework. Introducing some \emph{arbitrary, but fixed}
|
26777
|
748 |
variable via ``@{command "fix"}~@{text x}'' results in a local value
|
26767
|
749 |
that may be used in the subsequent proof as any other variable or
|
|
750 |
constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
|
|
751 |
the context will be universally closed wrt.\ @{text x} at the
|
|
752 |
outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
|
|
753 |
form using Isabelle's meta-variables).
|
|
754 |
|
|
755 |
Similarly, introducing some assumption @{text \<chi>} has two effects.
|
|
756 |
On the one hand, a local theorem is created that may be used as a
|
|
757 |
fact in subsequent proof steps. On the other hand, any result
|
|
758 |
@{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
|
|
759 |
the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
|
|
760 |
using such a result would basically introduce a new subgoal stemming
|
|
761 |
from the assumption. How this situation is handled depends on the
|
|
762 |
version of assumption command used: while @{command "assume"}
|
|
763 |
insists on solving the subgoal by unification with some premise of
|
|
764 |
the goal, @{command "presume"} leaves the subgoal unchanged in order
|
|
765 |
to be proved later by the user.
|
|
766 |
|
|
767 |
Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
|
|
768 |
t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
|
|
769 |
another version of assumption that causes any hypothetical equation
|
|
770 |
@{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
|
|
771 |
exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
|
|
772 |
\<phi>[t]"}.
|
|
773 |
|
|
774 |
\begin{rail}
|
|
775 |
'fix' (vars + 'and')
|
|
776 |
;
|
|
777 |
('assume' | 'presume') (props + 'and')
|
|
778 |
;
|
|
779 |
'def' (def + 'and')
|
|
780 |
;
|
|
781 |
def: thmdecl? \\ name ('==' | equiv) term termpat?
|
|
782 |
;
|
|
783 |
\end{rail}
|
|
784 |
|
|
785 |
\begin{descr}
|
|
786 |
|
|
787 |
\item [@{command "fix"}~@{text x}] introduces a local variable
|
|
788 |
@{text x} that is \emph{arbitrary, but fixed.}
|
|
789 |
|
|
790 |
\item [@{command "assume"}~@{text "a: \<phi>"} and @{command
|
|
791 |
"presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
|
|
792 |
assumption. Subsequent results applied to an enclosing goal (e.g.\
|
|
793 |
by @{command_ref "show"}) are handled as follows: @{command
|
|
794 |
"assume"} expects to be able to unify with existing premises in the
|
|
795 |
goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
|
|
796 |
|
|
797 |
Several lists of assumptions may be given (separated by
|
|
798 |
@{keyword_ref "and"}; the resulting list of current facts consists
|
|
799 |
of all of these concatenated.
|
|
800 |
|
|
801 |
\item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
|
|
802 |
(non-polymorphic) definition. In results exported from the context,
|
|
803 |
@{text x} is replaced by @{text t}. Basically, ``@{command
|
|
804 |
"def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
|
|
805 |
x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
|
|
806 |
hypothetical equation solved by reflexivity.
|
|
807 |
|
|
808 |
The default name for the definitional equation is @{text x_def}.
|
|
809 |
Several simultaneous definitions may be given at the same time.
|
|
810 |
|
|
811 |
\end{descr}
|
|
812 |
|
|
813 |
The special name @{fact_ref prems} refers to all assumptions of the
|
|
814 |
current context as a list of theorems. This feature should be used
|
|
815 |
with great care! It is better avoided in final proof texts.
|
|
816 |
*}
|
|
817 |
|
|
818 |
|
|
819 |
subsection {* Facts and forward chaining *}
|
|
820 |
|
|
821 |
text {*
|
|
822 |
\begin{matharray}{rcl}
|
|
823 |
@{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
824 |
@{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
825 |
@{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
826 |
@{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
|
|
827 |
@{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
|
|
828 |
@{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
|
|
829 |
\end{matharray}
|
|
830 |
|
|
831 |
New facts are established either by assumption or proof of local
|
|
832 |
statements. Any fact will usually be involved in further proofs,
|
|
833 |
either as explicit arguments of proof methods, or when forward
|
|
834 |
chaining towards the next goal via @{command "then"} (and variants);
|
|
835 |
@{command "from"} and @{command "with"} are composite forms
|
|
836 |
involving @{command "note"}. The @{command "using"} elements
|
|
837 |
augments the collection of used facts \emph{after} a goal has been
|
|
838 |
stated. Note that the special theorem name @{fact_ref this} refers
|
|
839 |
to the most recently established facts, but only \emph{before}
|
|
840 |
issuing a follow-up claim.
|
|
841 |
|
|
842 |
\begin{rail}
|
|
843 |
'note' (thmdef? thmrefs + 'and')
|
|
844 |
;
|
|
845 |
('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
|
|
846 |
;
|
|
847 |
\end{rail}
|
|
848 |
|
|
849 |
\begin{descr}
|
|
850 |
|
|
851 |
\item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
|
|
852 |
recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
|
|
853 |
the result as @{text a}. Note that attributes may be involved as
|
|
854 |
well, both on the left and right hand sides.
|
|
855 |
|
|
856 |
\item [@{command "then"}] indicates forward chaining by the current
|
|
857 |
facts in order to establish the goal to be claimed next. The
|
|
858 |
initial proof method invoked to refine that will be offered the
|
|
859 |
facts to do ``anything appropriate'' (see also
|
|
860 |
\secref{sec:proof-steps}). For example, method @{method_ref rule}
|
|
861 |
(see \secref{sec:pure-meth-att}) would typically do an elimination
|
|
862 |
rather than an introduction. Automatic methods usually insert the
|
|
863 |
facts into the goal state before operation. This provides a simple
|
|
864 |
scheme to control relevance of facts in automated proof search.
|
|
865 |
|
|
866 |
\item [@{command "from"}~@{text b}] abbreviates ``@{command
|
|
867 |
"note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
|
|
868 |
equivalent to ``@{command "from"}~@{text this}''.
|
|
869 |
|
|
870 |
\item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
|
|
871 |
abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
|
|
872 |
this"}''; thus the forward chaining is from earlier facts together
|
|
873 |
with the current ones.
|
|
874 |
|
|
875 |
\item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
|
|
876 |
the facts being currently indicated for use by a subsequent
|
|
877 |
refinement step (such as @{command_ref "apply"} or @{command_ref
|
|
878 |
"proof"}).
|
|
879 |
|
|
880 |
\item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
|
|
881 |
structurally similar to @{command "using"}, but unfolds definitional
|
|
882 |
equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
|
|
883 |
and facts.
|
|
884 |
|
|
885 |
\end{descr}
|
|
886 |
|
|
887 |
Forward chaining with an empty list of theorems is the same as not
|
|
888 |
chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
|
|
889 |
effect apart from entering @{text "prove(chain)"} mode, since
|
|
890 |
@{fact_ref nothing} is bound to the empty list of theorems.
|
|
891 |
|
|
892 |
Basic proof methods (such as @{method_ref rule}) expect multiple
|
|
893 |
facts to be given in their proper order, corresponding to a prefix
|
|
894 |
of the premises of the rule involved. Note that positions may be
|
|
895 |
easily skipped using something like @{command "from"}~@{text "_
|
|
896 |
\<AND> a \<AND> b"}, for example. This involves the trivial rule
|
|
897 |
@{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
|
|
898 |
``@{fact_ref "_"}'' (underscore).
|
|
899 |
|
|
900 |
Automated methods (such as @{method simp} or @{method auto}) just
|
|
901 |
insert any given facts before their usual operation. Depending on
|
|
902 |
the kind of procedure involved, the order of facts is less
|
|
903 |
significant here.
|
|
904 |
*}
|
|
905 |
|
|
906 |
|
|
907 |
subsection {* Goal statements \label{sec:goals} *}
|
|
908 |
|
|
909 |
text {*
|
|
910 |
\begin{matharray}{rcl}
|
26866
|
911 |
@{command_def "lemma"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
|
|
912 |
@{command_def "theorem"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
|
|
913 |
@{command_def "corollary"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
|
|
914 |
@{command_def "have"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
|
|
915 |
@{command_def "show"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
|
|
916 |
@{command_def "hence"} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
917 |
@{command_def "thus"} & : & \isartrans{proof(state)}{proof(prove)} \\
|
|
918 |
@{command_def "print_statement"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
26767
|
919 |
\end{matharray}
|
|
920 |
|
|
921 |
From a theory context, proof mode is entered by an initial goal
|
|
922 |
command such as @{command "lemma"}, @{command "theorem"}, or
|
|
923 |
@{command "corollary"}. Within a proof, new claims may be
|
|
924 |
introduced locally as well; four variants are available here to
|
|
925 |
indicate whether forward chaining of facts should be performed
|
|
926 |
initially (via @{command_ref "then"}), and whether the final result
|
|
927 |
is meant to solve some pending goal.
|
|
928 |
|
|
929 |
Goals may consist of multiple statements, resulting in a list of
|
|
930 |
facts eventually. A pending multi-goal is internally represented as
|
|
931 |
a meta-level conjunction (printed as @{text "&&"}), which is usually
|
|
932 |
split into the corresponding number of sub-goals prior to an initial
|
|
933 |
method application, via @{command_ref "proof"}
|
|
934 |
(\secref{sec:proof-steps}) or @{command_ref "apply"}
|
|
935 |
(\secref{sec:tactic-commands}). The @{method_ref induct} method
|
|
936 |
covered in \secref{sec:cases-induct} acts on multiple claims
|
|
937 |
simultaneously.
|
|
938 |
|
|
939 |
Claims at the theory level may be either in short or long form. A
|
|
940 |
short goal merely consists of several simultaneous propositions
|
|
941 |
(often just one). A long goal includes an explicit context
|
|
942 |
specification for the subsequent conclusion, involving local
|
|
943 |
parameters and assumptions. Here the role of each part of the
|
|
944 |
statement is explicitly marked by separate keywords (see also
|
|
945 |
\secref{sec:locale}); the local assumptions being introduced here
|
|
946 |
are available as @{fact_ref assms} in the proof. Moreover, there
|
|
947 |
are two kinds of conclusions: @{element_def "shows"} states several
|
|
948 |
simultaneous propositions (essentially a big conjunction), while
|
|
949 |
@{element_def "obtains"} claims several simultaneous simultaneous
|
|
950 |
contexts of (essentially a big disjunction of eliminated parameters
|
|
951 |
and assumptions, cf.\ \secref{sec:obtain}).
|
|
952 |
|
|
953 |
\begin{rail}
|
|
954 |
('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
|
|
955 |
;
|
|
956 |
('have' | 'show' | 'hence' | 'thus') goal
|
|
957 |
;
|
|
958 |
'print\_statement' modes? thmrefs
|
|
959 |
;
|
|
960 |
|
|
961 |
goal: (props + 'and')
|
|
962 |
;
|
|
963 |
longgoal: thmdecl? (contextelem *) conclusion
|
|
964 |
;
|
|
965 |
conclusion: 'shows' goal | 'obtains' (parname? case + '|')
|
|
966 |
;
|
|
967 |
case: (vars + 'and') 'where' (props + 'and')
|
|
968 |
;
|
|
969 |
\end{rail}
|
|
970 |
|
|
971 |
\begin{descr}
|
|
972 |
|
|
973 |
\item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
|
|
974 |
@{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
|
|
975 |
\<phi>"} to be put back into the target context. An additional
|
|
976 |
\railnonterm{context} specification may build up an initial proof
|
|
977 |
context for the subsequent claim; this includes local definitions
|
|
978 |
and syntax as well, see the definition of @{syntax contextelem} in
|
|
979 |
\secref{sec:locale}.
|
|
980 |
|
|
981 |
\item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
|
|
982 |
"corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
|
|
983 |
"lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
|
|
984 |
being of a different kind. This discrimination acts like a formal
|
|
985 |
comment.
|
|
986 |
|
|
987 |
\item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
|
|
988 |
eventually resulting in a fact within the current logical context.
|
|
989 |
This operation is completely independent of any pending sub-goals of
|
|
990 |
an enclosing goal statements, so @{command "have"} may be freely
|
|
991 |
used for experimental exploration of potential results within a
|
|
992 |
proof body.
|
|
993 |
|
|
994 |
\item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
|
|
995 |
"have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
|
|
996 |
sub-goal for each one of the finished result, after having been
|
|
997 |
exported into the corresponding context (at the head of the
|
|
998 |
sub-proof of this @{command "show"} command).
|
|
999 |
|
|
1000 |
To accommodate interactive debugging, resulting rules are printed
|
|
1001 |
before being applied internally. Even more, interactive execution
|
|
1002 |
of @{command "show"} predicts potential failure and displays the
|
|
1003 |
resulting error as a warning beforehand. Watch out for the
|
|
1004 |
following message:
|
|
1005 |
|
|
1006 |
%FIXME proper antiquitation
|
|
1007 |
\begin{ttbox}
|
|
1008 |
Problem! Local statement will fail to solve any pending goal
|
|
1009 |
\end{ttbox}
|
|
1010 |
|
|
1011 |
\item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
|
|
1012 |
"have"}'', i.e.\ claims a local goal to be proven by forward
|
|
1013 |
chaining the current facts. Note that @{command "hence"} is also
|
|
1014 |
equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
|
|
1015 |
|
|
1016 |
\item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
|
|
1017 |
"show"}''. Note that @{command "thus"} is also equivalent to
|
|
1018 |
``@{command "from"}~@{text this}~@{command "show"}''.
|
|
1019 |
|
|
1020 |
\item [@{command "print_statement"}~@{text a}] prints facts from the
|
|
1021 |
current theory or proof context in long statement form, according to
|
|
1022 |
the syntax for @{command "lemma"} given above.
|
|
1023 |
|
|
1024 |
\end{descr}
|
|
1025 |
|
|
1026 |
Any goal statement causes some term abbreviations (such as
|
|
1027 |
@{variable_ref "?thesis"}) to be bound automatically, see also
|
|
1028 |
\secref{sec:term-abbrev}. Furthermore, the local context of a
|
|
1029 |
(non-atomic) goal is provided via the @{case_ref rule_context} case.
|
|
1030 |
|
|
1031 |
The optional case names of @{element_ref "obtains"} have a twofold
|
|
1032 |
meaning: (1) during the of this claim they refer to the the local
|
|
1033 |
context introductions, (2) the resulting rule is annotated
|
|
1034 |
accordingly to support symbolic case splits when used with the
|
|
1035 |
@{method_ref cases} method (cf. \secref{sec:cases-induct}).
|
|
1036 |
|
|
1037 |
\medskip
|
|
1038 |
|
|
1039 |
\begin{warn}
|
|
1040 |
Isabelle/Isar suffers theory-level goal statements to contain
|
|
1041 |
\emph{unbound schematic variables}, although this does not conform
|
|
1042 |
to the aim of human-readable proof documents! The main problem
|
|
1043 |
with schematic goals is that the actual outcome is usually hard to
|
|
1044 |
predict, depending on the behavior of the proof methods applied
|
|
1045 |
during the course of reasoning. Note that most semi-automated
|
|
1046 |
methods heavily depend on several kinds of implicit rule
|
|
1047 |
declarations within the current theory context. As this would
|
|
1048 |
also result in non-compositional checking of sub-proofs,
|
|
1049 |
\emph{local goals} are not allowed to be schematic at all.
|
|
1050 |
Nevertheless, schematic goals do have their use in Prolog-style
|
|
1051 |
interactive synthesis of proven results, usually by stepwise
|
|
1052 |
refinement via emulation of traditional Isabelle tactic scripts
|
|
1053 |
(see also \secref{sec:tactic-commands}). In any case, users
|
|
1054 |
should know what they are doing.
|
|
1055 |
\end{warn}
|
|
1056 |
*}
|
|
1057 |
|
|
1058 |
|
|
1059 |
subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
|
|
1060 |
|
|
1061 |
text {*
|
|
1062 |
\begin{matharray}{rcl}
|
|
1063 |
@{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
|
|
1064 |
@{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
|
|
1065 |
@{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
1066 |
@{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
1067 |
@{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
1068 |
@{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
|
1069 |
\end{matharray}
|
|
1070 |
|
|
1071 |
Arbitrary goal refinement via tactics is considered harmful.
|
|
1072 |
Structured proof composition in Isar admits proof methods to be
|
|
1073 |
invoked in two places only.
|
|
1074 |
|
|
1075 |
\begin{enumerate}
|
|
1076 |
|
|
1077 |
\item An \emph{initial} refinement step @{command_ref
|
|
1078 |
"proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
|
|
1079 |
of sub-goals that are to be solved later. Facts are passed to
|
|
1080 |
@{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
|
|
1081 |
"proof(chain)"} mode.
|
|
1082 |
|
|
1083 |
\item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
|
|
1084 |
"m\<^sub>2"} is intended to solve remaining goals. No facts are
|
|
1085 |
passed to @{text "m\<^sub>2"}.
|
|
1086 |
|
|
1087 |
\end{enumerate}
|
|
1088 |
|
|
1089 |
The only other (proper) way to affect pending goals in a proof body
|
|
1090 |
is by @{command_ref "show"}, which involves an explicit statement of
|
|
1091 |
what is to be solved eventually. Thus we avoid the fundamental
|
|
1092 |
problem of unstructured tactic scripts that consist of numerous
|
|
1093 |
consecutive goal transformations, with invisible effects.
|
|
1094 |
|
|
1095 |
\medskip As a general rule of thumb for good proof style, initial
|
|
1096 |
proof methods should either solve the goal completely, or constitute
|
|
1097 |
some well-understood reduction to new sub-goals. Arbitrary
|
|
1098 |
automatic proof tools that are prone leave a large number of badly
|
|
1099 |
structured sub-goals are no help in continuing the proof document in
|
|
1100 |
an intelligible manner.
|
|
1101 |
|
|
1102 |
Unless given explicitly by the user, the default initial method is
|
|
1103 |
``@{method_ref rule}'', which applies a single standard elimination
|
|
1104 |
or introduction rule according to the topmost symbol involved.
|
|
1105 |
There is no separate default terminal method. Any remaining goals
|
|
1106 |
are always solved by assumption in the very last step.
|
|
1107 |
|
|
1108 |
\begin{rail}
|
|
1109 |
'proof' method?
|
|
1110 |
;
|
|
1111 |
'qed' method?
|
|
1112 |
;
|
|
1113 |
'by' method method?
|
|
1114 |
;
|
|
1115 |
('.' | '..' | 'sorry')
|
|
1116 |
;
|
|
1117 |
\end{rail}
|
|
1118 |
|
|
1119 |
\begin{descr}
|
|
1120 |
|
|
1121 |
\item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
|
|
1122 |
proof method @{text "m\<^sub>1"}; facts for forward chaining are
|
|
1123 |
passed if so indicated by @{text "proof(chain)"} mode.
|
|
1124 |
|
|
1125 |
\item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
|
|
1126 |
goals by proof method @{text "m\<^sub>2"} and concludes the
|
|
1127 |
sub-proof by assumption. If the goal had been @{text "show"} (or
|
|
1128 |
@{text "thus"}), some pending sub-goal is solved as well by the rule
|
|
1129 |
resulting from the result \emph{exported} into the enclosing goal
|
|
1130 |
context. Thus @{text "qed"} may fail for two reasons: either @{text
|
|
1131 |
"m\<^sub>2"} fails, or the resulting rule does not fit to any
|
|
1132 |
pending goal\footnote{This includes any additional ``strong''
|
26777
|
1133 |
assumptions as introduced by @{command "assume"}.} of the enclosing
|
26767
|
1134 |
context. Debugging such a situation might involve temporarily
|
|
1135 |
changing @{command "show"} into @{command "have"}, or weakening the
|
|
1136 |
local context by replacing occurrences of @{command "assume"} by
|
|
1137 |
@{command "presume"}.
|
|
1138 |
|
|
1139 |
\item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
|
|
1140 |
\emph{terminal proof}\index{proof!terminal}; it abbreviates
|
|
1141 |
@{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
|
|
1142 |
"m\<^sub>2"}, but with backtracking across both methods. Debugging
|
|
1143 |
an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
|
|
1144 |
command can be done by expanding its definition; in many cases
|
|
1145 |
@{command "proof"}~@{text "m\<^sub>1"} (or even @{text
|
|
1146 |
"apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
|
|
1147 |
problem.
|
|
1148 |
|
|
1149 |
\item [``@{command ".."}''] is a \emph{default
|
|
1150 |
proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
|
|
1151 |
"rule"}.
|
|
1152 |
|
|
1153 |
\item [``@{command "."}''] is a \emph{trivial
|
|
1154 |
proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
|
|
1155 |
"this"}.
|
|
1156 |
|
|
1157 |
\item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
|
|
1158 |
pretending to solve the pending claim without further ado. This
|
|
1159 |
only works in interactive development, or if the @{ML
|
|
1160 |
quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
|
|
1161 |
proofs are not the real thing. Internally, each theorem container
|
|
1162 |
is tainted by an oracle invocation, which is indicated as ``@{text
|
|
1163 |
"[!]"}'' in the printed result.
|
|
1164 |
|
|
1165 |
The most important application of @{command "sorry"} is to support
|
|
1166 |
experimentation and top-down proof development.
|
|
1167 |
|
|
1168 |
\end{descr}
|
|
1169 |
*}
|
|
1170 |
|
|
1171 |
|
|
1172 |
subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
|
|
1173 |
|
|
1174 |
text {*
|
|
1175 |
The following proof methods and attributes refer to basic logical
|
|
1176 |
operations of Isar. Further methods and attributes are provided by
|
|
1177 |
several generic and object-logic specific tools and packages (see
|
26852
|
1178 |
\chref{ch:gen-tools} and \chref{ch:hol}).
|
26767
|
1179 |
|
|
1180 |
\begin{matharray}{rcl}
|
|
1181 |
@{method_def "-"} & : & \isarmeth \\
|
|
1182 |
@{method_def "fact"} & : & \isarmeth \\
|
|
1183 |
@{method_def "assumption"} & : & \isarmeth \\
|
|
1184 |
@{method_def "this"} & : & \isarmeth \\
|
|
1185 |
@{method_def "rule"} & : & \isarmeth \\
|
|
1186 |
@{method_def "iprover"} & : & \isarmeth \\[0.5ex]
|
|
1187 |
@{attribute_def "intro"} & : & \isaratt \\
|
|
1188 |
@{attribute_def "elim"} & : & \isaratt \\
|
|
1189 |
@{attribute_def "dest"} & : & \isaratt \\
|
|
1190 |
@{attribute_def "rule"} & : & \isaratt \\[0.5ex]
|
|
1191 |
@{attribute_def "OF"} & : & \isaratt \\
|
|
1192 |
@{attribute_def "of"} & : & \isaratt \\
|
|
1193 |
@{attribute_def "where"} & : & \isaratt \\
|
|
1194 |
\end{matharray}
|
|
1195 |
|
|
1196 |
\begin{rail}
|
|
1197 |
'fact' thmrefs?
|
|
1198 |
;
|
|
1199 |
'rule' thmrefs?
|
|
1200 |
;
|
|
1201 |
'iprover' ('!' ?) (rulemod *)
|
|
1202 |
;
|
|
1203 |
rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
|
|
1204 |
;
|
|
1205 |
('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
|
|
1206 |
;
|
|
1207 |
'rule' 'del'
|
|
1208 |
;
|
|
1209 |
'OF' thmrefs
|
|
1210 |
;
|
|
1211 |
'of' insts ('concl' ':' insts)?
|
|
1212 |
;
|
|
1213 |
'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
|
|
1214 |
;
|
|
1215 |
\end{rail}
|
|
1216 |
|
|
1217 |
\begin{descr}
|
|
1218 |
|
26777
|
1219 |
\item [``@{method "-"}'' (minus)] does nothing but insert the
|
|
1220 |
forward chaining facts as premises into the goal. Note that command
|
26767
|
1221 |
@{command_ref "proof"} without any method actually performs a single
|
|
1222 |
reduction step using the @{method_ref rule} method; thus a plain
|
|
1223 |
\emph{do-nothing} proof step would be ``@{command "proof"}~@{text
|
|
1224 |
"-"}'' rather than @{command "proof"} alone.
|
|
1225 |
|
|
1226 |
\item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
|
|
1227 |
some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
|
|
1228 |
the current proof context) modulo unification of schematic type and
|
|
1229 |
term variables. The rule structure is not taken into account, i.e.\
|
|
1230 |
meta-level implication is considered atomic. This is the same
|
|
1231 |
principle underlying literal facts (cf.\ \secref{sec:syn-att}):
|
|
1232 |
``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
|
|
1233 |
equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
|
|
1234 |
"`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
|
|
1235 |
@{text "\<turnstile> \<phi>"} in the proof context.
|
|
1236 |
|
|
1237 |
\item [@{method assumption}] solves some goal by a single assumption
|
|
1238 |
step. All given facts are guaranteed to participate in the
|
|
1239 |
refinement; this means there may be only 0 or 1 in the first place.
|
|
1240 |
Recall that @{command "qed"} (\secref{sec:proof-steps}) already
|
|
1241 |
concludes any remaining sub-goals by assumption, so structured
|
|
1242 |
proofs usually need not quote the @{method assumption} method at
|
|
1243 |
all.
|
|
1244 |
|
|
1245 |
\item [@{method this}] applies all of the current facts directly as
|
|
1246 |
rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
|
|
1247 |
"by"}~@{text this}''.
|
|
1248 |
|
|
1249 |
\item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
|
|
1250 |
rule given as argument in backward manner; facts are used to reduce
|
|
1251 |
the rule before applying it to the goal. Thus @{method rule}
|
|
1252 |
without facts is plain introduction, while with facts it becomes
|
|
1253 |
elimination.
|
|
1254 |
|
|
1255 |
When no arguments are given, the @{method rule} method tries to pick
|
|
1256 |
appropriate rules automatically, as declared in the current context
|
|
1257 |
using the @{attribute intro}, @{attribute elim}, @{attribute dest}
|
|
1258 |
attributes (see below). This is the default behavior of @{command
|
|
1259 |
"proof"} and ``@{command ".."}'' (double-dot) steps (see
|
|
1260 |
\secref{sec:proof-steps}).
|
|
1261 |
|
|
1262 |
\item [@{method iprover}] performs intuitionistic proof search,
|
|
1263 |
depending on specifically declared rules from the context, or given
|
|
1264 |
as explicit arguments. Chained facts are inserted into the goal
|
|
1265 |
before commencing proof search; ``@{method iprover}@{text "!"}''
|
|
1266 |
means to include the current @{fact prems} as well.
|
|
1267 |
|
|
1268 |
Rules need to be classified as @{attribute intro}, @{attribute
|
26777
|
1269 |
elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
|
|
1270 |
refers to ``safe'' rules, which may be applied aggressively (without
|
26767
|
1271 |
considering back-tracking later). Rules declared with ``@{text
|
|
1272 |
"?"}'' are ignored in proof search (the single-step @{method rule}
|
|
1273 |
method still observes these). An explicit weight annotation may be
|
|
1274 |
given as well; otherwise the number of rule premises will be taken
|
|
1275 |
into account here.
|
|
1276 |
|
|
1277 |
\item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
|
|
1278 |
declare introduction, elimination, and destruct rules, to be used
|
|
1279 |
with the @{method rule} and @{method iprover} methods. Note that
|
|
1280 |
the latter will ignore rules declared with ``@{text "?"}'', while
|
|
1281 |
``@{text "!"}'' are used most aggressively.
|
|
1282 |
|
|
1283 |
The classical reasoner (see \secref{sec:classical}) introduces its
|
|
1284 |
own variants of these attributes; use qualified names to access the
|
|
1285 |
present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
|
|
1286 |
|
|
1287 |
\item [@{attribute rule}~@{text del}] undeclares introduction,
|
|
1288 |
elimination, or destruct rules.
|
|
1289 |
|
|
1290 |
\item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
|
|
1291 |
theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
|
|
1292 |
(in parallel). This corresponds to the @{ML "op MRS"} operation in
|
|
1293 |
ML, but note the reversed order. Positions may be effectively
|
26777
|
1294 |
skipped by including ``@{text _}'' (underscore) as argument.
|
26767
|
1295 |
|
|
1296 |
\item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
|
|
1297 |
positional instantiation of term variables. The terms @{text
|
|
1298 |
"t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
|
26777
|
1299 |
variables occurring in a theorem from left to right; ``@{text
|
26767
|
1300 |
_}'' (underscore) indicates to skip a position. Arguments following
|
|
1301 |
a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
|
|
1302 |
of the conclusion of a rule.
|
|
1303 |
|
|
1304 |
\item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
|
26777
|
1305 |
x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
|
|
1306 |
type and term variables occurring in a theorem. Schematic variables
|
|
1307 |
have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}).
|
|
1308 |
The question mark may be omitted if the variable name is a plain
|
|
1309 |
identifier without index. As type instantiations are inferred from
|
|
1310 |
term instantiations, explicit type instantiations are seldom
|
|
1311 |
necessary.
|
26767
|
1312 |
|
|
1313 |
\end{descr}
|
|
1314 |
*}
|
|
1315 |
|
|
1316 |
|
|
1317 |
subsection {* Term abbreviations \label{sec:term-abbrev} *}
|
|
1318 |
|
|
1319 |
text {*
|
|
1320 |
\begin{matharray}{rcl}
|
|
1321 |
@{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
1322 |
@{keyword_def "is"} & : & syntax \\
|
|
1323 |
\end{matharray}
|
|
1324 |
|
26777
|
1325 |
Abbreviations may be either bound by explicit @{command
|
|
1326 |
"let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
|
|
1327 |
goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
|
|
1328 |
p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
|
|
1329 |
bind extra-logical term variables, which may be either named
|
|
1330 |
schematic variables of the form @{text ?x}, or nameless dummies
|
|
1331 |
``@{variable _}'' (underscore). Note that in the @{command "let"}
|
|
1332 |
form the patterns occur on the left-hand side, while the @{keyword
|
|
1333 |
"is"} patterns are in postfix position.
|
26767
|
1334 |
|
|
1335 |
Polymorphism of term bindings is handled in Hindley-Milner style,
|
|
1336 |
similar to ML. Type variables referring to local assumptions or
|
|
1337 |
open goal statements are \emph{fixed}, while those of finished
|
|
1338 |
results or bound by @{command "let"} may occur in \emph{arbitrary}
|
|
1339 |
instances later. Even though actual polymorphism should be rarely
|
|
1340 |
used in practice, this mechanism is essential to achieve proper
|
|
1341 |
incremental type-inference, as the user proceeds to build up the
|
|
1342 |
Isar proof text from left to right.
|
|
1343 |
|
|
1344 |
\medskip Term abbreviations are quite different from local
|
|
1345 |
definitions as introduced via @{command "def"} (see
|
|
1346 |
\secref{sec:proof-context}). The latter are visible within the
|
|
1347 |
logic as actual equations, while abbreviations disappear during the
|
|
1348 |
input process just after type checking. Also note that @{command
|
|
1349 |
"def"} does not support polymorphism.
|
|
1350 |
|
|
1351 |
\begin{rail}
|
|
1352 |
'let' ((term + 'and') '=' term + 'and')
|
|
1353 |
;
|
|
1354 |
\end{rail}
|
|
1355 |
|
|
1356 |
The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
|
|
1357 |
or \railnonterm{proppat} (see \secref{sec:term-decls}).
|
|
1358 |
|
|
1359 |
\begin{descr}
|
|
1360 |
|
26777
|
1361 |
\item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
|
|
1362 |
p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
|
|
1363 |
"p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
|
|
1364 |
against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
|
26767
|
1365 |
|
|
1366 |
\item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
|
|
1367 |
"let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
|
|
1368 |
preceding statement. Also note that @{keyword "is"} is not a
|
|
1369 |
separate command, but part of others (such as @{command "assume"},
|
|
1370 |
@{command "have"} etc.).
|
|
1371 |
|
|
1372 |
\end{descr}
|
|
1373 |
|
|
1374 |
Some \emph{implicit} term abbreviations\index{term abbreviations}
|
|
1375 |
for goals and facts are available as well. For any open goal,
|
|
1376 |
@{variable_ref thesis} refers to its object-level statement,
|
|
1377 |
abstracted over any meta-level parameters (if present). Likewise,
|
|
1378 |
@{variable_ref this} is bound for fact statements resulting from
|
|
1379 |
assumptions or finished goals. In case @{variable this} refers to
|
|
1380 |
an object-logic statement that is an application @{text "f t"}, then
|
|
1381 |
@{text t} is bound to the special text variable ``@{variable "\<dots>"}''
|
|
1382 |
(three dots). The canonical application of this convenience are
|
|
1383 |
calculational proofs (see \secref{sec:calculation}).
|
|
1384 |
*}
|
|
1385 |
|
|
1386 |
|
|
1387 |
subsection {* Block structure *}
|
|
1388 |
|
|
1389 |
text {*
|
|
1390 |
\begin{matharray}{rcl}
|
|
1391 |
@{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
1392 |
@{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
1393 |
@{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
1394 |
\end{matharray}
|
|
1395 |
|
|
1396 |
While Isar is inherently block-structured, opening and closing
|
|
1397 |
blocks is mostly handled rather casually, with little explicit
|
|
1398 |
user-intervention. Any local goal statement automatically opens
|
|
1399 |
\emph{two} internal blocks, which are closed again when concluding
|
|
1400 |
the sub-proof (by @{command "qed"} etc.). Sections of different
|
|
1401 |
context within a sub-proof may be switched via @{command "next"},
|
|
1402 |
which is just a single block-close followed by block-open again.
|
|
1403 |
The effect of @{command "next"} is to reset the local proof context;
|
|
1404 |
there is no goal focus involved here!
|
|
1405 |
|
|
1406 |
For slightly more advanced applications, there are explicit block
|
|
1407 |
parentheses as well. These typically achieve a stronger forward
|
|
1408 |
style of reasoning.
|
|
1409 |
|
|
1410 |
\begin{descr}
|
|
1411 |
|
|
1412 |
\item [@{command "next"}] switches to a fresh block within a
|
|
1413 |
sub-proof, resetting the local context to the initial one.
|
|
1414 |
|
|
1415 |
\item [@{command "{"} and @{command "}"}] explicitly open and close
|
|
1416 |
blocks. Any current facts pass through ``@{command "{"}''
|
|
1417 |
unchanged, while ``@{command "}"}'' causes any result to be
|
|
1418 |
\emph{exported} into the enclosing context. Thus fixed variables
|
|
1419 |
are generalized, assumptions discharged, and local definitions
|
|
1420 |
unfolded (cf.\ \secref{sec:proof-context}). There is no difference
|
|
1421 |
of @{command "assume"} and @{command "presume"} in this mode of
|
|
1422 |
forward reasoning --- in contrast to plain backward reasoning with
|
|
1423 |
the result exported at @{command "show"} time.
|
|
1424 |
|
|
1425 |
\end{descr}
|
|
1426 |
*}
|
|
1427 |
|
|
1428 |
|
|
1429 |
subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
|
|
1430 |
|
|
1431 |
text {*
|
|
1432 |
The Isar provides separate commands to accommodate tactic-style
|
|
1433 |
proof scripts within the same system. While being outside the
|
|
1434 |
orthodox Isar proof language, these might come in handy for
|
|
1435 |
interactive exploration and debugging, or even actual tactical proof
|
|
1436 |
within new-style theories (to benefit from document preparation, for
|
|
1437 |
example). See also \secref{sec:tactics} for actual tactics, that
|
|
1438 |
have been encapsulated as proof methods. Proper proof methods may
|
|
1439 |
be used in scripts, too.
|
|
1440 |
|
|
1441 |
\begin{matharray}{rcl}
|
26866
|
1442 |
@{command_def "apply"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(prove)} \\
|
|
1443 |
@{command_def "apply_end"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(state)} \\
|
|
1444 |
@{command_def "done"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(state)} \\
|
|
1445 |
@{command_def "defer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
|
|
1446 |
@{command_def "prefer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
|
|
1447 |
@{command_def "back"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
|
26767
|
1448 |
\end{matharray}
|
|
1449 |
|
|
1450 |
\begin{rail}
|
|
1451 |
( 'apply' | 'apply\_end' ) method
|
|
1452 |
;
|
|
1453 |
'defer' nat?
|
|
1454 |
;
|
|
1455 |
'prefer' nat
|
|
1456 |
;
|
|
1457 |
\end{rail}
|
|
1458 |
|
|
1459 |
\begin{descr}
|
|
1460 |
|
|
1461 |
\item [@{command "apply"}~@{text m}] applies proof method @{text m}
|
|
1462 |
in initial position, but unlike @{command "proof"} it retains
|
|
1463 |
``@{text "proof(prove)"}'' mode. Thus consecutive method
|
|
1464 |
applications may be given just as in tactic scripts.
|
|
1465 |
|
|
1466 |
Facts are passed to @{text m} as indicated by the goal's
|
|
1467 |
forward-chain mode, and are \emph{consumed} afterwards. Thus any
|
|
1468 |
further @{command "apply"} command would always work in a purely
|
|
1469 |
backward manner.
|
|
1470 |
|
|
1471 |
\item [@{command "apply_end"}~@{text "m"}] applies proof method
|
|
1472 |
@{text m} as if in terminal position. Basically, this simulates a
|
|
1473 |
multi-step tactic script for @{command "qed"}, but may be given
|
|
1474 |
anywhere within the proof body.
|
|
1475 |
|
|
1476 |
No facts are passed to @{method m} here. Furthermore, the static
|
|
1477 |
context is that of the enclosing goal (as for actual @{command
|
|
1478 |
"qed"}). Thus the proof method may not refer to any assumptions
|
|
1479 |
introduced in the current body, for example.
|
|
1480 |
|
|
1481 |
\item [@{command "done"}] completes a proof script, provided that
|
|
1482 |
the current goal state is solved completely. Note that actual
|
|
1483 |
structured proof commands (e.g.\ ``@{command "."}'' or @{command
|
|
1484 |
"sorry"}) may be used to conclude proof scripts as well.
|
|
1485 |
|
|
1486 |
\item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
|
|
1487 |
n}] shuffle the list of pending goals: @{command "defer"} puts off
|
|
1488 |
sub-goal @{text n} to the end of the list (@{text "n = 1"} by
|
|
1489 |
default), while @{command "prefer"} brings sub-goal @{text n} to the
|
|
1490 |
front.
|
|
1491 |
|
|
1492 |
\item [@{command "back"}] does back-tracking over the result
|
|
1493 |
sequence of the latest proof command. Basically, any proof command
|
|
1494 |
may return multiple results.
|
|
1495 |
|
|
1496 |
\end{descr}
|
|
1497 |
|
|
1498 |
Any proper Isar proof method may be used with tactic script commands
|
|
1499 |
such as @{command "apply"}. A few additional emulations of actual
|
|
1500 |
tactics are provided as well; these would be never used in actual
|
|
1501 |
structured proofs, of course.
|
|
1502 |
*}
|
|
1503 |
|
|
1504 |
|
|
1505 |
subsection {* Meta-linguistic features *}
|
|
1506 |
|
|
1507 |
text {*
|
|
1508 |
\begin{matharray}{rcl}
|
|
1509 |
@{command_def "oops"} & : & \isartrans{proof}{theory} \\
|
|
1510 |
\end{matharray}
|
|
1511 |
|
|
1512 |
The @{command "oops"} command discontinues the current proof
|
|
1513 |
attempt, while considering the partial proof text as properly
|
|
1514 |
processed. This is conceptually quite different from ``faking''
|
|
1515 |
actual proofs via @{command_ref "sorry"} (see
|
|
1516 |
\secref{sec:proof-steps}): @{command "oops"} does not observe the
|
|
1517 |
proof structure at all, but goes back right to the theory level.
|
|
1518 |
Furthermore, @{command "oops"} does not produce any result theorem
|
|
1519 |
--- there is no intended claim to be able to complete the proof
|
|
1520 |
anyhow.
|
|
1521 |
|
|
1522 |
A typical application of @{command "oops"} is to explain Isar proofs
|
|
1523 |
\emph{within} the system itself, in conjunction with the document
|
|
1524 |
preparation tools of Isabelle described in \cite{isabelle-sys}.
|
|
1525 |
Thus partial or even wrong proof attempts can be discussed in a
|
|
1526 |
logically sound manner. Note that the Isabelle {\LaTeX} macros can
|
|
1527 |
be easily adapted to print something like ``@{text "\<dots>"}'' instead of
|
|
1528 |
the keyword ``@{command "oops"}''.
|
|
1529 |
|
|
1530 |
\medskip The @{command "oops"} command is undo-able, unlike
|
|
1531 |
@{command_ref "kill"} (see \secref{sec:history}). The effect is to
|
|
1532 |
get back to the theory just before the opening of the proof.
|
|
1533 |
*}
|
|
1534 |
|
|
1535 |
|
|
1536 |
section {* Other commands *}
|
|
1537 |
|
|
1538 |
subsection {* Diagnostics *}
|
|
1539 |
|
|
1540 |
text {*
|
|
1541 |
\begin{matharray}{rcl}
|
26866
|
1542 |
@{command_def "pr"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
|
|
1543 |
@{command_def "thm"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1544 |
@{command_def "term"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1545 |
@{command_def "prop"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1546 |
@{command_def "typ"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1547 |
@{command_def "prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1548 |
@{command_def "full_prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
26767
|
1549 |
\end{matharray}
|
|
1550 |
|
|
1551 |
These diagnostic commands assist interactive development. Note that
|
|
1552 |
@{command undo} does not apply here, the theory or proof
|
|
1553 |
configuration is not changed.
|
|
1554 |
|
|
1555 |
\begin{rail}
|
|
1556 |
'pr' modes? nat? (',' nat)?
|
|
1557 |
;
|
|
1558 |
'thm' modes? thmrefs
|
|
1559 |
;
|
|
1560 |
'term' modes? term
|
|
1561 |
;
|
|
1562 |
'prop' modes? prop
|
|
1563 |
;
|
|
1564 |
'typ' modes? type
|
|
1565 |
;
|
|
1566 |
'prf' modes? thmrefs?
|
|
1567 |
;
|
|
1568 |
'full\_prf' modes? thmrefs?
|
|
1569 |
;
|
|
1570 |
|
|
1571 |
modes: '(' (name + ) ')'
|
|
1572 |
;
|
|
1573 |
\end{rail}
|
|
1574 |
|
|
1575 |
\begin{descr}
|
|
1576 |
|
|
1577 |
\item [@{command "pr"}~@{text "goals, prems"}] prints the current
|
|
1578 |
proof state (if present), including the proof context, current facts
|
|
1579 |
and goals. The optional limit arguments affect the number of goals
|
|
1580 |
and premises to be displayed, which is initially 10 for both.
|
|
1581 |
Omitting limit values leaves the current setting unchanged.
|
|
1582 |
|
|
1583 |
\item [@{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] retrieves
|
|
1584 |
theorems from the current theory or proof context. Note that any
|
|
1585 |
attributes included in the theorem specifications are applied to a
|
|
1586 |
temporary context derived from the current theory or proof; the
|
|
1587 |
result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
|
|
1588 |
\<dots>, a\<^sub>n"} do not have any permanent effect.
|
|
1589 |
|
|
1590 |
\item [@{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}]
|
|
1591 |
read, type-check and print terms or propositions according to the
|
|
1592 |
current theory or proof context; the inferred type of @{text t} is
|
|
1593 |
output as well. Note that these commands are also useful in
|
|
1594 |
inspecting the current environment of term abbreviations.
|
|
1595 |
|
|
1596 |
\item [@{command "typ"}~@{text \<tau>}] reads and prints types of the
|
|
1597 |
meta-logic according to the current theory or proof context.
|
|
1598 |
|
|
1599 |
\item [@{command "prf"}] displays the (compact) proof term of the
|
|
1600 |
current proof state (if present), or of the given theorems. Note
|
|
1601 |
that this requires proof terms to be switched on for the current
|
|
1602 |
object logic (see the ``Proof terms'' section of the Isabelle
|
|
1603 |
reference manual for information on how to do this).
|
|
1604 |
|
|
1605 |
\item [@{command "full_prf"}] is like @{command "prf"}, but displays
|
|
1606 |
the full proof term, i.e.\ also displays information omitted in the
|
26777
|
1607 |
compact proof term, which is denoted by ``@{text _}'' placeholders
|
|
1608 |
there.
|
26767
|
1609 |
|
|
1610 |
\end{descr}
|
|
1611 |
|
|
1612 |
All of the diagnostic commands above admit a list of @{text modes}
|
|
1613 |
to be specified, which is appended to the current print mode (see
|
|
1614 |
also \cite{isabelle-ref}). Thus the output behavior may be modified
|
|
1615 |
according particular print mode features. For example, @{command
|
|
1616 |
"pr"}~@{text "(latex xsymbols symbols)"} would print the current
|
|
1617 |
proof state with mathematical symbols and special characters
|
|
1618 |
represented in {\LaTeX} source, according to the Isabelle style
|
|
1619 |
\cite{isabelle-sys}.
|
|
1620 |
|
|
1621 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
|
|
1622 |
systematic way to include formal items into the printed text
|
|
1623 |
document.
|
|
1624 |
*}
|
|
1625 |
|
|
1626 |
|
|
1627 |
subsection {* Inspecting the context *}
|
|
1628 |
|
|
1629 |
text {*
|
|
1630 |
\begin{matharray}{rcl}
|
26866
|
1631 |
@{command_def "print_commands"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
|
|
1632 |
@{command_def "print_theory"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1633 |
@{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1634 |
@{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1635 |
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1636 |
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1637 |
@{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1638 |
@{command_def "thms_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
|
|
1639 |
@{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
|
|
1640 |
@{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
|
26767
|
1641 |
\end{matharray}
|
|
1642 |
|
|
1643 |
\begin{rail}
|
|
1644 |
'print\_theory' ( '!'?)
|
|
1645 |
;
|
|
1646 |
|
|
1647 |
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
|
|
1648 |
;
|
|
1649 |
criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
|
|
1650 |
'simp' ':' term | term)
|
|
1651 |
;
|
|
1652 |
'thm\_deps' thmrefs
|
|
1653 |
;
|
|
1654 |
\end{rail}
|
|
1655 |
|
|
1656 |
These commands print certain parts of the theory and proof context.
|
|
1657 |
Note that there are some further ones available, such as for the set
|
|
1658 |
of rules declared for simplifications.
|
|
1659 |
|
|
1660 |
\begin{descr}
|
|
1661 |
|
|
1662 |
\item [@{command "print_commands"}] prints Isabelle's outer theory
|
|
1663 |
syntax, including keywords and command.
|
|
1664 |
|
|
1665 |
\item [@{command "print_theory"}] prints the main logical content of
|
|
1666 |
the theory context; the ``@{text "!"}'' option indicates extra
|
|
1667 |
verbosity.
|
|
1668 |
|
|
1669 |
\item [@{command "print_syntax"}] prints the inner syntax of types
|
|
1670 |
and terms, depending on the current context. The output can be very
|
|
1671 |
verbose, including grammar tables and syntax translation rules. See
|
|
1672 |
\cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
|
|
1673 |
inner syntax.
|
|
1674 |
|
|
1675 |
\item [@{command "print_methods"}] prints all proof methods
|
|
1676 |
available in the current theory context.
|
|
1677 |
|
|
1678 |
\item [@{command "print_attributes"}] prints all attributes
|
|
1679 |
available in the current theory context.
|
|
1680 |
|
|
1681 |
\item [@{command "print_theorems"}] prints theorems resulting from
|
|
1682 |
the last command.
|
|
1683 |
|
|
1684 |
\item [@{command "find_theorems"}~@{text criteria}] retrieves facts
|
|
1685 |
from the theory or proof context matching all of given search
|
|
1686 |
criteria. The criterion @{text "name: p"} selects all theorems
|
|
1687 |
whose fully qualified name matches pattern @{text p}, which may
|
|
1688 |
contain ``@{text "*"}'' wildcards. The criteria @{text intro},
|
|
1689 |
@{text elim}, and @{text dest} select theorems that match the
|
|
1690 |
current goal as introduction, elimination or destruction rules,
|
|
1691 |
respectively. The criterion @{text "simp: t"} selects all rewrite
|
|
1692 |
rules whose left-hand side matches the given term. The criterion
|
|
1693 |
term @{text t} selects all theorems that contain the pattern @{text
|
|
1694 |
t} -- as usual, patterns may contain occurrences of the dummy
|
26777
|
1695 |
``@{text _}'', schematic variables, and type constraints.
|
26767
|
1696 |
|
|
1697 |
Criteria can be preceded by ``@{text "-"}'' to select theorems that
|
|
1698 |
do \emph{not} match. Note that giving the empty list of criteria
|
|
1699 |
yields \emph{all} currently known facts. An optional limit for the
|
|
1700 |
number of printed facts may be given; the default is 40. By
|
|
1701 |
default, duplicates are removed from the search result. Use
|
|
1702 |
@{keyword "with_dups"} to display duplicates.
|
|
1703 |
|
|
1704 |
\item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
|
|
1705 |
visualizes dependencies of facts, using Isabelle's graph browser
|
|
1706 |
tool (see also \cite{isabelle-sys}).
|
|
1707 |
|
|
1708 |
\item [@{command "print_facts"}] prints all local facts of the
|
|
1709 |
current context, both named and unnamed ones.
|
|
1710 |
|
|
1711 |
\item [@{command "print_binds"}] prints all term abbreviations
|
|
1712 |
present in the context.
|
|
1713 |
|
|
1714 |
\end{descr}
|
|
1715 |
*}
|
|
1716 |
|
|
1717 |
|
|
1718 |
subsection {* History commands \label{sec:history} *}
|
|
1719 |
|
|
1720 |
text {*
|
|
1721 |
\begin{matharray}{rcl}
|
|
1722 |
@{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
|
|
1723 |
@{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
|
|
1724 |
@{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
|
|
1725 |
\end{matharray}
|
|
1726 |
|
|
1727 |
The Isabelle/Isar top-level maintains a two-stage history, for
|
|
1728 |
theory and proof state transformation. Basically, any command can
|
|
1729 |
be undone using @{command "undo"}, excluding mere diagnostic
|
|
1730 |
elements. Its effect may be revoked via @{command "redo"}, unless
|
|
1731 |
the corresponding @{command "undo"} step has crossed the beginning
|
|
1732 |
of a proof or theory. The @{command "kill"} command aborts the
|
|
1733 |
current history node altogether, discontinuing a proof or even the
|
|
1734 |
whole theory. This operation is \emph{not} undo-able.
|
|
1735 |
|
|
1736 |
\begin{warn}
|
|
1737 |
History commands should never be used with user interfaces such as
|
|
1738 |
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
|
|
1739 |
care of stepping forth and back itself. Interfering by manual
|
|
1740 |
@{command "undo"}, @{command "redo"}, or even @{command "kill"}
|
|
1741 |
commands would quickly result in utter confusion.
|
|
1742 |
\end{warn}
|
|
1743 |
*}
|
|
1744 |
|
|
1745 |
|
|
1746 |
subsection {* System operations *}
|
|
1747 |
|
|
1748 |
text {*
|
|
1749 |
\begin{matharray}{rcl}
|
26866
|
1750 |
@{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
|
|
1751 |
@{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
|
|
1752 |
@{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
|
|
1753 |
@{command_def "display_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
|
|
1754 |
@{command_def "print_drafts"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
|
26767
|
1755 |
\end{matharray}
|
|
1756 |
|
|
1757 |
\begin{rail}
|
|
1758 |
('cd' | 'use\_thy' | 'update\_thy') name
|
|
1759 |
;
|
|
1760 |
('display\_drafts' | 'print\_drafts') (name +)
|
|
1761 |
;
|
|
1762 |
\end{rail}
|
|
1763 |
|
|
1764 |
\begin{descr}
|
|
1765 |
|
|
1766 |
\item [@{command "cd"}~@{text path}] changes the current directory
|
|
1767 |
of the Isabelle process.
|
|
1768 |
|
|
1769 |
\item [@{command "pwd"}] prints the current working directory.
|
|
1770 |
|
|
1771 |
\item [@{command "use_thy"}~@{text A}] preload theory @{text A}.
|
|
1772 |
These system commands are scarcely used when working interactively,
|
|
1773 |
since loading of theories is done automatically as required.
|
|
1774 |
|
|
1775 |
\item [@{command "display_drafts"}~@{text paths} and @{command
|
|
1776 |
"print_drafts"}~@{text paths}] perform simple output of a given list
|
|
1777 |
of raw source files. Only those symbols that do not require
|
|
1778 |
additional {\LaTeX} packages are displayed properly, everything else
|
|
1779 |
is left verbatim.
|
|
1780 |
|
|
1781 |
\end{descr}
|
|
1782 |
*}
|
|
1783 |
|
|
1784 |
end
|