diff -r 7e0bf13bf743 -r 8084c353d196 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Fri Feb 27 13:02:19 2009 +0000
+++ b/CookBook/Tactical.thy	Fri Feb 27 15:59:38 2009 +0000
@@ -1018,11 +1018,89 @@
 section {* Simplifier Tactics *}
 
 text {*
-  @{ML rewrite_goals_tac}
+  A lot of convenience in the reasoning with Isabelle derives from its
+  powerful simplifier. There are the following five main tactics behind 
+  the simplifier (in parentheses is their userlevel counterpart)
+
+  \begin{isabelle}
+  \begin{tabular}{l@ {\hspace{2cm}}l}
+   @{ML simp_tac}            & @{text "(simp (no_asm))"} \\
+   @{ML asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
+   @{ML full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
+   @{ML asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
+   @{ML asm_full_simp_tac}   & @{text "(simp)"}
+  \end{tabular}
+  \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
+*}
+
+lemma "Suc (1 + 2) < 3 + 2"
+apply(simp)
+done
+
+text {*
+  corrsponds on the ML-level to the tactic
+*}
+
+lemma "Suc (1 + 2) < 3 + 2"
+apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
+done
+
+thm imp_cong simp_implies_cong
+
+text {*
+  The crucial information the developer has to control is the simpset
+  to be used by the simplifier. If not handled with care, then the 
+  simplifier can easily run forever. 
+
+  It might be surprising that a simpset is quite more complex than just
+  a simple list of theorems. 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 are meta-equalities 
+  typical of the form
+
+  \begin{isabelle}
+  \mbox{\inferrule{@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>s\<^isub>n"}}{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}}
+  \end{isabelle}
+
+  with @{text "constr"} being a term-constructor. However there are also more complicated 
+  congruence rules. The user can declare lemmas to be congruence rules using the 
+  attribute @{text "[cong]"} (theses lemmas are usually equations that are internally 
+  transformed into meta-equations (FIXME: check that).
   
-  @{ML ObjectLogic.full_atomize_tac}
-  
-  @{ML ObjectLogic.rulify_tac}
+  The rewriting with rules involving preconditions requires solvers. However
+  there are also 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. (FIXME: loopers and subgoalers?)
+
+  The most common combinators to modify simpsets are
+
+  \begin{isabelle}
+  \begin{tabular}{ll}
+  @{ML addsimps} & @{ML delsimps}\\
+  @{ML addcongs} & @{ML delcongs}\\
+  \end{tabular}
+  \end{isabelle}
+
+  The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}.
+*}
+
+text {*
+  (FIXME: what do the simplifier tactics do when nothing can be rewritten)
+
+
+  (FIXME: @{ML rewrite_goals_tac}, @{ML ObjectLogic.full_atomize_tac}, 
+  @{ML ObjectLogic.rulify_tac})
+
+
+  \begin{readmore}
+  For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
+  and @{ML_file "Pure/simplifier.ML"}.
+  \end{readmore}
 
 *}
 
@@ -1632,9 +1710,16 @@
   to worry about non-termination.
 
   \begin{exercise}\label{ex:addconversion}
-  Write a tactic that is based on conversions which does the same as the simproc in
-  exercise \ref{ex:addsimproc}, that is replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} 
-  by their result. You can make the same assumptions as in \ref{ex:addsimproc}.
+  Write a tactic that does the same as the simproc in exercise
+  \ref{ex:addsimproc}, but is based in conversions. That means replace terms
+  of the form @{term "t\<^isub>1 + t\<^isub>2"} by their result. You can make
+  the same assumptions as in \ref{ex:addsimproc}. FIXME: the current solution
+  requires some additional functions.
+  \end{exercise}
+
+  \begin{exercise}
+  Compare which way of rewriting such terms is more efficient. For this
+  you might have to construct quite large terms.
   \end{exercise}
 
   \begin{readmore}
@@ -1648,7 +1733,7 @@
 
 
 
-section {* Structured Proofs *}
+section {* Structured Proofs (TBD) *}
 
 text {* TBD *}