--- a/doc-src/IsarRef/Thy/document/Generic.tex Fri May 09 23:35:57 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sat May 10 00:14:00 2008 +0200
@@ -790,191 +790,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Derived proof schemes%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Generalized elimination \label{sec:obtain}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{obtain}\mbox{\isa{\isacommand{obtain}}} & : & \isartrans{proof(state)}{proof(prove)} \\
- \indexdef{}{command}{guess}\mbox{\isa{\isacommand{guess}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(prove)} \\
- \end{matharray}
-
- Generalized elimination means that additional elements with certain
- properties may be introduced in the current context, by virtue of a
- locally proven ``soundness statement''. Technically speaking, the
- \mbox{\isa{\isacommand{obtain}}} language element is like a declaration of
- \mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} (see also see
- \secref{sec:proof-context}), together with a soundness proof of its
- additional claim. According to the nature of existential reasoning,
- assumptions get eliminated from any result exported from the context
- later, provided that the corresponding parameters do \emph{not}
- occur in the conclusion.
-
- \begin{rail}
- 'obtain' parname? (vars + 'and') 'where' (props + 'and')
- ;
- 'guess' (vars + 'and')
- ;
- \end{rail}
-
- The derived Isar command \mbox{\isa{\isacommand{obtain}}} is defined as follows
- (where \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k{\isachardoublequote}} shall refer to (optional)
- facts indicated for forward chaining).
- \begin{matharray}{l}
- \isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[1ex]
- \quad \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
- \quad \mbox{\isa{\isacommand{proof}}}~\isa{succeed} \\
- \qquad \mbox{\isa{\isacommand{fix}}}~\isa{thesis} \\
- \qquad \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
- \qquad \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}~\isa{thesis} \\
- \quad\qquad \mbox{\isa{\isacommand{apply}}}~\isa{{\isacharminus}} \\
- \quad\qquad \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
- \quad \mbox{\isa{\isacommand{qed}}} \\
- \quad \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} \\
- \end{matharray}
-
- Typically, the soundness proof is relatively straight-forward, often
- just by canonical automated tools such as ``\mbox{\isa{\isacommand{by}}}~\isa{simp}'' or ``\mbox{\isa{\isacommand{by}}}~\isa{blast}''. Accordingly, the
- ``\isa{that}'' reduction above is declared as simplification and
- introduction rule.
-
- In a sense, \mbox{\isa{\isacommand{obtain}}} represents at the level of Isar
- proofs what would be meta-logical existential quantifiers and
- conjunctions. This concept has a broad range of useful
- applications, ranging from plain elimination (or introduction) of
- object-level existential and conjunctions, to elimination over
- results of symbolic evaluation of recursive definitions, for
- example. Also note that \mbox{\isa{\isacommand{obtain}}} without parameters acts
- much like \mbox{\isa{\isacommand{have}}}, where the result is treated as a
- genuine assumption.
-
- An alternative name to be used instead of ``\isa{that}'' above may
- be given in parentheses.
-
- \medskip The improper variant \mbox{\isa{\isacommand{guess}}} is similar to
- \mbox{\isa{\isacommand{obtain}}}, but derives the obtained statement from the
- course of reasoning! The proof starts with a fixed goal \isa{thesis}. The subsequent proof may refine this to anything of the
- form like \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}}, but must not introduce new subgoals. The
- final goal state is then used as reduction rule for the obtain
- scheme described above. Obtained parameters \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} are marked as internal by default, which prevents the
- proof context from being polluted by ad-hoc variables. The variable
- names and type constraints given as arguments for \mbox{\isa{\isacommand{guess}}}
- specify a prefix of obtained parameters explicitly in the text.
-
- It is important to note that the facts introduced by \mbox{\isa{\isacommand{obtain}}} and \mbox{\isa{\isacommand{guess}}} may not be polymorphic: any
- type-variables occurring here are fixed in the present context!%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Calculational reasoning \label{sec:calculation}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{command}{also}\mbox{\isa{\isacommand{also}}} & : & \isartrans{proof(state)}{proof(state)} \\
- \indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
- \indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
- \indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
- \indexdef{}{command}{print\_trans\_rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
- \mbox{\isa{trans}} & : & \isaratt \\
- \mbox{\isa{sym}} & : & \isaratt \\
- \mbox{\isa{symmetric}} & : & \isaratt \\
- \end{matharray}
-
- Calculational proof is forward reasoning with implicit application
- of transitivity rules (such those of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}},
- \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}). Isabelle/Isar maintains an auxiliary fact register
- \indexref{}{fact}{calculation}\mbox{\isa{calculation}} for accumulating results obtained by
- transitivity composed with the current result. Command \mbox{\isa{\isacommand{also}}} updates \mbox{\isa{calculation}} involving \mbox{\isa{this}}, while
- \mbox{\isa{\isacommand{finally}}} exhibits the final \mbox{\isa{calculation}} by
- forward chaining towards the next goal statement. Both commands
- require valid current facts, i.e.\ may occur only after commands
- that produce theorems such as \mbox{\isa{\isacommand{assume}}}, \mbox{\isa{\isacommand{note}}}, or some finished proof of \mbox{\isa{\isacommand{have}}}, \mbox{\isa{\isacommand{show}}} etc. The \mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}
- commands are similar to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}},
- but only collect further results in \mbox{\isa{calculation}} without
- applying any rules yet.
-
- Also note that the implicit term abbreviation ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' has
- its canonical application with calculational proofs. It refers to
- the argument of the preceding statement. (The argument of a curried
- infix expression happens to be its right-hand side.)
-
- Isabelle/Isar calculations are implicitly subject to block structure
- in the sense that new threads of calculational reasoning are
- commenced for any new block (as opened by a local goal, for
- example). This means that, apart from being able to nest
- calculations, there is no separate \emph{begin-calculation} command
- required.
-
- \medskip The Isar calculation proof commands may be defined as
- follows:\footnote{We suppress internal bookkeeping such as proper
- handling of block-structure.}
-
- \begin{matharray}{rcl}
- \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
- \mbox{\isa{\isacommand{finally}}} & \equiv & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
- \mbox{\isa{\isacommand{moreover}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
- \mbox{\isa{\isacommand{ultimately}}} & \equiv & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\
- \end{matharray}
-
- \begin{rail}
- ('also' | 'finally') ('(' thmrefs ')')?
- ;
- 'trans' (() | 'add' | 'del')
- ;
- \end{rail}
-
- \begin{descr}
-
- \item [\mbox{\isa{\isacommand{also}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
- maintains the auxiliary \mbox{\isa{calculation}} register as follows.
- The first occurrence of \mbox{\isa{\isacommand{also}}} in some calculational
- thread initializes \mbox{\isa{calculation}} by \mbox{\isa{this}}. Any
- subsequent \mbox{\isa{\isacommand{also}}} on the same level of block-structure
- updates \mbox{\isa{calculation}} by some transitivity rule applied to
- \mbox{\isa{calculation}} and \mbox{\isa{this}} (in that order). Transitivity
- rules are picked from the current context, unless alternative rules
- are given as explicit arguments.
-
- \item [\mbox{\isa{\isacommand{finally}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
- maintaining \mbox{\isa{calculation}} in the same way as \mbox{\isa{\isacommand{also}}}, and concludes the current calculational thread. The final
- result is exhibited as fact for forward chaining towards the next
- goal. Basically, \mbox{\isa{\isacommand{finally}}} just abbreviates \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\mbox{\isa{calculation}}. Typical idioms for
- concluding calculational proofs are ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{show}}}~\isa{{\isacharquery}thesis}~\mbox{\isa{\isacommand{{\isachardot}}}}'' and ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isasymphi}}~\mbox{\isa{\isacommand{{\isachardot}}}}''.
-
- \item [\mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}] are
- analogous to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}}, but collect
- results only, without applying rules.
-
- \item [\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}] prints the list of
- transitivity rules (for calculational commands \mbox{\isa{\isacommand{also}}} and
- \mbox{\isa{\isacommand{finally}}}) and symmetry rules (for the \mbox{\isa{symmetric}} operation and single step elimination patters) of the
- current context.
-
- \item [\mbox{\isa{trans}}] declares theorems as transitivity rules.
-
- \item [\mbox{\isa{sym}}] declares symmetry rules, as well as
- \mbox{\isa{Pure{\isachardot}elim{\isacharquery}}} rules.
-
- \item [\mbox{\isa{symmetric}}] resolves a theorem with some rule
- declared as \mbox{\isa{sym}} in the current context. For example,
- ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y{\isachardoublequote}}'' produces a
- swapped fact derived from that assumption.
-
- In structured proof texts it is often more appropriate to use an
- explicit single-step elimination proof, such as ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}}~\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}y\ {\isacharequal}\ x{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Proof tools%
}
\isamarkuptrue%