%
\begin{isabellebody}%
\def\isabellecontext{Logic}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Logic\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Primitive logic \label{ch:logic}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The logical foundations of Isabelle/Isar are that of the Pure logic,
which has been introduced as a Natural Deduction framework in
\cite{paulson700}. This is essentially the same logic as ``\isa{{\isasymlambda}HOL}'' in the more abstract setting of Pure Type Systems (PTS)
\cite{Barendregt-Geuvers:2001}, although there are some key
differences in the specific treatment of simple types in
Isabelle/Pure.
Following type-theoretic parlance, the Pure logic consists of three
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
\isa{{\isasymLongrightarrow}} for implication (proofs depending on proofs).
Derivations are relative to a logical theory, which declares type
constructors, constants, and axioms. Theory declarations support
schematic polymorphism, which is strictly speaking outside the
logic.\footnote{This is the deeper logical reason, why the theory
context \isa{{\isasymTheta}} is separate from the proof context \isa{{\isasymGamma}}
of the core calculus: type constructors, term constants, and facts
(proof constants) may involve arbitrary type schemes, but the type
of a locally fixed term parameter is also fixed!}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Types \label{sec:types}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The language of types is an uninterpreted order-sorted first-order
algebra; types are qualified by ordered type classes.
\medskip A \emph{type class} is an abstract syntactic entity
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
generating relation; the transitive closure is maintained
internally. The resulting relation is an ordering: reflexive,
transitive, and antisymmetric.
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}}, it represents symbolic intersection. Notationally, the
curly braces are omitted for singleton intersections, i.e.\ any
class \isa{c} may be read as a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering
on type classes is extended to 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 \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection \isa{{\isacharbraceleft}{\isacharbraceright}} refers to
the universal sort, which is the largest element wrt.\ the sort
order. Thus \isa{{\isacharbraceleft}{\isacharbraceright}} represents the ``full sort'', not the
empty one! The intersection of all (finitely many) classes declared
in the current theory is the least element wrt.\ the sort ordering.
\medskip A \emph{fixed type variable} is a pair of a basic name
(starting with a \isa{{\isacharprime}} character) and a sort constraint, e.g.\
\isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ s{\isacharparenright}} which is usually printed as \isa{{\isasymalpha}\isactrlisub s}.
A \emph{schematic type variable} is a pair of an indexname and a
sort constraint, e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually
printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.
Note that \emph{all} syntactic components contribute to the identity
of type variables: basic name, index, and sort constraint. The core
logic handles type variables with the same name but different sorts
as different, although the type-inference layer (which is outside
the core) rejects anything like that.
A \emph{type constructor} \isa{{\isasymkappa}} is a \isa{k}-ary operator
on types declared in the theory. Type constructor application is
written postfix as \isa{{\isacharparenleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub k{\isacharparenright}{\isasymkappa}}. For
\isa{k\ {\isacharequal}\ {\isadigit{0}}} the argument tuple is omitted, e.g.\ \isa{prop}
instead of \isa{{\isacharparenleft}{\isacharparenright}prop}. For \isa{k\ {\isacharequal}\ {\isadigit{1}}} the parentheses
are omitted, e.g.\ \isa{{\isasymalpha}\ list} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharparenright}list}.
Further notation is provided for specific constructors, notably the
right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}.
The logical category \emph{type} is defined inductively over type
variables and type 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}}.
A \emph{type abbreviation} is a syntactic definition \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} of an arbitrary type expression \isa{{\isasymtau}} over
variables \isa{\isactrlvec {\isasymalpha}}. Type abbreviations appear as type
constructors in the syntax, but are expanded before entering the
logical core.
A \emph{type arity} declares the image behavior of a type
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
of sort \isa{s} if every argument type \isa{{\isasymtau}\isactrlisub i} is
of sort \isa{s\isactrlisub i}. Arity declarations are implicitly
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}.
\medskip The sort algebra is always maintained as \emph{coregular},
which means that type arities are consistent with the subclass
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.
The key property of a coregular order-sorted algebra is that sort
constraints can be solved in a most general fashion: for each type
constructor \isa{{\isasymkappa}} and sort \isa{s} there is a most general
vector of argument sorts \isa{{\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub k{\isacharparenright}} such
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}.
Consequently, type unification has most general solutions (modulo
equivalence of sorts), so type-inference produces primary types as
expected \cite{nipkow-prehofer}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{class}\verb|type class = string| \\
\indexdef{}{ML type}{sort}\verb|type sort = class list| \\
\indexdef{}{ML type}{arity}\verb|type arity = string * sort list * sort| \\
\indexdef{}{ML type}{typ}\verb|type typ| \\
\indexdef{}{ML}{Term.map\_atyps}\verb|Term.map_atyps: (typ -> typ) -> typ -> typ| \\
\indexdef{}{ML}{Term.fold\_atyps}\verb|Term.fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
\indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
\indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (binding * int * mixfix) list -> theory -> theory| \\
\indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: binding * string list * typ -> theory -> theory| \\
\indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\
\indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
\indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
\end{mldecls}
\begin{description}
\item Type \verb|class| represents type classes.
\item Type \verb|sort| represents sorts, i.e.\ finite
intersections of classes. The empty list \verb|[]: sort| refers to
the empty class intersection, i.e.\ the ``full sort''.
\item Type \verb|arity| represents type arities. A triple
\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}\ {\isacharcolon}\ arity} represents \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} as described above.
\item Type \verb|typ| represents types; this is a datatype with
constructors \verb|TFree|, \verb|TVar|, \verb|Type|.
\item \verb|Term.map_atyps|~\isa{f\ {\isasymtau}} applies the mapping \isa{f} to all atomic types (\verb|TFree|, \verb|TVar|) occurring in
\isa{{\isasymtau}}.
\item \verb|Term.fold_atyps|~\isa{f\ {\isasymtau}} iterates the operation
\isa{f} over all occurrences of atomic types (\verb|TFree|, \verb|TVar|) in \isa{{\isasymtau}}; the type structure is traversed from left to
right.
\item \verb|Sign.subsort|~\isa{thy\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ s\isactrlisub {\isadigit{2}}{\isacharparenright}}
tests the subsort relation \isa{s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlisub {\isadigit{2}}}.
\item \verb|Sign.of_sort|~\isa{thy\ {\isacharparenleft}{\isasymtau}{\isacharcomma}\ s{\isacharparenright}} tests whether type
\isa{{\isasymtau}} is of sort \isa{s}.
\item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a new
type constructors \isa{{\isasymkappa}} with \isa{k} arguments and
optional mixfix syntax.
\item \verb|Sign.add_type_abbrev|~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}}.
\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
relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}, for \isa{i\ {\isacharequal}\ {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ n}.
\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}}}.
\item \verb|Sign.primitive_arity|~\isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares
the arity \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isatagmlantiq
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{class}\hypertarget{ML antiquotation.class}{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{sort}\hypertarget{ML antiquotation.sort}{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{type\_name}\hypertarget{ML antiquotation.type-name}{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isacharunderscore}name}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{type\_abbrev}\hypertarget{ML antiquotation.type-abbrev}{\hyperlink{ML antiquotation.type-abbrev}{\mbox{\isa{type{\isacharunderscore}abbrev}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{nonterminal}\hypertarget{ML antiquotation.nonterminal}{\hyperlink{ML antiquotation.nonterminal}{\mbox{\isa{nonterminal}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{typ}\hypertarget{ML antiquotation.typ}{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\end{matharray}
\begin{rail}
'class' nameref
;
'sort' sort
;
('type_name' | 'type_abbrev' | 'nonterminal') nameref
;
'typ' type
;
\end{rail}
\begin{description}
\item \isa{{\isacharat}{\isacharbraceleft}class\ c{\isacharbraceright}} inlines the internalized class \isa{c} --- as \verb|string| literal.
\item \isa{{\isacharat}{\isacharbraceleft}sort\ s{\isacharbraceright}} inlines the internalized sort \isa{s}
--- as \verb|string list| literal.
\item \isa{{\isacharat}{\isacharbraceleft}type{\isacharunderscore}name\ c{\isacharbraceright}} inlines the internalized type
constructor \isa{c} --- as \verb|string| literal.
\item \isa{{\isacharat}{\isacharbraceleft}type{\isacharunderscore}abbrev\ c{\isacharbraceright}} inlines the internalized type
abbreviation \isa{c} --- as \verb|string| literal.
\item \isa{{\isacharat}{\isacharbraceleft}nonterminal\ c{\isacharbraceright}} inlines the internalized syntactic
type~/ grammar nonterminal \isa{c} --- as \verb|string|
literal.
\item \isa{{\isacharat}{\isacharbraceleft}typ\ {\isasymtau}{\isacharbraceright}} inlines the internalized type \isa{{\isasymtau}}
--- as constructor term for datatype \verb|typ|.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlantiq
{\isafoldmlantiq}%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isamarkupsection{Terms \label{sec:terms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus
with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
or \cite{paulson-ml2}), with the types being determined by the
corresponding binders. In contrast, free variables and constants
have an explicit name and type in each occurrence.
\medskip A \emph{bound variable} is a natural number \isa{b},
which accounts for the number of intermediate binders between the
variable occurrence in the body and its binding position. For
example, the de-Bruijn term \isa{{\isasymlambda}\isactrlbsub bool\isactrlesub {\isachardot}\ {\isasymlambda}\isactrlbsub bool\isactrlesub {\isachardot}\ {\isadigit{1}}\ {\isasymand}\ {\isadigit{0}}} would
correspond to \isa{{\isasymlambda}x\isactrlbsub bool\isactrlesub {\isachardot}\ {\isasymlambda}y\isactrlbsub bool\isactrlesub {\isachardot}\ x\ {\isasymand}\ y} in a named
representation. Note that a bound variable may be represented by
different de-Bruijn indices at different occurrences, depending on
the nesting of abstractions.
A \emph{loose variable} is a bound variable that is outside the
scope of local binders. The types (and names) for loose variables
can be managed as a separate context, that is maintained as a stack
of hypothetical binders. The core logic operates on closed terms,
without any loose variables.
A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
\isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}} here. A
\emph{schematic variable} is a pair of an indexname and a type,
e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is likewise printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}.
\medskip A \emph{constant} is a pair of a basic name and a type,
e.g.\ \isa{{\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{c\isactrlisub {\isasymtau}}
here. Constants are declared in the context as polymorphic families
\isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that all substitution instances \isa{c\isactrlisub {\isasymtau}} for \isa{{\isasymtau}\ {\isacharequal}\ {\isasymsigma}{\isasymvartheta}} are valid.
The vector of \emph{type arguments} of constant \isa{c\isactrlisub {\isasymtau}} wrt.\
the declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is defined as the codomain of 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}}, corresponding to the
left-to-right occurrences of the \isa{{\isasymalpha}\isactrlisub i} in \isa{{\isasymsigma}}.
Within a given theory context, 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}}.
Constant declarations \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} may contain sort constraints
for type variables in \isa{{\isasymsigma}}. These are observed by
type-inference as expected, but \emph{ignored} by the core logic.
This means the primitive logic is able to reason with instances of
polymorphic constants that the user-level type-checker would reject
due to violation of type class restrictions.
\medskip An \emph{atomic term} is either a variable or constant.
The logical category \emph{term} is defined inductively over atomic
terms, with 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}}}. Parsing and printing takes care of
converting between an external representation with named bound
variables. Subsequently, we shall use the latter notation instead
of internal de-Bruijn representation.
The inductive relation \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} assigns a (unique) type to a
term according to the structure of atomic terms, abstractions, and
applicatins:
\[
\infer{\isa{a\isactrlisub {\isasymtau}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}{}
\qquad
\infer{\isa{{\isacharparenleft}{\isasymlambda}x\isactrlsub {\isasymtau}{\isachardot}\ t{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}
\qquad
\infer{\isa{t\ u\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}}{\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}} & \isa{u\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}
\]
A \emph{well-typed term} is a term that can be typed according to these rules.
Typing information can be omitted: type-inference is able to
reconstruct the most general type of a raw term, while assigning
most general types to all of its variables and constants.
Type-inference depends on a context of type constraints for fixed
variables, and declarations for polymorphic constants.
The identity of atomic terms consists both of the name and the type
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 instantiation. Type-inference rejects variables of the same
name, but different types. In contrast, mixed instances of
polymorphic constants occur routinely.
\medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}
is the set of type variables occurring in \isa{t}, but not in
its type \isa{{\isasymsigma}}. This means that the term implicitly depends
on type arguments that are not accounted in the result type, i.e.\
there are different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and
\isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type. This slightly
pathological situation notoriously demands additional care.
\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}},
without any hidden polymorphism. A term abbreviation looks like a
constant in the syntax, but is expanded before entering the logical
core. Abbreviations are usually reverted when printing terms, using
\isa{t\ {\isasymrightarrow}\ c\isactrlisub {\isasymsigma}} as rules for higher-order rewriting.
\medskip Canonical operations on \isa{{\isasymlambda}}-terms include \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion: \isa{{\isasymalpha}}-conversion refers to capture-free
renaming of bound variables; \isa{{\isasymbeta}}-conversion contracts an
abstraction applied to an argument term, substituting the argument
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
does not occur in \isa{f}.
Terms are normally treated modulo \isa{{\isasymalpha}}-conversion, which is
implicit in the de-Bruijn representation. Names for bound variables
in abstractions are maintained separately as (meaningless) comments,
mostly for parsing and printing. Full \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion is
commonplace in various standard operations (\secref{sec:obj-rules})
that are based on higher-order unification and matching.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{term}\verb|type term| \\
\indexdef{}{ML}{aconv}\verb|op aconv: term * term -> bool| \\
\indexdef{}{ML}{Term.map\_types}\verb|Term.map_types: (typ -> typ) -> term -> term| \\
\indexdef{}{ML}{Term.fold\_types}\verb|Term.fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
\indexdef{}{ML}{Term.map\_aterms}\verb|Term.map_aterms: (term -> term) -> term -> term| \\
\indexdef{}{ML}{Term.fold\_aterms}\verb|Term.fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
\indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
\indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: (binding * typ) * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
\indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%
\verb| theory -> (term * term) * theory| \\
\indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
\end{mldecls}
\begin{description}
\item Type \verb|term| represents de-Bruijn terms, with comments
in abstractions, and explicitly named free variables and constants;
this is a datatype with constructors \verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|, \verb|Abs|, \verb|op $|.
\item \isa{t}~\verb|aconv|~\isa{u} checks \isa{{\isasymalpha}}-equivalence of two terms. This is the basic equality relation
on type \verb|term|; raw datatype equality should only be used
for operations related to parsing or printing!
\item \verb|Term.map_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
\item \verb|Term.fold_types|~\isa{f\ t} iterates the operation
\isa{f} over all occurrences of types in \isa{t}; the term
structure is traversed from left to right.
\item \verb|Term.map_aterms|~\isa{f\ t} applies the mapping \isa{f} to all atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) occurring in \isa{t}.
\item \verb|Term.fold_aterms|~\isa{f\ t} iterates the operation
\isa{f} over all occurrences of atomic terms (\verb|Bound|, \verb|Free|, \verb|Var|, \verb|Const|) in \isa{t}; the term structure is
traversed from left to right.
\item \verb|fastype_of|~\isa{t} determines the type of a
well-typed term. This operation is relatively slow, despite the
omission of any sanity checks.
\item \verb|lambda|~\isa{a\ b} produces an abstraction \isa{{\isasymlambda}a{\isachardot}\ b}, where occurrences of the atomic term \isa{a} in the
body \isa{b} are replaced by bound variables.
\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
abstraction.
\item \verb|Sign.declare_const|~\isa{{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}}
declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix
syntax.
\item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
\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}}
convert between two representations of polymorphic constants: full
type instance vs.\ compact type arguments form.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isatagmlantiq
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{const\_name}\hypertarget{ML antiquotation.const-name}{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isacharunderscore}name}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{const\_abbrev}\hypertarget{ML antiquotation.const-abbrev}{\hyperlink{ML antiquotation.const-abbrev}{\mbox{\isa{const{\isacharunderscore}abbrev}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{const}\hypertarget{ML antiquotation.const}{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{term}\hypertarget{ML antiquotation.term}{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{prop}\hypertarget{ML antiquotation.prop}{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\end{matharray}
\begin{rail}
('const_name' | 'const_abbrev') nameref
;
'const' ('(' (type + ',') ')')?
;
'term' term
;
'prop' prop
;
\end{rail}
\begin{description}
\item \isa{{\isacharat}{\isacharbraceleft}const{\isacharunderscore}name\ c{\isacharbraceright}} inlines the internalized logical
constant name \isa{c} --- as \verb|string| literal.
\item \isa{{\isacharat}{\isacharbraceleft}const{\isacharunderscore}abbrev\ c{\isacharbraceright}} inlines the internalized
abbreviated constant name \isa{c} --- as \verb|string|
literal.
\item \isa{{\isacharat}{\isacharbraceleft}const\ c{\isacharparenleft}\isactrlvec {\isasymtau}{\isacharparenright}{\isacharbraceright}} inlines the internalized
constant \isa{c} with precise type instantiation in the sense of
\verb|Sign.const_instance| --- as \verb|Const| constructor term for
datatype \verb|term|.
\item \isa{{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}} inlines the internalized term \isa{t}
--- as constructor term for datatype \verb|term|.
\item \isa{{\isacharat}{\isacharbraceleft}prop\ {\isasymphi}{\isacharbraceright}} inlines the internalized proposition
\isa{{\isasymphi}} --- as constructor term for datatype \verb|term|.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlantiq
{\isafoldmlantiq}%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isamarkupsection{Theorems \label{sec:thms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A \emph{proposition} is a well-typed term of type \isa{prop}, a
\emph{theorem} is a proven proposition (depending on a context of
hypotheses and the background theory). Primitive inferences include
plain Natural Deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework. There is also a builtin
notion of equality/equivalence \isa{{\isasymequiv}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Primitive connectives and rules \label{sec:prim-rules}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The theory \isa{Pure} contains constant declarations for the
primitive connectives \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and \isa{{\isasymequiv}} of
the logical framework, see \figref{fig:pure-connectives}. The
derivability judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is
defined inductively by the primitive inferences given in
\figref{fig:prim-rules}, with the global restriction that the
hypotheses must \emph{not} contain any schematic variables. The
builtin equality is conceptually axiomatized as shown in
\figref{fig:pure-equality}, although the implementation works
directly with derived inferences.
\begin{figure}[htb]
\begin{center}
\begin{tabular}{ll}
\isa{all\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymRightarrow}\ prop{\isacharparenright}\ {\isasymRightarrow}\ prop} & universal quantification (binder \isa{{\isasymAnd}}) \\
\isa{{\isasymLongrightarrow}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & implication (right associative infix) \\
\isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\
\end{tabular}
\caption{Primitive connectives of Pure}\label{fig:pure-connectives}
\end{center}
\end{figure}
\begin{figure}[htb]
\begin{center}
\[
\infer[\isa{{\isacharparenleft}axiom{\isacharparenright}}]{\isa{{\isasymturnstile}\ A}}{\isa{A\ {\isasymin}\ {\isasymTheta}}}
\qquad
\infer[\isa{{\isacharparenleft}assume{\isacharparenright}}]{\isa{A\ {\isasymturnstile}\ A}}{}
\]
\[
\infer[\isa{{\isacharparenleft}{\isasymAnd}{\isasymdash}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}
\qquad
\infer[\isa{{\isacharparenleft}{\isasymAnd}{\isasymdash}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}
\]
\[
\infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isasymdash}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
\qquad
\infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isasymdash}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}}
\]
\caption{Primitive inferences of Pure}\label{fig:prim-rules}
\end{center}
\end{figure}
\begin{figure}[htb]
\begin{center}
\begin{tabular}{ll}
\isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}\ a\ {\isasymequiv}\ b{\isacharbrackleft}a{\isacharbrackright}} & \isa{{\isasymbeta}}-conversion \\
\isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity \\
\isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution \\
\isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\
\isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & logical equivalence \\
\end{tabular}
\caption{Conceptual axiomatization of Pure equality}\label{fig:pure-equality}
\end{center}
\end{figure}
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
are irrelevant in the Pure logic, though; they cannot occur within
propositions. The system provides a runtime option to record
explicit proof terms for primitive inferences. Thus all three
levels of \isa{{\isasymlambda}}-calculus become explicit: \isa{{\isasymRightarrow}} for
terms, and \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} for proofs (cf.\
\cite{Berghofer-Nipkow:2000:TPHOL}).
Observe that locally fixed parameters (as in \isa{{\isasymAnd}{\isasymdash}intro}) need not be recorded in the hypotheses, because
the simple syntactic 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 difference to ``\isa{{\isasymlambda}HOL}'' in
the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses
\isa{x\ {\isacharcolon}\ A} are treated uniformly for propositions and types.}
\medskip The axiomatization of a theory is implicitly closed by
forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} holds for any substitution instance of an axiom
\isa{{\isasymturnstile}\ A}. By pushing substitutions through derivations
inductively, we also get admissible \isa{generalize} and \isa{instantiate} rules as shown in \figref{fig:subst-rules}.
\begin{figure}[htb]
\begin{center}
\[
\infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} & \isa{{\isasymalpha}\ {\isasymnotin}\ {\isasymGamma}}}
\quad
\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}}}
\]
\[
\infer{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymtau}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}
\quad
\infer[\quad\isa{{\isacharparenleft}instantiate{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}t{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}
\]
\caption{Admissible substitution rules}\label{fig:subst-rules}
\end{center}
\end{figure}
Note that \isa{instantiate} does not require an explicit
side-condition, because \isa{{\isasymGamma}} may never contain schematic
variables.
In principle, variables could be substituted in hypotheses as well,
but this would disrupt the monotonicity of reasoning: deriving
\isa{{\isasymGamma}{\isasymvartheta}\ {\isasymturnstile}\ B{\isasymvartheta}} from \isa{{\isasymGamma}\ {\isasymturnstile}\ B} is
correct, but \isa{{\isasymGamma}{\isasymvartheta}\ {\isasymsupseteq}\ {\isasymGamma}} does not necessarily hold:
the result belongs to a different proof context.
\medskip An \emph{oracle} is a function that produces axioms on the
fly. Logically, this is an instance of the \isa{axiom} rule
(\figref{fig:prim-rules}), but there is an operational difference.
The system always records oracle invocations within derivations of
theorems by a unique tag.
Axiomatizations should be limited to the bare minimum, typically as
part of the initial logical basis of an object-logic formalization.
Later on, theories are usually developed in a strictly definitional
fashion, by stating only certain equalities over new constants.
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
may depend on further defined constants, but not \isa{c} itself.
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}.
An \emph{overloaded definition} consists of a collection of axioms
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
distinct variables \isa{\isactrlvec {\isasymalpha}}). The RHS may mention
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
primitive recursion over the syntactic structure of a single type
argument. See also \cite[\S4.3]{Haftmann-Wenzel:2006:classes}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{ctyp}\verb|type ctyp| \\
\indexdef{}{ML type}{cterm}\verb|type cterm| \\
\indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
\indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{thm}\verb|type thm| \\
\indexdef{}{ML}{proofs}\verb|proofs: int Unsynchronized.ref| \\
\indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
\indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
\indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
\indexdef{}{ML}{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
\indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
\indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
\indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
\indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: binding * term -> theory -> (string * thm) * theory| \\
\indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory ->|\isasep\isanewline%
\verb| (string * ('a -> thm)) * theory| \\
\indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: bool -> bool -> binding * term -> theory ->|\isasep\isanewline%
\verb| (string * thm) * theory| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list ->|\isasep\isanewline%
\verb| theory -> theory| \\
\end{mldecls}
\begin{description}
\item Types \verb|ctyp| and \verb|cterm| represent certified
types and terms, respectively. These are abstract datatypes that
guarantee that its values have passed the full well-formedness (and
well-typedness) checks, relative to the declarations of type
constructors, constants etc. in the theory.
\item \verb|Thm.ctyp_of|~\isa{thy\ {\isasymtau}} and \verb|Thm.cterm_of|~\isa{thy\ t} explicitly checks types and terms,
respectively. This also involves some basic normalizations, such
expansion of type and term abbreviations from the theory context.
Re-certification is relatively slow and should be avoided in tight
reasoning loops. There are separate operations to decompose
certified entities (including actual theorems).
\item Type \verb|thm| represents proven propositions. This is
an abstract datatype that guarantees that its values have been
constructed by basic principles of the \verb|Thm| module.
Every \verb|thm| value contains a sliding back-reference to the
enclosing theory, cf.\ \secref{sec:context-theory}.
\item \verb|proofs| specifies the detail of proof recording within
\verb|thm| values: \verb|0| records only the names of oracles,
\verb|1| records oracle names and propositions, \verb|2| additionally
records full proof terms. Officially named theorems that contribute
to a result are recorded in any case.
\item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim|
correspond to the primitive inferences of \figref{fig:prim-rules}.
\item \verb|Thm.generalize|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharcomma}\ \isactrlvec x{\isacharparenright}}
corresponds to the \isa{generalize} rules of
\figref{fig:subst-rules}. Here collections of type and term
variables are generalized simultaneously, specified by the given
basic names.
\item \verb|Thm.instantiate|~\isa{{\isacharparenleft}\isactrlvec {\isasymalpha}\isactrlisub s{\isacharcomma}\ \isactrlvec x\isactrlisub {\isasymtau}{\isacharparenright}} corresponds to the \isa{instantiate} rules
of \figref{fig:subst-rules}. Type variables are substituted before
term variables. Note that the types in \isa{\isactrlvec x\isactrlisub {\isasymtau}}
refer to the instantiated versions.
\item \verb|Thm.add_axiom|~\isa{{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}\ thy} declares an
arbitrary proposition as axiom, and retrieves it as a theorem from
the resulting theory, cf.\ \isa{axiom} in
\figref{fig:prim-rules}. Note that the low-level representation in
the axiom table may differ slightly from the returned theorem.
\item \verb|Thm.add_oracle|~\isa{{\isacharparenleft}binding{\isacharcomma}\ oracle{\isacharparenright}} produces a named
oracle rule, essentially generating arbitrary axioms on the fly,
cf.\ \isa{axiom} in \figref{fig:prim-rules}.
\item \verb|Thm.add_def|~\isa{unchecked\ overloaded\ {\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}} states a definitional axiom for an existing constant
\isa{c}. Dependencies are recorded via \verb|Theory.add_deps|,
unless the \isa{unchecked} option is set. Note that the
low-level representation in the axiom table may differ slightly from
the returned theorem.
\item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification
for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing
specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isatagmlantiq
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
\indexdef{}{ML antiquotation}{ctyp}\hypertarget{ML antiquotation.ctyp}{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{cterm}\hypertarget{ML antiquotation.cterm}{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{cprop}\hypertarget{ML antiquotation.cprop}{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{thm}\hypertarget{ML antiquotation.thm}{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{thms}\hypertarget{ML antiquotation.thms}{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\indexdef{}{ML antiquotation}{lemma}\hypertarget{ML antiquotation.lemma}{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
\end{matharray}
\begin{rail}
'ctyp' typ
;
'cterm' term
;
'cprop' prop
;
'thm' thmref
;
'thms' thmrefs
;
'lemma' ('(open)')? ((prop +) + 'and') \\ 'by' method method?
\end{rail}
\begin{description}
\item \isa{{\isacharat}{\isacharbraceleft}ctyp\ {\isasymtau}{\isacharbraceright}} produces a certified type wrt.\ the
current background theory --- as abstract value of type \verb|ctyp|.
\item \isa{{\isacharat}{\isacharbraceleft}cterm\ t{\isacharbraceright}} and \isa{{\isacharat}{\isacharbraceleft}cprop\ {\isasymphi}{\isacharbraceright}} produce a
certified term wrt.\ the current background theory --- as abstract
value of type \verb|cterm|.
\item \isa{{\isacharat}{\isacharbraceleft}thm\ a{\isacharbraceright}} produces a singleton fact --- as abstract
value of type \verb|thm|.
\item \isa{{\isacharat}{\isacharbraceleft}thms\ a{\isacharbraceright}} produces a general fact --- as abstract
value of type \verb|thm list|.
\item \isa{{\isacharat}{\isacharbraceleft}lemma\ {\isasymphi}\ by\ meth{\isacharbraceright}} produces a fact that is proven on
the spot according to the minimal proof, which imitates a terminal
Isar proof. The result is an abstract value of type \verb|thm|
or \verb|thm list|, depending on the number of propositions
given here.
The internal derivation object lacks a proper theorem name, but it
is formally closed, unless the \isa{{\isacharparenleft}open{\isacharparenright}} option is specified
(this may impact performance of applications with proof terms).
Since ML antiquotations are always evaluated at compile-time, there
is no run-time overhead even for non-trivial proofs. Nonetheless,
the justification is syntactically limited to a single \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} step. More complex Isar proofs should be done in regular
theory source, before compiling the corresponding ML text that uses
the result.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlantiq
{\isafoldmlantiq}%
%
\isadelimmlantiq
%
\endisadelimmlantiq
%
\isamarkupsubsection{Auxiliary definitions \label{sec:logic-aux}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Theory \isa{Pure} provides a few auxiliary definitions, see
\figref{fig:pure-aux}. These special constants are normally not
exposed to the user, but appear in internal encodings.
\begin{figure}[htb]
\begin{center}
\begin{tabular}{ll}
\isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}{\isacharampersand}{\isacharampersand}}) \\
\isa{{\isasymturnstile}\ A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\[1ex]
\isa{prop\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop} & (prefix \isa{{\isacharhash}}, suppressed) \\
\isa{{\isacharhash}A\ {\isasymequiv}\ A} \\[1ex]
\isa{term\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & (prefix \isa{TERM}) \\
\isa{term\ x\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}A{\isachardot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}} \\[1ex]
\isa{TYPE\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself} & (prefix \isa{TYPE}) \\
\isa{{\isacharparenleft}unspecified{\isacharparenright}} \\
\end{tabular}
\caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
\end{center}
\end{figure}
The introduction \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B}, and eliminations
(projections) \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymLongrightarrow}\ B} are
available as derived rules. Conjunction allows to treat
simultaneous assumptions and conclusions uniformly, e.g.\ consider
\isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ D}. In particular, the goal mechanism
represents multiple claims as explicit conjunction internally, but
this is refined (via backwards introduction) into separate sub-goals
before the user commences the proof; the final result is projected
into a list of theorems using eliminations (cf.\
\secref{sec:tactical-goals}).
The \isa{prop} marker (\isa{{\isacharhash}}) makes arbitrarily complex
propositions appear as atomic, without changing the meaning: \isa{{\isasymGamma}\ {\isasymturnstile}\ A} and \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isacharhash}A} are interchangeable. See
\secref{sec:tactical-goals} for specific operations.
The \isa{term} marker turns any well-typed term into a derivable
proposition: \isa{{\isasymturnstile}\ TERM\ t} holds unconditionally. Although
this is logically vacuous, it allows to treat terms and proofs
uniformly, similar to a type-theoretic framework.
The \isa{TYPE} constructor is the canonical representative of
the unspecified type \isa{{\isasymalpha}\ itself}; it essentially injects the
language of types into that of terms. There is specific notation
\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }.
Although being devoid of any particular meaning, the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} accounts for the type \isa{{\isasymtau}} within the term
language. In particular, \isa{TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}} may be used as formal
argument in primitive definitions, in order to circumvent hidden
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
a proposition \isa{A} that depends on an additional type
argument, which is essentially a predicate on types.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
\indexdef{}{ML}{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
\indexdef{}{ML}{Drule.mk\_term}\verb|Drule.mk_term: cterm -> thm| \\
\indexdef{}{ML}{Drule.dest\_term}\verb|Drule.dest_term: thm -> cterm| \\
\indexdef{}{ML}{Logic.mk\_type}\verb|Logic.mk_type: typ -> term| \\
\indexdef{}{ML}{Logic.dest\_type}\verb|Logic.dest_type: term -> typ| \\
\end{mldecls}
\begin{description}
\item \verb|Conjunction.intr| derives \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B} from \isa{A} and \isa{B}.
\item \verb|Conjunction.elim| derives \isa{A} and \isa{B}
from \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B}.
\item \verb|Drule.mk_term| derives \isa{TERM\ t}.
\item \verb|Drule.dest_term| recovers term \isa{t} from \isa{TERM\ t}.
\item \verb|Logic.mk_type|~\isa{{\isasymtau}} produces the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}}.
\item \verb|Logic.dest_type|~\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} recovers the type
\isa{{\isasymtau}}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsection{Object-level rules \label{sec:obj-rules}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The primitive inferences covered so far mostly serve foundational
purposes. User-level reasoning usually works via object-level rules
that are represented as theorems of Pure. Composition of rules
involves \emph{backchaining}, \emph{higher-order unification} modulo
\isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion of \isa{{\isasymlambda}}-terms, and so-called
\emph{lifting} of rules into a context of \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} connectives. Thus the full power of higher-order Natural
Deduction in Isabelle/Pure becomes readily available.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Hereditary Harrop Formulae%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The idea of object-level rules is to model Natural Deduction
inferences in the style of Gentzen \cite{Gentzen:1935}, but we allow
arbitrary nesting similar to \cite{extensions91}. The most basic
rule format is that of a \emph{Horn Clause}:
\[
\infer{\isa{A}}{\isa{A\isactrlsub {\isadigit{1}}} & \isa{{\isasymdots}} & \isa{A\isactrlsub n}}
\]
where \isa{A{\isacharcomma}\ A\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlsub n} are atomic propositions
of the framework, usually of the form \isa{Trueprop\ B}, where
\isa{B} is a (compound) object-level statement. This
object-level inference corresponds to an iterated implication in
Pure like this:
\[
\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ {\isasymLongrightarrow}\ A}
\]
As an example consider conjunction introduction: \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B}. Any parameters occurring in such rule statements are
conceptionally treated as arbitrary:
\[
\isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ A\isactrlsub {\isadigit{1}}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymLongrightarrow}\ {\isasymdots}\ A\isactrlsub n\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymLongrightarrow}\ A\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m}
\]
Nesting of rules means that the positions of \isa{A\isactrlsub i} may
again hold compound rules, not just atomic propositions.
Propositions of this format are called \emph{Hereditary Harrop
Formulae} in the literature \cite{Miller:1991}. Here we give an
inductive characterization as follows:
\medskip
\begin{tabular}{ll}
\isa{\isactrlbold x} & set of variables \\
\isa{\isactrlbold A} & set of atomic propositions \\
\isa{\isactrlbold H\ \ {\isacharequal}\ \ {\isasymAnd}\isactrlbold x\isactrlsup {\isacharasterisk}{\isachardot}\ \isactrlbold H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ \isactrlbold A} & set of Hereditary Harrop Formulas \\
\end{tabular}
\medskip
Thus we essentially impose nesting levels on propositions formed
from \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}. At each level there is a prefix
of parameters and compound premises, concluding an atomic
proposition. Typical examples are \isa{{\isasymlongrightarrow}}-introduction \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B} or mathematical induction \isa{P\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ P\ n\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n}. Even deeper nesting occurs in well-founded
induction \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymprec}\ x\ {\isasymLongrightarrow}\ P\ y{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x}, but this
already marks the limit of rule complexity that is usually seen in
practice.
\medskip Regular user-level inferences in Isabelle/Pure always
maintain the following canonical form of results:
\begin{itemize}
\item Normalization by \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}},
which is a theorem of Pure, means that quantifiers are pushed in
front of implication at each level of nesting. The normal form is a
Hereditary Harrop Formula.
\item The outermost prefix of parameters is represented via
schematic variables: instead of \isa{{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ A\ \isactrlvec x} we have \isa{\isactrlvec H\ {\isacharquery}\isactrlvec x\ {\isasymLongrightarrow}\ A\ {\isacharquery}\isactrlvec x}.
Note that this representation looses information about the order of
parameters, and vacuous quantifiers vanish automatically.
\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{Simplifier.norm\_hhf}\verb|Simplifier.norm_hhf: thm -> thm| \\
\end{mldecls}
\begin{description}
\item \verb|Simplifier.norm_hhf|~\isa{thm} normalizes the given
theorem according to the canonical form specified above. This is
occasionally helpful to repair some low-level tools that do not
handle Hereditary Harrop Formulae properly.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Rule composition%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The rule calculus of Isabelle/Pure provides two main inferences:
\hyperlink{inference.resolution}{\mbox{\isa{resolution}}} (i.e.\ back-chaining of rules) and
\hyperlink{inference.assumption}{\mbox{\isa{assumption}}} (i.e.\ closing a branch), both modulo
higher-order unification. There are also combined variants, notably
\hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isacharunderscore}resolution}}} and \hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isacharunderscore}resolution}}}.
To understand the all-important \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle,
we first consider raw \indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}} (modulo
higher-order unification with substitution \isa{{\isasymvartheta}}):
\[
\infer[(\indexdef{}{inference}{composition}\hypertarget{inference.composition}{\hyperlink{inference.composition}{\mbox{\isa{composition}}}})]{\isa{\isactrlvec A{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}
{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B} & \isa{B{\isacharprime}\ {\isasymLongrightarrow}\ C} & \isa{B{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}}}
\]
Here the conclusion of the first rule is unified with the premise of
the second; the resulting rule instance inherits the premises of the
first and conclusion of the second. Note that \isa{C} can again
consist of iterated implications. We can also permute the premises
of the second rule back-and-forth in order to compose with \isa{B{\isacharprime}} in any position (subsequently we shall always refer to
position 1 w.l.o.g.).
In \hyperlink{inference.composition}{\mbox{\isa{composition}}} the internal structure of the common
part \isa{B} and \isa{B{\isacharprime}} is not taken into account. For
proper \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} we require \isa{B} to be atomic,
and explicitly observe the structure \isa{{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x} of the premise of the second rule. The
idea is to adapt the first rule by ``lifting'' it into this context,
by means of iterated application of the following inferences:
\[
\infer[(\indexdef{}{inference}{imp\_lift}\hypertarget{inference.imp-lift}{\hyperlink{inference.imp-lift}{\mbox{\isa{imp{\isacharunderscore}lift}}}})]{\isa{{\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ \isactrlvec A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}\isactrlvec H\ {\isasymLongrightarrow}\ B{\isacharparenright}}}{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B}}
\]
\[
\infer[(\indexdef{}{inference}{all\_lift}\hypertarget{inference.all-lift}{\hyperlink{inference.all-lift}{\mbox{\isa{all{\isacharunderscore}lift}}}})]{\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}}
\]
By combining raw composition with lifting, we get full \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} as follows:
\[
\infer[(\indexdef{}{inference}{resolution}\hypertarget{inference.resolution}{\hyperlink{inference.resolution}{\mbox{\isa{resolution}}}})]
{\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}}}
{\begin{tabular}{l}
\isa{\isactrlvec A\ {\isacharquery}\isactrlvec a\ {\isasymLongrightarrow}\ B\ {\isacharquery}\isactrlvec a} \\
\isa{{\isacharparenleft}{\isasymAnd}\isactrlvec x{\isachardot}\ \isactrlvec H\ \isactrlvec x\ {\isasymLongrightarrow}\ B{\isacharprime}\ \isactrlvec x{\isacharparenright}\ {\isasymLongrightarrow}\ C} \\
\isa{{\isacharparenleft}{\isasymlambda}\isactrlvec x{\isachardot}\ B\ {\isacharparenleft}{\isacharquery}\isactrlvec a\ \isactrlvec x{\isacharparenright}{\isacharparenright}{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}} \\
\end{tabular}}
\]
Continued resolution of rules allows to back-chain a problem towards
more and sub-problems. Branches are closed either by resolving with
a rule of 0 premises, or by producing a ``short-circuit'' within a
solved situation (again modulo unification):
\[
\infer[(\indexdef{}{inference}{assumption}\hypertarget{inference.assumption}{\hyperlink{inference.assumption}{\mbox{\isa{assumption}}}})]{\isa{C{\isasymvartheta}}}
{\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})}}
\]
FIXME \indexdef{}{inference}{elim\_resolution}\hypertarget{inference.elim-resolution}{\hyperlink{inference.elim-resolution}{\mbox{\isa{elim{\isacharunderscore}resolution}}}}, \indexdef{}{inference}{dest\_resolution}\hypertarget{inference.dest-resolution}{\hyperlink{inference.dest-resolution}{\mbox{\isa{dest{\isacharunderscore}resolution}}}}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{RS}\verb|op RS: thm * thm -> thm| \\
\indexdef{}{ML}{OF}\verb|op OF: thm * thm list -> thm| \\
\end{mldecls}
\begin{description}
\item \isa{rule\isactrlsub {\isadigit{1}}\ RS\ rule\isactrlsub {\isadigit{2}}} resolves \isa{rule\isactrlsub {\isadigit{1}}} with \isa{rule\isactrlsub {\isadigit{2}}} according to the \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle
explained above. Note that the corresponding rule attribute in the
Isar language is called \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}.
\item \isa{rule\ OF\ rules} resolves a list of rules with the
first rule, addressing its premises \isa{{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ length\ rules}
(operating from last to first). This means the newly emerging
premises are all concatenated, without interfering. Also note that
compared to \isa{RS}, the rule argument order is swapped: \isa{rule\isactrlsub {\isadigit{1}}\ RS\ rule\isactrlsub {\isadigit{2}}\ {\isacharequal}\ rule\isactrlsub {\isadigit{2}}\ OF\ {\isacharbrackleft}rule\isactrlsub {\isadigit{1}}{\isacharbrackright}}.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: