diff -r bdd82350cf22 -r 258ce361ba1b CookBook/Tactical.thy --- a/CookBook/Tactical.thy Mon Feb 09 01:23:35 2009 +0000 +++ b/CookBook/Tactical.thy Mon Feb 09 04:18:14 2009 +0000 @@ -72,8 +72,9 @@ Note that 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 theorem @{ML thm}; for example @{ML "etac - (thm \"disjE\") 1"}. Both ways however are considered bad style. The reason + the theorem dynamically using the function @{ML thm}; for example + @{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 applied. This problem is nicely prevented by using antiquotations, because @@ -108,7 +109,7 @@ has a hard-coded number that stands for the subgoal analysed by the tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, - you can write + you can write\label{tac:footacprime} *} ML{*val foo_tac' = @@ -151,7 +152,9 @@ @{text [display, gray] "type tactic = thm -> thm Seq.seq"} It is custom that if a tactic fails, it should return the empty sequence: - therefore your own tactics should not raise exceptions willy-nilly. + therefore your own tactics should not raise exceptions willy-nilly. Only + in very grave failure situations should a tactic raise the exception + @{text THM}. The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns the empty sequence and is defined as @@ -161,19 +164,19 @@ text {* which means @{ML no_tac} always fails. The second returns the given theorem wrapped - as a single member sequence. It is defined as + as a single member sequence; @{ML all_tac} is defined as *} ML{*fun all_tac thm = Seq.single thm*} text {* - which means @{ML all_tac} always succeeds (but also does not make any progress + which means it always succeeds (but also does not make any progress with the proof). 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 - @{ML foo_tac'}. + @{ML foo_tac'}: either using the first assumption or the second. *} lemma "\P \ Q; P \ Q\ \ Q \ P" @@ -184,9 +187,8 @@ text {* By using \isacommand{back}, we construct the proof that uses the - second assumption. In more interesting situations, different possibilities - can lead to different proofs and even often need to be explored when - a first proof attempt is unsuccessful. + second assumption. In more interesting situations, only by exploring + different possibilities one might be able to find a proof. \begin{readmore} See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy @@ -213,9 +215,9 @@ 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 - now can inspect every proof 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}. + are now in the position to inspect every proof 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}. *} lemma shows "\A; B\ \ A \ B" @@ -275,11 +277,12 @@ 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)"}. Since the goal @{term C} can potentially be an implication, + @{text "C \ (C)"}, and 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; however this constant is invisible in the print out above). This - prevents that premises of @{text C} are misinterpreted as open subgoals. + 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. @@ -289,12 +292,18 @@ section {* Simple Tactics *} text {* - A simple tactic is @{ML print_tac}, which is useful for low-level debugging of tactics. + A simple tactic is @{ML print_tac}, which is quite useful for low-level debugging of tactics. It just prints out a message and the current goal state. *} lemma shows "False \ True" apply(tactic {* print_tac "foo message" *}) +txt{*\begin{minipage}{\textwidth}\small + @{text "foo message"}\\[3mm] + @{prop "False \ True"}\\ + @{text " 1. False \ True"}\\ + \end{minipage} + *} (*<*)oops(*>*) text {* @@ -338,7 +347,7 @@ text {* As mentioned in the previous section, most basic tactics take a number as argument, which addresses the subgoal they are analysing. In the proof below, - we first break up the second subgoal by focusing on this subgoal first. + we first analyse the second subgoal by focusing on this subgoal first. *} lemma shows "Foo" and "P \ Q" @@ -374,8 +383,18 @@ Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} (@{ML eresolve_tac}) and so on. - (FIXME: @{ML cut_facts_tac}) + Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems + into the assumptions of the current goal state. For example: +*} +lemma shows "True \ False" +apply(tactic {* cut_facts_tac [@{thm True_def}, @{thm False_def}] 1 *}) +txt{*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} +(*<*)oops(*>*) + +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 @@ -386,9 +405,19 @@ "@{thm disjI1} RS @{thm conjI}" "\?P1; ?Q\ \ (?P1 \ ?Q1) \ ?Q"} instantiates the first premise of the @{text conjI}-rule with the - rule @{text disjI1}. The function @{ML RSN} is similar, but - takes a number and makes explicit which premise should be instantiated. - To improve readability we are going use the following function + rule @{text disjI1}. If this is impossible, as in the case of + + @{ML_response_fake_both [display,gray] + "@{thm conjI} RS @{thm mp}" +"*** Exception- THM (\"RSN: no unifiers\", 1, +[\"\?P; ?Q\ \ ?P \ ?Q\", \"\?P \ ?Q; ?P\ \ ?Q\"]) raised"} + + the function raises an exception. The function @{ML RSN} is similar, but + takes a number as argument and thus you can make explicit which premise + should be instantiated. + + To improve readability of the theorems we produce below, we shall use + the following function *} ML{*fun no_vars ctxt thm = @@ -399,23 +428,23 @@ end*} text {* - to transform the schematic variables of a theorem into free variables. - This means for the @{ML RS}-expression above: + that transform the schematic variables of a theorem into free variables. + This means for the first @{ML RS}-expression above: @{ML_response_fake [display,gray] "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\P; Q\ \ (P \ Qa) \ Q"} - If you want to instantiate more than one premise, you can use the function - @{ML MRS}: + If you want to instantiate more than one premise of a theorem, you can use + the function @{ML MRS}: @{ML_response_fake [display,gray] "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" "\P; Q\ \ (P \ Qa) \ (Pa \ Q)"} If you need to instantiate lists of theorems, you can use the - functions @{ML RL} and @{ML MRL}. For example below every - theorem in the first list is instantiated against every theorem - in the second. + functions @{ML RL} and @{ML MRL}. For example in the code below + every theorem in the first list is instantiated against every + theorem in the second. @{ML_response_fake [display,gray] "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" @@ -472,7 +501,7 @@ apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? txt {* - which yields the printout: + which gives the printout: \begin{quote}\small \begin{tabular}{ll} @@ -504,7 +533,7 @@ apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? txt {* - then @{ML SUBPROOF} prints out + then @{ML sp_tac} prints out \begin{quote}\small \begin{tabular}{ll} @@ -528,15 +557,20 @@ *} ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*} + +text {* + If we apply it to the next lemma +*} + lemma shows "\x y. \B x y; A x y; C x y\ \ A x y" apply(tactic {* atac' @{context} 1 *}) -txt{* yields +txt{* we get @{subgoals [display]} *} (*<*)oops(*>*) text {* The restriction in this tactic is that it cannot instantiate any - schematic variables. This might be seen as a defect, but is actually + schematic variable. This might be seen as a defect, but it is actually an advantage in the situations for which @{ML SUBPROOF} was designed: the reason is that instantiation of schematic variables can affect several goals and can render them unprovable. @{ML SUBPROOF} is meant @@ -547,7 +581,7 @@ the \isacommand{apply}-step uses @{text "1"}. Another advantage of @{ML SUBGOAL} is that the addressing inside it is completely local to the subproof inside. It is therefore possible to also apply - @{ML atac'} to the second goal: + @{ML atac'} to the second goal by just writing: *} lemma shows "True" and "\x y. \B x y; A x y; C x y\ \ A x y" @@ -563,9 +597,10 @@ \end{readmore} A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. - It allows you to inspect a specified subgoal. With this you can implement - a tactic that applies a rule according to its topmost connective (we only - analyse a few connectives). The tactic is as follows: + It allows you to inspect a given subgoal. With this you can implement + a tactic that applies a rule according to the topmost connective in the + subgoal (to illustrate this we only analyse a few connectives). The code + of this tactic is as follows.\label{tac:selecttac} *} ML %linenumbers{*fun select_tac (t,i) = @@ -579,15 +614,18 @@ text {* In line 3 you need to decend under the outermost @{term "Trueprop"} in order - to get to the connective you like to analyse. Otherwise goals @{prop "A \ B"} - are not bropek up. In line 7, the pattern cannot be constructed using the - @{text "@term"}-antiquotation, because that would fix the type of the - quantified variable. In this case you really have to construct the pattern - by using the term-constructors. The other cases work, because their type - is always bool. In case that the goal does not fall into any of the categorories, - then we chose to just return @{ML all_tac} (i.e., the tactic never fails). + 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 + in this way. The reason is that an antiquotation would fix the type of the + 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. + In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac} + never fails). - Let us now see how to apply this tactic. + Let us now see how to apply this tactic. Consider the four goals: *} @@ -596,13 +634,16 @@ apply(tactic {* SUBGOAL select_tac 3 *}) apply(tactic {* SUBGOAL select_tac 2 *}) apply(tactic {* SUBGOAL select_tac 1 *}) -txt{* @{subgoals [display]} *} +txt{* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} (*<*)oops(*>*) text {* - Note that we applied it in ``reverse'' order. This is a trick in - order to be independent from what subgoals the rule produced. If we had - it applied in the other order + 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 *} lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" @@ -614,20 +655,21 @@ text {* then we have to be careful to not apply the tactic to the two subgoals the - first goal produced. This can be messy in an automated proof script. The - reverse application, on the other hand, is easy to implement. + first goal produced. To do this can result in quite messy code. In contrast, + the ``reverse application'' is easy to implement. - However, this example is contrived: there are much simpler ways to implement - such proof procedure that analyses a goal according to its topmost - connective. They will be explained in the next section. + However, this example is very contrived: there are much simpler methods to implement + such a proof procedure analying a goal according to its topmost + connective. These simpler methods use tactic combinators which will be explained + in the next section. *} section {* Tactic Combinators *} text {* - To be able to implement powerful tactics out of smaller component tactics, - Isabelle provides tactic combinators. In the previous section we already - used @{ML THEN} which strings two tactics together in sequence. For example: + The purpose of tactic combinators is to build powerful tactics out of + smaller components. In the previous section we already used @{ML THEN} which + strings two tactics together in sequence. For example: *} lemma shows "(Foo \ Bar) \ False" @@ -639,7 +681,7 @@ text {* If you want to avoid the hard-coded subgoal addressing, then you can use - @{ML THEN'}. For example: + the ``primed'' version of @{ML THEN}, namely @{ML THEN'}. For example: *} lemma shows "(Foo \ Bar) \ False" @@ -650,35 +692,129 @@ (*<*)oops(*>*) text {* - For most tactic combinators such a ``primed'' version exists. - In what follows we will, whenever appropriate, prefer the primed version of - the tactic combinator and omit to mention the simple one. + For most tactic combinators such a ``primed'' version exists and + in what follows we will usually prefer it over the ``unprimed'' one. + + 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 +*} + +ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, + atac, rtac @{thm disjI1}, atac]*} - With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics - sucessfully apply; otherwise the whole tactic will fail. If you want to - try out either one tactic, then you can use @{ML ORELSE'}. For - example +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 +*} + +ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, + 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 + 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'} + (or @{ML FIRST1}) for a list of tactics. For example, the tactic *} ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*} text {* - will first try out rule @{text disjI} and after that @{text conjI}. + will first try out whether rule @{text disjI} applies and after that + whether @{text conjI}. To see this consider the proof: *} lemma shows "True \ False" and "Foo \ Bar" apply(tactic {* orelse_xmp 1 *}) apply(tactic {* orelse_xmp 3 *}) -txt {* @{subgoals [display]} *} +txt {* which results in the goal state + + \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} +*} (*<*)oops(*>*) text {* - applies + Using @{ML FIRST'} we can write our @{ML select_tac} from Page~\ref{tac:selecttac} + simply as follows: +*} + +ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, + 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: +*} + +lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" +apply(tactic {* select_tac' 4 *}) +apply(tactic {* select_tac' 3 *}) +apply(tactic {* select_tac' 2 *}) +apply(tactic {* select_tac' 1 *}) +txt{* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)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: *} + +lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" +apply(tactic {* ALLGOALS select_tac' *}) +txt{* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)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 +*} + +lemma shows "E \ F" +apply(tactic {* select_tac' 1 *}) +txt{* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)oops(*>*) + +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 + 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(*>*) +text {* + @{ML REPEAT} @{ML DETERM} + @{ML CHANGED} + *} section {* Rewriting and Simplifier Tactics *}