doc-src/Ref/theories.tex
author clasohm
Fri Dec 01 12:27:09 1995 +0100 (1995-12-01)
changeset 1380 2f8055af9c04
parent 1369 b82815e61b30
child 1387 9bcad9c22fd4
permissions -rw-r--r--
changed HTML documentation
     1 %% $Id$
     2 
     3 \chapter{Theories, Terms and Types} \label{theories}
     4 \index{theories|(}\index{signatures|bold}
     5 \index{reading!axioms|see{{\tt assume_ax}}}
     6 Theories organize the syntax, declarations and axioms of a mathematical
     7 development.  They are built, starting from the Pure theory, by extending
     8 and merging existing theories.  They have the \ML\ type \mltydx{theory}.
     9 Theory operations signal errors by raising exception \xdx{THEORY},
    10 returning a message and a list of theories.
    11 
    12 Signatures, which contain information about sorts, types, constants and
    13 syntax, have the \ML\ type~\mltydx{Sign.sg}.  For identification, each
    14 signature carries a unique list of \bfindex{stamps}, which are \ML\
    15 references to strings.  The strings serve as human-readable names; the
    16 references serve as unique identifiers.  Each primitive signature has a
    17 single stamp.  When two signatures are merged, their lists of stamps are
    18 also merged.  Every theory carries a unique signature.
    19 
    20 Terms and types are the underlying representation of logical syntax.  Their
    21 \ML\ definitions are irrelevant to naive Isabelle users.  Programmers who
    22 wish to extend Isabelle may need to know such details, say to code a tactic
    23 that looks for subgoals of a particular form.  Terms and types may be
    24 `certified' to be well-formed with respect to a given signature.
    25 
    26 
    27 \section{Defining theories}\label{sec:ref-defining-theories}
    28 
    29 Theories are usually defined using theory definition files (which have a name
    30 suffix {\tt .thy}). There is also a low level interface provided by certain
    31 \ML{} functions (see \S\ref{BuildingATheory}).
    32 Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
    33 definitions; here is an explanation of the constituent parts:
    34 \begin{description}
    35 \item[{\it theoryDef}]
    36   is the full definition.  The new theory is called $id$.  It is the union
    37   of the named {\bf parent theories}\indexbold{theories!parent}, possibly
    38   extended with new classes, etc.  The basic theory, which contains only
    39   the meta-logic, is called \thydx{Pure}.
    40 
    41   Normally each {\it name\/} is an identifier, the name of the parent theory.
    42   Quoted strings can be used to document additional file dependencies; see
    43   \S\ref{LoadingTheories} for details.
    44 
    45 \item[$classes$]
    46   is a series of class declarations.  Declaring {\tt$id$ < $id@1$ \dots\
    47     $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
    48   id@n$.  This rules out cyclic class structures.  Isabelle automatically
    49   computes the transitive closure of subclass hierarchies; it is not
    50   necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
    51     e}.
    52 
    53 \item[$default$]
    54   introduces $sort$ as the new default sort for type variables.  This applies
    55   to unconstrained type variables in an input string but not to type
    56   variables created internally.  If omitted, the default sort is the listwise
    57   union of the default sorts of the parent theories (i.e.\ their logical
    58   intersection).
    59 
    60 \item[$sort$]
    61   is a finite set of classes.  A single class $id$ abbreviates the singleton
    62   set {\tt\{}$id${\tt\}}.
    63 
    64 \item[$types$]
    65   is a series of type declarations.  Each declares a new type constructor
    66   or type synonym.  An $n$-place type constructor is specified by
    67   $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
    68   indicate the number~$n$.
    69 
    70   A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
    71   $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where
    72   $name$ can be a string and $\tau$ must be enclosed in quotation marks.
    73 
    74 \item[$infix$]
    75   declares a type or constant to be an infix operator of priority $nat$
    76   associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
    77   2-place type constructors can have infix status; an example is {\tt
    78   ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.
    79 
    80 \item[$arities$]
    81   is a series of arity declarations.  Each assigns arities to type
    82   constructors.  The $name$ must be an existing type constructor, which is
    83   given the additional arity $arity$.
    84 
    85 \item[$constDecl$]
    86   is a series of constant declarations.  Each new constant $name$ is given
    87   the specified type.  The optional $mixfix$ annotations may
    88   attach concrete syntax to the constant. A variant of {\tt consts} is the
    89   {\tt syntax} section\index{*syntax section}, which adds just syntax without
    90   declaring logical constants.
    91 
    92 \item[$mixfix$] \index{mixfix declarations}
    93   annotations can take three forms:
    94   \begin{itemize}
    95   \item A mixfix template given as a $string$ of the form
    96     {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
    97     indicates the position where the $i$-th argument should go.  The list
    98     of numbers gives the priority of each argument.  The final number gives
    99     the priority of the whole construct.
   100 
   101   \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
   102     infix} status.
   103 
   104   \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
   105     binder} status.  The declaration {\tt binder} $\cal Q$ $p$ causes
   106   ${\cal Q}\,x.F(x)$ to be treated
   107   like $f(F)$, where $p$ is the priority.
   108   \end{itemize}
   109 
   110 \item[$trans$]
   111   specifies syntactic translation rules (macros).  There are three forms:
   112   parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
   113   ==}).
   114 
   115 \item[$rule$]
   116   is a series of rule declarations.  Each has a name $id$ and the formula is
   117   given by the $string$.  Rule names must be distinct within any single
   118   theory file.
   119 
   120 \item[$ml$] \index{*ML section}
   121   consists of \ML\ code, typically for parse and print translation functions.
   122 \end{description}
   123 %
   124 Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
   125 declarations, translation rules and the {\tt ML} section in more detail.
   126 
   127 
   128 \subsection{*Classes and arities}
   129 \index{classes!context conditions}\index{arities!context conditions}
   130 
   131 In order to guarantee principal types~\cite{nipkow-prehofer},
   132 arity declarations must obey two conditions:
   133 \begin{itemize}
   134 \item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
   135   (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, the following is
   136   forbidden:
   137 \begin{ttbox}
   138 types
   139   'a ty
   140 arities
   141   ty :: ({\ttlbrace}logic{\ttrbrace}) logic
   142   ty :: ({\ttlbrace}{\ttrbrace})logic
   143 \end{ttbox}
   144 
   145 \item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
   146   (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
   147   for $i=1,\dots,n$.  The relationship $\preceq$, defined as
   148 \[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
   149 expresses that the set of types represented by $s'$ is a subset of the set of
   150 types represented by $s$.  For example, the following is forbidden:
   151 \begin{ttbox}
   152 classes
   153   term < logic
   154 types
   155   'a ty
   156 arities
   157   ty :: ({\ttlbrace}logic{\ttrbrace})logic
   158   ty :: ({\ttlbrace}{\ttrbrace})term
   159 \end{ttbox}
   160 
   161 \end{itemize}
   162 
   163 
   164 \section{Loading a new theory}\label{LoadingTheories}
   165 \index{theories!loading}\index{files!reading}
   166 \begin{ttbox}
   167 use_thy         : string -> unit
   168 time_use_thy    : string -> unit
   169 loadpath        : string list ref \hfill{\bf initially {\tt["."]}}
   170 delete_tmpfiles : bool ref \hfill{\bf initially true}
   171 \end{ttbox}
   172 
   173 \begin{ttdescription}
   174 \item[\ttindexbold{use_thy} $thyname$]
   175   reads the theory $thyname$ and creates an \ML{} structure as described below.
   176 
   177 \item[\ttindexbold{time_use_thy} $thyname$]
   178   calls {\tt use_thy} $thyname$ and reports the time taken.
   179 
   180 \item[\ttindexbold{loadpath}]
   181   contains a list of directories to search when locating the files that
   182   define a theory.  This list is only used if the theory name in {\tt
   183     use_thy} does not specify the path explicitly.
   184 
   185 \item[\ttindexbold{delete_tmpfiles} := false;]
   186 suppresses the deletion of temporary files.
   187 \end{ttdescription}
   188 %
   189 Each theory definition must reside in a separate file.  Let the file {\it
   190   T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
   191 theories are $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"{\it
   192   T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
   193 file {\tt.{\it T}.thy.ML}, and reads the latter file.  Recursive {\tt
   194   use_thy} calls load those parent theories that have not been loaded
   195 previously; the recursive calls may continue to any depth.  One {\tt use_thy}
   196 call can read an entire logic provided all theories are linked appropriately.
   197 
   198 The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
   199 for the new theory and components for each of the rules.  The structure also
   200 contains the definitions of the {\tt ML} section, if present.  The file
   201 {\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
   202 true} and no errors occurred.
   203 
   204 Finally the file {\it T}{\tt.ML} is read, if it exists.  This file normally
   205 begins with the declaration {\tt open~$T$} and contains proofs involving
   206 the new theory.
   207 
   208 Some applications construct theories directly by calling \ML\ functions.  In
   209 this situation there is no {\tt.thy} file, only an {\tt.ML} file.  The
   210 {\tt.ML} file must declare an \ML\ structure having the theory's name and a
   211 component {\tt thy} containing the new theory object.
   212 Section~\ref{sec:pseudo-theories} below describes a way of linking such
   213 theories to their parents.
   214 
   215 \begin{warn}
   216   Temporary files are written to the current directory, so this must be
   217   writable.  Isabelle inherits the current directory from the operating
   218   system; you can change it within Isabelle by typing {\tt
   219   cd"$dir$"}\index{*cd}.
   220 \end{warn}
   221 
   222 
   223 \section{Reloading modified theories}\label{sec:reloading-theories}
   224 \indexbold{theories!reloading}
   225 \begin{ttbox}
   226 update     : unit -> unit
   227 unlink_thy : string -> unit
   228 \end{ttbox}
   229 Changing a theory on disk often makes it necessary to reload all theories
   230 descended from it.  However, {\tt use_thy} reads only one theory, even if
   231 some of the parent theories are out of date.  In this case you should call
   232 {\tt update()}.
   233 
   234 Isabelle keeps track of all loaded theories and their files.  If
   235 \ttindex{use_thy} finds that the theory to be loaded has been read before,
   236 it determines whether to reload the theory as follows.  First it looks for
   237 the theory's files in their previous location.  If it finds them, it
   238 compares their modification times to the internal data and stops if they
   239 are equal.  If the files have been moved, {\tt use_thy} searches for them
   240 as it would for a new theory.  After {\tt use_thy} reloads a theory, it
   241 marks the children as out-of-date.
   242 
   243 \begin{ttdescription}
   244 \item[\ttindexbold{update}()]
   245   reloads all modified theories and their descendants in the correct order.
   246 
   247 \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
   248   informs Isabelle that theory $thyname$ no longer exists.  If you delete the
   249   theory files for $thyname$ then you must execute {\tt unlink_thy};
   250   otherwise {\tt update} will complain about a missing file.
   251 \end{ttdescription}
   252 
   253 
   254 \goodbreak
   255 \subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
   256 The theory mechanism depends upon reference variables.  At the end of a
   257 Poly/\ML{} session, the contents of references are lost unless they are
   258 declared in the current database.  In particular, assignments to references
   259 of the {\tt Pure} database are lost, including all information about loaded
   260 theories. To avoid losing this information simply call
   261 \begin{ttbox}
   262 init_thy_reader();
   263 \end{ttbox}
   264 when building the new database.
   265 
   266 
   267 \subsection{*Pseudo theories}\label{sec:pseudo-theories}
   268 \indexbold{theories!pseudo}%
   269 Any automatic reloading facility requires complete knowledge of all
   270 dependencies.  Sometimes theories depend on objects created in \ML{} files
   271 with no associated theory definition file.  These objects may be theories but
   272 they could also be theorems, proof procedures, etc.
   273 
   274 Unless such dependencies are documented, {\tt update} fails to reload these
   275 \ML{} files and the system is left in a state where some objects, such as
   276 theorems, still refer to old versions of theories.  This may lead to the
   277 error
   278 \begin{ttbox}
   279 Attempt to merge different versions of theories: \dots
   280 \end{ttbox}
   281 Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
   282 those not associated with a theory definition.
   283 
   284 Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
   285 theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
   286 theorems proved in {\tt orphan.ML}.  Then {\tt B.thy} should
   287 mention this dependency as follows:
   288 \begin{ttbox}
   289 B = \(\ldots\) + "orphan" + \(\ldots\)
   290 \end{ttbox}
   291 Quoted strings stand for theories which have to be loaded before the
   292 current theory is read but which are not used in building the base of
   293 theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle
   294 knows that $B$ has to be updated, too.
   295 
   296 Note that it's necessary for {\tt orphan} to declare a special ML
   297 object of type {\tt theory} which is present in all theories. This is
   298 normally achieved by adding the file {\tt orphan.thy} to make {\tt
   299 orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy}
   300 would be
   301 
   302 \begin{ttbox}
   303 orphan = Pure
   304 \end{ttbox}
   305 
   306 which uses {\tt Pure} to make a dummy theory. Normally though the
   307 orphaned file has its own dependencies.  If {\tt orphan.ML} depends on
   308 theories or files $A@1$, \ldots, $A@n$, record this by creating the
   309 pseudo theory in the following way:
   310 \begin{ttbox}
   311 orphan = \(A@1\) + \(\ldots\) + \(A@n\)
   312 \end{ttbox}
   313 The resulting theory ensures that {\tt update} reloads {\tt orphan}
   314 whenever it reloads one of the $A@i$.
   315 
   316 For an extensive example of how this technique can be used to link lots of
   317 theory files and load them by just a few {\tt use_thy} calls, consult the
   318 sources of \ZF{} set theory.
   319 
   320 
   321 
   322 \section{Basic operations on theories}\label{BasicOperationsOnTheories}
   323 \subsection{Extracting an axiom or theorem from a theory}
   324 \index{theories!axioms of}\index{axioms!extracting}
   325 \index{theories!theorems of}\index{theorems!extracting}
   326 \begin{ttbox}
   327 get_axiom : theory -> string -> thm
   328 get_thm   : theory -> string -> thm
   329 assume_ax : theory -> string -> thm
   330 \end{ttbox}
   331 \begin{ttdescription}
   332 \item[\ttindexbold{get_axiom} $thy$ $name$]
   333   returns an axiom with the given $name$ from $thy$, raising exception
   334   \xdx{THEORY} if none exists.  Merging theories can cause several axioms
   335   to have the same name; {\tt get_axiom} returns an arbitrary one.
   336 
   337 \item[\ttindexbold{get_thm} $thy$ $name$]
   338   is analogous to {\tt get_axiom}, but looks for a stored theorem. Like
   339   {\tt get_axiom} it searches all parents of a theory if the theorem
   340   is not associated with $thy$.
   341 
   342 \item[\ttindexbold{assume_ax} $thy$ $formula$]
   343   reads the {\it formula} using the syntax of $thy$, following the same
   344   conventions as axioms in a theory definition.  You can thus pretend that
   345   {\it formula} is an axiom and use the resulting theorem like an axiom.
   346   Actually {\tt assume_ax} returns an assumption;  \ttindex{result}
   347   complains about additional assumptions, but \ttindex{uresult} does not.
   348 
   349 For example, if {\it formula} is
   350 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form
   351 \hbox{\verb'?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]'}
   352 \end{ttdescription}
   353 
   354 \subsection{Building a theory}
   355 \label{BuildingATheory}
   356 \index{theories!constructing|bold}
   357 \begin{ttbox}
   358 pure_thy       : theory
   359 merge_theories : theory * theory -> theory
   360 \end{ttbox}
   361 \begin{ttdescription}
   362 \item[\ttindexbold{pure_thy}] contains just the syntax and signature
   363   of the meta-logic.  There are no axioms: meta-level inferences are carried
   364   out by \ML\ functions.
   365 \item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
   366   theories $thy@1$ and $thy@2$.  The resulting theory contains all of the
   367   syntax, signature and axioms of the constituent theories. Merging theories
   368   that contain different identification stamps of the same name fails with
   369   the following message
   370 \begin{ttbox}
   371 Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
   372 \end{ttbox}
   373   This error may especially occur when a theory is redeclared --- say to
   374   change an incorrect axiom --- and bindings to old versions persist.
   375   Isabelle ensures that old and new theories of the same name are not
   376   involved in a proof.
   377 
   378 %% FIXME
   379 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
   380 %  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory
   381 %  internally.  When a theory is redeclared, say to change an incorrect axiom,
   382 %  bindings to the old axiom may persist.  Isabelle ensures that the old and
   383 %  new theories are not involved in the same proof.  Attempting to combine
   384 %  different theories having the same name $T$ yields the fatal error
   385 %extend_theory  : theory -> string -> \(\cdots\) -> theory
   386 %\begin{ttbox}
   387 %Attempt to merge different versions of theory: \(T\)
   388 %\end{ttbox}
   389 \end{ttdescription}
   390 
   391 %% FIXME
   392 %\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
   393 %      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
   394 %\hfill\break   %%% include if line is just too short
   395 %is the \ML{} equivalent of the following theory definition:
   396 %\begin{ttbox}
   397 %\(T\) = \(thy\) +
   398 %classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
   399 %        \dots
   400 %default {\(d@1,\dots,d@r\)}
   401 %types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
   402 %        \dots
   403 %arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
   404 %        \dots
   405 %consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
   406 %        \dots
   407 %rules   \(name\) \(rule\)
   408 %        \dots
   409 %end
   410 %\end{ttbox}
   411 %where
   412 %\begin{tabular}[t]{l@{~=~}l}
   413 %$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
   414 %$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
   415 %$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
   416 %$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
   417 %\\
   418 %$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
   419 %$rules$   & \tt[("$name$",$rule$),\dots]
   420 %\end{tabular}
   421 
   422 
   423 \subsection{Inspecting a theory}\label{sec:inspct-thy}
   424 \index{theories!inspecting|bold}
   425 \begin{ttbox}
   426 print_theory  : theory -> unit
   427 axioms_of     : theory -> (string * thm) list
   428 thms_of       : theory -> (string * thm) list
   429 parents_of    : theory -> theory list
   430 sign_of       : theory -> Sign.sg
   431 stamps_of_thy : theory -> string ref list
   432 \end{ttbox}
   433 These provide means of viewing a theory's components.
   434 \begin{ttdescription}
   435 \item[\ttindexbold{print_theory} $thy$]
   436 prints the contents of $thy$ excluding the syntax related parts (which are
   437 shown by {\tt print_syntax}).  The output is quite verbose.
   438 
   439 \item[\ttindexbold{axioms_of} $thy$]
   440 returns the additional axioms of the most recent extend node of~$thy$.
   441 
   442 \item[\ttindexbold{thms_of} $thy$]
   443 returns all theorems that are associated with $thy$.
   444 
   445 \item[\ttindexbold{parents_of} $thy$]
   446 returns the direct ancestors of~$thy$.
   447 
   448 \item[\ttindexbold{sign_of} $thy$]
   449 returns the signature associated with~$thy$.  It is useful with functions
   450 like {\tt read_instantiate_sg}, which take a signature as an argument.
   451 
   452 \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
   453 returns the identification \rmindex{stamps} of the signature associated
   454 with~$thy$.
   455 \end{ttdescription}
   456 
   457 
   458 \section{Generating HTML documents}
   459 \index{HTML|bold} 
   460 
   461 Isabelle is able to make HTML documents that show a theory's
   462 definition, the theorems proved in its ML file and the relationship
   463 with its ancestors and descendants. HTML stands for Hypertext Markup
   464 Language and is used in the World Wide Web to represent text
   465 containing images and links to other documents. Web browsers like
   466 {\tt xmosaic} or {\tt netscape} are used to view these documents.
   467 
   468 Besides the three HTML files that are made for every theory
   469 (definition and theorems, ancestors, descendants), Isabelle stores
   470 links to all theories in an index file. These indexes are themself
   471 linked with other indexes to represent the hierarchic structure of
   472 Isabelle's logics.
   473 
   474 To make HTML files for logics that are part of the Isabelle
   475 distribution, simply set the shell environment variable {\tt
   476 MAKE_HTML} before compiling a logic. This works for single logics as
   477 well as for the shell script {\tt make-all} (see
   478 \ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
   479 {\tt csh} style shell, the following commands can be used:
   480 
   481 \begin{ttbox}
   482 cd FOL
   483 setenv MAKE_HTML
   484 make
   485 \end{ttbox}
   486 
   487 As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
   488 {\tt FOL}) and because the HTML files list a theory's ancestors, you
   489 should not make HTML files for a logic if the HTML files for the base
   490 logic do not exist. Otherwise some of the hypertext links might point
   491 to non-existing documents.
   492 
   493 The entry point to all logics is the {\tt index.html} file located in
   494 Isabelle's main directory. You can also access a HTML version of the
   495 distribution package at
   496 
   497 \begin{ttbox}
   498 http://www4.informatik.tu-muenchen.de/~nipkow/isabelle
   499 \end{ttbox}
   500 
   501 
   502 \subsection*{Manual HTML generation}
   503 
   504 To manually activate and deactivate the generation of HTML files the
   505 following commands and reference variables are used:
   506 
   507 \begin{ttbox}
   508 init_html   : unit -> unit
   509 make_html   : bool ref
   510 finish_html : unit -> unit
   511 \end{ttbox}
   512 
   513 \begin{ttdescription}
   514 \item[\ttindexbold{init_html}]
   515 activates the HTML facility. It stores the current working directory
   516 as the place where the {\tt index.html} file for all theories loaded
   517 afterwards will be stored.
   518 
   519 \item[\ttindexbold{make_html}]
   520 is a boolean reference variable read by {\tt use_thy} and other
   521 functions to decide whether HTML files should be made. After you have
   522 used {\tt init_html} you can manually change {\tt make_html}'s value
   523 to temporarily disable HTML generation.
   524 
   525 \item[\ttindexbold{finish_html}]
   526 has to be called after all theories have been read that should be
   527 listed in the current {\tt index.html} file. It reads a temporary
   528 file with information about the theories read since the last use of
   529 {\tt init_html} and makes the {\tt index.html} file. If {\tt
   530 make_html} is {\tt false} nothing is done.
   531 
   532 The indexes made by this function also contain a link to the {\tt
   533 README} file if there exists one in the directory were the index is
   534 stored. If there's a {\tt README.html} file it is used instead of
   535 {\tt README}.
   536 
   537 \end{ttdescription}
   538 
   539 The above functions could be used in the following way:
   540 
   541 \begin{ttbox}
   542 init_html();
   543 {\out Setting path for index.html to "/home/stud/clasohm/isabelle/HOL"}
   544 use_thy "List";
   545 \dots
   546 finish_html();
   547 \end{ttbox}
   548 
   549 Please note that HTML files are made only for those theories that are
   550 read while {\tt make_html} is {\tt true}. These files may contain
   551 links to theories that were read with a {\tt false} {\tt make_html}
   552 and therefore point to non-existing files.
   553 
   554 
   555 \subsection*{Extending or adding a logic}
   556 
   557 If you add a new subdirectory to Isabelle's logics (or add a completly
   558 new logic), you would have to call {\tt init_html} at the start of every
   559 directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
   560 it. This is automatically done if you use
   561 
   562 \begin{ttbox}\index{use_dir}
   563 use_dir : string -> unit
   564 \end{ttbox}
   565 
   566 This function takes a path as its parameter, changes the working
   567 directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
   568 executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
   569 index.html} file written in this directory will be automatically
   570 linked to the first index found in the (recursively searched)
   571 superdirectories.
   572 
   573 Instead of adding something like
   574 
   575 \begin{ttbox}
   576 use"ex/ROOT.ML";
   577 \end{ttbox}
   578 
   579 to the logic's makefile you have to use this:
   580 
   581 \begin{ttbox}
   582 use_dir"ex";
   583 \end{ttbox}
   584 
   585 Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
   586 {\tt true} the generation of HTML files depends on the value this
   587 reference variable has. It can either be inherited from the used \ML{}
   588 database or set in the makefile before {\tt use_dir} is invoked,
   589 e.g. to set it's value according to the environment variable {\tt
   590 MAKE_HTML}.
   591 
   592 The generated HTML files contain all theorems that were proved in the
   593 theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
   594 or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
   595 is a hypertext link to the whole \ML{} file.
   596 
   597 
   598 \subsection*{Using someone else's database}
   599 
   600 To make them independent from their storage place, the HTML files only
   601 contain relative paths which are derived from absolute ones like the
   602 current working directory, {\tt gif_path} or {\tt base_path}. The
   603 latter two are reference variables which are initialized at the time
   604 when the {\tt Pure} database is made. Because you need write access
   605 for the current directory to make HTML files and therefore (probably)
   606 generate them in your home directory, the absolute {\tt base_path} is
   607 not correct if you use someone else's database or a database derived
   608 from it.
   609 
   610 In that case you first have to set {\tt base_path} to the value of
   611 {\em your} Isabelle main directory, i.e. the directory that contains
   612 the subdirectories where standard logics like {\tt FOL} and {\tt HOL}
   613 or your own logics are stored.
   614 
   615 It's also a good idea to set {\tt gif_path} which points to the
   616 directory containing two GIF images used in the HTML
   617 documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
   618 main directory. While its value in general is still valid, your HTML
   619 files would depend on files not owned by you. This prevents you from
   620 changing the location of the HTML files (as they contain relative
   621 paths) and also causes trouble if the database's maker (re)moves the
   622 GIFs.
   623 
   624 Here's what you have to do before invoking {\tt init_html} using
   625 someone else's \ML{} database:
   626 
   627 \begin{ttbox}
   628 base_path := "/home/smith/isabelle";
   629 gif_path := "/home/smith/isabelle/Tools";
   630 init_html();
   631 \dots
   632 \end{ttbox}
   633 
   634 \section{Terms}
   635 \index{terms|bold}
   636 Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
   637 with six constructors: there are six kinds of term.
   638 \begin{ttbox}
   639 type indexname = string * int;
   640 infix 9 $;
   641 datatype term = Const of string * typ
   642               | Free  of string * typ
   643               | Var   of indexname * typ
   644               | Bound of int
   645               | Abs   of string * typ * term
   646               | op $  of term * term;
   647 \end{ttbox}
   648 \begin{ttdescription}
   649 \item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold}
   650   is the {\bf constant} with name~$a$ and type~$T$.  Constants include
   651   connectives like $\land$ and $\forall$ as well as constants like~0
   652   and~$Suc$.  Other constants may be required to define a logic's concrete
   653   syntax.
   654 
   655 \item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold}
   656   is the {\bf free variable} with name~$a$ and type~$T$.
   657 
   658 \item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold}
   659   is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
   660   \mltydx{indexname} is a string paired with a non-negative index, or
   661   subscript; a term's scheme variables can be systematically renamed by
   662   incrementing their subscripts.  Scheme variables are essentially free
   663   variables, but may be instantiated during unification.
   664 
   665 \item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
   666   is the {\bf bound variable} with de Bruijn index~$i$, which counts the
   667   number of lambdas, starting from zero, between a variable's occurrence
   668   and its binding.  The representation prevents capture of variables.  For
   669   more information see de Bruijn \cite{debruijn72} or
   670   Paulson~\cite[page~336]{paulson91}.
   671 
   672 \item[\ttindexbold{Abs}($a$, $T$, $u$)]
   673   \index{lambda abs@$\lambda$-abstractions|bold}
   674   is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
   675   variable has name~$a$ and type~$T$.  The name is used only for parsing
   676   and printing; it has no logical significance.
   677 
   678 \item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
   679 is the {\bf application} of~$t$ to~$u$.
   680 \end{ttdescription}
   681 Application is written as an infix operator to aid readability.
   682 Here is an \ML\ pattern to recognize \FOL{} formulae of
   683 the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
   684 \begin{ttbox}
   685 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
   686 \end{ttbox}
   687 
   688 
   689 \section{Variable binding}
   690 \begin{ttbox}
   691 loose_bnos     : term -> int list
   692 incr_boundvars : int -> term -> term
   693 abstract_over  : term*term -> term
   694 variant_abs    : string * typ * term -> string * term
   695 aconv          : term*term -> bool\hfill{\bf infix}
   696 \end{ttbox}
   697 These functions are all concerned with the de Bruijn representation of
   698 bound variables.
   699 \begin{ttdescription}
   700 \item[\ttindexbold{loose_bnos} $t$]
   701   returns the list of all dangling bound variable references.  In
   702   particular, {\tt Bound~0} is loose unless it is enclosed in an
   703   abstraction.  Similarly {\tt Bound~1} is loose unless it is enclosed in
   704   at least two abstractions; if enclosed in just one, the list will contain
   705   the number 0.  A well-formed term does not contain any loose variables.
   706 
   707 \item[\ttindexbold{incr_boundvars} $j$]
   708   increases a term's dangling bound variables by the offset~$j$.  This is
   709   required when moving a subterm into a context where it is enclosed by a
   710   different number of abstractions.  Bound variables with a matching
   711   abstraction are unaffected.
   712 
   713 \item[\ttindexbold{abstract_over} $(v,t)$]
   714   forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
   715   It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
   716   correct index.
   717 
   718 \item[\ttindexbold{variant_abs} $(a,T,u)$]
   719   substitutes into $u$, which should be the body of an abstraction.
   720   It replaces each occurrence of the outermost bound variable by a free
   721   variable.  The free variable has type~$T$ and its name is a variant
   722   of~$a$ chosen to be distinct from all constants and from all variables
   723   free in~$u$.
   724 
   725 \item[$t$ \ttindexbold{aconv} $u$]
   726   tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
   727   to renaming of bound variables.
   728 \begin{itemize}
   729   \item
   730     Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
   731     if their names and types are equal.
   732     (Variables having the same name but different types are thus distinct.
   733     This confusing situation should be avoided!)
   734   \item
   735     Two bound variables are \(\alpha\)-convertible
   736     if they have the same number.
   737   \item
   738     Two abstractions are \(\alpha\)-convertible
   739     if their bodies are, and their bound variables have the same type.
   740   \item
   741     Two applications are \(\alpha\)-convertible
   742     if the corresponding subterms are.
   743 \end{itemize}
   744 
   745 \end{ttdescription}
   746 
   747 \section{Certified terms}\index{terms!certified|bold}\index{signatures}
   748 A term $t$ can be {\bf certified} under a signature to ensure that every type
   749 in~$t$ is well-formed and every constant in~$t$ is a type instance of a
   750 constant declared in the signature.  The term must be well-typed and its use
   751 of bound variables must be well-formed.  Meta-rules such as {\tt forall_elim}
   752 take certified terms as arguments.
   753 
   754 Certified terms belong to the abstract type \mltydx{cterm}.
   755 Elements of the type can only be created through the certification process.
   756 In case of error, Isabelle raises exception~\ttindex{TERM}\@.
   757 
   758 \subsection{Printing terms}
   759 \index{terms!printing of}
   760 \begin{ttbox}
   761      string_of_cterm :           cterm -> string
   762 Sign.string_of_term  : Sign.sg -> term -> string
   763 \end{ttbox}
   764 \begin{ttdescription}
   765 \item[\ttindexbold{string_of_cterm} $ct$]
   766 displays $ct$ as a string.
   767 
   768 \item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
   769 displays $t$ as a string, using the syntax of~$sign$.
   770 \end{ttdescription}
   771 
   772 \subsection{Making and inspecting certified terms}
   773 \begin{ttbox}
   774 cterm_of   : Sign.sg -> term -> cterm
   775 read_cterm : Sign.sg -> string * typ -> cterm
   776 cert_axm   : Sign.sg -> string * term -> string * term
   777 read_axm   : Sign.sg -> string * string -> string * term
   778 rep_cterm  : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
   779 \end{ttbox}
   780 \begin{ttdescription}
   781 \item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
   782 certifies $t$ with respect to signature~$sign$.
   783 
   784 \item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)]
   785 reads the string~$s$ using the syntax of~$sign$, creating a certified term.
   786 The term is checked to have type~$T$; this type also tells the parser what
   787 kind of phrase to parse.
   788 
   789 \item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)]
   790 certifies $t$ with respect to $sign$ as a meta-proposition and converts all
   791 exceptions to an error, including the final message
   792 \begin{ttbox}
   793 The error(s) above occurred in axiom "\(name\)"
   794 \end{ttbox}
   795 
   796 \item[\ttindexbold{read_axm} $sign$ ($name$, $s$)]
   797 similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of
   798 $sign$.
   799 
   800 \item[\ttindexbold{rep_cterm} $ct$]
   801 decomposes $ct$ as a record containing its type, the term itself, its
   802 signature, and the maximum subscript of its unknowns.  The type and maximum
   803 subscript are computed during certification.
   804 \end{ttdescription}
   805 
   806 
   807 \section{Types}\index{types|bold}
   808 Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
   809 three constructor functions.  These correspond to type constructors, free
   810 type variables and schematic type variables.  Types are classified by sorts,
   811 which are lists of classes (representing an intersection).  A class is
   812 represented by a string.
   813 \begin{ttbox}
   814 type class = string;
   815 type sort  = class list;
   816 
   817 datatype typ = Type  of string * typ list
   818              | TFree of string * sort
   819              | TVar  of indexname * sort;
   820 
   821 infixr 5 -->;
   822 fun S --> T = Type ("fun", [S, T]);
   823 \end{ttbox}
   824 \begin{ttdescription}
   825 \item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold}
   826   applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
   827   Type constructors include~\tydx{fun}, the binary function space
   828   constructor, as well as nullary type constructors such as~\tydx{prop}.
   829   Other type constructors may be introduced.  In expressions, but not in
   830   patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
   831   types.
   832 
   833 \item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold}
   834   is the {\bf type variable} with name~$a$ and sort~$s$.
   835 
   836 \item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold}
   837   is the {\bf type unknown} with indexname~$v$ and sort~$s$.
   838   Type unknowns are essentially free type variables, but may be
   839   instantiated during unification.
   840 \end{ttdescription}
   841 
   842 
   843 \section{Certified types}
   844 \index{types!certified|bold}
   845 Certified types, which are analogous to certified terms, have type
   846 \ttindexbold{ctyp}.
   847 
   848 \subsection{Printing types}
   849 \index{types!printing of}
   850 \begin{ttbox}
   851      string_of_ctyp :           ctyp -> string
   852 Sign.string_of_typ  : Sign.sg -> typ -> string
   853 \end{ttbox}
   854 \begin{ttdescription}
   855 \item[\ttindexbold{string_of_ctyp} $cT$]
   856 displays $cT$ as a string.
   857 
   858 \item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
   859 displays $T$ as a string, using the syntax of~$sign$.
   860 \end{ttdescription}
   861 
   862 
   863 \subsection{Making and inspecting certified types}
   864 \begin{ttbox}
   865 ctyp_of  : Sign.sg -> typ -> ctyp
   866 rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
   867 \end{ttbox}
   868 \begin{ttdescription}
   869 \item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
   870 certifies $T$ with respect to signature~$sign$.
   871 
   872 \item[\ttindexbold{rep_ctyp} $cT$]
   873 decomposes $cT$ as a record containing the type itself and its signature.
   874 \end{ttdescription}
   875 
   876 \index{theories|)}