9607

1 


2 
\chapter{The Isabelle/Isar Conversion Guide}


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


9 
of 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).

10111

12 
\item Actually redo ML proof scripts as human readable Isar proof texts


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


51 
is no longer the recommended way in any case! The \texttt{the_context}


52 
function 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 


70 
ML proof scripts have to be wellbehaved in storing theorems properly within


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)$]

10153

79 
store (lists of) 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


83 
the ML toplevel only has long been given up in Isabelle! Legacy proof scripts


84 
occasionally contain code such as \texttt{val foo = result();} which is


85 
illbehaved in several respects. Apart from preventing access from Isar


86 
theories, it also omits the result from the WWW presentation, for example.

10111

87 

10153

88 


89 
\subsection{ML declarations in Isar}

10111

90 


91 
\begin{matharray}{rcl}


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

10153

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

10111

94 
\end{matharray}


95 

10153

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


97 
oldstyle theorem binding may be mimicked as follows.

10111

98 
\[


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


100 
\]

10153

101 
This command cannot be undone; invalid theorem bindings in ML may persist.


102 
Also note that the current theory may not be modified; use


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

9607

104 


105 

10153

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

9607

107 

10111

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


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

10153

110 
\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable to


111 
use than the version for classic Isabelle. This is due to the fact that the


112 
generic ML toplevel has been replaced by a separate Isar interaction loop,


113 
with full control over input synchronization and error conditions.

10111

114 

10153

115 
Furthermore, the Isabelle document preparation system (see also


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


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


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

10111

119 


120 

10153

121 
\subsection{Theories}


122 


123 
Basically, the Isabelle/Isar theory syntax is a proper superset of the classic


124 
one. Only a few quirks and legacy problems have been eliminated, resulting in


125 
simpler rules and less special cases. The main changes of theory syntax are


126 
as follows.

10111

127 


128 
\begin{itemize}

10153

129 
\item Quoted strings may contain arbitrary white space, and span several lines


130 
without requiring \verb,\,\,\dots\verb,\, escapes.


131 
\item Names may always be quoted.


132 


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


134 
strings to accommodate certain syntactic features.

10111

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

10153

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


137 
y$''.

10111

138 


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

10153

140 
require less quoting in common cases; this was hard to predict, though. On


141 
the other hand, Isar does not require quotes for simple terms, such as plain


142 
identifiers $x$, numerals $1$, or symbols $\forall$ (input as


143 
\verb,\<forall>,).


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


145 
the statement (the name is usually optional). See the syntax of $\DEFS$ in


146 
\S\ref{sec:consts}, or $\THEOREMNAME$ in \S\ref{sec:axmsthms}), for


147 
example.

10111

148 
\end{itemize}


149 

10153

150 
Also note that Isabelle/Isar error messages are usually quite explicit about


151 
the problem at hand. So in cases of doubt, input syntax may be just as well


152 
tried interactively.

10111

153 


154 

10153

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

10111

156 

10153

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


158 
as follows:


159 
\begin{ttbox}


160 
Goal "\(\phi\)";


161 
by \(tac@1\);


162 
\(\vdots\)


163 
qed "\(name\)";


164 
\end{ttbox}


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

10111

166 
\begin{matharray}{l}

10153

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


168 
\quad \isarkeyword{apply}~meth@1 \\


169 
\qquad \vdots \\


170 
\quad \isarkeyword{done} \\

10111

171 
\end{matharray}

10153

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


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


174 
expressions into proof methods.

10111

175 


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


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


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


179 
script.


180 
\begin{ttbox}

10153

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

10111

182 
\end{ttbox}

10153

183 
This is replaced by using the $unfold$ proof method explicitly.

10111

184 
\begin{matharray}{l}


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

10153

186 
\quad \isarkeyword{apply}~(unfold~def@1~\dots) \\

10111

187 
\end{matharray}


188 


189 
%FIXME "goal" and higherorder rules;


190 


191 

10153

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


193 


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


195 
unstructured sequences of $\isarkeyword{apply}$ commands (cf.\


196 
\S\ref{sec:convgoal}). Isabelle/Isar provides emulations for all major ML


197 
tactic of classic Isabelle, mostly for the sake of easy porting of existing


198 
developments  actual Isar proof texts would demand much less diversity of


199 
proof methods.


200 


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 into a single method, with separate options to tune the


206 
behavior. 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'').


210 


211 


212 
\subsubsection{Resolution tactics}

10111

213 

10153

214 
Classic Isabelle provides several variant forms of tactics for singlestep


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


216 
tactics has the following main dimensions.


217 
\begin{enumerate}


218 
\item The ``mode'' of resolution: intro, elim, destruct, 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},


222 
\texttt{res_inst_tac}).


223 
\item Abbreviations for common arguments (e.g.\ \texttt{resolve_tac},


224 
\texttt{rtac}).


225 
\end{enumerate}


226 


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:puremethatt}), or any of its


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


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


234 
supported by $rule_tac$ versions.


235 


236 
\medskip Thus plain resolution tactics may be ported to Isar 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 \\


246 
\end{matharray}


247 


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:tacticcommands}).


251 


252 


253 
\subsubsection{Simplifier tactics}

10111

254 

10153

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


256 
(cf.\ \cite{isabelleref}) 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$).


260 


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) \\


267 
\end{matharray}

10111

268 

10153

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:


272 
\begin{ttbox}


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


274 
\end{ttbox}


275 
The corresponding Isar text is as follows:


276 
\[


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


278 
\]


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


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


281 


282 


283 
\subsubsection{Classical Reasoner tactics}

10111

284 

10153

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{isabelleref}). The corresponding Isar


288 
methods usually have the same base name, such as $blast$, $fast$, $clarify$


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

9798

290 

10153

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:


294 
\begin{ttbox}


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


296 
\end{ttbox}


297 
The corresponding Isar text is as follows:


298 
\[


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


300 
\]


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


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


303 
information.


304 


305 


306 
\subsubsection{Miscellaneous tactics}


307 


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.


311 


312 
\begin{matharray}{lll}

9798

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

10153

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 \\


318 
& \ll & clarify \\

9798

319 
\end{matharray}


320 


321 

10153

322 
\subsubsection{Tacticals}


323 


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). Nevertheless, these are usually sufficient in practice. If all


329 
fails, arbitrary ML tactic code may be invoked via the $tactic$ method (see


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


331 


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 \\


341 
\end{matharray}


342 


343 
\medskip \texttt{CHANGED} (see \cite{isabelleref}) 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.


347 


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


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


350 
Nevertheless, some basic methods (notably $simp_all$, see \S\ref{sec:simp})


351 
address all goals internally. Also note that \texttt{ALLGOALS} may be often


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


353 
slightly different operational behavior, such as solving goals in a different


354 
order.


355 


356 
\medskip Iterated resolution, such as


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


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


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

10111

360 

9607

361 

10153

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

9607

363 

10153

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


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


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


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


368 
expressions with \emph{attributes}.


369 


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


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


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


373 
\begin{matharray}{lll}


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


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


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


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


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


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


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


381 
\end{matharray}


382 
Note that $OF$ is often more readable then $THEN$; likewise positional


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


384 


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 the $rule_format$.


387 


388 
\medskip Global ML declarations may be expressed using the


389 
$\isarkeyword{declare}$ command (see \S\ref{sec:tacticcommands}) 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] \\


403 
\end{matharray}


404 
Note that explicit $\isarkeyword{declare}$ commands are actually needed only


405 
very rarely; Isar admits to declare theorems onthefly wherever they emerge.


406 
Consider the following ML idiom:


407 
\begin{ttbox}


408 
Goal "\(\phi\)";


409 
\(\vdots\)


410 
qed "name";


411 
Addsimps [name];


412 
\end{ttbox}


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


414 
\begin{matharray}{l}


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


416 
\quad\vdots


417 
\end{matharray}


418 


419 


420 
\section{Converting to actual Isar proof texts}


421 


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


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


424 
representation of the formal ``proof'' has been preserved. In contrast,


425 
converting existing Isabelle developments into actual human readably Isar


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


427 
paradigm.


428 


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


430 
programming languages (say assembly) into higherlevel ones (say Haskell). In


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


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


433 
code expressed in the lowlevel language.


434 


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


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


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


438 
\emph{informal} proof outlines available as well. In the worst case, obscure


439 
proof scripts would have to be reengineered by tracing forth and backwards,


440 
and by educated guessing!


441 


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


443 
proof scripts into Isar proof texts.


444 
\begin{enumerate}


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


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


447 
\item Get sufficiently acquainted with Isabelle/Isar proof


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


449 
to look at existing Isar examples.}


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


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


452 
Isar proof language elements.


453 
\end{enumerate}


454 


455 
Certainly, rewriting formal reasoning in Isar requires additional efforts. On


456 
the other hand, one gains a human readable representation of machinechecked


457 
formal proof. Depending on the context of application, this might be even


458 
indispensable to start with!

9607

459 


460 
%%% Local Variables:


461 
%%% mode: latex


462 
%%% TeXmaster: "isarref"


463 
%%% End:
