# HG changeset patch # User clasohm # Date 753980616 -3600 # Node ID 9ba8bff1addca05c25b863320318b1be2f11dc70 # Parent ad5414f5540cebcddf393811a4c4eceaf215a3d7 added chapter "Defining Theories" and made changes for new Readthy functions diff -r ad5414f5540c -r 9ba8bff1addc doc-src/Ref/introduction.tex --- 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} diff -r ad5414f5540c -r 9ba8bff1addc doc-src/Ref/ref.toc --- 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} diff -r ad5414f5540c -r 9ba8bff1addc doc-src/Ref/theories.tex --- 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}