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