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 old-style theory files to new-style 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 new-style 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 old-style theories used to emit many ML bindings to theorems (and
|
|
36 |
theories), this is no longer done for new-style 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 old-style theories was to bind any theorem as an ML value
|
|
45 |
as well. New-style 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 |
Old-style 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 new-style 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 well-behaved in storing theorems properly within
|
|
70 |
the current theory context, in order to enable new-style 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 ad-hoc 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 ill-behaved 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 new-style 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 |
New-style 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 old-style 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 |
new-style theories (see also \cite{isabelle-system}). 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 new-style 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 non-ASCII 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:axms-thms}).
|
|
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:conv-goal}
|
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:conv-tac}
|
|
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{isabelle-ref} 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 higher-order rules;
|
|
196 |
|
|
197 |
|
|
198 |
\subsection{Tactics vs.\ proof methods}\label{sec:conv-tac}
|
|
199 |
|
|
200 |
Proof methods closely resemble traditional tactics, when used in unstructured
|
|
201 |
sequences of $\isarkeyword{apply}$ commands (cf.\ \S\ref{sec:conv-goal}).
|
|
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 |
Well-structured 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 old-style 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 ad-hoc operations}
|
|
236 |
|
9607
|
237 |
|
|
238 |
|
10111
|
239 |
%\section{Performing actual proof}
|
|
240 |
%FIXME
|
9607
|
241 |
|
|
242 |
%%% Local Variables:
|
|
243 |
%%% mode: latex
|
|
244 |
%%% TeX-master: "isar-ref"
|
|
245 |
%%% End:
|