# HG changeset patch
# User wenzelm
# Date 1158087939 -7200
# Node ID 189811b398695e85b679f0fc29453ac97db141e1
# Parent  05fd007bdeb912252416b6904c135293fdcdc2d7
more on theorems;

diff -r 05fd007bdeb9 -r 189811b39869 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 12 17:45:58 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 12 21:05:39 2006 +0200
@@ -389,13 +389,13 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\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}. FIXME}
+\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
@@ -424,22 +424,41 @@
   \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}.
-  The connectives of minimal logic are declared as constants of the
-  basic theory:
+  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 are separate (derived)
+  rules for equality/equivalence \isa{{\isasymequiv}} and internal conjunction
+  \isa{{\isacharampersand}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Standard connectives and rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The basic theory is called \isa{Pure}, it contains declarations
+  for the standard logical connectives \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and
+  \isa{{\isasymequiv}} of the 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 syntactic restriction that
+  hypotheses may never contain schematic variables.  The builtin
+  equality is conceptually axiomatized shown in
+  \figref{fig:pure-equality}, although the implementation works
+  directly with (derived) inference rules.
 
-  \smallskip
+  \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}
-
-  \medskip A \emph{theorem} is a proven proposition, depending on a
-  collection of assumptions, and axioms from the theory context.  The
-  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}; there is a global syntactic restriction
-  that the hypotheses may not contain schematic variables.
+  \caption{Standard connectives of Pure}\label{fig:pure-connectives}
+  \end{center}
+  \end{figure}
 
   \begin{figure}[htb]
   \begin{center}
@@ -458,32 +477,51 @@
   \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 the Pure logic}\label{fig:prim-rules}
+  \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\ x{\isacharparenright}\ a\ {\isasymequiv}\ b\ a} & \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} & coincidence with equivalence \\
+  \end{tabular}
+  \caption{Conceptual axiomatization of builtin 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 \emph{irrelevant} in the Pure logic, they may never occur within
-  propositions, i.e.\ the \isa{{\isasymLongrightarrow}} arrow of the framework is a
-  non-dependent one.
+  propositions, i.e.\ the \isa{{\isasymLongrightarrow}} arrow is non-dependent.  The
+  system provides a runtime option to record explicit proof terms for
+  primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus
+  the three-fold \isa{{\isasymlambda}}-structure can be made explicit.
 
-  Also note that fixed parameters as in \isa{{\isasymAnd}{\isacharunderscore}intro} need not be
-  recorded in the context \isa{{\isasymGamma}}, since syntactic types are
-  always inhabitable.  An ``assumption'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} is logically
-  vacuous, because \isa{{\isasymtau}} is always non-empty.  This is the deeper
-  reason why \isa{{\isasymGamma}} only consists of hypothetical proofs, but no
-  hypothetical terms.
+  Observe that locally fixed parameters (as used in rule \isa{{\isasymAnd}{\isacharunderscore}intro}) need not be recorded in the hypotheses, because the
+  simple syntactic types of Pure are always inhabitable.  The typing
+  ``assumption'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} is logically vacuous, it disappears
+  automatically whenever the statement body ceases to mention variable
+  \isa{x\isactrlisub {\isasymtau}}.\footnote{This greatly simplifies many basic
+  reasoning steps, and is the key difference to the formulation of
+  this logic as ``\isa{{\isasymlambda}HOL}'' in the PTS framework
+  \cite{Barendregt-Geuvers:2001}.}
 
-  The corresponding proof terms are left implicit in the classic
-  ``LCF-approach'', although they could be exploited separately
-  \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
-  option to control the generation of full proof terms.
+  \medskip FIXME \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-equivalence and primitive definitions
+
+  Since the basic representation of terms already accounts for \isa{{\isasymalpha}}-conversion, Pure equality essentially acts like \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-equivalence on terms, while coinciding with bi-implication.
 
   \medskip The axiomatization of a theory is implicitly closed by
   forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} for
   any substitution instance of axiom \isa{{\isasymturnstile}\ A}.  By pushing
   substitution through derivations inductively, we get admissible
   substitution rules for theorems shown in \figref{fig:subst-rules}.
+  Alternatively, the term substitution rules could be derived from
+  \isa{{\isasymAnd}{\isacharunderscore}intro{\isacharslash}elim}.  The versions for types are genuine
+  admissible rules, due to the lack of true polymorphism in the logic.
 
   \begin{figure}[htb]
   \begin{center}
@@ -501,56 +539,134 @@
   \end{center}
   \end{figure}
 
-  Note that \isa{instantiate{\isacharunderscore}term} could be derived using \isa{{\isasymAnd}{\isacharunderscore}intro{\isacharslash}elim}, but this is not how it is implemented.  The type
-  instantiation rule is a genuine admissible one, due to the lack of
-  true polymorphism in the logic.
-
   Since \isa{{\isasymGamma}} may never contain any schematic variables, the
   \isa{instantiate} do not require an explicit side-condition.  In
   principle, variables could be substituted in hypotheses as well, but
   this could disrupt monotonicity of the basic calculus: derivations
-  could leave the current proof context.
+  could leave the current proof context.%
+\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| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|ctyp| FIXME
 
-  \medskip The framework also provides builtin equality \isa{{\isasymequiv}},
-  which is conceptually axiomatized shown in \figref{fig:equality},
-  although the implementation provides derived rules directly:
+  \item \verb|cterm| FIXME
+
+  \item \verb|thm| FIXME
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Auxiliary connectives%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Pure also provides various auxiliary connectives based on primitive
+  definitions, 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{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\
-  \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b\ x{\isacharparenright}\ a\ {\isasymequiv}\ b\ a} & \isa{{\isasymbeta}}-conversion \\
-  \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity law \\
-  \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution law \\
-  \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} & coincidence with equivalence \\
+  \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}}) \\
+  \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{Conceptual axiomatization of equality.}\label{fig:equality}
+  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   \end{center}
   \end{figure}
 
-  Since the basic representation of terms already accounts for \isa{{\isasymalpha}}-conversion, Pure equality essentially acts like \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-equivalence on terms, while coinciding with bi-implication.
-
+  Conjunction as an explicit connective allows to treat both
+  simultaneous assumptions and conclusions uniformly.  The definition
+  allows to derive the usual introduction \isa{{\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B},
+  and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.  For
+  example, several claims may be stated at the same time, which is
+  intermediately represented as an assumption, but the user only
+  encounters several sub-goals, and several resulting facts in the
+  very end (cf.\ \secref{sec:tactical-goals}).
 
-  \medskip Conjunction is defined in Pure as a derived connective, see
-  \figref{fig:conjunction}.  This is occasionally useful to represent
-  simultaneous statements behind the scenes --- framework conjunction
-  is usually not exposed to the user.
+  The \isa{{\isacharhash}} marker allows complex propositions (nested \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}) to appear formally 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.
 
-  \begin{figure}[htb]
-  \begin{center}
-  \begin{tabular}{ll}
-  \isa{{\isacharampersand}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & conjunction (hidden) \\
-  \isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\
-  \end{tabular}
-  \caption{Definition of conjunction.}\label{fig:equality}
-  \end{center}
-  \end{figure}
+  The \isa{TERM} marker turns any well-formed term into a
+  derivable proposition: \isa{{\isasymturnstile}\ TERM\ t} holds
+  unconditionally.  Despite its logically vacous meaning, this is
+  occasionally useful to treat syntactic terms and proven propositions
+  uniformly, as in a type-theoretic framework.
 
-  The definition allows to derive the usual introduction \isa{{\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B}, and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.%
+  The \isa{TYPE} constructor (which is the canonical
+  representative of the unspecified type \isa{{\isasymalpha}\ itself}) injects
+  the language of types into that of terms.  There is specific
+  notation \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }.
+  Although being devoid of any particular meaning, the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} is able to carry the type \isa{{\isasymtau}} formally.  \isa{TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}} may be used as an additional formal argument in primitive
+  definitions, in order to avoid hidden polymorphism (cf.\
+  \secref{sec:terms}).  For example, \isa{c\ TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}\ {\isasymequiv}\ A{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} turns
+  out as a formally correct definition of some proposition \isa{A}
+  that depends on an additional type argument.%
 \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 FIXME
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
 \isamarkupsection{Rules \label{sec:rules}%
 }
 \isamarkuptrue%
diff -r 05fd007bdeb9 -r 189811b39869 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:45:58 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 21:05:39 2006 +0200
@@ -384,13 +384,14 @@
 section {* Theorems \label{sec:thms} *}
 
 text {*
-  \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
-  @{text "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
-  @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---
-  anything else is considered atomic.  The canonical form for
-  propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}
+  \glossary{Proposition}{FIXME A \seeglossary{term} of
+  \seeglossary{type} @{text "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 @{text "A \<Longrightarrow> B"} or universal quantification @{text
+  "\<And>x. 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 @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
@@ -419,22 +420,39 @@
   \seeglossary{type variable}.  The distinguishing feature of
   different variables is their binding scope. FIXME}
 
-  A \emph{proposition} is a well-formed term of type @{text "prop"}.
-  The connectives of minimal logic are declared as constants of the
-  basic theory:
+  A \emph{proposition} is a well-formed term of type @{text "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 @{text
+  "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There are separate (derived)
+  rules for equality/equivalence @{text "\<equiv>"} and internal conjunction
+  @{text "&"}.
+*}
+
+subsection {* Standard connectives and rules *}
 
-  \smallskip
+text {*
+  The basic theory is called @{text "Pure"}, it contains declarations
+  for the standard logical connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and
+  @{text "\<equiv>"} of the framework, see \figref{fig:pure-connectives}.
+  The derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
+  defined inductively by the primitive inferences given in
+  \figref{fig:prim-rules}, with the global syntactic restriction that
+  hypotheses may never contain schematic variables.  The builtin
+  equality is conceptually axiomatized shown in
+  \figref{fig:pure-equality}, although the implementation works
+  directly with (derived) inference rules.
+
+  \begin{figure}[htb]
+  \begin{center}
   \begin{tabular}{ll}
   @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
   @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
+  @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   \end{tabular}
-
-  \medskip A \emph{theorem} is a proven proposition, depending on a
-  collection of assumptions, and axioms from the theory context.  The
-  judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined
-  inductively by the primitive inferences given in
-  \figref{fig:prim-rules}; there is a global syntactic restriction
-  that the hypotheses may not contain schematic variables.
+  \caption{Standard connectives of Pure}\label{fig:pure-connectives}
+  \end{center}
+  \end{figure}
 
   \begin{figure}[htb]
   \begin{center}
@@ -453,7 +471,20 @@
   \qquad
   \infer[@{text "(\<Longrightarrow>_elim)"}]{@{text "\<Gamma>\<^sub>1 \<union> \<Gamma>\<^sub>2 \<turnstile> B"}}{@{text "\<Gamma>\<^sub>1 \<turnstile> A \<Longrightarrow> B"} & @{text "\<Gamma>\<^sub>2 \<turnstile> A"}}
   \]
-  \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}
+  \caption{Primitive inferences of Pure}\label{fig:prim-rules}
+  \end{center}
+  \end{figure}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \begin{tabular}{ll}
+  @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
+  @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
+  @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
+  @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
+  @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
+  \end{tabular}
+  \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}
   \end{center}
   \end{figure}
 
@@ -461,26 +492,35 @@
   "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
   "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   are \emph{irrelevant} in the Pure logic, they may never occur within
-  propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a
-  non-dependent one.
+  propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow is non-dependent.  The
+  system provides a runtime option to record explicit proof terms for
+  primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus
+  the three-fold @{text "\<lambda>"}-structure can be made explicit.
 
-  Also note that fixed parameters as in @{text "\<And>_intro"} need not be
-  recorded in the context @{text "\<Gamma>"}, since syntactic types are
-  always inhabitable.  An ``assumption'' @{text "x :: \<tau>"} is logically
-  vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper
-  reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no
-  hypothetical terms.
+  Observe that locally fixed parameters (as used in rule @{text
+  "\<And>_intro"}) need not be recorded in the hypotheses, because the
+  simple syntactic types of Pure are always inhabitable.  The typing
+  ``assumption'' @{text "x :: \<tau>"} is logically vacuous, it disappears
+  automatically whenever the statement body ceases to mention variable
+  @{text "x\<^isub>\<tau>"}.\footnote{This greatly simplifies many basic
+  reasoning steps, and is the key difference to the formulation of
+  this logic as ``@{text "\<lambda>HOL"}'' in the PTS framework
+  \cite{Barendregt-Geuvers:2001}.}
 
-  The corresponding proof terms are left implicit in the classic
-  ``LCF-approach'', although they could be exploited separately
-  \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
-  option to control the generation of full proof terms.
+  \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions
+
+  Since the basic representation of terms already accounts for @{text
+  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
+  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
 
   \medskip The axiomatization of a theory is implicitly closed by
   forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
   any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
   substitution through derivations inductively, we get admissible
   substitution rules for theorems shown in \figref{fig:subst-rules}.
+  Alternatively, the term substitution rules could be derived from
+  @{text "\<And>_intro/elim"}.  The versions for types are genuine
+  admissible rules, due to the lack of true polymorphism in the logic.
 
   \begin{figure}[htb]
   \begin{center}
@@ -498,58 +538,105 @@
   \end{center}
   \end{figure}
 
-  Note that @{text "instantiate_term"} could be derived using @{text
-  "\<And>_intro/elim"}, but this is not how it is implemented.  The type
-  instantiation rule is a genuine admissible one, due to the lack of
-  true polymorphism in the logic.
-
   Since @{text "\<Gamma>"} may never contain any schematic variables, the
   @{text "instantiate"} do not require an explicit side-condition.  In
   principle, variables could be substituted in hypotheses as well, but
   this could disrupt monotonicity of the basic calculus: derivations
   could leave the current proof context.
+*}
 
-  \medskip The framework also provides builtin equality @{text "\<equiv>"},
-  which is conceptually axiomatized shown in \figref{fig:equality},
-  although the implementation provides derived rules directly:
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_type ctyp} \\
+  @{index_ML_type cterm} \\
+  @{index_ML_type thm} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML_type ctyp} FIXME
+
+  \item @{ML_type cterm} FIXME
+
+  \item @{ML_type thm} FIXME
+
+  \end{description}
+*}
+
+
+subsection {* Auxiliary connectives *}
+
+text {*
+  Pure also provides various auxiliary connectives based on primitive
+  definitions, 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}
-  @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
-  @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
-  @{text "\<turnstile> x \<equiv> x"} & reflexivity law \\
-  @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\
-  @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
-  @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
+  @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
+  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
+  @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}) \\
+  @{text "#A \<equiv> A"} \\[1ex]
+  @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
+  @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
+  @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
+  @{text "(unspecified)"} \\
   \end{tabular}
-  \caption{Conceptual axiomatization of equality.}\label{fig:equality}
+  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   \end{center}
   \end{figure}
 
-  Since the basic representation of terms already accounts for @{text
-  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
-  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
-
+  Conjunction as an explicit connective allows to treat both
+  simultaneous assumptions and conclusions uniformly.  The definition
+  allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow> B \<Longrightarrow> A & B"},
+  and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.  For
+  example, several claims may be stated at the same time, which is
+  intermediately represented as an assumption, but the user only
+  encounters several sub-goals, and several resulting facts in the
+  very end (cf.\ \secref{sec:tactical-goals}).
 
-  \medskip Conjunction is defined in Pure as a derived connective, see
-  \figref{fig:conjunction}.  This is occasionally useful to represent
-  simultaneous statements behind the scenes --- framework conjunction
-  is usually not exposed to the user.
+  The @{text "#"} marker allows complex propositions (nested @{text
+  "\<And>"} and @{text "\<Longrightarrow>"}) to appear formally as atomic, without changing
+  the meaning: @{text "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are
+  interchangeable.  See \secref{sec:tactical-goals} for specific
+  operations.
+
+  The @{text "TERM"} marker turns any well-formed term into a
+  derivable proposition: @{text "\<turnstile> TERM t"} holds
+  unconditionally.  Despite its logically vacous meaning, this is
+  occasionally useful to treat syntactic terms and proven propositions
+  uniformly, as in a type-theoretic framework.
 
-  \begin{figure}[htb]
-  \begin{center}
-  \begin{tabular}{ll}
-  @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\
-  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\
-  \end{tabular}
-  \caption{Definition of conjunction.}\label{fig:equality}
-  \end{center}
-  \end{figure}
+  The @{text "TYPE"} constructor (which is the canonical
+  representative of the unspecified type @{text "\<alpha> itself"}) injects
+  the language of types into that of terms.  There is specific
+  notation @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
+ itself\<^esub>"}.
+  Although being devoid of any particular meaning, the term @{text
+  "TYPE(\<tau>)"} is able to carry the type @{text "\<tau>"} formally.  @{text
+  "TYPE(\<alpha>)"} may be used as an additional formal argument in primitive
+  definitions, in order to avoid hidden polymorphism (cf.\
+  \secref{sec:terms}).  For example, @{text "c TYPE(\<alpha>) \<equiv> A[\<alpha>]"} turns
+  out as a formally correct definition of some proposition @{text "A"}
+  that depends on an additional type argument.
+*}
 
-  The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>
-  B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B
-  \<Longrightarrow> B"}.
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
+  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
+  @{index_ML Drule.mk_term: "cterm -> thm"} \\
+  @{index_ML Drule.dest_term: "thm -> cterm"} \\
+  @{index_ML Logic.mk_type: "typ -> term"} \\
+  @{index_ML Logic.dest_type: "term -> typ"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item FIXME
+
+  \end{description}
 *}