diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Tactical.thy Sat Feb 07 12:05:02 2009 +0000 @@ -6,20 +6,22 @@ text {* - The main reason for descending to the ML-level of Isabelle is to be able to - implement automatic proof procedures. Such proof procedures usually lessen - considerably the burden of manual reasoning, for example, when introducing - new definitions. These proof procedures are centred around refining a goal - state using tactics. This is similar to the @{text apply}-style reasoning at - the user level, where goals are modified in a sequence of proof steps until - all of them are solved. However, there are also more structured operations - that help with handling of variables and assumptions. + The main reason for descending to the ML-level of Isabelle is to be + able to implement automatic proof procedures. Such proof procedures usually + lessen considerably the burden of manual reasoning, for example, when + introducing new definitions. These proof procedures are centred around + refining a goal state using tactics. This is similar to the @{text + apply}-style reasoning at the user level, where goals are modified in a + sequence of proof steps until all of them are solved. However, there are + also more structured operations available on the ML-level that help with + the handling of variables and assumptions. + *} -section {* Tactical Reasoning *} +section {* Basics of Reasoning with Tactics*} text {* - To see how tactics work, let us first transcribe a simple @{text apply}-style proof + To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof into ML. Consider the following proof. *} @@ -57,7 +59,10 @@ it can make use of the local assumptions (there are none in this example). The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to @{text erule}, @{text rule} and @{text assumption}, respectively. - The operator @{ML THEN} strings the tactics together. + The operator @{ML THEN} strings the tactics together. A difference + between the \isacommand{apply}-script and the ML-code is that the + former causes the lemma to be stored under the name @{text "disj_swap"}, + whereas the latter does not include any code for this. \begin{readmore} To learn more about the function @{ML Goal.prove} see \isccite{sec:results} @@ -75,8 +80,8 @@ actually applied. This problem is nicely prevented by using antiquotations, because then the theorems are fixed statically at compile-time. - During the development of automatic proof procedures, it will often be necessary - to test a tactic on examples. This can be conveniently + During the development of automatic proof procedures, you will often find it + necessary to test a tactic on examples. This can be conveniently done with the command \isacommand{apply}@{text "(tactic \ \ \)"}. Consider the following sequence of tactics *} @@ -96,13 +101,15 @@ text {* By using @{text "tactic \ \ \"} in the apply-step, - you can call @{ML foo_tac} or any function that returns a tactic from the - user level of Isabelle. + you can call from the user level of Isabelle the tactic @{ML foo_tac} or + any other function that returns a tactic. - As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that - stands for the subgoal analysed by the tactic. In our case, we only focus on the first - subgoal. This is sometimes wanted, but usually not. To avoid the explicit numbering in the - tactic, you can write + The tactic @{ML foo_tac} is just a sequence of simple tactics stringed + together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} + 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 is + sometimes wanted, but usually not. To avoid the explicit numbering in + the tactic, you can write *} ML{*val foo_tac' = @@ -114,9 +121,9 @@ text {* and then give the number for the subgoal explicitly when the tactic is - called. For every operator that combines tactics, such a primed version - exists. So in the next proof we can first discharge the second subgoal, - and after that the first. + called. For every operator that combines tactics (@{ML THEN} is only one + such operator), a primed version exists. So in the next proof you + can first discharge the second subgoal, and after that the first. *} lemma "P1 \ Q1 \ Q1 \ P1" @@ -126,11 +133,11 @@ done text {* - (FIXME: maybe add something about how each goal state is interpreted - as a theorem) + This kind of addressing is more difficult to achieve when the goal is + hard-coded inside the tactic. - The tactic @{ML foo_tac} (and @{ML foo_tac'}) are very specific for - analysing goals only of the form @{prop "P \ Q \ Q \ P"}. If the goal is not + 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 @{ML foo_tac} throws the error message: \begin{isabelle} @@ -140,12 +147,29 @@ Meaning the tactic 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 + hence the type of a tactic is: @{text [display, gray] "type tactic = thm -> thm Seq.seq"} It is custom that if a tactic fails, it should return the empty sequence: - tactics should not raise exceptions willy-nilly. + your own tactics should not raise exceptions willy-nilly. + + The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns + the empty sequence and is defined as +*} + +ML{*fun no_tac thm = Seq.empty*} + +text {* + which means @{ML no_tac} always fails. The second returns the given theorem wrapped + as a single member sequence. It 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 + with the proof). The lazy list of possible successor states shows through to the user-level of Isabelle when using the command \isacommand{back}. For instance in the @@ -158,10 +182,12 @@ back done + text {* By using \isacommand{back}, we construct the proof that uses the - second assumption to complete the proof. In more interesting - situations, different possibilities can lead to different proofs. + 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. \begin{readmore} See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy @@ -170,9 +196,95 @@ instead. \end{readmore} + For a beginner it might be surprising that tactics, which transform + one proof state to the next, are functions from theorems to theorem + (sequences). The surprise resolves by knowing that every + proof state is indeed a theorem. To shed more light on this, + let us modify the code of @{ML all_tac} to obtain the following + tactic +*} + +ML{*fun my_print_tac ctxt thm = + let + val _ = warning (str_of_thm ctxt thm) + in + 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 + now can inspect every proof state in the follwing proof. On the left-hand + side we show the goal state as shown by the system; on the right-hand + side the print out from our @{ML my_print_tac}. +*} + +lemma shows "\A; B\ \ A \ B" +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{minipage}[t]{0.3\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"} + \end{tabular} *} -section {* Basic Tactics *} +apply(rule conjI) +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}} + \begin{minipage}[t]{0.26\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "(\A; B\ \ A) \ (\A; B\ \ B) \ (\A; B\ \ A \ B)"} + \end{tabular} +*} + +apply(assumption) +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{minipage}[t]{0.3\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "(\A; B\ \ B) \ (\A; B\ \ A \ B)"} + \end{tabular} +*} + +apply(assumption) +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{minipage}[t]{0.3\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "\A; B\ \ A \ B"} + \end{tabular} +*} + +done + +text {* + 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. Since the goal @{term C} can potentially be an implication, + there is a protector (invisible in the print out above) wrapped around + it. This prevents that premises are misinterpreted 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. + +*} + +section {* Simple Tactics *} text {* As seen above, the function @{ML atac} corresponds to the assumption tactic. @@ -184,7 +296,7 @@ text {* Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond - to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule}, + to @{text rule}, @{text drule}, @{text erule} and @{text frule}, respectively. Below are three examples with the resulting goal state. How they work should therefore be self-explanatory. *} @@ -247,7 +359,7 @@ (*<*)oops(*>*) text {* - Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and + Also for useful for debugging purposes are the tactics @{ML all_tac} and @{ML no_tac}. The former always succeeds (but does not change the goal state), and the latter always fails. @@ -274,9 +386,9 @@ val _ = (warning ("params: " ^ str_of_params); warning ("schematics: " ^ str_of_schms); - warning ("asms: " ^ str_of_asms); - warning ("concl: " ^ str_of_concl); - warning ("prems: " ^ str_of_prems)) + warning ("assumptions: " ^ str_of_asms); + warning ("conclusion: " ^ str_of_concl); + warning ("premises: " ^ str_of_prems)) in no_tac end*} @@ -303,11 +415,11 @@ \begin{quote}\small \begin{tabular}{ll} - params: & @{term x}, @{term y}\\ - schematics: & @{term z}\\ - asms: & @{term "A x y"}\\ - concl: & @{term "B y x \ C (z y) x"}\\ - prems: & @{term "A x y"} + params: & @{term x}, @{term y}\\ + schematics: & @{term z}\\ + assumptions: & @{term "A x y"}\\ + conclusion: & @{term "B y x \ C (z y) x"}\\ + premises: & @{term "A x y"} \end{tabular} \end{quote} @@ -335,11 +447,11 @@ \begin{quote}\small \begin{tabular}{ll} - params: & @{term x}, @{term y}\\ - schematics: & @{term z}\\ - asms: & @{term "A x y"}, @{term "B y x"}\\ - concl: & @{term "C (z y) x"}\\ - prems: & @{term "A x y"}, @{term "B y x"} + params: & @{term x}, @{term y}\\ + schematics: & @{term z}\\ + assumptions: & @{term "A x y"}, @{term "B y x"}\\ + conclusion: & @{term "C (z y) x"}\\ + premises: & @{term "A x y"}, @{term "B y x"} \end{tabular} \end{quote} *} @@ -428,35 +540,6 @@ @{ML resolve_tac} *} - - -text {* - - - A goal (or goal state) is a special @{ML_type thm}, which by - convention 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 open - subgoals. - Since the goal @{term C} can potentially be an implication, there is a - @{text "#"} wrapped around it, which prevents that premises are - misinterpreted as open subgoals. The wrapper @{text "# :: prop \ - prop"} is just the identity function and used as a syntactic marker. - - - - - - 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. - - - -*} - section {* Structured Proofs *} lemma True @@ -495,4 +578,5 @@ *} + end \ No newline at end of file