%
\begin{isabellebody}%
\def\isabellecontext{logic}%
%
\isadelimtheory
\isanewline
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ logic\ \isakeyword{imports}\ base\ \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.}%
\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}}, which 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. The intersections of all (finitely
many) classes declared in the current theory are the minimal
elements wrt.\ the sort order.
\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, including the sort constraint. The core logic
handles type variables with the same name but different sorts as
different, although some outer layers of the system make it hard to
produce anything like this.
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}.
A \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}k}.
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, unification on the algebra of types has most general
solutions (modulo equivalence of sorts). This means that
type-inference will produce primary types as expected
\cite{nipkow-prehofer}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{class}\verb|type class| \\
\indexmltype{sort}\verb|type sort| \\
\indexmltype{arity}\verb|type arity| \\
\indexmltype{typ}\verb|type typ| \\
\indexml{map-atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
\indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
\indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
\indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
\indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
\indexml{Sign.add-tyabbrs-i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
\verb| (string * string list * typ * mixfix) list -> theory -> theory| \\
\indexml{Sign.primitive-class}\verb|Sign.primitive_class: string * class list -> theory -> theory| \\
\indexml{Sign.primitive-classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
\indexml{Sign.primitive-arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
\end{mldecls}
\begin{description}
\item \verb|class| represents type classes; this is an alias for
\verb|string|.
\item \verb|sort| represents sorts; this is an alias for
\verb|class list|.
\item \verb|arity| represents type arities; this is an alias for
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.
\item \verb|typ| represents types; this is a datatype with
constructors \verb|TFree|, \verb|TVar|, \verb|Type|.
\item \verb|map_atyps|~\isa{f\ {\isasymtau}} applies the mapping \isa{f}
to all atomic types (\verb|TFree|, \verb|TVar|) occurring in \isa{{\isasymtau}}.
\item \verb|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_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
defines a new type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} with
optional mixfix syntax.
\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 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
%
\isamarkupsection{Terms \label{sec:terms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\glossary{Term}{FIXME}
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 determined
by the corresponding binders. In contrast, free variables and
constants are 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}\isactrlisub {\isasymtau}{\isachardot}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}}
would correspond to \isa{{\isasymlambda}x\isactrlisub {\isasymtau}{\isachardot}\ {\isasymlambda}y\isactrlisub {\isasymtau}{\isachardot}\ x\ {\isacharplus}\ 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 variables} 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 inside-out
like a stack of hypothetical binders. The core logic only 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}}. 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 usually 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}}. Constants are declared in the context as polymorphic
families \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that valid 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}}. 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 A \emph{term} is defined inductively over variables and
constants, 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. Some outer layers of the system make it hard to
produce variables of the same name, but different types. In
particular, type-inference always demands ``consistent'' type
constraints for free variables. In contrast, mixed instances of
polymorphic constants occur frequently.
\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
\isa{{\isasymsigma}}. This means that the term implicitly depends on type
arguments that are not accounted in 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 demands special 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 fully expanded before entering the
logical core. Abbreviations are usually reverted when printing
terms, using the collective \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 higher operations (\secref{sec:rules}) that
are based on higher-order unification and matching.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{term}\verb|type term| \\
\indexml{op aconv}\verb|op aconv: term * term -> bool| \\
\indexml{map-term-types}\verb|map_term_types: (typ -> typ) -> term -> term| \\ %FIXME rename map_types
\indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
\indexml{map-aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
\indexml{fold-aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
\indexml{fastype-of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
\indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
\indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline%
\verb| ((string * mixfix) * term) list -> theory -> theory| \\
\indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
\end{mldecls}
\begin{description}
\item \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|map_term_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
\item \verb|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|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|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.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a
new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.
\item \verb|Sign.add_abbrevs|~\isa{print{\isacharunderscore}mode\ {\isacharbrackleft}{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional
mixfix syntax.
\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 the representations of polymorphic constants: the
full type instance vs.\ the compact type arguments form (depending
on the most general declaration given in the context).
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsection{Theorems \label{sec:thms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\glossary{Proposition}{FIXME A \seeglossary{term} of
\seeglossary{type} \isa{prop}. Internally, there is nothing
special about propositions apart from their type, but the concrete
syntax enforces a clear distinction. Propositions are structured
via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything else is considered atomic. The canonical
form for propositions is that of a \seeglossary{Hereditary Harrop
Formula}. FIXME}
\glossary{Theorem}{A proven proposition within a certain theory and
proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
rarely spelled out explicitly. Theorems are usually normalized
according to the \seeglossary{HHF} format. FIXME}
\glossary{Fact}{Sometimes used interchangeably for
\seeglossary{theorem}. Strictly speaking, a list of theorems,
essentially an extra-logical conjunction. Facts emerge either as
local assumptions, or as results of local goal statements --- both
may be simultaneous, hence the list representation. FIXME}
\glossary{Schematic variable}{FIXME}
\glossary{Fixed variable}{A variable that is bound within a certain
proof context; an arbitrary-but-fixed entity within a portion of
proof text. FIXME}
\glossary{Free variable}{Synonymous for \seeglossary{fixed
variable}. FIXME}
\glossary{Bound variable}{FIXME}
\glossary{Variable}{See \seeglossary{schematic variable},
\seeglossary{fixed variable}, \seeglossary{bound variable}, or
\seeglossary{type variable}. The distinguishing feature of
different variables is their binding scope. FIXME}
A \emph{proposition} is a well-formed 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%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
The theory \isa{Pure} contains declarations for the standard
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 hypotheses
\isa{{\isasymGamma}} may \emph{not} contain schematic variables. The builtin
equality is conceptually axiomatized as shown in
\figref{fig:pure-equality}, although the implementation works
directly with derived inference rules.
\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}{\isacharunderscore}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}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}
\]
\[
\infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
\qquad
\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}}
\]
\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 may never 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}{\isacharunderscore}intro}) need
not be recorded in the hypotheses, because the simple syntactic
types of Pure are always inhabitable. Typing ``assumptions'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} are (implicitly) present only with occurrences of \isa{x\isactrlisub {\isasymtau}} in the statement body.\footnote{This is the key
difference ``\isa{{\isasymlambda}HOL}'' in the PTS framework
\cite{Barendregt-Geuvers:2001}, where \isa{x\ {\isacharcolon}\ A} hypotheses are
treated explicitly for types, in the same way as propositions.}
\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 substitution through derivations
inductively, we get admissible \isa{generalize} and \isa{instance} rules 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 monotonicity 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 The system allows axioms to be stated either as plain
propositions, or as arbitrary functions (``oracles'') that produce
propositions depending on given arguments. It is possible to trace
the used of axioms (and defined theorems) in derivations.
Invocations of oracles are recorded invariable.
Axiomatizations should be limited to the bare minimum, typically as
part of the initial logical basis of an object-logic formalization.
Normally, theories will be developed definitionally, by stating
restricted equalities over 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} is a closed term without any hidden polymorphism. The RHS may
depend on further defined constants, but not \isa{c} itself.
Definitions of constants with function type may be presented
liberally as \isa{c\ \isactrlvec \ {\isasymequiv}\ t} instead of the puristic \isa{c\ {\isasymequiv}\ {\isasymlambda}\isactrlvec x{\isachardot}\ t}.
An \emph{overloaded definition} consists may give zero or one
equality axioms \isa{c{\isacharparenleft}{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}{\isacharparenright}\ {\isasymequiv}\ t} for each type
constructor \isa{{\isasymkappa}}, with distinct variables \isa{\isactrlvec {\isasymalpha}}
as formal arguments. 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
\indexmltype{ctyp}\verb|type ctyp| \\
\indexmltype{cterm}\verb|type cterm| \\
\indexmltype{thm}\verb|type thm| \\
\indexml{proofs}\verb|proofs: int ref| \\
\indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
\indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
\indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
\indexml{Thm.forall-intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
\indexml{Thm.forall-elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
\indexml{Thm.implies-intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
\indexml{Thm.implies-elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
\indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
\indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
\indexml{Thm.get-axiom-i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
\indexml{Thm.invoke-oracle-i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
\indexml{Theory.add-axioms-i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
\indexml{Theory.add-deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
\indexml{Theory.add-oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
\indexml{Theory.add-defs-i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
\end{mldecls}
\begin{description}
\item \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.
This representation avoids syntactic rechecking in tight loops of
inferences. There are separate operations to decompose certified
entities (including actual theorems).
\item \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.
\item \verb|proofs| determines the detail of proof recording: \verb|0|
records only oracles, \verb|1| records oracles, axioms and named
theorems, \verb|2| records full proof terms.
\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}. A collection of type and term variables
is generalized simultaneously, according to 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.get_axiom_i|~\isa{thy\ name} retrieves a named
axiom, cf.\ \isa{axiom} in \figref{fig:prim-rules}.
\item \verb|Thm.invoke_oracle_i|~\isa{thy\ name\ arg} invokes the
oracle function \isa{name} of the theory. Logically, this is
just another instance of \isa{axiom} in \figref{fig:prim-rules},
but the system records an explicit trace of oracle invocations with
the \isa{thm} value.
\item \verb|Theory.add_axioms_i|~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} adds
arbitrary axioms, without any checking of the proposition.
\item \verb|Theory.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an
oracle, i.e.\ a function for generating arbitrary axioms.
\item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a new specification for
constant \isa{c\isactrlisub {\isasymtau}} from relative to existing ones for
constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.
\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 already
declared constant \isa{c}. Dependencies are recorded using \verb|Theory.add_deps|, unless the \isa{unchecked} option is set.
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\endisatagmlref
{\isafoldmlref}%
%
\isadelimmlref
%
\endisadelimmlref
%
\isamarkupsubsection{Auxiliary connectives%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Theory \isa{Pure} also defines a few auxiliary connectives, see
\figref{fig:pure-aux}. These are normally not exposed to the user,
but appear in internal encodings only.
\begin{figure}[htb]
\begin{center}
\begin{tabular}{ll}
\isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}}) \\
\isa{{\isasymturnstile}\ A\ {\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}}, hidden) \\
\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}
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}.
Conjunction allows to treat simultaneous assumptions and conclusions
uniformly. For example, multiple claims are intermediately
represented as explicit conjunction, but this is usually refined
into separate sub-goals before the user continues the proof; the
final result is projected into a list of theorems (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-formed 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 \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}
\indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
\indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
\indexml{Drule.mk-term}\verb|Drule.mk_term: cterm -> thm| \\
\indexml{Drule.dest-term}\verb|Drule.dest_term: thm -> cterm| \\
\indexml{Logic.mk-type}\verb|Logic.mk_type: typ -> term| \\
\indexml{Logic.dest-type}\verb|Logic.dest_type: term -> typ| \\
\end{mldecls}
\begin{description}
\item \verb|Conjunction.intr| derives \isa{A\ {\isacharampersand}\ B} from \isa{A} and \isa{B}.
\item \verb|Conjunction.intr| derives \isa{A} and \isa{B}
from \isa{A\ {\isacharampersand}\ B}.
\item \verb|Drule.mk_term|~\isa{t} derives \isa{TERM\ t}.
\item \verb|Drule.dest_term|~\isa{TERM\ t} recovers term \isa{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{Rules \label{sec:rules}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME
A \emph{rule} is any Pure theorem in HHF normal form; there is a
separate calculus for rule composition, which is modeled after
Gentzen's Natural Deduction \cite{Gentzen:1935}, but allows
rules to be nested arbitrarily, similar to \cite{extensions91}.
Normally, all theorems accessible to the user are proper rules.
Low-level inferences are occasional required internally, but the
result should be always presented in canonical form. The higher
interfaces of Isabelle/Isar will always produce proper rules. It is
important to maintain this invariant in add-on applications!
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
combined in the variants of \isa{elim{\isacharminus}resolution} and \isa{dest{\isacharminus}resolution}. Raw \isa{composition} is occasionally
useful as well, also it is strictly speaking outside of the proper
rule calculus.
Rules are treated modulo general higher-order unification, which is
unification modulo the equational theory of \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion
on \isa{{\isasymlambda}}-terms. Moreover, propositions are understood modulo
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}}.
This means that any operations within the rule calculus may be
subject to spontaneous \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-HHF conversions. It is common
practice not to contract or expand unnecessarily. Some mechanisms
prefer an one form, others the opposite, so there is a potential
danger to produce some oscillation!
Only few operations really work \emph{modulo} HHF conversion, but
expect a normal form: quantifiers \isa{{\isasymAnd}} before implications
\isa{{\isasymLongrightarrow}} at each level of nesting.
\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
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}.
Any proposition may be put into HHF form by normalizing with the rule
\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
quantifier prefix is represented via \seeglossary{schematic
variables}, such that the top-level structure is merely that of a
\seeglossary{Horn Clause}}.
\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
\[
\infer[\isa{{\isacharparenleft}assumption{\isacharparenright}}]{\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})}}
\]
\[
\infer[\isa{{\isacharparenleft}compose{\isacharparenright}}]{\isa{\isactrlvec A{\isasymvartheta}\ {\isasymLongrightarrow}\ C{\isasymvartheta}}}
{\isa{\isactrlvec A\ {\isasymLongrightarrow}\ B} & \isa{B{\isacharprime}\ {\isasymLongrightarrow}\ C} & \isa{B{\isasymvartheta}\ {\isacharequal}\ B{\isacharprime}{\isasymvartheta}}}
\]
\[
\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}}
\]
\[
\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}}
\]
The \isa{resolve} scheme is now acquired from \isa{{\isasymAnd}{\isacharunderscore}lift},
\isa{{\isasymLongrightarrow}{\isacharunderscore}lift}, and \isa{compose}.
\[
\infer[\isa{{\isacharparenleft}resolution{\isacharparenright}}]
{\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}}
\]
FIXME \isa{elim{\isacharunderscore}resolution}, \isa{dest{\isacharunderscore}resolution}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: