doc-src/IsarImplementation/Thy/document/logic.tex
author wenzelm
Sat May 10 14:13:20 2008 +0200 (2008-05-10)
changeset 26873 691f35f855cd
parent 26854 9b4aec46ad78
child 28086 db584d1d2af4
permissions -rw-r--r--
updated generated file;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{logic}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 \isanewline
     8 \isanewline
     9 %
    10 \endisadelimtheory
    11 %
    12 \isatagtheory
    13 \isacommand{theory}\isamarkupfalse%
    14 \ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
    15 \endisatagtheory
    16 {\isafoldtheory}%
    17 %
    18 \isadelimtheory
    19 %
    20 \endisadelimtheory
    21 %
    22 \isamarkupchapter{Primitive logic \label{ch:logic}%
    23 }
    24 \isamarkuptrue%
    25 %
    26 \begin{isamarkuptext}%
    27 The logical foundations of Isabelle/Isar are that of the Pure logic,
    28   which has been introduced as a natural-deduction framework in
    29   \cite{paulson700}.  This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract setting of Pure Type Systems (PTS)
    30   \cite{Barendregt-Geuvers:2001}, although there are some key
    31   differences in the specific treatment of simple types in
    32   Isabelle/Pure.
    33 
    34   Following type-theoretic parlance, the Pure logic consists of three
    35   levels of \isa{{\isasymlambda}}-calculus with corresponding arrows, \isa{{\isasymRightarrow}} for syntactic function space (terms depending on terms), \isa{{\isasymAnd}} for universal quantification (proofs depending on terms), and
    36   \isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs).
    37 
    38   Derivations are relative to a logical theory, which declares type
    39   constructors, constants, and axioms.  Theory declarations support
    40   schematic polymorphism, which is strictly speaking outside the
    41   logic.\footnote{This is the deeper logical reason, why the theory
    42   context \isa{{\isasymTheta}} is separate from the proof context \isa{{\isasymGamma}}
    43   of the core calculus.}%
    44 \end{isamarkuptext}%
    45 \isamarkuptrue%
    46 %
    47 \isamarkupsection{Types \label{sec:types}%
    48 }
    49 \isamarkuptrue%
    50 %
    51 \begin{isamarkuptext}%
    52 The language of types is an uninterpreted order-sorted first-order
    53   algebra; types are qualified by ordered type classes.
    54 
    55   \medskip A \emph{type class} is an abstract syntactic entity
    56   declared in the theory context.  The \emph{subclass relation} \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}} is specified by stating an acyclic
    57   generating relation; the transitive closure is maintained
    58   internally.  The resulting relation is an ordering: reflexive,
    59   transitive, and antisymmetric.
    60 
    61   A \emph{sort} is a list of type classes written as \isa{s\ {\isacharequal}\ {\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic
    62   intersection.  Notationally, the curly braces are omitted for
    63   singleton intersections, i.e.\ any class \isa{c} may be read as
    64   a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}.  The ordering on type classes is extended to
    65   sorts according to the meaning of intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff
    66   \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}.  The empty intersection
    67   \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the universal sort, which is the largest
    68   element wrt.\ the sort order.  The intersections of all (finitely
    69   many) classes declared in the current theory are the minimal
    70   elements wrt.\ the sort order.
    71 
    72   \medskip A \emph{fixed type variable} is a pair of a basic name
    73   (starting with a \isa{{\isacharprime}} character) and a sort constraint, e.g.\
    74   \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}.
    75   A \emph{schematic type variable} is a pair of an indexname and a
    76   sort constraint, e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually
    77   printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.
    78 
    79   Note that \emph{all} syntactic components contribute to the identity
    80   of type variables, including the sort constraint.  The core logic
    81   handles type variables with the same name but different sorts as
    82   different, although some outer layers of the system make it hard to
    83   produce anything like this.
    84 
    85   A \emph{type constructor} \isa{{\isasymkappa}} is a \isa{k}-ary operator
    86   on types declared in the theory.  Type constructor application is
    87   written postfix as \isa{{\isacharparenleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub k{\isacharparenright}{\isasymkappa}}.  For
    88   \isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop}
    89   instead of \isa{{\isacharparenleft}{\isacharparenright}prop}.  For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses
    90   are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}.
    91   Further notation is provided for specific constructors, notably the
    92   right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}.
    93   
    94   A \emph{type} is defined inductively over type variables and type
    95   constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}{\isasymkappa}}.
    96 
    97   A \emph{type abbreviation} is a syntactic definition \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} of an arbitrary type expression \isa{{\isasymtau}} over
    98   variables \isa{\isactrlvec {\isasymalpha}}.  Type abbreviations appear as type
    99   constructors in the syntax, but are expanded before entering the
   100   logical core.
   101 
   102   A \emph{type arity} declares the image behavior of a type
   103   constructor wrt.\ the algebra of sorts: \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}{\isasymkappa}} is
   104   of sort \isa{s} if every argument type \isa{{\isasymtau}\isactrlisub i} is
   105   of sort \isa{s\isactrlisub i}.  Arity declarations are implicitly
   106   completed, i.e.\ \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c} entails \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}} for any \isa{c{\isacharprime}\ {\isasymsupseteq}\ c}.
   107 
   108   \medskip The sort algebra is always maintained as \emph{coregular},
   109   which means that type arities are consistent with the subclass
   110   relation: for any type constructor \isa{{\isasymkappa}}, and classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, and arities \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} and \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} holds \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} component-wise.
   111 
   112   The key property of a coregular order-sorted algebra is that sort
   113   constraints can be solved in a most general fashion: for each type
   114   constructor \isa{{\isasymkappa}} and sort \isa{s} there is a most general
   115   vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such
   116   that a type scheme \isa{{\isacharparenleft}{\isasymalpha}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}{\isasymkappa}} is of sort \isa{s}.
   117   Consequently, type unification has most general solutions (modulo
   118   equivalence of sorts), so type-inference produces primary types as
   119   expected \cite{nipkow-prehofer}.%
   120 \end{isamarkuptext}%
   121 \isamarkuptrue%
   122 %
   123 \isadelimmlref
   124 %
   125 \endisadelimmlref
   126 %
   127 \isatagmlref
   128 %
   129 \begin{isamarkuptext}%
   130 \begin{mldecls}
   131   \indexmltype{class}\verb|type class| \\
   132   \indexmltype{sort}\verb|type sort| \\
   133   \indexmltype{arity}\verb|type arity| \\
   134   \indexmltype{typ}\verb|type typ| \\
   135   \indexml{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
   136   \indexml{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
   137   \end{mldecls}
   138   \begin{mldecls}
   139   \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
   140   \indexml{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
   141   \indexml{Sign.add\_types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
   142   \indexml{Sign.add\_tyabbrs\_i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
   143 \verb|  (string * string list * typ * mixfix) list -> theory -> theory| \\
   144   \indexml{Sign.primitive\_class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
   145   \indexml{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
   146   \indexml{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
   147   \end{mldecls}
   148 
   149   \begin{description}
   150 
   151   \item \verb|class| represents type classes; this is an alias for
   152   \verb|string|.
   153 
   154   \item \verb|sort| represents sorts; this is an alias for
   155   \verb|class list|.
   156 
   157   \item \verb|arity| represents type arities; this is an alias for
   158   triples of the form \isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} described above.
   159 
   160   \item \verb|typ| represents types; this is a datatype with
   161   constructors \verb|TFree|, \verb|TVar|, \verb|Type|.
   162 
   163   \item \verb|map_atyps|~\isa{f\ {\isasymtau}} applies the mapping \isa{f}
   164   to all atomic types (\verb|TFree|, \verb|TVar|) occurring in \isa{{\isasymtau}}.
   165 
   166   \item \verb|fold_atyps|~\isa{f\ {\isasymtau}} iterates the operation \isa{f} over all occurrences of atomic types (\verb|TFree|, \verb|TVar|)
   167   in \isa{{\isasymtau}}; the type structure is traversed from left to right.
   168 
   169   \item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}}
   170   tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}.
   171 
   172   \item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether type
   173   \isa{{\isasymtau}} is of sort \isa{s}.
   174 
   175   \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a new
   176   type constructors \isa{{\isasymkappa}} with \isa{k} arguments and
   177   optional mixfix syntax.
   178 
   179   \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
   180   defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} with
   181   optional mixfix syntax.
   182 
   183   \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares a new class \isa{c}, together with class
   184   relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}.
   185 
   186   \item \verb|Sign.primitive_classrel|~\isa{{\isacharparenleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ c\isactrlisub {\isadigit{2}}{\isacharparenright}} declares the class relation \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}.
   187 
   188   \item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares
   189   the arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}.
   190 
   191   \end{description}%
   192 \end{isamarkuptext}%
   193 \isamarkuptrue%
   194 %
   195 \endisatagmlref
   196 {\isafoldmlref}%
   197 %
   198 \isadelimmlref
   199 %
   200 \endisadelimmlref
   201 %
   202 \isamarkupsection{Terms \label{sec:terms}%
   203 }
   204 \isamarkuptrue%
   205 %
   206 \begin{isamarkuptext}%
   207 \glossary{Term}{FIXME}
   208 
   209   The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus
   210   with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
   211   or \cite{paulson-ml2}), with the types being determined determined
   212   by the corresponding binders.  In contrast, free variables and
   213   constants are have an explicit name and type in each occurrence.
   214 
   215   \medskip A \emph{bound variable} is a natural number \isa{b},
   216   which accounts for the number of intermediate binders between the
   217   variable occurrence in the body and its binding position.  For
   218   example, the de-Bruijn term \isa{{\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}} would
   219   correspond to \isa{{\isasymlambda}x\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}y\isactrlbsub nat\isactrlesub {\isachardot}\ x\ {\isacharplus}\ y} in a named
   220   representation.  Note that a bound variable may be represented by
   221   different de-Bruijn indices at different occurrences, depending on
   222   the nesting of abstractions.
   223 
   224   A \emph{loose variable} is a bound variable that is outside the
   225   scope of local binders.  The types (and names) for loose variables
   226   can be managed as a separate context, that is maintained as a stack
   227   of hypothetical binders.  The core logic operates on closed terms,
   228   without any loose variables.
   229 
   230   A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
   231   \isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}}.  A
   232   \emph{schematic variable} is a pair of an indexname and a type,
   233   e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}.
   234 
   235   \medskip A \emph{constant} is a pair of a basic name and a type,
   236   e.g.\ \isa{{\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{c\isactrlisub {\isasymtau}}.  Constants are declared in the context as polymorphic
   237   families \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that all substitution instances
   238   \isa{c\isactrlisub {\isasymtau}} for \isa{{\isasymtau}\ {\isacharequal}\ {\isasymsigma}{\isasymvartheta}} are valid.
   239 
   240   The vector of \emph{type arguments} of constant \isa{c\isactrlisub {\isasymtau}}
   241   wrt.\ the declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is defined as the codomain of
   242   the matcher \isa{{\isasymvartheta}\ {\isacharequal}\ {\isacharbraceleft}{\isacharquery}{\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymmapsto}\ {\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isacharquery}{\isasymalpha}\isactrlisub n\ {\isasymmapsto}\ {\isasymtau}\isactrlisub n{\isacharbraceright}} presented in canonical order \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}}.  Within a given theory context,
   243   there is a one-to-one correspondence between any constant \isa{c\isactrlisub {\isasymtau}} and the application \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} of its type arguments.  For example, with \isa{plus\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}}, the instance \isa{plus\isactrlbsub nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\isactrlesub } corresponds to \isa{plus{\isacharparenleft}nat{\isacharparenright}}.
   244 
   245   Constant declarations \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} may contain sort constraints
   246   for type variables in \isa{{\isasymsigma}}.  These are observed by
   247   type-inference as expected, but \emph{ignored} by the core logic.
   248   This means the primitive logic is able to reason with instances of
   249   polymorphic constants that the user-level type-checker would reject
   250   due to violation of type class restrictions.
   251 
   252   \medskip An \emph{atomic} term is either a variable or constant.  A
   253   \emph{term} is defined inductively over atomic terms, with
   254   abstraction and application as follows: \isa{t\ {\isacharequal}\ b\ {\isacharbar}\ x\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isacharquery}x\isactrlisub {\isasymtau}\ {\isacharbar}\ c\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ t\ {\isacharbar}\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}}.
   255   Parsing and printing takes care of converting between an external
   256   representation with named bound variables.  Subsequently, we shall
   257   use the latter notation instead of internal de-Bruijn
   258   representation.
   259 
   260   The inductive relation \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} assigns a (unique) type to a
   261   term according to the structure of atomic terms, abstractions, and
   262   applicatins:
   263   \[
   264   \infer{\isa{a\isactrlisub {\isasymtau}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}{}
   265   \qquad
   266   \infer{\isa{{\isacharparenleft}{\isasymlambda}x\isactrlsub {\isasymtau}{\isachardot}\ t{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}
   267   \qquad
   268   \infer{\isa{t\ u\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}} & \isa{u\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}
   269   \]
   270   A \emph{well-typed term} is a term that can be typed according to these rules.
   271 
   272   Typing information can be omitted: type-inference is able to
   273   reconstruct the most general type of a raw term, while assigning
   274   most general types to all of its variables and constants.
   275   Type-inference depends on a context of type constraints for fixed
   276   variables, and declarations for polymorphic constants.
   277 
   278   The identity of atomic terms consists both of the name and the type
   279   component.  This means that different variables \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{1}}\isactrlesub } and \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{2}}\isactrlesub } may become the same after type
   280   instantiation.  Some outer layers of the system make it hard to
   281   produce variables of the same name, but different types.  In
   282   contrast, mixed instances of polymorphic constants occur frequently.
   283 
   284   \medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}
   285   is the set of type variables occurring in \isa{t}, but not in
   286   \isa{{\isasymsigma}}.  This means that the term implicitly depends on type
   287   arguments that are not accounted in the result type, i.e.\ there are
   288   different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and \isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type.  This slightly
   289   pathological situation notoriously demands additional care.
   290 
   291   \medskip A \emph{term abbreviation} is a syntactic definition \isa{c\isactrlisub {\isasymsigma}\ {\isasymequiv}\ t} of a closed term \isa{t} of type \isa{{\isasymsigma}},
   292   without any hidden polymorphism.  A term abbreviation looks like a
   293   constant in the syntax, but is expanded before entering the logical
   294   core.  Abbreviations are usually reverted when printing terms, using
   295   \isa{t\ {\isasymrightarrow}\ c\isactrlisub {\isasymsigma}} as rules for higher-order rewriting.
   296 
   297   \medskip Canonical operations on \isa{{\isasymlambda}}-terms include \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion: \isa{{\isasymalpha}}-conversion refers to capture-free
   298   renaming of bound variables; \isa{{\isasymbeta}}-conversion contracts an
   299   abstraction applied to an argument term, substituting the argument
   300   in the body: \isa{{\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharparenright}a} becomes \isa{b{\isacharbrackleft}a{\isacharslash}x{\isacharbrackright}}; \isa{{\isasymeta}}-conversion contracts vacuous application-abstraction: \isa{{\isasymlambda}x{\isachardot}\ f\ x} becomes \isa{f}, provided that the bound variable
   301   does not occur in \isa{f}.
   302 
   303   Terms are normally treated modulo \isa{{\isasymalpha}}-conversion, which is
   304   implicit in the de-Bruijn representation.  Names for bound variables
   305   in abstractions are maintained separately as (meaningless) comments,
   306   mostly for parsing and printing.  Full \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion is
   307   commonplace in various standard operations (\secref{sec:rules}) that
   308   are based on higher-order unification and matching.%
   309 \end{isamarkuptext}%
   310 \isamarkuptrue%
   311 %
   312 \isadelimmlref
   313 %
   314 \endisadelimmlref
   315 %
   316 \isatagmlref
   317 %
   318 \begin{isamarkuptext}%
   319 \begin{mldecls}
   320   \indexmltype{term}\verb|type term| \\
   321   \indexml{op aconv}\verb|op aconv: term * term -> bool| \\
   322   \indexml{map\_types}\verb|map_types: (typ -> typ) -> term -> term| \\
   323   \indexml{fold\_types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
   324   \indexml{map\_aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
   325   \indexml{fold\_aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
   326   \end{mldecls}
   327   \begin{mldecls}
   328   \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
   329   \indexml{lambda}\verb|lambda: term -> term -> term| \\
   330   \indexml{betapply}\verb|betapply: term * term -> term| \\
   331   \indexml{Sign.declare\_const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%
   332 \verb|  theory -> term * theory| \\
   333   \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%
   334 \verb|  theory -> (term * term) * theory| \\
   335   \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   336   \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
   337   \end{mldecls}
   338 
   339   \begin{description}
   340 
   341   \item \verb|term| represents de-Bruijn terms, with comments in
   342   abstractions, and explicitly named free variables and constants;
   343   this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|op $|.
   344 
   345   \item \isa{t}~\verb|aconv|~\isa{u} checks \isa{{\isasymalpha}}-equivalence of two terms.  This is the basic equality relation
   346   on type \verb|term|; raw datatype equality should only be used
   347   for operations related to parsing or printing!
   348 
   349   \item \verb|map_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
   350 
   351   \item \verb|fold_types|~\isa{f\ t} iterates the operation \isa{f} over all occurrences of types in \isa{t}; the term
   352   structure is traversed from left to right.
   353 
   354   \item \verb|map_aterms|~\isa{f\ t} applies the mapping \isa{f}
   355   to all atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) occurring in \isa{t}.
   356 
   357   \item \verb|fold_aterms|~\isa{f\ t} iterates the operation \isa{f} over all occurrences of atomic terms (\verb|Bound|, \verb|Free|,
   358   \verb|Var|, \verb|Const|) in \isa{t}; the term structure is
   359   traversed from left to right.
   360 
   361   \item \verb|fastype_of|~\isa{t} determines the type of a
   362   well-typed term.  This operation is relatively slow, despite the
   363   omission of any sanity checks.
   364 
   365   \item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the atomic term \isa{a} in the
   366   body \isa{b} are replaced by bound variables.
   367 
   368   \item \verb|betapply|~\isa{{\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} is an
   369   abstraction.
   370 
   371   \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}}
   372   declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix
   373   syntax.
   374 
   375   \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
   376   introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
   377 
   378   \item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}
   379   convert between two representations of polymorphic constants: full
   380   type instance vs.\ compact type arguments form.
   381 
   382   \end{description}%
   383 \end{isamarkuptext}%
   384 \isamarkuptrue%
   385 %
   386 \endisatagmlref
   387 {\isafoldmlref}%
   388 %
   389 \isadelimmlref
   390 %
   391 \endisadelimmlref
   392 %
   393 \isamarkupsection{Theorems \label{sec:thms}%
   394 }
   395 \isamarkuptrue%
   396 %
   397 \begin{isamarkuptext}%
   398 \glossary{Proposition}{FIXME A \seeglossary{term} of
   399   \seeglossary{type} \isa{prop}.  Internally, there is nothing
   400   special about propositions apart from their type, but the concrete
   401   syntax enforces a clear distinction.  Propositions are structured
   402   via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything else is considered atomic.  The canonical
   403   form for propositions is that of a \seeglossary{Hereditary Harrop
   404   Formula}. FIXME}
   405 
   406   \glossary{Theorem}{A proven proposition within a certain theory and
   407   proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
   408   rarely spelled out explicitly.  Theorems are usually normalized
   409   according to the \seeglossary{HHF} format. FIXME}
   410 
   411   \glossary{Fact}{Sometimes used interchangeably for
   412   \seeglossary{theorem}.  Strictly speaking, a list of theorems,
   413   essentially an extra-logical conjunction.  Facts emerge either as
   414   local assumptions, or as results of local goal statements --- both
   415   may be simultaneous, hence the list representation. FIXME}
   416 
   417   \glossary{Schematic variable}{FIXME}
   418 
   419   \glossary{Fixed variable}{A variable that is bound within a certain
   420   proof context; an arbitrary-but-fixed entity within a portion of
   421   proof text. FIXME}
   422 
   423   \glossary{Free variable}{Synonymous for \seeglossary{fixed
   424   variable}. FIXME}
   425 
   426   \glossary{Bound variable}{FIXME}
   427 
   428   \glossary{Variable}{See \seeglossary{schematic variable},
   429   \seeglossary{fixed variable}, \seeglossary{bound variable}, or
   430   \seeglossary{type variable}.  The distinguishing feature of
   431   different variables is their binding scope. FIXME}
   432 
   433   A \emph{proposition} is a well-typed term of type \isa{prop}, a
   434   \emph{theorem} is a proven proposition (depending on a context of
   435   hypotheses and the background theory).  Primitive inferences include
   436   plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework.  There is also a builtin
   437   notion of equality/equivalence \isa{{\isasymequiv}}.%
   438 \end{isamarkuptext}%
   439 \isamarkuptrue%
   440 %
   441 \isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}%
   442 }
   443 \isamarkuptrue%
   444 %
   445 \begin{isamarkuptext}%
   446 The theory \isa{Pure} contains constant declarations for the
   447   primitive connectives \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and \isa{{\isasymequiv}} of
   448   the logical framework, see \figref{fig:pure-connectives}.  The
   449   derivability judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is
   450   defined inductively by the primitive inferences given in
   451   \figref{fig:prim-rules}, with the global restriction that the
   452   hypotheses must \emph{not} contain any schematic variables.  The
   453   builtin equality is conceptually axiomatized as shown in
   454   \figref{fig:pure-equality}, although the implementation works
   455   directly with derived inferences.
   456 
   457   \begin{figure}[htb]
   458   \begin{center}
   459   \begin{tabular}{ll}
   460   \isa{all\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymRightarrow}\ prop{\isacharparenright}\ {\isasymRightarrow}\ prop} & universal quantification (binder \isa{{\isasymAnd}}) \\
   461   \isa{{\isasymLongrightarrow}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & implication (right associative infix) \\
   462   \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\
   463   \end{tabular}
   464   \caption{Primitive connectives of Pure}\label{fig:pure-connectives}
   465   \end{center}
   466   \end{figure}
   467 
   468   \begin{figure}[htb]
   469   \begin{center}
   470   \[
   471   \infer[\isa{{\isacharparenleft}axiom{\isacharparenright}}]{\isa{{\isasymturnstile}\ A}}{\isa{A\ {\isasymin}\ {\isasymTheta}}}
   472   \qquad
   473   \infer[\isa{{\isacharparenleft}assume{\isacharparenright}}]{\isa{A\ {\isasymturnstile}\ A}}{}
   474   \]
   475   \[
   476   \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}
   477   \qquad
   478   \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}
   479   \]
   480   \[
   481   \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
   482   \qquad
   483   \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymunion}\ {\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ B}}{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B} & \isa{{\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ A}}
   484   \]
   485   \caption{Primitive inferences of Pure}\label{fig:prim-rules}
   486   \end{center}
   487   \end{figure}
   488 
   489   \begin{figure}[htb]
   490   \begin{center}
   491   \begin{tabular}{ll}
   492   \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ a\ {\isasymequiv}\ b{\isacharbrackleft}a{\isacharbrackright}} & \isa{{\isasymbeta}}-conversion \\
   493   \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity \\
   494   \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution \\
   495   \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\
   496   \isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & logical equivalence \\
   497   \end{tabular}
   498   \caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
   499   \end{center}
   500   \end{figure}
   501 
   502   The introduction and elimination rules for \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} are analogous to formation of dependently typed \isa{{\isasymlambda}}-terms representing the underlying proof objects.  Proof terms
   503   are irrelevant in the Pure logic, though; they cannot occur within
   504   propositions.  The system provides a runtime option to record
   505   explicit proof terms for primitive inferences.  Thus all three
   506   levels of \isa{{\isasymlambda}}-calculus become explicit: \isa{{\isasymRightarrow}} for
   507   terms, and \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} for proofs (cf.\
   508   \cite{Berghofer-Nipkow:2000:TPHOL}).
   509 
   510   Observe that locally fixed parameters (as in \isa{{\isasymAnd}{\isacharunderscore}intro}) need
   511   not be recorded in the hypotheses, because the simple syntactic
   512   types of Pure are always inhabitable.  ``Assumptions'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} for type-membership are only present as long as some \isa{x\isactrlisub {\isasymtau}} occurs in the statement body.\footnote{This is the key
   513   difference to ``\isa{{\isasymlambda}HOL}'' in the PTS framework
   514   \cite{Barendregt-Geuvers:2001}, where hypotheses \isa{x\ {\isacharcolon}\ A} are
   515   treated uniformly for propositions and types.}
   516 
   517   \medskip The axiomatization of a theory is implicitly closed by
   518   forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} holds for any substitution instance of an axiom
   519   \isa{{\isasymturnstile}\ A}.  By pushing substitutions through derivations
   520   inductively, we also get admissible \isa{generalize} and \isa{instance} rules as shown in \figref{fig:subst-rules}.
   521 
   522   \begin{figure}[htb]
   523   \begin{center}
   524   \[
   525   \infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} & \isa{{\isasymalpha}\ {\isasymnotin}\ {\isasymGamma}}}
   526   \quad
   527   \infer[\quad\isa{{\isacharparenleft}generalize{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}
   528   \]
   529   \[
   530   \infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymtau}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}
   531   \quad
   532   \infer[\quad\isa{{\isacharparenleft}instantiate{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}t{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}
   533   \]
   534   \caption{Admissible substitution rules}\label{fig:subst-rules}
   535   \end{center}
   536   \end{figure}
   537 
   538   Note that \isa{instantiate} does not require an explicit
   539   side-condition, because \isa{{\isasymGamma}} may never contain schematic
   540   variables.
   541 
   542   In principle, variables could be substituted in hypotheses as well,
   543   but this would disrupt the monotonicity of reasoning: deriving
   544   \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymturnstile}\ B{\isasymvartheta}} from \isa{{\isasymGamma}\ {\isasymturnstile}\ B} is
   545   correct, but \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymsupseteq}\ {\isasymGamma}} does not necessarily hold:
   546   the result belongs to a different proof context.
   547 
   548   \medskip An \emph{oracle} is a function that produces axioms on the
   549   fly.  Logically, this is an instance of the \isa{axiom} rule
   550   (\figref{fig:prim-rules}), but there is an operational difference.
   551   The system always records oracle invocations within derivations of
   552   theorems.  Tracing plain axioms (and named theorems) is optional.
   553 
   554   Axiomatizations should be limited to the bare minimum, typically as
   555   part of the initial logical basis of an object-logic formalization.
   556   Later on, theories are usually developed in a strictly definitional
   557   fashion, by stating only certain equalities over new constants.
   558 
   559   A \emph{simple definition} consists of a constant declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} together with an axiom \isa{{\isasymturnstile}\ c\ {\isasymequiv}\ t}, where \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is a closed term without any hidden polymorphism.  The RHS
   560   may depend on further defined constants, but not \isa{c} itself.
   561   Definitions of functions may be presented as \isa{c\ \isactrlvec x\ {\isasymequiv}\ t} instead of the puristic \isa{c\ {\isasymequiv}\ {\isasymlambda}\isactrlvec x{\isachardot}\ t}.
   562 
   563   An \emph{overloaded definition} consists of a collection of axioms
   564   for the same constant, with zero or one equations \isa{c{\isacharparenleft}{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}{\isacharparenright}\ {\isasymequiv}\ t} for each type constructor \isa{{\isasymkappa}} (for
   565   distinct variables \isa{\isactrlvec {\isasymalpha}}).  The RHS may mention
   566   previously defined constants as above, or arbitrary constants \isa{d{\isacharparenleft}{\isasymalpha}\isactrlisub i{\isacharparenright}} for some \isa{{\isasymalpha}\isactrlisub i} projected from \isa{\isactrlvec {\isasymalpha}}.  Thus overloaded definitions essentially work by
   567   primitive recursion over the syntactic structure of a single type
   568   argument.%
   569 \end{isamarkuptext}%
   570 \isamarkuptrue%
   571 %
   572 \isadelimmlref
   573 %
   574 \endisadelimmlref
   575 %
   576 \isatagmlref
   577 %
   578 \begin{isamarkuptext}%
   579 \begin{mldecls}
   580   \indexmltype{ctyp}\verb|type ctyp| \\
   581   \indexmltype{cterm}\verb|type cterm| \\
   582   \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
   583   \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
   584   \end{mldecls}
   585   \begin{mldecls}
   586   \indexmltype{thm}\verb|type thm| \\
   587   \indexml{proofs}\verb|proofs: int ref| \\
   588   \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
   589   \indexml{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
   590   \indexml{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
   591   \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
   592   \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
   593   \indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
   594   \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
   595   \indexml{Thm.get\_axiom\_i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
   596   \indexml{Thm.invoke\_oracle\_i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
   597   \end{mldecls}
   598   \begin{mldecls}
   599   \indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
   600   \indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
   601   \indexml{Theory.add\_oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
   602   \indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
   603   \end{mldecls}
   604 
   605   \begin{description}
   606 
   607   \item \verb|ctyp| and \verb|cterm| represent certified types
   608   and terms, respectively.  These are abstract datatypes that
   609   guarantee that its values have passed the full well-formedness (and
   610   well-typedness) checks, relative to the declarations of type
   611   constructors, constants etc. in the theory.
   612 
   613   \item \verb|ctyp_of|~\isa{thy\ {\isasymtau}} and \verb|cterm_of|~\isa{thy\ t} explicitly checks types and terms, respectively.  This also
   614   involves some basic normalizations, such expansion of type and term
   615   abbreviations from the theory context.
   616 
   617   Re-certification is relatively slow and should be avoided in tight
   618   reasoning loops.  There are separate operations to decompose
   619   certified entities (including actual theorems).
   620 
   621   \item \verb|thm| represents proven propositions.  This is an
   622   abstract datatype that guarantees that its values have been
   623   constructed by basic principles of the \verb|Thm| module.
   624   Every \verb|thm| value contains a sliding back-reference to the
   625   enclosing theory, cf.\ \secref{sec:context-theory}.
   626 
   627   \item \verb|proofs| determines the detail of proof recording within
   628   \verb|thm| values: \verb|0| records only oracles, \verb|1| records
   629   oracles, axioms and named theorems, \verb|2| records full proof
   630   terms.
   631 
   632   \item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim|
   633   correspond to the primitive inferences of \figref{fig:prim-rules}.
   634 
   635   \item \verb|Thm.generalize|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharcomma}\ \isactrlvec x{\isacharparenright}}
   636   corresponds to the \isa{generalize} rules of
   637   \figref{fig:subst-rules}.  Here collections of type and term
   638   variables are generalized simultaneously, specified by the given
   639   basic names.
   640 
   641   \item \verb|Thm.instantiate|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}\isactrlisub s{\isacharcomma}\ \isactrlvec x\isactrlisub {\isasymtau}{\isacharparenright}} corresponds to the \isa{instantiate} rules
   642   of \figref{fig:subst-rules}.  Type variables are substituted before
   643   term variables.  Note that the types in \isa{\isactrlvec x\isactrlisub {\isasymtau}}
   644   refer to the instantiated versions.
   645 
   646   \item \verb|Thm.get_axiom_i|~\isa{thy\ name} retrieves a named
   647   axiom, cf.\ \isa{axiom} in \figref{fig:prim-rules}.
   648 
   649   \item \verb|Thm.invoke_oracle_i|~\isa{thy\ name\ arg} invokes a
   650   named oracle function, cf.\ \isa{axiom} in
   651   \figref{fig:prim-rules}.
   652 
   653   \item \verb|Theory.add_axioms_i|~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares
   654   arbitrary propositions as axioms.
   655 
   656   \item \verb|Theory.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an oracle
   657   function for generating arbitrary axioms on the fly.
   658 
   659   \item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification
   660   for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing
   661   specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.
   662 
   663   \item \verb|Theory.add_defs_i|~\isa{unchecked\ overloaded\ {\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} states a definitional axiom for an existing
   664   constant \isa{c}.  Dependencies are recorded (cf.\ \verb|Theory.add_deps|), unless the \isa{unchecked} option is set.
   665 
   666   \end{description}%
   667 \end{isamarkuptext}%
   668 \isamarkuptrue%
   669 %
   670 \endisatagmlref
   671 {\isafoldmlref}%
   672 %
   673 \isadelimmlref
   674 %
   675 \endisadelimmlref
   676 %
   677 \isamarkupsubsection{Auxiliary definitions%
   678 }
   679 \isamarkuptrue%
   680 %
   681 \begin{isamarkuptext}%
   682 Theory \isa{Pure} provides a few auxiliary definitions, see
   683   \figref{fig:pure-aux}.  These special constants are normally not
   684   exposed to the user, but appear in internal encodings.
   685 
   686   \begin{figure}[htb]
   687   \begin{center}
   688   \begin{tabular}{ll}
   689   \isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}}) \\
   690   \isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\[1ex]
   691   \isa{prop\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop} & (prefix \isa{{\isacharhash}}, suppressed) \\
   692   \isa{{\isacharhash}A\ {\isasymequiv}\ A} \\[1ex]
   693   \isa{term\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & (prefix \isa{TERM}) \\
   694   \isa{term\ x\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}A{\isachardot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}} \\[1ex]
   695   \isa{TYPE\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself} & (prefix \isa{TYPE}) \\
   696   \isa{{\isacharparenleft}unspecified{\isacharparenright}} \\
   697   \end{tabular}
   698   \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   699   \end{center}
   700   \end{figure}
   701 
   702   Derived conjunction rules include introduction \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B}, and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.
   703   Conjunction allows to treat simultaneous assumptions and conclusions
   704   uniformly.  For example, multiple claims are intermediately
   705   represented as explicit conjunction, but this is refined into
   706   separate sub-goals before the user continues the proof; the final
   707   result is projected into a list of theorems (cf.\
   708   \secref{sec:tactical-goals}).
   709 
   710   The \isa{prop} marker (\isa{{\isacharhash}}) makes arbitrarily complex
   711   propositions appear as atomic, without changing the meaning: \isa{{\isasymGamma}\ {\isasymturnstile}\ A} and \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isacharhash}A} are interchangeable.  See
   712   \secref{sec:tactical-goals} for specific operations.
   713 
   714   The \isa{term} marker turns any well-typed term into a derivable
   715   proposition: \isa{{\isasymturnstile}\ TERM\ t} holds unconditionally.  Although
   716   this is logically vacuous, it allows to treat terms and proofs
   717   uniformly, similar to a type-theoretic framework.
   718 
   719   The \isa{TYPE} constructor is the canonical representative of
   720   the unspecified type \isa{{\isasymalpha}\ itself}; it essentially injects the
   721   language of types into that of terms.  There is specific notation
   722   \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }.
   723   Although being devoid of any particular meaning, the \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} accounts for the type \isa{{\isasymtau}} within the term
   724   language.  In particular, \isa{TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}} may be used as formal
   725   argument in primitive definitions, in order to circumvent hidden
   726   polymorphism (cf.\ \secref{sec:terms}).  For example, \isa{c\ TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}\ {\isasymequiv}\ A{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} defines \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself\ {\isasymRightarrow}\ prop} in terms of
   727   a proposition \isa{A} that depends on an additional type
   728   argument, which is essentially a predicate on types.%
   729 \end{isamarkuptext}%
   730 \isamarkuptrue%
   731 %
   732 \isadelimmlref
   733 %
   734 \endisadelimmlref
   735 %
   736 \isatagmlref
   737 %
   738 \begin{isamarkuptext}%
   739 \begin{mldecls}
   740   \indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
   741   \indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
   742   \indexml{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
   743   \indexml{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
   744   \indexml{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
   745   \indexml{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
   746   \end{mldecls}
   747 
   748   \begin{description}
   749 
   750   \item \verb|Conjunction.intr| derives \isa{A\ {\isacharampersand}\ B} from \isa{A} and \isa{B}.
   751 
   752   \item \verb|Conjunction.elim| derives \isa{A} and \isa{B}
   753   from \isa{A\ {\isacharampersand}\ B}.
   754 
   755   \item \verb|Drule.mk_term| derives \isa{TERM\ t}.
   756 
   757   \item \verb|Drule.dest_term| recovers term \isa{t} from \isa{TERM\ t}.
   758 
   759   \item \verb|Logic.mk_type|~\isa{{\isasymtau}} produces the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}}.
   760 
   761   \item \verb|Logic.dest_type|~\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} recovers the type
   762   \isa{{\isasymtau}}.
   763 
   764   \end{description}%
   765 \end{isamarkuptext}%
   766 \isamarkuptrue%
   767 %
   768 \endisatagmlref
   769 {\isafoldmlref}%
   770 %
   771 \isadelimmlref
   772 %
   773 \endisadelimmlref
   774 %
   775 \isamarkupsection{Rules \label{sec:rules}%
   776 }
   777 \isamarkuptrue%
   778 %
   779 \isadelimFIXME
   780 %
   781 \endisadelimFIXME
   782 %
   783 \isatagFIXME
   784 %
   785 \begin{isamarkuptext}%
   786 FIXME
   787 
   788   A \emph{rule} is any Pure theorem in HHF normal form; there is a
   789   separate calculus for rule composition, which is modeled after
   790   Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
   791   rules to be nested arbitrarily, similar to \cite{extensions91}.
   792 
   793   Normally, all theorems accessible to the user are proper rules.
   794   Low-level inferences are occasional required internally, but the
   795   result should be always presented in canonical form.  The higher
   796   interfaces of Isabelle/Isar will always produce proper rules.  It is
   797   important to maintain this invariant in add-on applications!
   798 
   799   There are two main principles of rule composition: \isa{resolution} (i.e.\ backchaining of rules) and \isa{by{\isacharminus}assumption} (i.e.\ closing a branch); both principles are
   800   combined in the variants of \isa{elim{\isacharminus}resolution} and \isa{dest{\isacharminus}resolution}.  Raw \isa{composition} is occasionally
   801   useful as well, also it is strictly speaking outside of the proper
   802   rule calculus.
   803 
   804   Rules are treated modulo general higher-order unification, which is
   805   unification modulo the equational theory of \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion
   806   on \isa{{\isasymlambda}}-terms.  Moreover, propositions are understood modulo
   807   the (derived) equivalence \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}.
   808 
   809   This means that any operations within the rule calculus may be
   810   subject to spontaneous \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-HHF conversions.  It is common
   811   practice not to contract or expand unnecessarily.  Some mechanisms
   812   prefer an one form, others the opposite, so there is a potential
   813   danger to produce some oscillation!
   814 
   815   Only few operations really work \emph{modulo} HHF conversion, but
   816   expect a normal form: quantifiers \isa{{\isasymAnd}} before implications
   817   \isa{{\isasymLongrightarrow}} at each level of nesting.
   818 
   819 \glossary{Hereditary Harrop Formula}{The set of propositions in HHF
   820 format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.
   821 Any proposition may be put into HHF form by normalizing with the rule
   822 \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}.  In Isabelle, the outermost
   823 quantifier prefix is represented via \seeglossary{schematic
   824 variables}, such that the top-level structure is merely that of a
   825 \seeglossary{Horn Clause}}.
   826 
   827 \glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
   828 
   829 
   830   \[
   831   \infer[\isa{{\isacharparenleft}assumption{\isacharparenright}}]{\isa{C{\isasymvartheta}}}
   832   {\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ A\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} & \isa{A{\isasymvartheta}\ {\isacharequal}\ H\isactrlsub i{\isasymvartheta}}~~\text{(for some~\isa{i})}}
   833   \]
   834 
   835 
   836   \[
   837   \infer[\isa{{\isacharparenleft}compose{\isacharparenright}}]{\isa{\isactrlvec A{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}
   838   {\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B} & \isa{B{\isacharprime}\ {\isasymLongrightarrow}\ C} & \isa{B{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}}}
   839   \]
   840 
   841 
   842   \[
   843   \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}lift{\isacharparenright}}]{\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}}}{\isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a}}
   844   \]
   845   \[
   846   \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}lift{\isacharparenright}}]{\isa{{\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ \isactrlvec A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ B{\isacharparenright}}}{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B}}
   847   \]
   848 
   849   The \isa{resolve} scheme is now acquired from \isa{{\isasymAnd}{\isacharunderscore}lift},
   850   \isa{{\isasymLongrightarrow}{\isacharunderscore}lift}, and \isa{compose}.
   851 
   852   \[
   853   \infer[\isa{{\isacharparenleft}resolution{\isacharparenright}}]
   854   {\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ \isactrlvec A\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}
   855   {\begin{tabular}{l}
   856     \isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a} \\
   857     \isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} \\
   858     \isa{{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}} \\
   859    \end{tabular}}
   860   \]
   861 
   862 
   863   FIXME \isa{elim{\isacharunderscore}resolution}, \isa{dest{\isacharunderscore}resolution}%
   864 \end{isamarkuptext}%
   865 \isamarkuptrue%
   866 %
   867 \endisatagFIXME
   868 {\isafoldFIXME}%
   869 %
   870 \isadelimFIXME
   871 %
   872 \endisadelimFIXME
   873 %
   874 \isadelimtheory
   875 %
   876 \endisadelimtheory
   877 %
   878 \isatagtheory
   879 \isacommand{end}\isamarkupfalse%
   880 %
   881 \endisatagtheory
   882 {\isafoldtheory}%
   883 %
   884 \isadelimtheory
   885 %
   886 \endisadelimtheory
   887 \isanewline
   888 \end{isabellebody}%
   889 %%% Local Variables:
   890 %%% mode: latex
   891 %%% TeX-master: "root"
   892 %%% End: