doc-src/Ref/simplifier.tex

 \subsection{*The solver}\label{sec:simp-solver}
 The solver is a tactic that attempts to solve a subgoal after
 simplification.  Typically it just proves trivial subgoals such as {\tt
   True} and $t=t$.  It could use sophisticated means such as {\tt
   fast_tac}, though that could make simplification expensive.  The solver
-is set using \ttindex{setsolver}.
+is set using \ttindex{setsolver}. Additional solvers, which are tried after
+the already set solver, may be added with \ttindex{addsolver}.
 
 Rewriting does not instantiate unknowns.  For example, rewriting cannot
 prove $a\in \Var{A}$ since this requires instantiating~$\Var{A}$.  The
 solver, however, is an arbitrary tactic and may instantiate unknowns as it
 pleases.  This is the only way the simplifier can handle a conditional

 simplification process is started all over again.  Each of the subgoals
 generated by the looper is attacked in turn, in reverse order.  A
 typical looper is case splitting: the expansion of a conditional.  Another
 possibility is to apply an elimination rule on the assumptions.  More
 adventurous loopers could start an induction.  The looper is set with 
-\ttindex{setloop}.
+\ttindex{setloop}. Additional loopers, which are tried after the already set
+looper, may be added with \ttindex{addloop}.
 
 
 \begin{figure}
 \index{*simpset ML type}
+\index{*empty_ss}
+\index{*rep_ss}
+\index{*prems_of_ss}
+\index{*setloop}
+\index{*addloop}
+\index{*setsolver}
+\index{*addsolver}
+\index{*setsubgoaler}
+\index{*setmksimps}
+\index{*addsimps}
+\index{*delsimps}
+\index{*addeqcongs}
+\index{*merge_ss}
+\index{*simpset}
+\index{*Addsimps}
+\index{*Delsimps}
 \index{*simp_tac}
 \index{*asm_simp_tac}
+\index{*full_simp_tac}
 \index{*asm_full_simp_tac}
-\index{*addeqcongs}
-\index{*addsimps}
-\index{*delsimps}
-\index{*empty_ss}
-\index{*merge_ss}
-\index{*setsubgoaler}
-\index{*setsolver}
-\index{*setloop}
-\index{*setmksimps}
-\index{*prems_of_ss}
-\index{*rep_ss}
-\begin{ttbox}
-infix addsimps addeqcongs delsimps
-      setsubgoaler setsolver setloop setmksimps;
+\index{*Simp_tac}
+\index{*Asm_simp_tac}
+\index{*Full_simp_tac}
+\index{*Asm_full_simp_tac}
+
+\begin{ttbox}
+infix 4 setloop addloop setsolver addsolver 
+        setsubgoaler setmksimps
+        addsimps addeqcongs delsimps;
 
 signature SIMPLIFIER =
 sig
   type simpset
-  val simp_tac:          simpset -> int -> tactic
-  val asm_simp_tac:      simpset -> int -> tactic
-  val full_simp_tac:     simpset -> int -> tactic
-  val asm_full_simp_tac: simpset -> int -> tactic\smallskip
-  val addeqcongs:   simpset * thm list -> simpset
-  val addsimps:     simpset * thm list -> simpset
-  val delsimps:     simpset * thm list -> simpset
-  val empty_ss:     simpset
-  val merge_ss:     simpset * simpset -> simpset
+  val empty_ss: simpset
+  val rep_ss: simpset -> {simps: thm list, congs: thm list}
+  val prems_of_ss: simpset -> thm list
+  val setloop: simpset * (int -> tactic) -> simpset
+  val addloop: simpset * (int -> tactic) -> simpset
+  val setsolver: simpset * (thm list -> int -> tactic) -> simpset
+  val addsolver: simpset * (thm list -> int -> tactic) -> simpset
   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
-  val setsolver:    simpset * (thm list -> int -> tactic) -> simpset
-  val setloop:      simpset * (int -> tactic) -> simpset
-  val setmksimps:   simpset * (thm -> thm list) -> simpset
-  val prems_of_ss:  simpset -> thm list
-  val rep_ss:       simpset -> \{simps: thm list, congs: thm list\}
+  val setmksimps: simpset * (thm -> thm list) -> simpset
+  val addsimps: simpset * thm list -> simpset
+  val delsimps: simpset * thm list -> simpset
+  val addeqcongs: simpset * thm list -> simpset
+  val merge_ss: simpset * simpset -> simpset
+  val simpset: simpset ref
+  val Addsimps: thm list -> unit
+  val Delsimps: thm list -> unit
+  val          simp_tac: simpset -> int -> tactic
+  val      asm_simp_tac: simpset -> int -> tactic
+  val     full_simp_tac: simpset -> int -> tactic
+  val asm_full_simp_tac: simpset -> int -> tactic
+  val          Simp_tac: int -> tactic
+  val      Asm_simp_tac: int -> tactic
+  val     Full_simp_tac: int -> tactic
+  val Asm_full_simp_tac: int -> tactic
 end;
 \end{ttbox}
 \caption{The simplifier primitives} \label{SIMPLIFIER}
 \end{figure}