2 \chapter{Isabelle/Isar Conversion Guide}\label{ap:conv}
4 Subsequently, we give a few practical hints on working in a mixed environment
5 of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are
6 basically three ways to cope with this issue.
8 \item Do not convert old sources at all, but communicate directly at the level
9 of \emph{internal} theory and theorem values.
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).
12 \item Actually redo ML proof scripts as human-readable Isar proof texts
13 (probably hard, depending who wrote the original scripts).
17 \section{No conversion}
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.
26 \subsection{Referring to theorem and theory values}
30 thms : xstring -> thm list
31 the_context : unit -> theory
32 theory : string -> theory
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.
40 \item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored
41 in the current theory context, including any ancestor node.
43 The convention of old-style theories was to bind any theorem as an ML value
44 as well. New-style theories no longer do this, so ML code may require
45 \texttt{thm~"foo"} rather than just \texttt{foo}.
47 \item [$\mathtt{the_context()}$] refers to the current theory context.
49 Old-style theories often use the ML binding \texttt{thy}, which is
50 dynamically created by the ML code generated from old theory source. This
51 is no longer the recommended way in any case! Function \texttt{the_context}
52 should be used for old scripts as well.
54 \item [$\mathtt{theory}~name$] retrieves the named theory from the global
55 theory-loader database.
57 The ML code generated from old-style theories would include an ML binding
58 $name\mathtt{.thy}$ as part of an ML structure.
62 \subsection{Storing theorem values}
66 bind_thm : string * thm -> unit
67 bind_thms : string * thm list -> unit
70 ML proof scripts have to be well-behaved by storing theorems properly within
71 the current theory context, in order to enable new-style theories to retrieve
75 \item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in
76 ML. This already manages entry in the theorem database of the current
78 \item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
79 store theorems that have been produced in ML in an ad-hoc manner.
82 Note that the original ``LCF-system'' approach of binding theorem values on
83 the ML toplevel only has long been given up in Isabelle! Despite of this, old
84 legacy proof scripts occasionally contain code such as \texttt{val foo =
85 result();} which is ill-behaved in several respects. Apart from preventing
86 access from Isar theories, it also omits the result from the WWW presentation,
90 \subsection{ML declarations in Isar}
92 \begin{matharray}{rcl}
93 \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
94 \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
97 Isabelle/Isar theories may contain ML declarations as well. For example, an
98 old-style theorem binding may be mimicked as follows.
100 \isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
102 Note that this command cannot be undone, so invalid theorem bindings in ML may
103 persist. Also note that the current theory may not be modified; use
104 $\isarkeyword{ML_setup}$ for declarations that act on the current context.
107 \section{Porting theories and proof scripts}\label{sec:port-scripts}
109 Porting legacy theory and ML files to proper Isabelle/Isar theories has
110 several advantages. For example, the Proof~General user interface
111 \cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to
112 use than the version for classic Isabelle. This is due to the fact that the
113 generic ML toplevel has been replaced by a separate Isar interaction loop,
114 with full control over input synchronization and error conditions.
116 Furthermore, the Isabelle document preparation system (see also
117 \cite{isabelle-sys}) only works properly with new-style theories. Output of
118 old-style sources is at the level of individual characters (and symbols),
119 without proper document markup as in Isabelle/Isar theories.
122 \subsection{Theories}
124 Basically, the Isabelle/Isar theory syntax is a proper superset of the classic
125 one. Only a few quirks and legacy problems have been eliminated, resulting in
126 simpler rules and less special cases. The main changes of theory syntax are
130 \item Quoted strings may contain arbitrary white space, and span several lines
131 without requiring \verb,\,\,\dots\verb,\, escapes.
132 \item Names may always be quoted.
134 The old syntax would occasionally demand plain identifiers vs.\ quoted
135 strings to accommodate certain syntactic features.
136 \item Types and terms have to be \emph{atomic} as far as the theory syntax is
137 concerned; this typically requires quoting of input strings, e.g.\ ``$x +
140 The old theory syntax used to fake part of the syntax of types in order to
141 require less quoting in common cases; this was hard to predict, though. On
142 the other hand, Isar does not require quotes for simple terms, such as plain
143 identifiers $x$, numerals $1$, or symbols $\forall$ (input as
145 \item Theorem declarations require an explicit colon to separate the name from
146 the statement (the name is usually optional). Cf.\ the syntax of $\DEFS$ in
147 \S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axms-thms}.
150 Note that Isabelle/Isar error messages are usually quite explicit about the
151 problem at hand. So in cases of doubt, input syntax may be just as well tried
155 \subsection{Goal statements}\label{sec:conv-goal}
157 In ML the canonical a goal statement together with a complete proof script is
165 This form may be turned into an Isar tactic-emulation script like this:
167 \LEMMA{name}\texttt"{\phi}\texttt" \\
168 \quad \isarkeyword{apply}~meth@1 \\
170 \quad \isarkeyword{done} \\
172 Note that the main statement may be $\THEOREMNAME$ as well. See
173 \S\ref{sec:conv-tac} for further details on how to convert actual tactic
174 expressions into proof methods.
176 \medskip Classic Isabelle provides many variant forms of goal commands, see
177 \cite{isabelle-ref} for further details. The second most common one is
178 \texttt{Goalw}, which expands definitions before commencing the actual proof
181 Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
183 This is replaced by using the $unfold$ proof method explicitly.
185 \LEMMA{name}\texttt"{\phi}\texttt" \\
186 \quad \isarkeyword{apply}~(unfold~def@1~\dots) \\
189 %FIXME "goal" and higher-order rules;
192 \subsection{Tactics}\label{sec:conv-tac}
194 Isar Proof methods closely resemble traditional tactics, when used in
195 unstructured sequences of $\isarkeyword{apply}$ commands (cf.\
196 \S\ref{sec:conv-goal}). Isabelle/Isar provides emulations for all major ML
197 tactics of classic Isabelle --- mostly for the sake of easy porting of
198 existing developments, as actual Isar proof texts would demand much less
199 diversity of proof methods.
201 Unlike tactic expressions in ML, Isar proof methods provide proper concrete
202 syntax for additional arguments, options, modifiers etc. Thus a typical
203 method text is usually more concise than the corresponding ML tactic.
204 Furthermore, the Isar versions of classic Isabelle tactics often cover several
205 variant forms by a single method with separate options to tune the behavior.
206 For example, method $simp$ replaces all of \texttt{simp_tac}~/
207 \texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},
208 there is also concrete syntax for augmenting the Simplifier context (the
209 current ``simpset'') in a handsome way.
212 \subsubsection{Resolution tactics}
214 Classic Isabelle provides several variant forms of tactics for single-step
215 rule applications (based on higher-order resolution). The space of resolution
216 tactics has the following main dimensions.
218 \item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
219 \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
220 \texttt{forward_tac}).
221 \item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
222 \texttt{res_inst_tac}).
223 \item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
227 Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$,
228 $drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to
229 cover the four modes, either with or without instantiation, and either with
230 single or multiple arguments. Although it is more convenient in most cases to
231 use the plain $rule$ method (see \S\ref{sec:pure-meth-att}), or any of its
232 ``improper'' variants $erule$, $drule$, $frule$ (see
233 \S\ref{sec:misc-methods}). Note that explicit goal addressing is only
234 supported by the actual $rule_tac$ version.
236 With this in mind, plain resolution tactics may be ported as follows.
237 \begin{matharray}{lll}
238 \texttt{rtac}~a~1 & & rule~a \\
239 \texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\
240 \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & &
241 rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex]
242 \texttt{rtac}~a~i & & rule_tac~[i]~a \\
243 \texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\
244 \texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & &
245 rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\
248 Note that explicit goal addressing may be usually avoided by changing the
249 order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see
250 \S\ref{sec:tactic-commands}).
253 \subsubsection{Simplifier tactics}
255 The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
256 (cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
257 methods (see \S\ref{sec:simp}). Note that there is no individual goal
258 addressing available, simplification acts either on the first goal ($simp$)
259 or all goals ($simp_all$).
261 \begin{matharray}{lll}
262 \texttt{Asm_full_simp_tac 1} & & simp \\
263 \texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex]
264 \texttt{Simp_tac 1} & & simp~(no_asm) \\
265 \texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\
266 \texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\
269 Isar also provides separate method modifier syntax for augmenting the
270 Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset''
271 in ML. A typical ML expression with simpset changes looks like this:
273 asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1
275 The corresponding Isar text is as follows:
277 simp~add:~a@1~\dots~del:~b@1~\dots
279 Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered
280 by application of attributes, see \S\ref{sec:conv-decls} for more information.
283 \subsubsection{Classical Reasoner tactics}
285 The Classical Reasoner provides a rather large number of variations of
286 automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},
287 \texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar
288 methods usually share the same base name, such as $blast$, $fast$, $clarify$
289 etc.\ (see \S\ref{sec:classical-auto}).
291 Similar to the Simplifier, there is separate method modifier syntax for
292 augmenting the Classical Reasoner context, which is known as the ``claset'' in
293 ML. A typical ML expression with claset changes looks like this:
295 blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1
297 The corresponding Isar text is as follows:
299 blast~intro:~a@1~\dots~elim!:~b@1~\dots
301 Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are
302 covered by application of attributes, see \S\ref{sec:conv-decls} for more
306 \subsubsection{Miscellaneous tactics}
308 There are a few additional tactics defined in various theories of
309 Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. The most
310 common ones of these may be ported to Isar as follows.
312 \begin{matharray}{lll}
313 \texttt{stac}~a~1 & & subst~a \\
314 \texttt{hyp_subst_tac}~1 & & hypsubst \\
315 \texttt{strip_tac}~1 & \approx & intro~strip \\
316 \texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\
317 & \approx & simp~only:~split_tupled_all \\
322 \subsubsection{Tacticals}
324 Classic Isabelle provides a huge amount of tacticals for combination and
325 modification of existing tactics. This has been greatly reduced in Isar,
326 providing the bare minimum of combinators only: ``$,$'' (sequential
327 composition), ``$|$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at
328 least once). These are usually sufficient in practice; if all fails,
329 arbitrary ML tactic code may be invoked via the $tactic$ method (see
330 \S\ref{sec:tactics}).
332 \medskip Common ML tacticals may be expressed directly in Isar as follows:
333 \begin{matharray}{lll}
334 tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\
335 tac@1~\texttt{ORELSE}~tac@2 & & meth@1~|~meth@2 \\
336 \texttt{TRY}~tac & & meth? \\
337 \texttt{REPEAT1}~tac & & meth+ \\
338 \texttt{REPEAT}~tac & & (meth+)? \\
339 \texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\
340 \texttt{FIRST}~[tac@1, \dots] & & meth@1~|~\dots \\
343 \medskip \texttt{CHANGED} (see \cite{isabelle-ref}) is usually not required in
344 Isar, since most basic proof methods already fail unless there is an actual
345 change in the goal state. Nevertheless, ``$?$'' (try) may be used to accept
346 \emph{unchanged} results as well.
348 \medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref})
349 are not available in Isar, since there is no direct goal addressing.
350 Nevertheless, some basic methods address all goals internally, notably
351 $simp_all$ (see \S\ref{sec:simp}). Also note that \texttt{ALLGOALS} may be
352 often replaced by ``$+$'' (repeat at least once), although this usually has a
353 different operational behavior, such as solving goals in a different order.
355 \medskip Iterated resolution, such as
356 \texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
357 using the $intro$ and $elim$ methods of Isar (see
358 \S\ref{sec:classical-basic}).
361 \subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
363 Apart from proof commands and tactic expressions, almost all of the remaining
364 ML code occurring in legacy proof scripts are either global context
365 declarations (such as \texttt{Addsimps}) or ad-hoc operations on theorems
366 (such as \texttt{RS}). In Isar both of these are covered by theorem
367 expressions with \emph{attributes}.
369 \medskip Theorem operations may be attached as attributes in the very place
370 where theorems are referenced, say within a method argument. The subsequent
371 common ML combinators may be expressed directly in Isar as follows.
372 \begin{matharray}{lll}
373 thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\
374 thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\
375 thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\
376 \relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\
377 \texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\
378 \texttt{standard}~thm & & thm~[standard] \\
379 \texttt{make_elim}~thm & & thm~[elim_format] \\
382 Note that $OF$ is often more readable as $THEN$; likewise positional
383 instantiation with $of$ is more handsome than $where$.
385 The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
386 replaced by passing the result of a proof through $rule_format$.
388 \medskip Global ML declarations may be expressed using the
389 $\isarkeyword{declare}$ command (see \S\ref{sec:tactic-commands}) together
390 with appropriate attributes. The most common ones are as follows.
391 \begin{matharray}{lll}
392 \texttt{Addsimps}~[thm] & & \isarkeyword{declare}~thm~[simp] \\
393 \texttt{Delsimps}~[thm] & & \isarkeyword{declare}~thm~[simp~del] \\
394 \texttt{Addsplits}~[thm] & & \isarkeyword{declare}~thm~[split] \\
395 \texttt{Delsplits}~[thm] & & \isarkeyword{declare}~thm~[split~del] \\[0.5ex]
396 \texttt{AddIs}~[thm] & & \isarkeyword{declare}~thm~[intro] \\
397 \texttt{AddEs}~[thm] & & \isarkeyword{declare}~thm~[elim] \\
398 \texttt{AddDs}~[thm] & & \isarkeyword{declare}~thm~[dest] \\
399 \texttt{AddSIs}~[thm] & & \isarkeyword{declare}~thm~[intro!] \\
400 \texttt{AddSEs}~[thm] & & \isarkeyword{declare}~thm~[elim!] \\
401 \texttt{AddSDs}~[thm] & & \isarkeyword{declare}~thm~[dest!] \\[0.5ex]
402 \texttt{AddIffs}~[thm] & & \isarkeyword{declare}~thm~[iff] \\
404 Note that explicit $\isarkeyword{declare}$ commands are actually needed only
405 very rarely; Isar admits to declare theorems on-the-fly wherever they emerge.
406 Consider the following ML idiom:
413 This may be expressed more concisely in Isar like this:
415 \LEMMA{name~[simp]}{\phi} \\
418 The $name$ may be even omitted, although this would make it difficult to
419 declare the theorem otherwise later (e.g.\ as $[simp~del]$).
422 \section{Converting to actual Isar proof texts}
424 Porting legacy ML proof scripts into Isar tactic emulation scripts (see
425 \S\ref{sec:port-scripts}) is mainly a technical issue, since the basic
426 representation of formal ``proof script'' is preserved. In contrast,
427 converting existing Isabelle developments into actual human-readably Isar
428 proof texts is more involved, due to the fundamental change of the underlying
431 This issue is comparable to that of converting programs written in a low-level
432 programming languages (say Assembler) into higher-level ones (say Haskell).
433 In order to accomplish this, one needs a working knowledge of the target
434 language, as well an understanding of the \emph{original} idea of the piece of
435 code expressed in the low-level language.
437 As far as Isar proofs are concerned, it is usually much easier to re-use only
438 definitions and the main statements directly, while following the arrangement
439 of proof scripts only very loosely. Ideally, one would also have some
440 \emph{informal} proof outlines available for guidance as well. In the worst
441 case, obscure proof scripts would have to be re-engineered by tracing forth
442 and backwards, and by educated guessing!
444 \medskip This is a possible schedule to embark on actual conversion of legacy
445 proof scripts into Isar proof texts.
447 \item Port ML scripts to Isar tactic emulation scripts (see
448 \S\ref{sec:port-scripts}).
449 \item Get sufficiently acquainted with Isabelle/Isar proof
450 development.\footnote{As there is still no Isar tutorial around, it is best
451 to look at existing Isar examples, see also \S\ref{sec:isar-howto}.}
452 \item Recover the proof structure of a few important theorems.
453 \item Rephrase the original intention of the course of reasoning in terms of
454 Isar proof language elements.
457 Certainly, rewriting formal reasoning in Isar requires much additional effort.
458 On the other hand, one gains a human-readable representation of
459 machine-checked formal proof. Depending on the context of application, this
460 might be even indispensable to start with!
465 %%% TeX-master: "isar-ref"