
diff -r 84d1392186d3 -r 253ea99c1441 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Wed Feb 25 22:13:41 2009 +0000
+++ b/CookBook/Tactical.thy	Thu Feb 26 12:16:24 2009 +0000
@@ -311,7 +311,7 @@
   "(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
+  is invisible in the figure). This wrapper 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
@@ -453,7 +453,7 @@
 (*<*)oops(*>*)
 
 text {*
-  where the application of Rule @{text bspec} generates two subgoals involving the
+  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"}
@@ -576,7 +576,7 @@
   \end{tabular}
   \end{quote}
 
-  Note in the actual output the brown colour of the variables @{term x} and 
+  Notice 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, 
@@ -727,12 +727,13 @@
   the first goal. To do this can result in quite messy code. In contrast, 
   the ``reverse application'' is easy to implement.
 
-  (FIXME: mention @{ML "CSUBGOAL"})
+  The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes
+  a @{ML_type cterm} instead of a @{ML_type term}.  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.
 
-  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 *}
@@ -1027,10 +1028,10 @@
 
 text {*
   In Isabelle you can also implement custom simplification procedures, called
-  \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and
-  rewrite a term according to a theorem. They are useful in cases where
-  a rewriting rule must be produced on ``demand'' or when rewriting by
-  simplification is too unpredictable and potentially loops.
+  \emph{simprocs}. Simprocs can be triggered by the simplifier on a specified
+  term-pattern and rewrite a term according to a theorem. They are useful in
+  cases where a rewriting rule must be produced on ``demand'' or when
+  rewriting by simplification is too unpredictable and potentially loops.
 
   To see how simprocs work, let us first write a simproc that just prints out
   the pattern which triggers it and otherwise does nothing. For this
@@ -1052,7 +1053,7 @@
   returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the
   moment we are \emph{not} interested in actually rewriting anything. We want
   that the simproc is triggered by the pattern @{term "Suc n"}. This can be
-  done by adding the simproc to the current simproc as follows
+  done by adding the simproc to the current simpset as follows
 *}
 
 simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
@@ -1114,7 +1115,8 @@
 text {*
   Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
   (therefore we printing it out using the function @{ML string_of_term in Syntax}).
-  We can turn this function into a proper simproc using
+  We can turn this function into a proper simproc using the function 
+  @{ML Simplifier.simproc_i}:
 *}
 
 
@@ -1130,7 +1132,7 @@
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
   The function also takes a list of patterns that can trigger the simproc.
   Now the simproc is set up and can be explicitly added using
-  {ML addsimprocs} to a simpset whenerver
+  @{ML addsimprocs} to a simpset whenerver
   needed. 
 
   Simprocs are applied from inside to outside and from left to right. You can
@@ -1138,7 +1140,7 @@
 *}
 
 lemma shows "Suc (Suc 0) = (Suc 1)"
-  apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
+  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
 (*<*)oops(*>*)
 
 text {*
@@ -1190,7 +1192,7 @@
 *}
 
 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-  apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sp]) 1*})
+  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
 txt{*
   where the simproc produces the goal state
 
@@ -1208,7 +1210,6 @@
   Next let us implement a simproc that replaces terms of the form @{term "Suc n"}
   with the number @{text n} increase by one. First we implement a function that
   takes a term and produces the corresponding integer value.
-
 *}
 
 ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t
@@ -1412,7 +1413,7 @@
 
   @{ML_response_fake [display,gray]
 "let 
-  val ctrm =  @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+  val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
 in
   Conv.rewr_conv @{thm true_conj1} ctrm
 end"
@@ -1439,7 +1440,8 @@
   "(\<lambda>x. x \<and> False) True \<equiv> False"}
 
   where we first beta-reduce the term and then rewrite according to
-  @{thm [source] true_conj1}. 
+  @{thm [source] true_conj1}. (Recall the problem with the pretty-printer
+  normalising all terms.)
 
   The conversion combinator @{ML else_conv} tries out the 
   first one, and if it does not apply, tries the second. For example 
@@ -1459,11 +1461,11 @@
   does not fail, however, because the combinator @{ML else_conv} will then 
   try out @{ML Conv.all_conv}, which always succeeds.
 
-  Apart from the function @{ML beta_conversion in Thm}, which able to fully
-  beta-normalise a term, the restriction of conversions so far is that they
+  Apart from the function @{ML beta_conversion in Thm}, which is able to fully
+  beta-normalise a term, the conversions so far are restricted in that they
   only apply to the outer-most level of a @{ML_type cterm}. In what follows we
   will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
-  the conversion on the first argument of an application, that is the term
+  the conversion to the first argument of an application, that is the term
   must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
   to @{text t2}.  For example
 
@@ -1477,7 +1479,7 @@
 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
 
   The reason for this behaviour is that @{text "(op \<or>)"} expects two
-  arguments.  So the term must be of the form @{text "Const \<dots> $ t1 $ t2"}. The
+  arguments.  So the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
   conversion is then applied to @{text "t2"} which in the example above
   stands for @{term "True \<and> Q"}.
 
@@ -1515,8 +1517,10 @@
 text {*
   This functions descends under applications (Line 6 and 7) and abstractions 
   (Line 8); and ``fires'' if the outer-most constant is an @{text "True \<and> \<dots>"}
-  (Lines 3-5); otherwise it leaves the term unchanged (Line 9). To see this 
-  conversion in action, consider the following example.
+  (Lines 3-5); otherwise it leaves the term unchanged (Line 9). In Line 2
+  we need to transform the @{ML_type cterm} into a @{ML_type term} in order
+  to be able to pattern-match the term. To see this 
+  conversion in action, consider the following example
 
 @{ML_response_fake [display,gray]
 "let
@@ -1527,9 +1531,11 @@
 end"
   "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
 
-  To see how much control you have about rewriting via conversions, let us 
+  where the conversion is applied ``deep'' inside the term.
+
+  To see how much control you have about rewriting by using conversions, let us 
   make the task a bit more complicated by rewriting according to the rule
-  @{text true_conj1}, but only in the first arguments of @{term If}s. The 
+  @{text true_conj1}, but only in the first arguments of @{term If}s. Then 
   the conversion should be as follows.
 *}
 
@@ -1543,7 +1549,7 @@
   | _ => Conv.all_conv ctrm *}
 
 text {*
-  Here is an application of this conversion:
+  Here is an example for this conversion:
 
   @{ML_response_fake [display,gray]
 "let
@@ -1560,7 +1566,7 @@
 text {*
   So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
   also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example, 
-  consider @{ML all_true1_conv} and the lemma:
+  consider the conversion @{ML all_true1_conv} and the lemma:
 *}
 
 lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
@@ -1583,7 +1589,7 @@
   the conclusion of a goal.
 
   Assume we want to apply @{ML all_true1_conv} only in the conclusion
-  of the goal, and @{ML if_true1_conv} should only be applied in the premises.
+  of the goal, and @{ML if_true1_conv} should only be applied to the premises.
   Here is a tactic doing exactly that:
 *}
 
@@ -1611,9 +1617,7 @@
 apply(tactic {* true1_tac 1 *})
 txt {* where the tactic yields the goal state
 
-       \begin{minipage}{\textwidth}
-       @{subgoals [display]} 
-       \end{minipage} *}
+       @{subgoals [display]}*}
 (*<*)oops(*>*)
 
 text {*




