doc-src/IsarImplementation/Thy/document/logic.tex

updated;

%
\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 framework of Pure Type Systems (PTS)
  \cite{Barendregt-Geuvers:2001}, although there are some key
  differences in the practical treatment of simple types.

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

  Pure derivations are relative to a logical theory, which declares
  type constructors, term constants, and axioms.  Term constants and
  axioms support schematic polymorphism.%
\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 maintained internally.

  A \emph{sort} is a list of type classes written as \isa{{\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 in the canonical fashion: \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 (i.e.\ finitely many) classes declared in
  the current theory are the minimal elements wrt.\ sort order.

  \medskip A \emph{fixed type variable} is pair of a basic name
  (starting with \isa{{\isacharprime}} character) and a sort constraint.  For
  example, \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.  For example, \isa{{\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ s{\isacharparenright}} which is usually printed \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.

  Note that \emph{all} syntactic components contribute to the identity
  of a type variables, including the literal sort constraint.  The
  core logic handles type variables with the same name but different
  sorts as different, even though the outer layers of the system make
  it hard to produce anything like this.

  A \emph{type constructor} is an \isa{k}-ary type operator
  declared in the theory.
  
  A \emph{type} is defined inductively over type variables and type
  constructors: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}c}.  Type constructor application is usually written
  postfix.  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{{\isasymtau}\ list} instead of \isa{{\isacharparenleft}{\isasymtau}{\isacharparenright}\ list}.  Further notation is provided for specific
  constructors, notably right-associative infix \isa{{\isasymtau}\isactrlisub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymtau}\isactrlisub {\isadigit{2}}} instead of \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymtau}\isactrlisub {\isadigit{2}}{\isacharparenright}fun}
  constructor.

  A \emph{type abbreviation} is a syntactic abbreviation of an
  arbitrary type expression of the theory.  Type abbreviations looks
  like type constructors at the surface, but are expanded before the
  core logic encounters them.

  A \emph{type arity} declares the image behavior of a type
  constructor wrt.\ the algebra of sorts: \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlisub n{\isacharparenright}s} means that \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub k{\isacharparenright}c} is
  of sort \isa{s} if each argument type \isa{{\isasymtau}\isactrlisub i} is of
  sort \isa{s\isactrlisub i}.  The sort algebra is always maintained as
  \emph{coregular}, which means that type arities are consistent with
  the subclass relation: for each type constructor \isa{c} and
  classes \isa{c\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlisub {\isadigit{2}}}, any arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{1}}{\isacharparenright}c\isactrlisub {\isadigit{1}}} has a corresponding arity \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlisub {\isadigit{2}}{\isacharparenright}c\isactrlisub {\isadigit{2}}} where \isa{\isactrlvec s\isactrlisub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlisub {\isadigit{2}}} holds pointwise for all argument sorts.

  The key property of the order-sorted algebra of types is that sort
  constraints may be always fulfilled in a most general fashion: for
  each type constructor \isa{c} 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 \isa{{\isacharparenleft}{\isasymtau}\isactrlbsub s\isactrlisub {\isadigit{1}}\isactrlesub {\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlbsub s\isactrlisub k\isactrlesub {\isacharparenright}} for arbitrary \isa{{\isasymtau}\isactrlisub i} of
  sort \isa{s\isactrlisub i}.  This means the unification problem on
  the algebra of types has most general solutions (modulo renaming and
  equivalence of sorts).  As a consequence, type-inference is able to
  produce primary types.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimmlref
%
\endisadelimmlref
%
\isatagmlref
%
\begin{isamarkuptext}%
\begin{mldecls}
  \indexmltype{class}\verb|type class| \\
  \indexmltype{sort}\verb|type sort| \\
  \indexmltype{typ}\verb|type typ| \\
  \indexmltype{arity}\verb|type arity| \\
  \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: (bstring * int * mixfix) list -> theory -> theory| \\
  \indexml{Sign.add-tyabbrs-i}\verb|Sign.add_tyabbrs_i: |\isasep\isanewline%
\verb|  (bstring * 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}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{c\ {\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|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 a type
  expression of of a given sort.

  \item \verb|Sign.add_types|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ k{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares new
  type constructors \isa{c} with \isa{k} arguments, and
  optional mixfix syntax.

  \item \verb|Sign.add_tyabbrs_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ \isactrlvec {\isasymalpha}{\isacharcomma}\ {\isasymtau}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
  defines type abbreviation \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}c} (with optional
  mixfix syntax) as \isa{{\isasymtau}}.

  \item \verb|Sign.primitive_class|~\isa{{\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub n{\isacharbrackright}{\isacharparenright}} declares new class \isa{c} derived together with
  class relations \isa{c\ {\isasymsubseteq}\ c\isactrlisub i}.

  \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}c{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} declares
  arity \isa{c\ {\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}

  FIXME de-Bruijn representation of lambda terms

  Term syntax provides explicit abstraction \isa{{\isasymlambda}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ b{\isacharparenleft}x{\isacharparenright}}
  and application \isa{t\ u}, while types are usually implicit
  thanks to type-inference.

  Terms of type \isa{prop} are called
  propositions.  Logical statements are composed via \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{A\ {\isasymLongrightarrow}\ B}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME

\glossary{Schematic polymorphism}{FIXME}

\glossary{Type variable}{FIXME}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Proof terms%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Theorems \label{sec:thms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Primitive reasoning operates on judgments of the form \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, with standard introduction and elimination rules for \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} that refer to fixed parameters \isa{x} and
  hypotheses \isa{A} from the context \isa{{\isasymGamma}}.  The
  corresponding proof terms are left implicit in the classic
  ``LCF-approach'', although they could be exploited separately
  \cite{Berghofer-Nipkow:2000}.

  The framework also provides definitional equality \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop}, with \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-conversion rules.  The internal
  conjunction \isa{{\isacharampersand}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} enables the view of
  assumptions and conclusions emerging uniformly as simultaneous
  statements.



  FIXME

\glossary{Proposition}{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}.}

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

\glossary{Fact}{Sometimes used interchangably 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.}

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

\glossary{Free variable}{Synonymous for \seeglossary{fixed variable}.}

\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.}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Primitive inferences%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Higher-order resolution%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME

\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}.}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Equational reasoning%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: