# HG changeset patch # User Christian Urban # Date 1234153094 0 # Node ID 258ce361ba1babdc91b5aa0e8b3be123dcca834e # Parent bdd82350cf226003703372cc89526a92cdc73a43 polished and more material in the tactic chapter diff -r bdd82350cf22 -r 258ce361ba1b CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Feb 09 01:23:35 2009 +0000 +++ b/CookBook/FirstSteps.thy Mon Feb 09 04:18:14 2009 +0000 @@ -43,7 +43,7 @@ value and function bindings, and even those can be undone when the proof script is retracted. As mentioned earlier, we will drop the \isacommand{ML}~@{text "\ \ \"} scaffolding whenever we - show code. The lines prefixed with @{text ">"} are not part of the + show code. The lines prefixed with @{text [quotes] ">"} are not part of the code, rather they indicate what the response is when the code is evaluated. Once a portion of code is relatively stable, you usually want to export it @@ -75,7 +75,7 @@ will print out @{text [quotes] "any string"} inside the response buffer of Isabelle. This function expects a string as argument. If you develop under PolyML, then there is a convenient, though again ``quick-and-dirty'', method for - converting values into strings, namely using the function @{ML makestring}: + converting values into strings, namely the function @{ML makestring}: @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} @@ -92,7 +92,7 @@ It is also possible to redirect the ``channel'' where the string @{text "foo"} is printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive - amounts of trace output. This redirection can be achieved using the code + amounts of trace output. This redirection can be achieved with the code: *} ML{*val strip_specials = @@ -112,12 +112,12 @@ Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} will cause that all tracing information is printed into the file @{text "foo.bar"}. - You can print out error messages with the function @{ML error}, as in: + You can print out error messages with the function @{ML error}; for example: @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""} Section~\ref{sec:printing} will give more information about printing - the main datas tructures of Isabelle, namely @{ML_type term}, @{ML_type cterm} + the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} and @{ML_type thm}. *} @@ -161,7 +161,7 @@ @{ML_response_fake [display,gray] "@{thm allI}" "(\x. ?P x) \ \x. ?P x"} - or simpsets: + and simpsets: @{ML_response_fake [display,gray] "let @@ -385,8 +385,9 @@ number representing their sum. \end{exercise} - (FIXME: maybe should go) - + 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 *} ML{*fun nat_to_int t = @@ -396,6 +397,8 @@ | _ => t)*} text {* + an then apply it as follows: + @{ML_response_fake [display,gray] "map_types nat_to_int @{term \"a = (1::nat)\"}" @@ -424,7 +427,7 @@ @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"} - This can also be wirtten with an antiquotation: + This can also be written with an antiquotation: @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} @@ -458,7 +461,9 @@ text {* Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} that can only be built by going through interfaces. As a consequence, every proof - in Isabelle is correct by construction (FIXME reference LCF-philosophy) + in Isabelle is correct by construction. + + (FIXME reference LCF-philosophy) To see theorems in ``action'', let us give a proof on the ML-level for the following statement: @@ -525,8 +530,8 @@ section {* Printing Terms and Theorems\label{sec:printing} *} text {* - During development, you often want to inspect terms, cterms - or theorems. Isabelle contains elaborate pretty-printing functions for printing them, + During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm} + or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform a term into a string is to use the function @{ML Syntax.string_of_term}. @@ -535,7 +540,7 @@ "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} This produces a string with some printing directions encoded in it. The string - can be properly printed by using @{ML warning} foe example. + can be properly printed by using the function @{ML warning}. @{ML_response_fake [display,gray] "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})" @@ -746,7 +751,9 @@ ML{*fun (x, y) |-> f = f x y*} -text {* and can be used to write the following version of the @{text double} function *} +text {* and can be used to write the following roundabout version + of the @{text double} function +*} ML{*fun double x = x |> (fn x => (x, x)) diff -r bdd82350cf22 -r 258ce361ba1b CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Feb 09 01:23:35 2009 +0000 +++ b/CookBook/Intro.thy Mon Feb 09 04:18:14 2009 +0000 @@ -96,7 +96,7 @@ The usual user-level commands of Isabelle are written in bold, for example \isacommand{lemma}, \isacommand{foobar} and so on. We use @{text "$"} to indicate that a command needs to be run - in a Unix-shell, for example + in a Unix-shell, for example: @{text [display] "$ ls -la"} 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 *} diff -r bdd82350cf22 -r 258ce361ba1b cookbook.pdf Binary file cookbook.pdf has changed