# HG changeset patch # User wenzelm # Date 1157136005 -7200 # Node ID 73c1ad6eda9d43b5da323e948d37e6a300a4d24a # Parent ab1d60e1ee3194e83a307cd7529a694a3d65ae3b tuned; diff -r ab1d60e1ee31 -r 73c1ad6eda9d doc-src/IsarImplementation/Thy/document/proof.tex --- a/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 01 20:17:31 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 01 20:40:05 2006 +0200 @@ -42,7 +42,8 @@ \begin{mldecls} \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\ \indexml{Variable.add-fixes}\verb|Variable.add_fixes: string list -> Proof.context -> string list * Proof.context| \\ - \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context| \\ + \indexml{Variable.import}\verb|Variable.import: bool ->|\isasep\isanewline% +\verb| thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context| \\ \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\ \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ @@ -119,17 +120,17 @@ 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). + \medskip The \isa{add{\isacharunderscore}assms} operation augments the context by + local assumptions, which are parameterized by an arbitrary \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). + difference 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.\ + \secref{sec:isar-proof-state}). \medskip The most basic export rule discharges assumptions directly by means of the \isa{{\isasymLongrightarrow}} introduction rule: @@ -144,13 +145,11 @@ \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: + \medskip Alternative assumptions may perform arbitrary + transformations on export, 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}} \] @@ -161,9 +160,9 @@ \medskip \begin{tabular}{l} - \isa{add{\isacharunderscore}assm\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\ + \isa{add{\isacharunderscore}assms\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\ \isa{{\isasymdots}} \\ - \isa{add{\isacharunderscore}assm\ e\isactrlisub n\ A\isactrlisub n} \\ + \isa{add{\isacharunderscore}assms\ e\isactrlisub n\ A\isactrlisub n} \\ \isa{export} \\ \end{tabular} \medskip @@ -184,31 +183,36 @@ \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.add-assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline% +\verb| cterm list -> Proof.context -> thm list * Proof.context| \\ + \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: |\isasep\isanewline% +\verb| 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.export| represents arbitrary export + rules, which is any function of type \verb|bool -> cterm list -> thm -> thm|, + where the \verb|bool| indicates goal mode, and the \verb|cterm list| the collection of assumptions to be discharged + simultaneously. - \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.assume|~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion + \isa{A{\isacharprime}} is in HHF normal form. \item \verb|Assumption.add_assms|~\isa{e\ As} augments the context - by generic assumptions that are discharged via rule \isa{e}. + by assumptions \isa{As} with export rule \isa{e}. The + resulting facts are hypothetical theorems as produced by \verb|Assumption.assume|. + + \item \verb|Assumption.add_assumes|~\isa{As} is a special case of + \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode. \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. + back into the \isa{outer} one; \isa{is{\isacharunderscore}goal\ {\isacharequal}\ true} means + this is a goal context. The result is in HHF normal form. Note + that \verb|ProofContext.export| combines \verb|Variable.export| + and \verb|Assumption.export| in the canonical way. \end{description}% \end{isamarkuptext}% diff -r ab1d60e1ee31 -r 73c1ad6eda9d doc-src/IsarImplementation/Thy/proof.thy --- a/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 01 20:17:31 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 01 20:40:05 2006 +0200 @@ -13,7 +13,8 @@ \begin{mldecls} @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\ @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\ - @{index_ML Variable.import: "bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\ + @{index_ML Variable.import: "bool -> + thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context"} \\ @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ @@ -83,17 +84,18 @@ 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). + \medskip The @{text "add_assms"} operation augments the context by + local assumptions, which are parameterized by an arbitrary @{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). + difference 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.\ + \secref{sec:isar-proof-state}). \medskip The most basic export rule discharges assumptions directly by means of the @{text "\"} introduction rule: @@ -108,13 +110,11 @@ \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: + \medskip Alternative assumptions may perform arbitrary + transformations on export, 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"}} \] @@ -125,9 +125,9 @@ \medskip \begin{tabular}{l} - @{text "add_assm e\<^isub>1 A\<^isub>1"} \\ + @{text "add_assms e\<^isub>1 A\<^isub>1"} \\ @{text "\"} \\ - @{text "add_assm e\<^isub>n A\<^isub>n"} \\ + @{text "add_assms e\<^isub>n A\<^isub>n"} \\ @{text "export"} \\ \end{tabular} \medskip @@ -142,32 +142,41 @@ \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"} \\ + "Assumption.export -> + cterm list -> Proof.context -> thm list * Proof.context"} \\ + @{index_ML Assumption.add_assumes: " + 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_type Assumption.export} represents arbitrary export + rules, which is any function of type @{ML_type "bool -> cterm list -> thm -> thm"}, + where the @{ML_type "bool"} indicates goal mode, and the @{ML_type + "cterm list"} the collection of assumptions to be discharged + simultaneously. - \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.assume}~@{text "A"} turns proposition @{text + "A"} into a raw assumption @{text "A \ A'"}, where the conclusion + @{text "A'"} is in HHF normal form. \item @{ML Assumption.add_assms}~@{text "e As"} augments the context - by generic assumptions that are discharged via rule @{text "e"}. + by assumptions @{text "As"} with export rule @{text "e"}. The + resulting facts are hypothetical theorems as produced by @{ML + Assumption.assume}. + + \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of + @{ML Assumption.add_assms} where the export rule performs @{text + "\_intro"} or @{text "#\_intro"}, depending on goal mode. \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. + back into the @{text "outer"} one; @{text "is_goal = true"} means + this is a goal context. The result is in HHF normal form. Note + that @{ML "ProofContext.export"} combines @{ML "Variable.export"} + and @{ML "Assumption.export"} in the canonical way. \end{description} *}