# HG changeset patch # User wenzelm # Date 1157392179 -7200 # Node ID af069653f1d7516355ab5cbd7e1836e0f4189bb4 # Parent 7ef72f030679caf6e84ebe14116f6a686089c053 tuned; diff -r 7ef72f030679 -r af069653f1d7 doc-src/IsarImplementation/Thy/document/proof.tex --- 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 diff -r 7ef72f030679 -r af069653f1d7 doc-src/IsarImplementation/Thy/document/tactic.tex --- 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}% diff -r 7ef72f030679 -r af069653f1d7 doc-src/IsarImplementation/Thy/proof.thy --- 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 "\"}-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), \, A\<^isub>n(x) \ 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 - "\ B(x)"} and @{text "\ \x. B(x)"} are interchangeable provided that - @{text "x"} does not occur elsewhere in the context. Inspecting - @{text "\ \x. B(x)"} more closely, we see that inside the + "\ B(x)"} and @{text "\ \x. B(x)"} are interchangeable, provided + that @{text "x"} does not occur elsewhere in the context. + Inspecting @{text "\ \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 "\"}-elimination). + (thanks to @{text "\"} 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 "\ \x. B(x)"} has the canonical form @{text + universal result @{text "\ \x. B(x)"} has the HHF normal form @{text "\ B(?x)"}, which represents its generality nicely without requiring - an explicit quantifier. The same principle works for type variables - as well: @{text "\ B(?\)"} expresses the idea of ``@{text "\ + an explicit quantifier. The same principle works for type + variables: @{text "\ B(?\)"} represents the idea of ``@{text "\ \\. B(\)"}'' 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>\"} 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 "\ = x: term, \: type, A(x\<^isub>\)"}, where type - @{text "\"} is fixed \emph{after} term @{text "x"}, and the - constraint @{text "x: \"} is an implicit consequence of the - occurrence of @{text "x\<^isub>\"} in the subsequent proposition. + @{text "x\<^isub>\"} 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 "\ = x: term, \: type, A(x\<^isub>\)"}, where type @{text + "\"} is fixed \emph{after} term @{text "x"}, and the constraint + @{text "x :: \"} is an implicit consequence of the occurrence of + @{text "x\<^isub>\"} 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 "\"} is considered fixed as long as it occurs in some fixed term variable of the context. For example, exporting @{text "x: - term, \: type \ x\<^isub>\ = x\<^isub>\"} produces @{text "x: term \ - x\<^isub>\ = x\<^isub>\"} for fixed @{text "\"} in the first step, - and @{text "\ ?x\<^isub>?\<^isub>\ = ?x\<^isub>?\<^isub>\"} for - schematic @{text "?x"} and @{text "?\"} only in the second step. + term, \: type \ x\<^isub>\ = x\<^isub>\"} produces in the first step + @{text "x: term \ x\<^isub>\ = x\<^isub>\"} for fixed @{text "\"}, + and only in the second step @{text "\ ?x\<^isub>?\<^isub>\ = + ?x\<^isub>?\<^isub>\"} for schematic @{text "?x"} and @{text "?\"}. \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 - "\x. B(x)"} is decomposed by inventing a fixed variable @{text "x"} - and for the body @{text "B(x)"}. + "\x\<^isub>1 \ x\<^isub>n. B(x\<^isub>1, \, x\<^isub>n)"} is + decomposed by inventing fixed variables @{text "x\<^isub>1, \, + 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 "\x\<^isub>1 \ - x\<^isub>n. B(x\<^isub>1, \, x\<^isub>n)"} invents fixed variables - for @{text "x\<^isub>1, \, x\<^isub>n"} and replaces these in the - body. + \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text + "\"} 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 "\x :: \. P - x"} we get @{text "\x :: \. P x \ P ?x"} for arbitrary @{text "?x"} - of the fixed type @{text "\"}. Local derivations accumulate more - and more explicit references to hypotheses: @{text "A\<^isub>1, \, + x"} we get @{text "\x :: \. P x \ P ?x"} for schematic @{text "?x"} + of fixed type @{text "\"}. Local derivations accumulate more and + more explicit references to hypotheses: @{text "A\<^isub>1, \, A\<^isub>n \ B"} where @{text "A\<^isub>1, \, A\<^isub>n"} needs to be covered by the assumptions of the current context. @@ -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 "#\_intro"})]{@{text "\ \\ A \ #A \ B"}}{@{text "\ \ 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 \ t"}, with the following export rule to reverse the effect: \[ \infer{@{text "\ \\ x \ t \ B t"}}{@{text "\ \ B x"}} \] - - \medskip The general concept supports block-structured reasoning - nicely, with arbitrary mechanisms for introducing local assumptions. - The common reasoning pattern is as follows: - - \medskip - \begin{tabular}{l} - @{text "add_assms e\<^isub>1 A\<^isub>1"} \\ - @{text "\"} \\ - @{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, \, A\<^isub>n \ B"} into some @{text "\ B'"}, by - applying the export rules @{text "e\<^isub>1, \, e\<^isub>n"} - inside-out. + This works, because the assumption @{text "x \ t"} was introduced in + a context with @{text "x"} being fresh, so @{text "x"} does not + occur in @{text "\"} here. *} text %mlref {* @@ -241,17 +227,17 @@ "A"} into a raw assumption @{text "A \ A'"}, where the conclusion @{text "A'"} is in HHF normal form. - \item @{ML Assumption.add_assms}~@{text "e As"} augments the context - by 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 "\_intro"} or @{text "#\_intro"}, depending on goal mode. - \item @{ML Assumption.export}~@{text "is_goal inner outer th"} - exports result @{text "th"} from the the @{text "inner"} context + \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 "\/\"} elimination, resolution rules, or - equational reasoning. Unaccounted context manipulations should be - ruled out, such as raw @{text "\/\"} introduction or ad-hoc + within a context. This allows common combinations of theorems, + e.g.\ via @{text "\/\"} elimination, resolution rules, or equational + reasoning, see \secref{sec:thms}. Unaccounted context manipulations + should be avoided, notably raw @{text "\/\"} 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 "(\x. A(x) \ B(x)) \ \"} - is turned into @{text "B(x) \ \"} after fixing @{text "x"} and - assuming @{text "A(x)"}. + \medskip Tactical proofs may be structured recursively by + decomposing a sub-goal: @{text "(\x. A(x) \ B(x)) \ \"} is turned + into @{text "B(x) \ \"} 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 "\xs. As \ C"}, but is normalized - by pulling @{text "\"} before @{text "\"} (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 diff -r 7ef72f030679 -r af069653f1d7 doc-src/IsarImplementation/Thy/tactic.thy --- 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 "\x\<^sub>1 \ - \x\<^sub>k. H\<^sub>1 \ \ \ H\<^sub>m \ B"} according to the normal - form where any local @{text \} is pulled before @{text \}. Here - @{text "x\<^sub>1, \, x\<^sub>k"} are goal parameters, i.e.\ + \x\<^sub>k. H\<^sub>1 \ \ \ H\<^sub>m \ B"} in normal form where. + Here @{text "x\<^sub>1, \, x\<^sub>k"} are goal parameters, i.e.\ arbitrary-but-fixed entities of certain types, and @{text "H\<^sub>1, \, 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 "\"} initializes a tactical goal from - the type-checked proposition @{text \}. + \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} *} diff -r 7ef72f030679 -r af069653f1d7 doc-src/IsarImplementation/Thy/unused.thy --- 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 "\"} \\ + @{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, \, A\<^isub>n \ B"} into some @{text "\ B'"}, by + applying the export rules @{text "e\<^isub>1, \, e\<^isub>n"} + inside-out. A \emph{fixed variable} acts like a local constant in the current