author nipkow Sat, 26 Feb 1994 16:27:45 +0100 changeset 273 538db1a98ba3 parent 272 0f6270bb9fe9 child 274 dc87495814d5
*** empty log message ***
 doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/theories.tex	Mon Feb 21 14:50:48 1994 +0100
+++ b/doc-src/Ref/theories.tex	Sat Feb 26 16:27:45 1994 +0100
@@ -27,114 +27,82 @@
\label{DefiningTheories}

Theories can be defined either using concrete syntax or by calling certain
-\ML-functions (see \S\ref{BuildingATheory}).  Figure~\ref{TheorySyntax}
-presents the concrete syntax for theories.  This grammar employs the
+\ML-functions (see \S\ref{BuildingATheory}).  Appendix~\ref{TheorySyntax}
+presents the concrete syntax for theories.
+This grammar employs the
following conventions:
\begin{itemize}
-\item Identifiers such as $theoryDef$ denote nonterminal symbols.
+\item Identifiers such as {\it theoryDef} denote nonterminal symbols.
\item Text in {\tt typewriter font} denotes terminal symbols.
-\item \ldots{} indicates repetition of a phrase.
-\item A vertical bar~($|$) separates alternative phrases.
-\item Square [brackets] enclose optional phrases.
-\item $id$ stands for an Isabelle identifier.
-\item $string$ stands for an ML string, with its quotation marks.
-\item $k$ stands for a natural number.
+\item $id$ is an Isabelle identifier.
+\item $string$ is an ML string, with its quotation marks.
+\item $nat$ is for a natural number.
+\item $tfree$ is an Isabelle type variable, i.e.\ an identifier starting with
+  a prime.
\item $text$ stands for arbitrary ML text.
\end{itemize}
-
-\begin{figure}[hp]
-\begin{center}
-\begin{tabular}{rclc}
-$theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$
-                            [{\tt+} $extension$]\\\\
-$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
-                [$trans$] [$rules$] {\tt end} [$ml$]\\\\
-$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
-$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
-$default$ &=& \ttindex{default} $sort$ \\\\
-$sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\
-$name$ &=& $id$ ~~$|$~~ $string$ \\\\
-$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\
-$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$
-               [{\tt(} $infix$ {\tt)}] \\\\
-$infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\
-$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\
-$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\
-$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\
-$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\
-$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$
-                [{\tt(} $mixfix$ {\tt)}] \\\\
-$mixfix$ &=& $string$
-             [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
-       &$|$& $infix$ \\
-       &$|$& \ttindex{binder} $string$ $k$\\\\
-$trans$ &=& \ttindex{translations} $transDecl$ \dots $transDecl$ \\\\
-$transDecl$ &=& [ {\tt(}$string${\tt)} ] $string$
-  [ {\tt=>} $|$ {\tt<=} $|$ {\tt==} ] [ ($string$) ] $string$ \\\\
-$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
-$rule$ &=& $id$ $string$ \\\\
-$ml$ &=& \ttindex{ML} $text$
-\end{tabular}
-\end{center}
-\caption{Theory Syntax}
-\label{TheorySyntax}
-\end{figure}
-
The different parts of a theory definition are interpreted as follows:
\begin{description}
-\item[$theoryDef$] A theory has a name $id$ and is an
-  extension of the union of theories $name@1$ \dots $name@n$ with new
-  classes, types, constants, syntax and axioms. The basic theory, which
-  contains only the meta-logic, is called {\tt Pure}.
+\item[{\it theoryDef}] A theory has a name $id$ and is an extension of the
+  union of theories {\it name}, the {\em parent theories}, with new classes,
+  types, constants, syntax and axioms.  The basic theory, which contains only
+  the meta-logic, is called {\tt Pure}.

-  If $name@i$ is a string, then theory $name@i$ is {\em not} used in building
-  the base of theory $id$. Strings stand for ML-files rather than
-  theory-files and document the dependence if $id$ on additional files. This
-  is required because $name@1$ \dots $name@n$ are loaded automatically when
-  theory $id$ is (re)built. See Chapter~\ref{LoadingTheories} for details.
-\item[$class$] The new class $id$ is declared as a subclass of existing
-  classes $id@1$ \dots $id@n$.  This rules out cyclic class structures.
-  Isabelle automatically computes the transitive closure of subclass
-  hierarchies.  Hence it is not necessary to declare $c@1 < c@3$ in addition
-  to $c@1 < c@2$ and $c@2 < c@3$.
+  If {\it name} is a string, then theory {\it name} is {\em not} used in
+  building the base of theory $id$. Strings stand for ML-files rather than
+  theory-files and document the dependence of $id$ on additional files. This
+  enables all required files, namely those corresponding to {\it name}s, to
+  be loaded automatically when theory $id$ is (re)built. See
+\item[$classes$] {\tt$id$ < $id@1$ \dots\ $id@n$} declares $id$ as a subclass
+  of existing classes $id@1\dots id@n$.  This rules out cyclic class
+  structures.  Isabelle automatically computes the transitive closure of
+  subclass hierarchies.  Hence it is not necessary to declare {\tt c < e} in
+  addition to {\tt c < d} and {\tt d < e}.
\item[$default$] introduces $sort$ as the new default sort for type
variables.  Unconstrained type variables in an input string are
automatically constrained by $sort$; this does not apply to type variables
-  created internally during type inference.  If omitted,
-  the default sort is the same as in the parent theory.
-\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class
-  $id$ abbreviates the singleton set {\tt\{}$id${\tt\}}.
-\item[$name$] is either an alphanumeric identifier or an arbitrary string.
-\item[$typeDecl$] Each $name$ is declared as a new type constructor with
-  $k$ arguments.  Only binary type constructors can have infix status and
-  symbolic names ($string$).
+  created internally during type inference.  If omitted, the default sort is
+  the union of the default sorts of the parent theories.
+\item[$sort$] is a finite set of classes; a single class $id$ abbreviates the
+  singleton set {\tt\{}$id${\tt\}}.
+\item[$type$] is either the declaration of a new type (constructor) or type
+  synonym $name$. Only binary type constructors can have infix status and
+  symbolic names, e.g.\ {\tt ('a,'b)"+"}. Type constructors of $n$ arguments
+  are declared by {\tt ($\alpha@1$,\dots,$\alpha@n$)$name$}.  Type
+  synonyms\indexbold{type!synonym} are defined as in ML, except that the
+  right-hand side must be enclosed in quotation marks.
\item[$infix$] declares a type or constant to be an infix operator of
-  precedence $k$ associating to the left ({\tt infixl}) or right ({\tt
+  precedence $nat$ associating to the left ({\tt infixl}) or right ({\tt
infixr}).
-\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$
-  is given the additional arity $arity$.
-\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to
-  be of type $string$.  For display purposes they can be annotated with
-  $mixfix$ declarations.
-\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_}
-  \dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position
-  where the $i$-th argument should go, $k@i$ is the minimum precedence of
-  the $i$-th argument, and $k$ the precedence of the construct.  The list
-  \hbox{\tt[$k@1$, \dots, $k@n$]} is optional.
+\item[$arities$] Each $name$ must be an existing type constructor which is
+  given the additional arity $arity$.
+\item[$constDecl$] Each new constant $name$ is declared to be of type
+  $string$.  For display purposes they can be annotated with $mixfix$
+  declarations.
+\item[$mixfix$] There are three forms of syntactic annotations:
+  \begin{itemize}
+  \item A mixfix template given as a $string$ of the form
+    {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
+    indicates the position where the $i$-th argument should go. The minimal
+    precedence of each argument is given by a list of natural numbers, the
+    precedence of the construct by the following natural number; precedences
+    are optional.

-  Binary constants can be given infix status.
+  \item Binary constants can be given infix status.

-  A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
+  \item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
like $f(F)$; $p$ is the precedence of the construct.
-\item[$transDecl$] Specifies a syntactic translation rule, that is a parse
-  rule ({\tt =>}), a print rule ({\tt <=}), or both ({\tt ==}).
+  \end{itemize}
+\item[$trans$] Specifies syntactic translation rules, that is parse
+  rules ({\tt =>}), print rules ({\tt <=}), or both ({\tt ==}).
\item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
names must be distinct.
\item[$ml$] This final part of a theory consists of ML code,
typically for parse and print translations.
\end{description}
-The $mixfix$, $transDecl$ and $ml$ sections are explained in more detail in
+The $mixfix$, $trans$ and $ml$ sections are explained in more detail in
the {\it Defining Logics} chapter of the {\it Logics} manual.

@@ -193,11 +161,13 @@
\subsection{Filenames and paths}
\indexbold{filenames}

-The files defining the theory must have the lower case name of the theory
-with {\tt".thy"} or {\tt".ML"} appended.  On the other hand
-\ttindex{use_thy}'s parameter has to be the exact theory name.  Optionally
-the name can be preceded by a path to specify the directory where the
-files can be found.  If no path is provided the reference variable
+\begin{warn}
+  The files defining the theory must have the lower case name of the theory
+  with {\tt".thy"} or {\tt".ML"} appended.  On the other hand
+  \ttindex{use_thy}'s parameter has to be the exact theory name.
+\end{warn}
+Optionally the name can be preceded by a path to specify the directory where
+the files can be found.  If no path is provided the reference variable
\ttindexbold{loadpath} is used which contains a list of paths that are
searched in the given order.  After the {\tt".thy"}-file for a theory has
been found, the same path is used to locate the (optional) {\tt".ML"}-file.
@@ -215,24 +185,27 @@
\ttindex{use_thy} keeps track of all loaded theories and stores information
before, the following happens: first the theory's files are searched at the
-place they were located the last time they were read. If they are found, their
-time of last modification is compared to the internal data and {\tt use_thy}
-stops if they are equal. In case the files have been moved, {\tt use_thy}
-searches them the same way a new theory would be searched for.  After all these
-tests have been passed, the theory is reloaded and all theories that depend on
-it (those that have its name in their $theoryDef$) are marked as out-of-date.
-
-As changing a theory often makes it necessary to reload all theories that
-(indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt
-theories and their descendants in the correct order.
+place they were located the last time they were read. If they are found,
+their time of last modification is compared to the internal data and {\tt
+  use_thy} stops if they are equal. In case the files have been moved, {\tt
+  use_thy} searches them the same way a new theory would be searched for.
+After all these tests have been passed, the theory is reloaded and all
+theories that depend on it (those that have its name in their {\it
+  theoryDef}) are marked as out-of-date.
+\begin{warn}
+  Changing a theory on disk often makes it necessary to reload all theories
+  that (indirectly) depend on it. However, {\tt use_thy} reads only one
+  theory, even if some of the parents are out of date. In this case
+  \ttindexbold{update}{\tt()} should be used.  This function reloads {\em all}
+  modified theories and their descendants in the correct order.
+\end{warn}

\subsection{Pseudo theories}
\indexbold{pseudo theories}

-There is a problem with \ttindex{update}: objects created in \ML-files that do
-not belong to a theory (see explanation of $theoryDef$ in
+There is a problem with \ttindex{update}: objects created in \ML-files that
+do not belong to a theory (see explanation of {\it theoryDef} in
\ref{DefiningTheories}).  These files are read manually between {\tt use_thy}
calls and define objects used in different theories.  As {\tt update} only
knows about the theories there still exist objects with references to the old
@@ -244,7 +217,7 @@

Therefore there is a way to link theories and the $orphaned$ \ML-files. The
link from a theory to an \ML-file has been mentioned in
-Chapter~\ref{DefiningTheories} (strings in $theoryDef$).  But to make this
+Chapter~\ref{DefiningTheories} (strings in {\it theoryDef}).  But to make this
work and to establish a link in the opposite direction we need to create a
{\it pseudo theory}.  Let's assume we have an \ML-file named {\tt orphan.ML}
that depends on theory $A$ and is itself used in theory $B$.  To link the