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