added chapter "Defining Theories" and made changes for new Readthy functions
Mon, 22 Nov 1993 16:03:36 +0100
changeset 138 9ba8bff1addc
parent 137 ad5414f5540c
child 139 4f83c0a0c3f4
added chapter "Defining Theories" and made changes for new Readthy functions
--- 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}
-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
 \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.
--- 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 @@
-$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 @@
 The different parts of a theory definition are interpreted as follows:
-\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}.
+\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}
+\subsection{Reading a new theory}
 use_thy: string -> unit
 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
+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
+\begin{center} \tt
+Attempt to merge different versions of theory: $T$
+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
+orphan = A
+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
+structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
+open Readthy;
+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}