doc-src/Ref/theories.tex
author wenzelm
Mon Aug 28 13:52:38 2000 +0200 (2000-08-28)
changeset 9695 ec7d7f877712
parent 8136 8c65f3ca13f2
child 11052 1379e49c0ee9
permissions -rw-r--r--
proper setup of iman.sty/extra.sty/ttbox.sty;
wenzelm@3201
     1
lcp@104
     2
%% $Id$
wenzelm@145
     3
lcp@104
     4
\chapter{Theories, Terms and Types} \label{theories}
lcp@104
     5
\index{theories|(}\index{signatures|bold}
wenzelm@9695
     6
\index{reading!axioms|see{\texttt{assume_ax}}} Theories organize the syntax,
wenzelm@9695
     7
declarations and axioms of a mathematical development.  They are built,
wenzelm@9695
     8
starting from the Pure or CPure theory, by extending and merging existing
wenzelm@9695
     9
theories.  They have the \ML\ type \mltydx{theory}.  Theory operations signal
wenzelm@9695
    10
errors by raising exception \xdx{THEORY}, returning a message and a list of
wenzelm@9695
    11
theories.
lcp@104
    12
lcp@104
    13
Signatures, which contain information about sorts, types, constants and
lcp@332
    14
syntax, have the \ML\ type~\mltydx{Sign.sg}.  For identification, each
wenzelm@864
    15
signature carries a unique list of \bfindex{stamps}, which are \ML\
lcp@324
    16
references to strings.  The strings serve as human-readable names; the
lcp@104
    17
references serve as unique identifiers.  Each primitive signature has a
lcp@104
    18
single stamp.  When two signatures are merged, their lists of stamps are
lcp@104
    19
also merged.  Every theory carries a unique signature.
lcp@104
    20
lcp@104
    21
Terms and types are the underlying representation of logical syntax.  Their
nipkow@275
    22
\ML\ definitions are irrelevant to naive Isabelle users.  Programmers who
nipkow@275
    23
wish to extend Isabelle may need to know such details, say to code a tactic
nipkow@275
    24
that looks for subgoals of a particular form.  Terms and types may be
lcp@104
    25
`certified' to be well-formed with respect to a given signature.
lcp@104
    26
lcp@324
    27
lcp@324
    28
\section{Defining theories}\label{sec:ref-defining-theories}
lcp@104
    29
wenzelm@6571
    30
Theories are defined via theory files $name$\texttt{.thy} (there are also
wenzelm@6571
    31
\ML-level interfaces which are only intended for people building advanced
wenzelm@6571
    32
theory definition packages).  Appendix~\ref{app:TheorySyntax} presents the
wenzelm@6571
    33
concrete syntax for theory files; here follows an explanation of the
wenzelm@6571
    34
constituent parts.
wenzelm@864
    35
\begin{description}
wenzelm@6568
    36
\item[{\it theoryDef}] is the full definition.  The new theory is called $id$.
paulson@8136
    37
  It is the union of the named \textbf{parent
wenzelm@3108
    38
    theories}\indexbold{theories!parent}, possibly extended with new
wenzelm@6568
    39
  components.  \thydx{Pure} and \thydx{CPure} are the basic theories, which
wenzelm@6568
    40
  contain only the meta-logic.  They differ just in their concrete syntax for
wenzelm@6568
    41
  function applications.
wenzelm@6571
    42
  
wenzelm@6571
    43
  The new theory begins as a merge of its parents.
wenzelm@6571
    44
  \begin{ttbox}
wenzelm@6571
    45
    Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
wenzelm@6571
    46
  \end{ttbox}
wenzelm@6571
    47
  This error may especially occur when a theory is redeclared --- say to
wenzelm@6571
    48
  change an inappropriate definition --- and bindings to old versions persist.
wenzelm@6571
    49
  Isabelle ensures that old and new theories of the same name are not involved
wenzelm@6571
    50
  in a proof.
lcp@324
    51
wenzelm@864
    52
\item[$classes$]
wenzelm@864
    53
  is a series of class declarations.  Declaring {\tt$id$ < $id@1$ \dots\
lcp@324
    54
    $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
lcp@324
    55
  id@n$.  This rules out cyclic class structures.  Isabelle automatically
lcp@324
    56
  computes the transitive closure of subclass hierarchies; it is not
paulson@6669
    57
  necessary to declare \texttt{c < e} in addition to \texttt{c < d} and \texttt{d <
lcp@324
    58
    e}.
lcp@324
    59
wenzelm@864
    60
\item[$default$]
wenzelm@864
    61
  introduces $sort$ as the new default sort for type variables.  This applies
wenzelm@864
    62
  to unconstrained type variables in an input string but not to type
wenzelm@864
    63
  variables created internally.  If omitted, the default sort is the listwise
wenzelm@864
    64
  union of the default sorts of the parent theories (i.e.\ their logical
wenzelm@864
    65
  intersection).
wenzelm@3108
    66
  
wenzelm@7168
    67
\item[$sort$] is a finite set of classes.  A single class $id$ abbreviates the
wenzelm@7168
    68
  sort $\{id\}$.
lcp@324
    69
wenzelm@864
    70
\item[$types$]
lcp@324
    71
  is a series of type declarations.  Each declares a new type constructor
lcp@324
    72
  or type synonym.  An $n$-place type constructor is specified by
lcp@324
    73
  $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
lcp@324
    74
  indicate the number~$n$.
lcp@324
    75
paulson@8136
    76
  A \textbf{type synonym}\indexbold{type synonyms} is an abbreviation
clasohm@1387
    77
  $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
clasohm@1387
    78
  be strings.
wenzelm@864
    79
wenzelm@864
    80
\item[$infix$]
paulson@8136
    81
  declares a type or constant to be an infix operator having priority $nat$
paulson@8136
    82
  and associating to the left (\texttt{infixl}) or right (\texttt{infixr}).
paulson@8136
    83
  Only 2-place type constructors can have infix status; an example is {\tt
wenzelm@3108
    84
  ('a,'b)~"*"~(infixr~20)}, which may express binary product types.
lcp@324
    85
wenzelm@3108
    86
\item[$arities$] is a series of type arity declarations.  Each assigns
wenzelm@3108
    87
  arities to type constructors.  The $name$ must be an existing type
wenzelm@3108
    88
  constructor, which is given the additional arity $arity$.
wenzelm@3108
    89
  
wenzelm@5369
    90
\item[$nonterminals$]\index{*nonterminal symbols} declares purely
wenzelm@5369
    91
  syntactic types to be used as nonterminal symbols of the context
wenzelm@5369
    92
  free grammar.
wenzelm@5369
    93
wenzelm@3108
    94
\item[$consts$] is a series of constant declarations.  Each new
wenzelm@3108
    95
  constant $name$ is given the specified type.  The optional $mixfix$
wenzelm@3108
    96
  annotations may attach concrete syntax to the constant.
wenzelm@3108
    97
  
wenzelm@3108
    98
\item[$syntax$] \index{*syntax section}\index{print mode} is a variant
wenzelm@3108
    99
  of $consts$ which adds just syntax without actually declaring
wenzelm@3108
   100
  logical constants.  This gives full control over a theory's context
paulson@3485
   101
  free grammar.  The optional $mode$ specifies the print mode where the
paulson@3485
   102
  mixfix productions should be added.  If there is no \texttt{output}
wenzelm@3108
   103
  option given, all productions are also added to the input syntax
wenzelm@3108
   104
  (regardless of the print mode).
lcp@324
   105
lcp@324
   106
\item[$mixfix$] \index{mixfix declarations}
lcp@324
   107
  annotations can take three forms:
nipkow@273
   108
  \begin{itemize}
nipkow@273
   109
  \item A mixfix template given as a $string$ of the form
nipkow@273
   110
    {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
lcp@324
   111
    indicates the position where the $i$-th argument should go.  The list
lcp@324
   112
    of numbers gives the priority of each argument.  The final number gives
lcp@324
   113
    the priority of the whole construct.
lcp@104
   114
lcp@324
   115
  \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
lcp@324
   116
    infix} status.
lcp@104
   117
lcp@324
   118
  \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
paulson@6669
   119
    binder} status.  The declaration \texttt{binder} $\cal Q$ $p$ causes
lcp@286
   120
  ${\cal Q}\,x.F(x)$ to be treated
lcp@286
   121
  like $f(F)$, where $p$ is the priority.
nipkow@273
   122
  \end{itemize}
lcp@324
   123
wenzelm@864
   124
\item[$trans$]
wenzelm@864
   125
  specifies syntactic translation rules (macros).  There are three forms:
paulson@6669
   126
  parse rules (\texttt{=>}), print rules (\texttt{<=}), and parse/print rules ({\tt
wenzelm@864
   127
  ==}).
lcp@324
   128
nipkow@1650
   129
\item[$rules$]
wenzelm@864
   130
  is a series of rule declarations.  Each has a name $id$ and the formula is
wenzelm@864
   131
  given by the $string$.  Rule names must be distinct within any single
wenzelm@3108
   132
  theory.
lcp@324
   133
paulson@1905
   134
\item[$defs$] is a series of definitions.  They are just like $rules$, except
paulson@1905
   135
  that every $string$ must be a definition (see below for details).
nipkow@1650
   136
nipkow@1650
   137
\item[$constdefs$] combines the declaration of constants and their
paulson@3485
   138
  definition.  The first $string$ is the type, the second the definition.
wenzelm@3108
   139
  
wenzelm@6625
   140
\item[$axclass$] \index{*axclass section} defines an \rmindex{axiomatic type
wenzelm@6625
   141
    class} \cite{Wenzel:1997:TPHOL} as the intersection of existing classes,
wenzelm@6625
   142
  with additional axioms holding.  Class axioms may not contain more than one
wenzelm@6625
   143
  type variable.  The class axioms (with implicit sort constraints added) are
wenzelm@6625
   144
  bound to the given names.  Furthermore a class introduction rule is
wenzelm@6625
   145
  generated, which is automatically employed by $instance$ to prove
wenzelm@6625
   146
  instantiations of this class.
wenzelm@3108
   147
  
wenzelm@3108
   148
\item[$instance$] \index{*instance section} proves class inclusions or
wenzelm@3108
   149
  type arities at the logical level and then transfers these to the
paulson@3485
   150
  type signature.  The instantiation is proven and checked properly.
wenzelm@3108
   151
  The user has to supply sufficient witness information: theorems
wenzelm@3108
   152
  ($longident$), axioms ($string$), or even arbitrary \ML{} tactic
wenzelm@3108
   153
  code $verbatim$.
nipkow@1650
   154
paulson@1846
   155
\item[$oracle$] links the theory to a trusted external reasoner.  It is
paulson@1846
   156
  allowed to create theorems, but each theorem carries a proof object
paulson@1846
   157
  describing the oracle invocation.  See \S\ref{sec:oracles} for details.
wenzelm@4543
   158
  
wenzelm@5369
   159
\item[$local$, $global$] change the current name declaration mode.
wenzelm@4543
   160
  Initially, theories start in $local$ mode, causing all names of
wenzelm@4543
   161
  types, constants, axioms etc.\ to be automatically qualified by the
wenzelm@4543
   162
  theory name.  Changing this to $global$ causes all names to be
wenzelm@4543
   163
  declared as short base names only.
wenzelm@4543
   164
  
wenzelm@4543
   165
  The $local$ and $global$ declarations act like switches, affecting
wenzelm@4543
   166
  all following theory sections until changed again explicitly.  Also
wenzelm@4543
   167
  note that the final state at the end of the theory will persist.  In
wenzelm@4543
   168
  particular, this determines how the names of theorems stored later
wenzelm@4543
   169
  on are handled.
wenzelm@5369
   170
  
wenzelm@5369
   171
\item[$setup$]\index{*setup!theory} applies a list of ML functions to
wenzelm@5369
   172
  the theory.  The argument should denote a value of type
wenzelm@5369
   173
  \texttt{(theory -> theory) list}.  Typically, ML packages are
wenzelm@5369
   174
  initialized in this way.
paulson@1846
   175
lcp@324
   176
\item[$ml$] \index{*ML section}
wenzelm@864
   177
  consists of \ML\ code, typically for parse and print translation functions.
lcp@104
   178
\end{description}
lcp@324
   179
%
wenzelm@864
   180
Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
paulson@6669
   181
declarations, translation rules and the \texttt{ML} section in more detail.
wenzelm@145
   182
wenzelm@145
   183
paulson@1905
   184
\subsection{Definitions}\indexbold{definitions}
paulson@1905
   185
paulson@8136
   186
\textbf{Definitions} are intended to express abbreviations.  The simplest
wenzelm@3108
   187
form of a definition is $f \equiv t$, where $f$ is a constant.
wenzelm@3108
   188
Isabelle also allows a derived forms where the arguments of~$f$ appear
wenzelm@3108
   189
on the left, abbreviating a string of $\lambda$-abstractions.
paulson@1905
   190
paulson@1905
   191
Isabelle makes the following checks on definitions:
paulson@1905
   192
\begin{itemize}
wenzelm@3108
   193
\item Arguments (on the left-hand side) must be distinct variables.
paulson@1905
   194
\item All variables on the right-hand side must also appear on the left-hand
paulson@1905
   195
  side. 
wenzelm@3108
   196
\item All type variables on the right-hand side must also appear on
wenzelm@3108
   197
  the left-hand side; this prohibits definitions such as {\tt
wenzelm@3108
   198
    (zero::nat) == length ([]::'a list)}.
paulson@1905
   199
\item The definition must not be recursive.  Most object-logics provide
paulson@1905
   200
  definitional principles that can be used to express recursion safely.
paulson@1905
   201
\end{itemize}
paulson@1905
   202
These checks are intended to catch the sort of errors that might be made
paulson@1905
   203
accidentally.  Misspellings, for instance, might result in additional
paulson@1905
   204
variables appearing on the right-hand side.  More elaborate checks could be
paulson@1905
   205
made, but the cost might be overly strict rules on declaration order, etc.
paulson@1905
   206
paulson@1905
   207
nipkow@275
   208
\subsection{*Classes and arities}
lcp@324
   209
\index{classes!context conditions}\index{arities!context conditions}
wenzelm@145
   210
lcp@286
   211
In order to guarantee principal types~\cite{nipkow-prehofer},
lcp@324
   212
arity declarations must obey two conditions:
wenzelm@145
   213
\begin{itemize}
wenzelm@3108
   214
\item There must not be any two declarations $ty :: (\vec{r})c$ and
wenzelm@3108
   215
  $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, this
wenzelm@3108
   216
  excludes the following:
wenzelm@145
   217
\begin{ttbox}
wenzelm@864
   218
arities
paulson@8136
   219
  foo :: (\{logic{\}}) logic
paulson@8136
   220
  foo :: (\{{\}})logic
wenzelm@145
   221
\end{ttbox}
lcp@286
   222
wenzelm@145
   223
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
wenzelm@145
   224
  (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
wenzelm@145
   225
  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
wenzelm@145
   226
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
wenzelm@3108
   227
expresses that the set of types represented by $s'$ is a subset of the
wenzelm@3108
   228
set of types represented by $s$.  Assuming $term \preceq logic$, the
wenzelm@3108
   229
following is forbidden:
wenzelm@145
   230
\begin{ttbox}
wenzelm@864
   231
arities
paulson@8136
   232
  foo :: (\{logic{\}})logic
paulson@8136
   233
  foo :: (\{{\}})term
wenzelm@145
   234
\end{ttbox}
lcp@286
   235
wenzelm@145
   236
\end{itemize}
wenzelm@145
   237
lcp@104
   238
wenzelm@6568
   239
\section{The theory loader}\label{sec:more-theories}
wenzelm@6568
   240
\index{theories!reading}\index{files!reading}
wenzelm@6568
   241
wenzelm@6568
   242
Isabelle's theory loader manages dependencies of the internal graph of theory
wenzelm@6568
   243
nodes (the \emph{theory database}) and the external view of the file system.
wenzelm@6568
   244
See \S\ref{sec:intro-theories} for its most basic commands, such as
wenzelm@6568
   245
\texttt{use_thy}.  There are a few more operations available.
wenzelm@6568
   246
wenzelm@864
   247
\begin{ttbox}
wenzelm@6568
   248
use_thy_only    : string -> unit
wenzelm@7136
   249
update_thy_only : string -> unit
wenzelm@6568
   250
touch_thy       : string -> unit
wenzelm@6658
   251
remove_thy      : string -> unit
paulson@8136
   252
delete_tmpfiles : bool ref \hfill\textbf{initially true}
lcp@286
   253
\end{ttbox}
lcp@286
   254
lcp@324
   255
\begin{ttdescription}
wenzelm@6569
   256
\item[\ttindexbold{use_thy_only} "$name$";] is similar to \texttt{use_thy},
wenzelm@6569
   257
  but processes the actual theory file $name$\texttt{.thy} only, ignoring
wenzelm@6568
   258
  $name$\texttt{.ML}.  This might be useful in replaying proof scripts by hand
wenzelm@6568
   259
  from the very beginning, starting with the fresh theory.
wenzelm@6568
   260
  
wenzelm@7136
   261
\item[\ttindexbold{update_thy_only} "$name$";] is similar to
wenzelm@7136
   262
  \texttt{update_thy}, but processes the actual theory file
wenzelm@7136
   263
  $name$\texttt{.thy} only, ignoring $name$\texttt{.ML}.
wenzelm@7136
   264
wenzelm@6569
   265
\item[\ttindexbold{touch_thy} "$name$";] marks theory node $name$ of the
wenzelm@6568
   266
  internal graph as outdated.  While the theory remains usable, subsequent
wenzelm@6568
   267
  operations such as \texttt{use_thy} may cause a reload.
wenzelm@6568
   268
  
wenzelm@6658
   269
\item[\ttindexbold{remove_thy} "$name$";] deletes theory node $name$,
wenzelm@6658
   270
  including \emph{all} of its descendants.  Beware!  This is a quick way to
wenzelm@6658
   271
  dispose a large number of theories at once.  Note that {\ML} bindings to
wenzelm@6658
   272
  theorems etc.\ of removed theories may still persist.
wenzelm@6658
   273
  
wenzelm@6568
   274
\item[reset \ttindexbold{delete_tmpfiles};] processing theory files usually
wenzelm@6568
   275
  involves temporary {\ML} files to be created.  By default, these are deleted
wenzelm@6568
   276
  afterwards.  Resetting the \texttt{delete_tmpfiles} flag inhibits this,
wenzelm@6568
   277
  leaving the generated code for debugging purposes.  The basic location for
wenzelm@6568
   278
  temporary files is determined by the \texttt{ISABELLE_TMP} environment
wenzelm@6571
   279
  variable (which is private to the running Isabelle process and may be
wenzelm@6568
   280
  retrieved by \ttindex{getenv} from {\ML}).
lcp@324
   281
\end{ttdescription}
clasohm@138
   282
wenzelm@6568
   283
\medskip Theory and {\ML} files are located by skimming through the
wenzelm@6568
   284
directories listed in Isabelle's internal load path, which merely contains the
wenzelm@6568
   285
current directory ``\texttt{.}'' by default.  The load path may be accessed by
wenzelm@6568
   286
the following operations.
lcp@332
   287
wenzelm@864
   288
\begin{ttbox}
wenzelm@6568
   289
show_path: unit -> string list
wenzelm@6568
   290
add_path: string -> unit
wenzelm@6568
   291
del_path: string -> unit
wenzelm@6568
   292
reset_path: unit -> unit
wenzelm@7440
   293
with_path: string -> ('a -> 'b) -> 'a -> 'b
lcp@286
   294
\end{ttbox}
lcp@286
   295
lcp@324
   296
\begin{ttdescription}
wenzelm@6568
   297
\item[\ttindexbold{show_path}();] displays the load path components in
wenzelm@6571
   298
  canonical string representation (which is always according to Unix rules).
wenzelm@6568
   299
  
wenzelm@6569
   300
\item[\ttindexbold{add_path} "$dir$";] adds component $dir$ to the beginning
wenzelm@6569
   301
  of the load path.
wenzelm@6568
   302
  
wenzelm@6569
   303
\item[\ttindexbold{del_path} "$dir$";] removes any occurrences of component
wenzelm@6568
   304
  $dir$ from the load path.
wenzelm@6568
   305
  
wenzelm@6568
   306
\item[\ttindexbold{reset_path}();] resets the load path to ``\texttt{.}''
wenzelm@6568
   307
  (current directory) only.
wenzelm@7440
   308
  
wenzelm@7440
   309
\item[\ttindexbold{with_path} "$dir$" $f$ $x$;] temporarily adds component
wenzelm@7440
   310
  $dir$ to the beginning of the load path before executing $(f~x)$.
wenzelm@7440
   311
lcp@324
   312
\end{ttdescription}
lcp@286
   313
wenzelm@7440
   314
Furthermore, in operations referring indirectly to some file (e.g.\ 
wenzelm@7440
   315
\texttt{use_dir}) the argument may be prefixed by a directory that will be
wenzelm@7440
   316
temporarily appended to the load path, too.
lcp@104
   317
lcp@104
   318
paulson@6669
   319
\section{Locales}
paulson@6669
   320
\label{Locales}
paulson@6669
   321
paulson@6669
   322
Locales \cite{kammueller-locales} are a concept of local proof contexts.  They
paulson@6669
   323
are introduced as named syntactic objects within theories and can be
paulson@6669
   324
opened in any descendant theory.
paulson@6669
   325
paulson@6669
   326
\subsection{Declaring Locales}
paulson@6669
   327
paulson@6669
   328
A locale is declared in a theory section that starts with the
paulson@6669
   329
keyword \texttt{locale}.  It consists typically of three parts, the
paulson@6669
   330
\texttt{fixes} part, the \texttt{assumes} part, and the \texttt{defines} part.
paulson@6669
   331
Appendix \ref{app:TheorySyntax} presents the full syntax.
paulson@6669
   332
paulson@6669
   333
\subsubsection{Parts of Locales}
paulson@6669
   334
paulson@6669
   335
The subsection introduced by the keyword \texttt{fixes} declares the locale
paulson@6669
   336
constants in a way that closely resembles a global \texttt{consts}
paulson@6669
   337
declaration.  In particular, there may be an optional pretty printing syntax
paulson@6669
   338
for the locale constants.
paulson@6669
   339
paulson@6669
   340
The subsequent \texttt{assumes} part specifies the locale rules.  They are
paulson@6669
   341
defined like \texttt{rules}: by an identifier followed by the rule
paulson@6669
   342
given as a string.  Locale rules admit the statement of local assumptions
paulson@6669
   343
about the locale constants.  The \texttt{assumes} part is optional.  Non-fixed
paulson@6669
   344
variables in locale rules are automatically bound by the universal quantifier
paulson@6669
   345
\texttt{!!} of the meta-logic.
paulson@6669
   346
paulson@6669
   347
Finally, the \texttt{defines} part introduces the definitions that are
paulson@6669
   348
available in the locale.  Locale constants declared in the \texttt{fixes}
paulson@6669
   349
section are defined using the meta-equality \texttt{==}.  If the
paulson@6669
   350
locale constant is a functiond then its definition can (as usual) have
paulson@6669
   351
variables on the left-hand side acting as formal parameters; they are
paulson@6669
   352
considered as schematic variables and are automatically generalized by
paulson@6669
   353
universal quantification of the meta-logic.  The right hand side of a
paulson@6669
   354
definition must not contain variables that are not already on the left hand
paulson@6669
   355
side.  In so far locale definitions behave like theory level definitions.
paulson@6669
   356
However, the locale concept realizes \emph{dependent definitions}: any variable
paulson@6669
   357
that is fixed as a locale constant can occur on the right hand side of
paulson@6669
   358
definitions.  For an illustration of these dependent definitions see the
paulson@6669
   359
occurrence of the locale constant \texttt{G} on the right hand side of the
paulson@6669
   360
definitions of the locale \texttt{group} below.  Naturally, definitions can
paulson@6669
   361
already use the syntax of the locale constants in the \texttt{fixes}
paulson@6669
   362
subsection.  The \texttt{defines} part is, as the \texttt{assumes} part,
paulson@6669
   363
optional.
paulson@6669
   364
paulson@6669
   365
\subsubsection{Example for Definition}
paulson@6669
   366
The concrete syntax of locale definitions is demonstrated by example below.
paulson@6669
   367
paulson@6669
   368
Locale \texttt{group} assumes the definition of groups in a theory
paulson@6669
   369
file\footnote{This and other examples are from \texttt{HOL/ex}.}.  A locale
paulson@6669
   370
defining a convenient proof environment for group related proofs may be
paulson@6669
   371
added to the theory as follows:
paulson@6669
   372
\begin{ttbox}
paulson@6669
   373
  locale group =
paulson@6669
   374
    fixes 
paulson@6669
   375
      G         :: "'a grouptype"
paulson@6669
   376
      e         :: "'a"
paulson@6669
   377
      binop     :: "'a => 'a => 'a"        (infixr "#" 80)
paulson@6669
   378
      inv       :: "'a => 'a"              ("i(_)" [90] 91)
paulson@6669
   379
    assumes
paulson@6669
   380
      Group_G   "G: Group"
paulson@6669
   381
    defines
paulson@6669
   382
      e_def     "e == unit G"
paulson@6669
   383
      binop_def "x # y == bin_op G x y"
paulson@6669
   384
      inv_def   "i(x) == inverse G x"
paulson@6669
   385
\end{ttbox}
paulson@6669
   386
paulson@6669
   387
\subsubsection{Polymorphism}
paulson@6669
   388
paulson@6669
   389
In contrast to polymorphic definitions in theories, the use of the
paulson@6669
   390
same type variable for the declaration of different locale constants in the
paulson@6669
   391
fixes part means \emph{the same} type.  In other words, the scope of the
paulson@6669
   392
polymorphic variables is extended over all constant declarations of a locale.
paulson@6669
   393
In the above example \texttt{'a} refers to the same type which is fixed inside
paulson@6669
   394
the locale.  In an exported theorem (see \S\ref{sec:locale-export}) the
paulson@6669
   395
constructors of locale \texttt{group} are polymorphic, yet only simultaneously
paulson@6669
   396
instantiatable.
paulson@6669
   397
paulson@6669
   398
\subsubsection{Nested Locales}
paulson@6669
   399
paulson@6669
   400
A locale can be defined as the extension of a previously defined
paulson@6669
   401
locale.  This operation of extension is optional and is syntactically
paulson@6669
   402
expressed as 
paulson@6669
   403
\begin{ttbox}
paulson@6669
   404
locale foo = bar + ...
paulson@6669
   405
\end{ttbox}
paulson@6669
   406
The locale \texttt{foo} builds on the constants and syntax of the locale {\tt
paulson@6669
   407
bar}.  That is, all contents of the locale \texttt{bar} can be used in
paulson@6669
   408
definitions and rules of the corresponding parts of the locale {\tt
paulson@6669
   409
foo}.  Although locale \texttt{foo} assumes the \texttt{fixes} part of \texttt{bar} it
paulson@6669
   410
does not automatically subsume its rules and definitions.  Normally, one
paulson@6669
   411
expects to use locale \texttt{foo} only if locale \texttt{bar} is already
paulson@6669
   412
active.  These aspects of use and activation of locales are considered in the
paulson@6669
   413
subsequent section.
paulson@6669
   414
paulson@6669
   415
paulson@6669
   416
\subsection{Locale Scope}
paulson@6669
   417
paulson@6669
   418
Locales are by default inactive, but they can be invoked.  The list of
paulson@6669
   419
currently active locales is called \emph{scope}.  The process of activating
paulson@6669
   420
them is called \emph{opening}; the reverse is \emph{closing}.
paulson@6669
   421
paulson@6669
   422
\subsubsection{Scope}
paulson@6669
   423
The locale scope is part of each theory.  It is a dynamic stack containing
paulson@6669
   424
all active locales at a certain point in an interactive session.
paulson@6669
   425
The scope lives until all locales are explicitly closed.  At one time there
paulson@6669
   426
can be more than one locale open.  The contents of these various active
paulson@6669
   427
locales are all visible in the scope.  In case of nested locales for example,
paulson@6669
   428
the nesting is actually reflected to the scope, which contains the nested
paulson@6669
   429
locales as layers.  To check the state of the scope during a development the
paulson@6669
   430
function \texttt{Print\_scope} may be used.  It displays the names of all open
paulson@6669
   431
locales on the scope.  The function \texttt{print\_locales} applied to a theory
paulson@6669
   432
displays all locales contained in that theory and in addition also the
paulson@6669
   433
current scope.
paulson@6669
   434
paulson@6669
   435
The scope is manipulated by the commands for opening and closing of locales. 
paulson@6669
   436
paulson@6669
   437
\subsubsection{Opening}
paulson@6669
   438
Locales can be \emph{opened} at any point during a session where
paulson@6669
   439
we want to prove theorems concerning the locale.  Opening a locale means
paulson@6669
   440
making its contents visible by pushing it onto the scope of the current
paulson@6669
   441
theory.  Inside a scope of opened locales, theorems can use all definitions and
paulson@6669
   442
rules contained in the locales on the scope.  The rules and definitions may
paulson@6669
   443
be accessed individually using the function \ttindex{thm}.  This function is
paulson@6669
   444
applied to the names assigned to locale rules and definitions as
paulson@6669
   445
strings.  The opening command is called \texttt{Open\_locale} and takes the 
paulson@6669
   446
name of the locale to be opened as its argument.
paulson@6669
   447
paulson@6669
   448
If one opens a locale \texttt{foo} that is defined by extension from locale
paulson@6669
   449
\texttt{bar}, the function \texttt{Open\_locale} checks if locale \texttt{bar}
paulson@6669
   450
is open.  If so, then it just opens \texttt{foo}, if not, then it prints a
paulson@6669
   451
message and opens \texttt{bar} before opening \texttt{foo}.  Naturally, this
paulson@6669
   452
carries on, if \texttt{bar} is again an extension.
paulson@6669
   453
paulson@6669
   454
\subsubsection{Closing}
paulson@6669
   455
paulson@6669
   456
\emph{Closing} means to cancel the last opened locale, pushing it out of the
paulson@6669
   457
scope.  Theorems proved during the life cycle of this locale will be disabled,
paulson@6669
   458
unless they have been explicitly exported, as described below.  However, when
paulson@6669
   459
the same locale is opened again these theorems may be used again as well,
paulson@6669
   460
provided that they were saved as theorems in the first place, using
paulson@6669
   461
\texttt{qed} or ML assignment.  The command \texttt{Close\_locale} takes a
paulson@6669
   462
locale name as a string and checks if this locale is actually the topmost
paulson@6669
   463
locale on the scope.  If this is the case, it removes this locale, otherwise
paulson@6669
   464
it prints a warning message and does not change the scope.
paulson@6669
   465
paulson@6669
   466
\subsubsection{Export of Theorems}
paulson@6669
   467
\label{sec:locale-export}
paulson@6669
   468
paulson@6669
   469
Export of theorems transports theorems out of the scope of locales.  Locale
paulson@6669
   470
rules that have been used in the proof of an exported theorem inside the
paulson@6669
   471
locale are carried by the exported form of the theorem as its individual
paulson@6669
   472
meta-assumptions.  The locale constants are universally quantified variables
paulson@6669
   473
in these theorems, hence such theorems can be instantiated individually.
paulson@6669
   474
Definitions become unfolded; locale constants that were merely used for
paulson@6669
   475
definitions vanish.  Logically, exporting corresponds to a combined
paulson@6669
   476
application of introduction rules for implication and universal
paulson@6669
   477
quantification.  Exporting forms a kind of normalization of theorems in a
paulson@6669
   478
locale scope.
paulson@6669
   479
paulson@6669
   480
According to the possibility of nested locales there are two different forms
paulson@6669
   481
of export.  The first one is realized by the function \texttt{export} that
paulson@6669
   482
exports theorems through all layers of opened locales of the scope.  Hence,
paulson@6669
   483
the application of export to a theorem yields a theorem of the global level,
paulson@6669
   484
that is, the current theory context without any local assumptions or
paulson@6669
   485
definitions.
paulson@6669
   486
paulson@6669
   487
When locales are nested we might want to export a theorem, not to the global
paulson@6669
   488
level of the current theory but just to the previous level.  The other export
paulson@6669
   489
function, \texttt{Export}, transports theorems one level up in the scope; the
paulson@6669
   490
theorem still uses locale constants, definitions and rules of the locales
paulson@6669
   491
underneath.
paulson@6669
   492
paulson@6669
   493
\subsection{Functions for Locales}
paulson@6669
   494
\label{Syntax}
paulson@6669
   495
\index{locales!functions}
paulson@6669
   496
paulson@6669
   497
Here is a quick reference list of locale functions.
paulson@6669
   498
\begin{ttbox}
paulson@6669
   499
  Open_locale  : xstring -> unit 
paulson@6669
   500
  Close_locale : xstring -> unit
paulson@6669
   501
  export       :     thm -> thm
paulson@6669
   502
  Export       :     thm -> thm
paulson@6669
   503
  thm          : xstring -> thm
paulson@6669
   504
  Print_scope  :    unit -> unit
paulson@6669
   505
  print_locales:  theory -> unit
paulson@6669
   506
\end{ttbox}
paulson@6669
   507
\begin{ttdescription}
paulson@6669
   508
\item[\ttindexbold{Open_locale} $xstring$] 
paulson@6669
   509
    opens the locale {\it xstring}, adding it to the scope of the theory of the
paulson@6669
   510
  current context.  If the opened locale is built by extension, the ancestors
paulson@6669
   511
  are opened automatically.
paulson@6669
   512
  
paulson@6669
   513
\item[\ttindexbold{Close_locale} $xstring$] eliminates the locale {\it
paulson@6669
   514
    xstring} from the scope if it is the topmost item on it, otherwise it does
paulson@6669
   515
  not change the scope and produces a warning.
paulson@6669
   516
paulson@6669
   517
\item[\ttindexbold{export} $thm$] locale definitions become expanded in {\it
paulson@6669
   518
    thm} and locale rules that were used in the proof of {\it thm} become part
paulson@6669
   519
  of its individual assumptions.  This normalization happens with respect to
paulson@6669
   520
  \emph{all open locales} on the scope.
paulson@6669
   521
  
paulson@6669
   522
\item[\ttindexbold{Export} $thm$] works like \texttt{export} but normalizes
paulson@6669
   523
  theorems only up to the previous level of locales on the scope.
paulson@6669
   524
  
paulson@6669
   525
\item[\ttindexbold{thm} $xstring$] applied to the name of a locale definition
paulson@6669
   526
  or rule it returns the definition as a theorem.
paulson@6669
   527
  
paulson@6669
   528
\item[\ttindexbold{Print_scope}()] prints the names of the locales in the
paulson@6669
   529
  current scope of the current theory context.
paulson@6669
   530
  
paulson@6669
   531
\item[\ttindexbold{print_locale} $theory$] prints all locales that are
paulson@6669
   532
  contained in {\it theory} directly or indirectly.  It also displays the
paulson@6669
   533
  current scope similar to \texttt{Print\_scope}.
paulson@6669
   534
\end{ttdescription}
paulson@6669
   535
paulson@6669
   536
clasohm@866
   537
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
wenzelm@4384
   538
wenzelm@4384
   539
\subsection{*Theory inclusion}
wenzelm@4384
   540
\begin{ttbox}
wenzelm@4384
   541
subthy      : theory * theory -> bool
wenzelm@4384
   542
eq_thy      : theory * theory -> bool
wenzelm@4384
   543
transfer    : theory -> thm -> thm
wenzelm@4384
   544
transfer_sg : Sign.sg -> thm -> thm
wenzelm@4384
   545
\end{ttbox}
wenzelm@4384
   546
wenzelm@4384
   547
Inclusion and equality of theories is determined by unique
wenzelm@4384
   548
identification stamps that are created when declaring new components.
wenzelm@4384
   549
Theorems contain a reference to the theory (actually to its signature)
wenzelm@4384
   550
they have been derived in.  Transferring theorems to super theories
wenzelm@4384
   551
has no logical significance, but may affect some operations in subtle
wenzelm@4384
   552
ways (e.g.\ implicit merges of signatures when applying rules, or
wenzelm@4384
   553
pretty printing of theorems).
wenzelm@4384
   554
wenzelm@4384
   555
\begin{ttdescription}
wenzelm@4384
   556
wenzelm@4384
   557
\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$
wenzelm@4384
   558
  is included in $thy@2$ wrt.\ identification stamps.
wenzelm@4384
   559
wenzelm@4384
   560
\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$
wenzelm@4384
   561
  is exactly the same as $thy@2$.
wenzelm@4384
   562
wenzelm@4384
   563
\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
wenzelm@4384
   564
  theory $thy$, provided the latter includes the theory of $thm$.
wenzelm@4384
   565
  
wenzelm@4384
   566
\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to
wenzelm@4384
   567
  \texttt{transfer}, but identifies the super theory via its
wenzelm@4384
   568
  signature.
wenzelm@4384
   569
wenzelm@4384
   570
\end{ttdescription}
wenzelm@4384
   571
wenzelm@4384
   572
wenzelm@6571
   573
\subsection{*Primitive theories}
wenzelm@864
   574
\begin{ttbox}
wenzelm@4317
   575
ProtoPure.thy  : theory
wenzelm@3108
   576
Pure.thy       : theory
wenzelm@3108
   577
CPure.thy      : theory
lcp@286
   578
\end{ttbox}
wenzelm@3108
   579
\begin{description}
wenzelm@4317
   580
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
wenzelm@4317
   581
  \ttindexbold{CPure.thy}] contain the syntax and signature of the
wenzelm@4317
   582
  meta-logic.  There are basically no axioms: meta-level inferences
wenzelm@4317
   583
  are carried out by \ML\ functions.  \texttt{Pure} and \texttt{CPure}
wenzelm@4317
   584
  just differ in their concrete syntax of prefix function application:
wenzelm@4317
   585
  $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
wenzelm@4317
   586
  \texttt{CPure}.  \texttt{ProtoPure} is their common parent,
wenzelm@4317
   587
  containing no syntax for printing prefix applications at all!
wenzelm@6571
   588
wenzelm@864
   589
%% FIXME
nipkow@478
   590
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
nipkow@478
   591
%  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory
nipkow@478
   592
%  internally.  When a theory is redeclared, say to change an incorrect axiom,
nipkow@478
   593
%  bindings to the old axiom may persist.  Isabelle ensures that the old and
nipkow@478
   594
%  new theories are not involved in the same proof.  Attempting to combine
nipkow@478
   595
%  different theories having the same name $T$ yields the fatal error
nipkow@478
   596
%extend_theory  : theory -> string -> \(\cdots\) -> theory
wenzelm@864
   597
%\begin{ttbox}
wenzelm@864
   598
%Attempt to merge different versions of theory: \(T\)
wenzelm@864
   599
%\end{ttbox}
wenzelm@3108
   600
\end{description}
lcp@286
   601
wenzelm@864
   602
%% FIXME
nipkow@275
   603
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
nipkow@275
   604
%      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
nipkow@275
   605
%\hfill\break   %%% include if line is just too short
lcp@286
   606
%is the \ML{} equivalent of the following theory definition:
nipkow@275
   607
%\begin{ttbox}
nipkow@275
   608
%\(T\) = \(thy\) +
nipkow@275
   609
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
nipkow@275
   610
%        \dots
nipkow@275
   611
%default {\(d@1,\dots,d@r\)}
nipkow@275
   612
%types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
nipkow@275
   613
%        \dots
nipkow@275
   614
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
nipkow@275
   615
%        \dots
nipkow@275
   616
%consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
nipkow@275
   617
%        \dots
nipkow@275
   618
%rules   \(name\) \(rule\)
nipkow@275
   619
%        \dots
nipkow@275
   620
%end
nipkow@275
   621
%\end{ttbox}
nipkow@275
   622
%where
nipkow@275
   623
%\begin{tabular}[t]{l@{~=~}l}
nipkow@275
   624
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
nipkow@275
   625
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
nipkow@275
   626
%$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
nipkow@275
   627
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
nipkow@275
   628
%\\
nipkow@275
   629
%$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
nipkow@275
   630
%$rules$   & \tt[("$name$",$rule$),\dots]
nipkow@275
   631
%\end{tabular}
lcp@104
   632
lcp@104
   633
wenzelm@864
   634
\subsection{Inspecting a theory}\label{sec:inspct-thy}
lcp@104
   635
\index{theories!inspecting|bold}
wenzelm@864
   636
\begin{ttbox}
wenzelm@4317
   637
print_syntax        : theory -> unit
wenzelm@4317
   638
print_theory        : theory -> unit
wenzelm@4317
   639
parents_of          : theory -> theory list
wenzelm@4317
   640
ancestors_of        : theory -> theory list
wenzelm@4317
   641
sign_of             : theory -> Sign.sg
wenzelm@4317
   642
Sign.stamp_names_of : Sign.sg -> string list
lcp@104
   643
\end{ttbox}
wenzelm@864
   644
These provide means of viewing a theory's components.
lcp@324
   645
\begin{ttdescription}
wenzelm@3108
   646
\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
wenzelm@3108
   647
  (grammar, macros, translation functions etc., see
wenzelm@3108
   648
  page~\pageref{pg:print_syn} for more details).
wenzelm@3108
   649
  
wenzelm@3108
   650
\item[\ttindexbold{print_theory} $thy$] prints the logical parts of
wenzelm@3108
   651
  $thy$, excluding the syntax.
wenzelm@4317
   652
  
wenzelm@4317
   653
\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
wenzelm@4317
   654
  of~$thy$.
wenzelm@4317
   655
  
wenzelm@4317
   656
\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
wenzelm@4317
   657
  (not including $thy$ itself).
wenzelm@4317
   658
  
wenzelm@4317
   659
\item[\ttindexbold{sign_of} $thy$] returns the signature associated
wenzelm@4317
   660
  with~$thy$.  It is useful with functions like {\tt
wenzelm@4317
   661
    read_instantiate_sg}, which take a signature as an argument.
wenzelm@4317
   662
  
wenzelm@4317
   663
\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
wenzelm@4317
   664
  returns the names of the identification \rmindex{stamps} of ax
wenzelm@4317
   665
  signature.  These coincide with the names of its full ancestry
wenzelm@4317
   666
  including that of $sg$ itself.
lcp@104
   667
lcp@324
   668
\end{ttdescription}
lcp@104
   669
clasohm@1369
   670
lcp@104
   671
\section{Terms}
lcp@104
   672
\index{terms|bold}
lcp@324
   673
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
wenzelm@3108
   674
with six constructors:
lcp@104
   675
\begin{ttbox}
lcp@104
   676
type indexname = string * int;
lcp@104
   677
infix 9 $;
lcp@104
   678
datatype term = Const of string * typ
lcp@104
   679
              | Free  of string * typ
lcp@104
   680
              | Var   of indexname * typ
lcp@104
   681
              | Bound of int
lcp@104
   682
              | Abs   of string * typ * term
lcp@104
   683
              | op $  of term * term;
lcp@104
   684
\end{ttbox}
lcp@324
   685
\begin{ttdescription}
wenzelm@4317
   686
\item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
paulson@8136
   687
  is the \textbf{constant} with name~$a$ and type~$T$.  Constants include
lcp@286
   688
  connectives like $\land$ and $\forall$ as well as constants like~0
lcp@286
   689
  and~$Suc$.  Other constants may be required to define a logic's concrete
wenzelm@864
   690
  syntax.
lcp@104
   691
wenzelm@4317
   692
\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
paulson@8136
   693
  is the \textbf{free variable} with name~$a$ and type~$T$.
lcp@104
   694
wenzelm@4317
   695
\item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
paulson@8136
   696
  is the \textbf{scheme variable} with indexname~$v$ and type~$T$.  An
lcp@324
   697
  \mltydx{indexname} is a string paired with a non-negative index, or
lcp@324
   698
  subscript; a term's scheme variables can be systematically renamed by
lcp@324
   699
  incrementing their subscripts.  Scheme variables are essentially free
lcp@324
   700
  variables, but may be instantiated during unification.
lcp@104
   701
lcp@324
   702
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
paulson@8136
   703
  is the \textbf{bound variable} with de Bruijn index~$i$, which counts the
lcp@324
   704
  number of lambdas, starting from zero, between a variable's occurrence
lcp@324
   705
  and its binding.  The representation prevents capture of variables.  For
lcp@324
   706
  more information see de Bruijn \cite{debruijn72} or
paulson@6592
   707
  Paulson~\cite[page~376]{paulson-ml2}.
lcp@104
   708
wenzelm@4317
   709
\item[\ttindexbold{Abs} ($a$, $T$, $u$)]
lcp@324
   710
  \index{lambda abs@$\lambda$-abstractions|bold}
paulson@8136
   711
  is the $\lambda$-\textbf{abstraction} with body~$u$, and whose bound
lcp@324
   712
  variable has name~$a$ and type~$T$.  The name is used only for parsing
lcp@324
   713
  and printing; it has no logical significance.
lcp@104
   714
lcp@324
   715
\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
paulson@8136
   716
is the \textbf{application} of~$t$ to~$u$.
lcp@324
   717
\end{ttdescription}
wenzelm@9695
   718
Application is written as an infix operator to aid readability.  Here is an
wenzelm@9695
   719
\ML\ pattern to recognize FOL formulae of the form~$A\imp B$, binding the
wenzelm@9695
   720
subformulae to~$A$ and~$B$:
wenzelm@864
   721
\begin{ttbox}
lcp@104
   722
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
lcp@104
   723
\end{ttbox}
lcp@104
   724
lcp@104
   725
wenzelm@4317
   726
\section{*Variable binding}
lcp@286
   727
\begin{ttbox}
lcp@286
   728
loose_bnos     : term -> int list
lcp@286
   729
incr_boundvars : int -> term -> term
lcp@286
   730
abstract_over  : term*term -> term
lcp@286
   731
variant_abs    : string * typ * term -> string * term
paulson@8136
   732
aconv          : term * term -> bool\hfill\textbf{infix}
lcp@286
   733
\end{ttbox}
lcp@286
   734
These functions are all concerned with the de Bruijn representation of
lcp@286
   735
bound variables.
lcp@324
   736
\begin{ttdescription}
wenzelm@864
   737
\item[\ttindexbold{loose_bnos} $t$]
lcp@286
   738
  returns the list of all dangling bound variable references.  In
paulson@6669
   739
  particular, \texttt{Bound~0} is loose unless it is enclosed in an
paulson@6669
   740
  abstraction.  Similarly \texttt{Bound~1} is loose unless it is enclosed in
lcp@286
   741
  at least two abstractions; if enclosed in just one, the list will contain
lcp@286
   742
  the number 0.  A well-formed term does not contain any loose variables.
lcp@286
   743
wenzelm@864
   744
\item[\ttindexbold{incr_boundvars} $j$]
lcp@332
   745
  increases a term's dangling bound variables by the offset~$j$.  This is
lcp@286
   746
  required when moving a subterm into a context where it is enclosed by a
lcp@286
   747
  different number of abstractions.  Bound variables with a matching
lcp@286
   748
  abstraction are unaffected.
lcp@286
   749
wenzelm@864
   750
\item[\ttindexbold{abstract_over} $(v,t)$]
lcp@286
   751
  forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
paulson@6669
   752
  It replaces every occurrence of \(v\) by a \texttt{Bound} variable with the
lcp@286
   753
  correct index.
lcp@286
   754
wenzelm@864
   755
\item[\ttindexbold{variant_abs} $(a,T,u)$]
lcp@286
   756
  substitutes into $u$, which should be the body of an abstraction.
lcp@286
   757
  It replaces each occurrence of the outermost bound variable by a free
lcp@286
   758
  variable.  The free variable has type~$T$ and its name is a variant
lcp@332
   759
  of~$a$ chosen to be distinct from all constants and from all variables
lcp@286
   760
  free in~$u$.
lcp@286
   761
wenzelm@864
   762
\item[$t$ \ttindexbold{aconv} $u$]
lcp@286
   763
  tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
lcp@286
   764
  to renaming of bound variables.
lcp@286
   765
\begin{itemize}
lcp@286
   766
  \item
paulson@6669
   767
    Two constants, \texttt{Free}s, or \texttt{Var}s are \(\alpha\)-convertible
lcp@286
   768
    if their names and types are equal.
lcp@286
   769
    (Variables having the same name but different types are thus distinct.
lcp@286
   770
    This confusing situation should be avoided!)
lcp@286
   771
  \item
lcp@286
   772
    Two bound variables are \(\alpha\)-convertible
lcp@286
   773
    if they have the same number.
lcp@286
   774
  \item
lcp@286
   775
    Two abstractions are \(\alpha\)-convertible
lcp@286
   776
    if their bodies are, and their bound variables have the same type.
lcp@286
   777
  \item
lcp@286
   778
    Two applications are \(\alpha\)-convertible
lcp@286
   779
    if the corresponding subterms are.
lcp@286
   780
\end{itemize}
lcp@286
   781
lcp@324
   782
\end{ttdescription}
lcp@286
   783
wenzelm@864
   784
\section{Certified terms}\index{terms!certified|bold}\index{signatures}
paulson@8136
   785
A term $t$ can be \textbf{certified} under a signature to ensure that every type
wenzelm@864
   786
in~$t$ is well-formed and every constant in~$t$ is a type instance of a
wenzelm@864
   787
constant declared in the signature.  The term must be well-typed and its use
paulson@6669
   788
of bound variables must be well-formed.  Meta-rules such as \texttt{forall_elim}
wenzelm@864
   789
take certified terms as arguments.
lcp@104
   790
lcp@324
   791
Certified terms belong to the abstract type \mltydx{cterm}.
lcp@104
   792
Elements of the type can only be created through the certification process.
lcp@104
   793
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
lcp@104
   794
lcp@104
   795
\subsection{Printing terms}
lcp@324
   796
\index{terms!printing of}
wenzelm@864
   797
\begin{ttbox}
nipkow@275
   798
     string_of_cterm :           cterm -> string
lcp@104
   799
Sign.string_of_term  : Sign.sg -> term -> string
lcp@104
   800
\end{ttbox}
lcp@324
   801
\begin{ttdescription}
wenzelm@864
   802
\item[\ttindexbold{string_of_cterm} $ct$]
lcp@104
   803
displays $ct$ as a string.
lcp@104
   804
wenzelm@864
   805
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
lcp@104
   806
displays $t$ as a string, using the syntax of~$sign$.
lcp@324
   807
\end{ttdescription}
lcp@104
   808
lcp@104
   809
\subsection{Making and inspecting certified terms}
wenzelm@864
   810
\begin{ttbox}
paulson@8136
   811
cterm_of       : Sign.sg -> term -> cterm
paulson@8136
   812
read_cterm     : Sign.sg -> string * typ -> cterm
paulson@8136
   813
cert_axm       : Sign.sg -> string * term -> string * term
paulson@8136
   814
read_axm       : Sign.sg -> string * string -> string * term
paulson@8136
   815
rep_cterm      : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
wenzelm@4543
   816
Sign.certify_term : Sign.sg -> term -> term * typ * int
lcp@104
   817
\end{ttbox}
lcp@324
   818
\begin{ttdescription}
wenzelm@4543
   819
  
wenzelm@4543
   820
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies
wenzelm@4543
   821
  $t$ with respect to signature~$sign$.
wenzelm@4543
   822
  
wenzelm@4543
   823
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$
wenzelm@4543
   824
  using the syntax of~$sign$, creating a certified term.  The term is
wenzelm@4543
   825
  checked to have type~$T$; this type also tells the parser what kind
wenzelm@4543
   826
  of phrase to parse.
wenzelm@4543
   827
  
wenzelm@4543
   828
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with
wenzelm@4543
   829
  respect to $sign$ as a meta-proposition and converts all exceptions
wenzelm@4543
   830
  to an error, including the final message
wenzelm@864
   831
\begin{ttbox}
wenzelm@864
   832
The error(s) above occurred in axiom "\(name\)"
wenzelm@864
   833
\end{ttbox}
wenzelm@864
   834
wenzelm@4543
   835
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt
wenzelm@4543
   836
    cert_axm}, but first reads the string $s$ using the syntax of
wenzelm@4543
   837
  $sign$.
wenzelm@4543
   838
  
wenzelm@4543
   839
\item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record
wenzelm@4543
   840
  containing its type, the term itself, its signature, and the maximum
wenzelm@4543
   841
  subscript of its unknowns.  The type and maximum subscript are
wenzelm@4543
   842
  computed during certification.
wenzelm@4543
   843
  
wenzelm@4543
   844
\item[\ttindexbold{Sign.certify_term}] is a more primitive version of
wenzelm@4543
   845
  \texttt{cterm_of}, returning the internal representation instead of
wenzelm@4543
   846
  an abstract \texttt{cterm}.
wenzelm@864
   847
lcp@324
   848
\end{ttdescription}
lcp@104
   849
lcp@104
   850
wenzelm@864
   851
\section{Types}\index{types|bold}
wenzelm@864
   852
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
wenzelm@864
   853
three constructor functions.  These correspond to type constructors, free
wenzelm@864
   854
type variables and schematic type variables.  Types are classified by sorts,
wenzelm@864
   855
which are lists of classes (representing an intersection).  A class is
wenzelm@864
   856
represented by a string.
lcp@104
   857
\begin{ttbox}
lcp@104
   858
type class = string;
lcp@104
   859
type sort  = class list;
lcp@104
   860
lcp@104
   861
datatype typ = Type  of string * typ list
lcp@104
   862
             | TFree of string * sort
lcp@104
   863
             | TVar  of indexname * sort;
lcp@104
   864
lcp@104
   865
infixr 5 -->;
wenzelm@864
   866
fun S --> T = Type ("fun", [S, T]);
lcp@104
   867
\end{ttbox}
lcp@324
   868
\begin{ttdescription}
wenzelm@4317
   869
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
paulson@8136
   870
  applies the \textbf{type constructor} named~$a$ to the type operand list~$Ts$.
lcp@324
   871
  Type constructors include~\tydx{fun}, the binary function space
lcp@324
   872
  constructor, as well as nullary type constructors such as~\tydx{prop}.
lcp@324
   873
  Other type constructors may be introduced.  In expressions, but not in
lcp@324
   874
  patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
lcp@324
   875
  types.
lcp@104
   876
wenzelm@4317
   877
\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
paulson@8136
   878
  is the \textbf{type variable} with name~$a$ and sort~$s$.
lcp@104
   879
wenzelm@4317
   880
\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
paulson@8136
   881
  is the \textbf{type unknown} with indexname~$v$ and sort~$s$.
lcp@324
   882
  Type unknowns are essentially free type variables, but may be
lcp@324
   883
  instantiated during unification.
lcp@324
   884
\end{ttdescription}
lcp@104
   885
lcp@104
   886
lcp@104
   887
\section{Certified types}
lcp@104
   888
\index{types!certified|bold}
wenzelm@864
   889
Certified types, which are analogous to certified terms, have type
nipkow@275
   890
\ttindexbold{ctyp}.
lcp@104
   891
lcp@104
   892
\subsection{Printing types}
lcp@324
   893
\index{types!printing of}
wenzelm@864
   894
\begin{ttbox}
nipkow@275
   895
     string_of_ctyp :           ctyp -> string
lcp@104
   896
Sign.string_of_typ  : Sign.sg -> typ -> string
lcp@104
   897
\end{ttbox}
lcp@324
   898
\begin{ttdescription}
wenzelm@864
   899
\item[\ttindexbold{string_of_ctyp} $cT$]
lcp@104
   900
displays $cT$ as a string.
lcp@104
   901
wenzelm@864
   902
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
lcp@104
   903
displays $T$ as a string, using the syntax of~$sign$.
lcp@324
   904
\end{ttdescription}
lcp@104
   905
lcp@104
   906
lcp@104
   907
\subsection{Making and inspecting certified types}
wenzelm@864
   908
\begin{ttbox}
wenzelm@4543
   909
ctyp_of          : Sign.sg -> typ -> ctyp
paulson@8136
   910
rep_ctyp         : ctyp -> \{T: typ, sign: Sign.sg\}
wenzelm@4543
   911
Sign.certify_typ : Sign.sg -> typ -> typ
lcp@104
   912
\end{ttbox}
lcp@324
   913
\begin{ttdescription}
wenzelm@4543
   914
  
wenzelm@4543
   915
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies
wenzelm@4543
   916
  $T$ with respect to signature~$sign$.
wenzelm@4543
   917
  
wenzelm@4543
   918
\item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record
wenzelm@4543
   919
  containing the type itself and its signature.
wenzelm@4543
   920
  
wenzelm@4543
   921
\item[\ttindexbold{Sign.certify_typ}] is a more primitive version of
wenzelm@4543
   922
  \texttt{ctyp_of}, returning the internal representation instead of
wenzelm@4543
   923
  an abstract \texttt{ctyp}.
lcp@104
   924
lcp@324
   925
\end{ttdescription}
lcp@104
   926
paulson@1846
   927
wenzelm@4317
   928
\section{Oracles: calling trusted external reasoners}
paulson@1846
   929
\label{sec:oracles}
paulson@1846
   930
\index{oracles|(}
paulson@1846
   931
paulson@1846
   932
Oracles allow Isabelle to take advantage of external reasoners such as
paulson@1846
   933
arithmetic decision procedures, model checkers, fast tautology checkers or
paulson@1846
   934
computer algebra systems.  Invoked as an oracle, an external reasoner can
paulson@1846
   935
create arbitrary Isabelle theorems.  It is your responsibility to ensure that
paulson@1846
   936
the external reasoner is as trustworthy as your application requires.
paulson@1846
   937
Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
paulson@1846
   938
depends upon oracle calls.
paulson@1846
   939
paulson@1846
   940
\begin{ttbox}
wenzelm@4317
   941
invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
paulson@4597
   942
Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory 
paulson@4597
   943
                    -> theory
paulson@1846
   944
\end{ttbox}
paulson@1846
   945
\begin{ttdescription}
wenzelm@4317
   946
\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
wenzelm@4317
   947
  invokes the oracle $name$ of theory $thy$ passing the information
wenzelm@4317
   948
  contained in the exception value $data$ and creating a theorem
wenzelm@4317
   949
  having signature $sign$.  Note that type \ttindex{object} is just an
wenzelm@4317
   950
  abbreviation for \texttt{exn}.  Errors arise if $thy$ does not have
wenzelm@4317
   951
  an oracle called $name$, if the oracle rejects its arguments or if
wenzelm@4317
   952
  its result is ill-typed.
wenzelm@4317
   953
  
wenzelm@4317
   954
\item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends
wenzelm@4317
   955
  $thy$ by oracle $fun$ called $name$.  It is seldom called
wenzelm@4317
   956
  explicitly, as there is concrete syntax for oracles in theory files.
paulson@1846
   957
\end{ttdescription}
paulson@1846
   958
paulson@1846
   959
A curious feature of {\ML} exceptions is that they are ordinary constructors.
paulson@6669
   960
The {\ML} type \texttt{exn} is a datatype that can be extended at any time.  (See
paulson@1846
   961
my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
paulson@1846
   962
page~136.)  The oracle mechanism takes advantage of this to allow an oracle to
paulson@1846
   963
take any information whatever.
paulson@1846
   964
paulson@1846
   965
There must be some way of invoking the external reasoner from \ML, either
paulson@1846
   966
because it is coded in {\ML} or via an operating system interface.  Isabelle
paulson@1846
   967
expects the {\ML} function to take two arguments: a signature and an
wenzelm@4317
   968
exception object.
paulson@1846
   969
\begin{itemize}
paulson@1846
   970
\item The signature will typically be that of a desendant of the theory
paulson@1846
   971
  declaring the oracle.  The oracle will use it to distinguish constants from
paulson@1846
   972
  variables, etc., and it will be attached to the generated theorems.
paulson@1846
   973
paulson@1846
   974
\item The exception is used to pass arbitrary information to the oracle.  This
paulson@1846
   975
  information must contain a full description of the problem to be solved by
paulson@1846
   976
  the external reasoner, including any additional information that might be
paulson@1846
   977
  required.  The oracle may raise the exception to indicate that it cannot
paulson@1846
   978
  solve the specified problem.
paulson@1846
   979
\end{itemize}
paulson@1846
   980
paulson@6669
   981
A trivial example is provided in theory \texttt{FOL/ex/IffOracle}.  This
wenzelm@4317
   982
oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
wenzelm@4317
   983
an even number of $P$s.
paulson@1846
   984
wenzelm@4317
   985
The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring
wenzelm@4317
   986
a few auxiliary functions (suppressed below) for creating the
wenzelm@4317
   987
tautologies.  Then it declares a new exception constructor for the
wenzelm@4317
   988
information required by the oracle: here, just an integer. It finally
wenzelm@4317
   989
defines the oracle function itself.
paulson@1846
   990
\begin{ttbox}
wenzelm@4317
   991
exception IffOracleExn of int;\medskip
wenzelm@4317
   992
fun mk_iff_oracle (sign, IffOracleExn n) =
wenzelm@4317
   993
  if n > 0 andalso n mod 2 = 0
paulson@6669
   994
  then Trueprop \$ mk_iff n
wenzelm@4317
   995
  else raise IffOracleExn n;
paulson@1846
   996
\end{ttbox}
paulson@6669
   997
Observe the function's two arguments, the signature \texttt{sign} and the
wenzelm@4317
   998
exception given as a pattern.  The function checks its argument for
wenzelm@4317
   999
validity.  If $n$ is positive and even then it creates a tautology
wenzelm@4317
  1000
containing $n$ occurrences of~$P$.  Otherwise it signals error by
wenzelm@4317
  1001
raising its own exception (just by happy coincidence).  Errors may be
paulson@6669
  1002
signalled by other means, such as returning the theorem \texttt{True}.
wenzelm@4317
  1003
Please ensure that the oracle's result is correctly typed; Isabelle
wenzelm@4317
  1004
will reject ill-typed theorems by raising a cryptic exception at top
wenzelm@4317
  1005
level.
paulson@1846
  1006
paulson@6669
  1007
The \texttt{oracle} section of \texttt{IffOracle.thy} installs above
wenzelm@4317
  1008
\texttt{ML} function as follows:
paulson@1846
  1009
\begin{ttbox}
wenzelm@4317
  1010
IffOracle = FOL +\medskip
wenzelm@4317
  1011
oracle
wenzelm@4317
  1012
  iff = mk_iff_oracle\medskip
paulson@1846
  1013
end
paulson@1846
  1014
\end{ttbox}
paulson@1846
  1015
wenzelm@4317
  1016
Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
wenzelm@4317
  1017
the oracle:
paulson@1846
  1018
\begin{ttbox}
paulson@4597
  1019
fun iff_oracle n = invoke_oracle IffOracle.thy "iff"
paulson@4597
  1020
                      (sign_of IffOracle.thy, IffOracleExn n);
wenzelm@4317
  1021
\end{ttbox}
wenzelm@4317
  1022
wenzelm@4317
  1023
Here are some example applications of the \texttt{iff} oracle.  An
wenzelm@4317
  1024
argument of 10 is allowed, but one of 5 is forbidden:
wenzelm@4317
  1025
\begin{ttbox}
wenzelm@4317
  1026
iff_oracle 10;
paulson@1846
  1027
{\out  "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
wenzelm@4317
  1028
iff_oracle 5;
paulson@1846
  1029
{\out Exception- IffOracleExn 5 raised}
paulson@1846
  1030
\end{ttbox}
paulson@1846
  1031
paulson@1846
  1032
\index{oracles|)}
lcp@104
  1033
\index{theories|)}
wenzelm@5369
  1034
wenzelm@5369
  1035
wenzelm@5369
  1036
%%% Local Variables: 
wenzelm@5369
  1037
%%% mode: latex
wenzelm@5369
  1038
%%% TeX-master: "ref"
wenzelm@5369
  1039
%%% End: