# HG changeset patch # User nipkow # Date 762276465 -3600 # Node ID 538db1a98ba3315d2c17f897ebf94aa0bf84244f # Parent 0f6270bb9fe914407fb9106044a50a0ad9c64d50 *** empty log message *** diff -r 0f6270bb9fe9 -r 538db1a98ba3 doc-src/Ref/theories.tex --- 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 + Chapter~\ref{LoadingTheories} for details. +\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 about their files. If it finds that the theory to be loaded was already read 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 -use_thy} to read a modified theory. This function reloads all changed -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