doc-src/Ref/theories.tex
author lcp
Wed, 10 Nov 1993 05:00:57 +0100
changeset 104 d8205bb279a7
child 138 9ba8bff1addc
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
\chapter{Theories, Terms and Types} \label{theories}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\index{theories|(}\index{signatures|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
Theories organize the syntax, declarations and axioms of a mathematical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
development.  They are built, starting from the Pure theory, by extending
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
and merging existing theories.  They have the \ML{} type \ttindex{theory}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
Theory operations signal errors by raising exception \ttindex{THEORY},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
returning a message and a list of theories.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
Signatures, which contain information about sorts, types, constants and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
syntax, have the \ML{} type~\ttindexbold{Sign.sg}.  For identification,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
each signature carries a unique list of {\bf stamps}, which are~\ML{}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
references (to strings).  The strings serve as human-readable names; the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
references serve as unique identifiers.  Each primitive signature has a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
single stamp.  When two signatures are merged, their lists of stamps are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
also merged.  Every theory carries a unique signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
Terms and types are the underlying representation of logical syntax.  Their
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
\ML{} definitions are irrelevant to naive Isabelle users.  Programmers who wish
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
to extend Isabelle may need to know such details, say to code a tactic that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
looks for subgoals of a particular form.  Terms and types may be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
`certified' to be well-formed with respect to a given signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
\section{Defining Theories}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
\label{DefiningTheories}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
Theories can be defined either using concrete syntax or by calling certain
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
\ML-functions (see \S\ref{BuildingATheory}).  Figure~\ref{TheorySyntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
presents the concrete syntax for theories.  This grammar employs the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
following conventions: 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
\item Identifiers such as $theoryDef$ denote nonterminal symbols.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\item Text in {\tt typewriter font} denotes terminal symbols.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
\item \ldots{} indicates repetition of a phrase.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
\item A vertical bar~($|$) separates alternative phrases.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
\item Square [brackets] enclose optional phrases.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
\item $id$ stands for an Isabelle identifier.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
\item $string$ stands for an ML string, with its quotation marks.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
\item $k$ stands for a natural number.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
\item $text$ stands for arbitrary ML text.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
\begin{figure}[hp]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
$theoryDef$ &=& $id$ {\tt=} $id@1$ {\tt+} \dots {\tt+} $id@n$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
                            [{\tt+} $extension$]\\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
                [$rules$] {\tt end} [$ml$]\\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
$default$ &=& \ttindex{default} $sort$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
$sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
$name$ &=& $id$ ~~$|$~~ $string$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
               [{\tt(} $infix$ {\tt)}] \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
$infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
                [{\tt(} $mixfix$ {\tt)}] \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
$mixfix$ &=& $string$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
             [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
       &$|$& $infix$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
       &$|$& \ttindex{binder} $string$ $k$\\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
$rule$ &=& $id$ $string$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
$ml$ &=& \ttindex{ML} $text$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\caption{Theory Syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
\label{TheorySyntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
The different parts of a theory definition are interpreted as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\item[$theoryDef$] A theory has a name $id$ and is an extension of the union
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
  of existing theories $id@1$ \dots $id@n$ with new classes, types,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
  constants, syntax and axioms.  The basic theory, which contains only the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
  meta-logic, is called {\tt Pure}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
\item[$class$] The new class $id$ is declared as a subclass of existing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
  classes $id@1$ \dots $id@n$.  This rules out cyclic class structures.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
  Isabelle automatically computes the transitive closure of subclass
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
  hierarchies.  Hence it is not necessary to declare $c@1 < c@3$ in addition
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
  to $c@1 < c@2$ and $c@2 < c@3$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
\item[$default$] introduces $sort$ as the new default sort for type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
  variables.  Unconstrained type variables in an input string are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
  automatically constrained by $sort$; this does not apply to type variables
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
  created internally during type inference.  If omitted,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
  the default sort is the same as in the parent theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
  $id$ abbreviates the singleton set {\tt\{}$id${\tt\}}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
\item[$name$] is either an alphanumeric identifier or an arbitrary string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
\item[$typeDecl$] Each $name$ is declared as a new type constructor with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
  $k$ arguments.  Only binary type constructors can have infix status and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
  symbolic names ($string$).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
\item[$infix$] declares a type or constant to be an infix operator of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
  precedence $k$ associating to the left ({\tt infixl}) or right ({\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
    infixr}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
  is given the additional arity $arity$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
  be of type $string$.  For display purposes they can be annotated with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
  $mixfix$ declarations.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
  \dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
  where the $i$-th argument should go, $k@i$ is the minimum precedence of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
  the $i$-th argument, and $k$ the precedence of the construct.  The list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
  \hbox{\tt[$k@1$, \dots, $k@n$]} is optional.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
  Binary constants can be given infix status.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
  A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
    binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
  like $f(F)$; $p$ is the precedence of the construct.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
\item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
  names must be distinct.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\item[$ml$] This final part of a theory consists of ML code, 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
  typically for parse and print translations.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
The $mixfix$ and $ml$ sections are explained in more detail in the {\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
Defining Logics} chapter of the {\it Logics} manual.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
use_thy: string -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
Each theory definition must reside in a separate file.  Let the file {\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
  tf}{\tt.thy} contain the definition of a theory called $TF$ with rules named
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
$r@1$ \dots $r@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it tf\/}{\tt"} reads
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file {\tt.}{\it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
  tf}{\tt.thy.ML}, and reads the latter file.  This declares an {\ML}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
structure~$TF$ containing a component {\tt thy} for the new theory
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
and components $r@1$ \dots $r@n$ for the rules; it also contains the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
definitions of the {\tt ML} section if any.  Then {\tt use_thy}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
reads the file {\it tf}{\tt.ML}, if it exists; this file normally contains
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
proofs involving the new theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
\section{Basic operations on theories}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\subsection{Extracting an axiom from a theory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
\index{theories!extracting axioms|bold}\index{axioms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
get_axiom: theory -> string -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
assume_ax: theory -> string -> thm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
\item[\ttindexbold{get_axiom} $thy$ $name$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
returns an axiom with the given $name$ from $thy$, raising exception
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
\ttindex{THEORY} if none exists.  Merging theories can cause several axioms
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
to have the same name; {\tt get_axiom} returns an arbitrary one.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\item[\ttindexbold{assume_ax} $thy$ $formula$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
reads the {\it formula} using the syntax of $thy$, following the same
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
conventions as axioms in a theory definition.  You can thus pretend that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
You can use the resulting theorem like an axiom.  Note that 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
\ttindex{result} complains about additional assumptions, but 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
\ttindex{uresult} does not.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
For example, if {\it formula} is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
\subsection{Building a theory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
\label{BuildingATheory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
\index{theories!constructing|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
pure_thy: theory
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
merge_theories: theory * theory -> theory
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
extend_theory: theory -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
        -> (class * class list) list 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
           * sort
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
           * (string list * int)list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
           * (string list * (sort list * class))list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
           * (string list * string)list * sext option
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
        -> (string*string)list -> theory
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
a synonym for \hbox{\tt class list}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
  of the meta-logic.  There are no axioms: meta-level inferences are carried
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
  out by \ML\ functions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
  theories $thy@1$ and $thy@2$.  The resulting theory contains all types,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
  constants and axioms of the constituent theories; its default sort is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
  union of the default sorts of the constituent theories.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
\hfill\break   %%% include if line is just too short
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
is the \ML-equivalent of the following theory definition:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
\(T\) = \(thy\) +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
        \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
default {\(d@1,\dots,d@r\)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
        \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
        \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
        \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
rules   \(name\) \(rule\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
        \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
where
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
\begin{tabular}[t]{l@{~=~}l}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
$rules$   & \tt[("$name$",$rule$),\dots]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
as mixfix annotations to constants.  Using {\tt extend_theory}, new syntax can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
latter case is not documented.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
$T$ identifies the theory internally.  When a theory is redeclared, say to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
change an incorrect axiom, bindings to the old axiom may persist.  Isabelle
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
ensures that the old and new theories are not involved in the same proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
Attempting to combine different theories having the same name $T$ yields the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
fatal error
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
\begin{center} \tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
Attempt to merge different versions of theory: $T$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
\subsection{Inspecting a theory}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
\index{theories!inspecting|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
print_theory  : theory -> unit
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
axioms_of     : theory -> (string*thm)list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
parents_of    : theory -> theory list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
sign_of       : theory -> Sign.sg
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
stamps_of_thy : theory -> string ref list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
These provide a simple means of viewing a theory's components.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
Unfortunately, there is no direct connection between a theorem and its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
theory.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
\item[\ttindexbold{print_theory} {\it thy}]  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
prints the theory {\it thy\/} at the terminal as a set of identifiers.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
\item[\ttindexbold{axioms_of} $thy$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
returns the axioms of~$thy$ and its ancestors.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
\item[\ttindexbold{parents_of} $thy$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
returns the parents of~$thy$.  This list contains zero, one or two
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
elements, depending upon whether $thy$ is {\tt pure_thy}, 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
returns the stamps of the signature associated with~$thy$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\item[\ttindexbold{sign_of} $thy$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
returns the signature associated with~$thy$.  It is useful with functions
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
like {\tt read_instantiate_sg}, which take a signature as an argument.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
\section{Terms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
\index{terms|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
with six constructors: there are six kinds of term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
type indexname = string * int;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
infix 9 $;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
datatype term = Const of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
              | Free  of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
              | Var   of indexname * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
              | Bound of int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
              | Abs   of string * typ * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
              | op $  of term * term;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
\item[\ttindexbold{Const}($a$, $T$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
is the {\bf constant} with name~$a$ and type~$T$.  Constants include
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
connectives like $\land$ and $\forall$ (logical constants), as well as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
constants like~0 and~$Suc$.  Other constants may be required to define the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
concrete syntax of a logic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
\item[\ttindexbold{Free}($a$, $T$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
is the {\bf free variable} with name~$a$ and type~$T$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
\item[\ttindexbold{Var}($v$, $T$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
\ttindexbold{indexname} is a string paired with a non-negative index, or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
subscript; a term's scheme variables can be systematically renamed by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
incrementing their subscripts.  Scheme variables are essentially free
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
variables, but may be instantiated during unification.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
\item[\ttindexbold{Bound} $i$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
is the {\bf bound variable} with de Bruijn index~$i$, which counts the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
number of lambdas, starting from zero, between a variable's occurrence and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
its binding.  The representation prevents capture of variables.  For more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
information see de Bruijn \cite{debruijn72} or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
Paulson~\cite[page~336]{paulson91}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
\item[\ttindexbold{Abs}($a$, $T$, $u$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
is the {\bf abstraction} with body~$u$, and whose bound variable has
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
name~$a$ and type~$T$.  The name is used only for parsing and printing; it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
has no logical significance.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
\item[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
is the {\bf application} of~$t$ to~$u$.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
Application is written as an infix operator in order to aid readability.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
For example, here is an \ML{} pattern to recognize first-order formula of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
\section{Certified terms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
\index{terms!certified|bold}\index{signatures}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
A term $t$ can be {\bf certified} under a signature to ensure that every
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
type in~$t$ is declared in the signature and every constant in~$t$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
declared as a constant of the same type in the signature.  It must be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
well-typed and must not have any `loose' bound variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
references.\footnote{This concerns the internal representation of variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
certified terms as arguments.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
Certified terms belong to the abstract type \ttindexbold{Sign.cterm}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
Elements of the type can only be created through the certification process.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
\subsection{Printing terms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
\index{printing!terms|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
Sign.string_of_cterm :      Sign.cterm -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
Sign.string_of_term  : Sign.sg -> term -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
\item[\ttindexbold{Sign.string_of_cterm} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
displays $ct$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
displays $t$ as a string, using the syntax of~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
\subsection{Making and inspecting certified terms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
Sign.cterm_of   : Sign.sg -> term -> Sign.cterm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
Sign.rep_cterm  : Sign.cterm -> \{T:typ, t:term, 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
                                 sign: Sign.sg, maxidx:int\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
certifies $t$ with respect to signature~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
\item[\ttindexbold{Sign.read_cterm} $sign$ ($s$, $T$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
reads the string~$s$ using the syntax of~$sign$, creating a certified term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
The term is checked to have type~$T$; this type also tells the parser what
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
kind of phrase to parse.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
\item[\ttindexbold{Sign.rep_cterm} $ct$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
decomposes $ct$ as a record containing its type, the term itself, its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
signature, and the maximum subscript of its unknowns.  The type and maximum
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
subscript are computed during certification.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
\section{Types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
\index{types|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
datatype with three constructors.  Types are classified by sorts, which are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
lists of classes.  A class is represented by a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
type class = string;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
type sort  = class list;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
datatype typ = Type  of string * typ list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
             | TFree of string * sort
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
             | TVar  of indexname * sort;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
infixr 5 -->;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
fun S --> T = Type("fun",[S,T]);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
\item[\ttindexbold{Type}($a$, $Ts$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
Type constructors include~\ttindexbold{fun}, the binary function space
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
constructor, as well as nullary type constructors such
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
as~\ttindexbold{prop}.  Other type constructors may be introduced.  In
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
expressions, but not in patterns, \hbox{\tt$S$-->$T$} is a convenient
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
shorthand for function types.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\item[\ttindexbold{TFree}($a$, $s$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
is the {\bf free type variable} with name~$a$ and sort~$s$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
\item[\ttindexbold{TVar}($v$, $s$)] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
is the {\bf scheme type variable} with indexname~$v$ and sort~$s$.  Scheme
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
type variables are essentially free type variables, but may be instantiated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
during unification.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
\section{Certified types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
\index{types!certified|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
Certified types, which are analogous to certified terms, have type 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
\ttindexbold{Sign.ctyp}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
\subsection{Printing types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
\index{printing!types|bold}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
Sign.string_of_ctyp :      Sign.ctyp -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
Sign.string_of_typ  : Sign.sg -> typ -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
\item[\ttindexbold{Sign.string_of_ctyp} $cT$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
displays $cT$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
displays $T$ as a string, using the syntax of~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
\subsection{Making and inspecting certified types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
\begin{ttbox} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
Sign.ctyp_of  : Sign.sg -> typ -> Sign.ctyp
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
certifies $T$ with respect to signature~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
\item[\ttindexbold{Sign.rep_ctyp} $cT$] 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
decomposes $cT$ as a record containing the type itself and its signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
\index{theories|)}