# HG changeset patch # User wenzelm # Date 1265112664 -3600 # Node ID f3bce1cc513ca3bb52ff992c1abed2de67cb2f22 # Parent 9700a87f1cc240295829db1a7212499a88d7a5d8 added Subgoal.FOCUS; misc tuning and clarification; diff -r 9700a87f1cc2 -r f3bce1cc513c doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Tue Feb 02 12:37:57 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Tue Feb 02 13:11:04 2010 +0100 @@ -25,10 +25,10 @@ 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 HHF normal form @{text - "\ B(?x)"}, which represents its generality nicely without requiring - an explicit quantifier. The same principle works for type - variables: @{text "\ B(?\)"} represents the idea of ``@{text "\ - \\. B(\)"}'' without demanding a truly polymorphic framework. + "\ B(?x)"}, which represents its generality without requiring 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 way that facilitates type-inference. In principle, term variables @@ -95,7 +95,8 @@ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ @{index_ML Variable.import: "bool -> thm list -> Proof.context -> (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\ - @{index_ML Variable.focus: "cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context"} \\ + @{index_ML Variable.focus: "cterm -> Proof.context -> + ((string * cterm) list * cterm) * Proof.context"} \\ \end{mldecls} \begin{description} @@ -171,21 +172,21 @@ context into a (smaller) outer context, by discharging the difference of the assumptions as specified by the associated export rules. Note that the discharged portion is determined by the - difference contexts, not the facts being exported! There is a + difference of contexts, not the facts being exported! There is a separate flag to indicate a goal context, where the result is meant to refine an enclosing sub-goal of a structured proof state. \medskip The most basic export rule discharges assumptions directly by means of the @{text "\"} introduction rule: \[ - \infer[(@{text "\_intro"})]{@{text "\ \\ A \ A \ B"}}{@{text "\ \ B"}} + \infer[(@{text "\\intro"})]{@{text "\ - A \ A \ B"}}{@{text "\ \ B"}} \] The variant for goal refinements marks the newly introduced premises, which causes the canonical Isar goal refinement scheme to enforce unification with local premises within the goal: \[ - \infer[(@{text "#\_intro"})]{@{text "\ \\ A \ #A \ B"}}{@{text "\ \ B"}} + \infer[(@{text "#\\intro"})]{@{text "\ - A \ #A \ B"}}{@{text "\ \ B"}} \] \medskip Alternative versions of assumptions may perform arbitrary @@ -194,7 +195,7 @@ definition works by fixing @{text "x"} and assuming @{text "x \ t"}, with the following export rule to reverse the effect: \[ - \infer[(@{text "\-expand"})]{@{text "\ \\ x \ t \ B t"}}{@{text "\ \ B x"}} + \infer[(@{text "\\expand"})]{@{text "\ - (x \ t) \ B t"}}{@{text "\ \ B x"}} \] This works, because the assumption @{text "x \ t"} was introduced in a context with @{text "x"} being fresh, so @{text "x"} does not @@ -222,8 +223,8 @@ simultaneously. \item @{ML Assumption.assume}~@{text "A"} turns proposition @{text - "A"} into a raw assumption @{text "A \ A'"}, where the conclusion - @{text "A'"} is in HHF normal form. + "A"} into a primitive assumption @{text "A \ A'"}, where the + conclusion @{text "A'"} is in HHF normal form. \item @{ML Assumption.add_assms}~@{text "r As"} augments the context by assumptions @{text "As"} with export rule @{text "r"}. The @@ -232,7 +233,8 @@ \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. + "\\intro"} or @{text "#\\intro"}, depending on goal + mode. \item @{ML Assumption.export}~@{text "is_goal inner outer thm"} exports result @{text "thm"} from the the @{text "inner"} context @@ -245,7 +247,7 @@ *} -section {* Results \label{sec:results} *} +section {* Structured goals and results \label{sec:struct-goals} *} text {* Local results are established by monotonic reasoning from facts @@ -263,6 +265,10 @@ the tactic needs to solve the conclusion, but may use the premise as a local fact, for locally fixed variables. + The family of @{text "FOCUS"} combinators is similar to @{text + "SUBPROOF"}, but allows to retain schematic variables and pending + subgoals in the resulting goal state. + 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 by @@ -275,7 +281,8 @@ The @{text "obtain"} operation produces results by eliminating existing facts by means of a given tactic. This acts like a dual conclusion: the proof demonstrates that the context may be augmented - by certain fixed variables and assumptions. See also + by parameters and assumptions, without affecting any conclusions + that do not mention these parameters. See also \cite{isabelle-isar-ref} for the user-level @{text "\"} and @{text "\"} elements. Final results, which may not refer to the parameters in the conclusion, need to exported explicitly into @@ -285,7 +292,11 @@ text %mlref {* \begin{mldecls} @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ + @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ + @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ + @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) -> Proof.context -> int -> tactic"} \\ \end{mldecls} + \begin{mldecls} @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ @@ -305,6 +316,12 @@ schematic parameters of the goal are imported into the context as fixed ones, which may not be instantiated in the sub-proof. + \item @{ML Subgoal.FOCUS}, @{ML Subgoal.FOCUS_PREMS}, and @{ML + Subgoal.FOCUS_PARAMS} are similar to @{ML SUBPROOF}, but are + slightly more flexible: only the specified parts of the subgoal are + imported into the context, and the body tactic may introduce new + subgoals and schematic variables. + \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text "C"} in the context augmented by fixed variables @{text "xs"} and assumptions @{text "As"}, and applies tactic @{text "tac"} to solve diff -r 9700a87f1cc2 -r f3bce1cc513c doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Tue Feb 02 12:37:57 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Tue Feb 02 13:11:04 2010 +0100 @@ -4,15 +4,13 @@ chapter {* Tactical reasoning *} -text {* - Tactical reasoning works by refining the initial claim in a +text {* Tactical reasoning works by refining an 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. -*} + "tactical"} is a combinator for composing tactics. *} section {* Goals \label{sec:tactical-goals} *} @@ -40,8 +38,8 @@ The main conclusion @{text C} is internally marked as a protected proposition, 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. + "#C"} here. 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: @@ -98,26 +96,27 @@ supporting memoing.\footnote{The lack of memoing and the strict nature of SML requires some care when working with low-level sequence operations, to avoid duplicate or premature evaluation of - results.} + results. It also means that modified runtime behavior, such as + timeout, is very hard to achieve for general tactics.} An \emph{empty result sequence} means that the tactic has failed: in - a compound tactic expressions other tactics might be tried instead, + a compound tactic expression other tactics might be tried instead, or the whole refinement step might fail outright, producing a - toplevel error message. When implementing tactics from scratch, one - should take care to observe the basic protocol of mapping regular - error conditions to an empty result; only serious faults should - emerge as exceptions. + toplevel error message in the end. When implementing tactics from + scratch, one should take care to observe the basic protocol of + mapping regular error conditions to an empty result; only serious + faults should emerge as exceptions. By enumerating \emph{multiple results}, a tactic can easily express the potential outcome of an internal search process. There are also combinators for building proof tools that involve search systematically, see also \secref{sec:tacticals}. - \medskip As explained in \secref{sec:tactical-goals}, a goal state - essentially consists of a list of subgoals that imply the main goal - (conclusion). Tactics may operate on all subgoals or on a - particularly specified subgoal, but must not change the main - conclusion (apart from instantiating schematic goal variables). + \medskip As explained before, a goal state essentially consists of a + list of subgoals that imply the main goal (conclusion). Tactics may + operate on all subgoals or on a particularly specified subgoal, but + must not change the main conclusion (apart from instantiating + schematic goal variables). Tactics with explicit \emph{subgoal addressing} are of the form @{text "int \ tactic"} and may be applied to a particular subgoal @@ -139,7 +138,7 @@ Tactics with internal subgoal addressing should expose the subgoal index as @{text "int"} argument in full generality; a hardwired - subgoal 1 inappropriate. + subgoal 1 is not acceptable. \medskip The main well-formedness conditions for proper tactics are summarized as follows. @@ -161,11 +160,11 @@ \end{itemize} Some of these conditions are checked by higher-level goal - infrastructure (\secref{sec:results}); others are not checked + infrastructure (\secref{sec:struct-goals}); others are not checked explicitly, and violating them merely results in ill-behaved tactics experienced by the user (e.g.\ tactics that insist in being - applicable only to singleton goals, or disallow composition with - basic tacticals). + applicable only to singleton goals, or prevent composition via + standard tacticals). *} text %mlref {* @@ -356,7 +355,7 @@ "(?'a, \)"}. Type instantiations are distinguished from term instantiations by the syntactic form of the schematic variable. Types are instantiated before terms are. Since term instantiation - already performs type-inference as expected, explicit type + already performs simple type-inference, so explicit type instantiations are seldom necessary. *} @@ -389,6 +388,12 @@ names} (which need to be distinct indentifiers). \end{description} + + For historical reasons, the above instantiation tactics take + unparsed string arguments, which makes them hard to use in general + ML code. The slightly more advanced @{ML Subgoal.FOCUS} combinator + of \secref{sec:struct-goals} allows to refer to internal goal + structure with explicit context management. *}