diff -r 492a3d5d2b17 -r 335efc3f5632 doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Mon May 05 21:18:01 1997 +0200 +++ b/doc-src/Ref/theories.tex Tue May 06 12:50:16 1997 +0200 @@ -2,12 +2,12 @@ \chapter{Theories, Terms and Types} \label{theories} \index{theories|(}\index{signatures|bold} -\index{reading!axioms|see{{\tt assume_ax}}} -Theories organize the syntax, declarations and axioms of a mathematical -development. They are built, starting from the Pure theory, by extending -and merging existing theories. They have the \ML\ type \mltydx{theory}. -Theory operations signal errors by raising exception \xdx{THEORY}, -returning a message and a list of theories. +\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the +syntax, declarations and axioms of a mathematical development. They +are built, starting from the {\Pure} or {\CPure} theory, by extending +and merging existing theories. They have the \ML\ type +\mltydx{theory}. Theory operations signal errors by raising exception +\xdx{THEORY}, returning a message and a list of theories. Signatures, which contain information about sorts, types, constants and syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each @@ -32,11 +32,12 @@ Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory definitions; here is an explanation of the constituent parts: \begin{description} -\item[{\it theoryDef}] - is the full definition. The new theory is called $id$. It is the union - of the named {\bf parent theories}\indexbold{theories!parent}, possibly - extended with new classes, etc. The basic theory, which contains only - the meta-logic, is called \thydx{Pure}. +\item[{\it theoryDef}] is the full definition. The new theory is + called $id$. It is the union of the named {\bf parent + theories}\indexbold{theories!parent}, possibly extended with new + components. \thydx{Pure} and \thydx{CPure} are the basic theories, + which contain only the meta-logic. They differ just in their + concrete syntax for function applications. Normally each {\it name\/} is an identifier, the name of the parent theory. Quoted strings can be used to document additional file dependencies; see @@ -56,10 +57,9 @@ variables created internally. If omitted, the default sort is the listwise union of the default sorts of the parent theories (i.e.\ their logical intersection). - -\item[$sort$] - is a finite set of classes. A single class $id$ abbreviates the singleton - set {\tt\{}$id${\tt\}}. + +\item[$sort$] is a finite set of classes. A single class $id$ + abbreviates the sort $\ttlbrace id\ttrbrace$. \item[$types$] is a series of type declarations. Each declares a new type constructor @@ -75,19 +75,23 @@ declares a type or constant to be an infix operator of priority $nat$ associating to the left ({\tt infixl}) or right ({\tt infixr}). Only 2-place type constructors can have infix status; an example is {\tt - ('a,'b)~"*"~(infixr~20)}, which expresses binary product types. - -\item[$arities$] - is a series of arity declarations. Each assigns arities to type - constructors. The $name$ must be an existing type constructor, which is - given the additional arity $arity$. + ('a,'b)~"*"~(infixr~20)}, which may express binary product types. -\item[$constDecl$] - is a series of constant declarations. Each new constant $name$ is given - the specified type. The optional $mixfix$ annotations may - attach concrete syntax to the constant. A variant of {\tt consts} is the - {\tt syntax} section\index{*syntax section}, which adds just syntax without - declaring logical constants. +\item[$arities$] is a series of type arity declarations. Each assigns + arities to type constructors. The $name$ must be an existing type + constructor, which is given the additional arity $arity$. + +\item[$consts$] is a series of constant declarations. Each new + constant $name$ is given the specified type. The optional $mixfix$ + annotations may attach concrete syntax to the constant. + +\item[$syntax$] \index{*syntax section}\index{print mode} is a variant + of $consts$ which adds just syntax without actually declaring + logical constants. This gives full control over a theory's context + free grammar. The optional $mode$ specifies the print mode where the + mixfix productions should be added. If there is no \texttt{output} + option given, all productions are also added to the input syntax + (regardless of the print mode). \item[$mixfix$] \index{mixfix declarations} annotations can take three forms: @@ -115,13 +119,28 @@ \item[$rules$] is a series of rule declarations. Each has a name $id$ and the formula is given by the $string$. Rule names must be distinct within any single - theory file. + theory. \item[$defs$] is a series of definitions. They are just like $rules$, except that every $string$ must be a definition (see below for details). \item[$constdefs$] combines the declaration of constants and their definition. The first $string$ is the type, the second the definition. + +\item[$axclass$] \index{*axclass section} defines an + \rmindex{axiomatic type class} as the intersection of existing + classes, with additional axioms holding. Class axioms may not + contain more than one type variable. The class axioms (with implicit + sort constraints added) are bound to the given names. Furthermore a + class introduction rule is generated, which is automatically + employed by $instance$ to prove instantiations of this class. + +\item[$instance$] \index{*instance section} proves class inclusions or + type arities at the logical level and then transfers these to the + type signature. The instantiation is proven and checked properly. + The user has to supply sufficient witness information: theorems + ($longident$), axioms ($string$), or even arbitrary \ML{} tactic + code $verbatim$. \item[$oracle$] links the theory to a trusted external reasoner. It is allowed to create theorems, but each theorem carries a proof object @@ -137,18 +156,19 @@ \subsection{Definitions}\indexbold{definitions} -{\bf Definitions} are intended to express abbreviations. The simplest form of -a definition is $f \equiv t$, where $f$ is a constant. Isabelle also allows a -derived form where the arguments of~$f$ appear on the left, abbreviating a -string of $\lambda$-abstractions. +{\bf Definitions} are intended to express abbreviations. The simplest +form of a definition is $f \equiv t$, where $f$ is a constant. +Isabelle also allows a derived forms where the arguments of~$f$ appear +on the left, abbreviating a string of $\lambda$-abstractions. Isabelle makes the following checks on definitions: \begin{itemize} -\item Arguments (on the left-hand side) must be distinct variables +\item Arguments (on the left-hand side) must be distinct variables. \item All variables on the right-hand side must also appear on the left-hand side. -\item All type variables on the right-hand side must also appear on the - left-hand side; this prohibits definitions such as {\tt zero == length []}. +\item All type variables on the right-hand side must also appear on + the left-hand side; this prohibits definitions such as {\tt + (zero::nat) == length ([]::'a list)}. \item The definition must not be recursive. Most object-logics provide definitional principles that can be used to express recursion safely. \end{itemize} @@ -164,31 +184,26 @@ In order to guarantee principal types~\cite{nipkow-prehofer}, arity declarations must obey two conditions: \begin{itemize} -\item There must be no two declarations $ty :: (\vec{r})c$ and $ty :: - (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is - forbidden: +\item There must not be any two declarations $ty :: (\vec{r})c$ and + $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this + excludes the following: \begin{ttbox} -types - 'a ty arities - ty :: ({\ttlbrace}logic{\ttrbrace}) logic - ty :: ({\ttlbrace}{\ttrbrace})logic + foo :: ({\ttlbrace}logic{\ttrbrace}) logic + foo :: ({\ttlbrace}{\ttrbrace})logic \end{ttbox} \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty :: (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold for $i=1,\dots,n$. The relationship $\preceq$, defined as \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \] -expresses that the set of types represented by $s'$ is a subset of the set of -types represented by $s$. For example, the following is forbidden: +expresses that the set of types represented by $s'$ is a subset of the +set of types represented by $s$. Assuming $term \preceq logic$, the +following is forbidden: \begin{ttbox} -classes - term < logic -types - 'a ty arities - ty :: ({\ttlbrace}logic{\ttrbrace})logic - ty :: ({\ttlbrace}{\ttrbrace})term + foo :: ({\ttlbrace}logic{\ttrbrace})logic + foo :: ({\ttlbrace}{\ttrbrace})term \end{ttbox} \end{itemize} @@ -219,14 +234,15 @@ suppresses the deletion of temporary files. \end{ttdescription} % -Each theory definition must reside in a separate file. Let the file {\it - T}{\tt.thy} contain the definition of a theory called~$T$, whose parent -theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it - T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{} -file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt - use_thy} calls load those parent theories that have not been loaded -previously; the recursive calls may continue to any depth. One {\tt use_thy} -call can read an entire logic provided all theories are linked appropriately. +Each theory definition must reside in a separate file. Let the file +{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose +parent theories are $TB@1$ \dots $TB@n$. Calling +\ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy}, +writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the +latter file. Recursive {\tt use_thy} calls load those parent theories +that have not been loaded previously; the recursive calls may continue +to any depth. One {\tt use_thy} call can read an entire logic +provided all theories are linked appropriately. The result is an \ML\ structure~$T$ containing at least a component {\tt thy} for the new theory and components for each of the rules. The structure also @@ -234,9 +250,9 @@ {\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt true} and no errors occurred. -Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally -begins with the declaration {\tt open~$T$} and contains proofs involving -the new theory. +Finally the file {\it T}{\tt.ML} is read, if it exists. Since the +structure $T$ is automatically open in this context, proof scripts may +(or even should) refer to its components by unqualified names. Some applications construct theories directly by calling \ML\ functions. In this situation there is no {\tt.thy} file, only an {\tt.ML} file. The @@ -284,17 +300,18 @@ \end{ttdescription} -\goodbreak -\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler} -The theory mechanism depends upon reference variables. At the end of a -Poly/\ML{} session, the contents of references are lost unless they are -declared in the current database. In particular, assignments to references -of the {\tt Pure} database are lost, including all information about loaded -theories. To avoid losing this information simply call -\begin{ttbox} -init_thy_reader(); -\end{ttbox} -when building the new database. +%FIXME remove +%\goodbreak +%\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler} +%The theory mechanism depends upon reference variables. At the end of a +%Poly/\ML{} session, the contents of references are lost unless they are +%declared in the current database. In particular, assignments to references +%of the {\tt Pure} database are lost, including all information about loaded +%theories. To avoid losing this information simply call +%\begin{ttbox} +%init_thy_reader(); +%\end{ttbox} +%when building the new database. \subsection{*Pseudo theories}\label{sec:pseudo-theories} @@ -346,9 +363,9 @@ The resulting theory ensures that {\tt update} reloads {\tt orphan} whenever it reloads one of the $A@i$. -For an extensive example of how this technique can be used to link lots of -theory files and load them by just a few {\tt use_thy} calls, consult the -sources of \ZF{} set theory. +For an extensive example of how this technique can be used to link +lots of theory files and load them by just a few {\tt use_thy} calls +see the sources of one of the major object-logics (e.g.\ \ZF). @@ -384,17 +401,21 @@ \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} \end{ttdescription} -\subsection{Building a theory} +\subsection{*Building a theory} \label{BuildingATheory} \index{theories!constructing|bold} \begin{ttbox} -pure_thy : theory +Pure.thy : theory +CPure.thy : theory merge_theories : theory * theory -> theory \end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{pure_thy}] contains just the syntax and signature - of the meta-logic. There are no axioms: meta-level inferences are carried - out by \ML\ functions. +\begin{description} +\item[\ttindexbold{Pure.thy}, \ttindexbold{CPure.thy}] contain the + syntax and signature of the meta-logic. There are no axioms: + meta-level inferences are carried out by \ML\ functions. The two + \Pure s just differ in their concrete syntax of function + application: $t(u@1, \ldots, u@n)$ vs.\ $t\,u@1,\ldots\,u@n$. + \item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two theories $thy@1$ and $thy@2$. The resulting theory contains all of the syntax, signature and axioms of the constituent theories. Merging theories @@ -419,7 +440,7 @@ %\begin{ttbox} %Attempt to merge different versions of theory: \(T\) %\end{ttbox} -\end{ttdescription} +\end{description} %% FIXME %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} @@ -456,6 +477,7 @@ \subsection{Inspecting a theory}\label{sec:inspct-thy} \index{theories!inspecting|bold} \begin{ttbox} +print_syntax : theory -> unit print_theory : theory -> unit axioms_of : theory -> (string * thm) list thms_of : theory -> (string * thm) list @@ -465,9 +487,12 @@ \end{ttbox} These provide means of viewing a theory's components. \begin{ttdescription} -\item[\ttindexbold{print_theory} $thy$] -prints the contents of $thy$ excluding the syntax related parts (which are -shown by {\tt print_syntax}). The output is quite verbose. +\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$ + (grammar, macros, translation functions etc., see + page~\pageref{pg:print_syn} for more details). + +\item[\ttindexbold{print_theory} $thy$] prints the logical parts of + $thy$, excluding the syntax. \item[\ttindexbold{axioms_of} $thy$] returns the additional axioms of the most recent extend node of~$thy$. @@ -487,223 +512,224 @@ with~$thy$. \end{ttdescription} - -\section{Generating HTML documents} -\index{HTML|bold} - -Isabelle is able to make HTML documents that show a theory's -definition, the theorems proved in its ML file and the relationship -with its ancestors and descendants. HTML stands for Hypertext Markup -Language and is used in the World Wide Web to represent text -containing images and links to other documents. Web browsers like -{\tt xmosaic} or {\tt netscape} are used to view these documents. - -Besides the three HTML files that are made for every theory -(definition and theorems, ancestors, descendants), Isabelle stores -links to all theories in an index file. These indexes are themself -linked with other indexes to represent the hierarchic structure of -Isabelle's logics. - -To make HTML files for logics that are part of the Isabelle -distribution, simply set the shell environment variable {\tt -MAKE_HTML} before compiling a logic. This works for single logics as -well as for the shell script {\tt make-all} (see -\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a -{\tt csh} style shell, the following commands can be used: - -\begin{ttbox} -cd FOL -setenv MAKE_HTML -make -\end{ttbox} - -The databases made this way do not differ from the ones made with an -unset {\tt MAKE_HTML}; in particular no HTML files are written if the -database is used to manually load a theory. - -As you will see below, the HTML generation is controlled by a boolean -reference variable. If you want to make databases which define this -variable's value as {\tt true} and where therefore HTML files are -written each time {\tt use_thy} is invoked, you have to set {\tt -MAKE_HTML} to ``{\tt true}'': - -\begin{ttbox} -cd FOL -setenv MAKE_HTML true -make -\end{ttbox} - -All theories loaded from within the {\tt FOL} database and all -databases derived from it will now cause HTML files to be written. -This behaviour can be changed by assigning a value of {\tt false} to -the boolean reference variable {\tt make_html}. Be careful when making -such databases publicly available since it means that your users will -generate HTML files though they might not intend to do so. - -As some of Isabelle's logics are based on others (e.g. {\tt ZF} on -{\tt FOL}) and because the HTML files list a theory's ancestors, you -should not make HTML files for a logic if the HTML files for the base -logic do not exist. Otherwise some of the hypertext links might point -to non-existing documents. - -The entry point to all logics is the {\tt index.html} file located in -Isabelle's main directory. You can also access a HTML version of the -distribution package at - -\begin{ttbox} -http://www4.informatik.tu-muenchen.de/~nipkow/isabelle -\end{ttbox} - - -\subsection*{Manual HTML generation} - -To manually control the generation of HTML files the following -commands and reference variables are used: - -\begin{ttbox} -init_html : unit -> unit -make_html : bool ref -finish_html : unit -> unit -\end{ttbox} - -\begin{ttdescription} -\item[\ttindexbold{init_html}] -activates the HTML facility. It stores the current working directory -as the place where the {\tt index.html} file for all theories loaded -afterwards will be stored. - -\item[\ttindexbold{make_html}] -is a boolean reference variable read by {\tt use_thy} and other -functions to decide whether HTML files should be made. After you have -used {\tt init_html} you can manually change {\tt make_html}'s value -to temporarily disable HTML generation. - -\item[\ttindexbold{finish_html}] -has to be called after all theories have been read that should be -listed in the current {\tt index.html} file. It reads a temporary -file with information about the theories read since the last use of -{\tt init_html} and makes the {\tt index.html} file. If {\tt -make_html} is {\tt false} nothing is done. - -The indexes made by this function also contain a link to the {\tt -README} file if there exists one in the directory where the index is -stored. If there's a {\tt README.html} file it is used instead of -{\tt README}. - -\end{ttdescription} +%FIXME move to sysman! +%\section{Generating HTML documents} +%\index{HTML|bold} +% +%Isabelle is able to make HTML documents that show a theory's +%definition, the theorems proved in its ML file and the relationship +%with its ancestors and descendants. HTML stands for Hypertext Markup +%Language and is used in the World Wide Web to represent text +%containing images and links to other documents. Web browsers like +%{\tt xmosaic} or {\tt netscape} are used to view these documents. +% +%Besides the three HTML files that are made for every theory +%(definition and theorems, ancestors, descendants), Isabelle stores +%links to all theories in an index file. These indexes are themself +%linked with other indexes to represent the hierarchic structure of +%Isabelle's logics. +% +%To make HTML files for logics that are part of the Isabelle +%distribution, simply set the shell environment variable {\tt +%MAKE_HTML} before compiling a logic. This works for single logics as +%well as for the shell script {\tt make-all} (see +%\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a +%{\tt csh} style shell, the following commands can be used: +% +%\begin{ttbox} +%cd FOL +%setenv MAKE_HTML +%make +%\end{ttbox} +% +%The databases made this way do not differ from the ones made with an +%unset {\tt MAKE_HTML}; in particular no HTML files are written if the +%database is used to manually load a theory. +% +%As you will see below, the HTML generation is controlled by a boolean +%reference variable. If you want to make databases which define this +%variable's value as {\tt true} and where therefore HTML files are +%written each time {\tt use_thy} is invoked, you have to set {\tt +%MAKE_HTML} to ``{\tt true}'': +% +%\begin{ttbox} +%cd FOL +%setenv MAKE_HTML true +%make +%\end{ttbox} +% +%All theories loaded from within the {\tt FOL} database and all +%databases derived from it will now cause HTML files to be written. +%This behaviour can be changed by assigning a value of {\tt false} to +%the boolean reference variable {\tt make_html}. Be careful when making +%such databases publicly available since it means that your users will +%generate HTML files though they might not intend to do so. +% +%As some of Isabelle's logics are based on others (e.g. {\tt ZF} on +%{\tt FOL}) and because the HTML files list a theory's ancestors, you +%should not make HTML files for a logic if the HTML files for the base +%logic do not exist. Otherwise some of the hypertext links might point +%to non-existing documents. +% +%The entry point to all logics is the {\tt index.html} file located in +%Isabelle's main directory. You can also access a HTML version of the +%distribution package at +% +%\begin{ttbox} +%http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/ +%\end{ttbox} +% +% +%\subsection*{Manual HTML generation} +% +%To manually control the generation of HTML files the following +%commands and reference variables are used: +% +%\begin{ttbox} +%init_html : unit -> unit +%make_html : bool ref +%finish_html : unit -> unit +%\end{ttbox} +% +%\begin{ttdescription} +%\item[\ttindexbold{init_html}] +%activates the HTML facility. It stores the current working directory +%as the place where the {\tt index.html} file for all theories loaded +%afterwards will be stored. +% +%\item[\ttindexbold{make_html}] +%is a boolean reference variable read by {\tt use_thy} and other +%functions to decide whether HTML files should be made. After you have +%used {\tt init_html} you can manually change {\tt make_html}'s value +%to temporarily disable HTML generation. +% +%\item[\ttindexbold{finish_html}] +%has to be called after all theories have been read that should be +%listed in the current {\tt index.html} file. It reads a temporary +%file with information about the theories read since the last use of +%{\tt init_html} and makes the {\tt index.html} file. If {\tt +%make_html} is {\tt false} nothing is done. +% +%The indexes made by this function also contain a link to the {\tt +%README} file if there exists one in the directory where the index is +%stored. If there's a {\tt README.html} file it is used instead of +%{\tt README}. +% +%\end{ttdescription} +% +%The above functions could be used in the following way: +% +%\begin{ttbox} +%init_html(); +%{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"} +%use_thy "List"; +%\dots +%finish_html(); +%\end{ttbox} +% +%Please note that HTML files are made only for those theories that are +%read while {\tt make_html} is {\tt true}. These files may contain +%links to theories that were read with a {\tt false} {\tt make_html} +%and therefore point to non-existing files. +% +% +%\subsection*{Extending or adding a logic} +% +%If you add a new subdirectory to Isabelle's logics (or add a completly +%new logic), you would have to call {\tt init_html} at the start of every +%directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of +%it. This is automatically done if you use +% +%\begin{ttbox}\index{use_dir} +%use_dir : string -> unit +%\end{ttbox} +% +%This function takes a path as its parameter, changes the working +%directory, calls {\tt init_html} if {\tt make_html} is {\tt true}, +%executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt +%index.html} file written in this directory will be automatically +%linked to the first index found in the (recursively searched) +%superdirectories. +% +%Instead of adding something like +% +%\begin{ttbox} +%use"ex/ROOT.ML"; +%\end{ttbox} +% +%to the logic's makefile you have to use this: +% +%\begin{ttbox} +%use_dir"ex"; +%\end{ttbox} +% +%Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is +%{\tt true} the generation of HTML files depends on the value this +%reference variable has. It can either be inherited from the used \ML{} +%database or set in the makefile before {\tt use_dir} is invoked, +%e.g. to set it's value according to the environment variable {\tt +%MAKE_HTML}. +% +%The generated HTML files contain all theorems that were proved in the +%theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw}, +%or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there +%is a hypertext link to the whole \ML{} file. +% +%You can add section headings to the list of theorems by using +% +%\begin{ttbox}\index{use_dir} +%section: string -> unit +%\end{ttbox} +% +%in a theory's ML file, which converts a plain string to a HTML +%heading and inserts it before the next theorem proved or stored with +%one of the above functions. If {\tt make_html} is {\tt false} nothing +%is done. +% +% +%\subsection*{Using someone else's database} +% +%To make them independent from their storage place, the HTML files only +%contain relative paths which are derived from absolute ones like the +%current working directory, {\tt gif_path} or {\tt base_path}. The +%latter two are reference variables which are initialized at the time +%when the {\tt Pure} database is made. Because you need write access +%for the current directory to make HTML files and therefore (probably) +%generate them in your home directory, the absolute {\tt base_path} is +%not correct if you use someone else's database or a database derived +%from it. +% +%In that case you first should set {\tt base_path} to the value of {\em +%your} Isabelle main directory, i.e. the directory that contains the +%subdirectories where standard logics like {\tt FOL} and {\tt HOL} or +%your own logics are stored. If you do not do this, the generated HTML +%files will still be usable but may contain incomplete titles and lack +%some hypertext links. +% +%It's also a good idea to set {\tt gif_path} which points to the +%directory containing two GIF images used in the HTML +%documents. Normally this is the {\tt Tools} subdirectory of Isabelle's +%main directory. While its value in general is still valid, your HTML +%files would depend on files not owned by you. This prevents you from +%changing the location of the HTML files (as they contain relative +%paths) and also causes trouble if the database's maker (re)moves the +%GIFs. +% +%Here's what you should do before invoking {\tt init_html} using +%someone else's \ML{} database: +% +%\begin{ttbox} +%base_path := "/home/smith/isabelle"; +%gif_path := "/home/smith/isabelle/Tools"; +%init_html(); +%\dots +%\end{ttbox} -The above functions could be used in the following way: - -\begin{ttbox} -init_html(); -{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"} -use_thy "List"; -\dots -finish_html(); -\end{ttbox} - -Please note that HTML files are made only for those theories that are -read while {\tt make_html} is {\tt true}. These files may contain -links to theories that were read with a {\tt false} {\tt make_html} -and therefore point to non-existing files. - - -\subsection*{Extending or adding a logic} - -If you add a new subdirectory to Isabelle's logics (or add a completly -new logic), you would have to call {\tt init_html} at the start of every -directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of -it. This is automatically done if you use - -\begin{ttbox}\index{use_dir} -use_dir : string -> unit -\end{ttbox} - -This function takes a path as its parameter, changes the working -directory, calls {\tt init_html} if {\tt make_html} is {\tt true}, -executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt -index.html} file written in this directory will be automatically -linked to the first index found in the (recursively searched) -superdirectories. - -Instead of adding something like - -\begin{ttbox} -use"ex/ROOT.ML"; -\end{ttbox} - -to the logic's makefile you have to use this: - -\begin{ttbox} -use_dir"ex"; -\end{ttbox} - -Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is -{\tt true} the generation of HTML files depends on the value this -reference variable has. It can either be inherited from the used \ML{} -database or set in the makefile before {\tt use_dir} is invoked, -e.g. to set it's value according to the environment variable {\tt -MAKE_HTML}. - -The generated HTML files contain all theorems that were proved in the -theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw}, -or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there -is a hypertext link to the whole \ML{} file. - -You can add section headings to the list of theorems by using - -\begin{ttbox}\index{use_dir} -section: string -> unit -\end{ttbox} - -in a theory's ML file, which converts a plain string to a HTML -heading and inserts it before the next theorem proved or stored with -one of the above functions. If {\tt make_html} is {\tt false} nothing -is done. - - -\subsection*{Using someone else's database} - -To make them independent from their storage place, the HTML files only -contain relative paths which are derived from absolute ones like the -current working directory, {\tt gif_path} or {\tt base_path}. The -latter two are reference variables which are initialized at the time -when the {\tt Pure} database is made. Because you need write access -for the current directory to make HTML files and therefore (probably) -generate them in your home directory, the absolute {\tt base_path} is -not correct if you use someone else's database or a database derived -from it. - -In that case you first should set {\tt base_path} to the value of {\em -your} Isabelle main directory, i.e. the directory that contains the -subdirectories where standard logics like {\tt FOL} and {\tt HOL} or -your own logics are stored. If you do not do this, the generated HTML -files will still be usable but may contain incomplete titles and lack -some hypertext links. - -It's also a good idea to set {\tt gif_path} which points to the -directory containing two GIF images used in the HTML -documents. Normally this is the {\tt Tools} subdirectory of Isabelle's -main directory. While its value in general is still valid, your HTML -files would depend on files not owned by you. This prevents you from -changing the location of the HTML files (as they contain relative -paths) and also causes trouble if the database's maker (re)moves the -GIFs. - -Here's what you should do before invoking {\tt init_html} using -someone else's \ML{} database: - -\begin{ttbox} -base_path := "/home/smith/isabelle"; -gif_path := "/home/smith/isabelle/Tools"; -init_html(); -\dots -\end{ttbox} \section{Terms} \index{terms|bold} Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype -with six constructors: there are six kinds of term. +with six constructors: \begin{ttbox} type indexname = string * int; infix 9 $; @@ -844,7 +870,7 @@ read_cterm : Sign.sg -> string * typ -> cterm cert_axm : Sign.sg -> string * term -> string * term read_axm : Sign.sg -> string * string -> string * term -rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\} +rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace \end{ttbox} \begin{ttdescription} \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} @@ -932,7 +958,7 @@ \subsection{Making and inspecting certified types} \begin{ttbox} ctyp_of : Sign.sg -> typ -> ctyp -rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\} +rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace \end{ttbox} \begin{ttdescription} \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} @@ -968,7 +994,7 @@ \item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to be $fn$. It is seldom called explicitly, as there is syntax for oracles in - theory files. A theory can have at most one oracle. + theory files. Any theory node can have at most one oracle. \end{ttdescription} A curious feature of {\ML} exceptions is that they are ordinary constructors.