9607
|
1 |
|
13048
|
2 |
\chapter{Isabelle/Isar conversion guide}\label{ap:conv}
|
9607
|
3 |
|
10111
|
4 |
Subsequently, we give a few practical hints on working in a mixed environment
|
10153
|
5 |
of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are
|
10111
|
6 |
basically three ways to cope with this issue.
|
|
7 |
\begin{enumerate}
|
|
8 |
\item Do not convert old sources at all, but communicate directly at the level
|
10160
|
9 |
of \emph{internal} theory and theorem values.
|
10153
|
10 |
\item Port old-style theory files to new-style ones (very easy), and ML proof
|
|
11 |
scripts to Isar tactic-emulation scripts (quite easy).
|
10160
|
12 |
\item Actually redo ML proof scripts as human-readable Isar proof texts
|
10111
|
13 |
(probably hard, depending who wrote the original scripts).
|
|
14 |
\end{enumerate}
|
|
15 |
|
|
16 |
|
9607
|
17 |
\section{No conversion}
|
|
18 |
|
10153
|
19 |
Internally, Isabelle is able to handle both old and new-style theories at the
|
|
20 |
same time; the theory loader automatically detects the input format. In any
|
|
21 |
case, the results are certain internal ML values of type \texttt{theory} and
|
|
22 |
\texttt{thm}. These may be accessed from either classic Isabelle or
|
|
23 |
Isabelle/Isar, provided that some minimal precautions are observed.
|
|
24 |
|
10111
|
25 |
|
|
26 |
\subsection{Referring to theorem and theory values}
|
|
27 |
|
|
28 |
\begin{ttbox}
|
|
29 |
thm : xstring -> thm
|
|
30 |
thms : xstring -> thm list
|
|
31 |
the_context : unit -> theory
|
|
32 |
theory : string -> theory
|
|
33 |
\end{ttbox}
|
|
34 |
|
10153
|
35 |
These functions provide general means to refer to logical objects from ML.
|
|
36 |
Old-style theories used to emit many ML bindings of theorems and theories, but
|
|
37 |
this is no longer done in new-style Isabelle/Isar theories.
|
10111
|
38 |
|
|
39 |
\begin{descr}
|
|
40 |
\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
|
|
41 |
in the current theory context, including any ancestor node.
|
13048
|
42 |
|
10111
|
43 |
The convention of old-style theories was to bind any theorem as an ML value
|
10153
|
44 |
as well. New-style theories no longer do this, so ML code may require
|
10111
|
45 |
\texttt{thm~"foo"} rather than just \texttt{foo}.
|
13048
|
46 |
|
10111
|
47 |
\item [$\mathtt{the_context()}$] refers to the current theory context.
|
13048
|
48 |
|
10111
|
49 |
Old-style theories often use the ML binding \texttt{thy}, which is
|
10153
|
50 |
dynamically created by the ML code generated from old theory source. This
|
10160
|
51 |
is no longer the recommended way in any case! Function \texttt{the_context}
|
|
52 |
should be used for old scripts as well.
|
13048
|
53 |
|
10111
|
54 |
\item [$\mathtt{theory}~name$] retrieves the named theory from the global
|
10153
|
55 |
theory-loader database.
|
13048
|
56 |
|
10153
|
57 |
The ML code generated from old-style theories would include an ML binding
|
10111
|
58 |
$name\mathtt{.thy}$ as part of an ML structure.
|
|
59 |
\end{descr}
|
|
60 |
|
|
61 |
|
10153
|
62 |
\subsection{Storing theorem values}
|
10111
|
63 |
|
|
64 |
\begin{ttbox}
|
|
65 |
qed : string -> unit
|
|
66 |
bind_thm : string * thm -> unit
|
|
67 |
bind_thms : string * thm list -> unit
|
|
68 |
\end{ttbox}
|
|
69 |
|
10160
|
70 |
ML proof scripts have to be well-behaved by storing theorems properly within
|
10111
|
71 |
the current theory context, in order to enable new-style theories to retrieve
|
13041
|
72 |
these later.
|
10111
|
73 |
|
|
74 |
\begin{descr}
|
13048
|
75 |
|
10111
|
76 |
\item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in
|
|
77 |
ML. This already manages entry in the theorem database of the current
|
|
78 |
theory context.
|
13048
|
79 |
|
10111
|
80 |
\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
|
10160
|
81 |
store theorems that have been produced in ML in an ad-hoc manner.
|
13041
|
82 |
|
10111
|
83 |
\end{descr}
|
|
84 |
|
10153
|
85 |
Note that the original ``LCF-system'' approach of binding theorem values on
|
10160
|
86 |
the ML toplevel only has long been given up in Isabelle! Despite of this, old
|
|
87 |
legacy proof scripts occasionally contain code such as \texttt{val foo =
|
|
88 |
result();} which is ill-behaved in several respects. Apart from preventing
|
|
89 |
access from Isar theories, it also omits the result from the WWW presentation,
|
|
90 |
for example.
|
10111
|
91 |
|
10153
|
92 |
|
|
93 |
\subsection{ML declarations in Isar}
|
10111
|
94 |
|
|
95 |
\begin{matharray}{rcl}
|
|
96 |
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
|
10153
|
97 |
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
|
10111
|
98 |
\end{matharray}
|
|
99 |
|
10153
|
100 |
Isabelle/Isar theories may contain ML declarations as well. For example, an
|
|
101 |
old-style theorem binding may be mimicked as follows.
|
10111
|
102 |
\[
|
|
103 |
\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
|
|
104 |
\]
|
10160
|
105 |
Note that this command cannot be undone, so invalid theorem bindings in ML may
|
|
106 |
persist. Also note that the current theory may not be modified; use
|
10153
|
107 |
$\isarkeyword{ML_setup}$ for declarations that act on the current context.
|
9607
|
108 |
|
|
109 |
|
10153
|
110 |
\section{Porting theories and proof scripts}\label{sec:port-scripts}
|
9607
|
111 |
|
10111
|
112 |
Porting legacy theory and ML files to proper Isabelle/Isar theories has
|
|
113 |
several advantages. For example, the Proof~General user interface
|
10153
|
114 |
\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to
|
|
115 |
use than the version for classic Isabelle. This is due to the fact that the
|
|
116 |
generic ML toplevel has been replaced by a separate Isar interaction loop,
|
|
117 |
with full control over input synchronization and error conditions.
|
10111
|
118 |
|
10153
|
119 |
Furthermore, the Isabelle document preparation system (see also
|
|
120 |
\cite{isabelle-sys}) only works properly with new-style theories. Output of
|
|
121 |
old-style sources is at the level of individual characters (and symbols),
|
|
122 |
without proper document markup as in Isabelle/Isar theories.
|
10111
|
123 |
|
|
124 |
|
10153
|
125 |
\subsection{Theories}
|
|
126 |
|
|
127 |
Basically, the Isabelle/Isar theory syntax is a proper superset of the classic
|
|
128 |
one. Only a few quirks and legacy problems have been eliminated, resulting in
|
|
129 |
simpler rules and less special cases. The main changes of theory syntax are
|
|
130 |
as follows.
|
10111
|
131 |
|
|
132 |
\begin{itemize}
|
10153
|
133 |
\item Quoted strings may contain arbitrary white space, and span several lines
|
|
134 |
without requiring \verb,\,\,\dots\verb,\, escapes.
|
|
135 |
\item Names may always be quoted.
|
13048
|
136 |
|
10153
|
137 |
The old syntax would occasionally demand plain identifiers vs.\ quoted
|
|
138 |
strings to accommodate certain syntactic features.
|
10111
|
139 |
\item Types and terms have to be \emph{atomic} as far as the theory syntax is
|
10153
|
140 |
concerned; this typically requires quoting of input strings, e.g.\ ``$x +
|
|
141 |
y$''.
|
13048
|
142 |
|
10111
|
143 |
The old theory syntax used to fake part of the syntax of types in order to
|
10153
|
144 |
require less quoting in common cases; this was hard to predict, though. On
|
|
145 |
the other hand, Isar does not require quotes for simple terms, such as plain
|
|
146 |
identifiers $x$, numerals $1$, or symbols $\forall$ (input as
|
|
147 |
\verb,\<forall>,).
|
|
148 |
\item Theorem declarations require an explicit colon to separate the name from
|
10160
|
149 |
the statement (the name is usually optional). Cf.\ the syntax of $\DEFS$ in
|
|
150 |
\S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}.
|
10111
|
151 |
\end{itemize}
|
|
152 |
|
10160
|
153 |
Note that Isabelle/Isar error messages are usually quite explicit about the
|
|
154 |
problem at hand. So in cases of doubt, input syntax may be just as well tried
|
|
155 |
out interactively.
|
10111
|
156 |
|
|
157 |
|
10153
|
158 |
\subsection{Goal statements}\label{sec:conv-goal}
|
10111
|
159 |
|
10239
|
160 |
\subsubsection{Simple goals}
|
|
161 |
|
10153
|
162 |
In ML the canonical a goal statement together with a complete proof script is
|
|
163 |
as follows:
|
|
164 |
\begin{ttbox}
|
|
165 |
Goal "\(\phi\)";
|
|
166 |
by \(tac@1\);
|
|
167 |
\(\vdots\)
|
|
168 |
qed "\(name\)";
|
|
169 |
\end{ttbox}
|
|
170 |
This form may be turned into an Isar tactic-emulation script like this:
|
10111
|
171 |
\begin{matharray}{l}
|
10239
|
172 |
\LEMMA{name}{\texttt"{\phi}\texttt"} \\
|
10223
|
173 |
\quad \APPLY{meth@1} \\
|
10153
|
174 |
\qquad \vdots \\
|
10223
|
175 |
\quad \DONE \\
|
10111
|
176 |
\end{matharray}
|
13013
|
177 |
Note that the main statement may be $\THEOREMNAME$ or $\COROLLARYNAME$ as
|
|
178 |
well. See \S\ref{sec:conv-tac} for further details on how to convert actual
|
|
179 |
tactic expressions into proof methods.
|
10111
|
180 |
|
|
181 |
\medskip Classic Isabelle provides many variant forms of goal commands, see
|
10239
|
182 |
also \cite{isabelle-ref} for further details. The second most common one is
|
10111
|
183 |
\texttt{Goalw}, which expands definitions before commencing the actual proof
|
|
184 |
script.
|
|
185 |
\begin{ttbox}
|
10153
|
186 |
Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
|
10111
|
187 |
\end{ttbox}
|
10239
|
188 |
This may be replaced by using the $unfold$ proof method explicitly.
|
10111
|
189 |
\begin{matharray}{l}
|
10239
|
190 |
\LEMMA{name}{\texttt"{\phi}\texttt"} \\
|
13042
|
191 |
\quad \APPLY{(unfold~def@1~\dots)} \\
|
10111
|
192 |
\end{matharray}
|
|
193 |
|
10239
|
194 |
|
|
195 |
\subsubsection{Deriving rules}
|
|
196 |
|
|
197 |
Deriving non-atomic meta-level propositions requires special precautions in
|
|
198 |
classic Isabelle: the primitive \texttt{goal} command decomposes a statement
|
|
199 |
into the atomic conclusion and a list of assumptions, which are exhibited as
|
|
200 |
ML values of type \texttt{thm}. After the proof is finished, these premises
|
13013
|
201 |
are discharged again, resulting in the original rule statement. The ``long
|
|
202 |
format'' of Isabelle/Isar goal statements admits to emulate this technique
|
13041
|
203 |
nicely. The general ML goal statement for derived rules looks like this:
|
10239
|
204 |
\begin{ttbox}
|
|
205 |
val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)";
|
|
206 |
by \(tac@1\);
|
|
207 |
\(\vdots\)
|
13013
|
208 |
qed "\(a\)"
|
10239
|
209 |
\end{ttbox}
|
13013
|
210 |
This form may be turned into a tactic-emulation script as follows:
|
10239
|
211 |
\begin{matharray}{l}
|
13013
|
212 |
\LEMMA{a}{} \\
|
|
213 |
\quad \ASSUMES{prem@1}{\texttt"\phi@1\texttt"}~\AND~\dots \\
|
|
214 |
\quad \SHOWS{}{\texttt"{\psi}\texttt"} \\
|
10239
|
215 |
\qquad \APPLY{meth@1} \\
|
|
216 |
\qquad\quad \vdots \\
|
|
217 |
\qquad \DONE \\
|
|
218 |
\end{matharray}
|
10111
|
219 |
|
10239
|
220 |
\medskip In practice, actual rules are often rather direct consequences of
|
|
221 |
corresponding atomic statements, typically stemming from the definition of a
|
|
222 |
new concept. In that case, the general scheme for deriving rules may be
|
11498
|
223 |
greatly simplified, using one of the standard automated proof tools, such as
|
13041
|
224 |
$simp$, $blast$, or $auto$. This could work as follows:
|
10239
|
225 |
\begin{matharray}{l}
|
|
226 |
\LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
|
13042
|
227 |
\quad \BYY{(unfold~defs)}{blast} \\
|
10239
|
228 |
\end{matharray}
|
|
229 |
Note that classic Isabelle would support this form only in the special case
|
|
230 |
where $\phi@1$, \dots are atomic statements (when using the standard
|
|
231 |
\texttt{Goal} command). Otherwise the special treatment of rules would be
|
|
232 |
applied, disturbing this simple setup.
|
|
233 |
|
|
234 |
\medskip Occasionally, derived rules would be established by first proving an
|
|
235 |
appropriate atomic statement (using $\forall$ and $\longrightarrow$ of the
|
|
236 |
object-logic), and putting the final result into ``rule format''. In classic
|
|
237 |
Isabelle this would usually proceed as follows:
|
|
238 |
\begin{ttbox}
|
|
239 |
Goal "\(\phi\)";
|
|
240 |
by \(tac@1\);
|
|
241 |
\(\vdots\)
|
|
242 |
qed_spec_mp "\(name\)";
|
|
243 |
\end{ttbox}
|
|
244 |
The operation performed by \texttt{qed_spec_mp} is also performed by the Isar
|
12618
|
245 |
attribute ``$rule_format$'', see also \S\ref{sec:object-logic}. Thus the
|
10239
|
246 |
corresponding Isar text may look like this:
|
|
247 |
\begin{matharray}{l}
|
|
248 |
\LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\
|
|
249 |
\quad \APPLY{meth@1} \\
|
|
250 |
\qquad \vdots \\
|
|
251 |
\quad \DONE \\
|
|
252 |
\end{matharray}
|
|
253 |
Note plain ``$rule_format$'' actually performs a slightly different operation:
|
|
254 |
it fully replaces object-level implication and universal quantification
|
|
255 |
throughout the whole result statement. This is the right thing in most cases.
|
|
256 |
For historical reasons, \texttt{qed_spec_mp} would only operate on the
|
|
257 |
conclusion; one may get this exact behavior by using
|
|
258 |
``$rule_format~(no_asm)$'' instead.
|
10111
|
259 |
|
13013
|
260 |
\medskip Actually ``$rule_format$'' is a bit unpleasant to work with, since
|
|
261 |
the final result statement is not shown in the text. An alternative is to
|
|
262 |
state the resulting rule in the intended form in the first place, and have the
|
|
263 |
initial refinement step turn it into internal object-logic form using the
|
|
264 |
$atomize$ method indicated below. The remaining script is unchanged.
|
|
265 |
|
|
266 |
\begin{matharray}{l}
|
|
267 |
\LEMMA{name}{\texttt"{\All{\vec x}\vec\phi \Imp \psi}\texttt"} \\
|
13042
|
268 |
\quad \APPLY{(atomize~(full))} \\
|
13013
|
269 |
\quad \APPLY{meth@1} \\
|
|
270 |
\qquad \vdots \\
|
|
271 |
\quad \DONE \\
|
|
272 |
\end{matharray}
|
|
273 |
|
13041
|
274 |
In many situations the $atomize$ step above is actually unnecessary,
|
|
275 |
especially if the subsequent script mainly consists of automated tools.
|
|
276 |
|
13013
|
277 |
|
10153
|
278 |
\subsection{Tactics}\label{sec:conv-tac}
|
|
279 |
|
|
280 |
Isar Proof methods closely resemble traditional tactics, when used in
|
10223
|
281 |
unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:conv-goal}).
|
|
282 |
Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle
|
|
283 |
--- mostly for the sake of easy porting of existing developments, as actual
|
|
284 |
Isar proof texts would demand much less diversity of proof methods.
|
10153
|
285 |
|
|
286 |
Unlike tactic expressions in ML, Isar proof methods provide proper concrete
|
|
287 |
syntax for additional arguments, options, modifiers etc. Thus a typical
|
|
288 |
method text is usually more concise than the corresponding ML tactic.
|
|
289 |
Furthermore, the Isar versions of classic Isabelle tactics often cover several
|
10160
|
290 |
variant forms by a single method with separate options to tune the behavior.
|
|
291 |
For example, method $simp$ replaces all of \texttt{simp_tac}~/
|
|
292 |
\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
|
10153
|
293 |
there is also concrete syntax for augmenting the Simplifier context (the
|
13041
|
294 |
current ``simpset'') in a convenient way.
|
10153
|
295 |
|
|
296 |
|
|
297 |
\subsubsection{Resolution tactics}
|
10111
|
298 |
|
10153
|
299 |
Classic Isabelle provides several variant forms of tactics for single-step
|
10160
|
300 |
rule applications (based on higher-order resolution). The space of resolution
|
10153
|
301 |
tactics has the following main dimensions.
|
|
302 |
\begin{enumerate}
|
13048
|
303 |
\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
|
10153
|
304 |
\texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
|
|
305 |
\texttt{forward_tac}).
|
13048
|
306 |
\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
|
10153
|
307 |
\texttt{res_inst_tac}).
|
13048
|
308 |
\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
|
10153
|
309 |
\texttt{rtac}).
|
|
310 |
\end{enumerate}
|
|
311 |
|
|
312 |
Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$,
|
|
313 |
$drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to
|
|
314 |
cover the four modes, either with or without instantiation, and either with
|
|
315 |
single or multiple arguments. Although it is more convenient in most cases to
|
|
316 |
use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its
|
|
317 |
``improper'' variants $erule$, $drule$, $frule$ (see
|
12618
|
318 |
\S\ref{sec:misc-meth-att}). Note that explicit goal addressing is only
|
10160
|
319 |
supported by the actual $rule_tac$ version.
|
10153
|
320 |
|
10160
|
321 |
With this in mind, plain resolution tactics may be ported as follows.
|
10153
|
322 |
\begin{matharray}{lll}
|
|
323 |
\texttt{rtac}~a~1 & & rule~a \\
|
|
324 |
\texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\
|
|
325 |
\texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & &
|
|
326 |
rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex]
|
|
327 |
\texttt{rtac}~a~i & & rule_tac~[i]~a \\
|
|
328 |
\texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\
|
|
329 |
\texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & &
|
|
330 |
rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\
|
|
331 |
\end{matharray}
|
|
332 |
|
|
333 |
Note that explicit goal addressing may be usually avoided by changing the
|
|
334 |
order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see
|
|
335 |
\S\ref{sec:tactic-commands}).
|
|
336 |
|
10740
|
337 |
\medskip Some further (less frequently used) combinations of basic resolution
|
|
338 |
tactics may be expressed as follows.
|
|
339 |
\begin{matharray}{lll}
|
|
340 |
\texttt{ares_tac}~[a@1, \dots]~1 & & assumption~|~rule~a@1~\dots \\
|
|
341 |
\texttt{eatac}~a~n~1 & & erule~(n)~a \\
|
|
342 |
\texttt{datac}~a~n~1 & & drule~(n)~a \\
|
|
343 |
\texttt{fatac}~a~n~1 & & frule~(n)~a \\
|
|
344 |
\end{matharray}
|
|
345 |
|
10153
|
346 |
|
|
347 |
\subsubsection{Simplifier tactics}
|
10111
|
348 |
|
10153
|
349 |
The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
|
|
350 |
(cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
|
13048
|
351 |
methods (see \S\ref{sec:simplifier}). Note that there is no individual goal
|
|
352 |
addressing available, simplification acts either on the first goal ($simp$) or
|
|
353 |
all goals ($simp_all$).
|
10153
|
354 |
|
|
355 |
\begin{matharray}{lll}
|
|
356 |
\texttt{Asm_full_simp_tac 1} & & simp \\
|
|
357 |
\texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex]
|
|
358 |
\texttt{Simp_tac 1} & & simp~(no_asm) \\
|
|
359 |
\texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\
|
|
360 |
\texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\
|
13625
|
361 |
\texttt{Asm_lr_simp_tac 1} & & simp~(asm_lr) \\
|
10153
|
362 |
\end{matharray}
|
10111
|
363 |
|
10153
|
364 |
Isar also provides separate method modifier syntax for augmenting the
|
13048
|
365 |
Simplifier context (see \S\ref{sec:simplifier}), which is known as the
|
|
366 |
``simpset'' in ML. A typical ML expression with simpset changes looks like
|
|
367 |
this:
|
10153
|
368 |
\begin{ttbox}
|
|
369 |
asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
|
|
370 |
\end{ttbox}
|
|
371 |
The corresponding Isar text is as follows:
|
|
372 |
\[
|
|
373 |
simp~add:~a@1~\dots~del:~b@1~\dots
|
|
374 |
\]
|
|
375 |
Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered
|
|
376 |
by application of attributes, see \S\ref{sec:conv-decls} for more information.
|
|
377 |
|
|
378 |
|
|
379 |
\subsubsection{Classical Reasoner tactics}
|
10111
|
380 |
|
10153
|
381 |
The Classical Reasoner provides a rather large number of variations of
|
|
382 |
automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
|
|
383 |
\texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar
|
10160
|
384 |
methods usually share the same base name, such as $blast$, $fast$, $clarify$
|
13048
|
385 |
etc.\ (see \S\ref{sec:classical}).
|
9798
|
386 |
|
10153
|
387 |
Similar to the Simplifier, there is separate method modifier syntax for
|
|
388 |
augmenting the Classical Reasoner context, which is known as the ``claset'' in
|
|
389 |
ML. A typical ML expression with claset changes looks like this:
|
|
390 |
\begin{ttbox}
|
|
391 |
blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1
|
|
392 |
\end{ttbox}
|
|
393 |
The corresponding Isar text is as follows:
|
|
394 |
\[
|
|
395 |
blast~intro:~a@1~\dots~elim!:~b@1~\dots
|
|
396 |
\]
|
|
397 |
Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are
|
|
398 |
covered by application of attributes, see \S\ref{sec:conv-decls} for more
|
|
399 |
information.
|
|
400 |
|
|
401 |
|
|
402 |
\subsubsection{Miscellaneous tactics}
|
|
403 |
|
|
404 |
There are a few additional tactics defined in various theories of
|
|
405 |
Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. The most
|
|
406 |
common ones of these may be ported to Isar as follows.
|
|
407 |
|
|
408 |
\begin{matharray}{lll}
|
9798
|
409 |
\texttt{stac}~a~1 & & subst~a \\
|
10153
|
410 |
\texttt{hyp_subst_tac}~1 & & hypsubst \\
|
|
411 |
\texttt{strip_tac}~1 & \approx & intro~strip \\
|
|
412 |
\texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\
|
|
413 |
& \approx & simp~only:~split_tupled_all \\
|
|
414 |
& \ll & clarify \\
|
9798
|
415 |
\end{matharray}
|
|
416 |
|
|
417 |
|
10153
|
418 |
\subsubsection{Tacticals}
|
|
419 |
|
|
420 |
Classic Isabelle provides a huge amount of tacticals for combination and
|
|
421 |
modification of existing tactics. This has been greatly reduced in Isar,
|
|
422 |
providing the bare minimum of combinators only: ``$,$'' (sequential
|
|
423 |
composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at
|
10160
|
424 |
least once). These are usually sufficient in practice; if all fails,
|
|
425 |
arbitrary ML tactic code may be invoked via the $tactic$ method (see
|
10153
|
426 |
\S\ref{sec:tactics}).
|
|
427 |
|
|
428 |
\medskip Common ML tacticals may be expressed directly in Isar as follows:
|
|
429 |
\begin{matharray}{lll}
|
|
430 |
tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\
|
|
431 |
tac@1~\texttt{ORELSE}~tac@2 & & meth@1~|~meth@2 \\
|
|
432 |
\texttt{TRY}~tac & & meth? \\
|
|
433 |
\texttt{REPEAT1}~tac & & meth+ \\
|
|
434 |
\texttt{REPEAT}~tac & & (meth+)? \\
|
|
435 |
\texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\
|
|
436 |
\texttt{FIRST}~[tac@1, \dots] & & meth@1~|~\dots \\
|
|
437 |
\end{matharray}
|
|
438 |
|
|
439 |
\medskip \texttt{CHANGED} (see \cite{isabelle-ref}) is usually not required in
|
|
440 |
Isar, since most basic proof methods already fail unless there is an actual
|
|
441 |
change in the goal state. Nevertheless, ``$?$'' (try) may be used to accept
|
|
442 |
\emph{unchanged} results as well.
|
|
443 |
|
|
444 |
\medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
|
10160
|
445 |
are not available in Isar, since there is no direct goal addressing.
|
|
446 |
Nevertheless, some basic methods address all goals internally, notably
|
13048
|
447 |
$simp_all$ (see \S\ref{sec:simplifier}). Also note that \texttt{ALLGOALS} may
|
|
448 |
be often replaced by ``$+$'' (repeat at least once), although this usually has
|
|
449 |
a different operational behavior, such as solving goals in a different order.
|
10153
|
450 |
|
|
451 |
\medskip Iterated resolution, such as
|
|
452 |
\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
|
13048
|
453 |
using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}).
|
10111
|
454 |
|
9607
|
455 |
|
10153
|
456 |
\subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
|
9607
|
457 |
|
10153
|
458 |
Apart from proof commands and tactic expressions, almost all of the remaining
|
|
459 |
ML code occurring in legacy proof scripts are either global context
|
|
460 |
declarations (such as \texttt{Addsimps}) or ad-hoc operations on theorems
|
|
461 |
(such as \texttt{RS}). In Isar both of these are covered by theorem
|
|
462 |
expressions with \emph{attributes}.
|
|
463 |
|
|
464 |
\medskip Theorem operations may be attached as attributes in the very place
|
|
465 |
where theorems are referenced, say within a method argument. The subsequent
|
13041
|
466 |
ML combinators may be expressed directly in Isar as follows.
|
10153
|
467 |
\begin{matharray}{lll}
|
|
468 |
thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\
|
10160
|
469 |
thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\
|
10153
|
470 |
thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\
|
|
471 |
\relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\
|
|
472 |
\texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\
|
13041
|
473 |
\texttt{make_elim}~thm & & thm~[elim_format] \\
|
10153
|
474 |
\texttt{standard}~thm & & thm~[standard] \\
|
|
475 |
\end{matharray}
|
10160
|
476 |
|
|
477 |
Note that $OF$ is often more readable as $THEN$; likewise positional
|
13041
|
478 |
instantiation with $of$ is often more appropriate than $where$.
|
10153
|
479 |
|
|
480 |
The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
|
10160
|
481 |
replaced by passing the result of a proof through $rule_format$.
|
10153
|
482 |
|
10223
|
483 |
\medskip Global ML declarations may be expressed using the $\DECLARE$ command
|
|
484 |
(see \S\ref{sec:tactic-commands}) together with appropriate attributes. The
|
|
485 |
most common ones are as follows.
|
10153
|
486 |
\begin{matharray}{lll}
|
10223
|
487 |
\texttt{Addsimps}~[thm] & & \DECLARE~thm~[simp] \\
|
|
488 |
\texttt{Delsimps}~[thm] & & \DECLARE~thm~[simp~del] \\
|
|
489 |
\texttt{Addsplits}~[thm] & & \DECLARE~thm~[split] \\
|
|
490 |
\texttt{Delsplits}~[thm] & & \DECLARE~thm~[split~del] \\[0.5ex]
|
|
491 |
\texttt{AddIs}~[thm] & & \DECLARE~thm~[intro] \\
|
|
492 |
\texttt{AddEs}~[thm] & & \DECLARE~thm~[elim] \\
|
|
493 |
\texttt{AddDs}~[thm] & & \DECLARE~thm~[dest] \\
|
|
494 |
\texttt{AddSIs}~[thm] & & \DECLARE~thm~[intro!] \\
|
|
495 |
\texttt{AddSEs}~[thm] & & \DECLARE~thm~[elim!] \\
|
|
496 |
\texttt{AddSDs}~[thm] & & \DECLARE~thm~[dest!] \\[0.5ex]
|
|
497 |
\texttt{AddIffs}~[thm] & & \DECLARE~thm~[iff] \\
|
10153
|
498 |
\end{matharray}
|
13041
|
499 |
Note that explicit $\DECLARE$ commands are rarely needed in practice; Isar
|
|
500 |
admits to declare theorems on-the-fly wherever they emerge. Consider the
|
10223
|
501 |
following ML idiom:
|
10153
|
502 |
\begin{ttbox}
|
|
503 |
Goal "\(\phi\)";
|
|
504 |
\(\vdots\)
|
|
505 |
qed "name";
|
|
506 |
Addsimps [name];
|
|
507 |
\end{ttbox}
|
13041
|
508 |
This may be expressed more succinctly in Isar like this:
|
10153
|
509 |
\begin{matharray}{l}
|
|
510 |
\LEMMA{name~[simp]}{\phi} \\
|
|
511 |
\quad\vdots
|
|
512 |
\end{matharray}
|
10160
|
513 |
The $name$ may be even omitted, although this would make it difficult to
|
|
514 |
declare the theorem otherwise later (e.g.\ as $[simp~del]$).
|
10153
|
515 |
|
|
516 |
|
12621
|
517 |
\section{Writing actual Isar proof texts}
|
10153
|
518 |
|
|
519 |
Porting legacy ML proof scripts into Isar tactic emulation scripts (see
|
10160
|
520 |
\S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
|
|
521 |
representation of formal ``proof script'' is preserved. In contrast,
|
|
522 |
converting existing Isabelle developments into actual human-readably Isar
|
10153
|
523 |
proof texts is more involved, due to the fundamental change of the underlying
|
|
524 |
paradigm.
|
|
525 |
|
|
526 |
This issue is comparable to that of converting programs written in a low-level
|
10160
|
527 |
programming languages (say Assembler) into higher-level ones (say Haskell).
|
|
528 |
In order to accomplish this, one needs a working knowledge of the target
|
10153
|
529 |
language, as well an understanding of the \emph{original} idea of the piece of
|
|
530 |
code expressed in the low-level language.
|
|
531 |
|
|
532 |
As far as Isar proofs are concerned, it is usually much easier to re-use only
|
13041
|
533 |
definitions and the main statements, while following the arrangement of proof
|
|
534 |
scripts only very loosely. Ideally, one would also have some \emph{informal}
|
|
535 |
proof outlines available for guidance as well. In the worst case, obscure
|
|
536 |
proof scripts would have to be re-engineered by tracing forth and backwards,
|
|
537 |
and by educated guessing!
|
10153
|
538 |
|
|
539 |
\medskip This is a possible schedule to embark on actual conversion of legacy
|
|
540 |
proof scripts into Isar proof texts.
|
13041
|
541 |
|
10153
|
542 |
\begin{enumerate}
|
13041
|
543 |
|
10153
|
544 |
\item Port ML scripts to Isar tactic emulation scripts (see
|
|
545 |
\S\ref{sec:port-scripts}).
|
13041
|
546 |
|
10153
|
547 |
\item Get sufficiently acquainted with Isabelle/Isar proof
|
|
548 |
development.\footnote{As there is still no Isar tutorial around, it is best
|
10160
|
549 |
to look at existing Isar examples, see also \S\ref{sec:isar-howto}.}
|
13041
|
550 |
|
10153
|
551 |
\item Recover the proof structure of a few important theorems.
|
13041
|
552 |
|
10153
|
553 |
\item Rephrase the original intention of the course of reasoning in terms of
|
|
554 |
Isar proof language elements.
|
13041
|
555 |
|
10153
|
556 |
\end{enumerate}
|
|
557 |
|
13041
|
558 |
Certainly, rewriting formal reasoning in Isar requires some additional effort.
|
10160
|
559 |
On the other hand, one gains a human-readable representation of
|
|
560 |
machine-checked formal proof. Depending on the context of application, this
|
|
561 |
might be even indispensable to start with!
|
|
562 |
|
13048
|
563 |
%%% Local Variables:
|
9607
|
564 |
%%% mode: latex
|
|
565 |
%%% TeX-master: "isar-ref"
|
13048
|
566 |
%%% End:
|