doc-src/Ref/theories.tex
author wenzelm
Fri, 09 Jan 1998 13:49:20 +0100
changeset 4543 82a45bdd0e80
parent 4384 429cba89b4c8
child 4597 a0bdee64194c
permissions -rw-r--r--
several minor updates;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3201
7c3cbf675e85 removed garbage;
wenzelm
parents: 3108
diff changeset
     1
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
%% $Id$
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
     3
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
\chapter{Theories, Terms and Types} \label{theories}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
\index{theories|(}\index{signatures|bold}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
     6
\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
     7
syntax, declarations and axioms of a mathematical development.  They
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
     8
are built, starting from the {\Pure} or {\CPure} theory, by extending
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
     9
and merging existing theories.  They have the \ML\ type
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    10
\mltydx{theory}.  Theory operations signal errors by raising exception
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    11
\xdx{THEORY}, returning a message and a list of theories.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
Signatures, which contain information about sorts, types, constants and
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
    14
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
    15
signature carries a unique list of \bfindex{stamps}, which are \ML\
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    16
references to strings.  The strings serve as human-readable names; the
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
references serve as unique identifiers.  Each primitive signature has a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
single stamp.  When two signatures are merged, their lists of stamps are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
also merged.  Every theory carries a unique signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
Terms and types are the underlying representation of logical syntax.  Their
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    22
\ML\ definitions are irrelevant to naive Isabelle users.  Programmers who
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    23
wish to extend Isabelle may need to know such details, say to code a tactic
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    24
that looks for subgoals of a particular form.  Terms and types may be
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
`certified' to be well-formed with respect to a given signature.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    27
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    28
\section{Defining theories}\label{sec:ref-defining-theories}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    30
Theories are usually defined using theory definition files (which have a name
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
    31
suffix {\tt .thy}).  There is also a low level interface provided by certain
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    32
\ML{} functions (see \S\ref{BuildingATheory}).
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    33
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
    34
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
    35
\begin{description}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    36
\item[{\it theoryDef}] is the full definition.  The new theory is
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    37
  called $id$.  It is the union of the named {\bf parent
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    38
    theories}\indexbold{theories!parent}, possibly extended with new
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    39
  components.  \thydx{Pure} and \thydx{CPure} are the basic theories,
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
    40
  which contain only the meta-logic.  They differ just in their
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    41
  concrete syntax for function applications.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
    42
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    43
  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
    44
  Quoted strings can be used to document additional file dependencies; see
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
    45
  \S\ref{LoadingTheories} for details.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    46
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    47
\item[$classes$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    48
  is a series of class declarations.  Declaring {\tt$id$ < $id@1$ \dots\
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    49
    $id@n$} makes $id$ a subclass of the existing classes $id@1\dots
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    50
  id@n$.  This rules out cyclic class structures.  Isabelle automatically
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    51
  computes the transitive closure of subclass hierarchies; it is not
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    52
  necessary to declare {\tt c < e} in addition to {\tt c < d} and {\tt d <
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    53
    e}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    54
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    55
\item[$default$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    56
  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
    57
  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
    58
  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
    59
  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
    60
  intersection).
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    61
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    62
\item[$sort$] is a finite set of classes.  A single class $id$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    63
  abbreviates the sort $\ttlbrace id\ttrbrace$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    64
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    65
\item[$types$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    66
  is a series of type declarations.  Each declares a new type constructor
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    67
  or type synonym.  An $n$-place type constructor is specified by
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    68
  $(\alpha@1,\dots,\alpha@n)name$, where the type variables serve only to
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    69
  indicate the number~$n$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    70
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
    71
  A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1380
diff changeset
    72
  $(\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
    73
  be strings.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    74
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    75
\item[$infix$]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    76
  declares a type or constant to be an infix operator of priority $nat$
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
    77
  associating to the left ({\tt infixl}) or right ({\tt infixr}).  Only
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
    78
  2-place type constructors can have infix status; an example is {\tt
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    79
  ('a,'b)~"*"~(infixr~20)}, which may express binary product types.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    80
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    81
\item[$arities$] is a series of type arity declarations.  Each assigns
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    82
  arities to type constructors.  The $name$ must be an existing type
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    83
  constructor, which is given the additional arity $arity$.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    84
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    85
\item[$consts$] is a series of constant declarations.  Each new
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    86
  constant $name$ is given the specified type.  The optional $mixfix$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    87
  annotations may attach concrete syntax to the constant.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    88
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    89
\item[$syntax$] \index{*syntax section}\index{print mode} is a variant
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    90
  of $consts$ which adds just syntax without actually declaring
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    91
  logical constants.  This gives full control over a theory's context
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
    92
  free grammar.  The optional $mode$ specifies the print mode where the
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
    93
  mixfix productions should be added.  If there is no \texttt{output}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    94
  option given, all productions are also added to the input syntax
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
    95
  (regardless of the print mode).
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    96
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    97
\item[$mixfix$] \index{mixfix declarations}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
    98
  annotations can take three forms:
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
    99
  \begin{itemize}
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
   100
  \item A mixfix template given as a $string$ of the form
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
   101
    {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   102
    indicates the position where the $i$-th argument should go.  The list
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   103
    of numbers gives the priority of each argument.  The final number gives
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   104
    the priority of the whole construct.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   106
  \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
   107
    infix} status.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   109
  \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
   110
    binder} status.  The declaration {\tt binder} $\cal Q$ $p$ causes
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   111
  ${\cal Q}\,x.F(x)$ to be treated
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   112
  like $f(F)$, where $p$ is the priority.
273
538db1a98ba3 *** empty log message ***
nipkow
parents: 185
diff changeset
   113
  \end{itemize}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   114
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   115
\item[$trans$]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   116
  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
   117
  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
   118
  ==}).
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   119
1650
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   120
\item[$rules$]
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   121
  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
   122
  given by the $string$.  Rule names must be distinct within any single
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   123
  theory.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   124
1905
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   125
\item[$defs$] is a series of definitions.  They are just like $rules$, except
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   126
  that every $string$ must be a definition (see below for details).
1650
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   127
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   128
\item[$constdefs$] combines the declaration of constants and their
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   129
  definition.  The first $string$ is the type, the second the definition.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   130
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   131
\item[$axclass$] \index{*axclass section} defines an
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   132
  \rmindex{axiomatic type class} as the intersection of existing
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   133
  classes, with additional axioms holding.  Class axioms may not
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   134
  contain more than one type variable.  The class axioms (with implicit
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   135
  sort constraints added) are bound to the given names.  Furthermore a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   136
  class introduction rule is generated, which is automatically
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   137
  employed by $instance$ to prove instantiations of this class.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   138
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   139
\item[$instance$] \index{*instance section} proves class inclusions or
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   140
  type arities at the logical level and then transfers these to the
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   141
  type signature.  The instantiation is proven and checked properly.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   142
  The user has to supply sufficient witness information: theorems
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   143
  ($longident$), axioms ($string$), or even arbitrary \ML{} tactic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   144
  code $verbatim$.
1650
a4ed2655b08c Added 'constdefs'
nipkow
parents: 1551
diff changeset
   145
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   146
\item[$oracle$] links the theory to a trusted external reasoner.  It is
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   147
  allowed to create theorems, but each theorem carries a proof object
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   148
  describing the oracle invocation.  See \S\ref{sec:oracles} for details.
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   149
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   150
\item[$local, global$] changes the current name declaration mode.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   151
  Initially, theories start in $local$ mode, causing all names of
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   152
  types, constants, axioms etc.\ to be automatically qualified by the
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   153
  theory name.  Changing this to $global$ causes all names to be
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   154
  declared as short base names only.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   155
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   156
  The $local$ and $global$ declarations act like switches, affecting
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   157
  all following theory sections until changed again explicitly.  Also
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   158
  note that the final state at the end of the theory will persist.  In
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   159
  particular, this determines how the names of theorems stored later
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   160
  on are handled.
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   161
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   162
\item[$ml$] \index{*ML section}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   163
  consists of \ML\ code, typically for parse and print translation functions.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
\end{description}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   165
%
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   166
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
   167
declarations, translation rules and the {\tt ML} section in more detail.
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   168
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   169
1905
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   170
\subsection{Definitions}\indexbold{definitions}
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   171
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   172
{\bf Definitions} are intended to express abbreviations.  The simplest
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   173
form of a definition is $f \equiv t$, where $f$ is a constant.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   174
Isabelle also allows a derived forms where the arguments of~$f$ appear
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   175
on the left, abbreviating a string of $\lambda$-abstractions.
1905
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   176
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   177
Isabelle makes the following checks on definitions:
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   178
\begin{itemize}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   179
\item Arguments (on the left-hand side) must be distinct variables.
1905
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   180
\item All variables on the right-hand side must also appear on the left-hand
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   181
  side. 
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   182
\item All type variables on the right-hand side must also appear on
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   183
  the left-hand side; this prohibits definitions such as {\tt
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   184
    (zero::nat) == length ([]::'a list)}.
1905
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   185
\item The definition must not be recursive.  Most object-logics provide
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   186
  definitional principles that can be used to express recursion safely.
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   187
\end{itemize}
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   188
These checks are intended to catch the sort of errors that might be made
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   189
accidentally.  Misspellings, for instance, might result in additional
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   190
variables appearing on the right-hand side.  More elaborate checks could be
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   191
made, but the cost might be overly strict rules on declaration order, etc.
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   192
81061bd61ad3 Added a new section on Definitions
paulson
parents: 1880
diff changeset
   193
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   194
\subsection{*Classes and arities}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   195
\index{classes!context conditions}\index{arities!context conditions}
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   196
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   197
In order to guarantee principal types~\cite{nipkow-prehofer},
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   198
arity declarations must obey two conditions:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   199
\begin{itemize}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   200
\item There must not be any two declarations $ty :: (\vec{r})c$ and
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   201
  $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$.  For example, this
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   202
  excludes the following:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   203
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   204
arities
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   205
  foo :: ({\ttlbrace}logic{\ttrbrace}) logic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   206
  foo :: ({\ttlbrace}{\ttrbrace})logic
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   207
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   208
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   209
\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
   210
  (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
   211
  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   212
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   213
expresses that the set of types represented by $s'$ is a subset of the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   214
set of types represented by $s$.  Assuming $term \preceq logic$, the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   215
following is forbidden:
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   216
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   217
arities
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   218
  foo :: ({\ttlbrace}logic{\ttrbrace})logic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   219
  foo :: ({\ttlbrace}{\ttrbrace})term
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   220
\end{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   221
145
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   222
\end{itemize}
422197c5a078 added subsection 'Classes and types';
wenzelm
parents: 141
diff changeset
   223
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   225
\section{Loading a new theory}\label{LoadingTheories}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   226
\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
   227
\begin{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   228
use_thy         : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   229
time_use_thy    : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   230
loadpath        : string list ref \hfill{\bf initially {\tt["."]}}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   231
delete_tmpfiles : bool ref \hfill{\bf initially true}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   232
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   233
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   234
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   235
\item[\ttindexbold{use_thy} $thyname$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   236
  reads the theory $thyname$ and creates an \ML{} structure as described below.
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   237
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   238
\item[\ttindexbold{time_use_thy} $thyname$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   239
  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
   240
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   241
\item[\ttindexbold{loadpath}]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   242
  contains a list of directories to search when locating the files that
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   243
  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
   244
    use_thy} does not specify the path explicitly.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   245
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   246
\item[reset \ttindexbold{delete_tmpfiles};]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   247
suppresses the deletion of temporary files.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   248
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   249
%
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   250
Each theory definition must reside in a separate file.  Let the file
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   251
{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   252
parent theories are $TB@1$ \dots $TB@n$.  Calling
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   253
\texttt{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy},
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   254
writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   255
latter file.  Recursive {\tt use_thy} calls load those parent theories
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   256
that have not been loaded previously; the recursive calls may continue
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   257
to any depth.  One {\tt use_thy} call can read an entire logic
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   258
provided all theories are linked appropriately.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   259
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   260
The result is an \ML\ structure~$T$ containing at least a component
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   261
{\tt thy} for the new theory and components for each of the rules.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   262
The structure also contains the definitions of the {\tt ML} section,
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   263
if present.  The file {\tt.{\it T}.thy.ML} is then deleted if {\tt
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   264
  delete_tmpfiles} is set and no errors occurred.
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   265
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   266
Finally the file {\it T}{\tt.ML} is read, if it exists.  The structure
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   267
$T$ is automatically open in this context.  Proof scripts typically
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   268
refer to its components by unqualified names.
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   269
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   270
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
   271
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
   272
{\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
   273
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
   274
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
   275
theories to their parents.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   276
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   277
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   278
\section{Reloading modified theories}\label{sec:reloading-theories}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   279
\indexbold{theories!reloading}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   280
\begin{ttbox}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   281
update     : unit -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   282
unlink_thy : string -> unit
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   283
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   284
Changing a theory on disk often makes it necessary to reload all theories
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   285
descended from it.  However, {\tt use_thy} reads only one theory, even if
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   286
some of the parent theories are out of date.  In this case you should call
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   287
{\tt update()}.
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   288
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   289
Isabelle keeps track of all loaded theories and their files.  If
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   290
\texttt{use_thy} finds that the theory to be loaded has been read
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   291
before, it determines whether to reload the theory as follows.  First
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   292
it looks for the theory's files in their previous location.  If it
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   293
finds them, it compares their modification times to the internal data
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   294
and stops if they are equal.  If the files have been moved, {\tt
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   295
  use_thy} searches for them as it would for a new theory.  After {\tt
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   296
  use_thy} reloads a theory, it marks the children as out-of-date.
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   297
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   298
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   299
\item[\ttindexbold{update}()]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   300
  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
   301
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   302
\item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   303
  informs Isabelle that theory $thyname$ no longer exists.  If you delete the
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   304
  theory files for $thyname$ then you must execute {\tt unlink_thy};
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   305
  otherwise {\tt update} will complain about a missing file.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   306
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   307
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   308
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   309
\subsection{*Pseudo theories}\label{sec:pseudo-theories}
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   310
\indexbold{theories!pseudo}%
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   311
Any automatic reloading facility requires complete knowledge of all
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   312
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
   313
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
   314
they could also be theorems, proof procedures, etc.
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   315
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   316
Unless such dependencies are documented, {\tt update} fails to reload these
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   317
\ML{} files and the system is left in a state where some objects, such as
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   318
theorems, still refer to old versions of theories.  This may lead to the
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   319
error
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   320
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   321
Attempt to merge different versions of theories: \dots
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   322
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   323
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
   324
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
   325
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   326
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
   327
theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   328
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
   329
mention this dependency as follows:
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   330
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   331
B = \(\ldots\) + "orphan" + \(\ldots\)
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   332
\end{ttbox}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   333
Quoted strings stand for theories which have to be loaded before the
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   334
current theory is read but which are not used in building the base of
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   335
theory~$B$.  Whenever {\tt orphan} changes and is reloaded, Isabelle
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   336
knows that $B$ has to be updated, too.
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   337
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   338
Note that it's necessary for {\tt orphan} to declare a special ML
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   339
object of type {\tt theory} which is present in all theories.  This is
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   340
normally achieved by adding the file {\tt orphan.thy} to make {\tt
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   341
orphan} a {\bf pseudo theory}.  A minimum version of {\tt orphan.thy}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   342
would be
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   343
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   344
\begin{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   345
orphan = Pure
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   346
\end{ttbox}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   347
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3201
diff changeset
   348
which uses {\tt Pure} to make a dummy theory.  Normally though the
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   349
orphaned file has its own dependencies.  If {\tt orphan.ML} depends on
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   350
theories or files $A@1$, \ldots, $A@n$, record this by creating the
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   351
pseudo theory in the following way:
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   352
\begin{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   353
orphan = \(A@1\) + \(\ldots\) + \(A@n\)
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   354
\end{ttbox}
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   355
The resulting theory ensures that {\tt update} reloads {\tt orphan}
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   356
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
   357
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   358
For an extensive example of how this technique can be used to link
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   359
lots of theory files and load them by just a few {\tt use_thy} calls
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   360
see the sources of one of the major object-logics (e.g.\ \ZF).
138
9ba8bff1addc added chapter "Defining Theories" and made changes for new Readthy functions
clasohm
parents: 104
diff changeset
   361
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   364
\section{Basic operations on theories}\label{BasicOperationsOnTheories}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   365
\subsection{Retrieving axioms and theorems}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   366
\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
   367
\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
   368
\begin{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   369
get_axiom : theory -> xstring -> thm
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   370
get_thm   : theory -> xstring -> thm
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   371
get_thms  : theory -> xstring -> thm list
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   372
axioms_of : theory -> (string * thm) list
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   373
thms_of   : theory -> (string * thm) list
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   374
assume_ax : theory -> string -> thm
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   376
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   377
\item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   378
  given $name$ from $thy$ or any of its ancestors, raising exception
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   379
  \xdx{THEORY} if none exists.  Merging theories can cause several
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   380
  axioms to have the same name; {\tt get_axiom} returns an arbitrary
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   381
  one.  Usually, axioms are also stored as theorems and may be
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   382
  retrieved via \texttt{get_thm} as well.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   383
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   384
\item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   385
    get_axiom}, but looks for a theorem stored in the theory's
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   386
  database.  Like {\tt get_axiom} it searches all parents of a theory
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   387
  if the theorem is not found directly in $thy$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   388
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   389
\item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   390
  for retrieving theorem lists stored within the theory.  It returns a
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   391
  singleton list if $name$ actually refers to a theorem rather than a
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   392
  theorem list.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   393
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   394
\item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   395
  node, not including the ones of its ancestors.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   396
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   397
\item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   398
  the database of this theory node, not including the ones of its
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   399
  ancestors.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   400
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   401
\item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   402
  using the syntax of $thy$, following the same conventions as axioms
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   403
  in a theory definition.  You can thus pretend that {\it formula} is
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   404
  an axiom and use the resulting theorem like an axiom.  Actually {\tt
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   405
    assume_ax} returns an assumption; \ttindex{qed} and
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   406
  \ttindex{result} complain about additional assumptions, but
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   407
  \ttindex{uresult} does not.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
For example, if {\it formula} is
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   410
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   411
\hbox{\verb'?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]'}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   412
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
4384
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   414
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   415
\subsection{*Theory inclusion}
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   416
\begin{ttbox}
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   417
subthy      : theory * theory -> bool
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   418
eq_thy      : theory * theory -> bool
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   419
transfer    : theory -> thm -> thm
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   420
transfer_sg : Sign.sg -> thm -> thm
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   421
\end{ttbox}
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   422
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   423
Inclusion and equality of theories is determined by unique
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   424
identification stamps that are created when declaring new components.
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   425
Theorems contain a reference to the theory (actually to its signature)
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   426
they have been derived in.  Transferring theorems to super theories
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   427
has no logical significance, but may affect some operations in subtle
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   428
ways (e.g.\ implicit merges of signatures when applying rules, or
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   429
pretty printing of theorems).
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   430
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   431
\begin{ttdescription}
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   432
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   433
\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   434
  is included in $thy@2$ wrt.\ identification stamps.
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   435
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   436
\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   437
  is exactly the same as $thy@2$.
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   438
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   439
\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   440
  theory $thy$, provided the latter includes the theory of $thm$.
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   441
  
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   442
\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   443
  \texttt{transfer}, but identifies the super theory via its
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   444
  signature.
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   445
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   446
\end{ttdescription}
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   447
429cba89b4c8 \subsection{*Theory inclusion};
wenzelm
parents: 4374
diff changeset
   448
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   449
\subsection{*Building a theory}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   450
\label{BuildingATheory}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   451
\index{theories!constructing|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   452
\begin{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   453
ProtoPure.thy  : theory
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   454
Pure.thy       : theory
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   455
CPure.thy      : theory
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   456
merge_theories : string -> theory * theory -> theory
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   457
\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   458
\begin{description}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   459
\item[\ttindexbold{ProtoPure.thy}, \ttindexbold{Pure.thy},
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   460
  \ttindexbold{CPure.thy}] contain the syntax and signature of the
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   461
  meta-logic.  There are basically no axioms: meta-level inferences
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   462
  are carried out by \ML\ functions.  \texttt{Pure} and \texttt{CPure}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   463
  just differ in their concrete syntax of prefix function application:
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   464
  $t(u@1, \ldots, u@n)$ in \texttt{Pure} vs.\ $t\,u@1,\ldots\,u@n$ in
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   465
  \texttt{CPure}.  \texttt{ProtoPure} is their common parent,
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   466
  containing no syntax for printing prefix applications at all!
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   467
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   468
\item[\ttindexbold{merge_theories} $name$ ($thy@1$, $thy@2$)] merges
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   469
  the two theories $thy@1$ and $thy@2$, creating a new named theory
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   470
  node.  The resulting theory contains all of the syntax, signature
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   471
  and axioms of the constituent theories.  Merging theories that
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   472
  contain different identification stamps of the same name fails with
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   473
  the following message
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   474
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   475
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
   476
\end{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   477
This error may especially occur when a theory is redeclared --- say to
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   478
change an inappropriate definition --- and bindings to old versions
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   479
persist.  Isabelle ensures that old and new theories of the same name
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   480
are not involved in a proof.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   481
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   482
%% FIXME
478
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   483
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
838bd766d536 added init_thy_reader and removed extend_theory
nipkow
parents: 332
diff changeset
   484
%  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
   485
%  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
   486
%  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
   487
%  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
   488
%  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
   489
%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
   490
%\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   491
%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
   492
%\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   493
\end{description}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   494
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   495
%% FIXME
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   496
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   497
%      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   498
%\hfill\break   %%% include if line is just too short
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   499
%is the \ML{} equivalent of the following theory definition:
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   500
%\begin{ttbox}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   501
%\(T\) = \(thy\) +
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   502
%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   503
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   504
%default {\(d@1,\dots,d@r\)}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   505
%types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   506
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   507
%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   508
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   509
%consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   510
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   511
%rules   \(name\) \(rule\)
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   512
%        \dots
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   513
%end
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   514
%\end{ttbox}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   515
%where
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   516
%\begin{tabular}[t]{l@{~=~}l}
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   517
%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   518
%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   519
%$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   520
%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   521
%\\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   522
%$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   523
%$rules$   & \tt[("$name$",$rule$),\dots]
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   524
%\end{tabular}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   527
\subsection{Inspecting a theory}\label{sec:inspct-thy}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
\index{theories!inspecting|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   529
\begin{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   530
print_syntax        : theory -> unit
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   531
print_theory        : theory -> unit
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   532
print_data          : theory -> string -> unit
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   533
parents_of          : theory -> theory list
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   534
ancestors_of        : theory -> theory list
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   535
sign_of             : theory -> Sign.sg
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   536
Sign.stamp_names_of : Sign.sg -> string list
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
\end{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   538
These provide means of viewing a theory's components.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   539
\begin{ttdescription}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   540
\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   541
  (grammar, macros, translation functions etc., see
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   542
  page~\pageref{pg:print_syn} for more details).
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   543
  
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   544
\item[\ttindexbold{print_theory} $thy$] prints the logical parts of
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   545
  $thy$, excluding the syntax.
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   546
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   547
\item[\ttindexbold{print_data} $thy$ $kind$] prints generic data of
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   548
  $thy$.  This invokes the print method associated with $kind$.  Refer
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   549
  to the output of \texttt{print_theory} for a list of available data
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   550
  kinds in $thy$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   551
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   552
\item[\ttindexbold{parents_of} $thy$] returns the direct ancestors
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   553
  of~$thy$.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   554
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   555
\item[\ttindexbold{ancestors_of} $thy$] returns all ancestors of~$thy$
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   556
  (not including $thy$ itself).
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   557
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   558
\item[\ttindexbold{sign_of} $thy$] returns the signature associated
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   559
  with~$thy$.  It is useful with functions like {\tt
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   560
    read_instantiate_sg}, which take a signature as an argument.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   561
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   562
\item[\ttindexbold{Sign.stamp_names_of} $sg$]\index{signatures}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   563
  returns the names of the identification \rmindex{stamps} of ax
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   564
  signature.  These coincide with the names of its full ancestry
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   565
  including that of $sg$ itself.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   567
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
1369
b82815e61b30 corrected documentation of pseudo theories;
clasohm
parents: 866
diff changeset
   569
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
\section{Terms}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
\index{terms|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   572
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 1905
diff changeset
   573
with six constructors:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
type indexname = string * int;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
infix 9 $;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
datatype term = Const of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
              | Free  of string * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
              | Var   of indexname * typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
              | Bound of int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
              | Abs   of string * typ * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
              | op $  of term * term;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   584
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   585
\item[\ttindexbold{Const} ($a$, $T$)] \index{constants|bold}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   586
  is the {\bf constant} with name~$a$ and type~$T$.  Constants include
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   587
  connectives like $\land$ and $\forall$ as well as constants like~0
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   588
  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
   589
  syntax.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   591
\item[\ttindexbold{Free} ($a$, $T$)] \index{variables!free|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   592
  is the {\bf free variable} with name~$a$ and type~$T$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   594
\item[\ttindexbold{Var} ($v$, $T$)] \index{unknowns|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   595
  is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   596
  \mltydx{indexname} is a string paired with a non-negative index, or
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   597
  subscript; a term's scheme variables can be systematically renamed by
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   598
  incrementing their subscripts.  Scheme variables are essentially free
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   599
  variables, but may be instantiated during unification.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   601
\item[\ttindexbold{Bound} $i$] \index{variables!bound|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   602
  is the {\bf bound variable} with de Bruijn index~$i$, which counts the
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   603
  number of lambdas, starting from zero, between a variable's occurrence
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   604
  and its binding.  The representation prevents capture of variables.  For
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   605
  more information see de Bruijn \cite{debruijn72} or
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   606
  Paulson~\cite[page~336]{paulson91}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   608
\item[\ttindexbold{Abs} ($a$, $T$, $u$)]
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   609
  \index{lambda abs@$\lambda$-abstractions|bold}
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   610
  is the $\lambda$-{\bf abstraction} with body~$u$, and whose bound
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   611
  variable has name~$a$ and type~$T$.  The name is used only for parsing
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   612
  and printing; it has no logical significance.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   614
\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
   615
is the {\bf application} of~$t$ to~$u$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   616
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   617
Application is written as an infix operator to aid readability.
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   618
Here is an \ML\ pattern to recognize \FOL{} formulae of
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
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
   620
\begin{ttbox}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   625
\section{*Variable binding}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   626
\begin{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   627
loose_bnos     : term -> int list
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   628
incr_boundvars : int -> term -> term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   629
abstract_over  : term*term -> term
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   630
variant_abs    : string * typ * term -> string * term
4374
wenzelm
parents: 4317
diff changeset
   631
aconv          : term * term -> bool\hfill{\bf infix}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   632
\end{ttbox}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   633
These functions are all concerned with the de Bruijn representation of
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   634
bound variables.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   635
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   636
\item[\ttindexbold{loose_bnos} $t$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   637
  returns the list of all dangling bound variable references.  In
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   638
  particular, {\tt Bound~0} is loose unless it is enclosed in an
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   639
  abstraction.  Similarly {\tt Bound~1} is loose unless it is enclosed in
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   640
  at least two abstractions; if enclosed in just one, the list will contain
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   641
  the number 0.  A well-formed term does not contain any loose variables.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   642
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   643
\item[\ttindexbold{incr_boundvars} $j$]
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   644
  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
   645
  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
   646
  different number of abstractions.  Bound variables with a matching
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   647
  abstraction are unaffected.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   648
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   649
\item[\ttindexbold{abstract_over} $(v,t)$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   650
  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
   651
  It replaces every occurrence of \(v\) by a {\tt Bound} variable with the
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   652
  correct index.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   653
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   654
\item[\ttindexbold{variant_abs} $(a,T,u)$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   655
  substitutes into $u$, which should be the body of an abstraction.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   656
  It replaces each occurrence of the outermost bound variable by a free
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   657
  variable.  The free variable has type~$T$ and its name is a variant
332
01b87a921967 final Springer copy
lcp
parents: 324
diff changeset
   658
  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
   659
  free in~$u$.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   660
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   661
\item[$t$ \ttindexbold{aconv} $u$]
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   662
  tests whether terms~$t$ and~$u$ are \(\alpha\)-convertible: identical up
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   663
  to renaming of bound variables.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   664
\begin{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   665
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   666
    Two constants, {\tt Free}s, or {\tt Var}s are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   667
    if their names and types are equal.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   668
    (Variables having the same name but different types are thus distinct.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   669
    This confusing situation should be avoided!)
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   670
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   671
    Two bound variables are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   672
    if they have the same number.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   673
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   674
    Two abstractions are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   675
    if their bodies are, and their bound variables have the same type.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   676
  \item
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   677
    Two applications are \(\alpha\)-convertible
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   678
    if the corresponding subterms are.
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   679
\end{itemize}
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   680
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   681
\end{ttdescription}
286
e7efbf03562b first draft of Springer book
lcp
parents: 275
diff changeset
   682
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   683
\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
   684
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
   685
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
   686
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
   687
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
   688
take certified terms as arguments.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   690
Certified terms belong to the abstract type \mltydx{cterm}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
Elements of the type can only be created through the certification process.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
In case of error, Isabelle raises exception~\ttindex{TERM}\@.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   693
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
\subsection{Printing terms}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   695
\index{terms!printing of}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   696
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   697
     string_of_cterm :           cterm -> string
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
Sign.string_of_term  : Sign.sg -> term -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   700
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   701
\item[\ttindexbold{string_of_cterm} $ct$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   702
displays $ct$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   703
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   704
\item[\ttindexbold{Sign.string_of_term} $sign$ $t$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
displays $t$ as a string, using the syntax of~$sign$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   706
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
\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
   709
\begin{ttbox}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   710
cterm_of          : Sign.sg -> term -> cterm
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   711
read_cterm        : Sign.sg -> string * typ -> cterm
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   712
cert_axm          : Sign.sg -> string * term -> string * term
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   713
read_axm          : Sign.sg -> string * string -> string * term
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   714
rep_cterm         : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   715
Sign.certify_term : Sign.sg -> term -> term * typ * int
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   716
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   717
\begin{ttdescription}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   718
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   719
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures} certifies
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   720
  $t$ with respect to signature~$sign$.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   721
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   722
\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] reads the string~$s$
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   723
  using the syntax of~$sign$, creating a certified term.  The term is
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   724
  checked to have type~$T$; this type also tells the parser what kind
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   725
  of phrase to parse.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   726
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   727
\item[\ttindexbold{cert_axm} $sign$ ($name$, $t$)] certifies $t$ with
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   728
  respect to $sign$ as a meta-proposition and converts all exceptions
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   729
  to an error, including the final message
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   730
\begin{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   731
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
   732
\end{ttbox}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   733
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   734
\item[\ttindexbold{read_axm} $sign$ ($name$, $s$)] similar to {\tt
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   735
    cert_axm}, but first reads the string $s$ using the syntax of
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   736
  $sign$.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   737
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   738
\item[\ttindexbold{rep_cterm} $ct$] decomposes $ct$ as a record
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   739
  containing its type, the term itself, its signature, and the maximum
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   740
  subscript of its unknowns.  The type and maximum subscript are
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   741
  computed during certification.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   742
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   743
\item[\ttindexbold{Sign.certify_term}] is a more primitive version of
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   744
  \texttt{cterm_of}, returning the internal representation instead of
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   745
  an abstract \texttt{cterm}.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   746
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   747
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   748
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   749
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   750
\section{Types}\index{types|bold}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   751
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
   752
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
   753
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
   754
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
   755
represented by a string.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
type class = string;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   758
type sort  = class list;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   760
datatype typ = Type  of string * typ list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   761
             | TFree of string * sort
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   762
             | TVar  of indexname * sort;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   763
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   764
infixr 5 -->;
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   765
fun S --> T = Type ("fun", [S, T]);
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   766
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   767
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   768
\item[\ttindexbold{Type} ($a$, $Ts$)] \index{type constructors|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   769
  applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   770
  Type constructors include~\tydx{fun}, the binary function space
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   771
  constructor, as well as nullary type constructors such as~\tydx{prop}.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   772
  Other type constructors may be introduced.  In expressions, but not in
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   773
  patterns, \hbox{\tt$S$-->$T$} is a convenient shorthand for function
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   774
  types.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   775
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   776
\item[\ttindexbold{TFree} ($a$, $s$)] \index{type variables|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   777
  is the {\bf type variable} with name~$a$ and sort~$s$.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   778
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   779
\item[\ttindexbold{TVar} ($v$, $s$)] \index{type unknowns|bold}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   780
  is the {\bf type unknown} with indexname~$v$ and sort~$s$.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   781
  Type unknowns are essentially free type variables, but may be
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   782
  instantiated during unification.
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   783
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   784
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   785
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   786
\section{Certified types}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   787
\index{types!certified|bold}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   788
Certified types, which are analogous to certified terms, have type
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   789
\ttindexbold{ctyp}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   790
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   791
\subsection{Printing types}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   792
\index{types!printing of}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   793
\begin{ttbox}
275
933ec96c522e update towards LNCS
nipkow
parents: 273
diff changeset
   794
     string_of_ctyp :           ctyp -> string
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   795
Sign.string_of_typ  : Sign.sg -> typ -> string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   796
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   797
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   798
\item[\ttindexbold{string_of_ctyp} $cT$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   799
displays $cT$ as a string.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   800
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 478
diff changeset
   801
\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$]
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   802
displays $T$ as a string, using the syntax of~$sign$.
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   803
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   804
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   805
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   806
\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
   807
\begin{ttbox}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   808
ctyp_of          : Sign.sg -> typ -> ctyp
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   809
rep_ctyp         : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   810
Sign.certify_typ : Sign.sg -> typ -> typ
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   811
\end{ttbox}
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   812
\begin{ttdescription}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   813
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   814
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures} certifies
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   815
  $T$ with respect to signature~$sign$.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   816
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   817
\item[\ttindexbold{rep_ctyp} $cT$] decomposes $cT$ as a record
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   818
  containing the type itself and its signature.
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   819
  
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   820
\item[\ttindexbold{Sign.certify_typ}] is a more primitive version of
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   821
  \texttt{ctyp_of}, returning the internal representation instead of
82a45bdd0e80 several minor updates;
wenzelm
parents: 4384
diff changeset
   822
  an abstract \texttt{ctyp}.
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   823
324
34bc15b546e6 penultimate Springer draft
lcp
parents: 286
diff changeset
   824
\end{ttdescription}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   825
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   826
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   827
\section{Oracles: calling trusted external reasoners}
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   828
\label{sec:oracles}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   829
\index{oracles|(}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   830
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   831
Oracles allow Isabelle to take advantage of external reasoners such as
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   832
arithmetic decision procedures, model checkers, fast tautology checkers or
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   833
computer algebra systems.  Invoked as an oracle, an external reasoner can
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   834
create arbitrary Isabelle theorems.  It is your responsibility to ensure that
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   835
the external reasoner is as trustworthy as your application requires.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   836
Isabelle's proof objects~(\S\ref{sec:proofObjects}) record how each theorem
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   837
depends upon oracle calls.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   838
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   839
\begin{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   840
invoke_oracle     : theory -> xstring -> Sign.sg * object -> thm
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   841
Theory.add_oracle : bstring * (Sign.sg * object -> term) -> theory -> theory
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   842
\end{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   843
\begin{ttdescription}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   844
\item[\ttindexbold{invoke_oracle} $thy$ $name$ ($sign$, $data$)]
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   845
  invokes the oracle $name$ of theory $thy$ passing the information
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   846
  contained in the exception value $data$ and creating a theorem
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   847
  having signature $sign$.  Note that type \ttindex{object} is just an
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   848
  abbreviation for \texttt{exn}.  Errors arise if $thy$ does not have
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   849
  an oracle called $name$, if the oracle rejects its arguments or if
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   850
  its result is ill-typed.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   851
  
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   852
\item[\ttindexbold{Theory.add_oracle} $name$ $fun$ $thy$] extends
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   853
  $thy$ by oracle $fun$ called $name$.  It is seldom called
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   854
  explicitly, as there is concrete syntax for oracles in theory files.
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   855
\end{ttdescription}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   856
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   857
A curious feature of {\ML} exceptions is that they are ordinary constructors.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   858
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
   859
my {\em {ML} for the Working Programmer}~\cite{paulson-ml2}, especially
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   860
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
   861
take any information whatever.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   862
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   863
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
   864
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
   865
expects the {\ML} function to take two arguments: a signature and an
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   866
exception object.
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   867
\begin{itemize}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   868
\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
   869
  declaring the oracle.  The oracle will use it to distinguish constants from
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   870
  variables, etc., and it will be attached to the generated theorems.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   871
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   872
\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
   873
  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
   874
  the external reasoner, including any additional information that might be
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   875
  required.  The oracle may raise the exception to indicate that it cannot
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   876
  solve the specified problem.
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   877
\end{itemize}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   878
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   879
A trivial example is provided in theory {\tt FOL/ex/IffOracle}.  This
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   880
oracle generates tautologies of the form $P\bimp\cdots\bimp P$, with
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   881
an even number of $P$s.
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   882
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   883
The \texttt{ML} section of \texttt{IffOracle.thy} begins by declaring
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   884
a few auxiliary functions (suppressed below) for creating the
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   885
tautologies.  Then it declares a new exception constructor for the
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   886
information required by the oracle: here, just an integer. It finally
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   887
defines the oracle function itself.
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   888
\begin{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   889
exception IffOracleExn of int;\medskip
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   890
fun mk_iff_oracle (sign, IffOracleExn n) =
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   891
  if n > 0 andalso n mod 2 = 0
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   892
  then Trueprop $ mk_iff n
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   893
  else raise IffOracleExn n;
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   894
\end{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   895
Observe the function's two arguments, the signature {\tt sign} and the
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   896
exception given as a pattern.  The function checks its argument for
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   897
validity.  If $n$ is positive and even then it creates a tautology
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   898
containing $n$ occurrences of~$P$.  Otherwise it signals error by
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   899
raising its own exception (just by happy coincidence).  Errors may be
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   900
signalled by other means, such as returning the theorem {\tt True}.
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   901
Please ensure that the oracle's result is correctly typed; Isabelle
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   902
will reject ill-typed theorems by raising a cryptic exception at top
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   903
level.
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   904
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   905
The \texttt{oracle} section of {\tt IffOracle.thy} installs above
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   906
\texttt{ML} function as follows:
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   907
\begin{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   908
IffOracle = FOL +\medskip
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   909
oracle
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   910
  iff = mk_iff_oracle\medskip
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   911
end
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   912
\end{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   913
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   914
Now in \texttt{IffOracle.ML} we first define a wrapper for invoking
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   915
the oracle:
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   916
\begin{ttbox}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   917
fun iff_oracle n =
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   918
  invoke_oracle IffOracle.thy "iff" (sign_of IffOracle.thy, IffOracleExn n);
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   919
\end{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   920
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   921
Here are some example applications of the \texttt{iff} oracle.  An
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   922
argument of 10 is allowed, but one of 5 is forbidden:
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   923
\begin{ttbox}
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   924
iff_oracle 10;
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   925
{\out  "P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P <-> P" : thm}
4317
7264fa2ff2ec several minor updates;
wenzelm
parents: 3485
diff changeset
   926
iff_oracle 5;
1846
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   927
{\out Exception- IffOracleExn 5 raised}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   928
\end{ttbox}
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   929
763f08fb194f Documentation of oracles and their syntax
paulson
parents: 1650
diff changeset
   930
\index{oracles|)}
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   931
\index{theories|)}