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. Suppose 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} in the code above 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"}. 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 in the code above we use 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 where there are no ML-binding obtain+ −
the theorem dynamically using the function @{ML thm}; for example + −
\mbox{@{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+ −
subsequently 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 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+ −
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 return the error message:+ −
+ −
\begin{isabelle}+ −
@{text "*** empty result sequence -- proof command failed"}\\+ −
@{text "*** At command \"apply\"."}+ −
\end{isabelle}+ −
+ −
This means the tactics failed. The reason for this error message is that tactics + −
are functions mapping a goal state to a (lazy) sequence of successor states. + −
Hence the type of a tactic is:+ −
*}+ −
+ −
ML{*type tactic = thm -> thm Seq.seq*}+ −
+ −
text {*+ −
By convention, if a tactic fails, then it should return the empty sequence. + −
Therefore, if you write your own tactics, they 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 + −
up in 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 goal 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. While in the proof above, it does not really matter which + −
assumption is used, in more interesting cases provability might depend+ −
on exploring different possibilities.+ −
+ −
\begin{readmore}+ −
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy+ −
sequences. In day-to-day Isabelle programming, however, one rarely + −
constructs sequences explicitly, but uses the predefined tactics and + −
tactic combinators instead.+ −
\end{readmore}+ −
+ −
It might be surprising that tactics, which transform+ −
one goal 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_raw {*+ −
\begin{figure}[p]+ −
\begin{isabelle}+ −
*}+ −
lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B" + −
apply(tactic {* my_print_tac @{context} *})+ −
+ −
txt{* \begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}\medskip + −
+ −
\begin{minipage}{\textwidth}+ −
\small\colorbox{gray!20}{+ −
\begin{tabular}{@ {}l@ {}}+ −
internal goal state:\\+ −
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}+ −
\end{tabular}}+ −
\end{minipage}\medskip+ −
*}+ −
+ −
apply(rule conjI)+ −
apply(tactic {* my_print_tac @{context} *})+ −
+ −
txt{* \begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}\medskip+ −
+ −
\begin{minipage}{\textwidth}+ −
\small\colorbox{gray!20}{+ −
\begin{tabular}{@ {}l@ {}}+ −
internal goal state:\\+ −
@{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}}+ −
\end{minipage}\medskip+ −
*}+ −
+ −
apply(assumption)+ −
apply(tactic {* my_print_tac @{context} *})+ −
+ −
txt{* \begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}\medskip+ −
+ −
\begin{minipage}{\textwidth}+ −
\small\colorbox{gray!20}{+ −
\begin{tabular}{@ {}l@ {}}+ −
internal goal state:\\+ −
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}+ −
\end{tabular}}+ −
\end{minipage}\medskip+ −
*}+ −
+ −
apply(assumption)+ −
apply(tactic {* my_print_tac @{context} *})+ −
+ −
txt{* \begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}\medskip + −
+ −
\begin{minipage}{\textwidth}+ −
\small\colorbox{gray!20}{+ −
\begin{tabular}{@ {}l@ {}}+ −
internal goal state:\\+ −
@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}+ −
\end{tabular}}+ −
\end{minipage}\medskip + −
*}+ −
done+ −
text_raw {* + −
\end{isabelle}+ −
\caption{The figure shows a proof where each intermediate goal state is+ −
printed by the Isabelle system and by @{ML my_print_tac}. The latter shows+ −
the goal state as represented internally (highlighted boxes). This+ −
illustrates that every goal state in Isabelle is represented by a theorem:+ −
when we start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is+ −
@{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when we finish the proof the+ −
theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}+ −
\end{figure}+ −
*}+ −
+ −
+ −
text {*+ −
which prints out the given theorem (using the string-function defined in+ −
Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this+ −
tactic we are in the position to inspect every goal state in a+ −
proof. Consider now the proof in Figure~\ref{fig:goalstates}: 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)"}; 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)"}; however this constant+ −
is invisible in the figure). 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. If you use the predefined tactics, which we describe in the next+ −
section, 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 *}+ −
+ −
text {*+ −
Let us start with the tactic @{ML print_tac}, which is quite useful for low-level + −
debugging of tactics. It just prints out a message and the current goal state. + −
Processing the proof+ −
*}+ −
+ −
lemma shows "False \<Longrightarrow> True"+ −
apply(tactic {* print_tac "foo message" *})+ −
txt{*gives:\medskip+ −
+ −
\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 *})+ −
txt{*\begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage}*}+ −
(*<*)oops(*>*)+ −
+ −
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 and attempts to + −
apply it to a goal. Below are three self-explanatory examples.+ −
*}+ −
+ −
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 {*+ −
Note the number in each tactic call. Also as mentioned in the previous section, most + −
basic tactics take such an argument; it addresses the subgoal they are analysing. + −
In the proof below, we first split up the conjunction in 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 {*+ −
(FIXME: is it important to get the number of subgoals?)+ −
+ −
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 taking a list of theorems exist for the tactics + −
@{ML dtac} (@{ML dresolve_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{*produces the goal state\medskip+ −
+ −
\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 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 "\<forall>x\<in>A. P x \<Longrightarrow> Q x"+ −
apply(tactic {* dtac @{thm bspec} 1 *})+ −
txt{*\begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}*}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
where the application of Rule @{text bspec} generates two subgoals involving the+ −
meta-variable @{text "?x"}. Now, 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 given by+ −
pre-instantiating theorems with other theorems. One function to do this is+ −
@{ML RS}+ −
+ −
@{ML_response_fake [display,gray]+ −
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}+ −
+ −
which in the example instantiates the first premise of the @{text conjI}-rule + −
with the rule @{text disjI1}. If the instantiation 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"}+ −
+ −
then the function raises an exception. The function @{ML RSN} is similar to @{ML RS}, but + −
takes an additional number as argument that makes 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.+ −
Using this function for the first @{ML RS}-expression above would produce+ −
the more readable result:+ −
+ −
@{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 second list is instantiated with every + −
theorem in the first.+ −
+ −
@{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 on the ML-level involve elaborate operations on assumptions and + −
@{text "\<And>"}-quantified variables. To do such operations 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 goal state to a record. + −
To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which+ −
takes a record and just prints out the content of this record (using the + −
string transformation functions from 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 {*+ −
The tactic produces the following 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. By convention these fixed variables are printed in brown colour.+ −
Similarly the schematic variable @{term z}. The assumption, or premise, + −
@{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 [quotes] "?"} to the+ −
\isacommand{apply}-command. 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 + −
``empty sequence'' 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 the tactic 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 {*+ −
Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.+ −
+ −
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 you can easily + −
implement a tactic that behaves almost like @{ML atac}:+ −
*}+ −
+ −
ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}+ −
+ −
text {*+ −
If you apply @{ML atac'} to the next lemma+ −
*}+ −
+ −
lemma shows "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"+ −
apply(tactic {* atac' @{context} 1 *})+ −
txt{* it will produce+ −
@{subgoals [display]} *}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
The restriction in this tactic which is not present in @{ML atac} 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, as mentioned before, instantiation of schematic variables can affect + −
several goals and can render them unprovable. @{ML SUBPROOF} is meant + −
to avoid this.+ −
+ −
Notice that @{ML atac'} inside @{ML SUBPROOF} 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"}. This is another advantage + −
of @{ML SUBPROOF}: the addressing inside it is completely + −
local to the tactic inside the subproof. It is therefore possible to also apply + −
@{ML atac'} to the second goal by just writing:+ −
*}+ −
+ −
lemma shows "True" and "\<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 logic connective in the + −
subgoal (to illustrate this we only analyse a few connectives). The code+ −
of the tactic is as follows.\label{tac:selecttac}+ −
*}+ −
+ −
ML %linenosgray{*fun select_tac (t,i) =+ −
case t of+ −
@{term "Trueprop"} $ t' => select_tac (t',i)+ −
| @{term "op \<Longrightarrow>"} $ _ $ 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 {*+ −
The input of the function is a term representing the subgoal and a number+ −
specifying the subgoal of interest. 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 \<and> B"} are not properly+ −
analysed. Similarly with meta-implications in the next line. While for the+ −
first five patterns we can use the @{text "@term"}-antiquotation to+ −
construct the patterns, the pattern in Line 8 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+ −
basic term-constructors. This is not necessary in other cases, because their type+ −
is always fixed to function types involving only the type @{typ bool}. For the+ −
final pattern, we chose to just return @{ML all_tac}. Consequently, + −
@{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 the goals in ``reverse'' order. + −
This is a trick in order to be independent from the subgoals that are + −
produced by the rule. If we had applied it 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 produced by + −
the first goal. To do this can result in quite messy code. In contrast, + −
the ``reverse application'' is easy to implement.+ −
+ −
Of course, this example is contrived: there are much simpler methods available in + −
Isabelle for implementing a proof procedure analysing a goal according to its topmost+ −
connective. These simpler methods use tactic combinators, which we will explain + −
in the next section.+ −
*}+ −
+ −
section {* Tactic Combinators *}+ −
+ −
text {* + −
The purpose of tactic combinators is to build compound tactics out of+ −
smaller tactics. In the previous section we already used @{ML THEN}, which+ −
just strings together two tactics in a 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}. 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 {* + −
Here you only have to specify the subgoal of interest only once and+ −
it is consistently applied to the component tactics.+ −
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~\pageref{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 way of implementing this tactic: 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 {*+ −
and call @{ML foo_tac1}. + −
+ −
With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be+ −
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'} (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 + −
@{text conjI}. To see this consider the proof+ −
*}+ −
+ −
lemma shows "True \<and> False" and "Foo \<or> Bar"+ −
apply(tactic {* orelse_xmp 2 *})+ −
apply(tactic {* orelse_xmp 1 *})+ −
txt {* which results in the goal state+ −
+ −
\begin{minipage}{\textwidth}+ −
@{subgoals [display]} + −
\end{minipage}+ −
*}+ −
(*<*)oops(*>*)+ −
+ −
+ −
text {*+ −
Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} + −
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 behaviour of @{ML select_tac} as closely as possible, + −
we must include @{ML all_tac} at the end of the list, otherwise the tactic will+ −
fail if no rule applies (we also have to wrap @{ML all_tac} using the + −
@{ML K}-combinator, because it does not take a subgoal number as argument). You can + −
test the tactic on the same goals:+ −
*}+ −
+ −
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 {* + −
Since such repeated applications of a tactic to the reverse order of + −
\emph{all} subgoals is quite common, there is the tactic combinator + −
@{ML ALLGOALS} that simplifies this. Using this combinator you 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 {*+ −
Remember that we chose to implement @{ML select_tac'} so that it + −
always succeeds. This can be potentially very confusing for the user, + −
for example, in cases where the goal is the form+ −
*}+ −
+ −
lemma shows "E \<Longrightarrow> F"+ −
apply(tactic {* select_tac' 1 *})+ −
txt{* \begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage} *}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
In this case no rule applies. The problem for the user is that there is little + −
chance to see whether or not progress in the proof has been made. By convention+ −
therefore, tactics visible to the user should either change something or fail.+ −
+ −
To comply with this convention, we could simply delete the @{ML "K all_tac"}+ −
from the end of the theorem list. As a result @{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 \emph{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{* gives the error message:+ −
\begin{isabelle}+ −
@{text "*** empty result sequence -- proof command failed"}\\+ −
@{text "*** At command \"apply\"."}+ −
\end{isabelle} + −
*}(*<*)oops(*>*)+ −
+ −
+ −
text {*+ −
We can further extend @{ML select_tac'} so that it not just applies to the topmost+ −
connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal + −
completely. For this you can use the tactic combinator @{ML REPEAT}. As an example + −
suppose the following tactic+ −
*}+ −
+ −
ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}+ −
+ −
text {* which applied to the proof *}+ −
+ −
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"+ −
apply(tactic {* repeat_xmp *})+ −
txt{* produces+ −
+ −
\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 (it applies the+ −
tactic as long as it succeeds). 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 you + −
need to implement it 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 analysed. This is because the tactic+ −
is applied repeatedly only to the first subgoal. To analyse also all+ −
resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}. + −
Suppose the tactic+ −
*}+ −
+ −
ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}+ −
+ −
text {* + −
you see that the following goal+ −
*}+ −
+ −
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"+ −
apply(tactic {* repeat_all_new_xmp 1 *})+ −
txt{* \begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage} *}+ −
(*<*)oops(*>*)+ −
+ −
text {*+ −
is completely analysed according to the theorems we chose to+ −
include in @{ML select_tac'}. + −
+ −
Recall that tactics produce a lazy sequence of successor goal states. These+ −
states can be explored using the command \isacommand{back}. For example+ −
+ −
*}+ −
+ −
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"+ −
apply(tactic {* etac @{thm disjE} 1 *})+ −
txt{* applies the rule to the first assumption yielding the goal state:\smallskip+ −
+ −
\begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage}\smallskip + −
+ −
After typing+ −
*}+ −
(*<*)+ −
oops+ −
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"+ −
apply(tactic {* etac @{thm disjE} 1 *})+ −
(*>*)+ −
back+ −
txt{* the rule now applies to the second assumption.\smallskip+ −
+ −
\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.+ −
These problems can be avoided by prefixing the tactic with the tactic + −
combinator @{ML DETERM}.+ −
*}+ −
+ −
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"+ −
apply(tactic {* DETERM (etac @{thm disjE} 1) *})+ −
txt {*\begin{minipage}{\textwidth}+ −
@{subgoals [display]}+ −
\end{minipage} *}+ −
(*<*)oops(*>*)+ −
text {*+ −
This combinator will prune the search space to just the first successful application.+ −
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 described in this section are defined in @{ML_file "Pure/tctical.ML"}.+ −
\end{readmore}+ −
+ −
*}+ −
+ −
section {* Rewriting and Simplifier Tactics *}+ −
+ −
text {*+ −
@{ML rewrite_goals_tac}+ −
+ −
@{ML ObjectLogic.full_atomize_tac}+ −
+ −
@{ML ObjectLogic.rulify_tac}+ −
+ −
Something about simprocs.+ −
+ −
*}+ −
+ −
+ −
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+ −