doc-src/Ref/theories.tex
author paulson
Thu, 11 Jul 1996 15:00:38 +0200
changeset 1846 763f08fb194f
parent 1650 a4ed2655b08c
child 1880 78c4b3ddba6c
permissions -rw-r--r--
Documentation of oracles and their syntax
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%% $Id$
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
     2
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
\chapter{Theories, Terms and Types} \label{theories}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\index{theories|(}\index{signatures|bold}
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
     5
\index{reading!axioms|see{{\tt assume_ax}}}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
Theories organize the syntax, declarations and axioms of a mathematical
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
development.  They are built, starting from the Pure theory, by extending
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
     8
and merging existing theories.  They have the \ML\ type \mltydx{theory}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
     9
Theory operations signal errors by raising exception \xdx{THEORY},
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
returning a message and a list of theories.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
Signatures, which contain information about sorts, types, constants and
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
    13
syntax, have the \ML\ type~\mltydx{Sign.sg}.  For identification, each
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    14
signature carries a unique list of \bfindex{stamps}, which are \ML\
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    15
references to strings.  The strings serve as human-readable names; the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
references serve as unique identifiers.  Each primitive signature has a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
single stamp.  When two signatures are merged, their lists of stamps are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
also merged.  Every theory carries a unique signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
Terms and types are the underlying representation of logical syntax.  Their
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    21
\ML\ definitions are irrelevant to naive Isabelle users.  Programmers who
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    22
wish to extend Isabelle may need to know such details, say to code a tactic
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    23
that looks for subgoals of a particular form.  Terms and types may be
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
`certified' to be well-formed with respect to a given signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    26
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    27
\section{Defining theories}\label{sec:ref-defining-theories}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    29
Theories are usually defined using theory definition files (which have a name
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    30
suffix {\tt .thy}). There is also a low level interface provided by certain
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    31
\ML{} functions (see \S\ref{BuildingATheory}).
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    32
Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    33
definitions; here is an explanation of the constituent parts:
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    34
\begin{description}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    35
\item[{\it theoryDef}]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    36
  is the full definition.  The new theory is called $id$.  It is the union
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    37
  of the named {\bf parent theories}\indexbold{theories!parent}, possibly
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    38
  extended with new classes, etc.  The basic theory, which contains only
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    39
  the meta-logic, is called \thydx{Pure}.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
    40
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    41
  Normally each {\it name\/} is an identifier, the name of the parent theory.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    42
  Quoted strings can be used to document additional file dependencies; see
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    43
  \S\ref{LoadingTheories} for details.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    44
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    45
\item[$classes$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    46
  is a series of class declarations.  Declaring {\tt$id$ < $id@1$ \dots\
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    47
    $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    48
  id@n$.  This rules out cyclic class structures.  Isabelle automatically
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    49
  computes the transitive closure of subclass hierarchies; it is not
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    50
  necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    51
    e}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    52
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    53
\item[$default$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    54
  introduces $sort$ as the new default sort for type variables.  This applies
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    55
  to unconstrained type variables in an input string but not to type
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    56
  variables created internally.  If omitted, the default sort is the listwise
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    57
  union of the default sorts of the parent theories (i.e.\ their logical
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    58
  intersection).
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    59
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    60
\item[$sort$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    61
  is a finite set of classes.  A single class $id$ abbreviates the singleton
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    62
  set {\tt\{}$id${\tt\}}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    63
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    64
\item[$types$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    65
  is a series of type declarations.  Each declares a new type constructor
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    66
  or type synonym.  An $n$-place type constructor is specified by
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    67
  $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    68
  indicate the number~$n$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    69
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
    70
  A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1380
diff changeset
    71
  $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1380
diff changeset
    72
  be strings.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    73
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    74
\item[$infix$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    75
  declares a type or constant to be an infix operator of priority $nat$
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    76
  associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    77
  2-place type constructors can have infix status; an example is {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    78
  ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    79
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    80
\item[$arities$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    81
  is a series of arity declarations.  Each assigns arities to type
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    82
  constructors.  The $name$ must be an existing type constructor, which is
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    83
  given the additional arity $arity$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    84
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    85
\item[$constDecl$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    86
  is a series of constant declarations.  Each new constant $name$ is given
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
    87
  the specified type.  The optional $mixfix$ annotations may
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    88
  attach concrete syntax to the constant. A variant of {\tt consts} is the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    89
  {\tt syntax} section\index{*syntax section}, which adds just syntax without
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    90
  declaring logical constants.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    91
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    92
\item[$mixfix$] \index{mixfix declarations}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    93
  annotations can take three forms:
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    94
  \begin{itemize}
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    95
  \item A mixfix template given as a $string$ of the form
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    96
    {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    97
    indicates the position where the $i$-th argument should go.  The list
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    98
    of numbers gives the priority of each argument.  The final number gives
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    99
    the priority of the whole construct.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   101
  \item A constant $f$ of type $\tau@1\To(\tau@2\To\tau)$ can be given {\bf
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   102
    infix} status.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   104
  \item A constant $f$ of type $(\tau@1\To\tau@2)\To\tau$ can be given {\bf
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   105
    binder} status.  The declaration {\tt binder} $\cal Q$ $p$ causes
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   106
  ${\cal Q}\,x.F(x)$ to be treated
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   107
  like $f(F)$, where $p$ is the priority.
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
   108
  \end{itemize}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   109
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   110
\item[$trans$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   111
  specifies syntactic translation rules (macros).  There are three forms:
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   112
  parse rules ({\tt =>}), print rules ({\tt <=}), and parse/print rules ({\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   113
  ==}).
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   114
1650
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   115
\item[$rules$]
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   116
  is a series of rule declarations.  Each has a name $id$ and the formula is
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   117
  given by the $string$.  Rule names must be distinct within any single
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   118
  theory file.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   119
1650
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   120
\item[$defs$]
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   121
  is a series of definitions.  Just like $rules$, except that every $string$
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   122
  must be a definition.
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   123
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   124
\item[$constdefs$] combines the declaration of constants and their
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   125
  definition. The first $string$ is the type, the second the definition.
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   126
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   127
\item[$oracle$] links the theory to a trusted external reasoner.  It is
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   128
  allowed to create theorems, but each theorem carries a proof object
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   129
  describing the oracle invocation.  See \S\ref{sec:oracles} for details.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   130
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   131
\item[$ml$] \index{*ML section}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   132
  consists of \ML\ code, typically for parse and print translation functions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\end{description}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   134
%
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   135
Chapters~\ref{Defining-Logics} and \ref{chap:syntax} explain mixfix
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   136
declarations, translation rules and the {\tt ML} section in more detail.
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   137
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   138
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   139
\subsection{*Classes and arities}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   140
\index{classes!context conditions}\index{arities!context conditions}
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   141
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   142
In order to guarantee principal types~\cite{nipkow-prehofer},
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   143
arity declarations must obey two conditions:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   144
\begin{itemize}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   145
\item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   146
  (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, the following is
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   147
  forbidden:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   148
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   149
types
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   150
  'a ty
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   151
arities
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   152
  ty :: ({\ttlbrace}logic{\ttrbrace}) logic
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   153
  ty :: ({\ttlbrace}{\ttrbrace})logic
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   154
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   155
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   156
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   157
  (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   158
  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   159
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   160
expresses that the set of types represented by $s'$ is a subset of the set of
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   161
types represented by $s$.  For example, the following is forbidden:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   162
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   163
classes
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   164
  term < logic
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   165
types
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   166
  'a ty
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   167
arities
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   168
  ty :: ({\ttlbrace}logic{\ttrbrace})logic
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   169
  ty :: ({\ttlbrace}{\ttrbrace})term
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   170
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   171
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   172
\end{itemize}
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   173
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   175
\section{Loading a new theory}\label{LoadingTheories}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   176
\index{theories!loading}\index{files!reading}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   177
\begin{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   178
use_thy         : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   179
time_use_thy    : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   180
loadpath        : string list ref \hfill{\bf initially {\tt["."]}}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   181
delete_tmpfiles : bool ref \hfill{\bf initially true}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   182
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   183
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   184
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   185
\item[\ttindexbold{use_thy} $thyname$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   186
  reads the theory $thyname$ and creates an \ML{} structure as described below.
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   187
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   188
\item[\ttindexbold{time_use_thy} $thyname$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   189
  calls {\tt use_thy} $thyname$ and reports the time taken.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   190
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   191
\item[\ttindexbold{loadpath}]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   192
  contains a list of directories to search when locating the files that
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   193
  define a theory.  This list is only used if the theory name in {\tt
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   194
    use_thy} does not specify the path explicitly.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   195
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   196
\item[\ttindexbold{delete_tmpfiles} := false;]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   197
suppresses the deletion of temporary files.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   198
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   199
%
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
Each theory definition must reside in a separate file.  Let the file {\it
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   201
  T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   202
theories are $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"{\it
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   203
  T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   204
file {\tt.{\it T}.thy.ML}, and reads the latter file.  Recursive {\tt
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   205
  use_thy} calls load those parent theories that have not been loaded
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   206
previously; the recursive calls may continue to any depth.  One {\tt use_thy}
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   207
call can read an entire logic provided all theories are linked appropriately.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   208
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   209
The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   210
for the new theory and components for each of the rules.  The structure also
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   211
contains the definitions of the {\tt ML} section, if present.  The file
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   212
{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   213
true} and no errors occurred.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   214
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   215
Finally the file {\it T}{\tt.ML} is read, if it exists.  This file normally
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   216
begins with the declaration {\tt open~$T$} and contains proofs involving
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   217
the new theory.
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   218
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   219
Some applications construct theories directly by calling \ML\ functions.  In
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   220
this situation there is no {\tt.thy} file, only an {\tt.ML} file.  The
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   221
{\tt.ML} file must declare an \ML\ structure having the theory's name and a
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   222
component {\tt thy} containing the new theory object.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   223
Section~\ref{sec:pseudo-theories} below describes a way of linking such
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   224
theories to their parents.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   225
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   226
\begin{warn}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   227
  Temporary files are written to the current directory, so this must be
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   228
  writable.  Isabelle inherits the current directory from the operating
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   229
  system; you can change it within Isabelle by typing {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   230
  cd"$dir$"}\index{*cd}.
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
   231
\end{warn}
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   232
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   233
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   234
\section{Reloading modified theories}\label{sec:reloading-theories}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   235
\indexbold{theories!reloading}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   236
\begin{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   237
update     : unit -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   238
unlink_thy : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   239
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   240
Changing a theory on disk often makes it necessary to reload all theories
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   241
descended from it.  However, {\tt use_thy} reads only one theory, even if
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   242
some of the parent theories are out of date.  In this case you should call
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   243
{\tt update()}.
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   244
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   245
Isabelle keeps track of all loaded theories and their files.  If
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   246
\ttindex{use_thy} finds that the theory to be loaded has been read before,
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   247
it determines whether to reload the theory as follows.  First it looks for
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   248
the theory's files in their previous location.  If it finds them, it
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   249
compares their modification times to the internal data and stops if they
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   250
are equal.  If the files have been moved, {\tt use_thy} searches for them
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   251
as it would for a new theory.  After {\tt use_thy} reloads a theory, it
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   252
marks the children as out-of-date.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   253
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   254
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   255
\item[\ttindexbold{update}()]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   256
  reloads all modified theories and their descendants in the correct order.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   257
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   258
\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   259
  informs Isabelle that theory $thyname$ no longer exists.  If you delete the
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   260
  theory files for $thyname$ then you must execute {\tt unlink_thy};
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   261
  otherwise {\tt update} will complain about a missing file.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   262
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   263
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   264
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   265
\goodbreak
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   266
\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   267
The theory mechanism depends upon reference variables.  At the end of a
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   268
Poly/\ML{} session, the contents of references are lost unless they are
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   269
declared in the current database.  In particular, assignments to references
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   270
of the {\tt Pure} database are lost, including all information about loaded
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   271
theories. To avoid losing this information simply call
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   272
\begin{ttbox}
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   273
init_thy_reader();
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   274
\end{ttbox}
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   275
when building the new database.
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   276
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   277
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   278
\subsection{*Pseudo theories}\label{sec:pseudo-theories}
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   279
\indexbold{theories!pseudo}%
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   280
Any automatic reloading facility requires complete knowledge of all
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   281
dependencies.  Sometimes theories depend on objects created in \ML{} files
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   282
with no associated theory definition file.  These objects may be theories but
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   283
they could also be theorems, proof procedures, etc.
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   284
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   285
Unless such dependencies are documented, {\tt update} fails to reload these
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   286
\ML{} files and the system is left in a state where some objects, such as
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   287
theorems, still refer to old versions of theories.  This may lead to the
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   288
error
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   289
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   290
Attempt to merge different versions of theories: \dots
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   291
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   292
Therefore there is a way to link theories and {\bf orphaned} \ML{} files ---
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   293
those not associated with a theory definition.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   294
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   295
Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   296
theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   297
theorems proved in {\tt orphan.ML}.  Then {\tt B.thy} should
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   298
mention this dependency as follows:
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   299
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   300
B = \(\ldots\) + "orphan" + \(\ldots\)
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   301
\end{ttbox}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   302
Quoted strings stand for theories which have to be loaded before the
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   303
current theory is read but which are not used in building the base of
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   304
theory~$B$. Whenever {\tt orphan} changes and is reloaded, Isabelle
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   305
knows that $B$ has to be updated, too.
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   306
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   307
Note that it's necessary for {\tt orphan} to declare a special ML
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   308
object of type {\tt theory} which is present in all theories. This is
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   309
normally achieved by adding the file {\tt orphan.thy} to make {\tt
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   310
orphan} a {\bf pseudo theory}. A minimum version of {\tt orphan.thy}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   311
would be
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   312
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   313
\begin{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   314
orphan = Pure
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   315
\end{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   316
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   317
which uses {\tt Pure} to make a dummy theory. Normally though the
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   318
orphaned file has its own dependencies.  If {\tt orphan.ML} depends on
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   319
theories or files $A@1$, \ldots, $A@n$, record this by creating the
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   320
pseudo theory in the following way:
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   321
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   322
orphan = \(A@1\) + \(\ldots\) + \(A@n\)
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   323
\end{ttbox}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   324
The resulting theory ensures that {\tt update} reloads {\tt orphan}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   325
whenever it reloads one of the $A@i$.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   326
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   327
For an extensive example of how this technique can be used to link lots of
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   328
theory files and load them by just a few {\tt use_thy} calls, consult the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   329
sources of \ZF{} set theory.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   330
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   333
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   334
\subsection{Extracting an axiom or theorem from a theory}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   335
\index{theories!axioms of}\index{axioms!extracting}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   336
\index{theories!theorems of}\index{theorems!extracting}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   337
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   338
get_axiom : theory -> string -> thm
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   339
get_thm   : theory -> string -> thm
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   340
assume_ax : theory -> string -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   342
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   343
\item[\ttindexbold{get_axiom} $thy$ $name$]
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   344
  returns an axiom with the given $name$ from $thy$, raising exception
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   345
  \xdx{THEORY} if none exists.  Merging theories can cause several axioms
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   346
  to have the same name; {\tt get_axiom} returns an arbitrary one.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   348
\item[\ttindexbold{get_thm} $thy$ $name$]
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   349
  is analogous to {\tt get_axiom}, but looks for a stored theorem. Like
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   350
  {\tt get_axiom} it searches all parents of a theory if the theorem
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   351
  is not associated with $thy$.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   352
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   353
\item[\ttindexbold{assume_ax} $thy$ $formula$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   354
  reads the {\it formula} using the syntax of $thy$, following the same
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   355
  conventions as axioms in a theory definition.  You can thus pretend that
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   356
  {\it formula} is an axiom and use the resulting theorem like an axiom.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   357
  Actually {\tt assume_ax} returns an assumption;  \ttindex{result}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   358
  complains about additional assumptions, but \ttindex{uresult} does not.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
For example, if {\it formula} is
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   361
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   362
\hbox{\verb'?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]'}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   363
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   365
\subsection{Building a theory}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   366
\label{BuildingATheory}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   367
\index{theories!constructing|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   368
\begin{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   369
pure_thy       : theory
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   370
merge_theories : theory * theory -> theory
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   371
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   372
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   373
\item[\ttindexbold{pure_thy}] contains just the syntax and signature
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   374
  of the meta-logic.  There are no axioms: meta-level inferences are carried
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   375
  out by \ML\ functions.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   376
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   377
  theories $thy@1$ and $thy@2$.  The resulting theory contains all of the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   378
  syntax, signature and axioms of the constituent theories. Merging theories
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   379
  that contain different identification stamps of the same name fails with
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   380
  the following message
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   381
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   382
Attempt to merge different versions of theories: "\(T@1\)", \(\ldots\), "\(T@n\)"
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   383
\end{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   384
  This error may especially occur when a theory is redeclared --- say to
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   385
  change an incorrect axiom --- and bindings to old versions persist.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   386
  Isabelle ensures that old and new theories of the same name are not
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   387
  involved in a proof.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   388
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   389
%% FIXME
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   390
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   391
%  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   392
%  internally.  When a theory is redeclared, say to change an incorrect axiom,
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   393
%  bindings to the old axiom may persist.  Isabelle ensures that the old and
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   394
%  new theories are not involved in the same proof.  Attempting to combine
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   395
%  different theories having the same name $T$ yields the fatal error
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   396
%extend_theory  : theory -> string -> \(\cdots\) -> theory
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   397
%\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   398
%Attempt to merge different versions of theory: \(T\)
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   399
%\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   400
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   401
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   402
%% FIXME
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   403
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   404
%      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   405
%\hfill\break   %%% include if line is just too short
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   406
%is the \ML{} equivalent of the following theory definition:
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   407
%\begin{ttbox}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   408
%\(T\) = \(thy\) +
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   409
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   410
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   411
%default {\(d@1,\dots,d@r\)}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   412
%types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   413
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   414
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   415
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   416
%consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   417
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   418
%rules   \(name\) \(rule\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   419
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   420
%end
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   421
%\end{ttbox}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   422
%where
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   423
%\begin{tabular}[t]{l@{~=~}l}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   424
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   425
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   426
%$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   427
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   428
%\\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   429
%$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   430
%$rules$   & \tt[("$name$",$rule$),\dots]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   431
%\end{tabular}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   434
\subsection{Inspecting a theory}\label{sec:inspct-thy}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
\index{theories!inspecting|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   436
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
print_theory  : theory -> unit
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   438
axioms_of     : theory -> (string * thm) list
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   439
thms_of       : theory -> (string * thm) list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
parents_of    : theory -> theory list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
sign_of       : theory -> Sign.sg
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
stamps_of_thy : theory -> string ref list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
\end{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   444
These provide means of viewing a theory's components.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   445
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   446
\item[\ttindexbold{print_theory} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   447
prints the contents of $thy$ excluding the syntax related parts (which are
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   448
shown by {\tt print_syntax}).  The output is quite verbose.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   449
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   450
\item[\ttindexbold{axioms_of} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   451
returns the additional axioms of the most recent extend node of~$thy$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   453
\item[\ttindexbold{thms_of} $thy$]
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   454
returns all theorems that are associated with $thy$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   456
\item[\ttindexbold{parents_of} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   457
returns the direct ancestors of~$thy$.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   458
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   459
\item[\ttindexbold{sign_of} $thy$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   460
returns the signature associated with~$thy$.  It is useful with functions
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   461
like {\tt read_instantiate_sg}, which take a signature as an argument.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   464
returns the identification \rmindex{stamps} of the signature associated
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   465
with~$thy$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   466
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   469
\section{Generating HTML documents}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   470
\index{HTML|bold} 
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   471
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   472
Isabelle is able to make HTML documents that show a theory's
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   473
definition, the theorems proved in its ML file and the relationship
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   474
with its ancestors and descendants. HTML stands for Hypertext Markup
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   475
Language and is used in the World Wide Web to represent text
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   476
containing images and links to other documents. Web browsers like
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   477
{\tt xmosaic} or {\tt netscape} are used to view these documents.
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   478
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   479
Besides the three HTML files that are made for every theory
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   480
(definition and theorems, ancestors, descendants), Isabelle stores
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   481
links to all theories in an index file. These indexes are themself
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   482
linked with other indexes to represent the hierarchic structure of
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   483
Isabelle's logics.
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   484
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   485
To make HTML files for logics that are part of the Isabelle
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   486
distribution, simply set the shell environment variable {\tt
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   487
MAKE_HTML} before compiling a logic. This works for single logics as
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   488
well as for the shell script {\tt make-all} (see
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   489
\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   490
{\tt csh} style shell, the following commands can be used:
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   491
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   492
\begin{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   493
cd FOL
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   494
setenv MAKE_HTML
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   495
make
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   496
\end{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   497
1497
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   498
The databases made this way do not differ from the ones made with an
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   499
unset {\tt MAKE_HTML}; in particular no HTML files are written if the
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   500
database is used to manually load a theory.
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   501
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   502
As you will see below, the HTML generation is controlled by a boolean
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   503
reference variable. If you want to make databases which define this
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   504
variable's value as {\tt true} and where therefore HTML files are
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   505
written each time {\tt use_thy} is invoked, you have to set {\tt
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   506
MAKE_HTML} to ``{\tt true}'':
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   507
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   508
\begin{ttbox}
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   509
cd FOL
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   510
setenv MAKE_HTML true
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   511
make
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   512
\end{ttbox}
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   513
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   514
All theories loaded from within the {\tt FOL} database and all
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   515
databases derived from it will now cause HTML files to be written.
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   516
This behaviour can be changed by assigning a value of {\tt false} to
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   517
the boolean reference variable {\tt make_html}. Be careful when making
1520
5fee0fef5019 removed note about "IO exceptions" during HTML generation
clasohm
parents: 1497
diff changeset
   518
such databases publicly available since it means that your users will
5fee0fef5019 removed note about "IO exceptions" during HTML generation
clasohm
parents: 1497
diff changeset
   519
generate HTML files though they might not intend to do so.
1452
ee54d2c15d66 added warning for databases made with set MAKE_HTML
clasohm
parents: 1409
diff changeset
   520
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   521
As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   522
{\tt FOL}) and because the HTML files list a theory's ancestors, you
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   523
should not make HTML files for a logic if the HTML files for the base
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   524
logic do not exist. Otherwise some of the hypertext links might point
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   525
to non-existing documents.
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   526
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   527
The entry point to all logics is the {\tt index.html} file located in
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   528
Isabelle's main directory. You can also access a HTML version of the
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   529
distribution package at
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   530
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   531
\begin{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   532
http://www4.informatik.tu-muenchen.de/~nipkow/isabelle
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   533
\end{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   534
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   535
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   536
\subsection*{Manual HTML generation}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   537
1551
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   538
To manually control the generation of HTML files the following
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   539
commands and reference variables are used:
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   540
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   541
\begin{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   542
init_html   : unit -> unit
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   543
make_html   : bool ref
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   544
finish_html : unit -> unit
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   545
\end{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   546
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   547
\begin{ttdescription}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   548
\item[\ttindexbold{init_html}]
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   549
activates the HTML facility. It stores the current working directory
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   550
as the place where the {\tt index.html} file for all theories loaded
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   551
afterwards will be stored.
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   552
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   553
\item[\ttindexbold{make_html}]
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   554
is a boolean reference variable read by {\tt use_thy} and other
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   555
functions to decide whether HTML files should be made. After you have
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   556
used {\tt init_html} you can manually change {\tt make_html}'s value
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   557
to temporarily disable HTML generation.
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   558
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   559
\item[\ttindexbold{finish_html}]
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   560
has to be called after all theories have been read that should be
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   561
listed in the current {\tt index.html} file. It reads a temporary
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   562
file with information about the theories read since the last use of
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   563
{\tt init_html} and makes the {\tt index.html} file. If {\tt
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   564
make_html} is {\tt false} nothing is done.
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   565
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   566
The indexes made by this function also contain a link to the {\tt
1497
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   567
README} file if there exists one in the directory where the index is
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   568
stored. If there's a {\tt README.html} file it is used instead of
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   569
{\tt README}.
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   570
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   571
\end{ttdescription}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   572
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   573
The above functions could be used in the following way:
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   574
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   575
\begin{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   576
init_html();
1497
41a1b0426b2e updated documentation of MAKE_HTML
clasohm
parents: 1453
diff changeset
   577
{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   578
use_thy "List";
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   579
\dots
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   580
finish_html();
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   581
\end{ttbox}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   582
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   583
Please note that HTML files are made only for those theories that are
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   584
read while {\tt make_html} is {\tt true}. These files may contain
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   585
links to theories that were read with a {\tt false} {\tt make_html}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   586
and therefore point to non-existing files.
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   587
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   588
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   589
\subsection*{Extending or adding a logic}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   590
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   591
If you add a new subdirectory to Isabelle's logics (or add a completly
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   592
new logic), you would have to call {\tt init_html} at the start of every
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   593
directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   594
it. This is automatically done if you use
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   595
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   596
\begin{ttbox}\index{use_dir}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   597
use_dir : string -> unit
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   598
\end{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   599
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   600
This function takes a path as its parameter, changes the working
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   601
directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   602
executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   603
index.html} file written in this directory will be automatically
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   604
linked to the first index found in the (recursively searched)
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   605
superdirectories.
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   606
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   607
Instead of adding something like
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   608
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   609
\begin{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   610
use"ex/ROOT.ML";
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   611
\end{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   612
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   613
to the logic's makefile you have to use this:
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   614
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   615
\begin{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   616
use_dir"ex";
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   617
\end{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   618
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   619
Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   620
{\tt true} the generation of HTML files depends on the value this
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   621
reference variable has. It can either be inherited from the used \ML{}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   622
database or set in the makefile before {\tt use_dir} is invoked,
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   623
e.g. to set it's value according to the environment variable {\tt
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   624
MAKE_HTML}.
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   625
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   626
The generated HTML files contain all theorems that were proved in the
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   627
theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   628
or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   629
is a hypertext link to the whole \ML{} file.
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   630
1551
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   631
You can add section headings to the list of theorems by using
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   632
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   633
\begin{ttbox}\index{use_dir}
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   634
section: string -> unit
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   635
\end{ttbox}
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   636
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   637
in a theory's ML file, which converts a plain string to a HTML
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   638
heading and inserts it before the next theorem proved or stored with
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   639
one of the above functions. If {\tt make_html} is {\tt false} nothing
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   640
is done.
4a617e14d12c documented new function 'section'
clasohm
parents: 1520
diff changeset
   641
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   642
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   643
\subsection*{Using someone else's database}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   644
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   645
To make them independent from their storage place, the HTML files only
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   646
contain relative paths which are derived from absolute ones like the
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   647
current working directory, {\tt gif_path} or {\tt base_path}. The
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   648
latter two are reference variables which are initialized at the time
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   649
when the {\tt Pure} database is made. Because you need write access
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   650
for the current directory to make HTML files and therefore (probably)
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   651
generate them in your home directory, the absolute {\tt base_path} is
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   652
not correct if you use someone else's database or a database derived
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   653
from it.
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   654
1409
3cc3fde8d005 setting base_path is now optional
clasohm
parents: 1387
diff changeset
   655
In that case you first should set {\tt base_path} to the value of {\em
3cc3fde8d005 setting base_path is now optional
clasohm
parents: 1387
diff changeset
   656
your} Isabelle main directory, i.e. the directory that contains the
3cc3fde8d005 setting base_path is now optional
clasohm
parents: 1387
diff changeset
   657
subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
3cc3fde8d005 setting base_path is now optional
clasohm
parents: 1387
diff changeset
   658
your own logics are stored. If you do not do this, the generated HTML
3cc3fde8d005 setting base_path is now optional
clasohm
parents: 1387
diff changeset
   659
files will still be usable but may contain incomplete titles and lack
3cc3fde8d005 setting base_path is now optional
clasohm
parents: 1387
diff changeset
   660
some hypertext links.
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   661
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   662
It's also a good idea to set {\tt gif_path} which points to the
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   663
directory containing two GIF images used in the HTML
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   664
documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   665
main directory. While its value in general is still valid, your HTML
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   666
files would depend on files not owned by you. This prevents you from
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   667
changing the location of the HTML files (as they contain relative
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   668
paths) and also causes trouble if the database's maker (re)moves the
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   669
GIFs.
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   670
1409
3cc3fde8d005 setting base_path is now optional
clasohm
parents: 1387
diff changeset
   671
Here's what you should do before invoking {\tt init_html} using
1380
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   672
someone else's \ML{} database:
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   673
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   674
\begin{ttbox}
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   675
base_path := "/home/smith/isabelle";
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   676
gif_path := "/home/smith/isabelle/Tools";
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   677
init_html();
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   678
\dots
2f8055af9c04 changed HTML documentation
clasohm
parents: 1369
diff changeset
   679
\end{ttbox}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   680
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
\section{Terms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
\index{terms|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   683
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
with six constructors: there are six kinds of term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
type indexname = string * int;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
infix 9 $;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
datatype term = Const of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
              | Free  of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   690
              | Var   of indexname * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
              | Bound of int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
              | Abs   of string * typ * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   693
              | op $  of term * term;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   695
\begin{ttdescription}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   696
\item[\ttindexbold{Const}($a$, $T$)] \index{constants|bold}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   697
  is the {\bf constant} with name~$a$ and type~$T$.  Constants include
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   698
  connectives like $\land$ and $\forall$ as well as constants like~0
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   699
  and~$Suc$.  Other constants may be required to define a logic's concrete
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   700
  syntax.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   701
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   702
\item[\ttindexbold{Free}($a$, $T$)] \index{variables!free|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   703
  is the {\bf free variable} with name~$a$ and type~$T$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   705
\item[\ttindexbold{Var}($v$, $T$)] \index{unknowns|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   706
  is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   707
  \mltydx{indexname} is a string paired with a non-negative index, or
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   708
  subscript; a term's scheme variables can be systematically renamed by
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   709
  incrementing their subscripts.  Scheme variables are essentially free
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   710
  variables, but may be instantiated during unification.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   712
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   713
  is the {\bf bound variable} with de Bruijn index~$i$, which counts the
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   714
  number of lambdas, starting from zero, between a variable's occurrence
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   715
  and its binding.  The representation prevents capture of variables.  For
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   716
  more information see de Bruijn \cite{debruijn72} or
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   717
  Paulson~\cite[page~336]{paulson91}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   718
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   719
\item[\ttindexbold{Abs}($a$, $T$, $u$)]
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   720
  \index{lambda abs@$\lambda$-abstractions|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   721
  is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   722
  variable has name~$a$ and type~$T$.  The name is used only for parsing
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   723
  and printing; it has no logical significance.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   724
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   725
\item[$t$ \$ $u$] \index{$@{\tt\$}|bold} \index{function applications|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   726
is the {\bf application} of~$t$ to~$u$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   727
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   728
Application is written as an infix operator to aid readability.
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   729
Here is an \ML\ pattern to recognize \FOL{} formulae of
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   731
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   733
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   734
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   735
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   736
\section{Variable binding}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   737
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   738
loose_bnos     : term -> int list
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   739
incr_boundvars : int -> term -> term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   740
abstract_over  : term*term -> term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   741
variant_abs    : string * typ * term -> string * term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   742
aconv          : term*term -> bool\hfill{\bf infix}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   743
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   744
These functions are all concerned with the de Bruijn representation of
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   745
bound variables.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   746
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   747
\item[\ttindexbold{loose_bnos} $t$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   748
  returns the list of all dangling bound variable references.  In
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   749
  particular, {\tt Bound~0} is loose unless it is enclosed in an
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   750
  abstraction.  Similarly {\tt Bound~1} is loose unless it is enclosed in
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   751
  at least two abstractions; if enclosed in just one, the list will contain
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   752
  the number 0.  A well-formed term does not contain any loose variables.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   753
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   754
\item[\ttindexbold{incr_boundvars} $j$]
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   755
  increases a term's dangling bound variables by the offset~$j$.  This is
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   756
  required when moving a subterm into a context where it is enclosed by a
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   757
  different number of abstractions.  Bound variables with a matching
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   758
  abstraction are unaffected.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   759
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   760
\item[\ttindexbold{abstract_over} $(v,t)$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   761
  forms the abstraction of~$t$ over~$v$, which may be any well-formed term.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   762
  It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   763
  correct index.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   764
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   765
\item[\ttindexbold{variant_abs} $(a,T,u)$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   766
  substitutes into $u$, which should be the body of an abstraction.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   767
  It replaces each occurrence of the outermost bound variable by a free
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   768
  variable.  The free variable has type~$T$ and its name is a variant
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   769
  of~$a$ chosen to be distinct from all constants and from all variables
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   770
  free in~$u$.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   771
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   772
\item[$t$ \ttindexbold{aconv} $u$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   773
  tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   774
  to renaming of bound variables.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   775
\begin{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   776
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   777
    Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   778
    if their names and types are equal.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   779
    (Variables having the same name but different types are thus distinct.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   780
    This confusing situation should be avoided!)
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   781
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   782
    Two bound variables are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   783
    if they have the same number.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   784
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   785
    Two abstractions are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   786
    if their bodies are, and their bound variables have the same type.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   787
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   788
    Two applications are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   789
    if the corresponding subterms are.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   790
\end{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   791
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   792
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   793
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   794
\section{Certified terms}\index{terms!certified|bold}\index{signatures}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   795
A term $t$ can be {\bf certified} under a signature to ensure that every type
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   796
in~$t$ is well-formed and every constant in~$t$ is a type instance of a
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   797
constant declared in the signature.  The term must be well-typed and its use
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   798
of bound variables must be well-formed.  Meta-rules such as {\tt forall_elim}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   799
take certified terms as arguments.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   800
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   801
Certified terms belong to the abstract type \mltydx{cterm}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   802
Elements of the type can only be created through the certification process.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   803
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   804
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   805
\subsection{Printing terms}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   806
\index{terms!printing of}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   807
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   808
     string_of_cterm :           cterm -> string
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   809
Sign.string_of_term  : Sign.sg -> term -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   810
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   811
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   812
\item[\ttindexbold{string_of_cterm} $ct$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   813
displays $ct$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   814
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   815
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   816
displays $t$ as a string, using the syntax of~$sign$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   817
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   818
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   819
\subsection{Making and inspecting certified terms}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   820
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   821
cterm_of   : Sign.sg -> term -> cterm
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   822
read_cterm : Sign.sg -> string * typ -> cterm
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   823
cert_axm   : Sign.sg -> string * term -> string * term
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   824
read_axm   : Sign.sg -> string * string -> string * term
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   825
rep_cterm  : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   826
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   827
\begin{ttdescription}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   828
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   829
certifies $t$ with respect to signature~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   830
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   831
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   832
reads the string~$s$ using the syntax of~$sign$, creating a certified term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   833
The term is checked to have type~$T$; this type also tells the parser what
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   834
kind of phrase to parse.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   835
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   836
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   837
certifies $t$ with respect to $sign$ as a meta-proposition and converts all
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   838
exceptions to an error, including the final message
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   839
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   840
The error(s) above occurred in axiom "\(name\)"
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   841
\end{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   842
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   843
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   844
similar to {\tt cert_axm}, but first reads the string $s$ using the syntax of
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   845
$sign$.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   846
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   847
\item[\ttindexbold{rep_cterm} $ct$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   848
decomposes $ct$ as a record containing its type, the term itself, its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   849
signature, and the maximum subscript of its unknowns.  The type and maximum
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   850
subscript are computed during certification.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   851
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   852
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   853
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   854
\section{Types}\index{types|bold}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   855
Types belong to the \ML\ type \mltydx{typ}, which is a concrete datatype with
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   856
three constructor functions.  These correspond to type constructors, free
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   857
type variables and schematic type variables.  Types are classified by sorts,
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   858
which are lists of classes (representing an intersection).  A class is
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   859
represented by a string.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   860
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   861
type class = string;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   862
type sort  = class list;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   863
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   864
datatype typ = Type  of string * typ list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   865
             | TFree of string * sort
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   866
             | TVar  of indexname * sort;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   867
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   868
infixr 5 -->;
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   869
fun S --> T = Type ("fun", [S, T]);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   870
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   871
\begin{ttdescription}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   872
\item[\ttindexbold{Type}($a$, $Ts$)] \index{type constructors|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   873
  applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   874
  Type constructors include~\tydx{fun}, the binary function space
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   875
  constructor, as well as nullary type constructors such as~\tydx{prop}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   876
  Other type constructors may be introduced.  In expressions, but not in
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   877
  patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   878
  types.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   879
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   880
\item[\ttindexbold{TFree}($a$, $s$)] \index{type variables|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   881
  is the {\bf type variable} with name~$a$ and sort~$s$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   882
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   883
\item[\ttindexbold{TVar}($v$, $s$)] \index{type unknowns|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   884
  is the {\bf type unknown} with indexname~$v$ and sort~$s$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   885
  Type unknowns are essentially free type variables, but may be
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   886
  instantiated during unification.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   887
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   888
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   889
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   890
\section{Certified types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   891
\index{types!certified|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   892
Certified types, which are analogous to certified terms, have type
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   893
\ttindexbold{ctyp}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   894
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   895
\subsection{Printing types}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   896
\index{types!printing of}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   897
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   898
     string_of_ctyp :           ctyp -> string
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   899
Sign.string_of_typ  : Sign.sg -> typ -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   900
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   901
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   902
\item[\ttindexbold{string_of_ctyp} $cT$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   903
displays $cT$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   904
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   905
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   906
displays $T$ as a string, using the syntax of~$sign$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   907
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   908
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   909
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   910
\subsection{Making and inspecting certified types}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   911
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   912
ctyp_of  : Sign.sg -> typ -> ctyp
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   913
rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   914
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   915
\begin{ttdescription}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   916
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   917
certifies $T$ with respect to signature~$sign$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   918
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   919
\item[\ttindexbold{rep_ctyp} $cT$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   920
decomposes $cT$ as a record containing the type itself and its signature.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   921
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   922
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   923
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   924
\section{Oracles: calling external reasoners }
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   925
\label{sec:oracles}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   926
\index{oracles|(}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   927
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   928
Oracles allow Isabelle to take advantage of external reasoners such as
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   929
arithmetic decision procedures, model checkers, fast tautology checkers or
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   930
computer algebra systems.  Invoked as an oracle, an external reasoner can
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   931
create arbitrary Isabelle theorems.  It is your responsibility to ensure that
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   932
the external reasoner is as trustworthy as your application requires.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   933
Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   934
depends upon oracle calls.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   935
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   936
\begin{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   937
     invoke_oracle : theory * Sign.sg * exn -> thm
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   938
     set_oracle    : Sign.sg -> typ -> string
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   939
\end{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   940
\begin{ttdescription}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   941
\item[\ttindexbold{invoke_oracle} ($thy$, $sign$, $exn$)] invokes the oracle
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   942
  of theory $thy$ passing the information contained in the exception value
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   943
  $exn$ and creating a theorem having signature $sign$.  Errors arise if $thy$
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   944
  does not have an oracle, if the oracle rejects its arguments or if its
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   945
  result is ill-typed.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   946
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   947
\item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   948
  be $fn$.  It is seldom called explicitly, as there is syntax for oracles in
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   949
  theory files.  A theory can have at most one oracle.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   950
\end{ttdescription}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   951
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   952
A curious feature of {\ML} exceptions is that they are ordinary constructors.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   953
The {\ML} type {\tt exn} is a datatype that can be extended at any time.  (See
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   954
my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   955
page~136.)  The oracle mechanism takes advantage of this to allow an oracle to
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   956
take any information whatever.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   957
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   958
There must be some way of invoking the external reasoner from \ML, either
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   959
because it is coded in {\ML} or via an operating system interface.  Isabelle
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   960
expects the {\ML} function to take two arguments: a signature and an
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   961
exception.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   962
\begin{itemize}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   963
\item The signature will typically be that of a desendant of the theory
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   964
  declaring the oracle.  The oracle will use it to distinguish constants from
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   965
  variables, etc., and it will be attached to the generated theorems.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   966
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   967
\item The exception is used to pass arbitrary information to the oracle.  This
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   968
  information must contain a full description of the problem to be solved by
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   969
  the external reasoner, including any additional information that might be
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   970
  required.  The oracle may raise the exception to indicate that it cannot
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   971
  solve the specified problem.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   972
\end{itemize}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   973
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   974
A trivial example is provided on directory {\tt FOL/ex}.  This oracle
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   975
generates tautologies of the form $P\bimp\cdots\bimp P$, with an even number
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   976
of $P$s. 
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   977
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   978
File {\tt declIffOracle.ML} begins by declaring a new exception constructor
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   979
for the oracle the information it requires: here, just an integer.  It
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   980
contains some code (suppressed below) for creating the tautologies, and
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   981
finally declares the oracle function itself:
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   982
\begin{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   983
exception IffOracleExn of int;
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   984
\(\vdots\)
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   985
fun mk_iff_oracle (sign, IffOracleExn n) = 
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   986
    if n>0 andalso n mod 2 = 0 
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   987
    then Trueprop $ mk_iff n
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   988
    else raise IffOracleExn n;
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   989
\end{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   990
Observe the function two arguments, the signature {\tt sign} and the exception
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   991
given as a pattern.  The function checks its argument for validity.  If $n$ is
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   992
positive and even then it creates a tautology containing $n$ occurrences
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   993
of~$P$.  Otherwise it signals error by raising its own exception.  Errors may
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   994
be signalled by other means, such as returning the theorem {\tt True}.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   995
Please ensure that the oracle's result is correctly typed; Isabelle will
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   996
reject ill-typed theorems by raising a cryptic exception at top level.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   997
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   998
The theory file {\tt IffOracle.thy} packages up the function above as an
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   999
oracle.  The first line indicates that the new theory depends upon the file
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1000
{\tt declIffOracle.ML} (which declares the {\ML} code) as well as on \FOL.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1001
The second line informs Isabelle that this theory has an oracle given by the
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1002
function {\tt mk_iff_oracle}.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1003
\begin{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1004
IffOracle = "declIffOracle" + FOL +
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1005
oracle mk_iff_oracle
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1006
end
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1007
\end{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1008
Because a theory can have at most one oracle, the theory itself serves to
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1009
identify the oracle.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1010
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1011
Here are some examples of invoking the oracle.  An argument of 10 is allowed,
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1012
but one of 5 is forbidden:
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1013
\begin{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1014
invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1015
{\out  "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1016
invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5); 
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1017
{\out Exception- IffOracleExn 5 raised}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1018
\end{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1019
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
  1020
\index{oracles|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
  1021
\index{theories|)}