--- a/doc-src/Ref/introduction.tex Mon Nov 22 12:08:45 1993 +0100
+++ b/doc-src/Ref/introduction.tex Mon Nov 22 16:03:36 1993 +0100
@@ -88,11 +88,15 @@
\section{Reading files of proofs and theories}
\index{files, reading|bold}
\begin{ttbox}
-cd : string -> unit
-use : string -> unit
-use_thy : string -> unit
-time_use : string -> unit
-time_use_thy : string -> unit
+cd : string -> unit
+use : string -> unit
+use_thy : string -> unit
+time_use : string -> unit
+time_use_thy : string -> unit
+update : unit -> unit
+unlink_thy : string -> unit
+loadpath : string list ref
+delete_tmpfiles : bool ref
\end{ttbox}
\begin{description}
\item[\ttindexbold{cd} \tt"{\it dir}";] changes to {\it dir\/} the default
@@ -104,14 +108,33 @@
\item[\ttindexbold{use_thy} \tt"$tname$";]
reads a theory definition from file {\it tname}{\tt.thy} and also reads
-{\ML} commands from the file {\it tname}{\tt.ML}, if it exists. See
-Chapter~\ref{theories} for details.
+{\ML} commands from the file {\it tname}{\tt.ML}, if it exists. If theory
+{\it tname} depends on theories that haven't been read already these are
+loaded automatically.
+See Chapter~\ref{theories} for details.
\item[\ttindexbold{time_use} \tt"$file$";]
performs {\tt use~"$file$"} and prints the total execution time.
\item[\ttindexbold{time_use_thy} \tt"$tname$";]
performs {\tt use_thy "$tname$"} and prints the total execution time.
+
+\item[\ttindexbold{update} \tt();]
+reads all theories that have changed since the last time they have been read.
+See Chapter~\ref{theories} for details.
+
+\item[\ttindexbold{unlink_thy} \tt"$tname$";]
+removes theory {\it tname} from internal list of theory dependencies and has to
+be used after removing a theory's files. Else {\tt update} would keep on
+searching for them. See Chapter~\ref{theories} for details.
+
+\item[\ttindexbold{loadpath}] contains a list of paths that is used by
+{\tt use_thy} and {\tt update} to find {\it tname}{\tt.ML} and {\it tname}
+{\tt.thy}. See Chapter~\ref{theories} for details.
+
+\item[\ttindexbold{delete_tmpfiles}] is used by use_thy and controls the
+removal of temporary files created during the reading of {\it tname}{\tt.thy}.
+See Chapter~\ref{theories} for details.
\end{description}
--- a/doc-src/Ref/ref.toc Mon Nov 22 12:08:45 1993 +0100
+++ b/doc-src/Ref/ref.toc Mon Nov 22 16:03:36 1993 +0100
@@ -2,13 +2,13 @@
\contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1}
\contentsline {section}{\numberline {1.2}Ending a session}{2}
\contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2}
-\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{2}
+\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3}
\contentsline {subsection}{Printing limits}{3}
\contentsline {subsection}{Printing of meta-level hypotheses}{3}
-\contentsline {subsection}{Printing of types and sorts}{3}
-\contentsline {subsection}{$\eta $-contraction before printing}{3}
+\contentsline {subsection}{Printing of types and sorts}{4}
+\contentsline {subsection}{$\eta $-contraction before printing}{4}
\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4}
-\contentsline {section}{\numberline {1.6}Shell scripts}{4}
+\contentsline {section}{\numberline {1.6}Shell scripts}{5}
\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6}
\contentsline {section}{\numberline {2.1}Basic commands}{6}
\contentsline {subsection}{Starting a backward proof}{6}
@@ -105,39 +105,46 @@
\contentsline {subsection}{Other meta-rules}{42}
\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44}
\contentsline {section}{\numberline {6.1}Defining Theories}{44}
-\contentsline {section}{\numberline {6.2}Basic operations on theories}{47}
-\contentsline {subsection}{Extracting an axiom from a theory}{47}
-\contentsline {subsection}{Building a theory}{47}
-\contentsline {subsection}{Inspecting a theory}{48}
-\contentsline {section}{\numberline {6.3}Terms}{49}
-\contentsline {section}{\numberline {6.4}Certified terms}{50}
-\contentsline {subsection}{Printing terms}{50}
-\contentsline {subsection}{Making and inspecting certified terms}{50}
-\contentsline {section}{\numberline {6.5}Types}{51}
-\contentsline {section}{\numberline {6.6}Certified types}{51}
-\contentsline {subsection}{Printing types}{51}
-\contentsline {subsection}{Making and inspecting certified types}{51}
-\contentsline {chapter}{\numberline {7}Substitution Tactics}{53}
-\contentsline {section}{\numberline {7.1}Simple substitution}{53}
-\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{54}
-\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{54}
-\contentsline {chapter}{\numberline {8}Simplification}{57}
-\contentsline {section}{\numberline {8.1}Simplification sets}{57}
-\contentsline {subsection}{Rewrite rules}{57}
-\contentsline {subsection}{Congruence rules}{58}
-\contentsline {subsection}{The subgoaler}{58}
-\contentsline {subsection}{The solver}{59}
-\contentsline {subsection}{The looper}{59}
-\contentsline {section}{\numberline {8.2}The simplification tactics}{59}
-\contentsline {section}{\numberline {8.3}Example: using the simplifier}{60}
-\contentsline {chapter}{\numberline {9}The classical theorem prover}{64}
-\contentsline {section}{\numberline {9.1}The sequent calculus}{64}
-\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{65}
-\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{66}
-\contentsline {section}{\numberline {9.4}Classical rule sets}{67}
-\contentsline {section}{\numberline {9.5}The classical tactics}{68}
-\contentsline {subsection}{Single-step tactics}{69}
-\contentsline {subsection}{The automatic tactics}{69}
-\contentsline {subsection}{Other useful tactics}{69}
-\contentsline {subsection}{Creating swapped rules}{70}
-\contentsline {section}{\numberline {9.6}Setting up the classical prover}{70}
+\contentsline {section}{\numberline {6.2}Loading Theories}{47}
+\contentsline {subsection}{Reading a new theory}{47}
+\contentsline {subsection}{Filenames and paths}{47}
+\contentsline {subsection}{Reloading a theory}{47}
+\contentsline {subsection}{Pseudo theories}{48}
+\contentsline {subsection}{Removing a theory}{48}
+\contentsline {subsection}{Using Poly/{\psc ml}}{48}
+\contentsline {section}{\numberline {6.3}Basic operations on theories}{49}
+\contentsline {subsection}{Extracting an axiom from a theory}{49}
+\contentsline {subsection}{Building a theory}{49}
+\contentsline {subsection}{Inspecting a theory}{50}
+\contentsline {section}{\numberline {6.4}Terms}{51}
+\contentsline {section}{\numberline {6.5}Certified terms}{52}
+\contentsline {subsection}{Printing terms}{52}
+\contentsline {subsection}{Making and inspecting certified terms}{52}
+\contentsline {section}{\numberline {6.6}Types}{53}
+\contentsline {section}{\numberline {6.7}Certified types}{53}
+\contentsline {subsection}{Printing types}{53}
+\contentsline {subsection}{Making and inspecting certified types}{53}
+\contentsline {chapter}{\numberline {7}Substitution Tactics}{55}
+\contentsline {section}{\numberline {7.1}Simple substitution}{55}
+\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{56}
+\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{56}
+\contentsline {chapter}{\numberline {8}Simplification}{59}
+\contentsline {section}{\numberline {8.1}Simplification sets}{59}
+\contentsline {subsection}{Rewrite rules}{59}
+\contentsline {subsection}{Congruence rules}{60}
+\contentsline {subsection}{The subgoaler}{60}
+\contentsline {subsection}{The solver}{61}
+\contentsline {subsection}{The looper}{61}
+\contentsline {section}{\numberline {8.2}The simplification tactics}{62}
+\contentsline {section}{\numberline {8.3}Example: using the simplifier}{63}
+\contentsline {chapter}{\numberline {9}The classical theorem prover}{66}
+\contentsline {section}{\numberline {9.1}The sequent calculus}{66}
+\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{67}
+\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{68}
+\contentsline {section}{\numberline {9.4}Classical rule sets}{69}
+\contentsline {section}{\numberline {9.5}The classical tactics}{70}
+\contentsline {subsection}{Single-step tactics}{71}
+\contentsline {subsection}{The automatic tactics}{71}
+\contentsline {subsection}{Other useful tactics}{71}
+\contentsline {subsection}{Creating swapped rules}{72}
+\contentsline {section}{\numberline {9.6}Setting up the classical prover}{72}
--- a/doc-src/Ref/theories.tex Mon Nov 22 12:08:45 1993 +0100
+++ b/doc-src/Ref/theories.tex Mon Nov 22 16:03:36 1993 +0100
@@ -44,7 +44,7 @@
\begin{figure}[hp]
\begin{center}
\begin{tabular}{rclc}
-$theoryDef$ &=& $id$ {\tt=} $id@1$ {\tt+} \dots {\tt+} $id@n$
+$theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$
[{\tt+} $extension$]\\\\
$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
[$rules$] {\tt end} [$ml$]\\\\
@@ -77,11 +77,19 @@
\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 existing theories $id@1$ \dots $id@n$ with new classes, types,
- constants, syntax and axioms. The basic theory, which contains only the
- meta-logic, is called {\tt Pure}.
+\begin{description}
+\item[$theoryDef$] A theory has a name $id$ and is an
+ extension of the union of theories $id@1$ \dots $id@n$ 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 the theory $name@i$ is {\em not} used in building
+ the base of theory $id$. The reason for using strings in $theoryDef$ is that
+ many theories use objects created in a \ML-file that does not belong to a
+ theory itself. Because $name@1$ \dots $name@n$ are loaded automatically a
+ string can be used to specify a file that is needed as a series of
+ \ML{}-declarations but not as a parent for theory $id$. 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
@@ -125,19 +133,128 @@
The $mixfix$ and $ml$ sections are explained in more detail in the {\it
Defining Logics} chapter of the {\it Logics} manual.
+\section{Loading Theories}
+\label{LoadingTheories}
+\subsection{Reading a new theory}
+
\begin{ttbox}
use_thy: string -> unit
\end{ttbox}
+
Each theory definition must reside in a separate file. Let the file {\it
- tf}{\tt.thy} contain the definition of a theory called $TF$ with rules named
-$r@1$ \dots $r@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it tf\/}{\tt"} reads
-file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file {\tt.}{\it
- tf}{\tt.thy.ML}, and reads the latter file. This declares an {\ML}
-structure~$TF$ containing a component {\tt thy} for the new theory
-and components $r@1$ \dots $r@n$ for the rules; it also contains the
-definitions of the {\tt ML} section if any. Then {\tt use_thy}
-reads the file {\it tf}{\tt.ML}, if it exists; this file normally contains
-proofs involving the new theory.
+tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
+theories $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"}{\it
+TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
+{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Any of the parent
+theories that have not been loaded yet are read now by recursive {\tt use_thy}
+calls until either an already loaded theory or {\tt Pure} is reached.
+Therefore one can read a complete logic by just one {\tt use_thy} call if all
+theories are linked appropriatly. Afterwards an {\ML} structure~$TF$
+containing a component {\tt thy} for the new theory and components $r@1$ \dots
+$r@n$ for the rules is declared; it also contains the definitions of the {\tt
+ML} section if any. (Normally {\tt.}{\it tf}{\tt.thy.ML} is deleted now if
+there have occured no errors. In case one wants to have a look at it,
+{\tt delete_tmpfiles := false} can be set before calling {\tt use_thy}.)
+Finally the file {\it tf}{\tt.ML} is read, if it exists; this file normally
+contains proofs involving the new theory.
+
+
+\subsection{Filenames and paths}
+
+The files the theory definition resides in must have the lower case name of
+the theory with ".thy" or ".ML" appended. On the other hand {\tt use_thy}'s
+parameter has to be the exact theory name. Optionally the name can be
+preceeded by a path to specify the directory where the files can be found. If
+no path is provided the reference variable {\tt loadpath} is used which
+contains a list of paths that are searched in the given order. After the
+".thy"-file for a theory has been found the same path is used to locate the
+(optional) ".ML"-file. (You might note that it is also possible to only
+provide a ".ML"- but no ".thy"-file. In this case a \ML{} structure with the
+theory's name has to be created in the ".ML" file. If both the ".thy"-file
+and a structure declaration in the ".ML"-file exist the declaration in the
+latter file is used. See {\tt ZF/ex/llist.ML} for an example.)
+
+
+\subsection{Reloading a theory}
+
+{\tt 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 at 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 as 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 (i.e. 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, {\tt 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.
+
+
+\subsection{Pseudo theories}
+
+There is a problem with {\tt update}: objects created in \ML-files that do not
+belong to a theory (see explanation of $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 theory version
+after the new one has been read. This (most probably) will produce the fatal
+error
+\begin{center} \tt
+Attempt to merge different versions of theory: $T$
+\end{center}
+
+Therefore there is a way to link theories and the $orphaned$ \ML-files. The
+link from a theory to a \ML-file has been mentioned in
+Chapter~\ref{DefiningTheories} (strings in $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 a \ML-file named {\tt orphan.ML} that
+depends on theory $A$ and itself is used in theory $B$. To link the three we
+have to create the file {\tt orphan.thy} containing the line
+\begin{ttbox}
+orphan = A
+\end{ttbox}
+and add {\tt "orphan"} to theory $B$'s $theoryDef$. Creating {\tt orphan.thy}
+is necessary because of two reasons: First it enables automatic loading of
+$orphan$'s parents and second it creates the \ML{}-object {\tt orphan} that
+is needed by {\tt use_thy} (though it is not added to the base of theory $B$).
+If {\tt orphan.ML} depended on no theory then {\tt Pure} would have been used
+instead of {\tt A}.
+
+For an extensive example of how this technique can be used to link over 30
+files and read them by just two {\tt use_thy} calls have a look at the ZF logic.
+
+
+\subsection{Removing a theory}
+
+If a previously read file is removed the {\tt update} function will keep
+on complaining about a missing file. The theory is not automatically removed
+from the internal list to preserve the links to other theories in case one
+forgot to adjust the {\tt loadpath} after moving a file. To manually remove a
+theory use {\tt unlink_thy}.
+
+
+\subsection{Using Poly/\ML}
+
+As the functions for reading theories depend on reference variables one has to
+take into consideration the way Poly/\ML{} handles them. They are only saved
+together with the state if they were declared in the current database. E.g.
+changes made to a reference variable declared in the $Pure$ database are $not$
+saved if made while using a child database. Therefore a new {\tt Readthy}
+structure has to be declared by
+\begin{ttbox}
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+\end{ttbox}
+in every newly created database. This is not necessary if the database is
+created by copying an existent one.
+
+The above declarations are contained in the $Pure$ database, so one could
+simply use e.g. {\tt use_thy} if saving of the reference variables is not
+needed. Also Standard ML of New Jersey does not have this behaviour.
\section{Basic operations on theories}