# HG changeset patch # User Christian Urban # Date 1234448150 0 # Node ID b4234e8a0202ecd507b8c2a9ab83474c739ae5cf # Parent 8bea3f74889de6f6bb09f32b32c7e7697ba64e7f polished diff -r 8bea3f74889d -r b4234e8a0202 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Wed Feb 11 17:40:24 2009 +0000 +++ b/CookBook/Tactical.thy Thu Feb 12 14:15:50 2009 +0000 @@ -72,7 +72,7 @@ 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! + \mbox{@{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 @@ -121,7 +121,7 @@ text {* and then give the number for the subgoal explicitly when the tactic is called. So in the next proof you can first discharge the second subgoal, and - after that the first. + subsequently the first. *} lemma "P1 \ Q1 \ Q1 \ P1" @@ -137,23 +137,25 @@ The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for analysing goals being only of the form @{prop "P \ Q \ Q \ P"}. If the goal is not - of this form, then they throw the error message: + of this form, then they return the error message: \begin{isabelle} @{text "*** empty result sequence -- proof command failed"}\\ @{text "*** At command \"apply\"."} \end{isabelle} - Meaning the tactics 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: + This means the tactics failed. The reason for this error message is that tactics + are functions mapping 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"} +ML{*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. Only - in very grave failure situations should a tactic raise the exception - @{text THM}. +text {* + By convention, if a tactic fails, then it should return the empty sequence. + Therefore, if you write your own tactics, they 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 @@ -163,16 +165,16 @@ text {* which means @{ML no_tac} always fails. The second returns the given theorem wrapped - as a single member sequence; @{ML all_tac} is defined as + up in a single member sequence; it is defined as *} ML{*fun all_tac thm = Seq.single thm*} text {* - which means it always succeeds (but also does not make any progress - with the proof). + which means @{ML all_tac} 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 + The lazy list of possible successor goal 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'}: either using the first assumption or the second. @@ -186,18 +188,19 @@ text {* By using \isacommand{back}, we construct the proof that uses the - second assumption. In more interesting situations, only by exploring - different possibilities one might be able to find a proof. + second assumption. While in the proof above, it does not really matter which + assumption is used, in more interesting cases provability might depend + on exploring different possibilities. \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. + sequences. In day-to-day Isabelle programming, however, one rarely + constructs sequences explicitly, but uses the predefined tactics and + tactic combinators instead. \end{readmore} It might be surprising that tactics, which transform - one proof state to the next, are functions from theorems to theorem + one goal state to the next, are functions from theorems to theorem (sequences). The surprise resolves by knowing that every goal state is indeed a theorem. To shed more light on this, let us modify the code of @{ML all_tac} to obtain the following @@ -211,81 +214,104 @@ Seq.single thm end*} -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 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}. +text_raw {* + \begin{figure}[p] + \begin{isabelle} *} - lemma shows "\A; B\ \ A \ B" apply(tactic {* my_print_tac @{context} *}) -txt{* \small - \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} - \begin{minipage}[t]{0.3\textwidth} +txt{* \begin{minipage}{\textwidth} @{subgoals [display]} - \end{minipage} & + \end{minipage}\medskip + + \begin{minipage}{\textwidth} + \small\colorbox{gray!20}{ + \begin{tabular}{@ {}l@ {}} + internal goal state:\\ @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"} - \end{tabularstar} + \end{tabular}} + \end{minipage}\medskip *} apply(rule conjI) apply(tactic {* my_print_tac @{context} *}) -txt{* \small - \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} - \begin{minipage}[t]{0.26\textwidth} +txt{* \begin{minipage}{\textwidth} @{subgoals [display]} - \end{minipage} & + \end{minipage}\medskip + + \begin{minipage}{\textwidth} + \small\colorbox{gray!20}{ + \begin{tabular}{@ {}l@ {}} + internal goal state:\\ @{text "(\A; B\ \ A) \ (\A; B\ \ B) \ (\A; B\ \ A \ B)"} - \end{tabularstar} + \end{tabular}} + \end{minipage}\medskip *} apply(assumption) apply(tactic {* my_print_tac @{context} *}) -txt{* \small - \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} - \begin{minipage}[t]{0.3\textwidth} +txt{* \begin{minipage}{\textwidth} @{subgoals [display]} - \end{minipage} & + \end{minipage}\medskip + + \begin{minipage}{\textwidth} + \small\colorbox{gray!20}{ + \begin{tabular}{@ {}l@ {}} + internal goal state:\\ @{text "(\A; B\ \ B) \ (\A; B\ \ A \ B)"} - \end{tabularstar} + \end{tabular}} + \end{minipage}\medskip *} apply(assumption) apply(tactic {* my_print_tac @{context} *}) -txt{* \small - \begin{tabularstar}{\textwidth}{@ {}l@ {\extracolsep{\fill}}l@ {}} - \begin{minipage}[t]{0.3\textwidth} +txt{* \begin{minipage}{\textwidth} @{subgoals [display]} - \end{minipage} & + \end{minipage}\medskip + + \begin{minipage}{\textwidth} + \small\colorbox{gray!20}{ + \begin{tabular}{@ {}l@ {}} + internal goal state:\\ @{text "\A; B\ \ A \ B"} - \end{tabularstar} + \end{tabular}} + \end{minipage}\medskip + *} +done +text_raw {* + \end{isabelle} + \caption{A proof where we show the goal state as printed + by the Isabelle system and as represented internally + (highlighted boxes).\label{fig:goalstates}} + \end{figure} *} -done text {* - As can be seen, internally every goal state is an implication of the form + which prints out the given theorem (using the string-function defined in + Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this + tactic we are in the position to inspect every goal state in a + proof. Consider now the proof in Figure~\ref{fig:goalstates}: as can be seen, + internally every goal state is an implication of the form @{text[display] "A\<^isub>1 \ \ \ A\<^isub>n \ (C)"} - 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)"}; 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 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. If you use - the predefined tactics, this will always be the case. + 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)"}; 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 figure). This 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. If you use the predefined tactics, which we describe in the next + section, this will always be the case. \begin{readmore} For more information about the internals of goals see \isccite{sec:tactical-goals}. @@ -296,13 +322,16 @@ section {* Simple Tactics *} text {* - 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. + Let us start with the tactic @{ML print_tac}, which is quite useful for low-level + debugging of tactics. It just prints out a message and the current goal state. + Processing the proof *} lemma shows "False \ True" apply(tactic {* print_tac "foo message" *}) -txt{*\begin{minipage}{\textwidth}\small +txt{*gives:\medskip + + \begin{minipage}{\textwidth}\small @{text "foo message"}\\[3mm] @{prop "False \ True"}\\ @{text " 1. False \ True"}\\ @@ -317,14 +346,16 @@ lemma shows "P \ P" apply(tactic {* atac 1 *}) -done +txt{*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} +(*<*)oops(*>*) text {* Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond to @{text rule}, @{text drule}, @{text erule} and @{text frule}, - respectively. Each of them takes a theorem as argument. Below are three - examples with the resulting goal state. How - they work should be self-explanatory. + respectively. Each of them takes a theorem as argument and attempts to + apply it to a goal. Below are three self-explanatory examples. *} lemma shows "P \ Q" @@ -349,9 +380,10 @@ (*<*)oops(*>*) 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 analyse the second subgoal by focusing on this subgoal first. + Note the number in each tactic call. Also as mentioned in the previous section, most + basic tactics take such an argument; it addresses the subgoal they are analysing. + In the proof below, we first split up the conjunction in the second subgoal by + focusing on this subgoal first. *} lemma shows "Foo" and "P \ Q" @@ -361,7 +393,9 @@ \end{minipage}*} (*<*)oops(*>*) -text {* +text {* + (FIXME: is it important to get the number of subgoals?) + The function @{ML resolve_tac} is similar to @{ML rtac}, except that it expects a list of theorems as arguments. From this list it will apply the first applicable theorem (later theorems that are also applicable can be @@ -384,16 +418,19 @@ (*<*)oops(*>*) text {* - Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac} - (@{ML eresolve_tac}) and so on. + Similarly versions taking a list of theorems exist for the tactics + @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on. + Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems - into the assumptions of the current goal state. For example: + 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} +txt{*produces the goal state\medskip + + \begin{minipage}{\textwidth} @{subgoals [display]} \end{minipage}*} (*<*)oops(*>*) @@ -413,28 +450,29 @@ (*<*)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 + where the application of Rule @{text bspec} generates two subgoals involving the + meta-variable @{text "?x"}. Now, 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} + constraint version of the @{text bspec}-rule. Such constraints can be given by + pre-instantiating theorems with other theorems. One function to do this is + @{ML RS} @{ML_response_fake [display,gray] "@{thm disjI1} RS @{thm conjI}" "\?P1; ?Q\ \ (?P1 \ ?Q1) \ ?Q"} - 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 + which in the example instantiates the first premise of the @{text conjI}-rule + with the rule @{text disjI1}. If the instantiation 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 + then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but + takes an additional number as argument that makes explicit which premise should be instantiated. To improve readability of the theorems we produce below, we shall use @@ -449,8 +487,9 @@ end*} text {* - that transform the schematic variables of a theorem into free variables. - This means for the first @{ML RS}-expression above: + that transform the schematic variables of a theorem into free variables. + Using this function for the first @{ML RS}-expression above would produce + the more readable result: @{ML_response_fake [display,gray] "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\P; Q\ \ (P \ Qa) \ Q"} @@ -463,9 +502,9 @@ "\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 in the code 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 second list is instantiated with every + theorem in the first. @{ML_response_fake [display,gray] "[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" @@ -478,15 +517,15 @@ The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}. \end{readmore} - Often proofs involve elaborate operations on assumptions and - @{text "\"}-quantified variables. To do such operations on the ML-level - using the basic tactics is very unwieldy and brittle. Some convenience and + Often proofs on the ML-level involve elaborate operations on assumptions and + @{text "\"}-quantified variables. To do such operations 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. + and binds the various components of a goal state to a record. 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 + takes a record and just prints out the content of this record (using the + string transformation functions from in Section~\ref{sec:printing}). Consider + now the proof: *} text_raw{* @@ -522,7 +561,7 @@ apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? txt {* - which gives the printout: + The tactic produces the following printout: \begin{quote}\small \begin{tabular}{ll} @@ -536,16 +575,18 @@ Note in the actual output the brown colour of the variables @{term x} and @{term y}. Although they are parameters in the original goal, they are fixed inside - the subproof. Similarly the schematic variable @{term z}. The assumption + the subproof. By convention these fixed variables are printed in brown colour. + Similarly the schematic variable @{term z}. The assumption, or premise, @{prop "A x y"} is bound as @{ML_type cterm} to the record-variable - @{text asms} but also as @{ML_type thm} to @{text prems}. + @{text asms}, but also as @{ML_type thm} to @{text prems}. - 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 an error message. + Notice also that we had to append @{text [quotes] "?"} to the + \isacommand{apply}-command. 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 an + ``empty sequence'' error message. If we continue the proof script by applying the @{text impI}-rule *} @@ -554,7 +595,7 @@ apply(tactic {* SUBPROOF sp_tac @{context} 1 *})? txt {* - then @{ML sp_tac} prints out + then tactic prints out \begin{quote}\small \begin{tabular}{ll} @@ -569,43 +610,44 @@ (*<*)oops(*>*) text {* - where we now also have @{term "B y x"} as an assumption. + Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}. One convenience of @{ML SUBPROOF} is that we can apply the assumptions using the usual tactics, because the parameter @{text prems} - contains them as theorems. With this we can easily - implement a tactic that almost behaves like @{ML atac}, namely: + contains them as theorems. With this you can easily + implement a tactic that behaves almost like @{ML atac}: *} ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*} text {* - If we apply it to the next lemma + If you apply @{ML atac'} to the next lemma *} -lemma shows "\x y. \B x y; A x y; C x y\ \ A x y" +lemma shows "\B x y; A x y; C x y\ \ A x y" apply(tactic {* atac' @{context} 1 *}) -txt{* we get +txt{* it will produce @{subgoals [display]} *} (*<*)oops(*>*) text {* - The restriction in this tactic is that it cannot instantiate any + The restriction in this tactic which is not present in @{ML atac} is + that it cannot instantiate any 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 + the reason is that, as mentioned before, instantiation of schematic variables can affect several goals and can render them unprovable. @{ML SUBPROOF} is meant to avoid this. - Notice that @{ML atac'} calls @{ML resolve_tac} with the subgoal - number @{text "1"} and also the ``outer'' call to @{ML SUBPROOF} in - 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 + Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with + the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in + the \isacommand{apply}-step uses @{text "1"}. This is another advantage + of @{ML SUBPROOF}: the addressing inside it is completely + local to the tactic inside the subproof. It is therefore possible to also apply @{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" +lemma shows "True" and "\B x y; A x y; C x y\ \ A x y" apply(tactic {* atac' @{context} 2 *}) apply(rule TrueI) done @@ -619,14 +661,15 @@ A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. 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 + a tactic that applies a rule according to the topmost logic connective in the subgoal (to illustrate this we only analyse a few connectives). The code - of this tactic is as follows.\label{tac:selecttac} + of the tactic is as follows.\label{tac:selecttac} *} ML %linenumbers{*fun select_tac (t,i) = case t of @{term "Trueprop"} $ t' => select_tac (t',i) + | @{term "op \"} $ _ $ t' => select_tac (t',i) | @{term "op \"} $ _ $ _ => rtac @{thm conjI} i | @{term "op \"} $ _ $ _ => rtac @{thm impI} i | @{term "Not"} $ _ => rtac @{thm notI} i @@ -634,17 +677,19 @@ | _ => all_tac*} text {* - 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 - 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 categories before. - In this case we chose to just return @{ML all_tac} (i.e., @{ML select_tac} - never fails). + The input of the function is a term representing the subgoal and a number + specifying the subgoal of interest. 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. Similarly with meta-implications in the next line. While for the + first five patterns we can use the @{text "@term"}-antiquotation to + construct the patterns, the pattern in Line 8 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 + basic term-constructors. This is not necessary in other cases, because their type + is always fixed to function types involving only the type @{typ bool}. The + final pattern, we chose to just return @{ML all_tac}. Consequently, + @{ML select_tac} never fails. Let us now see how to apply this tactic. Consider the four goals: *} @@ -662,9 +707,9 @@ text {* 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 applied it in the other order + Note that we applied the tactic to the goals in ``reverse'' order. + This is a trick in order to be independent from the subgoals 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" @@ -675,22 +720,22 @@ (*<*)oops(*>*) text {* - then we have to be careful to not apply the tactic to the two subgoals the - first goal produced. To do this can result in quite messy code. In contrast, + then we have to be careful to not apply the tactic to the two subgoals produced by + the first goal. To do this can result in quite messy code. In contrast, the ``reverse application'' is easy to implement. - However, this example is very contrived: there are much simpler methods to implement - such a proof procedure analysing a goal according to its topmost - connective. These simpler methods use tactic combinators which will be explained + Of course, this example is contrived: there are much simpler methods available in + Isabelle for implementing a proof procedure analysing a goal according to its topmost + connective. These simpler methods use tactic combinators, which we will explain in the next section. *} section {* Tactic Combinators *} 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 - strings two tactics together in sequence. For example: + The purpose of tactic combinators is to build compound tactics out of + smaller tactics. In the previous section we already used @{ML THEN}, which + just strings together two tactics in a sequence. For example: *} lemma shows "(Foo \ Bar) \ False" @@ -713,12 +758,14 @@ (*<*)oops(*>*) text {* + Here you only have to specify the subgoal of interest only once and + it is consistently applied to the component tactics. 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 + the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also be written as: *} @@ -726,28 +773,32 @@ atac, rtac @{thm disjI1}, atac]*} text {* - 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 + There is even another way of implementing this tactic: 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 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'} - (or @{ML FIRST1}) for a list of tactics. For example, the tactic + and just call @{ML foo_tac1}. + + With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be + 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'} (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 whether rule @{text disjI} applies and after that - whether @{text conjI}. To see this consider the proof: + @{text conjI}. To see this consider the proof *} lemma shows "True \ False" and "Foo \ Bar" @@ -763,8 +814,8 @@ text {* - Using @{ML FIRST'} we can write our @{ML select_tac} from Page~\ref{tac:selecttac} - simply as follows: + Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} + as follows: *} ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, @@ -772,9 +823,10 @@ text {* 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: + we must include @{ML all_tac} at the end of the list, otherwise the tactic will + fail if no rule applies (we laso have to wrap @{ML all_tac} using the + @{ML K}-combinator, because it does not take a subgoal number as argument). You can + test the tactic on the same goals: *} lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" @@ -788,9 +840,9 @@ (*<*)oops(*>*) text {* - 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 + Since such repeated applications of a tactic to the reverse order of + \emph{all} subgoals is quite common, there is the tactic combinator + @{ML ALLGOALS} that simplifies this. Using this combinator you can simply write: *} lemma shows "A \ B" and "A \ B \C" and "\x. D x" and "E \ F" @@ -801,9 +853,9 @@ (*<*)oops(*>*) text {* - 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 + Remember that we chose to implement @{ML select_tac'} so that it + always succeeds. This can be potentially very confusing for the user, + for example, in cases where the goal is the form *} lemma shows "E \ F" @@ -814,18 +866,22 @@ (*<*)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 - 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 + In this case no rule applies. The problem for the user is that there is little + chance to see whether or not progress in the proof has been made. By convention + therefore, tactics visible to the user should either change something or fail. + + To comply with this convention, we could simply delete the @{ML "K all_tac"} + from the end of the theorem list. As a result @{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 \emph{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 error message: +txt{* gives the error message: \begin{isabelle} @{text "*** empty result sequence -- proof command failed"}\\ @{text "*** At command \"apply\"."} @@ -834,32 +890,34 @@ text {* - Meaning the tactic failed. - - 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 + We can further extend @{ML select_tac'} so that it not just applies to the topmost + connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal + completely. For this you can use the tactic combinator @{ML REPEAT}. As an example + suppose the following tactic *} ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *} -text {* and the proof *} +text {* which applied to the proof *} lemma shows "((\A) \ (\x. B x)) \ (C \ D)" apply(tactic {* repeat_xmp *}) -txt{* \begin{minipage}{\textwidth} +txt{* produces + + \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 + because otherwise @{ML REPEAT} runs into an infinite loop (it applies the + tactic as long as it succeeds). 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 + If you are after the ``primed'' version of @{ML repeat_xmp} then you + need to implement it as *} ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*} @@ -869,17 +927,16 @@ 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}. + that goals 2 and 3 are not analysed. This is because the tactic + is applied repeatedly only to the first subgoal. To analyse also all + resulting subgoals, you can use the tactic combinator @{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. + you see that the following goal *} lemma shows "((\A) \ (\x. B x)) \ (C \ D)" @@ -890,26 +947,31 @@ (*<*)oops(*>*) text {* - The last tactic combinator we describe here is @{ML DETERM}. Recall - that tactics produce a lazy sequence of successor goal states. These + is completely analysed according to the theorems we chose to + include in @{ML select_tac}. + + 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 +txt{* applies the rule to the first assumption yielding the goal state:\smallskip \begin{minipage}{\textwidth} @{subgoals [display]} - \end{minipage} *} + \end{minipage}\smallskip + + After typing + *} (*<*) oops lemma "\P1 \ Q1; P2 \ Q2\ \ R" apply(tactic {* etac @{thm disjE} 1 *}) (*>*) back -txt{* whereas it is now applied to the second +txt{* the rule now applies to the second assumption.\smallskip \begin{minipage}{\textwidth} @{subgoals [display]} @@ -918,8 +980,9 @@ 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}. + the potential to explode the search space for tactics. + These problems can be avoided by prefixing the tactic with the tactic + combinator @{ML DETERM}. *} lemma "\P1 \ Q1; P2 \ Q2\ \ R" @@ -929,7 +992,7 @@ \end{minipage} *} (*<*)oops(*>*) text {* - This will prune the search space to just the first possibility. + This will combinator prune the search space to just the first successful application. Attempting to apply \isacommand{back} in this goal states gives the error message: @@ -939,7 +1002,7 @@ \end{isabelle} \begin{readmore} - Most tactic combinators are defined in @{ML_file "Pure/tctical.ML"}. + Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. \end{readmore} *} diff -r 8bea3f74889d -r b4234e8a0202 cookbook.pdf Binary file cookbook.pdf has changed