--- a/CookBook/Tactical.thy Fri Mar 06 16:12:16 2009 +0000
+++ b/CookBook/Tactical.thy Fri Mar 06 21:52:17 2009 +0000
@@ -2,7 +2,6 @@
imports Base FirstSteps
begin
-
chapter {* Tactical Reasoning\label{chp:tactical} *}
text {*
@@ -66,7 +65,7 @@
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.
+ Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual.
\end{readmore}
Note that in the code above we use antiquotations for referencing the theorems. Many theorems
@@ -1011,14 +1010,14 @@
text {*
A lot of convenience in the reasoning with Isabelle derives from its
- powerful simplifier. The power of simplifier is at the same time a
- strength and a weakness, because you can easily make the simplifier to
- loop and its behaviour can sometimes be difficult to predict. There is also
- a multitude of options that configurate the behaviour of the simplifier. We
- describe some of them in this and the next section.
+ powerful simplifier. The power of simplifier is a strength and a weakness at
+ the same time, because you can easily make the simplifier to run into a loop and its
+ behaviour can be difficult to predict. There is also a multitude
+ of options that you can configurate to control the behaviour of the simplifier.
+ We describe some of them in this and the next section.
There are the following five main tactics behind
- the simplifier (in parentheses is their user-level counterparts):
+ the simplifier (in parentheses is their user-level counterpart):
\begin{isabelle}
\begin{center}
@@ -1032,8 +1031,8 @@
\end{center}
\end{isabelle}
- All of them take a simpset and an interger as argument (the latter to specify the goal
- to be analysed). So the proof
+ All of the tactics take a simpset and an interger as argument (the latter as usual
+ to specify the goal to be analysed). So the proof
*}
lemma "Suc (1 + 2) < 3 + 2"
@@ -1049,18 +1048,19 @@
done
text {*
- If the simplifier cannot make any progress, then it leaves the goal unchanged
- and does not raise any error message. That means if you use it to unfold a definition
- for a constant and this constant is not present in a goal state, you can still
- safely apply the simplifier.
+ If the simplifier cannot make any progress, then it leaves the goal unchanged,
+ i.e.~does not raise any error message. That means if you use it to unfold a
+ definition for a constant and this constant is not present in the goal state,
+ you can still safely apply the simplifier.
- When using the simplifier, the crucial information you have to control is
- the simpset. If not handled with care, then the simplifier can easily run
- into a loop. It might be surprising that a simpset is more complex than just a
- simple collection of theorems used as simplification rules. One reason for
- the complexity is that the simplifier must be able to rewrite inside terms
- and should also be able to rewrite according to rules that have
- precoditions.
+ When using the simplifier, the crucial information you have to provide is
+ the simpset. If this information is not handled with care, then the
+ simplifier can easily run into a loop. Therefore a good rule of thumb is to
+ use simpsets that are as minimal as possible. It might be surprising that a
+ simpset is more complex than just a simple collection of theorems used as
+ simplification rules. One reason for the complexity is that the simplifier
+ must be able to rewrite inside terms and should also be able to rewrite
+ according to rules that have precoditions.
The rewriting inside terms requires congruence rules, which
@@ -1068,12 +1068,13 @@
\begin{isabelle}
\begin{center}
- \mbox{\inferrule{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}
+ \mbox{\inferrule{@{text "t\<^isub>1 \<equiv> s\<^isub>1 \<dots> t\<^isub>n \<equiv> s\<^isub>n"}}
{@{text "constr t\<^isub>1\<dots>t\<^isub>n \<equiv> constr s\<^isub>1\<dots>s\<^isub>n"}}}
\end{center}
\end{isabelle}
- with @{text "constr"} being a term-constructor. Every simpset contains only
+ with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}.
+ Every simpset contains only
one concruence rule for each term-constructor, which however can be
overwritten. The user can declare lemmas to be congruence rules using the
attribute @{text "[cong]"}. In HOL, the user usually states these lemmas as
@@ -1082,12 +1083,14 @@
The rewriting with rules involving preconditions requires what is in
Isabelle called a subgoaler, a solver and a looper. These can be arbitrary
- tactics that can be installed in a simpset. However, simpsets also include
+ tactics that can be installed in a simpset and which are called during
+ various stages during simplification. However, simpsets also include
simprocs, which can produce rewrite rules on demand (see next
section). Another component are split-rules, which can simplify for example
the ``then'' and ``else'' branches of if-statements under the corresponding
precoditions.
+
\begin{readmore}
For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
@@ -1162,7 +1165,7 @@
text {*
To see how they work, consider the two functions in Figure~\ref{fig:prettyss}, which
print out some parts of a simpset. If you use them to print out the components of the
- empty simpset, the most primitive simpset
+ empty simpset, in ML @{ML empty_ss} and the most primitive simpset
@{ML_response_fake [display,gray]
"print_parts @{context} empty_ss"
@@ -1177,7 +1180,7 @@
ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
text {*
- Printing out the components of this simpset gives:
+ Printing then out the components of the simpset gives:
@{ML_response_fake [display,gray]
"print_parts @{context} ss1"
@@ -1187,7 +1190,7 @@
(FIXME: Why does it print out ??.unknown)
- Adding the congruence rule @{thm [source] UN_cong}
+ Adding also the congruence rule @{thm [source] UN_cong}
*}
ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
@@ -1204,9 +1207,9 @@
Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
expects this form of the simplification and congruence rules. However, even
- adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
+ when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
- In the context of HOL the first useful simpset is @{ML HOL_basic_ss}. While
+ In the context of HOL, the first really useful simpset is @{ML HOL_basic_ss}. While
printing out the components of this simpset
@{ML_response_fake [display,gray]
@@ -1215,9 +1218,9 @@
Congruences rules:"}
also produces ``nothing'', the printout is misleading. In fact
- the simpset @{ML HOL_basic_ss} is setup so that it can be used to solve goals of the
- form @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]},
- and resolve with assumptions.
+ the @{ML HOL_basic_ss} is setup so that it can solve goals of the
+ form @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]};
+ and also resolve with assumptions. For example:
*}
lemma
@@ -1226,11 +1229,14 @@
done
text {*
- This is because how the tactics for the subgoaler, solver and looper are set
- up.
+ This behaviour is not because of simplification rules, but how the subgoaler, solver
+ and looper are set up. @{ML HOL_basic_ss} is usually a good start to build your
+ own simpsets, because of the low danger of causing loops via interacting simplifiction
+ rules.
- The simpset @{ML HOL_ss}, which is an extention of @{ML HOL_basic_ss}, contains
- already many useful simplification rules for the logical connectives in HOL.
+ The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing
+ already many useful simplification and congruence rules for the logical
+ connectives in HOL.
@{ML_response_fake [display,gray]
"print_parts @{context} HOL_ss"
@@ -1245,9 +1251,25 @@
op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'"}
- The main point of these simpsets is that they are small enough to
- not cause any loops with most of the simplification rules that
- you might like to add.
+ The simplifier is often used to unfold definitions in a proof. For this the
+ simplifier contains the @{ML rewrite_goals_tac}. Suppose for example the
+ definition
+*}
+
+definition "MyTrue \<equiv> True"
+
+lemma shows "MyTrue \<Longrightarrow> True \<and> True"
+apply(rule conjI)
+apply(tactic {* rewrite_goals_tac [@{thm MyTrue_def}] *})
+txt{* then the tactic produces the goal state
+
+ \begin{minipage}{\textwidth}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
+
+text {*
+ As you can see, the tactic unfolds the definitions in all subgoals.
*}
@@ -1259,9 +1281,8 @@
primrec (perm_nat)
"[]\<bullet>c = c"
- "(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab
- then snd ab
- else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))"
+ "(ab#pi)\<bullet>c = (if (pi\<bullet>c)=fst ab then snd ab
+ else (if (pi\<bullet>c)=snd ab then fst ab else (pi\<bullet>c)))"
primrec (perm_prod)
"pi\<bullet>(x, y) = (pi\<bullet>x, pi\<bullet>y)"
@@ -1300,17 +1321,18 @@
text {*
- Often the situation arises that simplification rules will cause the
- simplifier to run into an infinite loop. Consider for example the simple
- theory about permutations shown in Figure~\ref{fig:perms}. The purpose of
- the lemmas is to pus permutations as far inside a term where they might
- disappear using the lemma @{thm [source] perm_rev}. However, to fully
- simplifiy all instances, it would be desirable to add also the lemma @{thm
- [source] perm_compose} to the simplifier in order to push permutations over
- other permutations. Unfortunately, the right-hand side of this lemma is
- again an instance of the left-hand side and so causes an infinite
- loop. On the user-level it is difficult to work around such situations
- and we end up with clunky proofs such as:
+ The simplifier is often used in order to bring terms into a normal form.
+ Unfortunately, often the situation arises that the corresponding
+ simplification rules will cause the simplifier to run into an infinite
+ loop. Consider for example the simple theory about permutations over natural
+ numbers shown in Figure~\ref{fig:perms}. The purpose of the lemmas is to
+ push permutations as far inside as possible, where they might disappear by
+ Lemma @{thm [source] perm_rev}. However, to fully normalise all instances,
+ it would be desirable to add also the lemma @{thm [source] perm_compose} to
+ the simplifier for pushing permutations over other permutations. Unfortunately,
+ the right-hand side of this lemma is again an instance of the left-hand side
+ and so causes an infinite loop. The seems to be no easy way to reformulate
+ this rule and so one ends up with clunky proofs like:
*}
lemma
@@ -1323,9 +1345,10 @@
done
text {*
- On the ML-level, we can however generate a single simplifier tactic that solves
+ It is however possible to create a single simplifier tactic that solves
such proofs. The trick is to introduce an auxiliary constant for permutations
- and split the simplification into two phases. Let us say the auxiliary constant is
+ and split the simplification into two phases (below actually three). Let
+ assume the auxiliary constant is
*}
definition
@@ -1333,7 +1356,7 @@
where
"pi \<bullet>aux c \<equiv> pi \<bullet> c"
-text {* Now the lemmas *}
+text {* Now the two lemmas *}
lemma perm_aux_expand:
fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
@@ -1349,7 +1372,15 @@
are simple consequence of the definition and @{thm [source] perm_compose}.
More importantly, the lemma @{thm [source] perm_compose_aux} can be safely
added to the simplifier, because now the right-hand side is not anymore an instance
- of the left-hand side. So you can write
+ of the left-hand side. In a sense it freezes all redexes of permutation compositions
+ after one step. In this way, we can split simplification of permutations
+ into three phases without the user not noticing anything about the auxiliary
+ contant. We first freeze any instance of permutation compositions in the term using
+ lemma @{thm [source] "perm_aux_expand"} (Line 9);
+ then simplifiy all other permutations including pusing permutations over
+ other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
+ finally ``unfreeze'' all instances of permutation compositions by unfolding
+ the definition of the auxiliary constant.
*}
ML %linenosgray{*val perm_simp_tac =
@@ -1366,7 +1397,9 @@
end*}
text {*
- This trick is not noticable for the user.
+ For all three phases we have to build simpsets addig specific lemmas. As is sufficient
+ for our purposes here, we can add these lemma to @{ML HOL_basic_ss} in order to obtain
+ the desired results. Now we can solve the following lemma
*}
lemma
@@ -1377,6 +1410,12 @@
text {*
+ in one step. This tactic can deal with most instances of normalising permutations;
+ in order to solve all cases we have to deal with corner-cases such as the
+ lemma being an exact instance of the permutation composition lemma. This can
+ often be done easier by implementing a simproc or a conversion. Both will be
+ explained in the next two chapters.
+
(FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
(FIXME: Unfortunately one cannot access any simproc, as there is
@@ -1387,7 +1426,7 @@
(FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
- (FIXME: @{ML rewrite_goals_tac}, @{ML ObjectLogic.full_atomize_tac},
+ (FIXME: @{ML ObjectLogic.full_atomize_tac},
@{ML ObjectLogic.rulify_tac})
*}