--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu Sep 07 15:16:51 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu Sep 07 20:12:08 2006 +0200
@@ -217,7 +217,7 @@
definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
with the following export rule to reverse the effect:
\[
- \infer{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
+ \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
\]
This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in
a context with \isa{x} being fresh, so \isa{x} does not
@@ -291,22 +291,30 @@
references to free variables or assumptions not present in the proof
context.
- \medskip The \isa{prove} operation provides an interface for
- structured backwards reasoning under program control, with some
- explicit sanity checks of the result. The goal context can be
- augmented by additional fixed variables (cf.\
- \secref{sec:variables}) and assumptions (cf.\
- \secref{sec:assumptions}), which will be available as local facts
- during the proof and discharged into implications in the result.
- Type and term variables are generalized as usual, according to the
- context.
+ \medskip The \isa{SUBPROOF} combinator allows to structure a
+ tactical proof recursively by decomposing a selected sub-goal:
+ \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}}
+ after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}. This means
+ the tactic needs to solve the conclusion, but may use the premise as
+ a local fact, for locally fixed variables.
- The \isa{prove{\isacharunderscore}multi} operation handles several simultaneous
- claims within a single goal, by using Pure conjunction internally.
+ The \isa{prove} operation provides an interface for structured
+ backwards reasoning under program control, with some explicit sanity
+ checks of the result. The goal context can be augmented by
+ additional fixed variables (cf.\ \secref{sec:variables}) and
+ assumptions (cf.\ \secref{sec:assumptions}), which will be available
+ as local facts during the proof and discharged into implications in
+ the result. Type and term variables are generalized as usual,
+ according to the context.
- \medskip Tactical proofs may be structured recursively by
- decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned
- into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.%
+ The \isa{obtain} operation produces results by eliminating
+ existing facts by means of a given tactic. This acts like a dual
+ conclusion: the proof demonstrates that the context may be augmented
+ by certain fixed variables and assumptions. See also
+ \cite{isabelle-isar-ref} for the user-level \isa{{\isasymOBTAIN}} and
+ \isa{{\isasymGUESS}} elements. Final results, which may not refer to
+ the parameters in the conclusion, need to exported explicitly into
+ the original context.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -318,31 +326,39 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
+ \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
+\verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
+\verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
\indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
\indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
- \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
-\verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
-\verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic|
+ \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
+\verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context|
\end{mldecls}
\begin{description}
+ \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
+ particular sub-goal, producing an extended context and a reduced
+ goal, which needs to be solved by the given tactic. All schematic
+ parameters of the goal are imported into the context as fixed ones,
+ which may not be instantiated in the sub-proof.
+
\item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and
assumptions \isa{As}, and applies tactic \isa{tac} to solve
it. The latter may depend on the local assumptions being presented
as facts. The result is in HHF normal form.
\item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
- states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
- subgoals before commencing the actual proof.
+ states several conclusions simultaneously. The goal is encoded by
+ means of Pure conjunction; \verb|Tactic.conjunction_tac| will turn
+ this into a collection of individual subgoals.
- \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
- particular sub-goal, producing an extended context and a reduced
- goal, which needs to be solved by the given tactic. All schematic
- parameters of the goal are imported into the context as fixed ones,
- which may not be instantiated in the sub-proof.
+ \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the
+ given facts using a tactic, which results in additional fixed
+ variables and assumptions in the context. Final results need to be
+ exported explicitly.
\end{description}%
\end{isamarkuptext}%