more on theorems;
authorwenzelm
Tue Sep 12 21:05:39 2006 +0200 (2006-09-12)
changeset 20521189811b39869
parent 20520 05fd007bdeb9
child 20522 05072ae0d435
more on theorems;
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/logic.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 12 17:45:58 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Tue Sep 12 21:05:39 2006 +0200
     1.3 @@ -389,13 +389,13 @@
     1.4  \isamarkuptrue%
     1.5  %
     1.6  \begin{isamarkuptext}%
     1.7 -\glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
     1.8 -  \isa{prop}.  Internally, there is nothing special about
     1.9 -  propositions apart from their type, but the concrete syntax enforces
    1.10 -  a clear distinction.  Propositions are structured via implication
    1.11 -  \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} ---
    1.12 -  anything else is considered atomic.  The canonical form for
    1.13 -  propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}
    1.14 +\glossary{Proposition}{FIXME A \seeglossary{term} of
    1.15 +  \seeglossary{type} \isa{prop}.  Internally, there is nothing
    1.16 +  special about propositions apart from their type, but the concrete
    1.17 +  syntax enforces a clear distinction.  Propositions are structured
    1.18 +  via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything else is considered atomic.  The canonical
    1.19 +  form for propositions is that of a \seeglossary{Hereditary Harrop
    1.20 +  Formula}. FIXME}
    1.21  
    1.22    \glossary{Theorem}{A proven proposition within a certain theory and
    1.23    proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
    1.24 @@ -424,22 +424,41 @@
    1.25    \seeglossary{type variable}.  The distinguishing feature of
    1.26    different variables is their binding scope. FIXME}
    1.27  
    1.28 -  A \emph{proposition} is a well-formed term of type \isa{prop}.
    1.29 -  The connectives of minimal logic are declared as constants of the
    1.30 -  basic theory:
    1.31 +  A \emph{proposition} is a well-formed term of type \isa{prop}, a
    1.32 +  \emph{theorem} is a proven proposition (depending on a context of
    1.33 +  hypotheses and the background theory).  Primitive inferences include
    1.34 +  plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework.  There are separate (derived)
    1.35 +  rules for equality/equivalence \isa{{\isasymequiv}} and internal conjunction
    1.36 +  \isa{{\isacharampersand}}.%
    1.37 +\end{isamarkuptext}%
    1.38 +\isamarkuptrue%
    1.39 +%
    1.40 +\isamarkupsubsection{Standard connectives and rules%
    1.41 +}
    1.42 +\isamarkuptrue%
    1.43 +%
    1.44 +\begin{isamarkuptext}%
    1.45 +The basic theory is called \isa{Pure}, it contains declarations
    1.46 +  for the standard logical connectives \isa{{\isasymAnd}}, \isa{{\isasymLongrightarrow}}, and
    1.47 +  \isa{{\isasymequiv}} of the framework, see \figref{fig:pure-connectives}.
    1.48 +  The derivability judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is
    1.49 +  defined inductively by the primitive inferences given in
    1.50 +  \figref{fig:prim-rules}, with the global syntactic restriction that
    1.51 +  hypotheses may never contain schematic variables.  The builtin
    1.52 +  equality is conceptually axiomatized shown in
    1.53 +  \figref{fig:pure-equality}, although the implementation works
    1.54 +  directly with (derived) inference rules.
    1.55  
    1.56 -  \smallskip
    1.57 +  \begin{figure}[htb]
    1.58 +  \begin{center}
    1.59    \begin{tabular}{ll}
    1.60    \isa{all\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymRightarrow}\ prop{\isacharparenright}\ {\isasymRightarrow}\ prop} & universal quantification (binder \isa{{\isasymAnd}}) \\
    1.61    \isa{{\isasymLongrightarrow}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & implication (right associative infix) \\
    1.62 +  \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\
    1.63    \end{tabular}
    1.64 -
    1.65 -  \medskip A \emph{theorem} is a proven proposition, depending on a
    1.66 -  collection of assumptions, and axioms from the theory context.  The
    1.67 -  judgment \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} is defined
    1.68 -  inductively by the primitive inferences given in
    1.69 -  \figref{fig:prim-rules}; there is a global syntactic restriction
    1.70 -  that the hypotheses may not contain schematic variables.
    1.71 +  \caption{Standard connectives of Pure}\label{fig:pure-connectives}
    1.72 +  \end{center}
    1.73 +  \end{figure}
    1.74  
    1.75    \begin{figure}[htb]
    1.76    \begin{center}
    1.77 @@ -458,32 +477,51 @@
    1.78    \qquad
    1.79    \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}}
    1.80    \]
    1.81 -  \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}
    1.82 +  \caption{Primitive inferences of Pure}\label{fig:prim-rules}
    1.83 +  \end{center}
    1.84 +  \end{figure}
    1.85 +
    1.86 +  \begin{figure}[htb]
    1.87 +  \begin{center}
    1.88 +  \begin{tabular}{ll}
    1.89 +  \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b\ x{\isacharparenright}\ a\ {\isasymequiv}\ b\ a} & \isa{{\isasymbeta}}-conversion \\
    1.90 +  \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity \\
    1.91 +  \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution \\
    1.92 +  \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\
    1.93 +  \isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & coincidence with equivalence \\
    1.94 +  \end{tabular}
    1.95 +  \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}
    1.96    \end{center}
    1.97    \end{figure}
    1.98  
    1.99    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
   1.100    are \emph{irrelevant} in the Pure logic, they may never occur within
   1.101 -  propositions, i.e.\ the \isa{{\isasymLongrightarrow}} arrow of the framework is a
   1.102 -  non-dependent one.
   1.103 +  propositions, i.e.\ the \isa{{\isasymLongrightarrow}} arrow is non-dependent.  The
   1.104 +  system provides a runtime option to record explicit proof terms for
   1.105 +  primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus
   1.106 +  the three-fold \isa{{\isasymlambda}}-structure can be made explicit.
   1.107  
   1.108 -  Also note that fixed parameters as in \isa{{\isasymAnd}{\isacharunderscore}intro} need not be
   1.109 -  recorded in the context \isa{{\isasymGamma}}, since syntactic types are
   1.110 -  always inhabitable.  An ``assumption'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} is logically
   1.111 -  vacuous, because \isa{{\isasymtau}} is always non-empty.  This is the deeper
   1.112 -  reason why \isa{{\isasymGamma}} only consists of hypothetical proofs, but no
   1.113 -  hypothetical terms.
   1.114 +  Observe that locally fixed parameters (as used in rule \isa{{\isasymAnd}{\isacharunderscore}intro}) need not be recorded in the hypotheses, because the
   1.115 +  simple syntactic types of Pure are always inhabitable.  The typing
   1.116 +  ``assumption'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} is logically vacuous, it disappears
   1.117 +  automatically whenever the statement body ceases to mention variable
   1.118 +  \isa{x\isactrlisub {\isasymtau}}.\footnote{This greatly simplifies many basic
   1.119 +  reasoning steps, and is the key difference to the formulation of
   1.120 +  this logic as ``\isa{{\isasymlambda}HOL}'' in the PTS framework
   1.121 +  \cite{Barendregt-Geuvers:2001}.}
   1.122  
   1.123 -  The corresponding proof terms are left implicit in the classic
   1.124 -  ``LCF-approach'', although they could be exploited separately
   1.125 -  \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
   1.126 -  option to control the generation of full proof terms.
   1.127 +  \medskip FIXME \isa{{\isasymalpha}{\isasymbeta}{\isasymeta}}-equivalence and primitive definitions
   1.128 +
   1.129 +  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.
   1.130  
   1.131    \medskip The axiomatization of a theory is implicitly closed by
   1.132    forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} for
   1.133    any substitution instance of axiom \isa{{\isasymturnstile}\ A}.  By pushing
   1.134    substitution through derivations inductively, we get admissible
   1.135    substitution rules for theorems shown in \figref{fig:subst-rules}.
   1.136 +  Alternatively, the term substitution rules could be derived from
   1.137 +  \isa{{\isasymAnd}{\isacharunderscore}intro{\isacharslash}elim}.  The versions for types are genuine
   1.138 +  admissible rules, due to the lack of true polymorphism in the logic.
   1.139  
   1.140    \begin{figure}[htb]
   1.141    \begin{center}
   1.142 @@ -501,56 +539,134 @@
   1.143    \end{center}
   1.144    \end{figure}
   1.145  
   1.146 -  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
   1.147 -  instantiation rule is a genuine admissible one, due to the lack of
   1.148 -  true polymorphism in the logic.
   1.149 -
   1.150    Since \isa{{\isasymGamma}} may never contain any schematic variables, the
   1.151    \isa{instantiate} do not require an explicit side-condition.  In
   1.152    principle, variables could be substituted in hypotheses as well, but
   1.153    this could disrupt monotonicity of the basic calculus: derivations
   1.154 -  could leave the current proof context.
   1.155 +  could leave the current proof context.%
   1.156 +\end{isamarkuptext}%
   1.157 +\isamarkuptrue%
   1.158 +%
   1.159 +\isadelimmlref
   1.160 +%
   1.161 +\endisadelimmlref
   1.162 +%
   1.163 +\isatagmlref
   1.164 +%
   1.165 +\begin{isamarkuptext}%
   1.166 +\begin{mldecls}
   1.167 +  \indexmltype{ctyp}\verb|type ctyp| \\
   1.168 +  \indexmltype{cterm}\verb|type cterm| \\
   1.169 +  \indexmltype{thm}\verb|type thm| \\
   1.170 +  \end{mldecls}
   1.171 +
   1.172 +  \begin{description}
   1.173 +
   1.174 +  \item \verb|ctyp| FIXME
   1.175  
   1.176 -  \medskip The framework also provides builtin equality \isa{{\isasymequiv}},
   1.177 -  which is conceptually axiomatized shown in \figref{fig:equality},
   1.178 -  although the implementation provides derived rules directly:
   1.179 +  \item \verb|cterm| FIXME
   1.180 +
   1.181 +  \item \verb|thm| FIXME
   1.182 +
   1.183 +  \end{description}%
   1.184 +\end{isamarkuptext}%
   1.185 +\isamarkuptrue%
   1.186 +%
   1.187 +\endisatagmlref
   1.188 +{\isafoldmlref}%
   1.189 +%
   1.190 +\isadelimmlref
   1.191 +%
   1.192 +\endisadelimmlref
   1.193 +%
   1.194 +\isamarkupsubsection{Auxiliary connectives%
   1.195 +}
   1.196 +\isamarkuptrue%
   1.197 +%
   1.198 +\begin{isamarkuptext}%
   1.199 +Pure also provides various auxiliary connectives based on primitive
   1.200 +  definitions, see \figref{fig:pure-aux}.  These are normally not
   1.201 +  exposed to the user, but appear in internal encodings only.
   1.202  
   1.203    \begin{figure}[htb]
   1.204    \begin{center}
   1.205    \begin{tabular}{ll}
   1.206 -  \isa{{\isasymequiv}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & equality relation (infix) \\
   1.207 -  \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ b\ x{\isacharparenright}\ a\ {\isasymequiv}\ b\ a} & \isa{{\isasymbeta}}-conversion \\
   1.208 -  \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ x} & reflexivity law \\
   1.209 -  \isa{{\isasymturnstile}\ x\ {\isasymequiv}\ y\ {\isasymLongrightarrow}\ P\ x\ {\isasymLongrightarrow}\ P\ y} & substitution law \\
   1.210 -  \isa{{\isasymturnstile}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ f\ x\ {\isasymequiv}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\ f\ {\isasymequiv}\ g} & extensionality \\
   1.211 -  \isa{{\isasymturnstile}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymequiv}\ B} & coincidence with equivalence \\
   1.212 +  \isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}}) \\
   1.213 +  \isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\[1ex]
   1.214 +  \isa{prop\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop} & (prefix \isa{{\isacharhash}}) \\
   1.215 +  \isa{{\isacharhash}A\ {\isasymequiv}\ A} \\[1ex]
   1.216 +  \isa{term\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & (prefix \isa{TERM}) \\
   1.217 +  \isa{term\ x\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}A{\isachardot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}} \\[1ex]
   1.218 +  \isa{TYPE\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself} & (prefix \isa{TYPE}) \\
   1.219 +  \isa{{\isacharparenleft}unspecified{\isacharparenright}} \\
   1.220    \end{tabular}
   1.221 -  \caption{Conceptual axiomatization of equality.}\label{fig:equality}
   1.222 +  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   1.223    \end{center}
   1.224    \end{figure}
   1.225  
   1.226 -  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.
   1.227 -
   1.228 +  Conjunction as an explicit connective allows to treat both
   1.229 +  simultaneous assumptions and conclusions uniformly.  The definition
   1.230 +  allows to derive the usual introduction \isa{{\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B},
   1.231 +  and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.  For
   1.232 +  example, several claims may be stated at the same time, which is
   1.233 +  intermediately represented as an assumption, but the user only
   1.234 +  encounters several sub-goals, and several resulting facts in the
   1.235 +  very end (cf.\ \secref{sec:tactical-goals}).
   1.236  
   1.237 -  \medskip Conjunction is defined in Pure as a derived connective, see
   1.238 -  \figref{fig:conjunction}.  This is occasionally useful to represent
   1.239 -  simultaneous statements behind the scenes --- framework conjunction
   1.240 -  is usually not exposed to the user.
   1.241 +  The \isa{{\isacharhash}} marker allows complex propositions (nested \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}}) to appear formally as atomic, without changing
   1.242 +  the meaning: \isa{{\isasymGamma}\ {\isasymturnstile}\ A} and \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isacharhash}A} are
   1.243 +  interchangeable.  See \secref{sec:tactical-goals} for specific
   1.244 +  operations.
   1.245  
   1.246 -  \begin{figure}[htb]
   1.247 -  \begin{center}
   1.248 -  \begin{tabular}{ll}
   1.249 -  \isa{{\isacharampersand}\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & conjunction (hidden) \\
   1.250 -  \isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\
   1.251 -  \end{tabular}
   1.252 -  \caption{Definition of conjunction.}\label{fig:equality}
   1.253 -  \end{center}
   1.254 -  \end{figure}
   1.255 +  The \isa{TERM} marker turns any well-formed term into a
   1.256 +  derivable proposition: \isa{{\isasymturnstile}\ TERM\ t} holds
   1.257 +  unconditionally.  Despite its logically vacous meaning, this is
   1.258 +  occasionally useful to treat syntactic terms and proven propositions
   1.259 +  uniformly, as in a type-theoretic framework.
   1.260  
   1.261 -  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}.%
   1.262 +  The \isa{TYPE} constructor (which is the canonical
   1.263 +  representative of the unspecified type \isa{{\isasymalpha}\ itself}) injects
   1.264 +  the language of types into that of terms.  There is specific
   1.265 +  notation \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }.
   1.266 +  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
   1.267 +  definitions, in order to avoid hidden polymorphism (cf.\
   1.268 +  \secref{sec:terms}).  For example, \isa{c\ TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}\ {\isasymequiv}\ A{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} turns
   1.269 +  out as a formally correct definition of some proposition \isa{A}
   1.270 +  that depends on an additional type argument.%
   1.271  \end{isamarkuptext}%
   1.272  \isamarkuptrue%
   1.273  %
   1.274 +\isadelimmlref
   1.275 +%
   1.276 +\endisadelimmlref
   1.277 +%
   1.278 +\isatagmlref
   1.279 +%
   1.280 +\begin{isamarkuptext}%
   1.281 +\begin{mldecls}
   1.282 +  \indexml{Conjunction.intr}\verb|Conjunction.intr: thm -> thm -> thm| \\
   1.283 +  \indexml{Conjunction.elim}\verb|Conjunction.elim: thm -> thm * thm| \\
   1.284 +  \indexml{Drule.mk-term}\verb|Drule.mk_term: cterm -> thm| \\
   1.285 +  \indexml{Drule.dest-term}\verb|Drule.dest_term: thm -> cterm| \\
   1.286 +  \indexml{Logic.mk-type}\verb|Logic.mk_type: typ -> term| \\
   1.287 +  \indexml{Logic.dest-type}\verb|Logic.dest_type: term -> typ| \\
   1.288 +  \end{mldecls}
   1.289 +
   1.290 +  \begin{description}
   1.291 +
   1.292 +  \item FIXME
   1.293 +
   1.294 +  \end{description}%
   1.295 +\end{isamarkuptext}%
   1.296 +\isamarkuptrue%
   1.297 +%
   1.298 +\endisatagmlref
   1.299 +{\isafoldmlref}%
   1.300 +%
   1.301 +\isadelimmlref
   1.302 +%
   1.303 +\endisadelimmlref
   1.304 +%
   1.305  \isamarkupsection{Rules \label{sec:rules}%
   1.306  }
   1.307  \isamarkuptrue%
     2.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 17:45:58 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Tue Sep 12 21:05:39 2006 +0200
     2.3 @@ -384,13 +384,14 @@
     2.4  section {* Theorems \label{sec:thms} *}
     2.5  
     2.6  text {*
     2.7 -  \glossary{Proposition}{A \seeglossary{term} of \seeglossary{type}
     2.8 -  @{text "prop"}.  Internally, there is nothing special about
     2.9 -  propositions apart from their type, but the concrete syntax enforces
    2.10 -  a clear distinction.  Propositions are structured via implication
    2.11 -  @{text "A \<Longrightarrow> B"} or universal quantification @{text "\<And>x. B x"} ---
    2.12 -  anything else is considered atomic.  The canonical form for
    2.13 -  propositions is that of a \seeglossary{Hereditary Harrop Formula}. FIXME}
    2.14 +  \glossary{Proposition}{FIXME A \seeglossary{term} of
    2.15 +  \seeglossary{type} @{text "prop"}.  Internally, there is nothing
    2.16 +  special about propositions apart from their type, but the concrete
    2.17 +  syntax enforces a clear distinction.  Propositions are structured
    2.18 +  via implication @{text "A \<Longrightarrow> B"} or universal quantification @{text
    2.19 +  "\<And>x. B x"} --- anything else is considered atomic.  The canonical
    2.20 +  form for propositions is that of a \seeglossary{Hereditary Harrop
    2.21 +  Formula}. FIXME}
    2.22  
    2.23    \glossary{Theorem}{A proven proposition within a certain theory and
    2.24    proof context, formally @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}; both contexts are
    2.25 @@ -419,22 +420,39 @@
    2.26    \seeglossary{type variable}.  The distinguishing feature of
    2.27    different variables is their binding scope. FIXME}
    2.28  
    2.29 -  A \emph{proposition} is a well-formed term of type @{text "prop"}.
    2.30 -  The connectives of minimal logic are declared as constants of the
    2.31 -  basic theory:
    2.32 +  A \emph{proposition} is a well-formed term of type @{text "prop"}, a
    2.33 +  \emph{theorem} is a proven proposition (depending on a context of
    2.34 +  hypotheses and the background theory).  Primitive inferences include
    2.35 +  plain natural deduction rules for the primary connectives @{text
    2.36 +  "\<And>"} and @{text "\<Longrightarrow>"} of the framework.  There are separate (derived)
    2.37 +  rules for equality/equivalence @{text "\<equiv>"} and internal conjunction
    2.38 +  @{text "&"}.
    2.39 +*}
    2.40 +
    2.41 +subsection {* Standard connectives and rules *}
    2.42  
    2.43 -  \smallskip
    2.44 +text {*
    2.45 +  The basic theory is called @{text "Pure"}, it contains declarations
    2.46 +  for the standard logical connectives @{text "\<And>"}, @{text "\<Longrightarrow>"}, and
    2.47 +  @{text "\<equiv>"} of the framework, see \figref{fig:pure-connectives}.
    2.48 +  The derivability judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is
    2.49 +  defined inductively by the primitive inferences given in
    2.50 +  \figref{fig:prim-rules}, with the global syntactic restriction that
    2.51 +  hypotheses may never contain schematic variables.  The builtin
    2.52 +  equality is conceptually axiomatized shown in
    2.53 +  \figref{fig:pure-equality}, although the implementation works
    2.54 +  directly with (derived) inference rules.
    2.55 +
    2.56 +  \begin{figure}[htb]
    2.57 +  \begin{center}
    2.58    \begin{tabular}{ll}
    2.59    @{text "all :: (\<alpha> \<Rightarrow> prop) \<Rightarrow> prop"} & universal quantification (binder @{text "\<And>"}) \\
    2.60    @{text "\<Longrightarrow> :: prop \<Rightarrow> prop \<Rightarrow> prop"} & implication (right associative infix) \\
    2.61 +  @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
    2.62    \end{tabular}
    2.63 -
    2.64 -  \medskip A \emph{theorem} is a proven proposition, depending on a
    2.65 -  collection of assumptions, and axioms from the theory context.  The
    2.66 -  judgment @{text "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} is defined
    2.67 -  inductively by the primitive inferences given in
    2.68 -  \figref{fig:prim-rules}; there is a global syntactic restriction
    2.69 -  that the hypotheses may not contain schematic variables.
    2.70 +  \caption{Standard connectives of Pure}\label{fig:pure-connectives}
    2.71 +  \end{center}
    2.72 +  \end{figure}
    2.73  
    2.74    \begin{figure}[htb]
    2.75    \begin{center}
    2.76 @@ -453,7 +471,20 @@
    2.77    \qquad
    2.78    \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"}}
    2.79    \]
    2.80 -  \caption{Primitive inferences of the Pure logic}\label{fig:prim-rules}
    2.81 +  \caption{Primitive inferences of Pure}\label{fig:prim-rules}
    2.82 +  \end{center}
    2.83 +  \end{figure}
    2.84 +
    2.85 +  \begin{figure}[htb]
    2.86 +  \begin{center}
    2.87 +  \begin{tabular}{ll}
    2.88 +  @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
    2.89 +  @{text "\<turnstile> x \<equiv> x"} & reflexivity \\
    2.90 +  @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution \\
    2.91 +  @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
    2.92 +  @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
    2.93 +  \end{tabular}
    2.94 +  \caption{Conceptual axiomatization of builtin equality}\label{fig:pure-equality}
    2.95    \end{center}
    2.96    \end{figure}
    2.97  
    2.98 @@ -461,26 +492,35 @@
    2.99    "\<Longrightarrow>"} are analogous to formation of (dependently typed) @{text
   2.100    "\<lambda>"}-terms representing the underlying proof objects.  Proof terms
   2.101    are \emph{irrelevant} in the Pure logic, they may never occur within
   2.102 -  propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow of the framework is a
   2.103 -  non-dependent one.
   2.104 +  propositions, i.e.\ the @{text "\<Longrightarrow>"} arrow is non-dependent.  The
   2.105 +  system provides a runtime option to record explicit proof terms for
   2.106 +  primitive inferences, cf.\ \cite{Berghofer-Nipkow:2000:TPHOL}.  Thus
   2.107 +  the three-fold @{text "\<lambda>"}-structure can be made explicit.
   2.108  
   2.109 -  Also note that fixed parameters as in @{text "\<And>_intro"} need not be
   2.110 -  recorded in the context @{text "\<Gamma>"}, since syntactic types are
   2.111 -  always inhabitable.  An ``assumption'' @{text "x :: \<tau>"} is logically
   2.112 -  vacuous, because @{text "\<tau>"} is always non-empty.  This is the deeper
   2.113 -  reason why @{text "\<Gamma>"} only consists of hypothetical proofs, but no
   2.114 -  hypothetical terms.
   2.115 +  Observe that locally fixed parameters (as used in rule @{text
   2.116 +  "\<And>_intro"}) need not be recorded in the hypotheses, because the
   2.117 +  simple syntactic types of Pure are always inhabitable.  The typing
   2.118 +  ``assumption'' @{text "x :: \<tau>"} is logically vacuous, it disappears
   2.119 +  automatically whenever the statement body ceases to mention variable
   2.120 +  @{text "x\<^isub>\<tau>"}.\footnote{This greatly simplifies many basic
   2.121 +  reasoning steps, and is the key difference to the formulation of
   2.122 +  this logic as ``@{text "\<lambda>HOL"}'' in the PTS framework
   2.123 +  \cite{Barendregt-Geuvers:2001}.}
   2.124  
   2.125 -  The corresponding proof terms are left implicit in the classic
   2.126 -  ``LCF-approach'', although they could be exploited separately
   2.127 -  \cite{Berghofer-Nipkow:2000}.  The implementation provides a runtime
   2.128 -  option to control the generation of full proof terms.
   2.129 +  \medskip FIXME @{text "\<alpha>\<beta>\<eta>"}-equivalence and primitive definitions
   2.130 +
   2.131 +  Since the basic representation of terms already accounts for @{text
   2.132 +  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
   2.133 +  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
   2.134  
   2.135    \medskip The axiomatization of a theory is implicitly closed by
   2.136    forming all instances of type and term variables: @{text "\<turnstile> A\<vartheta>"} for
   2.137    any substitution instance of axiom @{text "\<turnstile> A"}.  By pushing
   2.138    substitution through derivations inductively, we get admissible
   2.139    substitution rules for theorems shown in \figref{fig:subst-rules}.
   2.140 +  Alternatively, the term substitution rules could be derived from
   2.141 +  @{text "\<And>_intro/elim"}.  The versions for types are genuine
   2.142 +  admissible rules, due to the lack of true polymorphism in the logic.
   2.143  
   2.144    \begin{figure}[htb]
   2.145    \begin{center}
   2.146 @@ -498,58 +538,105 @@
   2.147    \end{center}
   2.148    \end{figure}
   2.149  
   2.150 -  Note that @{text "instantiate_term"} could be derived using @{text
   2.151 -  "\<And>_intro/elim"}, but this is not how it is implemented.  The type
   2.152 -  instantiation rule is a genuine admissible one, due to the lack of
   2.153 -  true polymorphism in the logic.
   2.154 -
   2.155    Since @{text "\<Gamma>"} may never contain any schematic variables, the
   2.156    @{text "instantiate"} do not require an explicit side-condition.  In
   2.157    principle, variables could be substituted in hypotheses as well, but
   2.158    this could disrupt monotonicity of the basic calculus: derivations
   2.159    could leave the current proof context.
   2.160 +*}
   2.161  
   2.162 -  \medskip The framework also provides builtin equality @{text "\<equiv>"},
   2.163 -  which is conceptually axiomatized shown in \figref{fig:equality},
   2.164 -  although the implementation provides derived rules directly:
   2.165 +text %mlref {*
   2.166 +  \begin{mldecls}
   2.167 +  @{index_ML_type ctyp} \\
   2.168 +  @{index_ML_type cterm} \\
   2.169 +  @{index_ML_type thm} \\
   2.170 +  \end{mldecls}
   2.171 +
   2.172 +  \begin{description}
   2.173 +
   2.174 +  \item @{ML_type ctyp} FIXME
   2.175 +
   2.176 +  \item @{ML_type cterm} FIXME
   2.177 +
   2.178 +  \item @{ML_type thm} FIXME
   2.179 +
   2.180 +  \end{description}
   2.181 +*}
   2.182 +
   2.183 +
   2.184 +subsection {* Auxiliary connectives *}
   2.185 +
   2.186 +text {*
   2.187 +  Pure also provides various auxiliary connectives based on primitive
   2.188 +  definitions, see \figref{fig:pure-aux}.  These are normally not
   2.189 +  exposed to the user, but appear in internal encodings only.
   2.190  
   2.191    \begin{figure}[htb]
   2.192    \begin{center}
   2.193    \begin{tabular}{ll}
   2.194 -  @{text "\<equiv> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} & equality relation (infix) \\
   2.195 -  @{text "\<turnstile> (\<lambda>x. b x) a \<equiv> b a"} & @{text "\<beta>"}-conversion \\
   2.196 -  @{text "\<turnstile> x \<equiv> x"} & reflexivity law \\
   2.197 -  @{text "\<turnstile> x \<equiv> y \<Longrightarrow> P x \<Longrightarrow> P y"} & substitution law \\
   2.198 -  @{text "\<turnstile> (\<And>x. f x \<equiv> g x) \<Longrightarrow> f \<equiv> g"} & extensionality \\
   2.199 -  @{text "\<turnstile> (A \<Longrightarrow> B) \<Longrightarrow> (B \<Longrightarrow> A) \<Longrightarrow> A \<equiv> B"} & coincidence with equivalence \\
   2.200 +  @{text "conjunction :: prop \<Rightarrow> prop \<Rightarrow> prop"} & (infix @{text "&"}) \\
   2.201 +  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\[1ex]
   2.202 +  @{text "prop :: prop \<Rightarrow> prop"} & (prefix @{text "#"}) \\
   2.203 +  @{text "#A \<equiv> A"} \\[1ex]
   2.204 +  @{text "term :: \<alpha> \<Rightarrow> prop"} & (prefix @{text "TERM"}) \\
   2.205 +  @{text "term x \<equiv> (\<And>A. A \<Longrightarrow> A)"} \\[1ex]
   2.206 +  @{text "TYPE :: \<alpha> itself"} & (prefix @{text "TYPE"}) \\
   2.207 +  @{text "(unspecified)"} \\
   2.208    \end{tabular}
   2.209 -  \caption{Conceptual axiomatization of equality.}\label{fig:equality}
   2.210 +  \caption{Definitions of auxiliary connectives}\label{fig:pure-aux}
   2.211    \end{center}
   2.212    \end{figure}
   2.213  
   2.214 -  Since the basic representation of terms already accounts for @{text
   2.215 -  "\<alpha>"}-conversion, Pure equality essentially acts like @{text
   2.216 -  "\<alpha>\<beta>\<eta>"}-equivalence on terms, while coinciding with bi-implication.
   2.217 -
   2.218 +  Conjunction as an explicit connective allows to treat both
   2.219 +  simultaneous assumptions and conclusions uniformly.  The definition
   2.220 +  allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow> B \<Longrightarrow> A & B"},
   2.221 +  and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B \<Longrightarrow> B"}.  For
   2.222 +  example, several claims may be stated at the same time, which is
   2.223 +  intermediately represented as an assumption, but the user only
   2.224 +  encounters several sub-goals, and several resulting facts in the
   2.225 +  very end (cf.\ \secref{sec:tactical-goals}).
   2.226  
   2.227 -  \medskip Conjunction is defined in Pure as a derived connective, see
   2.228 -  \figref{fig:conjunction}.  This is occasionally useful to represent
   2.229 -  simultaneous statements behind the scenes --- framework conjunction
   2.230 -  is usually not exposed to the user.
   2.231 +  The @{text "#"} marker allows complex propositions (nested @{text
   2.232 +  "\<And>"} and @{text "\<Longrightarrow>"}) to appear formally as atomic, without changing
   2.233 +  the meaning: @{text "\<Gamma> \<turnstile> A"} and @{text "\<Gamma> \<turnstile> #A"} are
   2.234 +  interchangeable.  See \secref{sec:tactical-goals} for specific
   2.235 +  operations.
   2.236 +
   2.237 +  The @{text "TERM"} marker turns any well-formed term into a
   2.238 +  derivable proposition: @{text "\<turnstile> TERM t"} holds
   2.239 +  unconditionally.  Despite its logically vacous meaning, this is
   2.240 +  occasionally useful to treat syntactic terms and proven propositions
   2.241 +  uniformly, as in a type-theoretic framework.
   2.242  
   2.243 -  \begin{figure}[htb]
   2.244 -  \begin{center}
   2.245 -  \begin{tabular}{ll}
   2.246 -  @{text "& :: prop \<Rightarrow> prop \<Rightarrow> prop"} & conjunction (hidden) \\
   2.247 -  @{text "\<turnstile> A & B \<equiv> (\<And>C. (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C)"} \\
   2.248 -  \end{tabular}
   2.249 -  \caption{Definition of conjunction.}\label{fig:equality}
   2.250 -  \end{center}
   2.251 -  \end{figure}
   2.252 +  The @{text "TYPE"} constructor (which is the canonical
   2.253 +  representative of the unspecified type @{text "\<alpha> itself"}) injects
   2.254 +  the language of types into that of terms.  There is specific
   2.255 +  notation @{text "TYPE(\<tau>)"} for @{text "TYPE\<^bsub>\<tau>
   2.256 + itself\<^esub>"}.
   2.257 +  Although being devoid of any particular meaning, the term @{text
   2.258 +  "TYPE(\<tau>)"} is able to carry the type @{text "\<tau>"} formally.  @{text
   2.259 +  "TYPE(\<alpha>)"} may be used as an additional formal argument in primitive
   2.260 +  definitions, in order to avoid hidden polymorphism (cf.\
   2.261 +  \secref{sec:terms}).  For example, @{text "c TYPE(\<alpha>) \<equiv> A[\<alpha>]"} turns
   2.262 +  out as a formally correct definition of some proposition @{text "A"}
   2.263 +  that depends on an additional type argument.
   2.264 +*}
   2.265  
   2.266 -  The definition allows to derive the usual introduction @{text "\<turnstile> A \<Longrightarrow>
   2.267 -  B \<Longrightarrow> A & B"}, and destructions @{text "A & B \<Longrightarrow> A"} and @{text "A & B
   2.268 -  \<Longrightarrow> B"}.
   2.269 +text %mlref {*
   2.270 +  \begin{mldecls}
   2.271 +  @{index_ML Conjunction.intr: "thm -> thm -> thm"} \\
   2.272 +  @{index_ML Conjunction.elim: "thm -> thm * thm"} \\
   2.273 +  @{index_ML Drule.mk_term: "cterm -> thm"} \\
   2.274 +  @{index_ML Drule.dest_term: "thm -> cterm"} \\
   2.275 +  @{index_ML Logic.mk_type: "typ -> term"} \\
   2.276 +  @{index_ML Logic.dest_type: "term -> typ"} \\
   2.277 +  \end{mldecls}
   2.278 +
   2.279 +  \begin{description}
   2.280 +
   2.281 +  \item FIXME
   2.282 +
   2.283 +  \end{description}
   2.284  *}
   2.285  
   2.286