--- 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)
--- 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 ());
--- 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;