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