1.1 --- a/doc-src/Ref/theories.tex Mon Nov 22 16:03:36 1993 +0100
1.2 +++ b/doc-src/Ref/theories.tex Mon Nov 22 18:26:46 1993 +0100
1.3 @@ -79,17 +79,15 @@
1.4 The different parts of a theory definition are interpreted as follows:
1.5 \begin{description}
1.6 \item[$theoryDef$] A theory has a name $id$ and is an
1.7 - extension of the union of theories $id@1$ \dots $id@n$ with new
1.8 + extension of the union of theories $name@1$ \dots $name@n$ with new
1.9 classes, types, constants, syntax and axioms. The basic theory, which
1.10 contains only the meta-logic, is called {\tt Pure}.
1.11
1.12 - If $name@i$ is a string the theory $name@i$ is {\em not} used in building
1.13 - the base of theory $id$. The reason for using strings in $theoryDef$ is that
1.14 - many theories use objects created in a \ML-file that does not belong to a
1.15 - theory itself. Because $name@1$ \dots $name@n$ are loaded automatically a
1.16 - string can be used to specify a file that is needed as a series of
1.17 - \ML{}-declarations but not as a parent for theory $id$. See
1.18 - Chapter~\ref{LoadingTheories} for details.
1.19 + If $name@i$ is a string, then theory $name@i$ is {\em not} used in building
1.20 + the base of theory $id$. Strings stand for ML-files rather than
1.21 + theory-files and document the dependence if $id$ on additional files. This
1.22 + is required because $name@1$ \dots $name@n$ are loaded automatically when
1.23 + theory $id$ is (re)built. See Chapter~\ref{LoadingTheories} for details.
1.24 \item[$class$] The new class $id$ is declared as a subclass of existing
1.25 classes $id@1$ \dots $id@n$. This rules out cyclic class structures.
1.26 Isabelle automatically computes the transitive closure of subclass
1.27 @@ -140,23 +138,22 @@
1.28 \begin{ttbox}
1.29 use_thy: string -> unit
1.30 \end{ttbox}
1.31 -
1.32 Each theory definition must reside in a separate file. Let the file {\it
1.33 -tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
1.34 + tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
1.35 theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it
1.36 -TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
1.37 + TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
1.38 {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Any of the parent
1.39 -theories that have not been loaded yet are read now by recursive {\tt use_thy}
1.40 -calls until either an already loaded theory or {\tt Pure} is reached.
1.41 -Therefore one can read a complete logic by just one {\tt use_thy} call if all
1.42 -theories are linked appropriatly. Afterwards an {\ML} structure~$TF$
1.43 -containing a component {\tt thy} for the new theory and components $r@1$ \dots
1.44 -$r@n$ for the rules is declared; it also contains the definitions of the {\tt
1.45 -ML} section if any. (Normally {\tt.}{\it tf}{\tt.thy.ML} is deleted now if
1.46 -there have occured no errors. In case one wants to have a look at it,
1.47 -{\tt delete_tmpfiles := false} can be set before calling {\tt use_thy}.)
1.48 -Finally the file {\it tf}{\tt.ML} is read, if it exists; this file normally
1.49 -contains proofs involving the new theory.
1.50 +theories that have not been loaded yet are read now by recursive {\tt
1.51 + use_thy} calls until either an already loaded theory or {\tt Pure} is
1.52 +reached. Therefore one can read a complete logic by just one {\tt use_thy}
1.53 +call if all theories are linked appropriatly. Afterwards an {\ML}
1.54 +structure~$TF$ containing a component {\tt thy} for the new theory and
1.55 +components $r@1$ \dots $r@n$ for the rules is declared; it also contains the
1.56 +definitions of the {\tt ML} section if any. Unless
1.57 +\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it
1.58 + tf}{\tt.thy.ML} is deleted if no errors occured. Finally the file {\it
1.59 + tf}{\tt.ML} is read, if it exists; this file normally contains proofs
1.60 +involving the new theory.
1.61
1.62
1.63 \subsection{Filenames and paths}
1.64 @@ -167,9 +164,9 @@
1.65 preceeded by a path to specify the directory where the files can be found. If
1.66 no path is provided the reference variable {\tt loadpath} is used which
1.67 contains a list of paths that are searched in the given order. After the
1.68 -".thy"-file for a theory has been found the same path is used to locate the
1.69 +".thy"-file for a theory has been found, the same path is used to locate the
1.70 (optional) ".ML"-file. (You might note that it is also possible to only
1.71 -provide a ".ML"- but no ".thy"-file. In this case a \ML{} structure with the
1.72 +provide a ".ML"- but no ".thy"-file. In this case an \ML{} structure with the
1.73 theory's name has to be created in the ".ML" file. If both the ".thy"-file
1.74 and a structure declaration in the ".ML"-file exist the declaration in the
1.75 latter file is used. See {\tt ZF/ex/llist.ML} for an example.)
1.76 @@ -178,15 +175,15 @@
1.77 \subsection{Reloading a theory}
1.78
1.79 {\tt use_thy} keeps track of all loaded theories and stores information about
1.80 -their files. If it finds that the theory to be loaded was already read before
1.81 -the following happens: First the theory's files are searched at the place
1.82 -they were located at the last time they were read. If they are found their
1.83 -time of last modification is compared to the internal data and {\tt use_thy}
1.84 -stops if they are equal. In case the files have been moved, {\tt use_thy}
1.85 -searches them the same way as a new theory would be searched for. After all
1.86 -these tests have been passed the theory is reloaded and all theories that
1.87 -depend on it (i.e. that have its name in their $theoryDef$) are marked as
1.88 -out-of-date.
1.89 +their files. If it finds that the theory to be loaded was already read
1.90 +before, the following happens: First the theory's files are searched at the
1.91 +place they were located the last time they were read. If they are found,
1.92 +their time of last modification is compared to the internal data and {\tt
1.93 + use_thy} stops if they are equal. In case the files have been moved, {\tt
1.94 + use_thy} searches them the same way a new theory would be searched for.
1.95 +After all these tests have been passed, the theory is reloaded and all
1.96 +theories that depend on it (i.e. that have its name in their $theoryDef$) are
1.97 +marked as out-of-date.
1.98
1.99 As changing a theory often makes it necessary to reload all theories that
1.100 (indirectly) depend on it, {\tt update} should be used instead of {\tt
1.101 @@ -208,24 +205,25 @@
1.102 \end{center}
1.103
1.104 Therefore there is a way to link theories and the $orphaned$ \ML-files. The
1.105 -link from a theory to a \ML-file has been mentioned in
1.106 +link from a theory to an \ML-file has been mentioned in
1.107 Chapter~\ref{DefiningTheories} (strings in $theoryDef$). But to make this
1.108 work and to establish a link in the opposite direction we need to create a
1.109 -{\it pseudo theory}. Let's assume we have a \ML-file named {\tt orphan.ML} that
1.110 -depends on theory $A$ and itself is used in theory $B$. To link the three we
1.111 -have to create the file {\tt orphan.thy} containing the line
1.112 +{\it pseudo theory}. Let's assume we have an \ML-file named {\tt orphan.ML}
1.113 +that depends on theory $A$ and is itself used in theory $B$. To link the
1.114 +three we have to create the file {\tt orphan.thy} containing the line
1.115 \begin{ttbox}
1.116 orphan = A
1.117 \end{ttbox}
1.118 -and add {\tt "orphan"} to theory $B$'s $theoryDef$. Creating {\tt orphan.thy}
1.119 -is necessary because of two reasons: First it enables automatic loading of
1.120 -$orphan$'s parents and second it creates the \ML{}-object {\tt orphan} that
1.121 -is needed by {\tt use_thy} (though it is not added to the base of theory $B$).
1.122 -If {\tt orphan.ML} depended on no theory then {\tt Pure} would have been used
1.123 -instead of {\tt A}.
1.124 +and add {\tt "orphan"} to the list of $B$'s parents. Creating {\tt
1.125 + orphan.thy} is necessary because of two reasons: First it enables automatic
1.126 +loading of $orphan$'s parents and second it creates the \ML{}-object {\tt
1.127 + orphan} that is needed by {\tt use_thy} (though it is not added to the base
1.128 +of theory $B$). If {\tt orphan.ML} depended on no theory then {\tt Pure}
1.129 +would have been used instead of {\tt A}.
1.130
1.131 For an extensive example of how this technique can be used to link over 30
1.132 -files and read them by just two {\tt use_thy} calls have a look at the ZF logic.
1.133 +files and read them by just two {\tt use_thy} calls have a look at the ZF
1.134 +logic.
1.135
1.136
1.137 \subsection{Removing a theory}
1.138 @@ -252,9 +250,9 @@
1.139 in every newly created database. This is not necessary if the database is
1.140 created by copying an existent one.
1.141
1.142 -The above declarations are contained in the $Pure$ database, so one could
1.143 -simply use e.g. {\tt use_thy} if saving of the reference variables is not
1.144 -needed. Also Standard ML of New Jersey does not have this behaviour.
1.145 +%The above declarations are contained in the $Pure$ database, so one could
1.146 +%simply use e.g. {\tt use_thy} if saving of the reference variables is not
1.147 +%needed. Standard ML of New Jersey does not have this behaviour.
1.148
1.149
1.150 \section{Basic operations on theories}