%

\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}{\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}

  \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| \\

  \end{mldecls}

  \begin{mldecls}

  \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 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

%

\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}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}} would

  correspond to \isa{{\isasymlambda}x\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}y\isactrlbsub nat\isactrlesub {\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 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}}.  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 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 An \emph{atomic} term is either a variable or constant.  A

  \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.  Some outer layers of the system make it hard to

  produce variables of the same name, but different types.  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 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: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\_types}\verb|map_types: (typ -> typ) -> term -> term| \\

  \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| \\

  \end{mldecls}

  \begin{mldecls}

  \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\

  \indexml{lambda}\verb|lambda: term -> term -> term| \\

  \indexml{betapply}\verb|betapply: term * term -> term| \\

  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Markup.property list -> bstring * typ * mixfix ->|\isasep\isanewline%

\verb|  theory -> term * theory| \\

  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Markup.property list -> bstring * term ->|\isasep\isanewline%

\verb|  theory -> (term * term) * 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_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.declare_const|~\isa{properties\ {\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\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\ properties\ {\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

%

\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-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}{\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 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}{\isacharunderscore}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{instance} 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.  Tracing plain axioms (and named theorems) is optional.

  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.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isadelimmlref

%

\endisadelimmlref

%

\isatagmlref

%

\begin{isamarkuptext}%

\begin{mldecls}

  \indexmltype{ctyp}\verb|type ctyp| \\

  \indexmltype{cterm}\verb|type cterm| \\

  \indexml{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\

  \indexml{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\

  \end{mldecls}

  \begin{mldecls}

  \indexmltype{thm}\verb|type thm| \\

  \indexml{proofs}\verb|proofs: int ref| \\

  \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| \\

  \end{mldecls}

  \begin{mldecls}

  \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.

  \item \verb|ctyp_of|~\isa{thy\ {\isasymtau}} and \verb|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 \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| determines the detail of proof recording within

  \verb|thm| values: \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}.  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.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 a

  named oracle function, cf.\ \isa{axiom} in

  \figref{fig:prim-rules}.

  \item \verb|Theory.add_axioms_i|~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares

  arbitrary propositions as axioms.

  \item \verb|Theory.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an oracle

  function for generating arbitrary axioms on the fly.

  \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}}.

  \item \verb|Theory.add_defs_i|~\isa{unchecked\ overloaded\ {\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} states a definitional axiom for an existing

  constant \isa{c}.  Dependencies are recorded (cf.\ \verb|Theory.add_deps|), unless the \isa{unchecked} option is set.

  \end{description}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\endisatagmlref

{\isafoldmlref}%

%

\isadelimmlref

%

\endisadelimmlref

%

\isamarkupsubsection{Auxiliary definitions%

}

\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}}) \\

  \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}}, 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}

  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 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-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 \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.elim| derives \isa{A} and \isa{B}

  from \isa{A\ {\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{Rules \label{sec:rules}%

}

\isamarkuptrue%

%

\isadelimFIXME

%

\endisadelimFIXME

%

\isatagFIXME

%

\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%

%

\endisatagFIXME

{\isafoldFIXME}%

%

\isadelimFIXME

%

\endisadelimFIXME

%

\isadelimtheory

%

\endisadelimtheory

%

\isatagtheory

\isacommand{end}\isamarkupfalse%

%

\endisatagtheory

{\isafoldtheory}%

%

\isadelimtheory

%

\endisadelimtheory

\isanewline

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: