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


5 
with old Isabelle ML proof scripts and new Isabelle/Isar theories. There are


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.


10 
\item Manually port oldstyle theory files to newstyle ones (very easy), and


11 
ML proof 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).


14 
\end{enumerate}


15 


16 

9607

17 
\section{No conversion}


18 

10111

19 
Internally, Isabelle handles both old and newstyle theories at the same time;


20 
the theory loader automatically detects the input format. In any case, this


21 
results in certain internal ML values of type \texttt{theory} and


22 
\texttt{thm}. These may be accessed from either the classic or Isar version,


23 
provided that some minimal care is taken.


24 


25 
\subsection{Referring to theorem and theory values}


26 


27 
\begin{ttbox}


28 
thm : xstring > thm


29 
thms : xstring > thm list


30 
the_context : unit > theory


31 
theory : string > theory


32 
\end{ttbox}


33 


34 
These above functions provide general means to refer to logical objects from


35 
ML. While oldstyle theories used to emit many ML bindings to theorems (and


36 
theories), this is no longer done for newstyle Isabelle/Isar theories.


37 
Nevertheless, it is often more appropriate to use these explicit functions in


38 
any case, even if referring to old theories.


39 


40 
\begin{descr}


41 
\item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored


42 
in the current theory context, including any ancestor node.


43 


44 
The convention of oldstyle theories was to bind any theorem as an ML value


45 
as well. Newstyle theories no longer do this, so ML code may have to use


46 
\texttt{thm~"foo"} rather than just \texttt{foo}.


47 


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


49 


50 
Oldstyle theories often use the ML binding \texttt{thy}, which is


51 
dynamically created as part of producing ML code out of the theory source.


52 


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


54 
theory loader database.


55 


56 
The ML code generated from old style theories would include an ML binding


57 
$name\mathtt{.thy}$ as part of an ML structure.


58 
\end{descr}


59 


60 


61 
\subsection{Enabling newstyle theories to retrieve theory values}


62 


63 
\begin{ttbox}


64 
qed : string > unit


65 
bind_thm : string * thm > unit


66 
bind_thms : string * thm list > unit


67 
\end{ttbox}


68 


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


70 
the current theory context, in order to enable newstyle theories to retrieve


71 
these these later.


72 


73 
\begin{descr}


74 
\item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in


75 
ML. This already manages entry in the theorem database of the current


76 
theory context.


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


78 
store theorems that are produced in ML in an adhoc manner.


79 


80 
Note that the original ``LCF'' system approach of binding theorem values on


81 
the ML toplevel only has long been given up in Isabelle. Nevertheless,


82 
legacy proof scripts may occasionally contain illbehaved code like this:


83 
\texttt{val foo = result();} So far, this form did not give any immediate


84 
feedback that there is something wrong, apart from theorems missing in the


85 
WWW presentation, for example. Now it prevents such theorems to be referred


86 
from newstyle theories.


87 
\end{descr}


88 


89 


90 
\subsection{Providing legacy ML bindings}


91 


92 
\begin{matharray}{rcl}


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


94 
\end{matharray}


95 


96 
Newstyle theories may provide ML bindings to accommodate legacy ML scripts as


97 
follows.


98 
\[


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


100 
\]


101 
Note that this command cannot be undone; invalid theorem bindings in ML may


102 
persist.


103 


104 
By providing an oldstyle ML binding in the way that legacy proof scripts


105 
usually expect, one may avoid to change all occurrences of a \texttt{foo}


106 
reference into \texttt{thm~"foo"}.

9607

107 


108 


109 
\section{Porting proof scripts}


110 

10111

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


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


113 
\cite{proofgeneral} for Isabelle/Isar is more robust and more comfortable than


114 
the classic Isabelle version. This is due to the fact that the generic ML


115 
toplevel has been replaced by the new Isar interaction loop, with full control


116 
over input synchronization and errors.


117 


118 
Furthermore, the Isabelle document preparation system only properly with


119 
newstyle theories (see also \cite{isabellesystem}). There is only very


120 
basic document output of the plain sources of legacy theories, lacking


121 
theorems and proof scripts. Proper document markup is only available for


122 
Isabelle/Isar theories.


123 


124 


125 
\subsection{Theory syntax}


126 


127 
Basically, the newstyle Isabelle/Isar theory syntax is a proper superset of


128 
the old one. Only a few quirks and legacy problems have been eliminated,


129 
resulting in simpler rules with less exceptions.


130 


131 
\medskip The main differences in the new syntax are as follows.


132 
\begin{itemize}


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


134 
concerned; this usually requires proper quoting of input strings.


135 


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


137 
require less quoting. This has caused too many strange effects and is no


138 
longer supported.


139 


140 
Note that quotes are \emph{not} required for simple atomic terms, such as


141 
plain identifiers (e.g.\ $x$), numerals (e.g.\ $1$), or nonASCII symbols


142 
(e.g.\ $\forall$, which is input as \verb,\<forall>,).


143 
\item Every name may be quoted, if required. The old syntax would


144 
occasionally demand plain identifiers vs.\ quoted strings to accommodate


145 
certain (discontinued) syntactic features.


146 
\item Theorem declarations now require an explicit colon to separate the name


147 
and the statement (e.g.\ see the syntax of $\DEFS$ in \S\ref{sec:consts}, or


148 
$\THEOREMNAME$ in \S\ref{sec:axmsthms}).


149 
\end{itemize}


150 


151 
Isabelle/Isar error messages are usually quite explicit about the problem, so


152 
doubtful cases of syntax may as well just tried interactively.


153 


154 


155 
\subsection{Basic goal statements}\label{sec:convgoal}

9798

156 

10111

157 
In ML scripts, the canonical a goal statement with completed proof script is


158 
as follows.


159 
\begin{ttbox}


160 
Goal "\(\phi\)";


161 
by \(tac@1\);


162 
\(\vdots\);


163 
by \(tac@n\);


164 
qed "\(name\)";


165 
\end{ttbox}


166 


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


168 
\begin{matharray}{l}


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


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


171 
\quad \vdots \\


172 
\quad \isarkeyword{apply}~meth@n \\


173 
\quad \isarkeyword{done} \\


174 
\end{matharray}


175 


176 
The main statement may be $\THEOREMNAME$ as well. See \S\ref{sec:convtac}


177 
for further details on how to convert actual tactic expressions into proof


178 
methods.


179 


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


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


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


183 
script.


184 
\begin{ttbox}


185 
Goalw [defs] "\(\phi\)";


186 
\(\vdots\)


187 
\end{ttbox}


188 
This may be replaced by an explicit invocation of the $unfold$ proof method.


189 
\begin{matharray}{l}


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


191 
\quad \isarkeyword{apply}~(unfold~defs) \\


192 
\quad \vdots \\


193 
\end{matharray}


194 


195 
%FIXME "goal" and higherorder rules;


196 


197 


198 
\subsection{Tactics vs.\ proof methods}\label{sec:convtac}


199 


200 
Proof methods closely resemble traditional tactics, when used in unstructured


201 
sequences of $\isarkeyword{apply}$ commands (cf.\ \S\ref{sec:convgoal}).


202 
Unlike tactics, proof methods provide proper concrete syntax for additional


203 
arguments, options, and modifiers. Thus a typical method text is usually more


204 
concise than the corresponding tactic expression in ML.


205 


206 
Wellstructured Isar proof texts usually demand much less diverse methods than


207 
traditional proof scripts, so basically a few methods would be sufficient.


208 
Isabelle/Isar provides emulations for any major ML tactic of classic Isabelle,


209 
mostly for the sake of easy porting of existing developments. Nevertheless,


210 
the Isar versions often cover several oldstyle tactics by a single method.


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


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


213 
including concrete syntax for augmenting the Simplifier context (the current


214 
``simpset'').


215 


216 
\bigskip


217 


218 
FIXME

9798

219 


220 
\begin{matharray}{llll}


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


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


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


224 
rule_tac~x@1 = t@1~\dots~x@n = t@n~\textrm{in}~a \\


225 


226 
% \texttt{} & & \\


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


228 
\texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\

9846

229 
\texttt{split_all_tac} & & simp~(no_asm_simp)~only:~split_tupled_all & \Text{(HOL)} \\


230 
& \approx & simp~only:~split_tupled_all & \Text{(HOL)} \\

9819

231 
& \ll & clarify & \Text{(HOL)} \\

9798

232 
\end{matharray}


233 


234 

10111

235 
\subsection{Declarations and adhoc operations}


236 

9607

237 


238 

10111

239 
%\section{Performing actual proof}


240 
%FIXME

9607

241 


242 
%%% Local Variables:


243 
%%% mode: latex


244 
%%% TeXmaster: "isarref"


245 
%%% End:
