diff -r 0a5c95f4d70c -r de625e5f6a36 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Thu Feb 05 22:40:22 2009 +0000 +++ b/CookBook/Tactical.thy Thu Feb 05 22:40:46 2009 +0000 @@ -1,5 +1,5 @@ theory Tactical -imports Base +imports Base FirstSteps begin chapter {* Tactical Reasoning\label{chp:tactical} *} @@ -12,9 +12,8 @@ new definitions. These proof procedures are centred around refining a goal state using tactics. This is similar to the @{text apply}-style reasoning at the user level, where goals are modified in a sequence of proof steps until - all of them are solved. - - + all of them are solved. However, there are also more structured operations + that help with handling of variables and assumptions. *} section {* Tactical Reasoning *} @@ -50,19 +49,23 @@ end" "?P \ ?Q \ ?Q \ ?P"} To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C - tac"} sets up a goal state for proving the goal @{text C} under the - assumptions @{text As} (empty in the proof at hand) with the variables + tac"} sets up a goal state for proving the goal @{text C} + (that is @{prop "P \ Q \ Q \ P"} in the proof at hand) under the + assumptions @{text As} (happens to be empty) with the variables @{text xs} that will be generalised once the goal is proved (in our case @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal; it can make use of the local assumptions (there are none in this example). The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to @{text erule}, @{text rule} and @{text assumption}, respectively. - The operator @{ML THEN} strings tactics together. + The operator @{ML THEN} strings the tactics together. \begin{readmore} - To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and - the file @{ML_file "Pure/goal.ML"}. For more information about the internals of goals see - \isccite{sec:tactical-goals}. + To learn more about the function @{ML Goal.prove} see \isccite{sec:results} + and the file @{ML_file "Pure/goal.ML"}. For more information about the + internals of goals see \isccite{sec:tactical-goals}. See @{ML_file + "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic + tactics and tactic combinators; see also Chapters 3 and 4 in the old + Isabelle Reference Manual. \end{readmore} Note that we used antiquotations for referencing the theorems. We could also @@ -92,9 +95,9 @@ done text {* - The apply-step applies the @{ML foo_tac} and therefore solves the goal completely. - Inside @{text "tactic \ \ \"} - we can call any function that returns a tactic. + By using @{text "tactic \ \ \"} in the apply-step, + you can call @{ML foo_tac} or any function that returns a tactic from the + user level of Isabelle. As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that stands for the subgoal analysed by the tactic. In our case, we only focus on the first @@ -111,7 +114,8 @@ text {* and then give the number for the subgoal explicitly when the tactic is - called. So in the next proof we discharge first the second subgoal, + called. For every operator that combines tactics, such a primed version + exists. So in the next proof we can first discharge the second subgoal, and after that the first. *} @@ -122,20 +126,31 @@ done text {* - The tactic @{ML foo_tac} is very specific for analysing goals of the form - @{prop "P \ Q \ Q \ P"}. If the goal is not of this form, then @{ML foo_tac} - throws the error message about an empty result sequence---meaning the tactic - failed. The reason for this message is that tactics are functions that map - a goal state to a (lazy) sequence of successor states, hence the type of a - tactic is + (FIXME: maybe add something about how each goal state is interpreted + as a theorem) + + The tactic @{ML foo_tac} (and @{ML foo_tac'}) are very specific for + analysing goals only of the form @{prop "P \ Q \ Q \ P"}. If the goal is not + of this form, then @{ML foo_tac} throws the error message: + + \begin{isabelle} + @{text "*** empty result sequence -- proof command failed"}\\ + @{text "*** At command \"apply\"."} + \end{isabelle} + + Meaning the tactic failed. The reason for this error message is that tactics + are functions that map a goal state to a (lazy) sequence of successor states, + hence the type of a tactic is @{text [display, gray] "type tactic = thm -> thm Seq.seq"} - Consequently, if a tactic fails, then it returns the empty sequence. This - is by the way the default behaviour for a failing tactic; tactics should - not raise exceptions. + It is custom that if a tactic fails, it should return the empty sequence: + tactics should not raise exceptions willy-nilly. - In the following example there are two possibilities for how to apply the tactic. + The lazy list of possible successor states shows through to the user-level + of Isabelle when using the command \isacommand{back}. For instance in the + following proof, there are two possibilities for how to apply + @{ML foo_tac'}. *} lemma "\P \ Q; P \ Q\ \ Q \ P" @@ -144,82 +159,111 @@ done text {* - The application of the tactic results in a sequence of two possible - proofs. The Isabelle command \isacommand{back} allows us to explore both - possibilities. - + By using \isacommand{back}, we construct the proof that uses the + second assumption to complete the proof. In more interesting + situations, different possibilities can lead to different proofs. + \begin{readmore} See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy sequences. However in day-to-day Isabelle programming, one rarely constructs sequences explicitly, but uses the predefined functions - instead. See @{ML_file "Pure/tactic.ML"} and - @{ML_file "Pure/tctical.ML"} for the code of basic tactics and tactic - combinators; see also Chapters 3 and 4 in - the old Isabelle Reference Manual. + instead. \end{readmore} *} - section {* Basic Tactics *} -lemma shows "False \ False" +text {* + As seen above, the function @{ML atac} corresponds to the assumption tactic. +*} + +lemma shows "P \ P" apply(tactic {* atac 1 *}) done -lemma shows "True \ True" +text {* + Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond + to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule}, + respectively. Below are three examples with the resulting goal state. How + they work should therefore be self-explanatory. +*} + +lemma shows "P \ Q" apply(tactic {* rtac @{thm conjI} 1 *}) -txt {* @{subgoals [display]} *} +txt{*@{subgoals [display]}*} (*<*)oops(*>*) -lemma - shows "Foo" - and "True \ True" -apply(tactic {* rtac @{thm conjI} 2 *}) -txt {* @{subgoals [display]} *} -(*<*)oops(*>*) - -lemma shows "False \ False \ False" +lemma shows "P \ Q \ False" apply(tactic {* etac @{thm conjE} 1 *}) -txt {* @{subgoals [display]} *} +txt{*@{subgoals [display]}*} (*<*)oops(*>*) lemma shows "False \ True \ False" apply(tactic {* dtac @{thm conjunct2} 1 *}) -txt {* @{subgoals [display]} *} +txt{*@{subgoals [display]}*} (*<*)oops(*>*) text {* - similarly @{ML ftac} + As mentioned above, most basic tactics take a number as argument, which + addresses to subgoal they are analysing. +*} + +lemma shows "Foo" and "P \ Q" +apply(tactic {* rtac @{thm conjI} 2 *}) +txt {*@{subgoals [display]}*} +(*<*)oops(*>*) + +text {* + Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which + however expects a list of theorems as arguments. From this list it will apply with + the first applicable theorem (later theorems that are also applicable can be + explored via the lazy sequences mechanism). Given the abbreviation *} -text {* diagnostics *} -lemma shows "True \ False" +ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*} + +text {* + an example for @{ML resolve_tac} is the following proof where first an outermost + implication is analysed and then an outermost conjunction. +*} + +lemma shows "C \ (A \ B)" and "(A \ B) \ C" +apply(tactic {* resolve_tac_xmp 1 *}) +apply(tactic {* resolve_tac_xmp 2 *}) +txt{* @{subgoals [display]} *} +(*<*)oops(*>*) + +text {* + Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} + (@{ML eresolve_tac}) and so on. + + The tactic @{ML print_tac} is useful for low-level debugging of tactics: it + prints out a message and the current goal state. +*} + +lemma shows "False \ True" apply(tactic {* print_tac "foo message" *}) (*<*)oops(*>*) -text {* Let us assume the following four string conversion functions: *} - -ML{*fun str_of_cterm ctxt t = - Syntax.string_of_term ctxt (term_of t) - -fun str_of_cterms ctxt ts = - commas (map (str_of_cterm ctxt) ts) +text {* + Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and + @{ML no_tac}. The former always succeeds (but does not change the goal state), and + the latter always fails. -fun str_of_thm ctxt thm = - let - val {prop, ...} = crep_thm thm - in - str_of_cterm ctxt prop - end + (FIXME explain RS MRS) -fun str_of_thms ctxt thms = - commas (map (str_of_thm ctxt) thms)*} - -text {* - and the following function + Often proofs involve elaborate operations on assumptions and variables + @{text "\"}-quantified in the goal state. To do such operations on the ML-level + using the basic tactics, is very unwieldy and brittle. Some convenience and + safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters + and binds the various components of a proof state into a record. *} +text_raw{* +\begin{figure} +\begin{isabelle} +*} ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = let val str_of_params = str_of_cterms context params @@ -236,20 +280,28 @@ in no_tac end*} +text_raw{* +\end{isabelle} +\caption{A function that prints out the various parameters provided by the tactic + @{ML SUBPROOF}. It uses the functions extracting strings from @{ML_type cterm}s + and @{ML_type thm}s, which are defined in Section~\ref{sec:printing}.\label{fig:sptac}} +\end{figure} +*} text {* - then the tactic @{ML SUBPROOF} fixes the parameters and binds the various components - of a proof state into a record. For example + To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which + takes a record as argument and just prints out the content of this record (using the + string transformation functions defined in Section~\ref{sec:printing}). Consider + now the proof *} -lemma - shows "\x y. A x y \ B y x \ C (?z y) x" +lemma shows "\x y. A x y \ B y x \ C (?z y) x" apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? txt {* - prints out + which yields the printout: - \begin{center} + \begin{quote}\small \begin{tabular}{ll} params: & @{term x}, @{term y}\\ schematics: & @{term z}\\ @@ -257,18 +309,31 @@ concl: & @{term "B y x \ C (z y) x"}\\ prems: & @{term "A x y"} \end{tabular} - \end{center} + \end{quote} + + Note in the actual output the brown colour of the variables @{term x} and + @{term y}. Although parameters in the original goal, they are fixed inside + the subproof. Similarly the schematic variable @{term z}. The assumption + is bound once as @{ML_type cterm} to the record-variable @{text asms} and + another time as @{ML_type thm} to @{text prems}. - Continuing the proof script with + Notice also that we had to append @{text "?"} to \isacommand{apply}. The + reason is that @{ML SUBPROOF} normally expects that the subgoal is solved completely. + Since in the function @{ML sp_tac} we returned the tactic @{ML no_tac}, the subproof + obviously fails. The question-mark allows us to recover from this failure + in a graceful manner so that the warning messages are not overwritten + by the error message. + + If we continue the proof script by applying the @{text impI}-rule *} apply(rule impI) apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? txt {* - prints out + then @{ML SUBPROOF} prints out - \begin{center} + \begin{quote}\small \begin{tabular}{ll} params: & @{term x}, @{term y}\\ schematics: & @{term z}\\ @@ -276,36 +341,85 @@ concl: & @{term "C (z y) x"}\\ prems: & @{term "A x y"}, @{term "B y x"} \end{tabular} - \end{center} + \end{quote} *} (*<*)oops(*>*) +text {* + where we now also have @{term "B y x"} as assumption. + + One convenience of @{ML SUBPROOF} is that we can apply assumption + using the usual tactics, because the parameter @{text prems} + contains the assumptions as theorems. With this we can easily + implement a tactic that almost behaves like @{ML atac}: +*} + +lemma shows "\x y. \B x y; A x y; C x y\ \ A x y" +apply(tactic + {* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *}) +txt{* yields + @{subgoals [display]} *} +(*<*)oops(*>*) + text {* - @{ML PRIMITIVE}? @{ML SUBGOAL} see page 32 in ref + The restriction in this tactic is that it cannot instantiate any + schematic variables. This might be seen as a defect, but is actually + an advantage in the situations for which @{ML SUBPROOF} was designed: + the reason is that instantiation of schematic variables can potentially + has affect several goals and can render them unprovable. + + A similar but less powerful function is @{ML SUBGOAL}. It allows you to + inspect a subgoal specified by a number. *} -text {* - @{ML all_tac} @{ML no_tac} +ML %linenumbers{*fun select_tac (t,i) = + case t of + @{term "Trueprop"} $ t' => select_tac (t',i) + | @{term "op \"} $ _ $ _ => rtac @{thm conjI} i + | @{term "op \"} $ _ $ _ => rtac @{thm impI} i + | @{term "Not"} $ _ => rtac @{thm notI} i + | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i + | _ => no_tac*} + +lemma shows "A \ B" "A \ B" "\x. C x" +apply(tactic {* SUBGOAL select_tac 1 *}) +apply(tactic {* SUBGOAL select_tac 3 *}) +apply(tactic {* SUBGOAL select_tac 4 *}) +txt{* @{subgoals [display]} *} +(*<*)oops(*>*) + +text {* + However, this example is contrived, as there are much simpler ways + to implement a proof procedure like the one above. They will be explained + in the next section. + + A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal + as @{ML_type cterm} instead of a @{ML_type term}. *} + section {* Operations on Tactics *} -text {* THEN *} +text {* @{ML THEN} *} -lemma shows "(True \ True) \ False" -apply(tactic {* (rtac @{thm conjI} 1) THEN (rtac @{thm conjI} 1) *}) +lemma shows "(Foo \ Bar) \ False" +apply(tactic {* (rtac @{thm conjI} 1) + THEN (rtac @{thm conjI} 1) *}) txt {* @{subgoals [display]} *} (*<*)oops(*>*) -lemma shows "True \ False" -apply(tactic {* (rtac @{thm disjI1} 1) ORELSE (rtac @{thm conjI} 1) *}) +ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*} + +lemma shows "True \ False" and "Foo \ Bar" +apply(tactic {* orelse_xmp 1 *}) +apply(tactic {* orelse_xmp 3 *}) txt {* @{subgoals [display]} *} (*<*)oops(*>*) text {* - @{ML EVERY} @{ML REPEAT} + @{ML EVERY} @{ML REPEAT} @{ML DETERM} @{ML rewrite_goals_tac} @{ML cut_facts_tac}