doc-src/IsarRef/pure.tex
changeset 7981 5120a2a15d06
parent 7974 34245feb6e82
child 7987 d9aef93c0e32
     1.1 --- a/doc-src/IsarRef/pure.tex	Sat Oct 30 20:12:23 1999 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Sat Oct 30 20:13:16 1999 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4  \emph{improper commands}.  Some proof methods and attributes introduced later
     1.5  are classified as improper as well.  Improper Isar language elements, which
     1.6  are subsequently marked by $^*$, are often helpful when developing proof
     1.7 -documents, while their use is usually discouraged for the final outcome.
     1.8 -Typical examples are diagnostic commands that print terms or theorems
     1.9 -according to the current context; other commands even emulate old-style
    1.10 -tactical theorem proving, which facilitates porting of legacy proof scripts.
    1.11 +documents, while their use is discouraged for the final outcome.  Typical
    1.12 +examples are diagnostic commands that print terms or theorems according to the
    1.13 +current context; other commands even emulate old-style tactical theorem
    1.14 +proving, which facilitates porting of legacy proof scripts.
    1.15  
    1.16  
    1.17  \section{Theory commands}
    1.18 @@ -33,7 +33,7 @@
    1.19  \end{matharray}
    1.20  
    1.21  Isabelle/Isar ``new-style'' theories are either defined via theory files or
    1.22 -interactively.  Both actual theory specifications and proofs are handled
    1.23 +interactively.  Both theory-level specifications and proofs are handled
    1.24  uniformly --- occasionally definitional mechanisms even require some explicit
    1.25  proof as well.  In contrast, ``old-style'' Isabelle theories support batch
    1.26  processing only, with the proof scripts collected in separate ML files.
    1.27 @@ -67,23 +67,24 @@
    1.28    produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
    1.29    \S\ref{sec:markup-prf} for further markup commands.
    1.30    
    1.31 -\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
    1.32 -  existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader system ensures
    1.33 -  that any of the base theories are properly loaded (and fully up-to-date when
    1.34 -  $\THEORY$ is executed interactively).  The optional $\isarkeyword{files}$
    1.35 -  specification declares additional dependencies on ML files.  Unless put in
    1.36 -  parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see
    1.37 -  also \S\ref{sec:ML}).  The optional ML file \texttt{$A$.ML} that may be
    1.38 -  associated with any theory should \emph{not} be included in
    1.39 -  $\isarkeyword{files}$.
    1.40 +\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$
    1.41 +  based on existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader
    1.42 +  system ensures that any of the base theories are properly loaded (and fully
    1.43 +  up-to-date when $\THEORY$ is executed interactively).  The optional
    1.44 +  $\isarkeyword{files}$ specification declares additional dependencies on ML
    1.45 +  files.  Unless put in parentheses, any file will be loaded immediately via
    1.46 +  $\isarcmd{use}$ (see also \S\ref{sec:ML}).  The optional ML file
    1.47 +  \texttt{$A$.ML} that may be associated with any theory should \emph{not} be
    1.48 +  included in $\isarkeyword{files}$, though.
    1.49    
    1.50  \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
    1.51 -  mode, so only a limited set of commands may be performed.  Just as for
    1.52 -  $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
    1.53 +  mode, so only a limited set of commands may be performed without destroying
    1.54 +  the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
    1.55 +  loaded and up-to-date.
    1.56    
    1.57  \item [$\END$] concludes the current theory definition or context switch.
    1.58 -  Note that this command cannot be undone, instead the whole theory definition
    1.59 -  has to be retracted.
    1.60 +Note that this command cannot be undone, but the whole theory definition has
    1.61 +to be retracted.
    1.62  \end{descr}
    1.63  
    1.64  
    1.65 @@ -101,7 +102,7 @@
    1.66  \end{matharray}
    1.67  
    1.68  Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
    1.69 -another way to insert text into the document generated from a theory (see
    1.70 +a structured way to insert text into the document generated from a theory (see
    1.71  \cite{isabelle-sys} for more information on Isabelle's document preparation
    1.72  tools).
    1.73  
    1.74 @@ -127,16 +128,16 @@
    1.75    becomes available.  A typical application would be to emit
    1.76    \verb,\begin{comment}, and \verb,\end{comment}, commands to exclude certain
    1.77    parts from the final document.\footnote{This requires the \texttt{comment}
    1.78 -    {\LaTeX} package to be included}
    1.79 +    package to be included in {\LaTeX}.}
    1.80  \end{descr}
    1.81  
    1.82  Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
    1.83 -macro with the name derived from \verb,\isamarkup, (e.g.\ 
    1.84 +macro with the name prefixed by \verb,\isamarkup, (e.g.\ 
    1.85  \verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
    1.86 -argument is passed to that macro unchanged, i.e.\ any {\LaTeX} commands may be
    1.87 -included here.
    1.88 +argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands
    1.89 +may be included here as well.
    1.90  
    1.91 -\medskip Further markup commands are available for proofs (see
    1.92 +\medskip Additional markup commands are available for proofs (see
    1.93  \S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
    1.94  declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
    1.95  elements just preceding the actual theory definition.
    1.96 @@ -199,8 +200,7 @@
    1.97    $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
    1.98    as are available in Isabelle/HOL for example, type synonyms are just purely
    1.99    syntactic abbreviations without any logical significance.  Internally, type
   1.100 -  synonyms are fully expanded, as may be observed when printing terms or
   1.101 -  theorems.
   1.102 +  synonyms are fully expanded.
   1.103  \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
   1.104    $t$, intended as an actual logical type.  Note that object-logics such as
   1.105    Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
   1.106 @@ -214,7 +214,7 @@
   1.107  \end{descr}
   1.108  
   1.109  
   1.110 -\subsection{Constants and simple definitions}
   1.111 +\subsection{Constants and simple definitions}\label{sec:consts}
   1.112  
   1.113  \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
   1.114  \begin{matharray}{rcl}
   1.115 @@ -248,7 +248,7 @@
   1.116  \end{descr}
   1.117  
   1.118  
   1.119 -\subsection{Syntax and translations}
   1.120 +\subsection{Syntax and translations}\label{sec:syn-trans}
   1.121  
   1.122  \indexisarcmd{syntax}\indexisarcmd{translations}
   1.123  \begin{matharray}{rcl}
   1.124 @@ -274,7 +274,7 @@
   1.125    \texttt{output} flag given, all productions are added both to the input and
   1.126    output grammar.
   1.127  \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
   1.128 -  rules (i.e.\ \emph{macros}): parse/print rules (\texttt{==}), parse rules
   1.129 +  rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
   1.130    (\texttt{=>}), or print rules (\texttt{<=}).  Translation patterns may be
   1.131    prefixed by the syntactic category to be used for parsing; the default is
   1.132    \texttt{logic}.
   1.133 @@ -306,7 +306,7 @@
   1.134    Everyday work is typically done the hard way, with proper definitions and
   1.135    actual theorems.
   1.136  \item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
   1.137 -  Typical applications would also involve attributes, to augment the default
   1.138 +  Typical applications would also involve attributes, to augment the
   1.139    Simplifier context, for example.
   1.140  \item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
   1.141    tags the results as ``lemma''.
   1.142 @@ -358,7 +358,7 @@
   1.143  \begin{descr}
   1.144  \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
   1.145    The current theory context (if present) is passed down to the ML session,
   1.146 -  but must not be modified.  Furthermore, the file name is checked with the
   1.147 +  but may not be modified.  Furthermore, the file name is checked with the
   1.148    $\isarkeyword{files}$ dependency declaration given in the theory header (see
   1.149    also \S\ref{sec:begin-thy}).
   1.150    
   1.151 @@ -370,32 +370,33 @@
   1.152    afterwards.  Thus $text$ may actually change the theory as a side effect.
   1.153    
   1.154  \item [$\isarkeyword{setup}~text$] changes the current theory context by
   1.155 -  applying setup functions from $text$, which has to refer to an ML expression
   1.156 -  of type $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is
   1.157 -  the canonical way to initialize object-logic specific tools and packages
   1.158 -  written in ML.
   1.159 +  applying setup functions from $text$, which refers to an ML expression of
   1.160 +  type $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the
   1.161 +  canonical way to initialize object-logic specific tools and packages written
   1.162 +  in ML.
   1.163  \end{descr}
   1.164  
   1.165  
   1.166 -\subsection{Syntax translation functions}
   1.167 +%FIXME remove!?
   1.168 +%\subsection{Syntax translation functions}
   1.169  
   1.170 -\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
   1.171 -\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
   1.172 -\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
   1.173 -\begin{matharray}{rcl}
   1.174 -  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
   1.175 -  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
   1.176 -  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
   1.177 -  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
   1.178 -  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
   1.179 -  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
   1.180 -\end{matharray}
   1.181 +%\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
   1.182 +%\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
   1.183 +%\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
   1.184 +%\begin{matharray}{rcl}
   1.185 +%  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
   1.186 +%  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
   1.187 +%  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
   1.188 +%  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
   1.189 +%  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
   1.190 +%  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
   1.191 +%\end{matharray}
   1.192  
   1.193 -Syntax translation functions written in ML admit almost arbitrary
   1.194 -manipulations of Isabelle's inner syntax.  Any of the above commands have a
   1.195 -single \railqtoken{text} argument that refers to an ML expression of
   1.196 -appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
   1.197 -transformations.
   1.198 +%Syntax translation functions written in ML admit almost arbitrary
   1.199 +%manipulations of Isabelle's inner syntax.  Any of the above commands have a
   1.200 +%single \railqtoken{text} argument that refers to an ML expression of
   1.201 +%appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
   1.202 +%transformations.
   1.203  
   1.204  
   1.205  \subsection{Oracles}