diff -r f27cc0a43feb -r 8b2eb3b78cc3 doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Fri Mar 08 15:33:32 2002 +0100 +++ b/doc-src/IsarRef/conversion.tex Fri Mar 08 15:53:15 2002 +0100 @@ -1,5 +1,5 @@ -\chapter{Isabelle/Isar Conversion Guide}\label{ap:conv} +\chapter{Isabelle/Isar conversion guide}\label{ap:conv} Subsequently, we give a few practical hints on working in a mixed environment of old Isabelle ML proof scripts and new Isabelle/Isar theories. There are @@ -39,21 +39,21 @@ \begin{descr} \item [$\mathtt{thm}~name$ and $\mathtt{thms}~name$] retrieve theorems stored in the current theory context, including any ancestor node. - + The convention of old-style theories was to bind any theorem as an ML value as well. New-style theories no longer do this, so ML code may require \texttt{thm~"foo"} rather than just \texttt{foo}. - + \item [$\mathtt{the_context()}$] refers to the current theory context. - + Old-style theories often use the ML binding \texttt{thy}, which is dynamically created by the ML code generated from old theory source. This is no longer the recommended way in any case! Function \texttt{the_context} should be used for old scripts as well. - + \item [$\mathtt{theory}~name$] retrieves the named theory from the global theory-loader database. - + The ML code generated from old-style theories would include an ML binding $name\mathtt{.thy}$ as part of an ML structure. \end{descr} @@ -72,11 +72,11 @@ these later. \begin{descr} - + \item [$\mathtt{qed}~name$] is the canonical way to conclude a proof script in ML. This already manages entry in the theorem database of the current theory context. - + \item [$\mathtt{bind_thm}~(name, thm)$ and $\mathtt{bind_thms}~(name, thms)$] store theorems that have been produced in ML in an ad-hoc manner. @@ -133,13 +133,13 @@ \item Quoted strings may contain arbitrary white space, and span several lines without requiring \verb,\,\,\dots\verb,\, escapes. \item Names may always be quoted. - + The old syntax would occasionally demand plain identifiers vs.\ quoted strings to accommodate certain syntactic features. \item Types and terms have to be \emph{atomic} as far as the theory syntax is concerned; this typically requires quoting of input strings, e.g.\ ``$x + y$''. - + The old theory syntax used to fake part of the syntax of types in order to require less quoting in common cases; this was hard to predict, though. On the other hand, Isar does not require quotes for simple terms, such as plain @@ -300,12 +300,12 @@ rule applications (based on higher-order resolution). The space of resolution tactics has the following main dimensions. \begin{enumerate} -\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\ +\item The ``mode'' of resolution: intro, elim, destruct, or forward (e.g.\ \texttt{resolve_tac}, \texttt{eresolve_tac}, \texttt{dresolve_tac}, \texttt{forward_tac}). -\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\ +\item Optional explicit instantiation (e.g.\ \texttt{resolve_tac} vs.\ \texttt{res_inst_tac}). -\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\ +\item Abbreviations for singleton arguments (e.g.\ \texttt{resolve_tac} vs.\ \texttt{rtac}). \end{enumerate} @@ -348,9 +348,9 @@ The main Simplifier tactics \texttt{Simp_tac}, \texttt{simp_tac} and variants (cf.\ \cite{isabelle-ref}) are all covered by the $simp$ and $simp_all$ -methods (see \S\ref{sec:simp}). Note that there is no individual goal -addressing available, simplification acts either on the first goal ($simp$) -or all goals ($simp_all$). +methods (see \S\ref{sec:simplifier}). Note that there is no individual goal +addressing available, simplification acts either on the first goal ($simp$) or +all goals ($simp_all$). \begin{matharray}{lll} \texttt{Asm_full_simp_tac 1} & & simp \\ @@ -361,8 +361,9 @@ \end{matharray} Isar also provides separate method modifier syntax for augmenting the -Simplifier context (see \S\ref{sec:simp}), which is known as the ``simpset'' -in ML. A typical ML expression with simpset changes looks like this: +Simplifier context (see \S\ref{sec:simplifier}), which is known as the +``simpset'' in ML. A typical ML expression with simpset changes looks like +this: \begin{ttbox} asm_full_simp_tac (simpset () addsimps [\(a@1\), \(\dots\)] delsimps [\(b@1\), \(\dots\)]) 1 \end{ttbox} @@ -380,7 +381,7 @@ automated tactics, such as \texttt{Blast_tac}, \texttt{Fast_tac}, \texttt{Clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding Isar methods usually share the same base name, such as $blast$, $fast$, $clarify$ -etc.\ (see \S\ref{sec:classical-auto}). +etc.\ (see \S\ref{sec:classical}). Similar to the Simplifier, there is separate method modifier syntax for augmenting the Classical Reasoner context, which is known as the ``claset'' in @@ -442,14 +443,13 @@ \medskip \texttt{ALLGOALS}, \texttt{SOMEGOAL} etc.\ (see \cite{isabelle-ref}) are not available in Isar, since there is no direct goal addressing. Nevertheless, some basic methods address all goals internally, notably -$simp_all$ (see \S\ref{sec:simp}). Also note that \texttt{ALLGOALS} may be -often replaced by ``$+$'' (repeat at least once), although this usually has a -different operational behavior, such as solving goals in a different order. +$simp_all$ (see \S\ref{sec:simplifier}). Also note that \texttt{ALLGOALS} may +be often replaced by ``$+$'' (repeat at least once), although this usually has +a different operational behavior, such as solving goals in a different order. \medskip Iterated resolution, such as \texttt{REPEAT~(FIRSTGOAL~(resolve_tac~$\dots$))}, is usually better expressed -using the $intro$ and $elim$ methods of Isar (see -\S\ref{sec:classical-basic}). +using the $intro$ and $elim$ methods of Isar (see \S\ref{sec:classical}). \subsection{Declarations and ad-hoc operations}\label{sec:conv-decls} @@ -559,8 +559,7 @@ machine-checked formal proof. Depending on the context of application, this might be even indispensable to start with! - -%%% Local Variables: +%%% Local Variables: %%% mode: latex %%% TeX-master: "isar-ref" -%%% End: +%%% End: