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 oldstyle theory files to newstyle ones (very easy), and ML proof


11 
scripts to Isar tacticemulation scripts (quite easy).

10160

12 
\item Actually redo ML proof scripts as humanreadable 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 newstyle 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 
Oldstyle theories used to emit many ML bindings of theorems and theories, but


37 
this is no longer done in newstyle 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 oldstyle theories was to bind any theorem as an ML value

10153

44 
as well. Newstyle 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 
Oldstyle 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 
theoryloader database.

13048

56 

10153

57 
The ML code generated from oldstyle 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 wellbehaved by storing theorems properly within

10111

71 
the current theory context, in order to enable newstyle 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 adhoc manner.

13041

82 

10111

83 
\end{descr}


84 

10153

85 
Note that the original ``LCFsystem'' 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 illbehaved 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 
oldstyle 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:portscripts}

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{isabellesys}) only works properly with newstyle theories. Output of


121 
oldstyle 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:axmsthms}.

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:convgoal}

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 tacticemulation 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:convtac} 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{isabelleref} 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 nonatomic metalevel 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 tacticemulation 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 
objectlogic), 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:objectlogic}. 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 objectlevel 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 objectlogic 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:convtac}


279 


280 
Isar Proof methods closely resemble traditional tactics, when used in

10223

281 
unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:convgoal}).


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 singlestep

10160

300 
rule applications (based on higherorder 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:puremethatt}), or any of its


317 
``improper'' variants $erule$, $drule$, $frule$ (see

12618

318 
\S\ref{sec:miscmethatt}). 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:tacticcommands}).


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{isabelleref}) 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:convdecls} 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{isabelleref}). 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:convdecls} 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{isabelleref}) 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{isabelleref})

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 adhoc operations}\label{sec:convdecls}

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 adhoc 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:tacticcommands}) 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 onthefly 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:portscripts}) 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 humanreadably 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 lowlevel

10160

527 
programming languages (say Assembler) into higherlevel 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 lowlevel language.


531 


532 
As far as Isar proofs are concerned, it is usually much easier to reuse 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 reengineered 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:portscripts}).

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:isarhowto}.}

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 humanreadable representation of


560 
machinechecked 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 
%%% TeXmaster: "isarref"

13048

566 
%%% End:
