
diff -r 14d5f0cf91dc -r 6e0f56764ff8 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sun Apr 26 23:45:22 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Wed Apr 29 00:36:14 2009 +0200
@@ -734,7 +734,7 @@
 
   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
+  implementing a tactic analysing a goal according to its topmost
   connective. These simpler methods use tactic combinators, which we will
   explain in the next section.
 
@@ -808,8 +808,8 @@
 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
 
 text {*
-  will first try out whether rule @{text disjI} applies and after that 
-  @{text conjI}. To see this consider the proof
+  will first try out whether rule @{text disjI} applies and in case of failure 
+  will try @{text conjI}. To see this consider the proof
 *}
 
 lemma shows "True \<and> False" and "Foo \<or> Bar"
@@ -865,8 +865,21 @@
 
 text {*
   Remember that we chose to implement @{ML select_tac'} so that it 
-  always  succeeds. This can be potentially very confusing for the user, 
-  for example,  in cases where the goal is the form
+  always  succeeds by adding @{ML all_tac} at the end of the tactic
+  list. The same can be achieved with the tactic combinator @{ML TRY}.
+  For example:
+*}
+
+ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, 
+                          rtac @{thm notI}, rtac @{thm allI}]*}
+text_raw{*\label{tac:selectprimeprime}*}
+
+text {*
+  This tactic behaves in the same way as @{ML select_tac'}: it tries out
+  one of the given tactics and if none applies leaves the goal state 
+  unchanged. This, however, can be potentially very confusing when visible to 
+  the user, for example,  in cases where the goal is the form
+
 *}
 
 lemma shows "E \<Longrightarrow> F"
@@ -877,7 +890,8 @@
 (*<*)oops(*>*)
 
 text {*
-  In this case no rule applies. The problem for the user is that there is little 
+  In this case no rule applies, but because of @{ML TRY} or the inclusion of @{ML all_tac}
+  the tactics do not fail. The problem with this is that for the user there is little 
   chance to see whether or not progress in the proof has been made. By convention
   therefore, tactics visible to the user should either change something or fail.
   
@@ -928,7 +942,7 @@
   this is not possible).
 
   If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you 
-  need to implement it as
+  can implement it as
 *}
 
 ML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
@@ -936,7 +950,7 @@
 text {*
   since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
 
-  If you look closely at the goal state above, the tactics @{ML repeat_xmp_tac}
+  If you look closely at the goal state above, then you see the tactics @{ML repeat_xmp_tac}
   and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
   that goals 2 and 3 are not analysed. This is because the tactic
   is applied repeatedly only to the first subgoal. To analyse also all
@@ -1116,7 +1130,7 @@
   \end{center}
   \end{isabelle}
 
-  with @{text "constr"} being a term-constructor, like @{const "If"} or @{const "Let"}. 
+  with @{text "constr"} being a constant, like @{const "If"} or @{const "Let"}. 
   Every simpset contains only
   one congruence rule for each term-constructor, which however can be
   overwritten. The user can declare lemmas to be congruence rules using the
@@ -1137,7 +1151,7 @@
   \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 
-  @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in 
+  @{ML_file "HOL/Tools/simpdata.ML"}. The generic splitter is implemented in 
   @{ML_file  "Provers/splitter.ML"}.
   \end{readmore}
 
@@ -1165,25 +1179,24 @@
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
-  val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
+  val {simps, congs, procs, ...} = Simplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
       "  " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm)
   fun name_ctrm (nm, ctrm) =
       "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
 
-  val s = ["Simplification rules:"] @ (map name_thm simps) @
-          ["Congruences rules:"] @ (map name_thm congs) @
-          ["Simproc patterns:"] @ (map name_ctrm procs)
+  val s = ["Simplification rules:"] @ map name_thm simps @
+          ["Congruences rules:"] @ map name_thm congs @
+          ["Simproc patterns:"] @ map name_ctrm procs
 in
-  s |> separate "\n"
-    |> implode
+  s |> cat_lines
     |> writeln
 end*}
 text_raw {* 
 \end{isabelle}
 \end{minipage}
-\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
+\caption{The function @{ML Simplifier.dest_ss} returns a record containing
   all printable information stored in a simpset. We are here only interested in the 
   simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
@@ -1287,7 +1300,8 @@
 
   
   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
+  simplifier implements the tactic @{ML rewrite_goals_tac}.\footnote{FIXME: 
+  see LocalDefs infrastructure.} Suppose for example the
   definition
 *}
 
@@ -1499,7 +1513,7 @@
   you can use the function:
 *}
 
-ML %linenosgray{*fun fail_sp_aux simpset redex = 
+ML %linenosgray{*fun fail_simproc simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
   val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex))
@@ -1517,7 +1531,7 @@
   done by adding the simproc to the current simpset as follows
 *}
 
-simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
+simproc_setup %gray fail ("Suc n") = {* K fail_simproc *}
 
 text {*
   where the second argument specifies the pattern and the right-hand side
@@ -1547,16 +1561,16 @@
   with the declaration
 *}
 
-declare [[simproc del: fail_sp]]
+declare [[simproc del: fail]]
 
 text {*
   If you want to see what happens with just \emph{this} simproc, without any 
-  interference from other rewrite rules, you can call @{text fail_sp} 
+  interference from other rewrite rules, you can call @{text fail} 
   as follows:
 *}
 
 lemma shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail}]) 1*})
 (*<*)oops(*>*)
 
 text {*
@@ -1566,11 +1580,11 @@
   Setting up a simproc using the command \isacommand{simproc\_setup} will
   always add automatically the simproc to the current simpset. If you do not
   want this, then you have to use a slightly different method for setting 
-  up the simproc. First the function @{ML fail_sp_aux} needs to be modified
+  up the simproc. First the function @{ML fail_simproc} needs to be modified
   to
 *}
 
-ML{*fun fail_sp_aux' simpset redex = 
+ML{*fun fail_simproc' simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
   val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
@@ -1586,12 +1600,12 @@
 *}
 
 
-ML{*val fail_sp' = 
+ML{*val fail' = 
 let 
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
 in
-  Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+  Simplifier.simproc_i thy "fail_simproc'" pat (K fail_simproc')
 end*}
 
 text {*
@@ -1606,11 +1620,11 @@
 *}
 
 lemma shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail']) 1*})
 (*<*)oops(*>*)
 
 text {*
-  The simproc @{ML fail_sp'} prints out the sequence 
+  The simproc @{ML fail'} prints out the sequence 
 
 @{text [display]
 "> Suc 0
@@ -1633,7 +1647,7 @@
 *}
 
 
-ML{*fun plus_one_sp_aux ss redex =
+ML{*fun plus_one_simproc ss redex =
   case redex of
     @{term "Suc 0"} => NONE
   | _ => SOME @{thm plus_one}*}
@@ -1642,12 +1656,12 @@
   and set up the simproc as follows.
 *}
 
-ML{*val plus_one_sp =
+ML{*val plus_one =
 let
   val thy = @{theory}
   val pat = [@{term "Suc n"}] 
 in
-  Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+  Simplifier.simproc_i thy "sproc +1" pat (K plus_one_simproc)
 end*}
 
 text {*
@@ -1658,7 +1672,7 @@
 *}
 
 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
 txt{*
   where the simproc produces the goal state
   
@@ -1670,8 +1684,8 @@
 
 text {*
   As usual with rewriting you have to worry about looping: you already have
-  a loop with @{ML plus_one_sp}, if you apply it with the default simpset (because
-  the default simpset contains a rule which just does the opposite of @{ML plus_one_sp},
+  a loop with @{ML plus_one}, if you apply it with the default simpset (because
+  the default simpset contains a rule which just does the opposite of @{ML plus_one},
   namely rewriting @{text [quotes] "+ 1"} to a successor). So you have to be careful 
   in choosing the right simpset to which you add a simproc. 
 
@@ -1735,7 +1749,7 @@
   theorem for the simproc.
 *}
 
-ML{*fun nat_number_sp_aux ss t =
+ML{*fun nat_number_simproc ss t =
 let 
   val ctxt = Simplifier.the_context ss
 in
@@ -1744,18 +1758,18 @@
 end*}
 
 text {*
-  This function uses the fact that @{ML dest_suc_trm} might throw an exception 
+  This function uses the fact that @{ML dest_suc_trm} might raise an exception 
   @{ML TERM}. In this case there is nothing that can be rewritten and therefore no
   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 =
+ML{*val nat_number =
 let
   val thy = @{theory}
   val pat = [@{term "Suc n"}]
 in 
-  Simplifier.simproc_i thy "nat_number" pat (K nat_number_sp_aux) 
+  Simplifier.simproc_i thy "nat_number" pat (K nat_number_simproc) 
 end*}
 
 text {* 
@@ -1763,7 +1777,7 @@
   *}
 
 lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
 txt {* 
   you obtain the more legible goal state
   
@@ -1846,14 +1860,14 @@
   val ten = @{cterm \"10::nat\"}
   val thm = Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
 in
-  #prop (rep_thm thm)
+  Thm.prop_of thm
 end"
 "Const (\"==\",\<dots>) $ 
   (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
     (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
 
   The argument @{ML true} in @{ML Thm.beta_conversion} indicates that 
-  the right-hand side will be fully beta-normalised. If instead 
+  the right-hand side should be fully beta-normalised. If instead 
   @{ML false} is given, then only a single beta-reduction is performed 
   on the outer-most level. For example
 
@@ -1891,7 +1905,7 @@
   Note, however, that the function @{ML Conv.rewr_conv} only rewrites the 
   outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match 
   exactly the 
-  left-hand side of the theorem, then  @{ML Conv.rewr_conv} raises 
+  left-hand side of the theorem, then  @{ML Conv.rewr_conv} fails by raising 
   the exception @{ML CTERM}.
 
   This very primitive way of rewriting can be made more powerful by
@@ -1962,15 +1976,15 @@
   stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
   the conversion to the first argument of an application.
 
-  The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
+  The function @{ML Conv.abs_conv} applies a conversion under an abstraction.
   For example:
 
   @{ML_response_fake [display,gray]
 "let 
-  val conv = K (Conv.rewr_conv @{thm true_conj1}) 
+  val conv = Conv.rewr_conv @{thm true_conj1} 
   val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
 in
-  Conv.abs_conv conv @{context} ctrm
+  Conv.abs_conv (K conv) @{context} ctrm
 end"
   "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
   
@@ -2071,11 +2085,11 @@
   Here is a tactic doing exactly that:
 *}
 
-ML{*fun true1_tac ctxt = CSUBGOAL (fn (goal, i) =>
+ML{*fun true1_tac ctxt =
   CONVERSION 
     (Conv.params_conv ~1 (fn ctxt =>
        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
-          Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i)*}
+          Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt)*}
 
 text {* 
   We call the conversions with the argument @{ML "~1"}. This is to 
@@ -2100,9 +2114,10 @@
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
   the conclusion according to @{ML all_true1_conv}.
 
-  To sum up this section, conversions are not as powerful as the simplifier
-  and simprocs; the advantage of conversions, however, is that you never have
-  to worry about non-termination.
+  To sum up this section, conversions are more general than the simplifier
+  or simprocs, but you have to do more work yourself. Also conversions are
+  often much less efficient than the simplifier. The advantage of conversions, 
+  however, that they provide much less room for non-termination.
 
   \begin{exercise}\label{ex:addconversion}
   Write a tactic that does the same as the simproc in exercise
@@ -2120,7 +2135,7 @@
 
   \begin{readmore}
   See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. 
-  Further conversions are defined in  @{ML_file "Pure/thm.ML"},
+  Some basic conversions are defined in  @{ML_file "Pure/thm.ML"},
   @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
   \end{readmore}
 




