# HG changeset patch
# User wenzelm
# Date 869829489 -7200
# Node ID 9715b6e3ec5f24266333b4d5a5cbab96d36a663e
# Parent  9cd0a0919ba07a76f99cde841d202bbc26304fc1
added prems argument to simplification procedures;

diff -r 9cd0a0919ba0 -r 9715b6e3ec5f src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Jul 25 13:17:14 1997 +0200
+++ b/src/HOL/simpdata.ML	Fri Jul 25 13:18:09 1997 +0200
@@ -170,14 +170,14 @@
                  rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
   in rule_by_tactic tac (trivial ceqt) end;
 
-fun rearrange sg (F as ex $ Abs(x,T,P)) =
+fun rearrange sg _ (F as ex $ Abs(x,T,P)) =
      (case extract P of
         None => None
       | Some(eq,Q) =>
           let val ceqt = cterm_of sg
                        (Logic.mk_equals(F,ex $ Abs(x,T,HOLogic.conj$eq$Q)))
           in Some(prove_eq ceqt) end)
-  | rearrange _ _ = None;
+  | rearrange _ _ _ = None;
 
 val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
 
diff -r 9cd0a0919ba0 -r 9715b6e3ec5f src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Jul 25 13:17:14 1997 +0200
+++ b/src/Provers/simplifier.ML	Fri Jul 25 13:18:09 1997 +0200
@@ -2,7 +2,8 @@
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
-Generic simplifier, suitable for most logics.
+Generic simplifier, suitable for most logics.  See also Pure/thm.ML
+for the actual meta level rewriting engine.
 *)
 
 infix 4
@@ -14,7 +15,8 @@
 signature SIMPLIFIER =
 sig
   type simproc
-  val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc
+  val mk_simproc: string -> cterm list
+    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
   val conv_prover: (term * term -> term) -> thm -> (thm -> thm)
     -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm
   type simpset
@@ -33,17 +35,17 @@
   val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
   val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
   val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
-  val setmksimps:  simpset * (thm -> thm list) -> simpset
-  val settermless: simpset * (term * term -> bool) -> simpset
-  val addsimps:    simpset * thm list -> simpset
-  val delsimps:    simpset * thm list -> simpset
-  val addeqcongs:  simpset * thm list -> simpset
-  val deleqcongs:  simpset * thm list -> simpset
-  val addsimprocs: simpset * simproc list -> simpset
-  val delsimprocs: simpset * simproc list -> simpset
-  val merge_ss:    simpset * simpset -> simpset
-  val prems_of_ss: simpset -> thm list
-  val simpset:     simpset ref
+  val setmksimps:   simpset * (thm -> thm list) -> simpset
+  val settermless:  simpset * (term * term -> bool) -> simpset
+  val addsimps:     simpset * thm list -> simpset
+  val delsimps:     simpset * thm list -> simpset
+  val addeqcongs:   simpset * thm list -> simpset
+  val deleqcongs:   simpset * thm list -> simpset
+  val addsimprocs:  simpset * simproc list -> simpset
+  val delsimprocs:  simpset * simproc list -> simpset
+  val merge_ss:     simpset * simpset -> simpset
+  val prems_of_ss:  simpset -> thm list
+  val simpset:      simpset ref
   val Addsimps: thm list -> unit
   val Delsimps: thm list -> unit
   val Addsimprocs: simproc list -> unit
@@ -73,7 +75,7 @@
 (* datatype simproc *)
 
 datatype simproc =
-  Simproc of string * cterm list * (Sign.sg -> term -> thm option) * stamp;
+  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
 
 fun mk_simproc name lhss proc =
   Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
diff -r 9cd0a0919ba0 -r 9715b6e3ec5f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jul 25 13:17:14 1997 +0200
+++ b/src/Pure/thm.ML	Fri Jul 25 13:18:09 1997 +0200
@@ -152,9 +152,11 @@
   val add_congs         : meta_simpset * thm list -> meta_simpset
   val del_congs         : meta_simpset * thm list -> meta_simpset
   val add_simprocs	: meta_simpset *
-    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
+    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
+      -> meta_simpset
   val del_simprocs	: meta_simpset *
-    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
+    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
+      -> meta_simpset
   val add_prems         : meta_simpset * thm list -> meta_simpset
   val prems_of_mss      : meta_simpset -> thm list
   val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
@@ -1449,7 +1451,8 @@
 
 type rrule = {thm: thm, lhs: term, perm: bool};
 type cong = {thm: thm, lhs: term};
-type simproc = {name: string, proc: Sign.sg -> term -> thm option, lhs: cterm, id: stamp};
+type simproc =
+ {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
 
 fun eq_rrule ({thm = Thm {prop = p1, ...}, ...}: rrule,
   {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2;
@@ -1761,7 +1764,7 @@
     (4) simplification procedures
 *)
 
-fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) 
+fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
              (shypst,hypst,maxt,t,ders) =
   let
       val tsigt = #tsig(Sign.rep_sg signt);
@@ -1821,7 +1824,7 @@
         | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
             if Pattern.matches tsigt (plhs, t) then
              (trace_term ("Trying procedure " ^ name ^ " on:") signt eta_t;
-              case proc signt eta_t of
+              case proc signt prems eta_t of
                 None => (trace "FAILED"; proc_rews eta_t ps)
               | Some raw_thm =>
                  (trace_thm ("Procedure " ^ name ^ " proved rewrite rule:") raw_thm;