doc-src/IsarRef/conversion.tex
author haftmann
Fri Dec 29 12:11:04 2006 +0100 (2006-12-29)
changeset 21927 9677abe5d374
parent 13625 ca86e84ce200
permissions -rw-r--r--
added handling for explicit classrel witnesses
     1 
     2 \chapter{Isabelle/Isar conversion guide}\label{ap:conv}
     3 
     4 Subsequently, we give a few practical hints on working in a mixed environment
     5 of 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 \emph{internal} theory and theorem values.
    10 \item Port old-style theory files to new-style ones (very easy), and ML proof
    11   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 
    17 \section{No conversion}
    18 
    19 Internally, Isabelle is able to handle both old and new-style 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 
    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 
    35 These functions provide general means to refer to logical objects from ML.
    36 Old-style theories used to emit many ML bindings of theorems and theories, but
    37 this is no longer done in new-style Isabelle/Isar theories.
    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 old-style theories was to bind any theorem as an ML value
    44   as well.  New-style theories no longer do this, so ML code may require
    45   \texttt{thm~"foo"} rather than just \texttt{foo}.
    46 
    47 \item [$\mathtt{the_context()}$] refers to the current theory context.
    48 
    49   Old-style theories often use the ML binding \texttt{thy}, which is
    50   dynamically created by the ML code generated from old theory source.  This
    51   is no longer the recommended way in any case!  Function \texttt{the_context}
    52   should be used for old scripts as well.
    53 
    54 \item [$\mathtt{theory}~name$] retrieves the named theory from the global
    55   theory-loader database.
    56 
    57   The ML code generated from old-style theories would include an ML binding
    58   $name\mathtt{.thy}$ as part of an ML structure.
    59 \end{descr}
    60 
    61 
    62 \subsection{Storing theorem values}
    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 well-behaved by storing theorems properly within
    71 the current theory context, in order to enable new-style theories to retrieve
    72 these later.
    73 
    74 \begin{descr}
    75 
    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.
    79 
    80 \item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$]
    81   store theorems that have been produced in ML in an ad-hoc manner.
    82 
    83 \end{descr}
    84 
    85 Note that the original ``LCF-system'' approach of binding theorem values on
    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 ill-behaved in several respects.  Apart from preventing
    89 access from Isar theories, it also omits the result from the WWW presentation,
    90 for example.
    91 
    92 
    93 \subsection{ML declarations in Isar}
    94 
    95 \begin{matharray}{rcl}
    96   \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
    97   \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
    98 \end{matharray}
    99 
   100 Isabelle/Isar theories may contain ML declarations as well.  For example, an
   101 old-style theorem binding may be mimicked as follows.
   102 \[
   103 \isarkeyword{ML}~\{*~\mbox{\texttt{val foo = thm "foo"}}~*\}
   104 \]
   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
   107 $\isarkeyword{ML_setup}$ for declarations that act on the current context.
   108 
   109 
   110 \section{Porting theories and proof scripts}\label{sec:port-scripts}
   111 
   112 Porting legacy theory and ML files to proper Isabelle/Isar theories has
   113 several advantages.  For example, the Proof~General user interface
   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.
   118 
   119 Furthermore, the Isabelle document preparation system (see also
   120 \cite{isabelle-sys}) only works properly with new-style theories.  Output of
   121 old-style sources is at the level of individual characters (and symbols),
   122 without proper document markup as in Isabelle/Isar theories.
   123 
   124 
   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.
   131 
   132 \begin{itemize}
   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.
   136 
   137   The old syntax would occasionally demand plain identifiers vs.\ quoted
   138   strings to accommodate certain syntactic features.
   139 \item Types and terms have to be \emph{atomic} as far as the theory syntax is
   140   concerned; this typically requires quoting of input strings, e.g.\ ``$x +
   141   y$''.
   142 
   143   The old theory syntax used to fake part of the syntax of types in order to
   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
   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:axms-thms}.
   151 \end{itemize}
   152 
   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.
   156 
   157 
   158 \subsection{Goal statements}\label{sec:conv-goal}
   159 
   160 \subsubsection{Simple goals}
   161 
   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 tactic-emulation script like this:
   171 \begin{matharray}{l}
   172   \LEMMA{name}{\texttt"{\phi}\texttt"} \\
   173   \quad \APPLY{meth@1} \\
   174   \qquad \vdots \\
   175   \quad \DONE \\
   176 \end{matharray}
   177 Note that the main statement may be $\THEOREMNAME$ or $\COROLLARYNAME$ as
   178 well.  See \S\ref{sec:conv-tac} for further details on how to convert actual
   179 tactic expressions into proof methods.
   180 
   181 \medskip Classic Isabelle provides many variant forms of goal commands, see
   182 also \cite{isabelle-ref} for further details.  The second most common one is
   183 \texttt{Goalw}, which expands definitions before commencing the actual proof
   184 script.
   185 \begin{ttbox}
   186  Goalw [\(def@1\), \(\dots\)] "\(\phi\)";
   187 \end{ttbox}
   188 This may be replaced by using the $unfold$ proof method explicitly.
   189 \begin{matharray}{l}
   190 \LEMMA{name}{\texttt"{\phi}\texttt"} \\
   191 \quad \APPLY{(unfold~def@1~\dots)} \\
   192 \end{matharray}
   193 
   194 
   195 \subsubsection{Deriving rules}
   196 
   197 Deriving non-atomic meta-level 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
   201 are discharged again, resulting in the original rule statement.  The ``long
   202 format'' of Isabelle/Isar goal statements admits to emulate this technique
   203 nicely.  The general ML goal statement for derived rules looks like this:
   204 \begin{ttbox}
   205  val [\(prem@1\), \dots] = goal "\(\phi@1 \Imp \dots \Imp \psi\)";
   206  by \(tac@1\);
   207    \(\vdots\)
   208  qed "\(a\)"
   209 \end{ttbox}
   210 This form may be turned into a tactic-emulation script as follows:
   211 \begin{matharray}{l}
   212   \LEMMA{a}{} \\
   213   \quad \ASSUMES{prem@1}{\texttt"\phi@1\texttt"}~\AND~\dots \\
   214   \quad \SHOWS{}{\texttt"{\psi}\texttt"} \\
   215   \qquad \APPLY{meth@1} \\
   216   \qquad\quad \vdots \\
   217   \qquad \DONE \\
   218 \end{matharray}
   219 
   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
   223 greatly simplified, using one of the standard automated proof tools, such as
   224 $simp$, $blast$, or $auto$.  This could work as follows:
   225 \begin{matharray}{l}
   226   \LEMMA{}{\texttt"{\phi@1 \Imp \dots \Imp \psi}\texttt"} \\
   227   \quad \BYY{(unfold~defs)}{blast} \\
   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 object-logic), 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
   245 attribute ``$rule_format$'', see also \S\ref{sec:object-logic}.  Thus the
   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 object-level 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.
   259 
   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 object-logic 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"} \\
   268   \quad \APPLY{(atomize~(full))} \\
   269   \quad \APPLY{meth@1} \\
   270   \qquad \vdots \\
   271   \quad \DONE \\
   272 \end{matharray}
   273 
   274 In many situations the $atomize$ step above is actually unnecessary,
   275 especially if the subsequent script mainly consists of automated tools.
   276 
   277 
   278 \subsection{Tactics}\label{sec:conv-tac}
   279 
   280 Isar Proof methods closely resemble traditional tactics, when used in
   281 unstructured sequences of $\APPLYNAME$ commands (cf.\ \S\ref{sec:conv-goal}).
   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.
   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
   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},
   293 there is also concrete syntax for augmenting the Simplifier context (the
   294 current ``simpset'') in a convenient way.
   295 
   296 
   297 \subsubsection{Resolution tactics}
   298 
   299 Classic Isabelle provides several variant forms of tactics for single-step
   300 rule applications (based on higher-order resolution).  The space of resolution
   301 tactics has the following main dimensions.
   302 \begin{enumerate}
   303 \item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\
   304   \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac},
   305   \texttt{forward_tac}).
   306 \item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\
   307   \texttt{res_inst_tac}).
   308 \item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\
   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:pure-meth-att}), or any of its
   317 ``improper'' variants $erule$, $drule$, $frule$ (see
   318 \S\ref{sec:misc-meth-att}).  Note that explicit goal addressing is only
   319 supported by the actual $rule_tac$ version.
   320 
   321 With this in mind, plain resolution tactics may be ported as follows.
   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:tactic-commands}).
   336 
   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 
   346 
   347 \subsubsection{Simplifier tactics}
   348 
   349 The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants
   350 (cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$
   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$).
   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) \\
   361   \texttt{Asm_lr_simp_tac 1} & & simp~(asm_lr) \\
   362 \end{matharray}
   363 
   364 Isar also provides separate method modifier syntax for augmenting the
   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:
   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:conv-decls} for more information.
   377 
   378 
   379 \subsubsection{Classical Reasoner tactics}
   380 
   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{isabelle-ref}).  The corresponding Isar
   384 methods usually share the same base name, such as $blast$, $fast$, $clarify$
   385 etc.\ (see \S\ref{sec:classical}).
   386 
   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:conv-decls} 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}
   409   \texttt{stac}~a~1 & & subst~a \\
   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 \\
   415 \end{matharray}
   416 
   417 
   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
   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
   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{isabelle-ref}) 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{isabelle-ref})
   445 are not available in Isar, since there is no direct goal addressing.
   446 Nevertheless, some basic methods address all goals internally, notably
   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.
   450 
   451 \medskip Iterated resolution, such as
   452 \texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed
   453 using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}).
   454 
   455 
   456 \subsection{Declarations and ad-hoc operations}\label{sec:conv-decls}
   457 
   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 ad-hoc 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
   466 ML combinators may be expressed directly in Isar as follows.
   467 \begin{matharray}{lll}
   468   thm@1~\texttt{RS}~thm@2 & & thm@1~[THEN~thm@2] \\
   469   thm@1~\texttt{RSN}~(i, thm@2) & & thm@1~[THEN~[i]~thm@2] \\
   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] \\
   473   \texttt{make_elim}~thm & & thm~[elim_format] \\
   474   \texttt{standard}~thm & & thm~[standard] \\
   475 \end{matharray}
   476 
   477 Note that $OF$ is often more readable as $THEN$; likewise positional
   478 instantiation with $of$ is often more appropriate than $where$.
   479 
   480 The special ML command \texttt{qed_spec_mp} of Isabelle/HOL and FOL may be
   481 replaced by passing the result of a proof through $rule_format$.
   482 
   483 \medskip Global ML declarations may be expressed using the $\DECLARE$ command
   484 (see \S\ref{sec:tactic-commands}) together with appropriate attributes.  The
   485 most common ones are as follows.
   486 \begin{matharray}{lll}
   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] \\
   498 \end{matharray}
   499 Note that explicit $\DECLARE$ commands are rarely needed in practice; Isar
   500 admits to declare theorems on-the-fly wherever they emerge.  Consider the
   501 following ML idiom:
   502 \begin{ttbox}
   503 Goal "\(\phi\)";
   504  \(\vdots\)
   505 qed "name";
   506 Addsimps [name];
   507 \end{ttbox}
   508 This may be expressed more succinctly in Isar like this:
   509 \begin{matharray}{l}
   510   \LEMMA{name~[simp]}{\phi} \\
   511   \quad\vdots
   512 \end{matharray}
   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]$).
   515 
   516 
   517 \section{Writing actual Isar proof texts}
   518 
   519 Porting legacy ML proof scripts into Isar tactic emulation scripts (see
   520 \S\ref{sec:port-scripts}) 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 human-readably Isar
   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 low-level
   527 programming languages (say Assembler) into higher-level ones (say Haskell).
   528 In order to accomplish this, one needs a working knowledge of the target
   529 language, as well an understanding of the \emph{original} idea of the piece of
   530 code expressed in the low-level language.
   531 
   532 As far as Isar proofs are concerned, it is usually much easier to re-use only
   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 re-engineered by tracing forth and backwards,
   537 and by educated guessing!
   538 
   539 \medskip This is a possible schedule to embark on actual conversion of legacy
   540 proof scripts into Isar proof texts.
   541 
   542 \begin{enumerate}
   543 
   544 \item Port ML scripts to Isar tactic emulation scripts (see
   545   \S\ref{sec:port-scripts}).
   546 
   547 \item Get sufficiently acquainted with Isabelle/Isar proof
   548   development.\footnote{As there is still no Isar tutorial around, it is best
   549     to look at existing Isar examples, see also \S\ref{sec:isar-howto}.}
   550 
   551 \item Recover the proof structure of a few important theorems.
   552 
   553 \item Rephrase the original intention of the course of reasoning in terms of
   554   Isar proof language elements.
   555 
   556 \end{enumerate}
   557 
   558 Certainly, rewriting formal reasoning in Isar requires some additional effort.
   559 On the other hand, one gains a human-readable representation of
   560 machine-checked formal proof.  Depending on the context of application, this
   561 might be even indispensable to start with!
   562 
   563 %%% Local Variables:
   564 %%% mode: latex
   565 %%% TeX-master: "isar-ref"
   566 %%% End: