theory Tactical+ −
imports Base FirstSteps+ −
begin+ −
+ −
chapter {* Tactical Reasoning\label{chp:tactical} *}+ −
+ −
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 \isacommand{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 {* Basics of Reasoning with Tactics*}+ −
+ −
text {*+ −
To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof + −
into ML. Consider the following proof.+ −
*}+ −
+ −
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"+ −
apply(erule disjE)+ −
apply(rule disjI2)+ −
apply(assumption)+ −
apply(rule disjI1)+ −
apply(assumption)+ −
done+ −
+ −
text {*+ −
This proof translates to the following ML-code.+ −
+ −
@{ML_response_fake [display,gray]+ −
"let+ −
val ctxt = @{context}+ −
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}+ −
in+ −
Goal.prove ctxt [\"P\", \"Q\"] [] goal + −
(fn _ => + −
etac @{thm disjE} 1+ −
THEN rtac @{thm disjI2} 1+ −
THEN atac 1+ −
THEN rtac @{thm disjI1} 1+ −
THEN atac 1)+ −
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}+ −
+ −
To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C+ −
tac"} sets up a goal state for proving the goal @{text C} + −
(that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the+ −
assumptions @{text As} (happens to be empty) with the variables+ −
@{text xs} that will be generalised once the goal is proved (in our case+ −
@{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;+ −
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. + −
+ −
\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+ −
"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+ −
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. + −
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+ −
then the theorems are fixed statically at compile-time.+ −
+ −
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 \<verbopen> \<dots> \<verbclose>)"}. + −
Consider the following sequence of tactics+ −
*}+ −
+ −
ML{*val foo_tac = + −
(etac @{thm disjE} 1+ −
THEN rtac @{thm disjI2} 1+ −
THEN atac 1+ −
THEN rtac @{thm disjI1} 1+ −
THEN atac 1)*}+ −
+ −
text {* and the Isabelle proof: *}+ −
+ −
lemma "P \<or> Q \<Longrightarrow> Q \<or> P"+ −
apply(tactic {* foo_tac *})+ −
done+ −
+ −
text {*+ −
By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} 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+ −
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 hard-coding+ −
of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, + −
you can write\label{tac:footacprime}+ −
*}+ −
+ −
ML{*val foo_tac' = + −
(etac @{thm disjE} + −
THEN' rtac @{thm disjI2} + −
THEN' atac + −
THEN' rtac @{thm disjI1} + −
THEN' atac)*}+ −
+ −
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.+ −
*}+ −
+ −
lemma "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"+ −
and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"+ −
apply(tactic {* foo_tac' 2 *})+ −
apply(tactic {* foo_tac' 1 *})+ −
done+ −
+ −
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 + −
(@{ML THEN} is only one such operator) a ``primed'' version exists.+ −
+ −
The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for+ −
analysing goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not+ −
of this form, then they throw 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:+ −
+ −
@{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. 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+ −
*}+ −
+ −
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; @{ML all_tac} 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).+ −
+ −
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'}: either using the first assumption or the second.+ −
*}+ −
+ −
lemma "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"+ −
apply(tactic {* foo_tac' 1 *})+ −
back+ −
done+ −
+ −
+ −
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.+ −
+ −
\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.+ −
\end{readmore}+ −
+ −
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 + −
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+ −
*}+ −
+ −
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+ −
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 "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> 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 "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}+ −
\end{tabular}+ −
*}+ −
+ −
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 "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> 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 "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> 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 "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}+ −
\end{tabular}+ −
*}+ −
+ −
done+ −
+ −
text {*+ −
As can be seen, internally every goal state is an implication of the form+ −
+ −
@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (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 \<Longrightarrow> (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 \<Rightarrow> 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. + −
+ −
*}+ −
+ −
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.+ −
*}+ −
+ −
lemma shows "False \<Longrightarrow> True"+ −
apply(tactic {* print_tac "foo message" *})+ −
txt{*\begin{minipage}{\textwidth}\small+ −
@{text "foo message"}\\[3mm] + −
@{prop "False \<Longrightarrow> True"}\\+ −
@{text " 1. False \<Longrightarrow> True"}\\+ −
\end{minipage}+ −
*}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
Another simple tactic is the function @{ML atac}, which, as shown in the previous+ −
section, corresponds to the assumption command.+ −
*}+ −
+ −
lemma shows "P \<Longrightarrow> P"+ −
apply(tactic {* atac 1 *})+ −
done+ −
+ −
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. + −
*}+ −
+ −
lemma shows "P \<and> Q"+ −
apply(tactic {* rtac @{thm conjI} 1 *})+ −
txt{*\begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage}*}+ −
(*<*)oops(*>*)+ −
+ −
lemma shows "P \<and> Q \<Longrightarrow> False"+ −
apply(tactic {* etac @{thm conjE} 1 *})+ −
txt{*\begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage}*}+ −
(*<*)oops(*>*)+ −
+ −
lemma shows "False \<and> True \<Longrightarrow> False"+ −
apply(tactic {* dtac @{thm conjunct2} 1 *})+ −
txt{*\begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage}*}+ −
(*<*)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.+ −
*}+ −
+ −
lemma shows "Foo" and "P \<and> Q"+ −
apply(tactic {* rtac @{thm conjI} 2 *})+ −
txt {*\begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage}*}+ −
(*<*)oops(*>*)+ −
+ −
text {* + −
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+ −
explored via the lazy sequences mechanism). Given the code+ −
*}+ −
+ −
ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}+ −
+ −
text {*+ −
an example for @{ML resolve_tac} is the following proof where first an outermost + −
implication is analysed and then an outermost conjunction.+ −
*}+ −
+ −
lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"+ −
apply(tactic {* resolve_tac_xmp 1 *})+ −
apply(tactic {* resolve_tac_xmp 2 *})+ −
txt{*\begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}*}+ −
(*<*)oops(*>*)+ −
+ −
text {* + −
Similarly versions exists for @{ML atac} (@{ML assume_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:+ −
*}+ −
+ −
lemma shows "True \<noteq> 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+ −
pre-instantiating theorems with other theorems. You can do this using the+ −
function @{ML RS}. For example+ −
+ −
@{ML_response_fake [display,gray]+ −
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}+ −
+ −
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}" + −
"*** Exception- THM (\"RSN: no unifiers\", 1, + −
[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?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 =+ −
let + −
val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt+ −
in+ −
thm'+ −
end*}+ −
+ −
text {*+ −
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})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}+ −
+ −
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})" + −
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> 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.+ −
+ −
@{ML_response_fake [display,gray]+ −
"[@{thm impI}, @{thm disjI2}] RL [@{thm conjI}, @{thm disjI1}]" + −
"[\<lbrakk>P \<Longrightarrow> Q; Qa\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) \<and> Qa,+ −
\<lbrakk>Q; Qa\<rbrakk> \<Longrightarrow> (P \<or> Q) \<and> Qa,+ −
(P \<Longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q) \<or> Qa,+ −
Q \<Longrightarrow> (P \<or> Q) \<or> Qa]"}+ −
+ −
\begin{readmore}+ −
The combinators for instantiating theorems are defined in @{ML_file "Pure/drule.ML"}.+ −
\end{readmore}+ −
+ −
Often proofs involve elaborate operations on assumptions and + −
@{text "\<And>"}-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. + −
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+ −
*}+ −
+ −
text_raw{*+ −
\begin{figure}+ −
\begin{isabelle}+ −
*}+ −
ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = + −
let + −
val str_of_params = str_of_cterms context params+ −
val str_of_asms = str_of_cterms context asms+ −
val str_of_concl = str_of_cterm context concl+ −
val str_of_prems = str_of_thms context prems + −
val str_of_schms = str_of_cterms context (snd schematics) + −
+ −
val _ = (warning ("params: " ^ str_of_params);+ −
warning ("schematics: " ^ str_of_schms);+ −
warning ("assumptions: " ^ str_of_asms);+ −
warning ("conclusion: " ^ str_of_concl);+ −
warning ("premises: " ^ str_of_prems))+ −
in+ −
no_tac + −
end*}+ −
text_raw{*+ −
\end{isabelle}+ −
\caption{A function that prints out the various parameters provided by the tactic+ −
@{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for+ −
extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}+ −
\end{figure}+ −
*}+ −
+ −
+ −
lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"+ −
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?+ −
+ −
txt {*+ −
which gives the printout:+ −
+ −
\begin{quote}\small+ −
\begin{tabular}{ll}+ −
params: & @{term x}, @{term y}\\+ −
schematics: & @{term z}\\+ −
assumptions: & @{term "A x y"}\\+ −
conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\+ −
premises: & @{term "A x y"}+ −
\end{tabular}+ −
\end{quote}+ −
+ −
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 + −
@{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}.+ −
+ −
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.+ −
+ −
If we continue the proof script by applying the @{text impI}-rule+ −
*}+ −
+ −
apply(rule impI)+ −
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?+ −
+ −
txt {*+ −
then @{ML sp_tac} prints out + −
+ −
\begin{quote}\small+ −
\begin{tabular}{ll}+ −
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}+ −
*}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
where we now also have @{term "B y x"} as an assumption.+ −
+ −
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:+ −
*}+ −
+ −
ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}+ −
+ −
text {*+ −
If we apply it to the next lemma+ −
*}+ −
+ −
lemma shows "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"+ −
apply(tactic {* atac' @{context} 1 *})+ −
txt{* we get+ −
@{subgoals [display]} *}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
The restriction in this tactic 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 + −
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 + −
@{ML atac'} to the second goal by just writing:+ −
*}+ −
+ −
lemma shows "True" and "\<And>x y. \<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"+ −
apply(tactic {* atac' @{context} 2 *})+ −
apply(rule TrueI)+ −
done+ −
+ −
+ −
text {*+ −
\begin{readmore}+ −
The function @{ML SUBPROOF} is defined in @{ML_file "Pure/subgoal.ML"} and+ −
also described in \isccite{sec:results}. + −
\end{readmore}+ −
+ −
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 + −
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) =+ −
case t of+ −
@{term "Trueprop"} $ t' => select_tac (t',i)+ −
| @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i+ −
| @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i+ −
| @{term "Not"} $ _ => rtac @{thm notI} i+ −
| Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i+ −
| _ => all_tac*}+ −
+ −
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 like @{prop "A \<and> 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. Consider the four goals:+ −
*}+ −
+ −
+ −
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"+ −
apply(tactic {* SUBGOAL select_tac 4 *})+ −
apply(tactic {* SUBGOAL select_tac 3 *})+ −
apply(tactic {* SUBGOAL select_tac 2 *})+ −
apply(tactic {* SUBGOAL select_tac 1 *})+ −
txt{* \begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage} *}+ −
(*<*)oops(*>*)+ −
+ −
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 it applied in the other order + −
*}+ −
+ −
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"+ −
apply(tactic {* SUBGOAL select_tac 1 *})+ −
apply(tactic {* SUBGOAL select_tac 3 *})+ −
apply(tactic {* SUBGOAL select_tac 4 *})+ −
apply(tactic {* SUBGOAL select_tac 5 *})+ −
(*<*)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, + −
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+ −
connective. These simpler methods use tactic combinators which will be explained + −
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:+ −
*}+ −
+ −
lemma shows "(Foo \<and> Bar) \<and> False"+ −
apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})+ −
txt {* \begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage} *}+ −
(*<*)oops(*>*)+ −
+ −
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:+ −
*}+ −
+ −
lemma shows "(Foo \<and> Bar) \<and> False"+ −
apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})+ −
txt {* \begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage} *}+ −
(*<*)oops(*>*)+ −
+ −
text {* + −
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]*}+ −
+ −
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 whether rule @{text disjI} applies and after that + −
whether @{text conjI}. To see this consider the proof:+ −
*}+ −
+ −
lemma shows "True \<and> False" and "Foo \<or> Bar"+ −
apply(tactic {* orelse_xmp 1 *})+ −
apply(tactic {* orelse_xmp 3 *})+ −
txt {* which results in the goal state+ −
+ −
\begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}+ −
*}+ −
(*<*)oops(*>*)+ −
+ −
+ −
text {*+ −
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 \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> 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 \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 *}+ −
+ −
text {*+ −
@{ML rewrite_goals_tac}+ −
@{ML ObjectLogic.full_atomize_tac}+ −
@{ML ObjectLogic.rulify_tac}+ −
*}+ −
+ −
+ −
section {* Structured Proofs *}+ −
+ −
lemma True+ −
proof+ −
+ −
{+ −
fix A B C+ −
assume r: "A & B \<Longrightarrow> C"+ −
assume A B+ −
then have "A & B" ..+ −
then have C by (rule r)+ −
}+ −
+ −
{+ −
fix A B C+ −
assume r: "A & B \<Longrightarrow> C"+ −
assume A B+ −
note conjI [OF this]+ −
note r [OF this]+ −
}+ −
oops+ −
+ −
ML {* fun prop ctxt s =+ −
Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}+ −
+ −
ML {* + −
val ctxt0 = @{context};+ −
val ctxt = ctxt0;+ −
val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;+ −
val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;+ −
val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;+ −
val this = [@{thm conjI} OF this]; + −
val this = r OF this;+ −
val this = Assumption.export false ctxt ctxt0 this + −
val this = Variable.export ctxt ctxt0 [this] + −
*}+ −
+ −
+ −
+ −
end+ −