--- a/doc-src/IsarImplementation/Thy/document/proof.tex Mon Sep 04 18:41:33 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Mon Sep 04 19:49:39 2006 +0200
@@ -23,29 +23,29 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Variables%
+\isamarkupsection{Variables \label{sec:variables}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Any variable that is not explicitly bound by \isa{{\isasymlambda}}-abstraction
is considered as ``free''. Logically, free variables act like
- outermost universal quantification (at the sequent level): \isa{A\isactrlisub {\isadigit{1}}{\isacharparenleft}x{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n{\isacharparenleft}x{\isacharparenright}\ {\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} means that the result
+ outermost universal quantification at the sequent level: \isa{A\isactrlisub {\isadigit{1}}{\isacharparenleft}x{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n{\isacharparenleft}x{\isacharparenright}\ {\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} means that the result
holds \emph{for all} values of \isa{x}. Free variables for
- terms (not types) can be fully internalized into the logic: \isa{{\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} are interchangeable provided that
- \isa{x} does not occur elsewhere in the context. Inspecting
- \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} more closely, we see that inside the
+ terms (not types) can be fully internalized into the logic: \isa{{\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} are interchangeable, provided
+ that \isa{x} does not occur elsewhere in the context.
+ Inspecting \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} more closely, we see that inside the
quantifier, \isa{x} is essentially ``arbitrary, but fixed'',
while from outside it appears as a place-holder for instantiation
- (thanks to \isa{{\isasymAnd}}-elimination).
+ (thanks to \isa{{\isasymAnd}} elimination).
- The Pure logic represents the notion of variables being either
- inside or outside the current scope by providing separate syntactic
+ The Pure logic represents the idea of variables being either inside
+ or outside the current scope by providing separate syntactic
categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\
\emph{schematic variables} (e.g.\ \isa{{\isacharquery}x}). Incidently, a
- universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the canonical form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality nicely without requiring
- an explicit quantifier. The same principle works for type variables
- as well: \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} expresses the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}'' without demanding a truly polymorphic framework.
+ universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality nicely without requiring
+ an explicit quantifier. The same principle works for type
+ variables: \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}'' 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
@@ -57,37 +57,42 @@
We allow a slightly less formalistic mode of operation: term
variables \isa{x} are fixed without specifying a type yet
(essentially \emph{all} potential occurrences of some instance
- \isa{x\isactrlisub {\isasymtau}} will be fixed); the first occurrence of \isa{x} within a specific term assigns its most general type, which is
- then maintained consistently in the context. The above example
- becomes \isa{{\isasymGamma}\ {\isacharequal}\ x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}, where type
- \isa{{\isasymalpha}} is fixed \emph{after} term \isa{x}, and the
- constraint \isa{x{\isacharcolon}\ {\isasymalpha}} is an implicit consequence of the
- occurrence of \isa{x\isactrlisub {\isasymalpha}} in the subsequent proposition.
+ \isa{x\isactrlisub {\isasymtau}} are fixed); the first occurrence of \isa{x}
+ within a specific term assigns its most general type, which is then
+ maintained consistently in the context. The above example becomes
+ \isa{{\isasymGamma}\ {\isacharequal}\ x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}, where type \isa{{\isasymalpha}} is fixed \emph{after} term \isa{x}, and the constraint
+ \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}} is an implicit consequence of the occurrence of
+ \isa{x\isactrlisub {\isasymalpha}} in the subsequent proposition.
This twist of dependencies is also accommodated by the reverse
operation of exporting results from a context: a type variable
\isa{{\isasymalpha}} is considered fixed as long as it occurs in some fixed
- term variable of the context. For example, exporting \isa{x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} produces \isa{x{\isacharcolon}\ term\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} for fixed \isa{{\isasymalpha}} in the first step,
- and \isa{{\isasymturnstile}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}\ {\isacharequal}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}} for
- schematic \isa{{\isacharquery}x} and \isa{{\isacharquery}{\isasymalpha}} only in the second step.
+ term variable of the context. For example, exporting \isa{x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} produces in the first step
+ \isa{x{\isacharcolon}\ term\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} for fixed \isa{{\isasymalpha}},
+ and only in the second step \isa{{\isasymturnstile}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}\ {\isacharequal}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}} for schematic \isa{{\isacharquery}x} and \isa{{\isacharquery}{\isasymalpha}}.
\medskip The Isabelle/Isar proof context manages the gory details of
term vs.\ type variables, with high-level principles for moving the
- frontier between fixed and schematic variables. By observing a
- simple discipline of fixing variables and declaring terms
- explicitly, the fine points are treated by the \isa{export}
- operation.
+ frontier between fixed and schematic variables.
+
+ The \isa{add{\isacharunderscore}fixes} operation explictly declares fixed
+ variables; the \isa{declare{\isacharunderscore}term} operation absorbs a term into
+ a context by fixing new type variables and adding syntactic
+ constraints.
- There is also a separate \isa{import} 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 \isa{export} later, with a potentially extended context,
- but the result will be only equivalent modulo renaming of schematic
- variables.
+ The \isa{export} 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 \isa{import} 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 \isa{export} later,
+ potentially with an extended context; the result is equivalent to
+ the original modulo renaming of schematic variables.
The \isa{focus} operation provides a variant of \isa{import}
- for nested propositions (with explicit quantification): \isa{{\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} is decomposed by inventing a fixed variable \isa{x}
- and for the body \isa{B{\isacharparenleft}x{\isacharparenright}}.%
+ for nested propositions (with explicit quantification): \isa{{\isasymAnd}x\isactrlisub {\isadigit{1}}\ {\isasymdots}\ x\isactrlisub n{\isachardot}\ B{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n{\isacharparenright}} is
+ decomposed by inventing fixed variables \isa{x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n} for the body.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -99,14 +104,16 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexml{Variable.add-fixes}\verb|Variable.add_fixes: string list -> Proof.context -> string list * Proof.context| \\
- \indexml{Variable.invent-fixes}\verb|Variable.invent_fixes: string list -> Proof.context -> string list * Proof.context| \\
+ \indexml{Variable.add-fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
+\verb| string list -> Proof.context -> string list * Proof.context| \\
+ \indexml{Variable.invent-fixes}\verb|Variable.invent_fixes: |\isasep\isanewline%
+\verb| string list -> Proof.context -> string list * Proof.context| \\
\indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
\indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
\indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
\indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
- \indexml{Variable.import}\verb|Variable.import: bool ->|\isasep\isanewline%
-\verb| thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context| \\
+ \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
+\verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\
\indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
\end{mldecls}
@@ -115,21 +122,21 @@
\item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term
variables \isa{xs}, returning the resulting internal names. By
default, the internal representation coincides with the external
- one, which also means that the given variables must not have been
- fixed already. Within a local proof body, the given names are just
- hints for newly invented Skolem variables.
+ 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.
\item \verb|Variable.invent_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
- hints.
+ names.
\item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term
\isa{t} 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.
+ type and term variables are declared uniformly, though.
- \item \verb|Variable.declare_constraints|~\isa{t\ ctxt} derives
- type-inference information from term \isa{t}, without making it
- part of the context yet.
+ \item \verb|Variable.declare_constraints|~\isa{t\ ctxt} declares
+ syntactic constraints from term \isa{t}, without making it part
+ of the context yet.
\item \verb|Variable.export|~\isa{inner\ outer\ thms} generalizes
fixed type and term variables in \isa{thms} according to the
@@ -139,21 +146,16 @@
\item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
variables in \isa{ts} as far as possible, even those occurring
in fixed term variables. The default policy of type-inference is to
- fix newly introduced type variables; this is essentially reversed
- with \verb|Variable.polymorphic|, the given terms are detached from
- the context as far as possible.
+ fix newly introduced type variables, which is essentially reversed
+ with \verb|Variable.polymorphic|: here the given terms are detached
+ from the context as far as possible.
- \item \verb|Variable.import|~\isa{open\ thms\ ctxt} augments the
- context by new fixes for the schematic type and term variables
- occurring in \isa{thms}. The \isa{open} flag indicates
- whether the fixed names should be accessible to the user, otherwise
- internal names are chosen.
+ \item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed
+ type and term variables for the schematic ones occurring in \isa{thms}. The \isa{open} flag indicates whether the fixed names
+ should be accessible to the user, otherwise newly introduced names
+ are marked as ``internal'' (\secref{sec:names}).
- \verb|Variable.export| essentially reverses the effect of \verb|Variable.import|, modulo renaming of schematic variables.
-
- \item \verb|Variable.focus|~\isa{{\isasymAnd}x\isactrlisub {\isadigit{1}}\ {\isasymdots}\ x\isactrlisub n{\isachardot}\ B{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n{\isacharparenright}} invents fixed variables
- for \isa{x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n} and replaces these in the
- body.
+ \item \verb|Variable.focus|~\isa{B} decomposes the outermost \isa{{\isasymAnd}} prefix of proposition \isa{B}.
\end{description}%
\end{isamarkuptext}%
@@ -166,12 +168,7 @@
%
\endisadelimmlref
%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Assumptions%
+\isamarkupsection{Assumptions \label{sec:assumptions}%
}
\isamarkuptrue%
%
@@ -181,12 +178,12 @@
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.
+ 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 \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
+ 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 schematic \isa{{\isacharquery}x}
+ of 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}assms} operation augments the context by
@@ -208,37 +205,23 @@
\]
The variant for goal refinements marks the newly introduced
- premises, which causes the builtin goal refinement scheme of Isar to
+ premises, which causes the canonical Isar goal refinement scheme 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 assumptions may perform arbitrary
- transformations on export, as long as a particular portion of
+ \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 \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}assms\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\
- \isa{{\isasymdots}} \\
- \isa{add{\isacharunderscore}assms\ 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.%
+ This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in
+ a context with \isa{x} being fresh, so \isa{x} does not
+ occur in \isa{{\isasymGamma}} here.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -269,15 +252,16 @@
\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 assumptions \isa{As} with export rule \isa{e}. The
- resulting facts are hypothetical theorems as produced by \verb|Assumption.assume|.
+ \item \verb|Assumption.add_assms|~\isa{r\ As} augments the context
+ by assumptions \isa{As} with export rule \isa{r}. The
+ resulting facts are hypothetical theorems as produced by the raw
+ \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
+ \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ thm}
+ exports result \isa{thm} from the the \isa{inner} context
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|
@@ -300,28 +284,29 @@
%
\begin{isamarkuptext}%
Local results are established by monotonic reasoning from facts
- within a context. This admits arbitrary combination of theorems,
- e.g.\ using \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or
- equational reasoning. Unaccounted context manipulations should be
- ruled out, such as raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc
+ within a context. This allows common combinations of theorems,
+ e.g.\ via \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or equational
+ reasoning, see \secref{sec:thms}. Unaccounted context manipulations
+ should be avoided, notably raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc
references to free variables or assumptions not present in the proof
context.
- \medskip The \isa{prove} operation provides a separate interface
- for structured backwards reasoning under program control, with some
+ \medskip The \isa{prove} 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 locally by given fixed variables and assumptions, which
- will be available as local facts during the proof and discharged
- into implications in the result.
+ 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 \isa{prove{\isacharunderscore}multi} operation handles several simultaneous
- claims within a single goal statement, by using meta-level
- conjunction internally.
+ claims within a single goal, by using Pure conjunction internally.
- \medskip The tactical proof of a local claim may be structured
- further by decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}}
- is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and
- assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.%
+ \medskip Tactical proofs may be structured recursively by
+ decomposing a sub-goal: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned
+ into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -344,12 +329,10 @@
\begin{description}
- \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of fixed variables \isa{xs} and assumptions
- \isa{As} and applies tactic \isa{tac} to solve it. The
- latter may depend on the local assumptions being presented as facts.
- The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized
- by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}} (the conclusion \isa{C} itself may be a rule statement), turning the quantifier prefix
- into schematic variables, and generalizing implicit type-variables.
+ \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and
+ assumptions \isa{As}, and applies tactic \isa{tac} to solve
+ it. The latter may depend on the local assumptions being presented
+ as facts. The result is in HHF normal form.
\item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex Mon Sep 04 18:41:33 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Mon Sep 04 19:49:39 2006 +0200
@@ -24,14 +24,12 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The basic idea of tactical theorem proving is to refine the initial
- claim in a backwards fashion, until a solved form is reached. An
- intermediate goal consists of several subgoals that need to be
- solved in order to achieve the main statement; zero subgoals means
- that the proof may be finished. A \isa{tactic} is a refinement
- operation that maps a goal to a lazy sequence of potential
- successors. A \isa{tactical} is a combinator for composing
- tactics.%
+Tactical reasoning works by refining the initial claim in a
+ backwards fashion, until a solved form is reached. A \isa{goal}
+ consists of several subgoals that need to be solved in order to
+ achieve the main statement; zero subgoals means that the proof may
+ be finished. A \isa{tactic} is a refinement operation that maps
+ a goal to a lazy sequence of potential successors. A \isa{tactical} is a combinator for composing tactics.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -55,14 +53,13 @@
reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is called ``solved''.
The structure of each subgoal \isa{A\isactrlsub i} is that of a
- general Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} according to the normal
- form where any local \isa{{\isasymAnd}} is pulled before \isa{{\isasymLongrightarrow}}. Here
- \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\
+ general Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} in normal form where.
+ Here \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\
arbitrary-but-fixed entities of certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal hypotheses, i.e.\ facts that may
be assumed locally. Together, this forms the goal context of the
conclusion \isa{B} to be established. The goal hypotheses may be
- again Hereditary Harrop Formulas, although the level of nesting
- rarely exceeds 1--2 in practice.
+ again arbitrary Hereditary Harrop Formulas, although the level of
+ nesting rarely exceeds 1--2 in practice.
The main conclusion \isa{C} is internally marked as a protected
proposition\glossary{Protected proposition}{An arbitrarily
@@ -70,8 +67,9 @@
atomic by wrapping it into a propositional identity operator;
notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic
inferences from entering into that structure for the time being.},
- which is occasionally represented explicitly by the notation \isa{{\isacharhash}C}. This ensures that the decomposition into subgoals and main
- conclusion is well-defined for arbitrarily structured claims.
+ which is represented explicitly by the notation \isa{{\isacharhash}C}. This
+ ensures that the decomposition into subgoals and main conclusion is
+ well-defined for arbitrarily structured claims.
\medskip Basic goal management is performed via the following
Isabelle/Pure rules:
@@ -107,17 +105,18 @@
\begin{description}
- \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal from
- the type-checked proposition \isa{{\isasymphi}}.
-
- \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (no subgoals), and concludes
- the result by removing the goal protection.
+ \item \verb|Goal.init|~\isa{C} initializes a tactical goal from
+ the well-formed proposition \isa{C}.
- \item \verb|Goal.protect|~\isa{th} protects the full statement
- of theorem \isa{th}.
+ \item \verb|Goal.finish|~\isa{thm} checks whether theorem
+ \isa{thm} is a solved goal (no subgoals), and concludes the
+ result by removing the goal protection.
- \item \verb|Goal.conclude|~\isa{th} removes the goal protection
- for any number of pending subgoals.
+ \item \verb|Goal.protect|~\isa{thm} protects the full statement
+ of theorem \isa{thm}.
+
+ \item \verb|Goal.conclude|~\isa{thm} removes the goal
+ protection, even if there are pending subgoals.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/proof.thy Mon Sep 04 18:41:33 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Mon Sep 04 19:49:39 2006 +0200
@@ -5,30 +5,30 @@
chapter {* Structured proofs *}
-section {* Variables *}
+section {* Variables \label{sec:variables} *}
text {*
Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
is considered as ``free''. Logically, free variables act like
- outermost universal quantification (at the sequent level): @{text
+ outermost universal quantification at the sequent level: @{text
"A\<^isub>1(x), \<dots>, A\<^isub>n(x) \<turnstile> B(x)"} means that the result
holds \emph{for all} values of @{text "x"}. Free variables for
terms (not types) can be fully internalized into the logic: @{text
- "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable provided that
- @{text "x"} does not occur elsewhere in the context. Inspecting
- @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
+ "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
+ that @{text "x"} does not occur elsewhere in the context.
+ Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
while from outside it appears as a place-holder for instantiation
- (thanks to @{text "\<And>"}-elimination).
+ (thanks to @{text "\<And>"} elimination).
- The Pure logic represents the notion of variables being either
- inside or outside the current scope by providing separate syntactic
+ The Pure logic represents the idea of variables being either inside
+ or outside the current scope by providing separate syntactic
categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
\emph{schematic variables} (e.g.\ @{text "?x"}). Incidently, a
- universal result @{text "\<turnstile> \<And>x. B(x)"} has the canonical form @{text
+ universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
"\<turnstile> B(?x)"}, which represents its generality nicely without requiring
- an explicit quantifier. The same principle works for type variables
- as well: @{text "\<turnstile> B(?\<alpha>)"} expresses the idea of ``@{text "\<turnstile>
+ an explicit quantifier. The same principle works for type
+ variables: @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile>
\<forall>\<alpha>. B(\<alpha>)"}'' without demanding a truly polymorphic framework.
\medskip Additional care is required to treat type variables in a
@@ -41,53 +41,61 @@
We allow a slightly less formalistic mode of operation: term
variables @{text "x"} are fixed without specifying a type yet
(essentially \emph{all} potential occurrences of some instance
- @{text "x\<^isub>\<tau>"} will be fixed); the first occurrence of @{text
- "x"} within a specific term assigns its most general type, which is
- then maintained consistently in the context. The above example
- becomes @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type
- @{text "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the
- constraint @{text "x: \<alpha>"} is an implicit consequence of the
- occurrence of @{text "x\<^isub>\<alpha>"} in the subsequent proposition.
+ @{text "x\<^isub>\<tau>"} are fixed); the first occurrence of @{text "x"}
+ within a specific term assigns its most general type, which is then
+ maintained consistently in the context. The above example becomes
+ @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type @{text
+ "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
+ @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
+ @{text "x\<^isub>\<alpha>"} in the subsequent proposition.
This twist of dependencies is also accommodated by the reverse
operation of exporting results from a context: a type variable
@{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
term variable of the context. For example, exporting @{text "x:
- term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} produces @{text "x: term \<turnstile>
- x\<^isub>\<alpha> = x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"} in the first step,
- and @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> = ?x\<^isub>?\<^isub>\<alpha>"} for
- schematic @{text "?x"} and @{text "?\<alpha>"} only in the second step.
+ term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} produces in the first step
+ @{text "x: term \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"},
+ and only in the second step @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> =
+ ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
\medskip The Isabelle/Isar proof context manages the gory details of
term vs.\ type variables, with high-level principles for moving the
- frontier between fixed and schematic variables. By observing a
- simple discipline of fixing variables and declaring terms
- explicitly, the fine points are treated by the @{text "export"}
- operation.
+ frontier between fixed and schematic variables.
+
+ The @{text "add_fixes"} operation explictly declares fixed
+ variables; the @{text "declare_term"} operation absorbs a term into
+ a context by fixing new type variables and adding syntactic
+ constraints.
- There is also a separate @{text "import"} 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 @{text "export"} later, with a potentially extended context,
- but the result will be only equivalent modulo renaming of schematic
- variables.
+ The @{text "export"} 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 @{text "import"} 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 @{text "export"} later,
+ potentially with an extended context; the result is equivalent to
+ the original modulo renaming of schematic variables.
The @{text "focus"} operation provides a variant of @{text "import"}
for nested propositions (with explicit quantification): @{text
- "\<And>x. B(x)"} is decomposed by inventing a fixed variable @{text "x"}
- and for the body @{text "B(x)"}.
+ "\<And>x\<^isub>1 \<dots> x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} is
+ decomposed by inventing fixed variables @{text "x\<^isub>1, \<dots>,
+ x\<^isub>n"} for the body.
*}
text %mlref {*
\begin{mldecls}
- @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
- @{index_ML Variable.invent_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
+ @{index_ML Variable.add_fixes: "
+ string list -> Proof.context -> string list * Proof.context"} \\
+ @{index_ML Variable.invent_fixes: "
+ string list -> Proof.context -> string list * Proof.context"} \\
@{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
@{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
@{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
- @{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.focus: "cterm -> Proof.context -> (cterm list * cterm) * Proof.context"} \\
\end{mldecls}
@@ -96,22 +104,22 @@
\item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
variables @{text "xs"}, returning the resulting internal names. By
default, the internal representation coincides with the external
- one, which also means that the given variables must not have been
- fixed already. Within a local proof body, the given names are just
- hints for newly invented Skolem variables.
+ 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.
\item @{ML Variable.invent_fixes} is similar to @{ML
Variable.add_fixes}, but always produces fresh variants of the given
- hints.
+ names.
\item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
@{text "t"} 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.
+ type and term variables are declared uniformly, though.
- \item @{ML Variable.declare_constraints}~@{text "t ctxt"} derives
- type-inference information from term @{text "t"}, without making it
- part of the context yet.
+ \item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares
+ syntactic constraints from term @{text "t"}, without making it part
+ of the context yet.
\item @{ML Variable.export}~@{text "inner outer thms"} generalizes
fixed type and term variables in @{text "thms"} according to the
@@ -121,31 +129,24 @@
\item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
variables in @{text "ts"} as far as possible, even those occurring
in fixed term variables. The default policy of type-inference is to
- fix newly introduced type variables; this is essentially reversed
- with @{ML Variable.polymorphic}, the given terms are detached from
- the context as far as possible.
+ 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.
- \item @{ML Variable.import}~@{text "open thms ctxt"} augments the
- context by new fixes for the schematic type and term variables
- occurring in @{text "thms"}. The @{text "open"} flag indicates
- whether the fixed names should be accessible to the user, otherwise
- internal names are chosen.
+ \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
+ type and term variables for the schematic ones occurring in @{text
+ "thms"}. The @{text "open"} flag indicates whether the fixed names
+ should be accessible to the user, otherwise newly introduced names
+ are marked as ``internal'' (\secref{sec:names}).
- @{ML Variable.export} essentially reverses the effect of @{ML
- Variable.import}, modulo renaming of schematic variables.
-
- \item @{ML Variable.focus}~@{text "\<And>x\<^isub>1 \<dots>
- x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} invents fixed variables
- for @{text "x\<^isub>1, \<dots>, x\<^isub>n"} and replaces these in the
- body.
+ \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
+ "\<And>"} prefix of proposition @{text "B"}.
\end{description}
*}
-text FIXME
-
-section {* Assumptions *}
+section {* Assumptions \label{sec:assumptions} *}
text {*
An \emph{assumption} is a proposition that it is postulated in the
@@ -153,13 +154,13 @@
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.
+ 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 @{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>,
+ x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
+ of 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.
@@ -183,38 +184,23 @@
\]
The variant for goal refinements marks the newly introduced
- premises, which causes the builtin goal refinement scheme of Isar to
+ premises, which causes the canonical Isar goal refinement scheme 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 assumptions may perform arbitrary
- transformations on export, as long as a particular portion of
+ \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 @{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_assms e\<^isub>1 A\<^isub>1"} \\
- @{text "\<dots>"} \\
- @{text "add_assms 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.
+ This works, because the assumption @{text "x \<equiv> t"} was introduced in
+ a context with @{text "x"} being fresh, so @{text "x"} does not
+ occur in @{text "\<Gamma>"} here.
*}
text %mlref {*
@@ -241,17 +227,17 @@
"A"} into a raw assumption @{text "A \<turnstile> A'"}, where the conclusion
@{text "A'"} is in HHF normal form.
- \item @{ML Assumption.add_assms}~@{text "e As"} augments the context
- 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_assms}~@{text "r As"} augments the context
+ by assumptions @{text "As"} with export rule @{text "r"}. The
+ resulting facts are hypothetical theorems as produced by the raw
+ @{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
"\<Longrightarrow>_intro"} or @{text "#\<Longrightarrow>_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
+ \item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
+ exports result @{text "thm"} from the the @{text "inner"} context
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"}
@@ -265,28 +251,30 @@
text {*
Local results are established by monotonic reasoning from facts
- within a context. This admits arbitrary combination of theorems,
- e.g.\ using @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or
- equational reasoning. Unaccounted context manipulations should be
- ruled out, such as raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
+ within a context. This allows common combinations of theorems,
+ e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational
+ reasoning, see \secref{sec:thms}. Unaccounted context manipulations
+ should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
references to free variables or assumptions not present in the proof
context.
- \medskip The @{text "prove"} operation provides a separate interface
- for structured backwards reasoning under program control, with some
+ \medskip The @{text "prove"} 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 locally by given fixed variables and assumptions, which
- will be available as local facts during the proof and discharged
- into implications in the result.
+ 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 @{text "prove_multi"} operation handles several simultaneous
- claims within a single goal statement, by using meta-level
- conjunction internally.
+ claims within a single goal, by using Pure conjunction internally.
- \medskip The tactical proof of a local claim may be structured
- further by decomposing a sub-goal: @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"}
- is turned into @{text "B(x) \<Longrightarrow> \<dots>"} after fixing @{text "x"} and
- assuming @{text "A(x)"}.
+ \medskip Tactical proofs may be structured recursively by
+ decomposing a sub-goal: @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned
+ into @{text "B(x) \<Longrightarrow> \<dots>"} after fixing @{text "x"} and assuming @{text
+ "A(x)"}.
*}
text %mlref {*
@@ -304,13 +292,10 @@
\begin{description}
\item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
- "C"} in the context of fixed variables @{text "xs"} and assumptions
- @{text "As"} and applies tactic @{text "tac"} to solve it. The
- latter may depend on the local assumptions being presented as facts.
- The result is essentially @{text "\<And>xs. As \<Longrightarrow> C"}, but is normalized
- by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"} (the conclusion @{text
- "C"} itself may be a rule statement), turning the quantifier prefix
- into schematic variables, and generalizing implicit type-variables.
+ "C"} in the context augmented by fixed variables @{text "xs"} and
+ assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
+ it. The latter may depend on the local assumptions being presented
+ as facts. The result is in HHF normal form.
\item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
states several conclusions simultaneously. @{ML
--- a/doc-src/IsarImplementation/Thy/tactic.thy Mon Sep 04 18:41:33 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy Mon Sep 04 19:49:39 2006 +0200
@@ -6,14 +6,13 @@
chapter {* Tactical reasoning *}
text {*
- The basic idea of tactical theorem proving is to refine the initial
- claim in a backwards fashion, until a solved form is reached. An
- intermediate goal consists of several subgoals that need to be
- solved in order to achieve the main statement; zero subgoals means
- that the proof may be finished. A @{text "tactic"} is a refinement
- operation that maps a goal to a lazy sequence of potential
- successors. A @{text "tactical"} is a combinator for composing
- tactics.
+ Tactical reasoning works by refining the initial claim in a
+ backwards fashion, until a solved form is reached. A @{text "goal"}
+ consists of several subgoals that need to be solved in order to
+ achieve the main statement; zero subgoals means that the proof may
+ be finished. A @{text "tactic"} is a refinement operation that maps
+ a goal to a lazy sequence of potential successors. A @{text
+ "tactical"} is a combinator for composing tactics.
*}
@@ -38,15 +37,14 @@
The structure of each subgoal @{text "A\<^sub>i"} is that of a
general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
- \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal
- form where any local @{text \<And>} is pulled before @{text \<Longrightarrow>}. Here
- @{text "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
+ \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} in normal form where.
+ Here @{text "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
arbitrary-but-fixed entities of certain types, and @{text
"H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
be assumed locally. Together, this forms the goal context of the
conclusion @{text B} to be established. The goal hypotheses may be
- again Hereditary Harrop Formulas, although the level of nesting
- rarely exceeds 1--2 in practice.
+ again arbitrary Hereditary Harrop Formulas, although the level of
+ nesting rarely exceeds 1--2 in practice.
The main conclusion @{text C} is internally marked as a protected
proposition\glossary{Protected proposition}{An arbitrarily
@@ -54,9 +52,9 @@
atomic by wrapping it into a propositional identity operator;
notation @{text "#C"}. Protecting a proposition prevents basic
inferences from entering into that structure for the time being.},
- which is occasionally represented explicitly by the notation @{text
- "#C"}. This ensures that the decomposition into subgoals and main
- conclusion is well-defined for arbitrarily structured claims.
+ which is represented explicitly by the notation @{text "#C"}. This
+ ensures that the decomposition into subgoals and main conclusion is
+ well-defined for arbitrarily structured claims.
\medskip Basic goal management is performed via the following
Isabelle/Pure rules:
@@ -85,18 +83,18 @@
\begin{description}
- \item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal from
- the type-checked proposition @{text \<phi>}.
+ \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
+ the well-formed proposition @{text C}.
- \item @{ML "Goal.finish"}~@{text "th"} checks whether theorem @{text
- "th"} is a solved goal configuration (no subgoals), and concludes
- the result by removing the goal protection.
+ \item @{ML "Goal.finish"}~@{text "thm"} checks whether theorem
+ @{text "thm"} is a solved goal (no subgoals), and concludes the
+ result by removing the goal protection.
- \item @{ML "Goal.protect"}~@{text "th"} protects the full statement
- of theorem @{text "th"}.
+ \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement
+ of theorem @{text "thm"}.
- \item @{ML "Goal.conclude"}~@{text "th"} removes the goal protection
- for any number of pending subgoals.
+ \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
+ protection, even if there are pending subgoals.
\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/unused.thy Mon Sep 04 18:41:33 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/unused.thy Mon Sep 04 19:49:39 2006 +0200
@@ -1,6 +1,24 @@
text {*
+
+ \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_assms e\<^isub>1 A\<^isub>1"} \\
+ @{text "\<dots>"} \\
+ @{text "add_assms 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.
A \emph{fixed variable} acts like a local constant in the current