diff -r fe10da5354a3 -r 5dcad9348e4d CookBook/Tactical.thy --- a/CookBook/Tactical.thy Sat Feb 07 14:21:33 2009 +0000 +++ b/CookBook/Tactical.thy Sun Feb 08 08:45:25 2009 +0000 @@ -100,8 +100,8 @@ done text {* - By using @{text "tactic \ \ \"} in the apply-step, - you can call from the user level of Isabelle the tactic @{ML foo_tac} or + By using @{text "tactic \ \ \"} you can call from the + user level of Isabelle the tactic @{ML foo_tac} or any other function that returns a tactic. The tactic @{ML foo_tac} is just a sequence of simple tactics stringed @@ -196,10 +196,10 @@ instead. \end{readmore} - For a beginner it might be surprising that tactics, which transform + 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, + 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 tactic *} @@ -216,7 +216,7 @@ 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}. + side the print out from @{ML my_print_tac}. *} lemma shows "\A; B\ \ A \ B" @@ -275,9 +275,12 @@ @{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. + subgoals. So in the first step the goal state is always of the form + @{text "C \ (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 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. @@ -297,23 +300,30 @@ text {* Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond 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. + 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. *} lemma shows "P \ Q" apply(tactic {* rtac @{thm conjI} 1 *}) -txt{*@{subgoals [display]}*} +txt{*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} (*<*)oops(*>*) lemma shows "P \ Q \ False" apply(tactic {* etac @{thm conjE} 1 *}) -txt{*@{subgoals [display]}*} +txt{*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} (*<*)oops(*>*) lemma shows "False \ True \ False" apply(tactic {* dtac @{thm conjunct2} 1 *}) -txt{*@{subgoals [display]}*} +txt{*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} (*<*)oops(*>*) text {* @@ -323,7 +333,9 @@ lemma shows "Foo" and "P \ Q" apply(tactic {* rtac @{thm conjI} 2 *}) -txt {*@{subgoals [display]}*} +txt {*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} (*<*)oops(*>*) text {* @@ -343,7 +355,9 @@ lemma shows "C \ (A \ B)" and "(A \ B) \ C" apply(tactic {* resolve_tac_xmp 1 *}) apply(tactic {* resolve_tac_xmp 2 *}) -txt{* @{subgoals [display]} *} +txt{*\begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}*} (*<*)oops(*>*) text {* @@ -359,15 +373,12 @@ (*<*)oops(*>*) text {* - 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. - + (FIXME explain RS MRS) - Often proofs involve elaborate operations on assumptions and variables - @{text "\"}-quantified in the goal state. To do such operations on the ML-level - using the basic tactics, is very unwieldy and brittle. Some convenience and + 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 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. *} @@ -426,15 +437,15 @@ Note in the actual output the brown colour of the variables @{term x} and @{term y}. Although parameters in the original goal, they are fixed inside the subproof. Similarly the schematic variable @{term z}. The assumption - is bound once as @{ML_type cterm} to the record-variable @{text asms} and - another time as @{ML_type thm} to @{text prems}. + @{prop "A x y"} is bound once as @{ML_type cterm} to the record-variable + @{text asms} and another time 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 the error message. + by an error message. If we continue the proof script by applying the @{text impI}-rule *} @@ -458,7 +469,7 @@ (*<*)oops(*>*) text {* - where we now also have @{term "B y x"} as assumption. + where we now also have @{term "B y x"} as an assumption. One convenience of @{ML SUBPROOF} is that we can apply assumption using the usual tactics, because the parameter @{text prems} @@ -466,23 +477,42 @@ implement a tactic that almost behaves like @{ML atac}: *} +ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*} lemma shows "\x y. \B x y; A x y; C x y\ \ A x y" -apply(tactic - {* SUBPROOF (fn {prems, ...} => resolve_tac prems 1) @{context} 1 *}) +apply(tactic {* atac' @{context} 1 *}) txt{* yields @{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 + 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 + 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 proof inside. It is therefore possible to also apply + @{ML atac'} to the second goal: +*} + +lemma shows "True" and "\x y. \B x y; A x y; C x y\ \ A x y" +apply(tactic {* atac' @{context} 2 *}) +txt{* This gives: + @{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 - an advantage in the situations for which @{ML SUBPROOF} was designed: - the reason is that instantiation of schematic variables can potentially - has affect several goals and can render them unprovable. - - A similar but less powerful function is @{ML SUBGOAL}. It allows you to - inspect a subgoal specified by a number. + A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. + It allows you to inspect a subgoal specified by a number. With this we can + implement a little tactic that applies a rule corresponding to its + topmost connective. The tactic should only apply ``safe'' rules (that is + which do not render the goal unprovable). For this we can write: *} ML %linenumbers{*fun select_tac (t,i) = @@ -492,12 +522,13 @@ | @{term "op \"} $ _ $ _ => rtac @{thm impI} i | @{term "Not"} $ _ => rtac @{thm notI} i | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i - | _ => no_tac*} + | _ => all_tac*} -lemma shows "A \ B" "A \ B" "\x. C x" +lemma shows "A \ B" "A \ B" "\x. C x" "D \ E" +apply(tactic {* SUBGOAL select_tac 4 *}) +apply(tactic {* SUBGOAL select_tac 3 *}) +apply(tactic {* SUBGOAL select_tac 2 *}) apply(tactic {* SUBGOAL select_tac 1 *}) -apply(tactic {* SUBGOAL select_tac 3 *}) -apply(tactic {* SUBGOAL select_tac 4 *}) txt{* @{subgoals [display]} *} (*<*)oops(*>*) @@ -506,6 +537,8 @@ to implement a proof procedure like the one above. They will be explained in the next section. + (Notice that we applied the goals in reverse order) + A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal as @{ML_type cterm} instead of a @{ML_type term}. *}