# HG changeset patch
# User oheimb
# Date 854722440 -3600
# Node ID 7a28e02e10b7014ecb9c2bc7fdf282b2ac3122ae
# Parent  cbf02fc743320c9e26492606770bc190cfdcb690
added addloop (and also documentation of addsolver

diff -r cbf02fc74332 -r 7a28e02e10b7 doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Fri Jan 31 13:57:33 1997 +0100
+++ b/doc-src/Ref/simplifier.tex	Fri Jan 31 15:54:00 1997 +0100
@@ -268,7 +268,8 @@
 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
@@ -312,47 +313,69 @@
 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{*simp_tac}
-\index{*asm_simp_tac}
-\index{*asm_full_simp_tac}
-\index{*addeqcongs}
+\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{*empty_ss}
+\index{*addeqcongs}
 \index{*merge_ss}
-\index{*setsubgoaler}
-\index{*setsolver}
-\index{*setloop}
-\index{*setmksimps}
-\index{*prems_of_ss}
-\index{*rep_ss}
+\index{*simpset}
+\index{*Addsimps}
+\index{*Delsimps}
+\index{*simp_tac}
+\index{*asm_simp_tac}
+\index{*full_simp_tac}
+\index{*asm_full_simp_tac}
+\index{*Simp_tac}
+\index{*Asm_simp_tac}
+\index{*Full_simp_tac}
+\index{*Asm_full_simp_tac}
+
 \begin{ttbox}
-infix addsimps addeqcongs delsimps
-      setsubgoaler setsolver setloop setmksimps;
+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}
diff -r cbf02fc74332 -r 7a28e02e10b7 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Jan 31 13:57:33 1997 +0100
+++ b/src/Provers/simplifier.ML	Fri Jan 31 15:54:00 1997 +0100
@@ -11,8 +11,11 @@
   - improve merge
 *)
 
-infix 4 addsimps addeqcongs addsimprocs delsimprocs addsolver delsimps
-  setsolver setloop setmksimps settermless setsubgoaler;
+infix 4 setloop addloop setsolver addsolver 
+        setsubgoaler setmksimps
+	addsimps addeqcongs delsimps 
+	settermless addsimprocs delsimprocs;
+
 
 signature SIMPLIFIER =
 sig
@@ -26,6 +29,7 @@
   val rep_ss: simpset -> {simps: thm list, procs: string 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
@@ -135,11 +139,16 @@
     setloop loop_tac =
   make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, DETERM o loop_tac);
 
+fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac})
+    addloop tac =
+  make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, 
+    loop_tac ORELSE' (DETERM o tac));
+
 fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac = _, loop_tac})
     setsolver finish_tac =
   make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac);
 
-fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, finish_tac})
+fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac})
     addsolver tac =
   make_ss (mss, simps, procs, congs, subgoal_tac,
     fn hyps => finish_tac hyps ORELSE' tac hyps, loop_tac);