
diff -r a21d7b300616 -r 8db9195bb3e9 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Sun Feb 22 13:37:47 2009 +0000
+++ b/CookBook/Tactical.thy	Mon Feb 23 00:27:27 2009 +0000
@@ -798,7 +798,7 @@
 
 *}
 
-ML{*val orelse_xmp = (rtac @{thm disjI1} ORELSE' rtac @{thm conjI})*}
+ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
 
 text {*
   will first try out whether rule @{text disjI} applies and after that 
@@ -1059,13 +1059,13 @@
 text {*
   where the second argument specifies the pattern and the right-hand side
   contains the code of the simproc (we have to use @{ML K} since we ignoring
-  an argument about a morphism\footnote{FIXME: what does the morphism do?}). 
+  an argument about morphisms\footnote{FIXME: what does the morphism do?}). 
   After this, the simplifier is aware of the simproc and you can test whether 
-  it fires on the lemma
+  it fires on the lemma:
 *}
 
 lemma shows "Suc 0 = 1"
-apply(simp)
+  apply(simp)
 (*<*)oops(*>*)
 
 text {*
@@ -1074,8 +1074,9 @@
   simplifier will at some point reduce the term @{term "1::nat"} to @{term "Suc
   0"}, and then the simproc ``fires'' also on that term. 
 
-  We can add or delete the simproc by the usual \isacommand{declare}-statement. 
-  For example the simproc will be deleted if you type:
+  We can add or delete the simproc from the current simpset by the usual 
+  \isacommand{declare}-statement. For example the simproc will be deleted 
+  if you type:
 *}
 
 declare [[simproc del: fail_sp]]
@@ -1087,13 +1088,14 @@
 *}
 
 lemma shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
+  apply(tactic {* simp_tac (HOL_ss addsimprocs [@{simproc fail_sp}]) 1*})
 (*<*)oops(*>*)
 
 text {*
   (FIXME: should one use HOL-basic-ss or HOL-ss?)
 
-  Now the message shows up only once since @{term "1::nat"} is left unchanged. 
+  Now the message shows up only once since the term @{term "1::nat"} is 
+  left unchanged. 
 
   Setting up a simproc using the command \isacommand{setup\_simproc} will
   always add automatically the simproc to the current simpset. If you do not
@@ -1133,18 +1135,18 @@
 *}
 
 lemma shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
+  apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*})
 (*<*)oops(*>*)
 
 text {*
-  since the @{ML fail_sp'}-simproc prints out the sequence 
+  since @{ML fail_sp'} prints out the sequence 
 
 @{text [display]
 "> Suc 0
 > Suc (Suc 0) 
 > Suc 1"}
 
-  To see how a simproc applies a theorem  let us implement a simproc that
+  To see how a simproc applies a theorem,  let us implement a simproc that
   rewrites terms according to the equation:
 *}
 
@@ -1153,12 +1155,13 @@
 
 text {*
   Simprocs expect that the given equation is a meta-equation, however the
-  equation can contain preconditions (the simproc then will only fire if the 
-  preconditions can be solved). To see how rewriting can be tuned precisely, let us 
-  further assume we want that the simproc only rewrites terms greater than 
-  @{term "Suc 0"}. For this we can write
+  equation can contain preconditions (the simproc then will only fire if the
+  preconditions can be solved). To see one has relatively precise control over
+  the rewriting with simprocs, let us further assume we want that the simproc
+  only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write 
 *}
 
+
 ML{*fun plus_one_sp_aux ss redex =
   case redex of
     @{term "Suc 0"} => NONE
@@ -1177,23 +1180,23 @@
   end*}
 
 text {*
-  Now the have set up the simproc so that it is triggered by terms
+  Now the simproc is set up xso that it is triggered by terms
   of the form @{term "Suc n"}, but inside the simproc we only produce
   a theorem if the term is not @{term "Suc 0"}. The result you can see
-  in the following proof.
+  in the following proof
 *}
 
 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_ss addsimprocs [plus_one_sp]) 1*})
 txt{*
-  the simproc produces the goal state
+  where the simproc produces the goal state
 
   @{subgoals[display]}
 *}  
 (*<*)oops(*>*)
 
 text {*
-  As usual with simplification you have to be careful with loops: you already have
+  As usual with simplification you have to be careful with looping: you already have
   one @{ML plus_one_sp}, if you apply if with the default simpset (because
   the default simpset contains a rule which just undoes the rewriting 
   @{ML plus_one_sp}).
@@ -1210,9 +1213,9 @@
 text {* 
   It uses the library function @{ML dest_number in HOLogic} that transforms
   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
-  on, into integer values. This function raises the exception @{ML TERM} if
+  on, into integer values. This function raises the exception @{ML TERM}, if
   the term is not a number. The next function expects a pair consisting of a term
-  @{text t} and the corresponding integer value @{text n}. 
+  @{text t} (containing @{term Suc}s) and the corresponding integer value @{text n}. 
 *}
 
 ML %linenosgray{*fun get_thm ctxt (t, n) =
@@ -1224,10 +1227,12 @@
 end*}
 
 text {*
-  From the integer value it generates the corresponding Isabelle term, called 
-  @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4)
+  (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
+
+  From the integer value it generates the corresponding number term, called 
+  @{text num} (Line 3), and then generates the equation @{text "t = num"} (Line 4),
   which it proves by simplification in Line 6. The function @{ML mk_meta_eq} 
-  at the outside of the proof just transforms the equality to a meta-equality.
+  at the outside of the proof just transforms the equality into a meta-equality.
 
   Both functions can be stringed together in the function that produces the 
   actual theorem for the simproc.
@@ -1242,12 +1247,10 @@
 end*}
 
 text {*
-  (FIXME: is @{text "@{simpset}"} kosher here? Otherwise the following will loop.)
-
   This function uses the fact that @{ML dest_suc_trm} might throw an exception 
   @{ML TERM}. In this case there is nothing that can be rewritten and therefore no
-  theorem is produced. To try out the simproc on an example, you can set it up as 
-  follows:
+  theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc 
+  on an example, you can set it up as follows:
 *}
 
 ML{*val nat_number_sp =




