--- a/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 01 08:51:53 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 01 20:17:31 2006 +0200
@@ -67,7 +67,110 @@
section {* Assumptions *}
-text FIXME
+text {*
+ 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 @{text "\<And>x :: \<alpha>. P
+ x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for arbitrary @{text "?x"}
+ of the fixed type @{text "\<alpha>"}. Local derivations accumulate more
+ and more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>,
+ A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, A\<^isub>n"} needs to
+ be covered by the assumptions of the current context.
+
+ \medskip The @{text "add_assm"} operation augments the context by
+ local assumptions, parameterized by an @{text "export"} rule (see
+ below).
+
+ The @{text "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 @{text "\<Longrightarrow>"} introduction rule:
+ \[
+ \infer[(@{text "\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> 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[(@{text "#\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> 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 @{text "x"} and
+ assuming @{text "x \<equiv> t"}, with the following export rule to reverse
+ the effect:
+ \[
+ \infer{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> 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}
+ @{text "add_assm e\<^isub>1 A\<^isub>1"} \\
+ @{text "\<dots>"} \\
+ @{text "add_assm e\<^isub>n A\<^isub>n"} \\
+ @{text "export"} \\
+ \end{tabular}
+ \medskip
+
+ \noindent The final @{text "export"} will turn any fact @{text
+ "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} into some @{text "\<turnstile> B'"}, by
+ applying the export rules @{text "e\<^isub>1, \<dots>, e\<^isub>n"}
+ inside-out.
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML_type Assumption.export} \\
+ @{index_ML Assumption.assume: "cterm -> thm"} \\
+ @{index_ML Assumption.add_assumes: "cterm list -> Proof.context -> thm list * Proof.context"} \\
+ @{index_ML Assumption.add_assms:
+ "Assumption.export -> cterm list -> Proof.context -> thm list * Proof.context"} \\
+ @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML_type Assumption.export}
+
+ \item @{ML Assumption.assume}~@{text "A"} produces a raw assumption
+ @{text "A \<turnstile> A'"}, where the conclusion @{text "A'"} is in HHF normal
+ form.
+
+ \item @{ML Assumption.add_assumes}~@{text "As"} augments the context
+ by plain assumptions that are discharged via @{text "\<Longrightarrow>_intro"} or
+ @{text "#\<Longrightarrow>_intro"}, depending on goal mode. The resulting facts are
+ hypothetical theorems as produced by @{ML Assumption.assume}.
+
+ \item @{ML Assumption.add_assms}~@{text "e As"} augments the context
+ by generic assumptions that are discharged via rule @{text "e"}.
+
+ \item @{ML Assumption.export}~@{text "is_goal inner outer th"}
+ exports result @{text "th"} from the the @{text "inner"} context
+ back into the @{text "outer"} one. The @{text "is_goal"} flag is
+ @{text "true"} for goal mode. The result is in HHF normal form.
+
+ \end{description}
+*}
section {* Conclusions *}