--- a/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 01 08:51:53 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 01 20:17:31 2006 +0200
@@ -106,10 +106,121 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+An \emph{assumption} is a proposition that it is postulated in the
+ current context. Local conclusions may use assumptions as
+ additional facts, but this imposes implicit hypotheses that weaken
+ the overall statement.
+
+ Assumptions are restricted to fixed non-schematic statements, all
+ generality needs to be expressed by explicit quantifiers.
+ Nevertheless, the result will be in HHF normal form with outermost
+ quantifiers stripped. For example, by assuming \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x} we get \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x\ {\isasymturnstile}\ P\ {\isacharquery}x} for arbitrary \isa{{\isacharquery}x}
+ of the fixed type \isa{{\isasymalpha}}. Local derivations accumulate more
+ and more explicit references to hypotheses: \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} where \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n} needs to
+ be covered by the assumptions of the current context.
+
+ \medskip The \isa{add{\isacharunderscore}assm} operation augments the context by
+ local assumptions, parameterized by an \isa{export} rule (see
+ below).
+
+ The \isa{export} operation moves facts from a (larger) inner
+ context into a (smaller) outer context, by discharging the
+ difference of the assumptions as specified by the associated export
+ rules. Note that the discharged portion is determined by the
+ contexts, not the facts being exported! There is a separate flag to
+ indicate a goal context, where the result is meant to refine an
+ enclosing sub-goal of a structured proof state (cf.\ FIXME).
+
+ \medskip The most basic export rule discharges assumptions directly
+ by means of the \isa{{\isasymLongrightarrow}} introduction rule:
+ \[
+ \infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
+ \]
+
+ The variant for goal refinements marks the newly introduced
+ premises, which causes the builtin goal refinement scheme of Isar to
+ enforce unification with local premises within the goal:
+ \[
+ \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
+ \]
+
+ \medskip Alternative versions of assumptions may perform arbitrary
+ transformations as long as a particular portion of hypotheses is
+ removed from the given facts.
+
+ For example, a local 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}}
+ \]
+
+ \medskip The general concept supports block-structured reasoning
+ nicely, with arbitrary mechanisms for introducing local assumptions.
+ The common reasoning pattern is as follows:
+
+ \medskip
+ \begin{tabular}{l}
+ \isa{add{\isacharunderscore}assm\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\
+ \isa{{\isasymdots}} \\
+ \isa{add{\isacharunderscore}assm\ e\isactrlisub n\ A\isactrlisub n} \\
+ \isa{export} \\
+ \end{tabular}
+ \medskip
+
+ \noindent The final \isa{export} will turn any fact \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} into some \isa{{\isasymturnstile}\ B{\isacharprime}}, by
+ applying the export rules \isa{e\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ e\isactrlisub n}
+ inside-out.%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexmltype{Assumption.export}\verb|type Assumption.export| \\
+ \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
+ \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: cterm list -> Proof.context -> thm list * Proof.context| \\
+ \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export -> cterm list -> Proof.context -> thm list * Proof.context| \\
+ \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Assumption.export|
+
+ \item \verb|Assumption.assume|~\isa{A} produces a raw assumption
+ \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion \isa{A{\isacharprime}} is in HHF normal
+ form.
+
+ \item \verb|Assumption.add_assumes|~\isa{As} augments the context
+ by plain assumptions that are discharged via \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or
+ \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode. The resulting facts are
+ hypothetical theorems as produced by \verb|Assumption.assume|.
+
+ \item \verb|Assumption.add_assms|~\isa{e\ As} augments the context
+ by generic assumptions that are discharged via rule \isa{e}.
+
+ \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ th}
+ exports result \isa{th} from the the \isa{inner} context
+ back into the \isa{outer} one. The \isa{is{\isacharunderscore}goal} flag is
+ \isa{true} for goal mode. The result is in HHF normal form.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsection{Conclusions%
}
\isamarkuptrue%