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