author wenzelm Fri, 01 Sep 2006 20:17:31 +0200 changeset 20458 ab1d60e1ee31 parent 20457 85414caac94a child 20459 73c1ad6eda9d
explain assumptions;
--- 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{{\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%
%
+%
+%
+\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}%
+%
+%
+%
\isamarkupsection{Conclusions%
}
\isamarkuptrue%
--- 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"} \\
+    "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 *}