added prems argument to simplification procedures;
authorwenzelm
Fri Jul 25 13:18:09 1997 +0200 (1997-07-25)
changeset 35779715b6e3ec5f
parent 3576 9cd0a0919ba0
child 3578 b2b9a9ddb9cc
added prems argument to simplification procedures;
src/HOL/simpdata.ML
src/Provers/simplifier.ML
src/Pure/thm.ML
     1.1 --- a/src/HOL/simpdata.ML	Fri Jul 25 13:17:14 1997 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Fri Jul 25 13:18:09 1997 +0200
     1.3 @@ -170,14 +170,14 @@
     1.4                   rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)])
     1.5    in rule_by_tactic tac (trivial ceqt) end;
     1.6  
     1.7 -fun rearrange sg (F as ex $ Abs(x,T,P)) =
     1.8 +fun rearrange sg _ (F as ex $ Abs(x,T,P)) =
     1.9       (case extract P of
    1.10          None => None
    1.11        | Some(eq,Q) =>
    1.12            let val ceqt = cterm_of sg
    1.13                         (Logic.mk_equals(F,ex $ Abs(x,T,HOLogic.conj$eq$Q)))
    1.14            in Some(prove_eq ceqt) end)
    1.15 -  | rearrange _ _ = None;
    1.16 +  | rearrange _ _ _ = None;
    1.17  
    1.18  val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
    1.19  
     2.1 --- a/src/Provers/simplifier.ML	Fri Jul 25 13:17:14 1997 +0200
     2.2 +++ b/src/Provers/simplifier.ML	Fri Jul 25 13:18:09 1997 +0200
     2.3 @@ -2,7 +2,8 @@
     2.4      ID:         $Id$
     2.5      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     2.6  
     2.7 -Generic simplifier, suitable for most logics.
     2.8 +Generic simplifier, suitable for most logics.  See also Pure/thm.ML
     2.9 +for the actual meta level rewriting engine.
    2.10  *)
    2.11  
    2.12  infix 4
    2.13 @@ -14,7 +15,8 @@
    2.14  signature SIMPLIFIER =
    2.15  sig
    2.16    type simproc
    2.17 -  val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc
    2.18 +  val mk_simproc: string -> cterm list
    2.19 +    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    2.20    val conv_prover: (term * term -> term) -> thm -> (thm -> thm)
    2.21      -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm
    2.22    type simpset
    2.23 @@ -33,17 +35,17 @@
    2.24    val addSSolver:   simpset * (thm list -> int -> tactic) -> simpset
    2.25    val setSolver:    simpset * (thm list -> int -> tactic) -> simpset
    2.26    val addSolver:    simpset * (thm list -> int -> tactic) -> simpset
    2.27 -  val setmksimps:  simpset * (thm -> thm list) -> simpset
    2.28 -  val settermless: simpset * (term * term -> bool) -> simpset
    2.29 -  val addsimps:    simpset * thm list -> simpset
    2.30 -  val delsimps:    simpset * thm list -> simpset
    2.31 -  val addeqcongs:  simpset * thm list -> simpset
    2.32 -  val deleqcongs:  simpset * thm list -> simpset
    2.33 -  val addsimprocs: simpset * simproc list -> simpset
    2.34 -  val delsimprocs: simpset * simproc list -> simpset
    2.35 -  val merge_ss:    simpset * simpset -> simpset
    2.36 -  val prems_of_ss: simpset -> thm list
    2.37 -  val simpset:     simpset ref
    2.38 +  val setmksimps:   simpset * (thm -> thm list) -> simpset
    2.39 +  val settermless:  simpset * (term * term -> bool) -> simpset
    2.40 +  val addsimps:     simpset * thm list -> simpset
    2.41 +  val delsimps:     simpset * thm list -> simpset
    2.42 +  val addeqcongs:   simpset * thm list -> simpset
    2.43 +  val deleqcongs:   simpset * thm list -> simpset
    2.44 +  val addsimprocs:  simpset * simproc list -> simpset
    2.45 +  val delsimprocs:  simpset * simproc list -> simpset
    2.46 +  val merge_ss:     simpset * simpset -> simpset
    2.47 +  val prems_of_ss:  simpset -> thm list
    2.48 +  val simpset:      simpset ref
    2.49    val Addsimps: thm list -> unit
    2.50    val Delsimps: thm list -> unit
    2.51    val Addsimprocs: simproc list -> unit
    2.52 @@ -73,7 +75,7 @@
    2.53  (* datatype simproc *)
    2.54  
    2.55  datatype simproc =
    2.56 -  Simproc of string * cterm list * (Sign.sg -> term -> thm option) * stamp;
    2.57 +  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
    2.58  
    2.59  fun mk_simproc name lhss proc =
    2.60    Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
     3.1 --- a/src/Pure/thm.ML	Fri Jul 25 13:17:14 1997 +0200
     3.2 +++ b/src/Pure/thm.ML	Fri Jul 25 13:18:09 1997 +0200
     3.3 @@ -152,9 +152,11 @@
     3.4    val add_congs         : meta_simpset * thm list -> meta_simpset
     3.5    val del_congs         : meta_simpset * thm list -> meta_simpset
     3.6    val add_simprocs	: meta_simpset *
     3.7 -    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
     3.8 +    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
     3.9 +      -> meta_simpset
    3.10    val del_simprocs	: meta_simpset *
    3.11 -    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
    3.12 +    (string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp) list
    3.13 +      -> meta_simpset
    3.14    val add_prems         : meta_simpset * thm list -> meta_simpset
    3.15    val prems_of_mss      : meta_simpset -> thm list
    3.16    val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
    3.17 @@ -1449,7 +1451,8 @@
    3.18  
    3.19  type rrule = {thm: thm, lhs: term, perm: bool};
    3.20  type cong = {thm: thm, lhs: term};
    3.21 -type simproc = {name: string, proc: Sign.sg -> term -> thm option, lhs: cterm, id: stamp};
    3.22 +type simproc =
    3.23 + {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
    3.24  
    3.25  fun eq_rrule ({thm = Thm {prop = p1, ...}, ...}: rrule,
    3.26    {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2;
    3.27 @@ -1761,7 +1764,7 @@
    3.28      (4) simplification procedures
    3.29  *)
    3.30  
    3.31 -fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) 
    3.32 +fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, prems, ...}) 
    3.33               (shypst,hypst,maxt,t,ders) =
    3.34    let
    3.35        val tsigt = #tsig(Sign.rep_sg signt);
    3.36 @@ -1821,7 +1824,7 @@
    3.37          | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
    3.38              if Pattern.matches tsigt (plhs, t) then
    3.39               (trace_term ("Trying procedure " ^ name ^ " on:") signt eta_t;
    3.40 -              case proc signt eta_t of
    3.41 +              case proc signt prems eta_t of
    3.42                  None => (trace "FAILED"; proc_rews eta_t ps)
    3.43                | Some raw_thm =>
    3.44                   (trace_thm ("Procedure " ^ name ^ " proved rewrite rule:") raw_thm;