--- a/src/Doc/Implementation/Proof.thy Wed Dec 16 16:31:36 2015 +0100
+++ b/src/Doc/Implementation/Proof.thy Wed Dec 16 17:28:49 2015 +0100
@@ -9,52 +9,48 @@
section \<open>Variables \label{sec:variables}\<close>
text \<open>
- Any variable that is not explicitly bound by \<open>\<lambda>\<close>-abstraction
- is considered as ``free''. Logically, free variables act like
- outermost universal quantification at the sequent level: \<open>A\<^sub>1(x), \<dots>, A\<^sub>n(x) \<turnstile> B(x)\<close> means that the result
- holds \<^emph>\<open>for all\<close> values of \<open>x\<close>. Free variables for
- terms (not types) can be fully internalized into the logic: \<open>\<turnstile> B(x)\<close> and \<open>\<turnstile> \<And>x. B(x)\<close> are interchangeable, provided
- that \<open>x\<close> does not occur elsewhere in the context.
- Inspecting \<open>\<turnstile> \<And>x. B(x)\<close> more closely, we see that inside the
- quantifier, \<open>x\<close> is essentially ``arbitrary, but fixed'',
- while from outside it appears as a place-holder for instantiation
- (thanks to \<open>\<And>\<close> elimination).
+ Any variable that is not explicitly bound by \<open>\<lambda>\<close>-abstraction is considered
+ as ``free''. Logically, free variables act like outermost universal
+ quantification at the sequent level: \<open>A\<^sub>1(x), \<dots>, A\<^sub>n(x) \<turnstile> B(x)\<close> means that
+ the result holds \<^emph>\<open>for all\<close> values of \<open>x\<close>. Free variables for terms (not
+ types) can be fully internalized into the logic: \<open>\<turnstile> B(x)\<close> and \<open>\<turnstile> \<And>x. B(x)\<close>
+ are interchangeable, provided that \<open>x\<close> does not occur elsewhere in the
+ context. Inspecting \<open>\<turnstile> \<And>x. B(x)\<close> more closely, we see that inside the
+ quantifier, \<open>x\<close> is essentially ``arbitrary, but fixed'', while from outside
+ it appears as a place-holder for instantiation (thanks to \<open>\<And>\<close> elimination).
- The Pure logic represents the idea of variables being either inside
- or outside the current scope by providing separate syntactic
- categories for \<^emph>\<open>fixed variables\<close> (e.g.\ \<open>x\<close>) vs.\
- \<^emph>\<open>schematic variables\<close> (e.g.\ \<open>?x\<close>). Incidently, a
- universal result \<open>\<turnstile> \<And>x. B(x)\<close> has the HHF normal form \<open>\<turnstile> B(?x)\<close>, which represents its generality without requiring an
- explicit quantifier. The same principle works for type variables:
- \<open>\<turnstile> B(?\<alpha>)\<close> represents the idea of ``\<open>\<turnstile> \<forall>\<alpha>. B(\<alpha>)\<close>''
- without demanding a truly polymorphic framework.
+ The Pure logic represents the idea of variables being either inside or
+ outside the current scope by providing separate syntactic categories for
+ \<^emph>\<open>fixed variables\<close> (e.g.\ \<open>x\<close>) vs.\ \<^emph>\<open>schematic variables\<close> (e.g.\ \<open>?x\<close>).
+ Incidently, a universal result \<open>\<turnstile> \<And>x. B(x)\<close> has the HHF normal form \<open>\<turnstile>
+ B(?x)\<close>, which represents its generality without requiring an explicit
+ quantifier. The same principle works for type variables: \<open>\<turnstile> B(?\<alpha>)\<close>
+ represents the idea of ``\<open>\<turnstile> \<forall>\<alpha>. B(\<alpha>)\<close>'' without demanding a truly
+ polymorphic framework.
\<^medskip>
- Additional care is required to treat type variables in a
- way that facilitates type-inference. In principle, term variables
- depend on type variables, which means that type variables would have
- to be declared first. For example, a raw type-theoretic framework
- would demand the context to be constructed in stages as follows:
- \<open>\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^sub>\<alpha>)\<close>.
+ Additional care is required to treat type variables in a way that
+ facilitates type-inference. In principle, term variables depend on type
+ variables, which means that type variables would have to be declared first.
+ For example, a raw type-theoretic framework would demand the context to be
+ constructed in stages as follows: \<open>\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^sub>\<alpha>)\<close>.
- We allow a slightly less formalistic mode of operation: term
- variables \<open>x\<close> are fixed without specifying a type yet
- (essentially \<^emph>\<open>all\<close> potential occurrences of some instance
- \<open>x\<^sub>\<tau>\<close> are fixed); the first occurrence of \<open>x\<close>
+ We allow a slightly less formalistic mode of operation: term variables \<open>x\<close>
+ are fixed without specifying a type yet (essentially \<^emph>\<open>all\<close> potential
+ occurrences of some instance \<open>x\<^sub>\<tau>\<close> are fixed); the first occurrence of \<open>x\<close>
within a specific term assigns its most general type, which is then
- maintained consistently in the context. The above example becomes
- \<open>\<Gamma> = x: term, \<alpha>: type, A(x\<^sub>\<alpha>)\<close>, where type \<open>\<alpha>\<close> is fixed \<^emph>\<open>after\<close> term \<open>x\<close>, and the constraint
- \<open>x :: \<alpha>\<close> is an implicit consequence of the occurrence of
- \<open>x\<^sub>\<alpha>\<close> in the subsequent proposition.
+ maintained consistently in the context. The above example becomes \<open>\<Gamma> = x:
+ term, \<alpha>: type, A(x\<^sub>\<alpha>)\<close>, where type \<open>\<alpha>\<close> is fixed \<^emph>\<open>after\<close> term \<open>x\<close>, and the
+ constraint \<open>x :: \<alpha>\<close> is an implicit consequence of the occurrence of \<open>x\<^sub>\<alpha>\<close> in
+ the subsequent proposition.
- This twist of dependencies is also accommodated by the reverse
- operation of exporting results from a context: a type variable
- \<open>\<alpha>\<close> is considered fixed as long as it occurs in some fixed
- term variable of the context. For example, exporting \<open>x:
- term, \<alpha>: type \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>\<close> produces in the first step \<open>x: term
- \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>\<close> for fixed \<open>\<alpha>\<close>, and only in the second step
- \<open>\<turnstile> ?x\<^sub>?\<^sub>\<alpha> \<equiv> ?x\<^sub>?\<^sub>\<alpha>\<close> for schematic \<open>?x\<close> and \<open>?\<alpha>\<close>.
- The following Isar source text illustrates this scenario.
+ This twist of dependencies is also accommodated by the reverse operation of
+ exporting results from a context: a type variable \<open>\<alpha>\<close> is considered fixed as
+ long as it occurs in some fixed term variable of the context. For example,
+ exporting \<open>x: term, \<alpha>: type \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>\<close> produces in the first step \<open>x: term
+ \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>\<close> for fixed \<open>\<alpha>\<close>, and only in the second step \<open>\<turnstile> ?x\<^sub>?\<^sub>\<alpha> \<equiv> ?x\<^sub>?\<^sub>\<alpha>\<close>
+ for schematic \<open>?x\<close> and \<open>?\<alpha>\<close>. The following Isar source text illustrates this
+ scenario.
\<close>
notepad
@@ -70,29 +66,28 @@
thm this \<comment> \<open>fully general result for arbitrary \<open>?x::?'a\<close>\<close>
end
-text \<open>The Isabelle/Isar proof context manages the details of term
- vs.\ type variables, with high-level principles for moving the
- frontier between fixed and schematic variables.
+text \<open>
+ The Isabelle/Isar proof context manages the details of term vs.\ type
+ variables, with high-level principles for moving the frontier between fixed
+ and schematic variables.
- The \<open>add_fixes\<close> operation explicitly declares fixed
- variables; the \<open>declare_term\<close> operation absorbs a term into
- a context by fixing new type variables and adding syntactic
- constraints.
+ The \<open>add_fixes\<close> operation explicitly declares fixed variables; the
+ \<open>declare_term\<close> operation absorbs a term into a context by fixing new type
+ variables and adding syntactic constraints.
- The \<open>export\<close> operation is able to perform the main work of
- generalizing term and type variables as sketched above, assuming
- that fixing variables and terms have been declared properly.
+ The \<open>export\<close> operation is able to perform the main work of generalizing term
+ and type variables as sketched above, assuming that fixing variables and
+ terms have been declared properly.
- There \<open>import\<close> operation makes a generalized fact a genuine
- part of the context, by inventing fixed variables for the schematic
- ones. The effect can be reversed by using \<open>export\<close> later,
- potentially with an extended context; the result is equivalent to
- the original modulo renaming of schematic variables.
+ There \<open>import\<close> operation makes a generalized fact a genuine part of the
+ context, by inventing fixed variables for the schematic ones. The effect can
+ be reversed by using \<open>export\<close> later, potentially with an extended context;
+ the result is equivalent to the original modulo renaming of schematic
+ variables.
- The \<open>focus\<close> operation provides a variant of \<open>import\<close>
- for nested propositions (with explicit quantification): \<open>\<And>x\<^sub>1 \<dots> x\<^sub>n. B(x\<^sub>1, \<dots>, x\<^sub>n)\<close> is
- decomposed by inventing fixed variables \<open>x\<^sub>1, \<dots>,
- x\<^sub>n\<close> for the body.
+ The \<open>focus\<close> operation provides a variant of \<open>import\<close> for nested propositions
+ (with explicit quantification): \<open>\<And>x\<^sub>1 \<dots> x\<^sub>n. B(x\<^sub>1, \<dots>, x\<^sub>n)\<close> is decomposed
+ by inventing fixed variables \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close> for the body.
\<close>
text %mlref \<open>
@@ -111,48 +106,47 @@
((string * (string * typ)) list * term) * Proof.context"} \\
\end{mldecls}
- \<^descr> @{ML Variable.add_fixes}~\<open>xs ctxt\<close> fixes term
- variables \<open>xs\<close>, returning the resulting internal names. By
- default, the internal representation coincides with the external
- one, which also means that the given variables must not be fixed
- already. There is a different policy within a local proof body: the
- given names are just hints for newly invented Skolem variables.
+ \<^descr> @{ML Variable.add_fixes}~\<open>xs ctxt\<close> fixes term variables \<open>xs\<close>, returning
+ the resulting internal names. By default, the internal representation
+ coincides with the external one, which also means that the given variables
+ must not be fixed already. There is a different policy within a local proof
+ body: the given names are just hints for newly invented Skolem variables.
- \<^descr> @{ML Variable.variant_fixes} is similar to @{ML
- Variable.add_fixes}, but always produces fresh variants of the given
- names.
+ \<^descr> @{ML Variable.variant_fixes} is similar to @{ML Variable.add_fixes}, but
+ always produces fresh variants of the given names.
- \<^descr> @{ML Variable.declare_term}~\<open>t ctxt\<close> declares term
- \<open>t\<close> to belong to the context. This automatically fixes new
- type variables, but not term variables. Syntactic constraints for
- type and term variables are declared uniformly, though.
+ \<^descr> @{ML Variable.declare_term}~\<open>t ctxt\<close> declares term \<open>t\<close> to belong to the
+ context. This automatically fixes new type variables, but not term
+ variables. Syntactic constraints for type and term variables are declared
+ uniformly, though.
+
+ \<^descr> @{ML Variable.declare_constraints}~\<open>t ctxt\<close> declares syntactic constraints
+ from term \<open>t\<close>, without making it part of the context yet.
- \<^descr> @{ML Variable.declare_constraints}~\<open>t ctxt\<close> declares
- syntactic constraints from term \<open>t\<close>, without making it part
- of the context yet.
-
- \<^descr> @{ML Variable.export}~\<open>inner outer thms\<close> generalizes
- fixed type and term variables in \<open>thms\<close> according to the
- difference of the \<open>inner\<close> and \<open>outer\<close> context,
- following the principles sketched above.
+ \<^descr> @{ML Variable.export}~\<open>inner outer thms\<close> generalizes fixed type and term
+ variables in \<open>thms\<close> according to the difference of the \<open>inner\<close> and \<open>outer\<close>
+ context, following the principles sketched above.
- \<^descr> @{ML Variable.polymorphic}~\<open>ctxt ts\<close> generalizes type
- variables in \<open>ts\<close> as far as possible, even those occurring
- in fixed term variables. The default policy of type-inference is to
- fix newly introduced type variables, which is essentially reversed
- with @{ML Variable.polymorphic}: here the given terms are detached
- from the context as far as possible.
+ \<^descr> @{ML Variable.polymorphic}~\<open>ctxt ts\<close> generalizes type variables in \<open>ts\<close> as
+ far as possible, even those occurring in fixed term variables. The default
+ policy of type-inference is to fix newly introduced type variables, which is
+ essentially reversed with @{ML Variable.polymorphic}: here the given terms
+ are detached from the context as far as possible.
- \<^descr> @{ML Variable.import}~\<open>open thms ctxt\<close> invents fixed
- type and term variables for the schematic ones occurring in \<open>thms\<close>. The \<open>open\<close> flag indicates whether the fixed names
- should be accessible to the user, otherwise newly introduced names
- are marked as ``internal'' (\secref{sec:names}).
+ \<^descr> @{ML Variable.import}~\<open>open thms ctxt\<close> invents fixed type and term
+ variables for the schematic ones occurring in \<open>thms\<close>. The \<open>open\<close> flag
+ indicates whether the fixed names should be accessible to the user,
+ otherwise newly introduced names are marked as ``internal''
+ (\secref{sec:names}).
- \<^descr> @{ML Variable.focus}~\<open>bindings B\<close> decomposes the outermost \<open>\<And>\<close> prefix of proposition \<open>B\<close>, using the given name bindings.
+ \<^descr> @{ML Variable.focus}~\<open>bindings B\<close> decomposes the outermost \<open>\<And>\<close> prefix of
+ proposition \<open>B\<close>, using the given name bindings.
\<close>
-text %mlex \<open>The following example shows how to work with fixed term
- and type parameters and with type-inference.\<close>
+text %mlex \<open>
+ The following example shows how to work with fixed term and type parameters
+ and with type-inference.
+\<close>
ML_val \<open>
(*static compile-time context -- for testing only*)
@@ -173,12 +167,13 @@
val t2 = Syntax.read_term ctxt2 "x"; (*x::nat is enforced*)
\<close>
-text \<open>In the above example, the starting context is derived from the
- toplevel theory, which means that fixed variables are internalized
- literally: \<open>x\<close> is mapped again to \<open>x\<close>, and
- attempting to fix it again in the subsequent context is an error.
- Alternatively, fixed parameters can be renamed explicitly as
- follows:\<close>
+text \<open>
+ In the above example, the starting context is derived from the toplevel
+ theory, which means that fixed variables are internalized literally: \<open>x\<close> is
+ mapped again to \<open>x\<close>, and attempting to fix it again in the subsequent
+ context is an error. Alternatively, fixed parameters can be renamed
+ explicitly as follows:
+\<close>
ML_val \<open>
val ctxt0 = @{context};
@@ -186,11 +181,12 @@
ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
\<close>
-text \<open>The following ML code can now work with the invented names of
- \<open>x1\<close>, \<open>x2\<close>, \<open>x3\<close>, without depending on
- the details on the system policy for introducing these variants.
- Recall that within a proof body the system always invents fresh
- ``Skolem constants'', e.g.\ as follows:\<close>
+text \<open>
+ The following ML code can now work with the invented names of \<open>x1\<close>, \<open>x2\<close>,
+ \<open>x3\<close>, without depending on the details on the system policy for introducing
+ these variants. Recall that within a proof body the system always invents
+ fresh ``Skolem constants'', e.g.\ as follows:
+\<close>
notepad
begin
@@ -205,68 +201,63 @@
ctxt3 |> Variable.variant_fixes ["y", "y"];\<close>
end
-text \<open>In this situation @{ML Variable.add_fixes} and @{ML
- Variable.variant_fixes} are very similar, but identical name
- proposals given in a row are only accepted by the second version.
+text \<open>
+ In this situation @{ML Variable.add_fixes} and @{ML Variable.variant_fixes}
+ are very similar, but identical name proposals given in a row are only
+ accepted by the second version.
\<close>
section \<open>Assumptions \label{sec:assumptions}\<close>
text \<open>
- An \<^emph>\<open>assumption\<close> 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.
+ An \<^emph>\<open>assumption\<close> 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, i.e.\
- 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 \<open>\<And>x :: \<alpha>. P
- x\<close> we get \<open>\<And>x :: \<alpha>. P x \<turnstile> P ?x\<close> for schematic \<open>?x\<close>
- of fixed type \<open>\<alpha>\<close>. Local derivations accumulate more and
- more explicit references to hypotheses: \<open>A\<^sub>1, \<dots>,
- A\<^sub>n \<turnstile> B\<close> where \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close> needs to
- be covered by the assumptions of the current context.
+ Assumptions are restricted to fixed non-schematic statements, i.e.\ 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 \<open>\<And>x :: \<alpha>. P x\<close> we get \<open>\<And>x :: \<alpha>. P x \<turnstile> P ?x\<close> for
+ schematic \<open>?x\<close> of fixed type \<open>\<alpha>\<close>. Local derivations accumulate more and more
+ explicit references to hypotheses: \<open>A\<^sub>1, \<dots>, A\<^sub>n \<turnstile> B\<close> where \<open>A\<^sub>1, \<dots>, A\<^sub>n\<close>
+ needs to be covered by the assumptions of the current context.
\<^medskip>
- The \<open>add_assms\<close> operation augments the context by
- local assumptions, which are parameterized by an arbitrary \<open>export\<close> rule (see below).
+ The \<open>add_assms\<close> operation augments the context by local assumptions, which
+ are parameterized by an arbitrary \<open>export\<close> rule (see below).
- The \<open>export\<close> 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
- difference of 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.
+ The \<open>export\<close> 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 difference of 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.
\<^medskip>
- The most basic export rule discharges assumptions directly
- by means of the \<open>\<Longrightarrow>\<close> introduction rule:
+ The most basic export rule discharges assumptions directly by means of the
+ \<open>\<Longrightarrow>\<close> introduction rule:
\[
\infer[(\<open>\<Longrightarrow>\<hyphen>intro\<close>)]{\<open>\<Gamma> - A \<turnstile> A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}
\]
- The variant for goal refinements marks the newly introduced
- premises, which causes the canonical Isar goal refinement scheme to
- enforce unification with local premises within the goal:
+ The variant for goal refinements marks the newly introduced premises, which
+ causes the canonical Isar goal refinement scheme to enforce unification with
+ local premises within the goal:
\[
\infer[(\<open>#\<Longrightarrow>\<hyphen>intro\<close>)]{\<open>\<Gamma> - A \<turnstile> #A \<Longrightarrow> B\<close>}{\<open>\<Gamma> \<turnstile> B\<close>}
\]
\<^medskip>
- Alternative versions of assumptions may perform arbitrary
- transformations on export, as long as the corresponding portion of
- hypotheses is removed from the given facts. For example, a local
- definition works by fixing \<open>x\<close> and assuming \<open>x \<equiv> t\<close>,
- with the following export rule to reverse the effect:
+ Alternative versions of assumptions may perform arbitrary transformations on
+ export, as long as the corresponding portion of hypotheses is removed from
+ the given facts. For example, a local definition works by fixing \<open>x\<close> and
+ assuming \<open>x \<equiv> t\<close>, with the following export rule to reverse the effect:
\[
\infer[(\<open>\<equiv>\<hyphen>expand\<close>)]{\<open>\<Gamma> - (x \<equiv> t) \<turnstile> B t\<close>}{\<open>\<Gamma> \<turnstile> B x\<close>}
\]
- This works, because the assumption \<open>x \<equiv> t\<close> was introduced in
- a context with \<open>x\<close> being fresh, so \<open>x\<close> does not
- occur in \<open>\<Gamma>\<close> here.
+ This works, because the assumption \<open>x \<equiv> t\<close> was introduced in a context with
+ \<open>x\<close> being fresh, so \<open>x\<close> does not occur in \<open>\<Gamma>\<close> here.
\<close>
text %mlref \<open>
@@ -281,36 +272,33 @@
@{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
\end{mldecls}
- \<^descr> Type @{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.
+ \<^descr> Type @{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.
- \<^descr> @{ML Assumption.assume}~\<open>ctxt A\<close> turns proposition \<open>A\<close> into a primitive assumption \<open>A \<turnstile> A'\<close>, where the
- conclusion \<open>A'\<close> is in HHF normal form.
+ \<^descr> @{ML Assumption.assume}~\<open>ctxt A\<close> turns proposition \<open>A\<close> into a primitive
+ assumption \<open>A \<turnstile> A'\<close>, where the conclusion \<open>A'\<close> is in HHF normal form.
- \<^descr> @{ML Assumption.add_assms}~\<open>r As\<close> augments the context
- by assumptions \<open>As\<close> with export rule \<open>r\<close>. The
- resulting facts are hypothetical theorems as produced by the raw
- @{ML Assumption.assume}.
+ \<^descr> @{ML Assumption.add_assms}~\<open>r As\<close> augments the context by assumptions \<open>As\<close>
+ with export rule \<open>r\<close>. The resulting facts are hypothetical theorems as
+ produced by the raw @{ML Assumption.assume}.
- \<^descr> @{ML Assumption.add_assumes}~\<open>As\<close> is a special case of
- @{ML Assumption.add_assms} where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or \<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal
- mode.
+ \<^descr> @{ML Assumption.add_assumes}~\<open>As\<close> is a special case of @{ML
+ Assumption.add_assms} where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
+ \<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal mode.
- \<^descr> @{ML Assumption.export}~\<open>is_goal inner outer thm\<close>
- exports result \<open>thm\<close> from the the \<open>inner\<close> context
- back into the \<open>outer\<close> one; \<open>is_goal = true\<close> means
- this is a goal context. The result is in HHF normal form. Note
- that @{ML "Proof_Context.export"} combines @{ML "Variable.export"}
- and @{ML "Assumption.export"} in the canonical way.
+ \<^descr> @{ML Assumption.export}~\<open>is_goal inner outer thm\<close> exports result \<open>thm\<close>
+ from the the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close>
+ means this is a goal context. The result is in HHF normal form. Note that
+ @{ML "Proof_Context.export"} combines @{ML "Variable.export"} and @{ML
+ "Assumption.export"} in the canonical way.
\<close>
-text %mlex \<open>The following example demonstrates how rules can be
- derived by building up a context of assumptions first, and exporting
- some local fact afterwards. We refer to @{theory Pure} equality
- here for testing purposes.
+text %mlex \<open>
+ The following example demonstrates how rules can be derived by building up a
+ context of assumptions first, and exporting some local fact afterwards. We
+ refer to @{theory Pure} equality here for testing purposes.
\<close>
ML_val \<open>
@@ -325,52 +313,50 @@
val r = Assumption.export false ctxt1 ctxt0 eq';
\<close>
-text \<open>Note that the variables of the resulting rule are not
- generalized. This would have required to fix them properly in the
- context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML
- Variable.export} or the combined @{ML "Proof_Context.export"}).\<close>
+text \<open>
+ Note that the variables of the resulting rule are not generalized. This
+ would have required to fix them properly in the context beforehand, and
+ export wrt.\ variables afterwards (cf.\ @{ML Variable.export} or the
+ combined @{ML "Proof_Context.export"}).
+\<close>
section \<open>Structured goals and results \label{sec:struct-goals}\<close>
text \<open>
- Local results are established by monotonic reasoning from facts
- within a context. This allows common combinations of theorems,
- e.g.\ via \<open>\<And>/\<Longrightarrow>\<close> elimination, resolution rules, or equational
- reasoning, see \secref{sec:thms}. Unaccounted context manipulations
- should be avoided, notably raw \<open>\<And>/\<Longrightarrow>\<close> introduction or ad-hoc
- references to free variables or assumptions not present in the proof
- context.
+ Local results are established by monotonic reasoning from facts within a
+ context. This allows common combinations of theorems, e.g.\ via \<open>\<And>/\<Longrightarrow>\<close>
+ elimination, resolution rules, or equational reasoning, see
+ \secref{sec:thms}. Unaccounted context manipulations should be avoided,
+ notably raw \<open>\<And>/\<Longrightarrow>\<close> introduction or ad-hoc references to free variables or
+ assumptions not present in the proof context.
\<^medskip>
- The \<open>SUBPROOF\<close> combinator allows to structure a
- tactical proof recursively by decomposing a selected sub-goal:
- \<open>(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>\<close> is turned into \<open>B(x) \<Longrightarrow> \<dots>\<close>
- after fixing \<open>x\<close> and assuming \<open>A(x)\<close>. This means
- the tactic needs to solve the conclusion, but may use the premise as
- a local fact, for locally fixed variables.
+ The \<open>SUBPROOF\<close> combinator allows to structure a tactical proof recursively
+ by decomposing a selected sub-goal: \<open>(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>\<close> is turned into
+ \<open>B(x) \<Longrightarrow> \<dots>\<close> after fixing \<open>x\<close> and assuming \<open>A(x)\<close>. This means the tactic needs
+ to solve the conclusion, but may use the premise as a local fact, for
+ locally fixed variables.
- The family of \<open>FOCUS\<close> combinators is similar to \<open>SUBPROOF\<close>, but allows to retain schematic variables and pending
- subgoals in the resulting goal state.
+ The family of \<open>FOCUS\<close> combinators is similar to \<open>SUBPROOF\<close>, but allows to
+ retain schematic variables and pending subgoals in the resulting goal state.
- The \<open>prove\<close> operation provides an interface for structured
- backwards reasoning under program control, with some explicit sanity
- checks of the result. The goal context can be augmented by
- additional fixed variables (cf.\ \secref{sec:variables}) and
- assumptions (cf.\ \secref{sec:assumptions}), which will be available
- as local facts during the proof and discharged into implications in
- the result. Type and term variables are generalized as usual,
- according to the context.
+ The \<open>prove\<close> operation provides an interface for structured backwards
+ reasoning under program control, with some explicit sanity checks of the
+ result. The goal context can be augmented by additional fixed variables
+ (cf.\ \secref{sec:variables}) and assumptions (cf.\
+ \secref{sec:assumptions}), which will be available as local facts during the
+ proof and discharged into implications in the result. Type and term
+ variables are generalized as usual, according to the context.
- The \<open>obtain\<close> operation produces results by eliminating
- existing facts by means of a given tactic. This acts like a dual
- conclusion: the proof demonstrates that the context may be augmented
- by parameters and assumptions, without affecting any conclusions
- that do not mention these parameters. See also
- @{cite "isabelle-isar-ref"} for the user-level @{command obtain} and
- @{command guess} elements. Final results, which may not refer to
- the parameters in the conclusion, need to exported explicitly into
- the original context.\<close>
+ The \<open>obtain\<close> operation produces results by eliminating existing facts by
+ means of a given tactic. This acts like a dual conclusion: the proof
+ demonstrates that the context may be augmented by parameters and
+ assumptions, without affecting any conclusions that do not mention these
+ parameters. See also @{cite "isabelle-isar-ref"} for the user-level
+ @{command obtain} and @{command guess} elements. Final results, which may
+ not refer to the parameters in the conclusion, need to exported explicitly
+ into the original context.\<close>
text %mlref \<open>
\begin{mldecls}
@@ -402,54 +388,54 @@
Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
\end{mldecls}
- \<^descr> @{ML SUBPROOF}~\<open>tac ctxt i\<close> decomposes the structure
- of the specified sub-goal, producing an extended context and a
- reduced goal, which needs to be solved by the given tactic. All
- schematic parameters of the goal are imported into the context as
- fixed ones, which may not be instantiated in the sub-proof.
+ \<^descr> @{ML SUBPROOF}~\<open>tac ctxt i\<close> decomposes the structure of the specified
+ sub-goal, producing an extended context and a reduced goal, which needs to
+ be solved by the given tactic. All schematic parameters of the goal are
+ imported into the context as fixed ones, which may not be instantiated in
+ the sub-proof.
\<^descr> @{ML Subgoal.FOCUS}, @{ML Subgoal.FOCUS_PREMS}, and @{ML
- Subgoal.FOCUS_PARAMS} are similar to @{ML SUBPROOF}, but are
- slightly more flexible: only the specified parts of the subgoal are
- imported into the context, and the body tactic may introduce new
- subgoals and schematic variables.
+ Subgoal.FOCUS_PARAMS} are similar to @{ML SUBPROOF}, but are slightly more
+ flexible: only the specified parts of the subgoal are imported into the
+ context, and the body tactic may introduce new subgoals and schematic
+ variables.
- \<^descr> @{ML Subgoal.focus}, @{ML Subgoal.focus_prems}, @{ML
- Subgoal.focus_params} extract the focus information from a goal
- state in the same way as the corresponding tacticals above. This is
- occasionally useful to experiment without writing actual tactics
- yet.
+ \<^descr> @{ML Subgoal.focus}, @{ML Subgoal.focus_prems}, @{ML Subgoal.focus_params}
+ extract the focus information from a goal state in the same way as the
+ corresponding tacticals above. This is occasionally useful to experiment
+ without writing actual tactics yet.
- \<^descr> @{ML Goal.prove}~\<open>ctxt xs As C tac\<close> states goal \<open>C\<close> in the context augmented by fixed variables \<open>xs\<close> and
- assumptions \<open>As\<close>, and applies tactic \<open>tac\<close> to solve
- it. The latter may depend on the local assumptions being presented
- as facts. The result is in HHF normal form.
+ \<^descr> @{ML Goal.prove}~\<open>ctxt xs As C tac\<close> states goal \<open>C\<close> in the context
+ augmented by fixed variables \<open>xs\<close> and assumptions \<open>As\<close>, and applies tactic
+ \<open>tac\<close> to solve it. The latter may depend on the local assumptions being
+ presented as facts. The result is in HHF normal form.
- \<^descr> @{ML Goal.prove_common}~\<open>ctxt fork_pri\<close> is the common form
- to state and prove a simultaneous goal statement, where @{ML Goal.prove}
- is a convenient shorthand that is most frequently used in applications.
+ \<^descr> @{ML Goal.prove_common}~\<open>ctxt fork_pri\<close> is the common form to state and
+ prove a simultaneous goal statement, where @{ML Goal.prove} is a convenient
+ shorthand that is most frequently used in applications.
The given list of simultaneous conclusions is encoded in the goal state by
- means of Pure conjunction: @{ML Goal.conjunction_tac} will turn this into
- a collection of individual subgoals, but note that the original multi-goal
+ means of Pure conjunction: @{ML Goal.conjunction_tac} will turn this into a
+ collection of individual subgoals, but note that the original multi-goal
state is usually required for advanced induction.
- It is possible to provide an optional priority for a forked proof,
- typically @{ML "SOME ~1"}, while @{ML NONE} means the proof is immediate
- (sequential) as for @{ML Goal.prove}. Note that a forked proof does not
- exhibit any failures in the usual way via exceptions in ML, but
- accumulates error situations under the execution id of the running
- transaction. Thus the system is able to expose error messages ultimately
- to the end-user, even though the subsequent ML code misses them.
+ It is possible to provide an optional priority for a forked proof, typically
+ @{ML "SOME ~1"}, while @{ML NONE} means the proof is immediate (sequential)
+ as for @{ML Goal.prove}. Note that a forked proof does not exhibit any
+ failures in the usual way via exceptions in ML, but accumulates error
+ situations under the execution id of the running transaction. Thus the
+ system is able to expose error messages ultimately to the end-user, even
+ though the subsequent ML code misses them.
- \<^descr> @{ML Obtain.result}~\<open>tac thms ctxt\<close> eliminates the
- given facts using a tactic, which results in additional fixed
- variables and assumptions in the context. Final results need to be
- exported explicitly.
+ \<^descr> @{ML Obtain.result}~\<open>tac thms ctxt\<close> eliminates the given facts using a
+ tactic, which results in additional fixed variables and assumptions in the
+ context. Final results need to be exported explicitly.
\<close>
-text %mlex \<open>The following minimal example illustrates how to access
- the focus information of a structured goal state.\<close>
+text %mlex \<open>
+ The following minimal example illustrates how to access the focus
+ information of a structured goal state.
+\<close>
notepad
begin
@@ -467,8 +453,9 @@
text \<open>
\<^medskip>
- The next example demonstrates forward-elimination in
- a local context, using @{ML Obtain.result}.\<close>
+ The next example demonstrates forward-elimination in a local context, using
+ @{ML Obtain.result}.
+\<close>
notepad
begin