diff -r 258ce361ba1b -r 8bea3f74889d CookBook/Tactical.thy --- a/CookBook/Tactical.thy Mon Feb 09 04:18:14 2009 +0000 +++ b/CookBook/Tactical.thy Wed Feb 11 17:40:24 2009 +0000 @@ -21,7 +21,7 @@ text {* To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof - into ML. Consider the following proof. + into ML. Suppose the following proof. *} lemma disj_swap: "P \ Q \ Q \ P" @@ -62,18 +62,17 @@ \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}. See @{ML_file + and the file @{ML_file "Pure/goal.ML"}. 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. Many theorems + Note that in the code above we used antiquotations for referencing the theorems. Many theorems also have ML-bindings with the same name. Therefore, we could also just have written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained the theorem dynamically using the function @{ML thm}; for example - @{ML "etac (thm \"disjE\") 1"}. Both ways however are considered bad style. + @{ML "etac (thm \"disjE\") 1"}. Both ways however are considered bad style! The reason is that the binding for @{ML disjE} can be re-assigned by the user and thus one does not have complete control over which theorem is actually @@ -133,7 +132,7 @@ text {* This kind of addressing is more difficult to achieve when the goal is - hard-coded inside the tactic. For every operator that combines tactics + hard-coded inside the tactic. For most operators that combine tactics (@{ML THEN} is only one such operator) a ``primed'' version exists. The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for @@ -175,7 +174,7 @@ The lazy list of possible successor states shows through at 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 + following proof there are two possibilities for how to apply @{ML foo_tac'}: either using the first assumption or the second. *} @@ -215,7 +214,7 @@ text {* which prints out the given theorem (using the string-function defined in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We - are now in the position to inspect every proof state in a proof. Consider + are now in the position to inspect every goal state in a proof. Consider the proof below: on the left-hand side we show the goal state as shown by Isabelle, on the right-hand side the print out from @{ML my_print_tac}. *} @@ -224,48 +223,48 @@ apply(tactic {* my_print_tac @{context} *}) txt{* \small - \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} \begin{minipage}[t]{0.3\textwidth} @{subgoals [display]} \end{minipage} & - \hfill@{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"} - \end{tabular} + @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"} + \end{tabularstar} *} apply(rule conjI) apply(tactic {* my_print_tac @{context} *}) txt{* \small - \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}} + \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} \begin{minipage}[t]{0.26\textwidth} @{subgoals [display]} \end{minipage} & - \hfill@{text "(\A; B\ \ A) \ (\A; B\ \ B) \ (\A; B\ \ A \ B)"} - \end{tabular} + @{text "(\A; B\ \ A) \ (\A; B\ \ B) \ (\A; B\ \ A \ B)"} + \end{tabularstar} *} apply(assumption) apply(tactic {* my_print_tac @{context} *}) txt{* \small - \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} \begin{minipage}[t]{0.3\textwidth} @{subgoals [display]} \end{minipage} & - \hfill@{text "(\A; B\ \ B) \ (\A; B\ \ A \ B)"} - \end{tabular} + @{text "(\A; B\ \ B) \ (\A; B\ \ A \ B)"} + \end{tabularstar} *} apply(assumption) apply(tactic {* my_print_tac @{context} *}) txt{* \small - \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} \begin{minipage}[t]{0.3\textwidth} @{subgoals [display]} \end{minipage} & - \hfill@{text "\A; B\ \ A \ B"} - \end{tabular} + @{text "\A; B\ \ A \ B"} + \end{tabularstar} *} done @@ -277,7 +276,7 @@ where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the subgoals. So after setting up the lemma, the goal state is always of the form - @{text "C \ (C)"}, and when the proof is finished we are left with @{text "(C)"}. + @{text "C \ (C)"}; when the proof is finished we are left with @{text "(C)"}. Since the goal @{term C} can potentially be an implication, there is a ``protector'' wrapped around it (in from of an outermost constant @{text "Const (\"prop\", bool \ bool)"} applied to each goal; @@ -285,8 +284,13 @@ prevents that premises of @{text C} are mis-interpreted as open subgoals. While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion @{term C} intact, with the - exception of possibly instantiating schematic variables. + exception of possibly instantiating schematic variables. If you use + the predefined tactics, this will always be the case. + \begin{readmore} + For more information about the internals of goals see \isccite{sec:tactical-goals}. + \end{readmore} + *} section {* Simple Tactics *} @@ -396,16 +400,33 @@ text {* Since rules are applied using higher-order unification, an automatic proof - procedure might become too fragile, if it just applies inference rules shown - in the fashion above. More constraints can be introduced by - pre-instantiating theorems with other theorems. You can do this using the - function @{ML RS}. For example + procedure might become too fragile, if it just applies inference rules as + shown above. The reason is that a number of rules introduce meta-variables + into the goal state. Consider for example the proof +*} + +lemma shows "\x\A. P x \ Q x" +apply(drule bspec) +txt{*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} +(*<*)oops(*>*) + +text {* + where the application of @{text bspec} results into two subgoals involving the + meta-variable @{text "?x"}. The point is that if you are not careful, tactics + applied to the first subgoal might instantiate this meta-variable in such a + way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"} + should be, then this situation can be avoided by introducing a more + constraint version of the @{text bspec}-rule. Such constraints can be enforced by + pre-instantiating theorems with other theorems, for example by using the + function @{ML RS} @{ML_response_fake [display,gray] "@{thm disjI1} RS @{thm conjI}" "\?P1; ?Q\ \ (?P1 \ ?Q1) \ ?Q"} - instantiates the first premise of the @{text conjI}-rule with the - rule @{text disjI1}. If this is impossible, as in the case of + which, for instance, instantiates the first premise of the @{text conjI}-rule + with the rule @{text disjI1}. If this is impossible, as in the case of @{ML_response_fake_both [display,gray] "@{thm conjI} RS @{thm mp}" @@ -613,7 +634,7 @@ | _ => all_tac*} text {* - In line 3 you need to decend under the outermost @{term "Trueprop"} in order + In line 3 you need to descend under the outermost @{term "Trueprop"} in order to get to the connective you like to analyse. Otherwise goals like @{prop "A \ B"} are not properly analysed. While for the first four pattern we can use the @{text "@term"}-antiquotation, the pattern in Line 7 cannot be constructed @@ -621,7 +642,7 @@ quantified variable. So you really have to construct the pattern using the term-constructors. This is not necessary in other cases, because their type is always something involving @{typ bool}. The final patter is - for the case where the goal does not fall into any of the categorories before. + for the case where the goal does not fall into any of the categories before. In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac} never fails). @@ -643,7 +664,7 @@ where in all but the last the tactic applied an introduction rule. Note that we applied the tactic to subgoals in ``reverse'' order. This is a trick in order to be independent from what subgoals are - that are produced by the rule. If we had it applied in the other order + that are produced by the rule. If we had applied it in the other order *} lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" @@ -659,7 +680,7 @@ the ``reverse application'' is easy to implement. However, this example is very contrived: there are much simpler methods to implement - such a proof procedure analying a goal according to its topmost + such a proof procedure analysing a goal according to its topmost connective. These simpler methods use tactic combinators which will be explained in the next section. *} @@ -668,7 +689,7 @@ text {* The purpose of tactic combinators is to build powerful tactics out of - smaller components. In the previous section we already used @{ML THEN} which + smaller components. In the previous section we already used @{ML THEN}, which strings two tactics together in sequence. For example: *} @@ -681,7 +702,7 @@ text {* If you want to avoid the hard-coded subgoal addressing, then you can use - the ``primed'' version of @{ML THEN}, namely @{ML THEN'}. For example: + the ``primed'' version of @{ML THEN}. For example: *} lemma shows "(Foo \ Bar) \ False" @@ -698,28 +719,27 @@ If there is a list of tactics that should all be tried out in sequence, you can use the combinator @{ML EVERY'}. For example the function @{ML foo_tac'} from page~\ref{tac:footacprime} can also - be written as + be written as: *} ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, atac, rtac @{thm disjI1}, atac]*} text {* - There is even another variant for @{ML foo_tac''}: in automatic proof - procedures (in contrast to tactics that might be called by the user) - there are often long lists of tactics that are applied to the first - subgoal. Instead of writing the code above and then calling - @{ML "foo_tac'' 1"}, you can also just write + There is even another way: in automatic proof procedures (in contrast to + tactics that might be called by the user) there are often long lists of + tactics that are applied to the first subgoal. Instead of writing the code + above and then calling @{ML "foo_tac'' 1"}, you can also just write *} ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, - atac, rtac @{thm disjI1}, atac]*} + atac, rtac @{thm disjI1}, atac]*} text {* With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be - guaranteed that all component tactics sucessfully apply; otherwise the + guaranteed that all component tactics successfully apply; otherwise the whole tactic will fail. If you rather want to try out a number of tactics, - then you can use the combinator @{ML ORELSE'} for two tactics and @{ML FIRST'} + then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic *} @@ -731,8 +751,8 @@ *} lemma shows "True \ False" and "Foo \ Bar" +apply(tactic {* orelse_xmp 2 *}) apply(tactic {* orelse_xmp 1 *}) -apply(tactic {* orelse_xmp 3 *}) txt {* which results in the goal state \begin{minipage}{\textwidth} @@ -751,10 +771,10 @@ rtac @{thm notI}, rtac @{thm allI}, K all_tac]*} text {* - Since we like to mimic the bahaviour of @{ML select_tac}, we must include - @{ML all_tac} at the end (@{ML all_tac} must also be ``wrapped up'' using - the @{ML K}-combinator as it does not take a subgoal number as argument). - We can test the tactic on the same proof: + Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, + we must include @{ML all_tac} at the end of the list (@{ML all_tac} must also + be ``wrapped up'' using the @{ML K}-combinator, as it does not take a subgoal + number as argument). We can test the tactic on the same proof: *} lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" @@ -768,10 +788,10 @@ (*<*)oops(*>*) text {* - and obtain the same subgoals. Since this repeated application of a tactic - to the reverse order of \emph{all} subgoals is quite common, there is - the tactics combinator @{ML ALLGOALS} that simplifies this. Using this - combinator we can simply write: *} + Because such repeated applications of a tactic to the reverse order of + \emph{all} subgoals is quite common, there is the tactics combinator + @{ML ALLGOALS} that simplifies this. Using this combinator we can simply + write: *} lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" apply(tactic {* ALLGOALS select_tac' *}) @@ -781,9 +801,9 @@ (*<*)oops(*>*) text {* - We chose to write @{ML select_tac'} in such a way that it always succeeds. - This can be potetially very confusing for the user in cases of goals - of the form + Remember that we chose to write @{ML select_tac'} in such a way that it always + succeeds. This can be potentially very confusing for the user, for example, + in cases the goals is the form *} lemma shows "E \ F" @@ -796,24 +816,131 @@ text {* where no rule applies. The reason is that the user has little chance to see whether progress in the proof has been made or not. We could simply - remove @{ML "K all_tac"} from the end of the list. Then the tactic would - only apply in cases where it can make some progress. But for the sake of - argument, let us assume that this is not an option. In such cases, you + delete th @{ML "K all_tac"} from the end of the list. Then @{ML select_tac'} + would only succeed on goals where it can make progress. But for the sake of + argument, let us suppose that this deletion is not an option. In such cases, you can use the combinator @{ML CHANGED} to make sure the subgoal has been changed by the tactic. Because now *} lemma shows "E \ F" apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*) -txt{* results in the usual error message for empty result sequences. *} -(*<*)oops(*>*) +txt{* results in the error message: + \begin{isabelle} + @{text "*** empty result sequence -- proof command failed"}\\ + @{text "*** At command \"apply\"."} + \end{isabelle} +*}(*<*)oops(*>*) text {* + Meaning the tactic failed. - @{ML REPEAT} @{ML DETERM} + We can extend @{ML select_tac'} so that it not just applies to the top-most + connective, but also to the ones immediately ``underneath''. For this you can use the + tactic combinator @{ML REPEAT}. For example suppose the following tactic +*} + +ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *} + +text {* and the proof *} + +lemma shows "((\A) \ (\x. B x)) \ (C \ D)" +apply(tactic {* repeat_xmp *}) +txt{* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)oops(*>*) + +text {* + Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, + because otherwise @{ML REPEAT} runs into an infinite loop. The function + @{ML REPEAT1} is similar, but runs the tactic at least once (failing if + this is not possible). + + If you are after the ``primed'' version of @{ML repeat_xmp} then it + needs to be coded as +*} + +ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*} + +text {* + since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}. + + If you look closely at the goal state above, the tactics @{ML repeat_xmp} + and @{ML repeat_xmp'} are not yet quite what we are after: the problem is + that goals 2 and 3 are not yet analysed. This is because both tactics + apply repeatedly only to the first subgoal. To analyse also all + resulting subgoals, you can use the function @{ML REPEAT_ALL_NEW}. + Suppose the tactic +*} + +ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*} + +text {* + which analyses the topmost connectives also in all resulting + subgoals. +*} + +lemma shows "((\A) \ (\x. B x)) \ (C \ D)" +apply(tactic {* repeat_all_new_xmp 1 *}) +txt{* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)oops(*>*) - @{ML CHANGED} +text {* + The last tactic combinator we describe here is @{ML DETERM}. Recall + that tactics produce a lazy sequence of successor goal states. These + states can be explored using the command \isacommand{back}. For example + +*} + +lemma "\P1 \ Q1; P2 \ Q2\ \ R" +apply(tactic {* etac @{thm disjE} 1 *}) +txt{* applies the rule to the first assumption + + \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*) +oops +lemma "\P1 \ Q1; P2 \ Q2\ \ R" +apply(tactic {* etac @{thm disjE} 1 *}) +(*>*) +back +txt{* whereas it is now applied to the second + + \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)oops(*>*) + +text {* + Sometimes this leads to confusing behaviour of tactics and also has + the potential to explode the search space for tactics build on top. + This can be avoided by prefixing the tactic with @{ML DETERM}. +*} + +lemma "\P1 \ Q1; P2 \ Q2\ \ R" +apply(tactic {* DETERM (etac @{thm disjE} 1) *}) +txt {*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)oops(*>*) +text {* + This will prune the search space to just the first possibility. + Attempting to apply \isacommand{back} in this goal states gives the + error message: + + \begin{isabelle} + @{text "*** back: no alternatives"}\\ + @{text "*** At command \"back\"."} + \end{isabelle} + + \begin{readmore} + Most tactic combinators are defined in @{ML_file "Pure/tctical.ML"}. + \end{readmore} *}