doc-src/Ref/theories.tex
author wenzelm
Wed, 18 Jan 1995 10:17:55 +0100
changeset 864 d63b111b917a
parent 478 838bd766d536
child 866 2d3d020eef11
permissions -rw-r--r--
quite a lot of minor and major revisions (inspecting theories, read_axm, cert_axm, grammar generation, lexical matters, macro examples, ...);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
     2
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\chapter{Theories, Terms and Types} \label{theories}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\index{theories|(}\index{signatures|bold}
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
     5
\index{reading!axioms|see{{\tt assume_ax}}}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
Theories organize the syntax, declarations and axioms of a mathematical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
development.  They are built, starting from the Pure theory, by extending
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
     8
and merging existing theories.  They have the \ML\ type \mltydx{theory}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
     9
Theory operations signal errors by raising exception \xdx{THEORY},
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
returning a message and a list of theories.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
Signatures, which contain information about sorts, types, constants and
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
    13
syntax, have the \ML\ type~\mltydx{Sign.sg}.  For identification, each
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    14
signature carries a unique list of \bfindex{stamps}, which are \ML\
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    15
references to strings.  The strings serve as human-readable names; the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
references serve as unique identifiers.  Each primitive signature has a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
single stamp.  When two signatures are merged, their lists of stamps are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
also merged.  Every theory carries a unique signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
Terms and types are the underlying representation of logical syntax.  Their
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    21
\ML\ definitions are irrelevant to naive Isabelle users.  Programmers who
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    22
wish to extend Isabelle may need to know such details, say to code a tactic
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    23
that looks for subgoals of a particular form.  Terms and types may be
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
`certified' to be well-formed with respect to a given signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    26
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    27
\section{Defining theories}\label{sec:ref-defining-theories}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    29
Theories are usually defined using theory definition files (which have a name
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    30
suffix {\tt .thy}). There is also a low level interface provided by certain
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    31
\ML{} functions (see \S\ref{BuildingATheory}).
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    32
Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    33
definitions; here is an explanation of the constituent parts:
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    34
\begin{description}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    35
\item[{\it theoryDef}]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    36
  is the full definition.  The new theory is called $id$.  It is the union
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    37
  of the named {\bf parent theories}\indexbold{theories!parent}, possibly
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    38
  extended with new classes, etc.  The basic theory, which contains only
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    39
  the meta-logic, is called \thydx{Pure}.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
    40
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    41
  Normally each {\it name\/} is an identifier, the name of the parent theory.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    42
  Quoted strings can be used to document additional file dependencies; see
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    43
  \S\ref{LoadingTheories} for details.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    44
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    45
\item[$classes$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    46
  is a series of class declarations.  Declaring {\tt$id$ < $id@1$ \dots\
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    47
    $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    48
  id@n$.  This rules out cyclic class structures.  Isabelle automatically
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    49
  computes the transitive closure of subclass hierarchies; it is not
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    50
  necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    51
    e}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    52
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    53
\item[$default$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    54
  introduces $sort$ as the new default sort for type variables.  This applies
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    55
  to unconstrained type variables in an input string but not to type
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    56
  variables created internally.  If omitted, the default sort is the listwise
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    57
  union of the default sorts of the parent theories (i.e.\ their logical
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    58
  intersection).
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    59
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    60
\item[$sort$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    61
  is a finite set of classes.  A single class $id$ abbreviates the singleton
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    62
  set {\tt\{}$id${\tt\}}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    63
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    64
\item[$types$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    65
  is a series of type declarations.  Each declares a new type constructor
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    66
  or type synonym.  An $n$-place type constructor is specified by
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    67
  $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    68
  indicate the number~$n$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    69
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
    70
  A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    71
  $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    72
  $name$ can be a string and $\tau$ must be enclosed in quotation marks.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    73
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    74
\item[$infix$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    75
  declares a type or constant to be an infix operator of priority $nat$
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    76
  associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    77
  2-place type constructors can have infix status; an example is {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    78
  ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    79
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    80
\item[$arities$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    81
  is a series of arity declarations.  Each assigns arities to type
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    82
  constructors.  The $name$ must be an existing type constructor, which is
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    83
  given the additional arity $arity$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    84
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    85
\item[$constDecl$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    86
  is a series of constant declarations.  Each new constant $name$ is given
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    87
  the type specified by the $string$.  The optional $mixfix$ annotations may
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    88
  attach concrete syntax to the constant. A variant of {\tt consts} is the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    89
  {\tt syntax} section\index{*syntax section}, which adds just syntax without
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    90
  declaring logical constants.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    91
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    92
\item[$mixfix$] \index{mixfix declarations}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    93
  annotations can take three forms:
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    94
  \begin{itemize}
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    95
  \item A mixfix template given as a $string$ of the form
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    96
    {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    97
    indicates the position where the $i$-th argument should go.  The list
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    98
    of numbers gives the priority of each argument.  The final number gives
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    99
    the priority of the whole construct.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   101
  \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   102
    infix} status.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   104
  \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   105
    binder} status.  The declaration {\tt binder} $\cal Q$ $p$ causes
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   106
  ${\cal Q}\,x.F(x)$ to be treated
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   107
  like $f(F)$, where $p$ is the priority.
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
   108
  \end{itemize}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   109
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   110
\item[$trans$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   111
  specifies syntactic translation rules (macros).  There are three forms:
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   112
  parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   113
  ==}).
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   114
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   115
\item[$rule$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   116
  is a series of rule declarations.  Each has a name $id$ and the formula is
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   117
  given by the $string$.  Rule names must be distinct within any single
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   118
  theory file.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   119
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   120
\item[$ml$] \index{*ML section}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   121
  consists of \ML\ code, typically for parse and print translation functions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\end{description}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   123
%
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   124
Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   125
declarations, translation rules and the {\tt ML} section in more detail.
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   126
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   127
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   128
\subsection{*Classes and arities}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   129
\index{classes!context conditions}\index{arities!context conditions}
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   130
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   131
In order to guarantee principal types~\cite{nipkow-prehofer},
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   132
arity declarations must obey two conditions:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   133
\begin{itemize}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   134
\item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   135
  (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, the following is
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   136
  forbidden:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   137
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   138
types
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   139
  'a ty
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   140
arities
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   141
  ty :: ({\ttlbrace}logic{\ttrbrace}) logic
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   142
  ty :: ({\ttlbrace}{\ttrbrace})logic
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   143
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   144
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   145
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   146
  (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   147
  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   148
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   149
expresses that the set of types represented by $s'$ is a subset of the set of
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   150
types represented by $s$.  For example, the following is forbidden:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   151
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   152
classes
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   153
  term < logic
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   154
types
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   155
  'a ty
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   156
arities
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   157
  ty :: ({\ttlbrace}logic{\ttrbrace})logic
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   158
  ty :: ({\ttlbrace}{\ttrbrace})term
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   159
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   160
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   161
\end{itemize}
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   162
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   164
\section{Loading a new theory}\label{LoadingTheories}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   165
\index{theories!loading}\index{files!reading}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   166
\begin{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   167
use_thy         : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   168
time_use_thy    : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   169
loadpath        : string list ref \hfill{\bf initially {\tt["."]}}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   170
delete_tmpfiles : bool ref \hfill{\bf initially true}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   171
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   172
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   173
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   174
\item[\ttindexbold{use_thy} $thyname$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   175
  reads the theory $thyname$ and creates an \ML{} structure as described below.
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   176
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   177
\item[\ttindexbold{time_use_thy} $thyname$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   178
  calls {\tt use_thy} $thyname$ and reports the time taken.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   179
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   180
\item[\ttindexbold{loadpath}]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   181
  contains a list of directories to search when locating the files that
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   182
  define a theory.  This list is only used if the theory name in {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   183
    use_thy} does not specify the path explicitly.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   184
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   185
\item[\ttindexbold{delete_tmpfiles} := false;]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   186
suppresses the deletion of temporary files.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   187
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   188
%
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
Each theory definition must reside in a separate file.  Let the file {\it
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   190
  T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   191
theories are $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"{\it
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   192
  T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   193
file {\tt.{\it T}.thy.ML}, and reads the latter file.  Recursive {\tt
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   194
  use_thy} calls load those parent theories that have not been loaded
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   195
previously; the recursive calls may continue to any depth.  One {\tt use_thy}
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   196
call can read an entire logic provided all theories are linked appropriately.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   197
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   198
The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   199
for the new theory and components for each of the rules.  The structure also
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   200
contains the definitions of the {\tt ML} section, if present.  The file
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   201
{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   202
true} and no errors occurred.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   203
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   204
Finally the file {\it T}{\tt.ML} is read, if it exists.  This file normally
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   205
begins with the declaration {\tt open~$T$} and contains proofs involving
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   206
the new theory.
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   207
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   208
Some applications construct theories directly by calling \ML\ functions.  In
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   209
this situation there is no {\tt.thy} file, only an {\tt.ML} file.  The
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   210
{\tt.ML} file must declare an \ML\ structure having the theory's name and a
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   211
component {\tt thy} containing the new theory object.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   212
Section~\ref{sec:pseudo-theories} below describes a way of linking such
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   213
theories to their parents.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   214
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   215
\begin{warn}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   216
  Temporary files are written to the current directory, so this must be
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   217
  writable.  Isabelle inherits the current directory from the operating
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   218
  system; you can change it within Isabelle by typing {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   219
  cd"$dir$"}\index{*cd}.
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
   220
\end{warn}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   221
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   222
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   223
\section{Reloading modified theories}\label{sec:reloading-theories}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   224
\indexbold{theories!reloading}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   225
\begin{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   226
update     : unit -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   227
unlink_thy : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   228
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   229
Changing a theory on disk often makes it necessary to reload all theories
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   230
descended from it.  However, {\tt use_thy} reads only one theory, even if
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   231
some of the parent theories are out of date.  In this case you should call
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   232
{\tt update()}.
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   233
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   234
Isabelle keeps track of all loaded theories and their files.  If
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   235
\ttindex{use_thy} finds that the theory to be loaded has been read before,
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   236
it determines whether to reload the theory as follows.  First it looks for
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   237
the theory's files in their previous location.  If it finds them, it
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   238
compares their modification times to the internal data and stops if they
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   239
are equal.  If the files have been moved, {\tt use_thy} searches for them
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   240
as it would for a new theory.  After {\tt use_thy} reloads a theory, it
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   241
marks the children as out-of-date.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   242
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   243
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   244
\item[\ttindexbold{update}()]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   245
  reloads all modified theories and their descendants in the correct order.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   246
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   247
\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   248
  informs Isabelle that theory $thyname$ no longer exists.  If you delete the
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   249
  theory files for $thyname$ then you must execute {\tt unlink_thy};
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   250
  otherwise {\tt update} will complain about a missing file.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   251
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   252
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   253
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   254
\goodbreak
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   255
\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   256
The theory mechanism depends upon reference variables.  At the end of a
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   257
Poly/\ML{} session, the contents of references are lost unless they are
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   258
declared in the current database.  In particular, assignments to references
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   259
of the {\tt Pure} database are lost, including all information about loaded
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   260
theories. To avoid losing this information simply call
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   261
\begin{ttbox}
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   262
init_thy_reader();
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   263
\end{ttbox}
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   264
when building the new database.
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   265
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   266
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   267
\subsection{*Pseudo theories}\label{sec:pseudo-theories}
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   268
\indexbold{theories!pseudo}%
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   269
Any automatic reloading facility requires complete knowledge of all
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   270
dependencies.  Sometimes theories depend on objects created in \ML{} files
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   271
with no associated theory definition file.  These objects may be theories but
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   272
they could also be theorems, proof procedures, etc.
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   273
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   274
Unless such dependencies are documented, {\tt update} fails to reload these
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   275
\ML{} files and the system is left in a state where some objects, such as
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   276
theorems, still refer to old versions of theories.  This may lead to the
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   277
error
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   278
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   279
Attempt to merge different versions of theories: \dots
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   280
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   281
Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   282
those not associated with a theory definition.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   283
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   284
Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   285
theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   286
theorems proved in {\tt orphan.ML}.  Then {\tt B.thy} should
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   287
mention this dependency as follows:
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   288
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   289
B = \(\ldots\) + "orphan" + \(\ldots\)
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   290
\end{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   291
Quoted strings stand for \ML{} files rather than theories, and merely
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   292
document additional dependencies.  Thus {\tt orphan} is not used in building
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   293
the base of theory~$B$, but {\tt orphan.ML} is loaded automatically
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   294
whenever~$B$ is (re)built.
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   295
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   296
The orphaned file may have its own dependencies.  If {\tt orphan.ML} depends
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   297
on theories or files $A@1$, \ldots, $A@n$, record this by creating a {\bf
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   298
  pseudo theory} in the file {\tt orphan.thy}:
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   299
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   300
orphan = \(A@1\) + \(\ldots\) + \(A@n\)
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   301
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   302
The resulting theory is a dummy, but it ensures that {\tt update} reloads
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   303
{\tt orphan} whenever it reloads one of the $A@i$.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   304
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   305
For an extensive example of how this technique can be used to link lots of
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   306
theory files and load them by just a few {\tt use_thy} calls, consult the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   307
sources of \ZF{} set theory.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   308
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
\section{Basic operations on theories}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   312
\subsection{Extracting an axiom or theorem from a theory}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   313
\index{theories!axioms of}\index{axioms!extracting}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   314
\index{theories!theorems of}\index{theorems!extracting}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   315
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   316
get_axiom : theory -> string -> thm
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   317
get_thm   : theory -> string -> thm
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   318
assume_ax : theory -> string -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   320
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   321
\item[\ttindexbold{get_axiom} $thy$ $name$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
returns an axiom with the given $name$ from $thy$, raising exception
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   323
\xdx{THEORY} if none exists.  Merging theories can cause several axioms
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
to have the same name; {\tt get_axiom} returns an arbitrary one.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   326
\item[\ttindexbold{get_thm} $thy$ $name$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   327
  is analogous to {\tt get_axiom}, but looks for a stored theorem.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   328
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   329
\item[\ttindexbold{assume_ax} $thy$ $formula$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   330
  reads the {\it formula} using the syntax of $thy$, following the same
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   331
  conventions as axioms in a theory definition.  You can thus pretend that
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   332
  {\it formula} is an axiom and use the resulting theorem like an axiom.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   333
  Actually {\tt assume_ax} returns an assumption;  \ttindex{result}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   334
  complains about additional assumptions, but \ttindex{uresult} does not.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
For example, if {\it formula} is
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   337
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   338
\hbox{\verb'?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]'}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   339
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   341
\subsection{Building a theory}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   342
\label{BuildingATheory}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   343
\index{theories!constructing|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   344
\begin{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   345
pure_thy       : theory
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   346
merge_theories : theory * theory -> theory
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   347
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   348
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   349
\item[\ttindexbold{pure_thy}] contains just the syntax and signature
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   350
  of the meta-logic.  There are no axioms: meta-level inferences are carried
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   351
  out by \ML\ functions.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   352
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   353
  theories $thy@1$ and $thy@2$.  The resulting theory contains all of the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   354
  syntax, signature and axioms of the constituent theories. Merging theories
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   355
  that contain different identification stamps of the same name fails with
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   356
  the following message
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   357
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   358
Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   359
\end{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   360
  This error may especially occur when a theory is redeclared --- say to
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   361
  change an incorrect axiom --- and bindings to old versions persist.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   362
  Isabelle ensures that old and new theories of the same name are not
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   363
  involved in a proof.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   364
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   365
%% FIXME
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   366
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   367
%  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   368
%  internally.  When a theory is redeclared, say to change an incorrect axiom,
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   369
%  bindings to the old axiom may persist.  Isabelle ensures that the old and
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   370
%  new theories are not involved in the same proof.  Attempting to combine
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   371
%  different theories having the same name $T$ yields the fatal error
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   372
%extend_theory  : theory -> string -> \(\cdots\) -> theory
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   373
%\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   374
%Attempt to merge different versions of theory: \(T\)
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   375
%\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   376
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   377
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   378
%% FIXME
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   379
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   380
%      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   381
%\hfill\break   %%% include if line is just too short
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   382
%is the \ML{} equivalent of the following theory definition:
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   383
%\begin{ttbox}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   384
%\(T\) = \(thy\) +
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   385
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   386
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   387
%default {\(d@1,\dots,d@r\)}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   388
%types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   389
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   390
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   391
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   392
%consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   393
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   394
%rules   \(name\) \(rule\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   395
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   396
%end
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   397
%\end{ttbox}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   398
%where
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   399
%\begin{tabular}[t]{l@{~=~}l}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   400
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   401
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   402
%$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   403
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   404
%\\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   405
%$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   406
%$rules$   & \tt[("$name$",$rule$),\dots]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   407
%\end{tabular}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   410
\subsection{Inspecting a theory}\label{sec:inspct-thy}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
\index{theories!inspecting|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   412
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
print_theory  : theory -> unit
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   414
axioms_of     : theory -> (string * thm) list
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   415
thms_of       : theory -> (string * thm) list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
parents_of    : theory -> theory list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
sign_of       : theory -> Sign.sg
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
stamps_of_thy : theory -> string ref list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
\end{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   420
These provide means of viewing a theory's components.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   421
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   422
\item[\ttindexbold{print_theory} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   423
prints the contents of $thy$ excluding the syntax related parts (which are
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   424
shown by {\tt print_syntax}).  The output is quite verbose.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   425
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   426
\item[\ttindexbold{axioms_of} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   427
returns the additional axioms of the most recent extend node of~$thy$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   429
\item[\ttindexbold{thms_of} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   430
similar to {\tt axioms_of}, but returns the stored theorems.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   432
\item[\ttindexbold{parents_of} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   433
returns the direct ancestors of~$thy$.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   434
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   435
\item[\ttindexbold{sign_of} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   436
returns the signature associated with~$thy$.  It is useful with functions
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   437
like {\tt read_instantiate_sg}, which take a signature as an argument.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   440
returns the identification \rmindex{stamps} of the signature associated
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   441
with~$thy$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   442
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
\section{Terms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
\index{terms|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   447
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
with six constructors: there are six kinds of term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
type indexname = string * int;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
infix 9 $;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
datatype term = Const of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
              | Free  of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
              | Var   of indexname * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
              | Bound of int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
              | Abs   of string * typ * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
              | op $  of term * term;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   459
\begin{ttdescription}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   460
\item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   461
  is the {\bf constant} with name~$a$ and type~$T$.  Constants include
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   462
  connectives like $\land$ and $\forall$ as well as constants like~0
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   463
  and~$Suc$.  Other constants may be required to define a logic's concrete
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   464
  syntax.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   466
\item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   467
  is the {\bf free variable} with name~$a$ and type~$T$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   469
\item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   470
  is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   471
  \mltydx{indexname} is a string paired with a non-negative index, or
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   472
  subscript; a term's scheme variables can be systematically renamed by
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   473
  incrementing their subscripts.  Scheme variables are essentially free
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   474
  variables, but may be instantiated during unification.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   476
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   477
  is the {\bf bound variable} with de Bruijn index~$i$, which counts the
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   478
  number of lambdas, starting from zero, between a variable's occurrence
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   479
  and its binding.  The representation prevents capture of variables.  For
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   480
  more information see de Bruijn \cite{debruijn72} or
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   481
  Paulson~\cite[page~336]{paulson91}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   483
\item[\ttindexbold{Abs}($a$, $T$, $u$)]
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   484
  \index{lambda abs@$\lambda$-abstractions|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   485
  is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   486
  variable has name~$a$ and type~$T$.  The name is used only for parsing
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   487
  and printing; it has no logical significance.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   489
\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   490
is the {\bf application} of~$t$ to~$u$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   491
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   492
Application is written as an infix operator to aid readability.
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   493
Here is an \ML\ pattern to recognize \FOL{} formulae of
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   495
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   500
\section{Variable binding}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   501
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   502
loose_bnos     : term -> int list
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   503
incr_boundvars : int -> term -> term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   504
abstract_over  : term*term -> term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   505
variant_abs    : string * typ * term -> string * term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   506
aconv          : term*term -> bool\hfill{\bf infix}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   507
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   508
These functions are all concerned with the de Bruijn representation of
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   509
bound variables.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   510
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   511
\item[\ttindexbold{loose_bnos} $t$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   512
  returns the list of all dangling bound variable references.  In
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   513
  particular, {\tt Bound~0} is loose unless it is enclosed in an
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   514
  abstraction.  Similarly {\tt Bound~1} is loose unless it is enclosed in
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   515
  at least two abstractions; if enclosed in just one, the list will contain
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   516
  the number 0.  A well-formed term does not contain any loose variables.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   517
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   518
\item[\ttindexbold{incr_boundvars} $j$]
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   519
  increases a term's dangling bound variables by the offset~$j$.  This is
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   520
  required when moving a subterm into a context where it is enclosed by a
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   521
  different number of abstractions.  Bound variables with a matching
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   522
  abstraction are unaffected.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   523
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   524
\item[\ttindexbold{abstract_over} $(v,t)$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   525
  forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   526
  It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   527
  correct index.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   528
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   529
\item[\ttindexbold{variant_abs} $(a,T,u)$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   530
  substitutes into $u$, which should be the body of an abstraction.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   531
  It replaces each occurrence of the outermost bound variable by a free
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   532
  variable.  The free variable has type~$T$ and its name is a variant
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   533
  of~$a$ chosen to be distinct from all constants and from all variables
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   534
  free in~$u$.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   535
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   536
\item[$t$ \ttindexbold{aconv} $u$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   537
  tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   538
  to renaming of bound variables.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   539
\begin{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   540
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   541
    Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   542
    if their names and types are equal.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   543
    (Variables having the same name but different types are thus distinct.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   544
    This confusing situation should be avoided!)
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   545
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   546
    Two bound variables are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   547
    if they have the same number.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   548
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   549
    Two abstractions are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   550
    if their bodies are, and their bound variables have the same type.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   551
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   552
    Two applications are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   553
    if the corresponding subterms are.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   554
\end{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   555
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   556
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   557
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   558
\section{Certified terms}\index{terms!certified|bold}\index{signatures}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   559
A term $t$ can be {\bf certified} under a signature to ensure that every type
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   560
in~$t$ is well-formed and every constant in~$t$ is a type instance of a
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   561
constant declared in the signature.  The term must be well-typed and its use
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   562
of bound variables must be well-formed.  Meta-rules such as {\tt forall_elim}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   563
take certified terms as arguments.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   565
Certified terms belong to the abstract type \mltydx{cterm}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
Elements of the type can only be created through the certification process.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
\subsection{Printing terms}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   570
\index{terms!printing of}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   571
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   572
     string_of_cterm :           cterm -> string
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
Sign.string_of_term  : Sign.sg -> term -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   575
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   576
\item[\ttindexbold{string_of_cterm} $ct$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
displays $ct$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   579
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
displays $t$ as a string, using the syntax of~$sign$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   581
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
\subsection{Making and inspecting certified terms}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   584
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   585
cterm_of   : Sign.sg -> term -> cterm
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   586
read_cterm : Sign.sg -> string * typ -> cterm
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   587
cert_axm   : Sign.sg -> string * term -> string * term
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   588
read_axm   : Sign.sg -> string * string -> string * term
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   589
rep_cterm  : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   591
\begin{ttdescription}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   592
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
certifies $t$ with respect to signature~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   595
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
reads the string~$s$ using the syntax of~$sign$, creating a certified term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
The term is checked to have type~$T$; this type also tells the parser what
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
kind of phrase to parse.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   600
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   601
certifies $t$ with respect to $sign$ as a meta-proposition and converts all
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   602
exceptions to an error, including the final message
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   603
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   604
The error(s) above occurred in axiom "\(name\)"
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   605
\end{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   606
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   607
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   608
similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   609
$sign$.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   610
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   611
\item[\ttindexbold{rep_cterm} $ct$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
decomposes $ct$ as a record containing its type, the term itself, its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
signature, and the maximum subscript of its unknowns.  The type and maximum
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
subscript are computed during certification.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   615
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   616
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   617
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   618
\section{Types}\index{types|bold}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   619
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   620
three constructor functions.  These correspond to type constructors, free
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   621
type variables and schematic type variables.  Types are classified by sorts,
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   622
which are lists of classes (representing an intersection).  A class is
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   623
represented by a string.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
type class = string;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
type sort  = class list;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   627
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
datatype typ = Type  of string * typ list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   629
             | TFree of string * sort
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   630
             | TVar  of indexname * sort;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
infixr 5 -->;
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   633
fun S --> T = Type ("fun", [S, T]);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   635
\begin{ttdescription}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   636
\item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   637
  applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   638
  Type constructors include~\tydx{fun}, the binary function space
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   639
  constructor, as well as nullary type constructors such as~\tydx{prop}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   640
  Other type constructors may be introduced.  In expressions, but not in
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   641
  patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   642
  types.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   644
\item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   645
  is the {\bf type variable} with name~$a$ and sort~$s$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   647
\item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   648
  is the {\bf type unknown} with indexname~$v$ and sort~$s$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   649
  Type unknowns are essentially free type variables, but may be
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   650
  instantiated during unification.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   651
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
\section{Certified types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
\index{types!certified|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   656
Certified types, which are analogous to certified terms, have type
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   657
\ttindexbold{ctyp}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
\subsection{Printing types}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   660
\index{types!printing of}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   661
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   662
     string_of_ctyp :           ctyp -> string
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
Sign.string_of_typ  : Sign.sg -> typ -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   665
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   666
\item[\ttindexbold{string_of_ctyp} $cT$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
displays $cT$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   669
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
displays $T$ as a string, using the syntax of~$sign$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   671
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
\subsection{Making and inspecting certified types}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   675
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   676
ctyp_of  : Sign.sg -> typ -> ctyp
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   677
rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   678
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   679
\begin{ttdescription}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   680
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
certifies $T$ with respect to signature~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   683
\item[\ttindexbold{rep_ctyp} $cT$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
decomposes $cT$ as a record containing the type itself and its signature.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   685
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
\index{theories|)}