author nipkow Tue, 01 Mar 1994 17:21:47 +0100 changeset 275 933ec96c522e parent 274 dc87495814d5 child 276 4cf7139e5b7a
update towards LNCS
 doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/theories.tex	Tue Mar 01 16:00:53 1994 +0100
+++ b/doc-src/Ref/theories.tex	Tue Mar 01 17:21:47 1994 +0100
@@ -5,22 +5,22 @@
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 \ttindex{theory}.
+and merging existing theories.  They have the \ML\ type \ttindex{theory}.
Theory operations signal errors by raising exception \ttindex{THEORY},
returning a message and a list of theories.

Signatures, which contain information about sorts, types, constants and
-syntax, have the \ML{} type~\ttindexbold{Sign.sg}.  For identification,
-each signature carries a unique list of {\bf stamps}, which are~\ML{}
+syntax, have the \ML\ type~\ttindexbold{Sign.sg}.  For identification,
+each signature carries a unique list of {\bf stamps}, which are \ML\
references (to strings).  The strings serve as human-readable names; the
references serve as unique identifiers.  Each primitive signature has a
single stamp.  When two signatures are merged, their lists of stamps are
also merged.  Every theory carries a unique signature.

Terms and types are the underlying representation of logical syntax.  Their
-\ML{} definitions are irrelevant to naive Isabelle users.  Programmers who wish
-to extend Isabelle may need to know such details, say to code a tactic that
-looks for subgoals of a particular form.  Terms and types may be
+\ML\ definitions are irrelevant to naive Isabelle users.  Programmers who
+wish to extend Isabelle may need to know such details, say to code a tactic
+that looks for subgoals of a particular form.  Terms and types may be
certified' to be well-formed with respect to a given signature.

\section{Defining Theories}
@@ -28,32 +28,25 @@

Theories can be defined either using concrete syntax or by calling certain
\ML-functions (see \S\ref{BuildingATheory}).  Appendix~\ref{TheorySyntax}
-presents the concrete syntax for theories.
-This grammar employs the
-following conventions:
+presents the concrete syntax for theories following convention that
\begin{itemize}
-\item Identifiers such as {\it theoryDef} denote nonterminal symbols.
-\item Text in {\tt typewriter font} denotes terminal symbols.
-\item $id$ is an Isabelle identifier.
-\item $string$ is an ML string, with its quotation marks.
-\item $nat$ is for a natural number.
-\item $tfree$ is an Isabelle type variable, i.e.\ an identifier starting with
-  a prime.
-\item $text$ stands for arbitrary ML text.
+\item {\tt typewriter font} denotes terminal symbols;
+\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
+  identifiers, type identifiers, natural numbers, \ML\ strings (with their
+  quotation marks) and arbitrary \ML\ text. The first three are fully defined
+  in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.
\end{itemize}
The different parts of a theory definition are interpreted as follows:
\begin{description}
\item[{\it theoryDef}] A theory has a name $id$ and is an extension of the
-  union of theories {\it name}, the {\em parent theories}, with new classes,
-  types, constants, syntax and axioms.  The basic theory, which contains only
-  the meta-logic, is called {\tt Pure}.
+  union of theories with name {\it name}, the {\bf parent
+    theories}\indexbold{theories!parent}, with new classes, types, constants,
+  syntax and axioms.  The basic theory, which contains only the meta-logic,
+  is called {\tt Pure}.

-  If {\it name} is a string, then theory {\it name} is {\em not} used in
-  building the base of theory $id$. Strings stand for ML-files rather than
-  theory-files and document the dependence of $id$ on additional files. This
-  enables all required files, namely those corresponding to {\it name}s, to
-  be loaded automatically when theory $id$ is (re)built. See
+  Normally each {\it name\/} is an identifier, the precise name of the parent
+  theory. Strings can be used to document additional dependencies; see
\item[$classes$] {\tt$id$ < $id@1$ \dots\ $id@n$} declares $id$ as a subclass
of existing classes $id@1\dots id@n$.  This rules out cyclic class
structures.  Isabelle automatically computes the transitive closure of
@@ -68,54 +61,56 @@
singleton set {\tt\{}$id${\tt\}}.
\item[$type$] is either the declaration of a new type (constructor) or type
synonym $name$. Only binary type constructors can have infix status and
-  symbolic names, e.g.\ {\tt ('a,'b)"+"}. Type constructors of $n$ arguments
-  are declared by {\tt ($\alpha@1$,\dots,$\alpha@n$)$name$}.  Type
-  synonyms\indexbold{type!synonym} are defined as in ML, except that the
-  right-hand side must be enclosed in quotation marks.
+  symbolic names, e.g.\ {\tt ('a,'b)"*"}. Type constructors of $n$ arguments
+  are declared by $(\alpha@1,\dots,\alpha@n)name$.  A {\bf type
+    synonym}\indexbold{type!synonym} is simply an abbreviation
+  $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$ and follows
+  the same rules as in \ML, except that $name$ can be a string and $\tau$
+  must be enclosed in quotation marks.
\item[$infix$] declares a type or constant to be an infix operator of
precedence $nat$ associating to the left ({\tt infixl}) or right ({\tt
infixr}).
\item[$arities$] Each $name$ must be an existing type constructor which is
given the additional arity $arity$.
\item[$constDecl$] Each new constant $name$ is declared to be of type
-  $string$.  For display purposes they can be annotated with $mixfix$
-  declarations.
+  $string$.  For display purposes $mixfix$ annotations can be attached.
\item[$mixfix$] There are three forms of syntactic annotations:
\begin{itemize}
\item A mixfix template given as a $string$ of the form
{\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
indicates the position where the $i$-th argument should go. The minimal
precedence of each argument is given by a list of natural numbers, the
-    precedence of the construct by the following natural number; precedences
-    are optional.
+    precedence of the whole construct by the following natural number;
+    precedences are optional.

\item Binary constants can be given infix status.

\item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
-    binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
+    binder\/} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
like $f(F)$; $p$ is the precedence of the construct.
\end{itemize}
\item[$trans$] Specifies syntactic translation rules, that is parse
rules ({\tt =>}), print rules ({\tt <=}), or both ({\tt ==}).
\item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
names must be distinct.
-\item[$ml$] This final part of a theory consists of ML code,
+\item[$ml$] This final part of a theory consists of \ML\ code,
typically for parse and print translations.
\end{description}
The $mixfix$, $trans$ and $ml$ sections are explained in more detail in
-the {\it Defining Logics} chapter of the {\it Logics} manual.
+the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.

-\subsection{Classes and types}
+\subsection{*Classes and arities}
+\index{*classes!context conditions}
\index{*arities!context conditions}

-Type declarations are subject to the following two well-formedness
+Classes and arities are subject to the following two well-formedness
conditions:
\begin{itemize}
\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
with $\vec{r} \neq \vec{s}$.  For example
\begin{ttbox}
-types ty 1
+types 'a ty
arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic
ty :: ({\ttlbrace}{\ttrbrace})logic
\end{ttbox}
@@ -128,7 +123,7 @@
types represented by $s$.  For example
\begin{ttbox}
classes term < logic
-types ty 1
+types 'a ty
arities ty :: ({\ttlbrace}logic{\ttrbrace})logic
ty :: ({\ttlbrace}{\ttrbrace})term
\end{ttbox}
@@ -139,48 +134,54 @@

+

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 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. \indexbold{automatic
-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 appropriately.  Afterwards an {\ML}
+  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 appropriately.  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. Unless
-\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML}
-is deleted if no errors occurred. Finally the file {\it tf}{\tt.ML} is read, if
-it exists; this file normally contains proofs involving the new theory.
+\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it
+  tf}{\tt.thy.ML} is deleted if no errors occurred. 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}
-\indexbold{filenames}
+\subsection{Theory names, file names and search paths}
+\indexbold{theories!names of}
+\indexbold{files!names of}
+\indexbold{search path}

\begin{warn}
The files defining the theory must have the lower case name of the theory
-  with {\tt".thy"} or {\tt".ML"} appended.  On the other hand
-  \ttindex{use_thy}'s parameter has to be the exact theory name.
+  with {\tt.thy} or {\tt.ML} appended.  On the other hand \ttindex{use_thy}'s
+  parameter has to be the exact theory name.
\end{warn}
Optionally the name can be preceded by a path to specify the directory where
the files can be found.  If no path is provided the reference variable
\ttindexbold{loadpath} is used which contains a list of paths that are
-searched in the given order.  After the {\tt".thy"}-file for a theory has
-been found, the same path is used to locate the (optional) {\tt".ML"}-file.
+searched in the given order.  After the {\tt.thy}-file for a theory has
+been found, the same path is used to locate the (optional) {\tt.ML}-file.

-It is also possible to provide only a {\tt".ML"}-file, with no
-{\tt".thy"}-file.  In this case the {\tt".ML"}-file must declare an \ML{}
-structure having the theory's name.  If both the {\tt".thy"}-file and a
-structure declaration in the {\tt".ML"}-file exist, then the latter
+It is also possible to provide only a {\tt.ML}-file, with no
+{\tt.thy}-file.  In this case the {\tt.ML}-file must declare an \ML\
+structure having the theory's name.  If both the {\tt.thy}-file and a
+structure declaration in the {\tt.ML}-file exist, then the latter
declaration is used.  See {\tt ZF/ex/llist.ML} for an example.

+\index{*update|(}

\ttindex{use_thy} keeps track of all loaded theories and stores information
@@ -190,75 +191,77 @@
use_thy} stops if they are equal. In case the files have been moved, {\tt
use_thy} searches them the same way 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 (those that have its name in their {\it
-  theoryDef}) are marked as out-of-date.
+its children are marked as out-of-date.
\begin{warn}
Changing a theory on disk often makes it necessary to reload all theories
-  that (indirectly) depend on it. However, {\tt use_thy} reads only one
-  theory, even if some of the parents are out of date. In this case
-  \ttindexbold{update}{\tt()} should be used.  This function reloads {\em all}
+  that directly or indirectly depend on it. However, {\tt use_thy} reads only
+  one theory, even if some of the parent theories are out of date. In this
+  case {\tt update()} should be used.  This function reloads {\em all\/}
modified theories and their descendants in the correct order.
\end{warn}

-\subsection{Pseudo theories}
-\indexbold{pseudo theories}
+\subsection{*Pseudo theories}
+\indexbold{theories!pseudo}

-There is a problem with \ttindex{update}: objects created in \ML-files that
-do not belong to a theory (see explanation of {\it 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}
+dependencies. Sometimes theories depend on objects created in \ML-files
+without associated {\tt.thy}-file. Unless such dependencies are documented,
+{\tt update} fails to reload these \ML-files and the system is left in a
+state where some objects, e.g.\ theorems, still refer to old versions of
+theories. This may lead to the error
+\begin{ttbox}
+Attempt to merge different versions of theory: $$T$$
+\end{ttbox}
+Therefore there is a way to link theories and {\em orphaned\/} \ML-files,
+i.e.\ those without associated {\tt.thy}-file.

-Therefore there is a way to link theories and the $orphaned$ \ML-files. The
-link from a theory to an \ML-file has been mentioned in
-Chapter~\ref{DefiningTheories} (strings in {\it 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 an \ML-file named {\tt orphan.ML}
-that depends on theory $A$ and is itself used in theory $B$.  To link the
-three we have to create the file {\tt orphan.thy} containing the line
+Let us assume we have an orphaned \ML-file named {\tt orphan.ML} and a theory
+$B$ which depends on {\tt orphan.ML} (for example, {\tt b.ML} uses theorems
+that are proved in {\tt orphan.ML}). Then {\tt b.thy} should mention this
+dependence:
\begin{ttbox}
-orphan = A
+B = ... + "orphan" + ...
\end{ttbox}
-and add {\tt "orphan"} to the list of $B$'s parents.
-% 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$).
-Creating {\tt orphan.thy} enables automatic loading of $orphan$'s parents.
-If {\tt orphan.ML} depended on no theory then {\tt Pure} should have been
+Although {\tt orphan} is {\em not\/} used in building the base of theory $B$
+(strings stand for \ML-files rather than {\tt.thy}-files and merely document
+additional dependencies), {\tt orphan.ML} is loaded automatically when $B$ is
+(re)built.
+
+If {\tt orphan.ML} depends on theories $A@1\dots A@n$, this should be recorded
+by creating a {\bf pseudo theory} in the file {\tt orphan.thy}:
+\begin{ttbox}
+orphan = A1 + $$...$$ + An
+\end{ttbox}
+The resulting theory is never used but guarantees that {\tt update} reloads
+theory {\it orphan} whenever it reloads one of the $A@i$.

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.
+files and load them by just two {\tt use_thy} calls, consult the ZF source
+files.

\subsection{Removing a theory}
-\index{removing theories}
+\indexbold{theories!removing}

-If a previously read file is removed the \ttindex{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
+If a previously read file is removed, {\tt update} 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 remove a theory manually

\subsection{Using Poly/\ML}
\index{Poly/\ML}
\index{reference variables}

-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 created by
+As the functions for reading theories depend on reference variables one has
+to take into account the way Poly/\ML\ handles them.  They are only saved
+together with the state if they were declared in the current database.  For
+example, changes made to a reference variable declared in the {\tt Pure}
+database are {\em not\/} saved if made while using a child database.
+Therefore a new {\tt Readthy} structure has to be created by
\begin{ttbox}
@@ -295,22 +298,83 @@
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]}
\end{description}

+%\subsection{Building a theory}
+%\label{BuildingATheory}
+%\index{theories!constructing|bold}
+%\begin{ttbox}
+%pure_thy: theory
+%merge_theories: theory * theory -> theory
+%extend_theory: theory -> string
+%        -> (class * class list) list
+%           * sort
+%           * (string list * int)list
+%           * (string list * (sort list * class))list
+%           * (string list * string)list * sext option
+%        -> (string*string)list -> theory
+%\end{ttbox}
+%Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
+%a synonym for \hbox{\tt class list}.
+%\begin{description}
+%\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
+%  of the meta-logic.  There are no axioms: meta-level inferences are carried
+%  out by \ML\ functions.
+%\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
+%  theories $thy@1$ and $thy@2$.  The resulting theory contains all types,
+%  constants and axioms of the constituent theories; its default sort is the
+%  union of the default sorts of the constituent theories.
+%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
+%      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
+%\hfill\break   %%% include if line is just too short
+%is the \ML-equivalent of the following theory definition:
+%\begin{ttbox}
+%$$T$$ = $$thy$$ +
+%classes $$c$$ < $$c@1$$,$$\dots$$,$$c@m$$
+%        \dots
+%default {$$d@1,\dots,d@r$$}
+%types   $$tycon@1$$,\dots,$$tycon@i$$ $$n$$
+%        \dots
+%arities $$tycon@1'$$,\dots,$$tycon@j'$$ :: ($$s@1$$,\dots,$$s@n$$)$$c$$
+%        \dots
+%consts  $$b@1$$,\dots,$$b@k$$ :: $$\tau$$
+%        \dots
+%rules   $$name$$ $$rule$$
+%        \dots
+%end
+%\end{ttbox}
+%where
+%\begin{tabular}[t]{l@{~=~}l}
+%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
+%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
+%$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
+%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
+%\\
+%$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
+%$rules$   & \tt[("$name$",$rule$),\dots]
+%\end{tabular}
+%
+%If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
+%as mixfix annotations to constants.  Using {\tt extend_theory}, new syntax can
+%be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}.  The
+%latter case is not documented.
+%
+%$T$ identifies the theory internally.  When a theory is redeclared, say to
+%change an incorrect axiom, bindings to the old axiom may persist.  Isabelle
+%ensures that the old and new theories are not involved in the same proof.
+%Attempting to combine different theories having the same name $T$ yields the
+%fatal error
+%\begin{ttbox}
+%Attempt to merge different versions of theory: $$T$$
+%\end{ttbox}
+%\end{description}
+
\subsection{Building a theory}
\label{BuildingATheory}
\index{theories!constructing|bold}
\begin{ttbox}
pure_thy: theory
merge_theories: theory * theory -> theory
-extend_theory: theory -> string
-        -> (class * class list) list
-           * sort
-           * (string list * int)list
-           * (string list * (sort list * class))list
-           * (string list * string)list * sext option
-        -> (string*string)list -> theory
+extend_theory: theory -> string -> $$\cdots$$ -> theory
\end{ttbox}
-Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
-a synonym for \hbox{\tt class list}.
\begin{description}
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
of the meta-logic.  There are no axioms: meta-level inferences are carried
@@ -319,49 +383,15 @@
theories $thy@1$ and $thy@2$.  The resulting theory contains all types,
constants and axioms of the constituent theories; its default sort is the
union of the default sorts of the constituent theories.
-\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
-      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
-\hfill\break   %%% include if line is just too short
-is the \ML-equivalent of the following theory definition:
+\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
+  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory
+  internally.  When a theory is redeclared, say to change an incorrect axiom,
+  bindings to the old axiom may persist.  Isabelle ensures that the old and
+  new theories are not involved in the same proof.  Attempting to combine
+  different theories having the same name $T$ yields the fatal error
\begin{ttbox}
-$$T$$ = $$thy$$ +
-classes $$c$$ < $$c@1$$,$$\dots$$,$$c@m$$
-        \dots
-default {$$d@1,\dots,d@r$$}
-types   $$tycon@1$$,\dots,$$tycon@i$$ $$n$$
-        \dots
-arities $$tycon@1'$$,\dots,$$tycon@j'$$ :: ($$s@1$$,\dots,$$s@n$$)$$c$$
-        \dots
-consts  $$b@1$$,\dots,$$b@k$$ :: $$\tau$$
-        \dots
-rules   $$name$$ $$rule$$
-        \dots
-end
+Attempt to merge different versions of theory: $$T$$
\end{ttbox}
-where
-\begin{tabular}[t]{l@{~=~}l}
-$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
-$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
-$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
-$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
-\\
-$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
-$rules$   & \tt[("$name$",$rule$),\dots]
-\end{tabular}
-
-If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
-as mixfix annotations to constants.  Using {\tt extend_theory}, new syntax can
-be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}.  The
-latter case is not documented.
-
-$T$ identifies the theory internally.  When a theory is redeclared, say to
-change an incorrect axiom, bindings to the old axiom may persist.  Isabelle
-ensures that the old and new theories are not involved in the same proof.
-Attempting to combine different theories having the same name $T$ yields the
-fatal error
-\begin{center} \tt
-Attempt to merge different versions of theory: $T$
-\end{center}
\end{description}

@@ -400,7 +430,7 @@

\section{Terms}
\index{terms|bold}
-Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype
+Terms belong to the \ML\ type \ttindexbold{term}, which is a concrete datatype
with six constructors: there are six kinds of term.
\begin{ttbox}
type indexname = string * int;
@@ -445,7 +475,7 @@
is the {\bf application} of~$t$ to~$u$.
\end{description}
Application is written as an infix operator in order to aid readability.
-For example, here is an \ML{} pattern to recognize first-order formula of
+For example, here is an \ML\ pattern to recognize first-order formula of
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
\begin{ttbox}
Const("Trueprop",_) $(Const("op -->",_)$ A $B) @@ -462,18 +492,18 @@ binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take certified terms as arguments. -Certified terms belong to the abstract type \ttindexbold{Sign.cterm}. +Certified terms belong to the abstract type \ttindexbold{cterm}. Elements of the type can only be created through the certification process. In case of error, Isabelle raises exception~\ttindex{TERM}\@. \subsection{Printing terms} \index{printing!terms|bold} \begin{ttbox} -Sign.string_of_cterm : Sign.cterm -> string + string_of_cterm : cterm -> string Sign.string_of_term : Sign.sg -> term -> string \end{ttbox} \begin{description} -\item[\ttindexbold{Sign.string_of_cterm}$ct$] +\item[\ttindexbold{string_of_cterm}$ct$] displays$ct$as a string. \item[\ttindexbold{Sign.string_of_term}$signt$] @@ -482,21 +512,20 @@ \subsection{Making and inspecting certified terms} \begin{ttbox} -Sign.cterm_of : Sign.sg -> term -> Sign.cterm -Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm -Sign.rep_cterm : Sign.cterm -> \{T:typ, t:term, - sign: Sign.sg, maxidx:int\} +cterm_of : Sign.sg -> term -> cterm +read_cterm : Sign.sg -> string * typ -> cterm +rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\} \end{ttbox} \begin{description} -\item[\ttindexbold{Sign.cterm_of}$signt$] \index{signatures} +\item[\ttindexbold{cterm_of}$signt$] \index{signatures} certifies$t$with respect to signature~$sign$. -\item[\ttindexbold{Sign.read_cterm}$sign$($s$,$T$)] +\item[\ttindexbold{read_cterm}$sign$($s$,$T$)] reads the string~$s$using the syntax of~$sign$, creating a certified term. The term is checked to have type~$T$; this type also tells the parser what kind of phrase to parse. -\item[\ttindexbold{Sign.rep_cterm}$ct$] +\item[\ttindexbold{rep_cterm}$ct$] decomposes$ct$as a record containing its type, the term itself, its signature, and the maximum subscript of its unknowns. The type and maximum subscript are computed during certification. @@ -505,7 +534,7 @@ \section{Types} \index{types|bold} -Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete +Types belong to the \ML\ type \ttindexbold{typ}, which is a concrete datatype with three constructors. Types are classified by sorts, which are lists of classes. A class is represented by a string. \begin{ttbox} @@ -541,16 +570,16 @@ \section{Certified types} \index{types!certified|bold} Certified types, which are analogous to certified terms, have type -\ttindexbold{Sign.ctyp}. +\ttindexbold{ctyp}. \subsection{Printing types} \index{printing!types|bold} \begin{ttbox} -Sign.string_of_ctyp : Sign.ctyp -> string + string_of_ctyp : ctyp -> string Sign.string_of_typ : Sign.sg -> typ -> string \end{ttbox} \begin{description} -\item[\ttindexbold{Sign.string_of_ctyp}$cT$] +\item[\ttindexbold{string_of_ctyp}$cT$] displays$cT$as a string. \item[\ttindexbold{Sign.string_of_typ}$signT$] @@ -560,14 +589,14 @@ \subsection{Making and inspecting certified types} \begin{ttbox} -Sign.ctyp_of : Sign.sg -> typ -> Sign.ctyp -Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\} +ctyp_of : Sign.sg -> typ -> ctyp +rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\} \end{ttbox} \begin{description} -\item[\ttindexbold{Sign.ctyp_of}$signT$] \index{signatures} +\item[\ttindexbold{ctyp_of}$signT$] \index{signatures} certifies$T$with respect to signature~$sign$. -\item[\ttindexbold{Sign.rep_ctyp}$cT$] +\item[\ttindexbold{rep_ctyp}$cT$] decomposes$cT\$ as a record containing the type itself and its signature.
\end{description}
`