# HG changeset patch # User Christian Urban # Date 1234374024 0 # Node ID 8bea3f74889de6f6bb09f32b32c7e7697ba64e7f # Parent 258ce361ba1babdc91b5aa0e8b3be123dcca834e added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*) diff -r 258ce361ba1b -r 8bea3f74889d CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Feb 09 04:18:14 2009 +0000 +++ b/CookBook/FirstSteps.thy Wed Feb 11 17:40:24 2009 +0000 @@ -171,11 +171,11 @@ end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} The code about simpsets extracts the theorem names stored in the - current simpset. We get hold of the current simpset with the antiquotation + current simpset. You can get hold of the current simpset with the antiquotation @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record containing all information about the simpset. The rules of a simpset are stored in a \emph{discrimination net} (a data structure for fast - indexing). From this net we can extract the entries using the function @{ML + indexing). From this net you can extract the entries using the function @{ML Net.entries}. @@ -258,7 +258,7 @@ @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \) $ Free (\"x\", \), Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} - where an coercion is inserted in the second component and + where a coercion is inserted in the second component and @{ML_response [display,gray] "(@{term \"P x \ Q x\"}, @{prop \"P x \ Q x\"})" "(Const (\"==>\", \) $ \ $ \, Const (\"==>\", \) $ \ $ \)"} @@ -345,7 +345,7 @@ (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) - Although to some extend types of terms can be inferred, there are many + Although types of terms can often be inferred, there are many situations where you need to construct types manually, especially when defining constants. For example the function returning a function type is as follows: @@ -387,7 +387,7 @@ A handy function for manipulating terms is @{ML map_types}: it takes a function and applies it to every type in the term. You can, for example, - change every @{typ nat} into an @{typ int} using the function + change every @{typ nat} in a term into an @{typ int} using the function *} ML{*fun nat_to_int t = @@ -411,7 +411,7 @@ text {* - You can freely construct and manipulate terms, since they are just + You can freely construct and manipulate @{ML_type "term"}s, since they are just arbitrary unchecked trees. However, you eventually want to see if a term is well-formed, or type-checks, relative to a theory. Type-checking is done via the function @{ML cterm_of}, which converts @@ -525,6 +525,8 @@ section {* Storing Theorems *} +text {* @{ML PureThy.add_thms_dynamic} *} + section {* Theorem Attributes *} section {* Printing Terms and Theorems\label{sec:printing} *} @@ -695,11 +697,11 @@ text {* which is the function composed of first the increment-by-one function and then increment-by-two, followed by increment-by-three. Again, the reverse function - composition allows one to read the code top-down. + composition allows you to read the code top-down. The remaining combinators described in this section add convenience for the ``waterfall method'' of writing functions. The combinator @{ML tap} allows - one to get hold of an intermediate result (to do some side-calculations for + you to get hold of an intermediate result (to do some side-calculations for instance). The function *} @@ -709,12 +711,13 @@ |> tap (fn x => tracing (makestring x)) |> (fn x => x + 2)*} -text {* increments the argument first by one and then by two. In the middle (Line 3), - however, it uses @{ML tap} for printing the ``plus-one'' intermediate - result inside the tracing buffer. The function @{ML tap} can only - be used for side-calculations, because any value that is computed cannot - be merged back into the ``main waterfall''. To do this, you can use the next - combinator. +text {* + increments the argument first by @{text "1"} and then by @{text "2"}. In the + middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one'' + intermediate result inside the tracing buffer. The function @{ML tap} can + only be used for side-calculations, because any value that is computed + cannot be merged back into the ``main waterfall''. To do this, you can use + the next combinator. The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value and returns the result together with the value (as a pair). For example @@ -752,7 +755,7 @@ ML{*fun (x, y) |-> f = f x y*} text {* and can be used to write the following roundabout version - of the @{text double} function + of the @{text double} function: *} ML{*fun double x = @@ -764,7 +767,7 @@ reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, @{ML "|>>"} and @{ML "||>"} described above have related combinators for function composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, - for example, the function @{text double} can also be written as + for example, the function @{text double} can also be written as: *} ML{*val double = diff -r 258ce361ba1b -r 8bea3f74889d CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Feb 09 04:18:14 2009 +0000 +++ b/CookBook/Intro.thy Wed Feb 11 17:40:24 2009 +0000 @@ -89,7 +89,7 @@ Whenever appropriate we also show the response the code generates when evaluated. This response is prefixed with a - @{text [quotes] ">"} like: + @{text [quotes] ">"}, like: @{ML_response [display,gray] "3 + 4" "7"} diff -r 258ce361ba1b -r 8bea3f74889d CookBook/Parsing.thy --- a/CookBook/Parsing.thy Mon Feb 09 04:18:14 2009 +0000 +++ b/CookBook/Parsing.thy Wed Feb 11 17:40:24 2009 +0000 @@ -37,7 +37,7 @@ text {* Let us first have a look at parsing strings using generic parsing combinators. - The function @{ML "(op $$)"} takes a string as argument and will ``consume'' this string from + The function @{ML "$$"} takes a string as argument and will ``consume'' this string from a given input list of strings. ``Consume'' in this context means that it will return a pair consisting of this string and the rest of the input list. For example: @@ -61,13 +61,13 @@ \item @{text "MORE"} indicates that there is not enough input for the parser. For example in @{text "($$ \"h\") []"}. \item @{text "ABORT"} is the exception that is raised when a dead end is reached. - It is used for example in the function @{ML "(op !!)"} (see below). + It is used for example in the function @{ML "!!"} (see below). \end{itemize} However, note that these exceptions are private to the parser and cannot be accessed by the programmer (for example to handle them). - Slightly more general than the parser @{ML "(op $$)"} is the function @{ML + Slightly more general than the parser @{ML "$$"} is the function @{ML Scan.one}, in that it takes a predicate as argument and then parses exactly one item from the input list satisfying this predicate. For example the following parser either consumes an @{text [quotes] "h"} or a @{text @@ -84,7 +84,7 @@ end" "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} - Two parser can be connected in sequence by using the function @{ML "(op --)"}. + Two parser can be connected in sequence by using the function @{ML "--"}. For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this sequence you can achieve by: @@ -100,7 +100,7 @@ "(\"hell\", [\"o\"])"} Parsers that explore alternatives can be constructed using the function @{ML - "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the + "||"}. For example, the parser @{ML "(p || q)" for p q} returns the result of @{text "p"}, in case it succeeds, otherwise it returns the result of @{text "q"}. For example: @@ -115,7 +115,7 @@ end" "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"} - The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function + The functions @{ML "|--"} and @{ML "--|"} work like the sequencing function for parsers, except that they discard the item being parsed by the first (respectively second) parser. For example: @@ -155,7 +155,7 @@ (p input1, p input2) end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"} - The function @{ML "(op !!)"} helps to produce appropriate error messages + The function @{ML "!!"} helps to produce appropriate error messages during parsing. For example if you want to parse that @{text p} is immediately followed by @{text q}, or start a completely different parser @{text r}, you might write: @@ -171,7 +171,7 @@ circumstance this will be the wrong parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then caused by the failure of @{text r}, not by the absence of @{text q} in the input. This - kind of situation can be avoided when using the function @{ML "(op !!)"}. + kind of situation can be avoided when using the function @{ML "!!"}. This function aborts the whole process of parsing in case of a failure and prints an error message. For example if you invoke the parser @@ -189,7 +189,7 @@ @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")" "Exception ABORT raised"} - then the parsing aborts and the error message @{text "foo"} is printed out. In order to + then the parsing aborts and the error message @{text "foo"} is printed. In order to see the error message properly, we need to prefix the parser with the function @{ML "Scan.error"}. For example: @@ -430,7 +430,7 @@ end" "((\"where\",\),(\"|\",\))"} - Like before, you can sequentially connect parsers with @{ML "(op --)"}. For example: + Like before, you can sequentially connect parsers with @{ML "--"}. For example: @{ML_response [display,gray] "let @@ -571,7 +571,7 @@ (FIXME: should for-fixes take any syntax annotation?) @{ML OuterParse.for_fixes} is an ``optional'' that prefixes - @{ML OuterParse.fixes} with the comman \isacommand{for}. + @{ML OuterParse.fixes} with the command \isacommand{for}. (FIXME give an example and explain more) @{ML_response [display,gray] 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} *} diff -r 258ce361ba1b -r 8bea3f74889d CookBook/document/root.tex --- a/CookBook/document/root.tex Mon Feb 09 04:18:14 2009 +0000 +++ b/CookBook/document/root.tex Wed Feb 11 17:40:24 2009 +0000 @@ -99,6 +99,11 @@ \newcommand{\isasymverbclose}{\isacharverbatimclose} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% since * cannot be used in text {*...*} +\newenvironment{tabularstar}[2] +{\begin{tabular*}{#1}{#2}}{\end{tabular*}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{document} \title{\mbox{}\\[-10ex] diff -r 258ce361ba1b -r 8bea3f74889d cookbook.pdf Binary file cookbook.pdf has changed