
diff -r 83f36a1c62f2 -r 3fb9f820a294 CookBook/Tactical.thy
--- 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})
 
 *}




