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