author wenzelm Tue Sep 12 21:05:39 2006 +0200 (2006-09-12) changeset 20521 189811b39869 parent 20520 05fd007bdeb9 child 20522 05072ae0d435
more on theorems;
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.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.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.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.75    \begin{figure}[htb]
1.76    \begin{center}
1.77 @@ -458,32 +477,51 @@
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.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.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.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.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.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.140    \begin{figure}[htb]
1.141    \begin{center}
1.142 @@ -501,56 +539,134 @@
1.143    \end{center}
1.144    \end{figure}
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.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.160 +%
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.172 +  \begin{description}
1.174 +  \item \verb|ctyp| FIXME
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.181 +  \item \verb|thm| FIXME
1.183 +  \end{description}%
1.184 +\end{isamarkuptext}%
1.185 +\isamarkuptrue%
1.186 +%
1.187 +\endisatagmlref
1.188 +{\isafoldmlref}%
1.189 +%
1.191 +%
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.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.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.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.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.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.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.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.290 + \begin{description} 1.292 + \item FIXME 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.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.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.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.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.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.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.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.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.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.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.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.144    \begin{figure}[htb]
2.145    \begin{center}
2.146 @@ -498,58 +538,105 @@
2.147    \end{center}
2.148    \end{figure}
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.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.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.172 +  \begin{description}
2.174 +  \item @{ML_type ctyp} FIXME
2.176 +  \item @{ML_type cterm} FIXME
2.178 +  \item @{ML_type thm} FIXME
2.180 +  \end{description}
2.181 +*}
2.184 +subsection {* Auxiliary connectives *}
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.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.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.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.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.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.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.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.279 +  \begin{description}
2.281 +  \item FIXME
2.283 +  \end{description}
2.284  *}