9607

1 

10160

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.


42 


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


46 


47 
\item [$\mathtt{the_context()}$] refers to the current theory context.


48 


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.

10111

53 


54 
\item [$\mathtt{theory}~name$] retrieves the named theory from the global

10153

55 
theoryloader database.

10111

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


72 
these these later.


73 


74 
\begin{descr}


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


77 
theory context.


78 
\item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]

10160

79 
store theorems that have been produced in ML in an adhoc manner.

10111

80 
\end{descr}


81 

10153

82 
Note that the original ``LCFsystem'' approach of binding theorem values on

10160

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 illbehaved in several respects. Apart from preventing


86 
access from Isar theories, it also omits the result from the WWW presentation,


87 
for example.

10111

88 

10153

89 


90 
\subsection{ML declarations in Isar}

10111

91 


92 
\begin{matharray}{rcl}


93 
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\

10153

94 
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\

10111

95 
\end{matharray}


96 

10153

97 
Isabelle/Isar theories may contain ML declarations as well. For example, an


98 
oldstyle theorem binding may be mimicked as follows.

10111

99 
\[


100 
\isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}


101 
\]

10160

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

10153

104 
$\isarkeyword{ML_setup}$ for declarations that act on the current context.

9607

105 


106 

10153

107 
\section{Porting theories and proof scripts}\label{sec:portscripts}

9607

108 

10111

109 
Porting legacy theory and ML files to proper Isabelle/Isar theories has


110 
several advantages. For example, the Proof~General user interface

10153

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.

10111

115 

10153

116 
Furthermore, the Isabelle document preparation system (see also


117 
\cite{isabellesys}) only works properly with newstyle theories. Output of


118 
oldstyle sources is at the level of individual characters (and symbols),


119 
without proper document markup as in Isabelle/Isar theories.

10111

120 


121 

10153

122 
\subsection{Theories}


123 


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


127 
as follows.

10111

128 


129 
\begin{itemize}

10153

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.


133 


134 
The old syntax would occasionally demand plain identifiers vs.\ quoted


135 
strings to accommodate certain syntactic features.

10111

136 
\item Types and terms have to be \emph{atomic} as far as the theory syntax is

10153

137 
concerned; this typically requires quoting of input strings, e.g.\ ``$x +


138 
y$''.

10111

139 


140 
The old theory syntax used to fake part of the syntax of types in order to

10153

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


144 
\verb,\<forall>,).


145 
\item Theorem declarations require an explicit colon to separate the name from

10160

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

10111

148 
\end{itemize}


149 

10160

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


152 
out interactively.

10111

153 


154 

10153

155 
\subsection{Goal statements}\label{sec:convgoal}

10111

156 

10239

157 
\subsubsection{Simple goals}


158 

10153

159 
In ML the canonical a goal statement together with a complete proof script is


160 
as follows:


161 
\begin{ttbox}


162 
Goal "\(\phi\)";


163 
by \(tac@1\);


164 
\(\vdots\)


165 
qed "\(name\)";


166 
\end{ttbox}


167 
This form may be turned into an Isar tacticemulation script like this:

10111

168 
\begin{matharray}{l}

10239

169 
\LEMMA{name}{\texttt"{\phi}\texttt"} \\

10223

170 
\quad \APPLY{meth@1} \\

10153

171 
\qquad \vdots \\

10223

172 
\quad \DONE \\

10111

173 
\end{matharray}

10153

174 
Note that the main statement may be $\THEOREMNAME$ as well. See


175 
\S\ref{sec:convtac} for further details on how to convert actual tactic


176 
expressions into proof methods.

10111

177 


178 
\medskip Classic Isabelle provides many variant forms of goal commands, see

10239

179 
also \cite{isabelleref} for further details. The second most common one is

10111

180 
\texttt{Goalw}, which expands definitions before commencing the actual proof


181 
script.


182 
\begin{ttbox}

10153

183 
Goalw [\(def@1\), \(\dots\)] "\(\phi\)";

10111

184 
\end{ttbox}

10239

185 
This may be replaced by using the $unfold$ proof method explicitly.

10111

186 
\begin{matharray}{l}

10239

187 
\LEMMA{name}{\texttt"{\phi}\texttt"} \\

10223

188 
\quad \APPLY{unfold~def@1~\dots} \\

10111

189 
\end{matharray}


190 

10239

191 


192 
\subsubsection{Deriving rules}


193 


194 
Deriving nonatomic metalevel propositions requires special precautions in


195 
classic Isabelle: the primitive \texttt{goal} command decomposes a statement


196 
into the atomic conclusion and a list of assumptions, which are exhibited as


197 
ML values of type \texttt{thm}. After the proof is finished, these premises


198 
are discharged again, resulting in the original rule statement.


199 


200 
In contrast, Isabelle/Isar does \emph{not} require any special treatment of


201 
nonatomic statements  assumptions and goals may be arbitrarily complex.


202 
While this would basically require to proceed by structured proof, decomposing


203 
the main problem into subproblems according to the basic Isar scheme of


204 
backward reasoning, the old tacticstyle procedure may be mimicked as follows.


205 
The general ML goal statement for derived rules looks like this:


206 
\begin{ttbox}


207 
val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)";


208 
by \(tac@1\);


209 
\(\vdots\)


210 
\end{ttbox}


211 
This form may be turned into a tacticemulation script that is wrapped in an


212 
Isar text to get access to the premises as local facts.


213 
\begin{matharray}{l}


214 
\LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\


215 
\PROOF{}~ \\


216 
\quad \ASSUME{prem@1}{\phi@1}~\AND~\dots \\


217 
\quad \SHOW{}{\Var{thesis}} \\


218 
\qquad \APPLY{meth@1} \\


219 
\qquad\quad \vdots \\


220 
\qquad \DONE \\


221 
\QED{} \\


222 
\end{matharray}


223 
Note that the above scheme repeats the text of premises $\phi@1$, \dots, while


224 
the conclusion $\psi$ is referenced via the automatic text abbreviation


225 
$\Var{thesis}$. The assumption context may be invoked in a less verbose


226 
manner as well, using ``$\CASE{antecedent}$'' instead of


227 
``$\ASSUME{prem@1}{\phi@1}~\AND~\dots$'' above. Then the list of \emph{all}


228 
premises is bound to the name $antecedent$; Isar does not provide a way to


229 
destruct lists into single items, though.

10111

230 

10239

231 
\medskip In practice, actual rules are often rather direct consequences of


232 
corresponding atomic statements, typically stemming from the definition of a


233 
new concept. In that case, the general scheme for deriving rules may be


234 
greatly simplified, using one of the standard automated proof tools, such ad


235 
$simp$, $blast$, or $auto$. This would work as follows:


236 
\begin{matharray}{l}


237 
\LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\


238 
\quad \APPLY{unfold~defs} \quad \CMT{or ``$\APPLY{insert~facts}$''} \\


239 
\quad \APPLY{blast} \\


240 
\quad \DONE \\


241 
\end{matharray}


242 
Note that classic Isabelle would support this form only in the special case


243 
where $\phi@1$, \dots are atomic statements (when using the standard


244 
\texttt{Goal} command). Otherwise the special treatment of rules would be


245 
applied, disturbing this simple setup.


246 


247 
\medskip Occasionally, derived rules would be established by first proving an


248 
appropriate atomic statement (using $\forall$ and $\longrightarrow$ of the


249 
objectlogic), and putting the final result into ``rule format''. In classic


250 
Isabelle this would usually proceed as follows:


251 
\begin{ttbox}


252 
Goal "\(\phi\)";


253 
by \(tac@1\);


254 
\(\vdots\)


255 
qed_spec_mp "\(name\)";


256 
\end{ttbox}


257 
The operation performed by \texttt{qed_spec_mp} is also performed by the Isar


258 
attribute ``$rule_format$'', see also \S\ref{sec:ruleformat}. Thus the


259 
corresponding Isar text may look like this:


260 
\begin{matharray}{l}


261 
\LEMMA{name~[rule_format]}{\texttt"{\phi}\texttt"} \\


262 
\quad \APPLY{meth@1} \\


263 
\qquad \vdots \\


264 
\quad \DONE \\


265 
\end{matharray}


266 
Note plain ``$rule_format$'' actually performs a slightly different operation:


267 
it fully replaces objectlevel implication and universal quantification


268 
throughout the whole result statement. This is the right thing in most cases.


269 
For historical reasons, \texttt{qed_spec_mp} would only operate on the


270 
conclusion; one may get this exact behavior by using


271 
``$rule_format~(no_asm)$'' instead.

10111

272 

10153

273 
\subsection{Tactics}\label{sec:convtac}


274 


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

10223

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


277 
Isabelle/Isar provides emulations for all major ML tactics of classic Isabelle


278 
 mostly for the sake of easy porting of existing developments, as actual


279 
Isar proof texts would demand much less diversity of proof methods.

10153

280 


281 
Unlike tactic expressions in ML, Isar proof methods provide proper concrete


282 
syntax for additional arguments, options, modifiers etc. Thus a typical


283 
method text is usually more concise than the corresponding ML tactic.


284 
Furthermore, the Isar versions of classic Isabelle tactics often cover several

10160

285 
variant forms by a single method with separate options to tune the behavior.


286 
For example, method $simp$ replaces all of \texttt{simp_tac}~/


287 
\texttt{asm_simp_tac}~/ \texttt{full_simp_tac}~/ \texttt{asm_full_simp_tac},

10153

288 
there is also concrete syntax for augmenting the Simplifier context (the

10160

289 
current ``simpset'') in a handsome way.

10153

290 


291 


292 
\subsubsection{Resolution tactics}

10111

293 

10153

294 
Classic Isabelle provides several variant forms of tactics for singlestep

10160

295 
rule applications (based on higherorder resolution). The space of resolution

10153

296 
tactics has the following main dimensions.


297 
\begin{enumerate}

10160

298 
\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\

10153

299 
\texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},


300 
\texttt{forward_tac}).

10160

301 
\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\

10153

302 
\texttt{res_inst_tac}).

10160

303 
\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\

10153

304 
\texttt{rtac}).


305 
\end{enumerate}


306 


307 
Basically, the set of Isar tactic emulations $rule_tac$, $erule_tac$,


308 
$drule_tac$, $frule_tac$ (see \S\ref{sec:tactics}) would be sufficient to


309 
cover the four modes, either with or without instantiation, and either with


310 
single or multiple arguments. Although it is more convenient in most cases to


311 
use the plain $rule$ method (see \S\ref{sec:puremethatt}), or any of its


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


313 
\S\ref{sec:miscmethods}). Note that explicit goal addressing is only

10160

314 
supported by the actual $rule_tac$ version.

10153

315 

10160

316 
With this in mind, plain resolution tactics may be ported as follows.

10153

317 
\begin{matharray}{lll}


318 
\texttt{rtac}~a~1 & & rule~a \\


319 
\texttt{resolve_tac}~[a@1, \dots]~1 & & rule~a@1~\dots \\


320 
\texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~1 & &


321 
rule_tac~x@1 = t@1~and~\dots~in~a \\[0.5ex]


322 
\texttt{rtac}~a~i & & rule_tac~[i]~a \\


323 
\texttt{resolve_tac}~[a@1, \dots]~i & & rule_tac~[i]~a@1~\dots \\


324 
\texttt{res_inst_tac}~[(x@1, t@1), \dots]~a~i & &


325 
rule_tac~[i]~x@1 = t@1~and~\dots~in~a \\


326 
\end{matharray}


327 


328 
Note that explicit goal addressing may be usually avoided by changing the


329 
order of subgoals with $\isarkeyword{defer}$ or $\isarkeyword{prefer}$ (see


330 
\S\ref{sec:tacticcommands}).


331 


332 


333 
\subsubsection{Simplifier tactics}

10111

334 

10153

335 
The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants


336 
(cf.\ \cite{isabelleref}) are all covered by the $simp$ and $simp_all$


337 
methods (see \S\ref{sec:simp}). Note that there is no individual goal


338 
addressing available, simplification acts either on the first goal ($simp$)


339 
or all goals ($simp_all$).


340 


341 
\begin{matharray}{lll}


342 
\texttt{Asm_full_simp_tac 1} & & simp \\


343 
\texttt{ALLGOALS Asm_full_simp_tac} & & simp_all \\[0.5ex]


344 
\texttt{Simp_tac 1} & & simp~(no_asm) \\


345 
\texttt{Asm_simp_tac 1} & & simp~(no_asm_simp) \\


346 
\texttt{Full_simp_tac 1} & & simp~(no_asm_use) \\


347 
\end{matharray}

10111

348 

10153

349 
Isar also provides separate method modifier syntax for augmenting the


350 
Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset''


351 
in ML. A typical ML expression with simpset changes looks like this:


352 
\begin{ttbox}


353 
asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1


354 
\end{ttbox}


355 
The corresponding Isar text is as follows:


356 
\[


357 
simp~add:~a@1~\dots~del:~b@1~\dots


358 
\]


359 
Global declarations of Simplifier rules (e.g.\ \texttt{Addsimps}) are covered


360 
by application of attributes, see \S\ref{sec:convdecls} for more information.


361 


362 


363 
\subsubsection{Classical Reasoner tactics}

10111

364 

10153

365 
The Classical Reasoner provides a rather large number of variations of


366 
automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac},


367 
\texttt{Clarify_tac} etc.\ (see \cite{isabelleref}). The corresponding Isar

10160

368 
methods usually share the same base name, such as $blast$, $fast$, $clarify$

10153

369 
etc.\ (see \S\ref{sec:classicalauto}).

9798

370 

10153

371 
Similar to the Simplifier, there is separate method modifier syntax for


372 
augmenting the Classical Reasoner context, which is known as the ``claset'' in


373 
ML. A typical ML expression with claset changes looks like this:


374 
\begin{ttbox}


375 
blast_tac (claset () addIs [\(a@1\), \(\dots\)] addSEs [\(b@1\), \(\dots\)]) 1


376 
\end{ttbox}


377 
The corresponding Isar text is as follows:


378 
\[


379 
blast~intro:~a@1~\dots~elim!:~b@1~\dots


380 
\]


381 
Global declarations of Classical Reasoner rules (e.g.\ \texttt{AddIs}) are


382 
covered by application of attributes, see \S\ref{sec:convdecls} for more


383 
information.


384 


385 


386 
\subsubsection{Miscellaneous tactics}


387 


388 
There are a few additional tactics defined in various theories of


389 
Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. The most


390 
common ones of these may be ported to Isar as follows.


391 


392 
\begin{matharray}{lll}

9798

393 
\texttt{stac}~a~1 & & subst~a \\

10153

394 
\texttt{hyp_subst_tac}~1 & & hypsubst \\


395 
\texttt{strip_tac}~1 & \approx & intro~strip \\


396 
\texttt{split_all_tac}~1 & & simp~(no_asm_simp)~only:~split_tupled_all \\


397 
& \approx & simp~only:~split_tupled_all \\


398 
& \ll & clarify \\

9798

399 
\end{matharray}


400 


401 

10153

402 
\subsubsection{Tacticals}


403 


404 
Classic Isabelle provides a huge amount of tacticals for combination and


405 
modification of existing tactics. This has been greatly reduced in Isar,


406 
providing the bare minimum of combinators only: ``$,$'' (sequential


407 
composition), ``$$'' (alternative choices), ``$?$'' (try), ``$+$'' (repeat at

10160

408 
least once). These are usually sufficient in practice; if all fails,


409 
arbitrary ML tactic code may be invoked via the $tactic$ method (see

10153

410 
\S\ref{sec:tactics}).


411 


412 
\medskip Common ML tacticals may be expressed directly in Isar as follows:


413 
\begin{matharray}{lll}


414 
tac@1~\texttt{THEN}~tac@2 & & meth@1, meth@2 \\


415 
tac@1~\texttt{ORELSE}~tac@2 & & meth@1~~meth@2 \\


416 
\texttt{TRY}~tac & & meth? \\


417 
\texttt{REPEAT1}~tac & & meth+ \\


418 
\texttt{REPEAT}~tac & & (meth+)? \\


419 
\texttt{EVERY}~[tac@1, \dots] & & meth@1, \dots \\


420 
\texttt{FIRST}~[tac@1, \dots] & & meth@1~~\dots \\


421 
\end{matharray}


422 


423 
\medskip \texttt{CHANGED} (see \cite{isabelleref}) is usually not required in


424 
Isar, since most basic proof methods already fail unless there is an actual


425 
change in the goal state. Nevertheless, ``$?$'' (try) may be used to accept


426 
\emph{unchanged} results as well.


427 


428 
\medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelleref})

10160

429 
are not available in Isar, since there is no direct goal addressing.


430 
Nevertheless, some basic methods address all goals internally, notably


431 
$simp_all$ (see \S\ref{sec:simp}). Also note that \texttt{ALLGOALS} may be


432 
often replaced by ``$+$'' (repeat at least once), although this usually has a


433 
different operational behavior, such as solving goals in a different order.

10153

434 


435 
\medskip Iterated resolution, such as


436 
\texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed


437 
using the $intro$ and $elim$ methods of Isar (see


438 
\S\ref{sec:classicalbasic}).

10111

439 

9607

440 

10153

441 
\subsection{Declarations and adhoc operations}\label{sec:convdecls}

9607

442 

10153

443 
Apart from proof commands and tactic expressions, almost all of the remaining


444 
ML code occurring in legacy proof scripts are either global context


445 
declarations (such as \texttt{Addsimps}) or adhoc operations on theorems


446 
(such as \texttt{RS}). In Isar both of these are covered by theorem


447 
expressions with \emph{attributes}.


448 


449 
\medskip Theorem operations may be attached as attributes in the very place


450 
where theorems are referenced, say within a method argument. The subsequent


451 
common ML combinators may be expressed directly in Isar as follows.


452 
\begin{matharray}{lll}


453 
thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\

10160

454 
thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\

10153

455 
thm@1~\texttt{COMP}~thm@2 & & thm@1~[COMP~thm@2] \\


456 
\relax[thm@1, \dots]~\texttt{MRS}~thm & & thm~[OF~thm@1~\dots] \\


457 
\texttt{read_instantiate}~[(x@1, t@1), \dots]~thm & & thm~[where~x@1 = t@1~and~\dots] \\


458 
\texttt{standard}~thm & & thm~[standard] \\


459 
\texttt{make_elim}~thm & & thm~[elim_format] \\


460 
\end{matharray}

10160

461 


462 
Note that $OF$ is often more readable as $THEN$; likewise positional

10153

463 
instantiation with $of$ is more handsome than $where$.


464 


465 
The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be

10160

466 
replaced by passing the result of a proof through $rule_format$.

10153

467 

10223

468 
\medskip Global ML declarations may be expressed using the $\DECLARE$ command


469 
(see \S\ref{sec:tacticcommands}) together with appropriate attributes. The


470 
most common ones are as follows.

10153

471 
\begin{matharray}{lll}

10223

472 
\texttt{Addsimps}~[thm] & & \DECLARE~thm~[simp] \\


473 
\texttt{Delsimps}~[thm] & & \DECLARE~thm~[simp~del] \\


474 
\texttt{Addsplits}~[thm] & & \DECLARE~thm~[split] \\


475 
\texttt{Delsplits}~[thm] & & \DECLARE~thm~[split~del] \\[0.5ex]


476 
\texttt{AddIs}~[thm] & & \DECLARE~thm~[intro] \\


477 
\texttt{AddEs}~[thm] & & \DECLARE~thm~[elim] \\


478 
\texttt{AddDs}~[thm] & & \DECLARE~thm~[dest] \\


479 
\texttt{AddSIs}~[thm] & & \DECLARE~thm~[intro!] \\


480 
\texttt{AddSEs}~[thm] & & \DECLARE~thm~[elim!] \\


481 
\texttt{AddSDs}~[thm] & & \DECLARE~thm~[dest!] \\[0.5ex]


482 
\texttt{AddIffs}~[thm] & & \DECLARE~thm~[iff] \\

10153

483 
\end{matharray}

10223

484 
Note that explicit $\DECLARE$ commands are actually needed only very rarely;


485 
Isar admits to declare theorems onthefly wherever they emerge. Consider the


486 
following ML idiom:

10153

487 
\begin{ttbox}


488 
Goal "\(\phi\)";


489 
\(\vdots\)


490 
qed "name";


491 
Addsimps [name];


492 
\end{ttbox}


493 
This may be expressed more concisely in Isar like this:


494 
\begin{matharray}{l}


495 
\LEMMA{name~[simp]}{\phi} \\


496 
\quad\vdots


497 
\end{matharray}

10160

498 
The $name$ may be even omitted, although this would make it difficult to


499 
declare the theorem otherwise later (e.g.\ as $[simp~del]$).

10153

500 


501 


502 
\section{Converting to actual Isar proof texts}


503 


504 
Porting legacy ML proof scripts into Isar tactic emulation scripts (see

10160

505 
\S\ref{sec:portscripts}) is mainly a technical issue, since the basic


506 
representation of formal ``proof script'' is preserved. In contrast,


507 
converting existing Isabelle developments into actual humanreadably Isar

10153

508 
proof texts is more involved, due to the fundamental change of the underlying


509 
paradigm.


510 


511 
This issue is comparable to that of converting programs written in a lowlevel

10160

512 
programming languages (say Assembler) into higherlevel ones (say Haskell).


513 
In order to accomplish this, one needs a working knowledge of the target

10153

514 
language, as well an understanding of the \emph{original} idea of the piece of


515 
code expressed in the lowlevel language.


516 


517 
As far as Isar proofs are concerned, it is usually much easier to reuse only


518 
definitions and the main statements directly, while following the arrangement


519 
of proof scripts only very loosely. Ideally, one would also have some

10160

520 
\emph{informal} proof outlines available for guidance as well. In the worst


521 
case, obscure proof scripts would have to be reengineered by tracing forth


522 
and backwards, and by educated guessing!

10153

523 


524 
\medskip This is a possible schedule to embark on actual conversion of legacy


525 
proof scripts into Isar proof texts.


526 
\begin{enumerate}


527 
\item Port ML scripts to Isar tactic emulation scripts (see


528 
\S\ref{sec:portscripts}).


529 
\item Get sufficiently acquainted with Isabelle/Isar proof


530 
development.\footnote{As there is still no Isar tutorial around, it is best

10160

531 
to look at existing Isar examples, see also \S\ref{sec:isarhowto}.}

10153

532 
\item Recover the proof structure of a few important theorems.


533 
\item Rephrase the original intention of the course of reasoning in terms of


534 
Isar proof language elements.


535 
\end{enumerate}


536 

10160

537 
Certainly, rewriting formal reasoning in Isar requires much additional effort.


538 
On the other hand, one gains a humanreadable representation of


539 
machinechecked formal proof. Depending on the context of application, this


540 
might be even indispensable to start with!


541 

9607

542 


543 
%%% Local Variables:


544 
%%% mode: latex


545 
%%% TeXmaster: "isarref"


546 
%%% End:
