--- 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