--- a/CookBook/Tactical.thy Sun Feb 08 08:45:25 2009 +0000
+++ b/CookBook/Tactical.thy Mon Feb 09 01:12:00 2009 +0000
@@ -5,16 +5,15 @@
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 @{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.
+ 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.
*}
@@ -59,10 +58,7 @@
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. 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.
+ The operator @{ML THEN} strings the tactics together.
\begin{readmore}
To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
@@ -73,12 +69,15 @@
Isabelle Reference Manual.
\end{readmore}
- Note that we used antiquotations for referencing the theorems. We could also
- just have written @{ML "etac disjE 1"} and so on, but this is 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.
+ Note that we used antiquotations for referencing the theorems. Many theorems
+ also have ML-bindings with the same name. Therefore, we could also just have
+ written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
+ the theorem dynamically using the theorem @{ML thm}; for example @{ML "etac
+ (thm \"disjE\") 1"}. Both ways however are considered bad style. The reason
+ 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
@@ -107,9 +106,9 @@
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
+ 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
*}
ML{*val foo_tac' =
@@ -121,9 +120,8 @@
text {*
and then give the number for the subgoal explicitly when the tactic is
- 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.
+ 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"
@@ -134,25 +132,26 @@
text {*
This kind of addressing is more difficult to achieve when the goal is
- hard-coded inside the tactic.
+ 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 @{ML foo_tac} throws the error message:
+ 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 tactic failed. The reason for this error message is that tactics
+ 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:
- your own tactics should not raise exceptions willy-nilly.
+ therefore 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
@@ -171,7 +170,7 @@
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
+ 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'}.
@@ -214,12 +213,12 @@
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 @{ML my_print_tac}.
+ now can inspect every proof state in a proof. Consider the proof below: on
+ the left-hand side we show the goal state as shown by Isabelle; on the
+ right-hand side the print out from @{ML my_print_tac}.
*}
-lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
+lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
apply(tactic {* my_print_tac @{context} *})
txt{* \small
@@ -275,12 +274,12 @@
@{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 in the first step the goal state is always of the form
+ subgoals. So after setting up the lemma, the goal state is always of the form
@{text "C \<Longrightarrow> (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 are misinterpreted as open subgoals.
+ prevents that premises of @{text C} 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.
@@ -290,7 +289,17 @@
section {* Simple Tactics *}
text {*
- As seen above, the function @{ML atac} corresponds to the assumption tactic.
+ A simple tactic is @{ML print_tac}, which is 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" *})
+(*<*)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"
@@ -327,8 +336,9 @@
(*<*)oops(*>*)
text {*
- As mentioned above, most basic tactics take a number as argument, which
- addresses to subgoal they are analysing.
+ As mentioned in the previous section, most basic tactics take a number as
+ argument, which addresses the subgoal they are analysing. In the proof below,
+ we first break up the second subgoal by focusing on this subgoal first.
*}
lemma shows "Foo" and "P \<and> Q"
@@ -339,10 +349,10 @@
(*<*)oops(*>*)
text {*
- Corresponding to @{ML rtac}, there is also the tactic @{ML resolve_tac}, which
- however expects a list of theorems as arguments. From this list it will apply with
- the first applicable theorem (later theorems that are also applicable can be
- explored via the lazy sequences mechanism). Given the abbreviation
+ 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}]*}
@@ -362,25 +372,71 @@
text {*
Similarly versions exists for @{ML atac} (@{ML assume_tac}), @{ML etac}
- (@{ML eresolve_tac}) and so on.
+ (@{ML eresolve_tac}) and so on.
+
+ (FIXME: @{ML cut_facts_tac})
- The tactic @{ML print_tac} is useful for low-level debugging of tactics: it
- prints out a message and the current goal state.
+ 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}. The function @{ML RSN} is similar, but
+ takes a number and makes explicit which premise should be instantiated.
+ To improve readability we are going use the following function
*}
-
-lemma shows "False \<Longrightarrow> True"
-apply(tactic {* print_tac "foo message" *})
-(*<*)oops(*>*)
+
+ML{*fun no_vars ctxt thm =
+let
+ val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+in
+ thm'
+end*}
text {*
-
- (FIXME explain RS MRS)
+ to transform the schematic variables of a theorem into free variables.
+ This means for the @{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, 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 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{*
@@ -406,17 +462,11 @@
text_raw{*
\end{isabelle}
\caption{A function that prints out the various parameters provided by the tactic
- @{ML SUBPROOF}. It uses the functions extracting strings from @{ML_type cterm}s
- and @{ML_type thm}s, which are defined in Section~\ref{sec:printing}.\label{fig:sptac}}
+ @{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}
*}
-text {*
- 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
-*}
lemma shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
@@ -435,10 +485,10 @@
\end{quote}
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
+ @{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 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 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.
@@ -471,10 +521,10 @@
text {*
where we now also have @{term "B y x"} as an assumption.
- One convenience of @{ML SUBPROOF} is that we can apply assumption
+ One convenience of @{ML SUBPROOF} is that we can apply the assumptions
using the usual tactics, because the parameter @{text prems}
- contains the assumptions as theorems. With this we can easily
- implement a tactic that almost behaves like @{ML atac}:
+ 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)*}
@@ -496,23 +546,26 @@
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
+ local to the subproof inside. It is therefore possible to also apply
@{ML atac'} to the second goal:
*}
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 *})
-txt{* This gives:
- @{subgoals [display]} *}
-(*<*)oops(*>*)
+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 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:
+ It allows you to inspect a specified subgoal. With this you can implement
+ a tactic that applies a rule according to its topmost connective (we only
+ analyse a few connectives). The tactic is as follows:
*}
ML %linenumbers{*fun select_tac (t,i) =
@@ -524,7 +577,21 @@
| Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
| _ => all_tac*}
-lemma shows "A \<and> B" "A \<longrightarrow> B" "\<forall>x. C x" "D \<Longrightarrow> E"
+text {*
+ In line 3 you need to decend under the outermost @{term "Trueprop"} in order
+ to get to the connective you like to analyse. Otherwise goals @{prop "A \<and> B"}
+ are not bropek up. In line 7, the pattern cannot be constructed using the
+ @{text "@term"}-antiquotation, because that would fix the type of the
+ quantified variable. In this case you really have to construct the pattern
+ by using the term-constructors. The other cases work, because their type
+ is always bool. In case that the goal does not fall into any of the categorories,
+ then we chose to just return @{ML all_tac} (i.e., the tactic never fails).
+
+ Let us now see how to apply this tactic.
+*}
+
+
+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 *})
@@ -533,29 +600,72 @@
(*<*)oops(*>*)
text {*
- However, this example is contrived, as there are much simpler ways
- to implement a proof procedure like the one above. They will be explained
- in the next section.
+ Note that we applied it in ``reverse'' order. This is a trick in
+ order to be independent from what subgoals the rule produced. If we had
+ it applied in the other order
+*}
+
+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(*>*)
- (Notice that we applied the goals in reverse order)
+text {*
+ then we have to be careful to not apply the tactic to the two subgoals the
+ first goal produced. This can be messy in an automated proof script. The
+ reverse application, on the other hand, is easy to implement.
- A variant of @{ML SUBGOAL} is @{ML CSUBGOAL} which allows access to the goal
- as @{ML_type cterm} instead of a @{ML_type term}.
+ However, this example is contrived: there are much simpler ways to implement
+ such proof procedure that analyses a goal according to its topmost
+ connective. They will be explained in the next section.
+*}
+
+section {* Tactic Combinators *}
+
+text {*
+ To be able to implement powerful tactics out of smaller component tactics,
+ Isabelle provides tactic combinators. In the previous section we already
+ used @{ML THEN} which strings two tactics together in sequence. For example:
*}
+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(*>*)
-section {* Operations on Tactics *}
-
-text {* @{ML THEN} *}
+text {*
+ If you want to avoid the hard-coded subgoal addressing, then you can use
+ @{ML THEN'}. For example:
+*}
lemma shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* (rtac @{thm conjI} 1)
- THEN (rtac @{thm conjI} 1) *})
-txt {* @{subgoals [display]} *}
+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.
+ In what follows we will, whenever appropriate, prefer the primed version of
+ the tactic combinator and omit to mention the simple one.
+
+ With @{ML THEN} and @{ML THEN'} it must be guaranteed that both tactics
+ sucessfully apply; otherwise the whole tactic will fail. If you want to
+ try out either one tactic, then you can use @{ML ORELSE'}. For
+ example
+*}
+
ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
+text {*
+ will first try out rule @{text disjI} and after that @{text conjI}.
+*}
+
lemma shows "True \<and> False" and "Foo \<or> Bar"
apply(tactic {* orelse_xmp 1 *})
apply(tactic {* orelse_xmp 3 *})
@@ -564,15 +674,22 @@
text {*
- @{ML EVERY} @{ML REPEAT} @{ML DETERM}
+ applies
+
+
+ @{ML REPEAT} @{ML DETERM}
+*}
+
+section {* Rewriting and Simplifier Tactics *}
+
+text {*
@{ML rewrite_goals_tac}
- @{ML cut_facts_tac}
@{ML ObjectLogic.full_atomize_tac}
@{ML ObjectLogic.rulify_tac}
- @{ML resolve_tac}
*}
+
section {* Structured Proofs *}
lemma True