wenzelm@7046
|
1 |
|
wenzelm@7335
|
2 |
\chapter{Basic Isar Elements}\label{ch:pure-syntax}
|
wenzelm@7046
|
3 |
|
wenzelm@7315
|
4 |
Subsequently, we introduce the main part of the basic Isar theory and proof
|
wenzelm@7315
|
5 |
commands as provided by Isabelle/Pure. Chapter~\ref{ch:gen-tools} describes
|
wenzelm@7335
|
6 |
further Isar elements as provided by generic tools and packages (such as the
|
wenzelm@7335
|
7 |
Simplifier) that are either part of Pure Isabelle, or pre-loaded by most
|
wenzelm@7335
|
8 |
object logics. See chapter~\ref{ch:hol-tools} for actual object-logic
|
wenzelm@7335
|
9 |
specific elements (for Isabelle/HOL).
|
wenzelm@7167
|
10 |
|
wenzelm@7167
|
11 |
\medskip
|
wenzelm@7167
|
12 |
|
wenzelm@7167
|
13 |
Isar commands may be either \emph{proper} document constructors, or
|
wenzelm@7175
|
14 |
\emph{improper commands} (indicated by $^*$). Some proof methods and
|
wenzelm@7335
|
15 |
attributes introduced later are classified as improper as well. Improper Isar
|
wenzelm@7335
|
16 |
language elements might be helpful when developing proof documents, while
|
wenzelm@7175
|
17 |
their use is strongly discouraged for the final version. Typical examples are
|
wenzelm@7175
|
18 |
diagnostic commands that print terms or theorems according to the current
|
wenzelm@7175
|
19 |
context; other commands even emulate old-style tactical theorem proving, which
|
wenzelm@7175
|
20 |
facilitates porting of legacy proof scripts.
|
wenzelm@7167
|
21 |
|
wenzelm@7134
|
22 |
|
wenzelm@7134
|
23 |
\section{Theory commands}
|
wenzelm@7134
|
24 |
|
wenzelm@7167
|
25 |
\subsection{Defining theories}\label{sec:begin-thy}
|
wenzelm@7134
|
26 |
|
wenzelm@7134
|
27 |
\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
|
wenzelm@7134
|
28 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
29 |
\isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
|
wenzelm@7134
|
30 |
\isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
|
wenzelm@7134
|
31 |
\isarcmd{end} & : & \isartrans{theory}{\cdot} \\
|
wenzelm@7134
|
32 |
\end{matharray}
|
wenzelm@7134
|
33 |
|
wenzelm@7134
|
34 |
Isabelle/Isar ``new-style'' theories are either defined via theory files or
|
wenzelm@7167
|
35 |
interactively. Both actual theory specifications and proofs are handled
|
wenzelm@7335
|
36 |
uniformly --- occasionally definitional mechanisms even require some explicit
|
wenzelm@7335
|
37 |
proof as well. In contrast, ``old-style'' Isabelle theories support batch
|
wenzelm@7335
|
38 |
processing only, with the proof scripts collected in separate ML files.
|
wenzelm@7134
|
39 |
|
wenzelm@7134
|
40 |
The first command of any theory has to be $\THEORY$, starting a new theory
|
wenzelm@7175
|
41 |
based on the merge of existing ones. The theory context may be also changed
|
wenzelm@7175
|
42 |
by $\CONTEXT$ without creating a new theory. In both cases, $\END$ concludes
|
wenzelm@7175
|
43 |
the theory development; it has to be the very last command of any proper
|
wenzelm@7175
|
44 |
theory file.
|
wenzelm@7134
|
45 |
|
wenzelm@7134
|
46 |
\begin{rail}
|
wenzelm@7134
|
47 |
'theory' name '=' (name + '+') filespecs? ':'
|
wenzelm@7134
|
48 |
;
|
wenzelm@7134
|
49 |
'context' name
|
wenzelm@7134
|
50 |
;
|
wenzelm@7134
|
51 |
'end'
|
wenzelm@7134
|
52 |
;;
|
wenzelm@7134
|
53 |
|
wenzelm@7167
|
54 |
filespecs: 'files' ((name | parname) +);
|
wenzelm@7134
|
55 |
\end{rail}
|
wenzelm@7134
|
56 |
|
wenzelm@7167
|
57 |
\begin{descr}
|
wenzelm@7134
|
58 |
\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
|
wenzelm@7175
|
59 |
existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader system ensures
|
wenzelm@7175
|
60 |
that any of the base theories are properly loaded (and fully up-to-date when
|
wenzelm@7175
|
61 |
$\THEORY$ is executed interactively). The optional $\isarkeyword{files}$
|
wenzelm@7175
|
62 |
specification declares additional dependencies on ML files. Unless put in
|
wenzelm@7175
|
63 |
parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see
|
wenzelm@7335
|
64 |
also \S\ref{sec:ML}). The optional ML file \texttt{$A$.ML} that may be
|
wenzelm@7335
|
65 |
associated with any theory should \emph{not} be included in
|
wenzelm@7335
|
66 |
$\isarkeyword{files}$.
|
wenzelm@7134
|
67 |
|
wenzelm@7167
|
68 |
\item [$\CONTEXT~B$] enters an existing theory context $B$, basically in
|
wenzelm@7134
|
69 |
read-only mode, so only a limited set of commands may be performed. Just as
|
wenzelm@7134
|
70 |
for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
|
wenzelm@7175
|
71 |
|
wenzelm@7167
|
72 |
\item [$\END$] concludes the current theory definition or context switch.
|
wenzelm@7175
|
73 |
Note that this command cannot be undone, instead the theory definition
|
wenzelm@7175
|
74 |
itself has to be retracted.
|
wenzelm@7167
|
75 |
\end{descr}
|
wenzelm@7134
|
76 |
|
wenzelm@7134
|
77 |
|
wenzelm@7167
|
78 |
\subsection{Formal comments}\label{sec:formal-cmt-thy}
|
wenzelm@7134
|
79 |
|
wenzelm@7167
|
80 |
\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
|
wenzelm@7167
|
81 |
\indexisarcmd{subsubsection}\indexisarcmd{text}
|
wenzelm@7134
|
82 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
83 |
\isarcmd{title} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
84 |
\isarcmd{chapter} & : & \isartrans{theory}{theory} \\
|
wenzelm@7167
|
85 |
\isarcmd{section} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
86 |
\isarcmd{subsection} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
87 |
\isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
88 |
\isarcmd{text} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
89 |
\end{matharray}
|
wenzelm@7134
|
90 |
|
wenzelm@7167
|
91 |
There are several commands to include \emph{formal comments} in theory
|
wenzelm@7167
|
92 |
specification (a few more are available for proofs, see
|
wenzelm@7167
|
93 |
\S\ref{sec:formal-cmt-prf}). In contrast to source-level comments
|
wenzelm@7134
|
94 |
\verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text
|
wenzelm@7134
|
95 |
given as formal comment is meant to be part of the actual document.
|
wenzelm@7134
|
96 |
Consequently, it would be included in the final printed version.
|
wenzelm@7134
|
97 |
|
wenzelm@7134
|
98 |
Apart from plain prose, formal comments may also refer to logical entities of
|
wenzelm@7175
|
99 |
the theory context (types, terms, theorems etc.). Proper processing of the
|
wenzelm@7175
|
100 |
text would then include some further consistency checks with the items
|
wenzelm@7175
|
101 |
declared in the current theory, e.g.\ type-checking of included
|
wenzelm@7175
|
102 |
terms.\footnote{The current version of Isabelle/Isar does not process formal
|
wenzelm@7134
|
103 |
comments in any such way. This will be available as part of the automatic
|
wenzelm@7175
|
104 |
theory and proof document preparation system (using (PDF){\LaTeX}) that is
|
wenzelm@7134
|
105 |
planned for the near future.}
|
wenzelm@7134
|
106 |
|
wenzelm@7134
|
107 |
\begin{rail}
|
wenzelm@7134
|
108 |
'title' text text? text?
|
wenzelm@7134
|
109 |
;
|
wenzelm@7167
|
110 |
('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') text
|
wenzelm@7134
|
111 |
;
|
wenzelm@7134
|
112 |
\end{rail}
|
wenzelm@7134
|
113 |
|
wenzelm@7167
|
114 |
\begin{descr}
|
wenzelm@7134
|
115 |
\item [$\isarkeyword{title}~title~author~date$] specifies the document title
|
wenzelm@7175
|
116 |
just as in typical {\LaTeX} documents.
|
wenzelm@7335
|
117 |
\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
|
wenzelm@7335
|
118 |
$\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
|
wenzelm@7335
|
119 |
and section headings.
|
wenzelm@7335
|
120 |
\item [$\TEXT$] specifies an actual body of prose text, including references
|
wenzelm@7335
|
121 |
to formal entities.\footnote{The latter feature is not yet exploited.
|
wenzelm@7335
|
122 |
Nevertheless, any text of the form \texttt{\at\ttlbrace\dots\ttrbrace}
|
wenzelm@7335
|
123 |
should be considered as reserved for future use.}
|
wenzelm@7167
|
124 |
\end{descr}
|
wenzelm@7134
|
125 |
|
wenzelm@7134
|
126 |
|
wenzelm@7135
|
127 |
\subsection{Type classes and sorts}\label{sec:classes}
|
wenzelm@7134
|
128 |
|
wenzelm@7134
|
129 |
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
|
wenzelm@7134
|
130 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
131 |
\isarcmd{classes} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
132 |
\isarcmd{classrel} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
133 |
\isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
134 |
\end{matharray}
|
wenzelm@7134
|
135 |
|
wenzelm@7134
|
136 |
\begin{rail}
|
wenzelm@7167
|
137 |
'classes' (classdecl comment? +)
|
wenzelm@7134
|
138 |
;
|
wenzelm@7134
|
139 |
'classrel' nameref '<' nameref comment?
|
wenzelm@7134
|
140 |
;
|
wenzelm@7134
|
141 |
'defaultsort' sort comment?
|
wenzelm@7134
|
142 |
;
|
wenzelm@7134
|
143 |
\end{rail}
|
wenzelm@7134
|
144 |
|
wenzelm@7167
|
145 |
\begin{descr}
|
wenzelm@7335
|
146 |
\item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass
|
wenzelm@7335
|
147 |
of existing classes $\vec c$. Cyclic class structures are ruled out.
|
wenzelm@7134
|
148 |
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
|
wenzelm@7134
|
149 |
existing classes $c@1$ and $c@2$. This is done axiomatically! The
|
wenzelm@7175
|
150 |
$\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way
|
wenzelm@7175
|
151 |
introduce proven class relations.
|
wenzelm@7134
|
152 |
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
|
wenzelm@7175
|
153 |
any type variables input without sort constraints. Usually, the default
|
wenzelm@7134
|
154 |
sort would be only changed when defining new logics.
|
wenzelm@7167
|
155 |
\end{descr}
|
wenzelm@7134
|
156 |
|
wenzelm@7134
|
157 |
|
wenzelm@7315
|
158 |
\subsection{Primitive types and type abbreviations}\label{sec:types-pure}
|
wenzelm@7134
|
159 |
|
wenzelm@7134
|
160 |
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
|
wenzelm@7134
|
161 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
162 |
\isarcmd{types} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
163 |
\isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
164 |
\isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
165 |
\isarcmd{arities} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
166 |
\end{matharray}
|
wenzelm@7134
|
167 |
|
wenzelm@7134
|
168 |
\begin{rail}
|
wenzelm@7134
|
169 |
'types' (typespec '=' type infix? comment? +)
|
wenzelm@7134
|
170 |
;
|
wenzelm@7134
|
171 |
'typedecl' typespec infix? comment?
|
wenzelm@7134
|
172 |
;
|
wenzelm@7134
|
173 |
'nonterminals' (name +) comment?
|
wenzelm@7134
|
174 |
;
|
wenzelm@7134
|
175 |
'arities' (nameref '::' arity comment? +)
|
wenzelm@7134
|
176 |
;
|
wenzelm@7134
|
177 |
\end{rail}
|
wenzelm@7134
|
178 |
|
wenzelm@7167
|
179 |
\begin{descr}
|
wenzelm@7335
|
180 |
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
|
wenzelm@7134
|
181 |
$(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions,
|
wenzelm@7134
|
182 |
as are available in Isabelle/HOL for example, type synonyms are just purely
|
wenzelm@7134
|
183 |
syntactic abbreviations, without any logical significance. Internally, type
|
wenzelm@7134
|
184 |
synonyms are fully expanded, as may be observed when printing terms or
|
wenzelm@7134
|
185 |
theorems.
|
wenzelm@7134
|
186 |
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
|
wenzelm@7134
|
187 |
$t$, intended as an actual logical type. Note that some logics such as
|
wenzelm@7134
|
188 |
Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.
|
wenzelm@7175
|
189 |
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
|
wenzelm@7175
|
190 |
$\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
|
wenzelm@7175
|
191 |
Isabelle's inner syntax of terms or types.
|
wenzelm@7335
|
192 |
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
|
wenzelm@7335
|
193 |
signature of types by new type constructor arities. This is done
|
wenzelm@7335
|
194 |
axiomatically! The $\isarkeyword{instance}$ command (see
|
wenzelm@7175
|
195 |
\S\ref{sec:axclass}) provides a way introduce proven type arities.
|
wenzelm@7167
|
196 |
\end{descr}
|
wenzelm@7134
|
197 |
|
wenzelm@7134
|
198 |
|
wenzelm@7134
|
199 |
\subsection{Constants and simple definitions}
|
wenzelm@7134
|
200 |
|
wenzelm@7175
|
201 |
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
|
wenzelm@7134
|
202 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
203 |
\isarcmd{consts} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
204 |
\isarcmd{defs} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
205 |
\isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
206 |
\end{matharray}
|
wenzelm@7134
|
207 |
|
wenzelm@7134
|
208 |
\begin{rail}
|
wenzelm@7134
|
209 |
'consts' (constdecl +)
|
wenzelm@7134
|
210 |
;
|
wenzelm@7134
|
211 |
'defs' (thmdecl? prop comment? +)
|
wenzelm@7134
|
212 |
;
|
wenzelm@7134
|
213 |
'constdefs' (constdecl prop comment? +)
|
wenzelm@7134
|
214 |
;
|
wenzelm@7134
|
215 |
|
wenzelm@7134
|
216 |
constdecl: name '::' type mixfix? comment?
|
wenzelm@7134
|
217 |
;
|
wenzelm@7134
|
218 |
\end{rail}
|
wenzelm@7134
|
219 |
|
wenzelm@7167
|
220 |
\begin{descr}
|
wenzelm@7335
|
221 |
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
|
wenzelm@7335
|
222 |
scheme $\sigma$. The optional mixfix annotations may attach concrete syntax
|
wenzelm@7335
|
223 |
constants.
|
wenzelm@7335
|
224 |
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
|
wenzelm@7335
|
225 |
existing constant. See \cite[\S6]{isabelle-ref} for more details on the
|
wenzelm@7335
|
226 |
form of equations admitted as constant definitions.
|
wenzelm@7335
|
227 |
\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
|
wenzelm@7335
|
228 |
definitions of constants, using canonical name $c_def$ for the definitional
|
wenzelm@7335
|
229 |
axiom.
|
wenzelm@7167
|
230 |
\end{descr}
|
wenzelm@7134
|
231 |
|
wenzelm@7134
|
232 |
|
wenzelm@7167
|
233 |
\subsection{Syntax and translations}
|
wenzelm@7134
|
234 |
|
wenzelm@7134
|
235 |
\indexisarcmd{syntax}\indexisarcmd{translations}
|
wenzelm@7134
|
236 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
237 |
\isarcmd{syntax} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
238 |
\isarcmd{translations} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
239 |
\end{matharray}
|
wenzelm@7134
|
240 |
|
wenzelm@7134
|
241 |
\begin{rail}
|
wenzelm@7134
|
242 |
'syntax' ('(' name 'output'? ')')? (constdecl +)
|
wenzelm@7134
|
243 |
;
|
wenzelm@7134
|
244 |
'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
|
wenzelm@7134
|
245 |
;
|
wenzelm@7134
|
246 |
transpat: ('(' nameref ')')? string
|
wenzelm@7134
|
247 |
;
|
wenzelm@7134
|
248 |
\end{rail}
|
wenzelm@7134
|
249 |
|
wenzelm@7167
|
250 |
\begin{descr}
|
wenzelm@7175
|
251 |
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
|
wenzelm@7175
|
252 |
except that the actual logical signature extension is omitted. Thus the
|
wenzelm@7175
|
253 |
context free grammar of Isabelle's inner syntax may be augmented in
|
wenzelm@7335
|
254 |
arbitrary ways, independently of the logic. The $mode$ argument refers to
|
wenzelm@7335
|
255 |
the print mode that the grammar rules belong; unless there is the
|
wenzelm@7335
|
256 |
\texttt{output} flag given, all productions are added both to the input and
|
wenzelm@7335
|
257 |
output grammar.
|
wenzelm@7175
|
258 |
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
|
wenzelm@7175
|
259 |
rules (also known as \emph{macros}): parse/print rules (\texttt{==}), parse
|
wenzelm@7335
|
260 |
rules (\texttt{=>}), or print rules (\texttt{<=}). Translation patterns may
|
wenzelm@7335
|
261 |
be prefixed by the syntactic category to be used for parsing; the default is
|
wenzelm@7134
|
262 |
\texttt{logic}.
|
wenzelm@7167
|
263 |
\end{descr}
|
wenzelm@7134
|
264 |
|
wenzelm@7134
|
265 |
|
wenzelm@7134
|
266 |
\subsection{Axioms and theorems}
|
wenzelm@7134
|
267 |
|
wenzelm@7134
|
268 |
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
|
wenzelm@7134
|
269 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
270 |
\isarcmd{axioms} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
271 |
\isarcmd{theorems} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
272 |
\isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
273 |
\end{matharray}
|
wenzelm@7134
|
274 |
|
wenzelm@7134
|
275 |
\begin{rail}
|
wenzelm@7135
|
276 |
'axioms' (axmdecl prop comment? +)
|
wenzelm@7134
|
277 |
;
|
wenzelm@7134
|
278 |
('theorems' | 'lemmas') thmdef? thmrefs
|
wenzelm@7134
|
279 |
;
|
wenzelm@7134
|
280 |
\end{rail}
|
wenzelm@7134
|
281 |
|
wenzelm@7167
|
282 |
\begin{descr}
|
wenzelm@7335
|
283 |
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
|
wenzelm@7335
|
284 |
logical axioms. In fact, axioms are ``axiomatic theorems'', and may be
|
wenzelm@7335
|
285 |
referred later just as any other theorem.
|
wenzelm@7134
|
286 |
|
wenzelm@7134
|
287 |
Axioms are usually only introduced when declaring new logical systems.
|
wenzelm@7175
|
288 |
Everyday work is typically done the hard way, with proper definitions and
|
wenzelm@7134
|
289 |
actual theorems.
|
wenzelm@7335
|
290 |
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
|
wenzelm@7335
|
291 |
Typical applications would also involve attributes, to augment the default
|
wenzelm@7335
|
292 |
Simplifier context, for example.
|
wenzelm@7134
|
293 |
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
|
wenzelm@7134
|
294 |
tags the results as ``lemma''.
|
wenzelm@7167
|
295 |
\end{descr}
|
wenzelm@7134
|
296 |
|
wenzelm@7134
|
297 |
|
wenzelm@7167
|
298 |
\subsection{Name spaces}
|
wenzelm@7134
|
299 |
|
wenzelm@7167
|
300 |
\indexisarcmd{global}\indexisarcmd{local}
|
wenzelm@7134
|
301 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
302 |
\isarcmd{global} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
303 |
\isarcmd{local} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
304 |
\end{matharray}
|
wenzelm@7134
|
305 |
|
wenzelm@7335
|
306 |
Isabelle organizes any kind of names (of types, constants, theorems etc.) by
|
wenzelm@7175
|
307 |
hierarchically structured name spaces. Normally the user never has to control
|
wenzelm@7335
|
308 |
the behavior of name space entry by hand, yet the following commands provide
|
wenzelm@7175
|
309 |
some way to do so.
|
wenzelm@7175
|
310 |
|
wenzelm@7167
|
311 |
\begin{descr}
|
wenzelm@7167
|
312 |
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
|
wenzelm@7167
|
313 |
name declaration mode. Initially, theories start in $\isarkeyword{local}$
|
wenzelm@7167
|
314 |
mode, causing all names to be automatically qualified by the theory name.
|
wenzelm@7167
|
315 |
Changing this to $\isarkeyword{global}$ causes all names to be declared as
|
wenzelm@7175
|
316 |
base names only, until $\isarkeyword{local}$ is declared again.
|
wenzelm@7167
|
317 |
\end{descr}
|
wenzelm@7134
|
318 |
|
wenzelm@7134
|
319 |
|
wenzelm@7167
|
320 |
\subsection{Incorporating ML code}\label{sec:ML}
|
wenzelm@7134
|
321 |
|
wenzelm@7134
|
322 |
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}
|
wenzelm@7134
|
323 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
324 |
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
|
wenzelm@7134
|
325 |
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
|
wenzelm@7175
|
326 |
\isarcmd{setup} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
327 |
\end{matharray}
|
wenzelm@7134
|
328 |
|
wenzelm@7134
|
329 |
\begin{rail}
|
wenzelm@7134
|
330 |
'use' name
|
wenzelm@7134
|
331 |
;
|
wenzelm@7134
|
332 |
'ML' text
|
wenzelm@7134
|
333 |
;
|
wenzelm@7134
|
334 |
'setup' text
|
wenzelm@7134
|
335 |
;
|
wenzelm@7134
|
336 |
\end{rail}
|
wenzelm@7134
|
337 |
|
wenzelm@7167
|
338 |
\begin{descr}
|
wenzelm@7175
|
339 |
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
|
wenzelm@7175
|
340 |
The current theory context (if present) is passed down to the ML session.
|
wenzelm@7175
|
341 |
Furthermore, the file name is checked with the $\isarkeyword{files}$
|
wenzelm@7175
|
342 |
dependency declaration given in the theory header (see also
|
wenzelm@7175
|
343 |
\S\ref{sec:begin-thy}).
|
wenzelm@7175
|
344 |
\item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.
|
wenzelm@7175
|
345 |
The theory context is passed just as for $\isarkeyword{use}$.
|
wenzelm@7335
|
346 |
%FIXME picked up again!?
|
wenzelm@7167
|
347 |
\item [$\isarkeyword{setup}~text$] changes the current theory context by
|
wenzelm@7175
|
348 |
applying setup functions $text$, which has to be an ML expression of type
|
wenzelm@7175
|
349 |
$(theory \to theory)~list$. The $\isarkeyword{setup}$ command is the usual
|
wenzelm@7335
|
350 |
way to initialize object-logic specific tools and packages written in ML.
|
wenzelm@7167
|
351 |
\end{descr}
|
wenzelm@7134
|
352 |
|
wenzelm@7134
|
353 |
|
wenzelm@7167
|
354 |
\subsection{Syntax translation functions}
|
wenzelm@7134
|
355 |
|
wenzelm@7167
|
356 |
\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
|
wenzelm@7167
|
357 |
\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
|
wenzelm@7167
|
358 |
\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
|
wenzelm@7134
|
359 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
360 |
\isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
361 |
\isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
362 |
\isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
363 |
\isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
364 |
\isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
365 |
\isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
366 |
\end{matharray}
|
wenzelm@7134
|
367 |
|
wenzelm@7134
|
368 |
Syntax translation functions written in ML admit almost arbitrary
|
wenzelm@7134
|
369 |
manipulations of Isabelle's inner syntax. Any of the above commands have a
|
wenzelm@7134
|
370 |
single \railqtoken{text} argument that refers to an ML expression of
|
wenzelm@7134
|
371 |
appropriate type. See \cite[\S8]{isabelle-ref} for more information on syntax
|
wenzelm@7134
|
372 |
transformations.
|
wenzelm@7134
|
373 |
|
wenzelm@7134
|
374 |
|
wenzelm@7134
|
375 |
\subsection{Oracles}
|
wenzelm@7134
|
376 |
|
wenzelm@7134
|
377 |
\indexisarcmd{oracle}
|
wenzelm@7134
|
378 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
379 |
\isarcmd{oracle} & : & \isartrans{theory}{theory} \\
|
wenzelm@7134
|
380 |
\end{matharray}
|
wenzelm@7134
|
381 |
|
wenzelm@7175
|
382 |
Oracles provide an interface to external reasoning systems, without giving up
|
wenzelm@7175
|
383 |
control completely --- each theorem carries a derivation object recording any
|
wenzelm@7175
|
384 |
oracle invocation. See \cite[\S6]{isabelle-ref} for more information.
|
wenzelm@7175
|
385 |
|
wenzelm@7134
|
386 |
\begin{rail}
|
wenzelm@7134
|
387 |
'oracle' name '=' text comment?
|
wenzelm@7134
|
388 |
;
|
wenzelm@7134
|
389 |
\end{rail}
|
wenzelm@7134
|
390 |
|
wenzelm@7167
|
391 |
\begin{descr}
|
wenzelm@7175
|
392 |
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
|
wenzelm@7315
|
393 |
function $text$, which has to be of type $Sign\mathord.sg \times
|
wenzelm@7335
|
394 |
Object\mathord.T \to term$.
|
wenzelm@7167
|
395 |
\end{descr}
|
wenzelm@7134
|
396 |
|
wenzelm@7134
|
397 |
|
wenzelm@7134
|
398 |
\section{Proof commands}
|
wenzelm@7134
|
399 |
|
wenzelm@7315
|
400 |
Proof commands provide transitions of Isar/VM machine configurations, which
|
wenzelm@7315
|
401 |
are block-structured, consisting of a stack of nodes with three main
|
wenzelm@7335
|
402 |
components: logical proof context, current facts, and open goals. Isar/VM
|
wenzelm@7335
|
403 |
transitions are \emph{typed} according to the following three three different
|
wenzelm@7335
|
404 |
modes of operation:
|
wenzelm@7167
|
405 |
\begin{descr}
|
wenzelm@7167
|
406 |
\item [$proof(prove)$] means that a new goal has just been stated that is now
|
wenzelm@7167
|
407 |
to be \emph{proven}; the next command may refine it by some proof method
|
wenzelm@7175
|
408 |
($\approx$ tactic), and enter a sub-proof to establish the final result.
|
wenzelm@7167
|
409 |
\item [$proof(state)$] is like an internal theory mode: the context may be
|
wenzelm@7175
|
410 |
augmented by \emph{stating} additional assumptions, intermediate result etc.
|
wenzelm@7175
|
411 |
\item [$proof(chain)$] is an intermediate mode between $proof(state)$ and
|
wenzelm@7315
|
412 |
$proof(prove)$: existing facts have been just picked up in order to use them
|
wenzelm@7335
|
413 |
when refining the goal claimed next.
|
wenzelm@7167
|
414 |
\end{descr}
|
wenzelm@7134
|
415 |
|
wenzelm@7167
|
416 |
|
wenzelm@7167
|
417 |
\subsection{Formal comments}\label{sec:formal-cmt-prf}
|
wenzelm@7167
|
418 |
|
wenzelm@7167
|
419 |
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}
|
wenzelm@7134
|
420 |
\begin{matharray}{rcl}
|
wenzelm@7167
|
421 |
\isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7167
|
422 |
\isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7167
|
423 |
\isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7167
|
424 |
\isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
425 |
\end{matharray}
|
wenzelm@7134
|
426 |
|
wenzelm@7175
|
427 |
These formal comments in proof mode closely correspond to the ones of theory
|
wenzelm@7175
|
428 |
mode (see \S\ref{sec:formal-cmt-thy}).
|
wenzelm@7175
|
429 |
|
wenzelm@7134
|
430 |
\begin{rail}
|
wenzelm@7167
|
431 |
('sect' | 'subsect' | 'subsubsect' | 'txt') text
|
wenzelm@7134
|
432 |
;
|
wenzelm@7134
|
433 |
\end{rail}
|
wenzelm@7134
|
434 |
|
wenzelm@7134
|
435 |
|
wenzelm@7315
|
436 |
\subsection{Proof context}\label{sec:proof-context}
|
wenzelm@7134
|
437 |
|
wenzelm@7315
|
438 |
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
|
wenzelm@7134
|
439 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
440 |
\isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
441 |
\isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
442 |
\isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
443 |
\isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
444 |
\end{matharray}
|
wenzelm@7134
|
445 |
|
wenzelm@7315
|
446 |
The logical proof context consists of fixed variables and assumptions. The
|
wenzelm@7315
|
447 |
former closely correspond to Skolem constants, or meta-level universal
|
wenzelm@7315
|
448 |
quantification as provided by the Isabelle/Pure logical framework.
|
wenzelm@7315
|
449 |
Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
|
wenzelm@7319
|
450 |
a local object that may be used in the subsequent proof as any other variable
|
wenzelm@7315
|
451 |
or constant. Furthermore, any result $\phi[x]$ exported from the current
|
wenzelm@7315
|
452 |
context will be universally closed wrt.\ $x$ at the outermost level (this is
|
wenzelm@7315
|
453 |
expressed using Isabelle's meta-variables).
|
wenzelm@7315
|
454 |
|
wenzelm@7315
|
455 |
Similarly, introducing some assumption $\chi$ has two effects. On the one
|
wenzelm@7315
|
456 |
hand, a local theorem is created that may be used as a fact in subsequent
|
wenzelm@7315
|
457 |
proof steps. On the other hand, any result $\phi$ exported from the context
|
wenzelm@7315
|
458 |
becomes conditional wrt.\ the assumption. Thus, solving an enclosing goal
|
wenzelm@7335
|
459 |
using such a result would basically introduce a new subgoal stemming from the
|
wenzelm@7315
|
460 |
assumption. How this situation is handled depends on the actual version of
|
wenzelm@7315
|
461 |
assumption command used: while $\ASSUMENAME$ solves the subgoal by unifying
|
wenzelm@7315
|
462 |
with some premise of the goal, $\PRESUMENAME$ leaves the subgoal unchanged to
|
wenzelm@7315
|
463 |
be proved later by the user.
|
wenzelm@7315
|
464 |
|
wenzelm@7319
|
465 |
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
|
wenzelm@7319
|
466 |
combining $\FIX x$ with another kind of assumption that causes any
|
wenzelm@7315
|
467 |
hypothetical equation $x = t$ to be eliminated by reflexivity. Thus,
|
wenzelm@7315
|
468 |
exporting some result $\phi[x]$ simply yields $\phi[t]$.
|
wenzelm@7175
|
469 |
|
wenzelm@7134
|
470 |
\begin{rail}
|
wenzelm@7134
|
471 |
'fix' (var +) comment?
|
wenzelm@7134
|
472 |
;
|
wenzelm@7315
|
473 |
('assume' | 'presume') (assm comment? + 'and')
|
wenzelm@7134
|
474 |
;
|
wenzelm@7175
|
475 |
'def' thmdecl? \\ var '==' term termpat? comment?
|
wenzelm@7134
|
476 |
;
|
wenzelm@7134
|
477 |
|
wenzelm@7134
|
478 |
var: name ('::' type)?
|
wenzelm@7134
|
479 |
;
|
wenzelm@7315
|
480 |
assm: thmdecl? (prop proppat? +)
|
wenzelm@7315
|
481 |
;
|
wenzelm@7134
|
482 |
\end{rail}
|
wenzelm@7134
|
483 |
|
wenzelm@7167
|
484 |
\begin{descr}
|
wenzelm@7315
|
485 |
\item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
|
wenzelm@7315
|
486 |
\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
|
wenzelm@7335
|
487 |
$\Phi$ by assumption. Subsequent results applied to an enclosing goal
|
wenzelm@7335
|
488 |
(e.g.\ via $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be
|
wenzelm@7335
|
489 |
able to unify with existing premises in the goal, while $\PRESUMENAME$
|
wenzelm@7335
|
490 |
leaves $\Phi$ as new subgoals.
|
wenzelm@7335
|
491 |
|
wenzelm@7335
|
492 |
Several lists of assumptions may be given (separated by
|
wenzelm@7335
|
493 |
$\isarkeyword{and}$); the resulting list of facts consists of all of these
|
wenzelm@7335
|
494 |
concatenated.
|
wenzelm@7315
|
495 |
\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
|
wenzelm@7315
|
496 |
In results exported from the context, $x$ is replaced by $t$. Basically,
|
wenzelm@7335
|
497 |
$\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
|
wenzelm@7335
|
498 |
resulting hypothetical equation solved by reflexivity.
|
wenzelm@7167
|
499 |
\end{descr}
|
wenzelm@7167
|
500 |
|
wenzelm@7335
|
501 |
The special theorem name $prems$\indexisarreg{prems} refers to all current
|
wenzelm@7335
|
502 |
assumptions.
|
wenzelm@7315
|
503 |
|
wenzelm@7167
|
504 |
|
wenzelm@7167
|
505 |
\subsection{Facts and forward chaining}
|
wenzelm@7167
|
506 |
|
wenzelm@7167
|
507 |
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
|
wenzelm@7167
|
508 |
\begin{matharray}{rcl}
|
wenzelm@7167
|
509 |
\isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7167
|
510 |
\isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
|
wenzelm@7167
|
511 |
\isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
|
wenzelm@7167
|
512 |
\isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
|
wenzelm@7167
|
513 |
\end{matharray}
|
wenzelm@7167
|
514 |
|
wenzelm@7319
|
515 |
New facts are established either by assumption or proof of local statements.
|
wenzelm@7335
|
516 |
Any fact will usually be involved in further proofs, either as explicit
|
wenzelm@7335
|
517 |
arguments of proof methods or when forward chaining towards the next goal via
|
wenzelm@7335
|
518 |
$\THEN$ (and variants). Note that the special theorem name
|
wenzelm@7335
|
519 |
$facts$.\indexisarreg{facts} refers to the most recently established facts.
|
wenzelm@7167
|
520 |
\begin{rail}
|
wenzelm@7167
|
521 |
'note' thmdef? thmrefs comment?
|
wenzelm@7167
|
522 |
;
|
wenzelm@7167
|
523 |
'then' comment?
|
wenzelm@7167
|
524 |
;
|
wenzelm@7167
|
525 |
('from' | 'with') thmrefs comment?
|
wenzelm@7167
|
526 |
;
|
wenzelm@7167
|
527 |
\end{rail}
|
wenzelm@7167
|
528 |
|
wenzelm@7167
|
529 |
\begin{descr}
|
wenzelm@7175
|
530 |
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
|
wenzelm@7175
|
531 |
as $a$. Note that attributes may be involved as well, both on the left and
|
wenzelm@7175
|
532 |
right hand sides.
|
wenzelm@7167
|
533 |
\item [$\THEN$] indicates forward chaining by the current facts in order to
|
wenzelm@7335
|
534 |
establish the goal claimed next. The initial proof method invoked to refine
|
wenzelm@7335
|
535 |
that will be offered these facts to do ``anything appropriate'' (see also
|
wenzelm@7335
|
536 |
\S\ref{sec:proof-steps}). For example, method $rule$ (see
|
wenzelm@7167
|
537 |
\S\ref{sec:pure-meth}) would do an elimination rather than an introduction.
|
wenzelm@7335
|
538 |
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
|
wenzelm@7335
|
539 |
equivalent to $\FROM{facts}$.
|
wenzelm@7175
|
540 |
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
|
wenzelm@7175
|
541 |
chaining is from earlier facts together with the current ones.
|
wenzelm@7167
|
542 |
\end{descr}
|
wenzelm@7167
|
543 |
|
wenzelm@7167
|
544 |
|
wenzelm@7167
|
545 |
\subsection{Goal statements}
|
wenzelm@7167
|
546 |
|
wenzelm@7167
|
547 |
\indexisarcmd{theorem}\indexisarcmd{lemma}
|
wenzelm@7167
|
548 |
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
|
wenzelm@7167
|
549 |
\begin{matharray}{rcl}
|
wenzelm@7167
|
550 |
\isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
|
wenzelm@7167
|
551 |
\isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
|
wenzelm@7167
|
552 |
\isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
|
wenzelm@7167
|
553 |
\isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
|
wenzelm@7167
|
554 |
\isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
|
wenzelm@7167
|
555 |
\isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
|
wenzelm@7167
|
556 |
\end{matharray}
|
wenzelm@7167
|
557 |
|
wenzelm@7175
|
558 |
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
|
wenzelm@7175
|
559 |
and $\LEMMANAME$. New local goals may be claimed within proof mode: four
|
wenzelm@7175
|
560 |
variants are available, indicating whether the result is meant to solve some
|
wenzelm@7175
|
561 |
pending goal and whether forward chaining is employed.
|
wenzelm@7175
|
562 |
|
wenzelm@7167
|
563 |
\begin{rail}
|
wenzelm@7167
|
564 |
('theorem' | 'lemma') goal
|
wenzelm@7167
|
565 |
;
|
wenzelm@7167
|
566 |
('have' | 'show' | 'hence' | 'thus') goal
|
wenzelm@7167
|
567 |
;
|
wenzelm@7167
|
568 |
|
wenzelm@7167
|
569 |
goal: thmdecl? proppat comment?
|
wenzelm@7167
|
570 |
;
|
wenzelm@7167
|
571 |
\end{rail}
|
wenzelm@7167
|
572 |
|
wenzelm@7167
|
573 |
\begin{descr}
|
wenzelm@7335
|
574 |
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
|
wenzelm@7175
|
575 |
eventually resulting in some theorem $\turn \phi$, which will be stored in
|
wenzelm@7175
|
576 |
the theory.
|
wenzelm@7167
|
577 |
\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
|
wenzelm@7167
|
578 |
``lemma''.
|
wenzelm@7335
|
579 |
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
|
wenzelm@7167
|
580 |
theorem with the current assumption context as hypotheses.
|
wenzelm@7335
|
581 |
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
|
wenzelm@7175
|
582 |
pending goal with the result \emph{exported} into the corresponding context.
|
wenzelm@7335
|
583 |
\item [$\HENCE{a}{\phi}$] abbreviates $\THEN~\HAVE{a}{\phi}$, i.e.\ claims a
|
wenzelm@7335
|
584 |
local goal to be proven by forward chaining the current facts.
|
wenzelm@7335
|
585 |
\item [$\THUS{a}{\phi}$] abbreviates $\THEN~\SHOW{a}{\phi}$.
|
wenzelm@7167
|
586 |
\end{descr}
|
wenzelm@7167
|
587 |
|
wenzelm@7167
|
588 |
|
wenzelm@7167
|
589 |
\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
|
wenzelm@7167
|
590 |
|
wenzelm@7167
|
591 |
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
|
wenzelm@7167
|
592 |
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
|
wenzelm@7167
|
593 |
\begin{matharray}{rcl}
|
wenzelm@7167
|
594 |
\isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
|
wenzelm@7167
|
595 |
\isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
|
wenzelm@7167
|
596 |
\isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
wenzelm@7175
|
597 |
\isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
wenzelm@7167
|
598 |
\isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
wenzelm@7167
|
599 |
\isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
|
wenzelm@7167
|
600 |
\end{matharray}
|
wenzelm@7167
|
601 |
|
wenzelm@7335
|
602 |
Arbitrary goal refinement via tactics is considered harmful. Consequently the
|
wenzelm@7335
|
603 |
Isar framework admits proof methods to be invoked in two places only.
|
wenzelm@7175
|
604 |
\begin{enumerate}
|
wenzelm@7175
|
605 |
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
|
wenzelm@7335
|
606 |
goal to a number of sub-goals that are to be solved later. Facts are passed
|
wenzelm@7335
|
607 |
to $m@1$ for forward chaining if so indicated by $proof(chain)$ mode.
|
wenzelm@7175
|
608 |
|
wenzelm@7335
|
609 |
\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals
|
wenzelm@7335
|
610 |
completely. No facts are passed to $m@2$.
|
wenzelm@7175
|
611 |
\end{enumerate}
|
wenzelm@7175
|
612 |
|
wenzelm@7335
|
613 |
The only other proper way to affect pending goals is by $\SHOWNAME$ (or
|
wenzelm@7335
|
614 |
$\THUSNAME$), which involves an explicit statement of what is to be solved.
|
wenzelm@7175
|
615 |
|
wenzelm@7175
|
616 |
\medskip
|
wenzelm@7175
|
617 |
|
wenzelm@7175
|
618 |
Also note that initial proof methods should either solve the goal completely,
|
wenzelm@7175
|
619 |
or constitute some well-understood deterministic reduction to new sub-goals.
|
wenzelm@7175
|
620 |
Arbitrary automatic proof tools that are prone leave a large number of badly
|
wenzelm@7175
|
621 |
structured sub-goals are no help in continuing the proof document in any
|
wenzelm@7175
|
622 |
intelligible way. A much better technique would be to $\SHOWNAME$ some
|
wenzelm@7175
|
623 |
non-trivial reduction as an explicit rule, which is solved completely by some
|
wenzelm@7175
|
624 |
automated method, and then applied to some pending goal.
|
wenzelm@7175
|
625 |
|
wenzelm@7175
|
626 |
\medskip
|
wenzelm@7175
|
627 |
|
wenzelm@7175
|
628 |
Unless given explicitly by the user, the default initial method is
|
wenzelm@7175
|
629 |
``$default$'', which is usually set up to apply a single standard elimination
|
wenzelm@7175
|
630 |
or introduction rule according to the topmost symbol involved. The default
|
wenzelm@7175
|
631 |
terminal method is ``$finish$''; it solves all goals by assumption.
|
wenzelm@7175
|
632 |
|
wenzelm@7167
|
633 |
\begin{rail}
|
wenzelm@7167
|
634 |
'proof' interest? meth? comment?
|
wenzelm@7167
|
635 |
;
|
wenzelm@7167
|
636 |
'qed' meth? comment?
|
wenzelm@7167
|
637 |
;
|
wenzelm@7167
|
638 |
'by' meth meth? comment?
|
wenzelm@7167
|
639 |
;
|
wenzelm@7167
|
640 |
('.' | '..' | 'sorry') comment?
|
wenzelm@7167
|
641 |
;
|
wenzelm@7167
|
642 |
|
wenzelm@7167
|
643 |
meth: method interest?
|
wenzelm@7167
|
644 |
;
|
wenzelm@7167
|
645 |
\end{rail}
|
wenzelm@7167
|
646 |
|
wenzelm@7167
|
647 |
\begin{descr}
|
wenzelm@7335
|
648 |
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
|
wenzelm@7335
|
649 |
forward chaining are passed if so indicated by $proof(chain)$ mode.
|
wenzelm@7335
|
650 |
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
|
wenzelm@7335
|
651 |
concludes the sub-proof. If the goal had been $\SHOWNAME$ (or $\THUSNAME$),
|
wenzelm@7335
|
652 |
some pending sub-goal is solved as well by the rule resulting from the
|
wenzelm@7335
|
653 |
result exported to the enclosing goal context. Thus $\QEDNAME$ may fail for
|
wenzelm@7335
|
654 |
two reasons: either $m@2$ fails to solve all remaining goals completely, or
|
wenzelm@7335
|
655 |
the resulting rule does not resolve with any enclosing goal. Debugging such
|
wenzelm@7335
|
656 |
a situation might involve temporarily changing $\SHOWNAME$ into $\HAVENAME$,
|
wenzelm@7335
|
657 |
or softening the local context by replacing $\ASSUMENAME$ by $\PRESUMENAME$.
|
wenzelm@7175
|
658 |
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates
|
wenzelm@7175
|
659 |
$\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods.
|
wenzelm@7175
|
660 |
Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply
|
wenzelm@7175
|
661 |
expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually
|
wenzelm@7175
|
662 |
sufficient to see what is going wrong.
|
wenzelm@7321
|
663 |
\item [``$\DDOT$''] is a \emph{default proof}; it abbreviates $\BY{default}$.
|
wenzelm@7335
|
664 |
\item [``$\DOT$''] is a \emph{trivial proof}; it abbreviates $\BY{-}$.
|
wenzelm@7167
|
665 |
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
|
wenzelm@7167
|
666 |
\texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
|
wenzelm@7335
|
667 |
the goal without further ado. Of course, the result is a fake theorem only,
|
wenzelm@7175
|
668 |
involving some oracle in its internal derivation object (this is indicated
|
wenzelm@7319
|
669 |
as $[!]$ in the printed result). The main application of
|
wenzelm@7167
|
670 |
$\isarkeyword{sorry}$ is to support top-down proof development.
|
wenzelm@7167
|
671 |
\end{descr}
|
wenzelm@7134
|
672 |
|
wenzelm@7134
|
673 |
|
wenzelm@7315
|
674 |
\subsection{Improper proof steps}
|
wenzelm@7315
|
675 |
|
wenzelm@7315
|
676 |
The following commands emulate unstructured tactic scripts to some extent.
|
wenzelm@7315
|
677 |
While these are anathema for writing proper Isar proof documents, they might
|
wenzelm@7315
|
678 |
come in handy for exploring and debugging.
|
wenzelm@7315
|
679 |
|
wenzelm@7315
|
680 |
\indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
|
wenzelm@7315
|
681 |
\begin{matharray}{rcl}
|
wenzelm@7315
|
682 |
\isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
|
wenzelm@7315
|
683 |
\isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
|
wenzelm@7315
|
684 |
\isarcmd{back}^* & : & \isartrans{proof}{proof} \\
|
wenzelm@7315
|
685 |
\end{matharray}
|
wenzelm@7315
|
686 |
|
wenzelm@7315
|
687 |
\railalias{thenapply}{then\_apply}
|
wenzelm@7315
|
688 |
\railterm{thenapply}
|
wenzelm@7315
|
689 |
|
wenzelm@7315
|
690 |
\begin{rail}
|
wenzelm@7315
|
691 |
'apply' method
|
wenzelm@7315
|
692 |
;
|
wenzelm@7315
|
693 |
thenapply method
|
wenzelm@7315
|
694 |
;
|
wenzelm@7315
|
695 |
'back'
|
wenzelm@7315
|
696 |
;
|
wenzelm@7315
|
697 |
\end{rail}
|
wenzelm@7315
|
698 |
|
wenzelm@7315
|
699 |
\begin{descr}
|
wenzelm@7335
|
700 |
\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the
|
wenzelm@7315
|
701 |
plain-old-tactic sense. Facts for forward chaining are ignored.
|
wenzelm@7335
|
702 |
\item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,
|
wenzelm@7335
|
703 |
but observes the goal's facts.
|
wenzelm@7315
|
704 |
\item [$\isarkeyword{back}$] does back-tracking over the result sequence of
|
wenzelm@7315
|
705 |
the last proof command. Basically, any proof command may return multiple
|
wenzelm@7315
|
706 |
results.
|
wenzelm@7315
|
707 |
\end{descr}
|
wenzelm@7315
|
708 |
|
wenzelm@7315
|
709 |
|
wenzelm@7315
|
710 |
\subsection{Term abbreviations}\label{sec:term-abbrev}
|
wenzelm@7315
|
711 |
|
wenzelm@7315
|
712 |
\indexisarcmd{let}
|
wenzelm@7315
|
713 |
\begin{matharray}{rcl}
|
wenzelm@7315
|
714 |
\isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7315
|
715 |
\isarkeyword{is} & : & syntax \\
|
wenzelm@7315
|
716 |
\end{matharray}
|
wenzelm@7315
|
717 |
|
wenzelm@7315
|
718 |
Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
|
wenzelm@7315
|
719 |
or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
|
wenzelm@7315
|
720 |
etc.) with a list of patterns $\IS{p@1 \dots p@n}$. In both cases,
|
wenzelm@7315
|
721 |
higher-order matching is applied to bind extra-logical text
|
wenzelm@7315
|
722 |
variables\index{text variables}, which may be either of the form $\VVar{x}$
|
wenzelm@7315
|
723 |
(token class \railtoken{textvar}, see \S\ref{sec:lex-syntax}) or nameless
|
wenzelm@7315
|
724 |
dummies ``\verb,_,'' (underscore).\index{dummy variables} Note that in the
|
wenzelm@7315
|
725 |
$\LETNAME$ form the patterns occur on the left-hand side, while the $\ISNAME$
|
wenzelm@7315
|
726 |
patterns are in postfix position.
|
wenzelm@7315
|
727 |
|
wenzelm@7319
|
728 |
Term abbreviations are quite different from actual local definitions as
|
wenzelm@7319
|
729 |
introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are
|
wenzelm@7315
|
730 |
visible within the logic as actual equations, while abbreviations disappear
|
wenzelm@7315
|
731 |
during the input process just after type checking.
|
wenzelm@7315
|
732 |
|
wenzelm@7315
|
733 |
\begin{rail}
|
wenzelm@7315
|
734 |
'let' ((term + 'as') '=' term comment? + 'and')
|
wenzelm@7315
|
735 |
;
|
wenzelm@7315
|
736 |
\end{rail}
|
wenzelm@7315
|
737 |
|
wenzelm@7315
|
738 |
The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
|
wenzelm@7315
|
739 |
\railnonterm{proppat} (see \S\ref{sec:term-pats}).
|
wenzelm@7315
|
740 |
|
wenzelm@7315
|
741 |
\begin{descr}
|
wenzelm@7315
|
742 |
\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
|
wenzelm@7315
|
743 |
by simultaneous higher-order matching against terms $\vec t$.
|
wenzelm@7315
|
744 |
\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
|
wenzelm@7315
|
745 |
preceding statement. Also note that $\ISNAME$ is not a separate command,
|
wenzelm@7315
|
746 |
but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
|
wenzelm@7315
|
747 |
\end{descr}
|
wenzelm@7315
|
748 |
|
wenzelm@7319
|
749 |
A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
|
wenzelm@7335
|
750 |
goals and facts are available as well. For any open goal,
|
wenzelm@7335
|
751 |
$\VVar{thesis_prop}$ refers to the full proposition (which may be a rule),
|
wenzelm@7335
|
752 |
$\VVar{thesis_concl}$ to its (atomic) conclusion, and $\VVar{thesis}$ to its
|
wenzelm@7335
|
753 |
object-logical statement. The latter two abstract over any meta-level
|
wenzelm@7335
|
754 |
parameters.
|
wenzelm@7315
|
755 |
|
wenzelm@7315
|
756 |
Facts (i.e.\ assumptions and finished goals) that have an application $f(x)$
|
wenzelm@7315
|
757 |
as object-logic statement get $x$ bound to the special text variable
|
wenzelm@7315
|
758 |
``$\dots$'' (three dots). The canonical application of this feature are
|
wenzelm@7335
|
759 |
calculational proofs (see \S\ref{sec:calculation}).
|
wenzelm@7315
|
760 |
|
wenzelm@7315
|
761 |
|
wenzelm@7134
|
762 |
\subsection{Block structure}
|
wenzelm@7134
|
763 |
|
wenzelm@7167
|
764 |
While Isar is inherently block-structured, opening and closing blocks is
|
wenzelm@7167
|
765 |
mostly handled rather casually, with little explicit user-intervention. Any
|
wenzelm@7167
|
766 |
local goal statement automatically opens \emph{two} blocks, which are closed
|
wenzelm@7167
|
767 |
again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of
|
wenzelm@7167
|
768 |
different context within a sub-proof are typically switched via
|
wenzelm@7167
|
769 |
$\isarkeyword{next}$, which is just a single block-close followed by
|
wenzelm@7167
|
770 |
block-open again. Thus the effect of $\isarkeyword{next}$ is to reset the
|
wenzelm@7167
|
771 |
proof context to that of the head of the sub-proof. Note that there is no
|
wenzelm@7175
|
772 |
goal focus involved here!
|
wenzelm@7167
|
773 |
|
wenzelm@7175
|
774 |
For slightly more advanced applications, there are explicit block parentheses
|
wenzelm@7175
|
775 |
as well. These typically achieve a strong forward style of reasoning.
|
wenzelm@7167
|
776 |
|
wenzelm@7134
|
777 |
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
|
wenzelm@7134
|
778 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
779 |
\isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
780 |
\isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
781 |
\isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
|
wenzelm@7134
|
782 |
\end{matharray}
|
wenzelm@7134
|
783 |
|
wenzelm@7167
|
784 |
\begin{descr}
|
wenzelm@7167
|
785 |
\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
|
wenzelm@7167
|
786 |
resetting the context to the initial one.
|
wenzelm@7167
|
787 |
\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
|
wenzelm@7167
|
788 |
close blocks. Any current facts pass through $\isarkeyword{\{\{}$
|
wenzelm@7167
|
789 |
unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into
|
wenzelm@7335
|
790 |
the enclosing context. Thus fixed variables are generalized, assumptions
|
wenzelm@7335
|
791 |
discharged, and local definitions eliminated. There is no difference of
|
wenzelm@7335
|
792 |
$\ASSUMENAME$ and $\PRESUMENAME$ here.
|
wenzelm@7167
|
793 |
\end{descr}
|
wenzelm@7134
|
794 |
|
wenzelm@7134
|
795 |
|
wenzelm@7134
|
796 |
\section{Other commands}
|
wenzelm@7134
|
797 |
|
wenzelm@7134
|
798 |
\subsection{Diagnostics}
|
wenzelm@7134
|
799 |
|
wenzelm@7134
|
800 |
\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
|
wenzelm@7134
|
801 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
802 |
\isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
|
wenzelm@7134
|
803 |
\isarcmd{term} & : & \isarkeep{theory~|~proof} \\
|
wenzelm@7134
|
804 |
\isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
|
wenzelm@7134
|
805 |
\isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
|
wenzelm@7134
|
806 |
\end{matharray}
|
wenzelm@7134
|
807 |
|
wenzelm@7335
|
808 |
These commands are not part of the actual Isabelle/Isar syntax, but assist
|
wenzelm@7335
|
809 |
interactive development. Also note that $undo$ does not apply here, since the
|
wenzelm@7335
|
810 |
theory or proof configuration is not changed.
|
wenzelm@7335
|
811 |
|
wenzelm@7134
|
812 |
\begin{rail}
|
wenzelm@7134
|
813 |
'typ' type
|
wenzelm@7134
|
814 |
;
|
wenzelm@7134
|
815 |
'term' term
|
wenzelm@7134
|
816 |
;
|
wenzelm@7134
|
817 |
'prop' prop
|
wenzelm@7134
|
818 |
;
|
wenzelm@7134
|
819 |
'thm' thmrefs
|
wenzelm@7134
|
820 |
;
|
wenzelm@7134
|
821 |
\end{rail}
|
wenzelm@7134
|
822 |
|
wenzelm@7167
|
823 |
\begin{descr}
|
wenzelm@7134
|
824 |
\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,
|
wenzelm@7134
|
825 |
$\isarkeyword{prop}~\phi$] read and print types / terms / propositions
|
wenzelm@7134
|
826 |
according to the current theory or proof context.
|
wenzelm@7134
|
827 |
\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
|
wenzelm@7134
|
828 |
theory or proof context. Note that any attributes included in the theorem
|
wenzelm@7175
|
829 |
specifications are applied to a temporary context derived from the current
|
wenzelm@7335
|
830 |
theory or proof; the result is discarded, i.e.\ attributes involved in
|
wenzelm@7335
|
831 |
$thms$ only have a temporary effect.
|
wenzelm@7167
|
832 |
\end{descr}
|
wenzelm@7134
|
833 |
|
wenzelm@7134
|
834 |
|
wenzelm@7134
|
835 |
\subsection{System operations}
|
wenzelm@7134
|
836 |
|
wenzelm@7167
|
837 |
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
|
wenzelm@7167
|
838 |
\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
|
wenzelm@7134
|
839 |
\begin{matharray}{rcl}
|
wenzelm@7134
|
840 |
\isarcmd{cd} & : & \isarkeep{\cdot} \\
|
wenzelm@7134
|
841 |
\isarcmd{pwd} & : & \isarkeep{\cdot} \\
|
wenzelm@7134
|
842 |
\isarcmd{use_thy} & : & \isarkeep{\cdot} \\
|
wenzelm@7134
|
843 |
\isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
|
wenzelm@7134
|
844 |
\isarcmd{update_thy} & : & \isarkeep{\cdot} \\
|
wenzelm@7134
|
845 |
\isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
|
wenzelm@7134
|
846 |
\end{matharray}
|
wenzelm@7134
|
847 |
|
wenzelm@7167
|
848 |
\begin{descr}
|
wenzelm@7134
|
849 |
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
|
wenzelm@7134
|
850 |
process.
|
wenzelm@7134
|
851 |
\item [$\isarkeyword{pwd}~$] prints the current working directory.
|
wenzelm@7175
|
852 |
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
|
wenzelm@7175
|
853 |
$\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
|
wenzelm@7175
|
854 |
theory given as $name$ argument. These commands are exactly the same as the
|
wenzelm@7335
|
855 |
corresponding ML functions (see also \cite[\S1,\S6]{isabelle-ref}). Note
|
wenzelm@7335
|
856 |
that both the ML and Isar versions of these commands may load new- and
|
wenzelm@7175
|
857 |
old-style theories alike.
|
wenzelm@7167
|
858 |
\end{descr}
|
wenzelm@7134
|
859 |
|
wenzelm@7335
|
860 |
Note that these system commands are scarcely used when working with
|
wenzelm@7335
|
861 |
Proof~General, since loading of theories is done fully automatic.
|
wenzelm@7335
|
862 |
|
wenzelm@7134
|
863 |
|
wenzelm@7046
|
864 |
%%% Local Variables:
|
wenzelm@7046
|
865 |
%%% mode: latex
|
wenzelm@7046
|
866 |
%%% TeX-master: "isar-ref"
|
wenzelm@7046
|
867 |
%%% End:
|