# HG changeset patch
# User wenzelm
# Date 1157978130 -7200
# Node ID 08d227db6c74af1d485ed4b07a5ef3c83d13d902
# Parent  de0b523b0d62e89f5445c4ec9e0a9d3a96bd5f59
updated;

diff -r de0b523b0d62 -r 08d227db6c74 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Mon Sep 11 14:35:25 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Mon Sep 11 14:35:30 2006 +0200
@@ -209,14 +209,13 @@
   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}.
-
 
   \[
-  \infer{\isa{{\isacharparenleft}{\isasymlambda}x\isactrlsub {\isasymtau}{\isachardot}\ t{\isacharparenright}{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}}}{\isa{t{\isacharcolon}\ {\isasymsigma}}}
+  \infer{\isa{a\isactrlisub {\isasymtau}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}}}{}
   \qquad
-  \infer{\isa{{\isacharparenleft}t\ u{\isacharparenright}{\isacharcolon}\ {\isasymsigma}}}{\isa{t{\isacharcolon}\ {\isasymtau}\ {\isasymRightarrow}\ {\isasymsigma}} & \isa{u{\isacharcolon}\ {\isasymtau}}}
+  \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}}}
   \]%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -235,55 +234,60 @@
 \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.
+\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}
 
-
-
-  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{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{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. 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{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{Free variable}{Synonymous for \seeglossary{fixed
+  variable}. FIXME}
+
+  \glossary{Bound variable}{FIXME}
 
-\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{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}
 
-\glossary{Schematic variable}{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:
 
-\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}.}
+  \smallskip
+  \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) \\
+  \end{tabular}
 
-\glossary{Bound variable}{FIXME}
+  \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.
 
-\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.}
-
-
+  \begin{figure}[htb]
+  \begin{center}
   \[
   \infer[\isa{{\isacharparenleft}axiom{\isacharparenright}}]{\isa{{\isasymturnstile}\ A}}{\isa{A\ {\isasymin}\ {\isasymTheta}}}
   \qquad
@@ -299,36 +303,96 @@
   \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}
+  \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.
 
-  Admissible rules:
+  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.
+
+  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 The axiomatization of a theory is implicitly closed by
+  forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymtheta}} for
+  any substirution 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}.
+
+  \begin{figure}[htb]
+  \begin{center}
   \[
-  \infer[\isa{{\isacharparenleft}generalize{\isacharunderscore}type{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} & \isa{{\isasymalpha}\ {\isasymnotin}\ {\isasymGamma}}}
-  \qquad
-  \infer[\isa{{\isacharparenleft}generalize{\isacharunderscore}term{\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}{\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{{\isacharparenleft}instantiate{\isacharunderscore}type{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isasymtau}{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}{\isasymalpha}{\isacharbrackright}}}
-  \qquad
-  \infer[\isa{{\isacharparenleft}instantiate{\isacharunderscore}term{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}t{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}}
+  \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{\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.
-
+  instantiation rule is a genuine admissible one, due to the lack of
+  true polymorphism in the logic.
 
-  Equality and logical equivalence:
+  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.
 
-  \smallskip
+  \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:
+
+  \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 \\
   \end{tabular}
-  \smallskip%
+  \caption{Conceptual axiomatization of equality.}\label{fig:equality}
+  \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.
+
+
+  \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.
+
+  \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 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}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %