# HG changeset patch # User wenzelm # Date 1157134651 -7200 # Node ID ab1d60e1ee3194e83a307cd7529a694a3d65ae3b # Parent 85414caac94a1c653e6d7e2b15229c89f437c0d3 explain assumptions; diff -r 85414caac94a -r ab1d60e1ee31 doc-src/IsarImplementation/Thy/document/proof.tex --- 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% diff -r 85414caac94a -r ab1d60e1ee31 doc-src/IsarImplementation/Thy/proof.thy --- 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 "\x :: \. P + x"} we get @{text "\x :: \. P x \ P ?x"} for arbitrary @{text "?x"} + of the fixed type @{text "\"}. Local derivations accumulate more + and more explicit references to hypotheses: @{text "A\<^isub>1, \, + A\<^isub>n \ B"} where @{text "A\<^isub>1, \, 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 "\"} introduction rule: + \[ + \infer[(@{text "\_intro"})]{@{text "\ \\ A \ A \ B"}}{@{text "\ \ 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 "#\_intro"})]{@{text "\ \\ A \ #A \ B"}}{@{text "\ \ 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 \ t"}, with the following export rule to reverse + the effect: + \[ + \infer{@{text "\ \\ x \ t \ B t"}}{@{text "\ \ 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 "\"} \\ + @{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, \, A\<^isub>n \ B"} into some @{text "\ B'"}, by + applying the export rules @{text "e\<^isub>1, \, 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 \ 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 "\_intro"} or + @{text "#\_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 *}