doc-src/IsarRef/Thy/document/Spec.tex
author wenzelm
Thu May 15 17:39:20 2008 +0200 (2008-05-15)
changeset 26902 8db1e960d636
parent 26870 94bedbb34b92
child 27042 8fcf19f2168b
permissions -rw-r--r--
updated generated file;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Spec}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 \isanewline
     8 %
     9 \endisadelimtheory
    10 %
    11 \isatagtheory
    12 \isacommand{theory}\isamarkupfalse%
    13 \ Spec\isanewline
    14 \isakeyword{imports}\ Main\isanewline
    15 \isakeyword{begin}%
    16 \endisatagtheory
    17 {\isafoldtheory}%
    18 %
    19 \isadelimtheory
    20 %
    21 \endisadelimtheory
    22 %
    23 \isamarkupchapter{Specifications%
    24 }
    25 \isamarkuptrue%
    26 %
    27 \isamarkupsection{Defining theories \label{sec:begin-thy}%
    28 }
    29 \isamarkuptrue%
    30 %
    31 \begin{isamarkuptext}%
    32 \begin{matharray}{rcl}
    33     \indexdef{}{command}{header}\hypertarget{command.header}{\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}} & : & \isarkeep{toplevel} \\
    34     \indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isartrans{toplevel}{theory} \\
    35     \indexdef{}{command}{end}\hypertarget{command.end}{\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isartrans{theory}{toplevel} \\
    36   \end{matharray}
    37 
    38   Isabelle/Isar theories are defined via theory, which contain both
    39   specifications and proofs; occasionally definitional mechanisms also
    40   require some explicit proof.
    41 
    42   The first ``real'' command of any theory has to be \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which starts a new theory based on the merge of existing
    43   ones.  Just preceding the \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} keyword, there may be
    44   an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is relevant to
    45   document preparation only; it acts very much like a special
    46   pre-theory markup command (cf.\ \secref{sec:markup-thy} and
    47   \secref{sec:markup-thy}).  The \hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}} command concludes a
    48   theory development; it has to be the very last command of any theory
    49   file loaded in batch-mode.
    50 
    51   \begin{rail}
    52     'header' text
    53     ;
    54     'theory' name 'imports' (name +) uses? 'begin'
    55     ;
    56 
    57     uses: 'uses' ((name | parname) +);
    58   \end{rail}
    59 
    60   \begin{descr}
    61 
    62   \item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
    63   markup just preceding the formal beginning of a theory.  In actual
    64   document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
    65   headings.  See also \secref{sec:markup-thy} and
    66   \secref{sec:markup-prf} for further markup commands.
    67   
    68   \item [\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the
    69   merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
    70   
    71   Due to inclusion of several ancestors, the overall theory structure
    72   emerging in an Isabelle session forms a directed acyclic graph
    73   (DAG).  Isabelle's theory loader ensures that the sources
    74   contributing to the development graph are always up-to-date.
    75   Changed files are automatically reloaded when processing theory
    76   headers.
    77   
    78   The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional
    79   dependencies on extra files (usually ML sources).  Files will be
    80   loaded immediately (as ML), unless the name is put in parentheses,
    81   which merely documents the dependency to be resolved later in the
    82   text (typically via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} in the body text,
    83   see \secref{sec:ML}).
    84   
    85   \item [\hyperlink{command.end}{\mbox{\isa{\isacommand{end}}}}] concludes the current theory definition or
    86   context switch.
    87 
    88   \end{descr}%
    89 \end{isamarkuptext}%
    90 \isamarkuptrue%
    91 %
    92 \isadelimtheory
    93 %
    94 \endisadelimtheory
    95 %
    96 \isatagtheory
    97 \isacommand{end}\isamarkupfalse%
    98 %
    99 \endisatagtheory
   100 {\isafoldtheory}%
   101 %
   102 \isadelimtheory
   103 %
   104 \endisadelimtheory
   105 \isanewline
   106 \end{isabellebody}%
   107 %%% Local Variables:
   108 %%% mode: latex
   109 %%% TeX-master: "root"
   110 %%% End: