major cleanup; got rid of obsolete meta_simpset;
authorwenzelm
Thu Jul 08 19:33:51 2004 +0200 (2004-07-08)
changeset 150230e4689f411d5
parent 15022 9a9a79fb33ee
child 15024 341cd221c3e1
major cleanup; got rid of obsolete meta_simpset;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Jul 08 19:33:31 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Jul 08 19:33:51 2004 +0200
     1.3 @@ -6,330 +6,386 @@
     1.4  *)
     1.5  
     1.6  infix 4
     1.7 -  setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
     1.8 -  addSolver addsimps delsimps addeqcongs deleqcongs addcongs delcongs
     1.9 -  setmksimps setmkeqTrue setmkcong setmksym settermless addsimprocs delsimprocs;
    1.10 +  addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
    1.11 +  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
    1.12 +  setloop addloop delloop setSSolver addSSolver setSolver addSolver;
    1.13  
    1.14  signature BASIC_META_SIMPLIFIER =
    1.15  sig
    1.16 +  val debug_simp: bool ref
    1.17    val trace_simp: bool ref
    1.18 -  val debug_simp: bool ref
    1.19    val simp_depth_limit: int ref
    1.20 -end;
    1.21 -
    1.22 -signature AUX_SIMPLIFIER =
    1.23 -sig
    1.24 -  type meta_simpset
    1.25 -  type simpset
    1.26 -  type simproc
    1.27 -  val full_mk_simproc: string -> cterm list
    1.28 -    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
    1.29 -  val mk_simproc: string -> cterm list
    1.30 -    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.31 +  type rrule
    1.32 +  type cong
    1.33    type solver
    1.34    val mk_solver: string -> (thm list -> int -> tactic) -> solver
    1.35 -  val empty_ss: simpset
    1.36 +  type simpset
    1.37 +  type proc
    1.38    val rep_ss: simpset ->
    1.39 -   {mss: meta_simpset,
    1.40 -    mk_cong: thm -> thm,
    1.41 +   {rules: rrule Net.net,
    1.42 +    prems: thm list,
    1.43 +    bounds: string list,
    1.44 +    depth: int} *
    1.45 +   {congs: (string * cong) list * string list,
    1.46 +    procs: proc Net.net,
    1.47 +    mk_rews:
    1.48 +     {mk: thm -> thm list,
    1.49 +      mk_cong: thm -> thm,
    1.50 +      mk_sym: thm -> thm option,
    1.51 +      mk_eq_True: thm -> thm option},
    1.52 +    termless: term * term -> bool,
    1.53      subgoal_tac: simpset -> int -> tactic,
    1.54      loop_tacs: (string * (int -> tactic)) list,
    1.55 -    unsafe_solvers: solver list,
    1.56 -    solvers: solver list}
    1.57 -  val from_mss: meta_simpset -> simpset
    1.58 -  val ss_of            : thm list -> simpset
    1.59 +    solvers: solver list * solver list}
    1.60    val print_ss: simpset -> unit
    1.61 -  val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    1.62 -  val setloop:      simpset *             (int -> tactic) -> simpset
    1.63 -  val addloop:      simpset *  (string * (int -> tactic)) -> simpset
    1.64 -  val delloop:      simpset *   string                    -> simpset
    1.65 -  val setSSolver:   simpset * solver -> simpset
    1.66 -  val addSSolver:   simpset * solver -> simpset
    1.67 -  val setSolver:    simpset * solver -> simpset
    1.68 -  val addSolver:    simpset * solver -> simpset
    1.69 -  val setmksimps:   simpset * (thm -> thm list) -> simpset
    1.70 -  val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
    1.71 -  val setmkcong:    simpset * (thm -> thm) -> simpset
    1.72 -  val setmksym:     simpset * (thm -> thm option) -> simpset
    1.73 -  val settermless:  simpset * (term * term -> bool) -> simpset
    1.74 -  val addsimps:     simpset * thm list -> simpset
    1.75 -  val delsimps:     simpset * thm list -> simpset
    1.76 -  val addeqcongs:   simpset * thm list -> simpset
    1.77 -  val deleqcongs:   simpset * thm list -> simpset
    1.78 -  val addcongs:     simpset * thm list -> simpset
    1.79 -  val delcongs:     simpset * thm list -> simpset
    1.80 -  val addsimprocs:  simpset * simproc list -> simpset
    1.81 -  val delsimprocs:  simpset * simproc list -> simpset
    1.82 -  val merge_ss:     simpset * simpset -> simpset
    1.83 -  val prems_of_ss:  simpset -> thm list
    1.84 +  val empty_ss: simpset
    1.85 +  val merge_ss: simpset * simpset -> simpset
    1.86 +  type simproc
    1.87 +  val mk_simproc: string -> cterm list ->
    1.88 +    (Sign.sg -> simpset -> term -> thm option) -> simproc
    1.89 +  val add_prems: thm list -> simpset -> simpset
    1.90 +  val prems_of_ss: simpset -> thm list
    1.91 +  val addsimps: simpset * thm list -> simpset
    1.92 +  val delsimps: simpset * thm list -> simpset
    1.93 +  val addeqcongs: simpset * thm list -> simpset
    1.94 +  val deleqcongs: simpset * thm list -> simpset
    1.95 +  val addcongs: simpset * thm list -> simpset
    1.96 +  val delcongs: simpset * thm list -> simpset
    1.97 +  val addsimprocs: simpset * simproc list -> simpset
    1.98 +  val delsimprocs: simpset * simproc list -> simpset
    1.99 +  val setmksimps: simpset * (thm -> thm list) -> simpset
   1.100 +  val setmkcong: simpset * (thm -> thm) -> simpset
   1.101 +  val setmksym: simpset * (thm -> thm option) -> simpset
   1.102 +  val setmkeqTrue: simpset * (thm -> thm option) -> simpset
   1.103 +  val settermless: simpset * (term * term -> bool) -> simpset
   1.104 +  val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   1.105 +  val setloop: simpset * (int -> tactic) -> simpset
   1.106 +  val addloop: simpset * (string * (int -> tactic)) -> simpset
   1.107 +  val delloop: simpset * string -> simpset
   1.108 +  val setSSolver: simpset * solver -> simpset
   1.109 +  val addSSolver: simpset * solver -> simpset
   1.110 +  val setSolver: simpset * solver -> simpset
   1.111 +  val addSolver: simpset * solver -> simpset
   1.112    val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
   1.113 -  val simproc: Sign.sg -> string -> string list
   1.114 -    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
   1.115 -  val simproc_i: Sign.sg -> string -> term list
   1.116 -    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
   1.117 -  val full_simproc: Sign.sg -> string -> string list
   1.118 -    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
   1.119 -  val full_simproc_i: Sign.sg -> string -> term list
   1.120 -    -> (simpset -> Sign.sg -> thm list -> term -> thm option) -> simproc
   1.121 -  val clear_ss  : simpset -> simpset
   1.122 -  val simp_thm  : bool * bool * bool -> simpset -> thm -> thm
   1.123 -  val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm
   1.124  end;
   1.125  
   1.126  signature META_SIMPLIFIER =
   1.127  sig
   1.128    include BASIC_META_SIMPLIFIER
   1.129 -  include AUX_SIMPLIFIER
   1.130    exception SIMPLIFIER of string * thm
   1.131 -  exception SIMPROC_FAIL of string * exn
   1.132 -  val dest_mss          : meta_simpset ->
   1.133 +  val dest_ss: simpset ->
   1.134      {simps: thm list, congs: thm list, procs: (string * cterm list) list}
   1.135 -  val empty_mss         : meta_simpset
   1.136 -  val clear_mss         : meta_simpset -> meta_simpset
   1.137 -  val merge_mss         : meta_simpset * meta_simpset -> meta_simpset
   1.138 -  val add_simps         : meta_simpset * thm list -> meta_simpset
   1.139 -  val del_simps         : meta_simpset * thm list -> meta_simpset
   1.140 -  val mss_of            : thm list -> meta_simpset
   1.141 -  val add_congs         : meta_simpset * thm list -> meta_simpset
   1.142 -  val del_congs         : meta_simpset * thm list -> meta_simpset
   1.143 -  val add_simprocs      : meta_simpset *
   1.144 -    (string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp) list
   1.145 -      -> meta_simpset
   1.146 -  val del_simprocs      : meta_simpset *
   1.147 -    (string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp) list
   1.148 -      -> meta_simpset
   1.149 -  val add_prems         : meta_simpset * thm list -> meta_simpset
   1.150 -  val prems_of_mss      : meta_simpset -> thm list
   1.151 -  val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
   1.152 -  val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
   1.153 -  val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
   1.154 -  val get_mk_rews       : meta_simpset -> thm -> thm list
   1.155 -  val get_mk_sym        : meta_simpset -> thm -> thm option
   1.156 -  val get_mk_eq_True    : meta_simpset -> thm -> thm option
   1.157 -  val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
   1.158 +  val clear_ss: simpset -> simpset
   1.159 +  exception SIMPROC_FAIL of string * exn
   1.160 +  val simproc_i: Sign.sg -> string -> term list
   1.161 +    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   1.162 +  val simproc: Sign.sg -> string -> string list
   1.163 +    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
   1.164    val rewrite_cterm: bool * bool * bool ->
   1.165 -    (meta_simpset -> thm -> thm option) -> simpset -> cterm -> thm
   1.166 -  val rewrite_aux       : (meta_simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
   1.167 -  val simplify_aux      : (meta_simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
   1.168 -  val rewrite_thm       : bool * bool * bool
   1.169 -                          -> (meta_simpset -> thm -> thm option)
   1.170 -                          -> simpset -> thm -> thm
   1.171 -  val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   1.172 -  val rewrite_goal_rule : bool* bool * bool
   1.173 -                          -> (meta_simpset -> thm -> thm option)
   1.174 -                          -> simpset -> int -> thm -> thm
   1.175 +    (simpset -> thm -> thm option) -> simpset -> cterm -> thm
   1.176 +  val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
   1.177 +  val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
   1.178    val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
   1.179 -  val asm_rewrite_goal_tac: bool*bool*bool ->
   1.180 -    (meta_simpset -> tactic) -> simpset -> int -> tactic
   1.181 -
   1.182 +  val rewrite_thm: bool * bool * bool ->
   1.183 +    (simpset -> thm -> thm option) -> simpset -> thm -> thm
   1.184 +  val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
   1.185 +  val rewrite_goal_rule: bool * bool * bool ->
   1.186 +    (simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
   1.187 +  val asm_rewrite_goal_tac: bool * bool * bool ->
   1.188 +    (simpset -> tactic) -> simpset -> int -> tactic
   1.189 +  val simp_thm: bool * bool * bool -> simpset -> thm -> thm
   1.190 +  val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm
   1.191  end;
   1.192  
   1.193 -structure MetaSimplifier : META_SIMPLIFIER =
   1.194 +structure MetaSimplifier: META_SIMPLIFIER =
   1.195  struct
   1.196  
   1.197 +
   1.198  (** diagnostics **)
   1.199  
   1.200  exception SIMPLIFIER of string * thm;
   1.201 -exception SIMPROC_FAIL of string * exn;
   1.202  
   1.203 +val debug_simp = ref false;
   1.204 +val trace_simp = ref false;
   1.205  val simp_depth = ref 0;
   1.206  val simp_depth_limit = ref 1000;
   1.207  
   1.208  local
   1.209  
   1.210  fun println a =
   1.211 -  tracing ((case ! simp_depth of 0 => "" | n => "[" ^ string_of_int n ^ "]") ^ a);
   1.212 +  tracing (case ! simp_depth of 0 => a | n => enclose "[" "]" (string_of_int n) ^ a);
   1.213  
   1.214  fun prnt warn a = if warn then warning a else println a;
   1.215 -fun prtm warn a sign t = prnt warn (a ^ "\n" ^ Sign.string_of_term sign t);
   1.216 +fun prtm warn a sg t = prnt warn (a ^ "\n" ^ Sign.string_of_term sg t);
   1.217  fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
   1.218  
   1.219  in
   1.220  
   1.221 -fun prthm warn a = prctm warn a o Thm.cprop_of;
   1.222 -
   1.223 -val trace_simp = ref false;
   1.224 -val debug_simp = ref false;
   1.225 -
   1.226 -fun trace warn a = if !trace_simp then prnt warn a else ();
   1.227 -fun debug warn a = if !debug_simp then prnt warn a else ();
   1.228 +fun debug warn a = if ! debug_simp then prnt warn a else ();
   1.229 +fun trace warn a = if ! trace_simp then prnt warn a else ();
   1.230  
   1.231 -fun trace_term warn a sign t = if !trace_simp then prtm warn a sign t else ();
   1.232 -fun trace_cterm warn a t = if !trace_simp then prctm warn a t else ();
   1.233 -fun debug_term warn a sign t = if !debug_simp then prtm warn a sign t else ();
   1.234 -
   1.235 -fun trace_thm a thm =
   1.236 -  let val {sign, prop, ...} = rep_thm thm
   1.237 -  in trace_term false a sign prop end;
   1.238 +fun debug_term warn a sign t = if ! debug_simp then prtm warn a sign t else ();
   1.239 +fun trace_term warn a sign t = if ! trace_simp then prtm warn a sign t else ();
   1.240 +fun trace_cterm warn a ct = if ! trace_simp then prctm warn a ct else ();
   1.241 +fun trace_thm a th = if ! trace_simp then prctm false a (Thm.cprop_of th) else ();
   1.242  
   1.243  fun trace_named_thm a (thm, name) =
   1.244 -  trace_thm (a ^ (if name = "" then "" else " " ^ quote name) ^ ":") thm;
   1.245 +  if ! trace_simp then
   1.246 +    prctm false (if name = "" then a else a ^ " " ^ quote name ^ ":") (Thm.cprop_of thm)
   1.247 +  else ();
   1.248 +
   1.249 +fun warn_thm a = prctm true a o Thm.cprop_of;
   1.250  
   1.251  end;
   1.252  
   1.253  
   1.254 -(** meta simp sets **)
   1.255  
   1.256 -(* basic components *)
   1.257 +(** datatype simpset **)
   1.258 +
   1.259 +(* rewrite rules *)
   1.260  
   1.261  type rrule = {thm: thm, name: string, lhs: term, elhs: cterm, fo: bool, perm: bool};
   1.262 -(* thm: the rewrite rule
   1.263 -   name: name of theorem from which rewrite rule was extracted
   1.264 -   lhs: the left-hand side
   1.265 -   elhs: the etac-contracted lhs.
   1.266 -   fo:  use first-order matching
   1.267 -   perm: the rewrite rule is permutative
   1.268 +
   1.269 +(*thm: the rewrite rule;
   1.270 +  name: name of theorem from which rewrite rule was extracted;
   1.271 +  lhs: the left-hand side;
   1.272 +  elhs: the etac-contracted lhs;
   1.273 +  fo: use first-order matching;
   1.274 +  perm: the rewrite rule is permutative;
   1.275 +
   1.276  Remarks:
   1.277    - elhs is used for matching,
   1.278 -    lhs only for preservation of bound variable names.
   1.279 +    lhs only for preservation of bound variable names;
   1.280    - fo is set iff
   1.281      either elhs is first-order (no Var is applied),
   1.282 -           in which case fo-matching is complete,
   1.283 +      in which case fo-matching is complete,
   1.284      or elhs is not a pattern,
   1.285 -       in which case there is nothing better to do.
   1.286 -*)
   1.287 -type cong = {thm: thm, lhs: cterm};
   1.288 +      in which case there is nothing better to do;*)
   1.289  
   1.290  fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
   1.291 -  #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   1.292 +  Drule.eq_thm_prop (thm1, thm2);
   1.293 +
   1.294 +
   1.295 +(* congruences *)
   1.296 +
   1.297 +type cong = {thm: thm, lhs: cterm};
   1.298  
   1.299  fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) =
   1.300 -  #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   1.301 -
   1.302 -fun eq_prem (thm1, thm2) =
   1.303 -  #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   1.304 +  Drule.eq_thm_prop (thm1, thm2);
   1.305  
   1.306  
   1.307 -(* datatype mss *)
   1.308 +(* solvers *)
   1.309 +
   1.310 +datatype solver =
   1.311 +  Solver of
   1.312 +   {name: string,
   1.313 +    solver: thm list -> int -> tactic,
   1.314 +    id: stamp};
   1.315 +
   1.316 +fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()};
   1.317 +
   1.318 +fun solver ths (Solver {solver = tacf, ...}) = tacf ths;
   1.319  
   1.320 -(*
   1.321 -  A "mss" contains data needed during conversion:
   1.322 +fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
   1.323 +val merge_solvers = gen_merge_lists eq_solver;
   1.324 +
   1.325 +
   1.326 +(* simplification sets and procedures *)
   1.327 +
   1.328 +(*A simpset contains data required during conversion:
   1.329      rules: discrimination net of rewrite rules;
   1.330 +    prems: current premises;
   1.331 +    bounds: names of bound variables already used
   1.332 +      (for generating new names when rewriting under lambda abstractions);
   1.333 +    depth: depth of conditional rewriting;
   1.334      congs: association list of congruence rules and
   1.335             a list of `weak' congruence constants.
   1.336             A congruence is `weak' if it avoids normalization of some argument.
   1.337      procs: discrimination net of simplification procedures
   1.338        (functions that prove rewrite rules on the fly);
   1.339 -    bounds: names of bound variables already used
   1.340 -      (for generating new names when rewriting under lambda abstractions);
   1.341 -    prems: current premises;
   1.342 -    mk_rews: mk: turns simplification thms into rewrite rules;
   1.343 -             mk_sym: turns == around; (needs Drule!)
   1.344 -             mk_eq_True: turns P into P == True - logic specific;
   1.345 -    termless: relation for ordered rewriting;
   1.346 -    depth: depth of conditional rewriting;
   1.347 -*)
   1.348 -
   1.349 -datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   1.350 +    mk_rews:
   1.351 +      mk: turn simplification thms into rewrite rules;
   1.352 +      mk_cong: prepare congruence rules;
   1.353 +      mk_sym: turn == around;
   1.354 +      mk_eq_True: turn P into P == True;
   1.355 +    termless: relation for ordered rewriting;*)
   1.356  
   1.357 -datatype meta_simpset =
   1.358 -  Mss of {
   1.359 -    rules: rrule Net.net,
   1.360 -    congs: (string * cong) list * string list,
   1.361 -    procs: meta_simproc Net.net,
   1.362 -    bounds: string list,
   1.363 +type mk_rews =
   1.364 + {mk: thm -> thm list,
   1.365 +  mk_cong: thm -> thm,
   1.366 +  mk_sym: thm -> thm option,
   1.367 +  mk_eq_True: thm -> thm option};
   1.368 +
   1.369 +datatype simpset =
   1.370 +  Simpset of
   1.371 +   {rules: rrule Net.net,
   1.372      prems: thm list,
   1.373 -    mk_rews: {mk: thm -> thm list,
   1.374 -              mk_sym: thm -> thm option,
   1.375 -              mk_eq_True: thm -> thm option},
   1.376 +    bounds: string list,
   1.377 +    depth: int} *
   1.378 +   {congs: (string * cong) list * string list,
   1.379 +    procs: proc Net.net,
   1.380 +    mk_rews: mk_rews,
   1.381      termless: term * term -> bool,
   1.382 -    depth: int}
   1.383 -and simpset =
   1.384 -  Simpset of {
   1.385 -    mss: meta_simpset,
   1.386 -    mk_cong: thm -> thm,
   1.387      subgoal_tac: simpset -> int -> tactic,
   1.388      loop_tacs: (string * (int -> tactic)) list,
   1.389 -    unsafe_solvers: solver list,
   1.390 -    solvers: solver list}
   1.391 -withtype meta_simproc =
   1.392 - {name: string, proc: simpset -> Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
   1.393 +    solvers: solver list * solver list}
   1.394 +and proc =
   1.395 +  Proc of
   1.396 +   {name: string,
   1.397 +    lhs: cterm,
   1.398 +    proc: Sign.sg -> simpset -> term -> thm option,
   1.399 +    id: stamp};
   1.400 +
   1.401 +fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = (id1 = id2);
   1.402 +
   1.403 +fun rep_ss (Simpset args) = args;
   1.404  
   1.405 -fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth) =
   1.406 -  Mss {rules = rules, congs = congs, procs = procs, bounds = bounds,
   1.407 -       prems=prems, mk_rews=mk_rews, termless=termless, depth=depth};
   1.408 +fun make_ss1 (rules, prems, bounds, depth) =
   1.409 +  {rules = rules, prems = prems, bounds = bounds, depth = depth};
   1.410 +
   1.411 +fun map_ss1 f {rules, prems, bounds, depth} =
   1.412 +  make_ss1 (f (rules, prems, bounds, depth));
   1.413  
   1.414 -fun upd_rules(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}, rules') =
   1.415 -  mk_mss(rules',congs,procs,bounds,prems,mk_rews,termless,depth);
   1.416 +fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
   1.417 +  {congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
   1.418 +    subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
   1.419 +
   1.420 +fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
   1.421 +  make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   1.422 +
   1.423 +fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
   1.424  
   1.425 -val empty_mss =
   1.426 -  let val mk_rews = {mk = K [], mk_sym = K None, mk_eq_True = K None}
   1.427 -  in mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, Term.termless, 0) end;
   1.428 +fun map_simpset f (Simpset ({rules, prems, bounds, depth},
   1.429 +    {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers})) =
   1.430 +  make_simpset (f ((rules, prems, bounds, depth),
   1.431 +    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)));
   1.432  
   1.433 -fun clear_mss (Mss {mk_rews, termless, ...}) =
   1.434 -  mk_mss (Net.empty, ([], []), Net.empty, [], [], mk_rews, termless,0);
   1.435 +fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
   1.436 +fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
   1.437 +
   1.438 +
   1.439 +(* print simpsets *)
   1.440  
   1.441 -fun incr_depth(Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) =
   1.442 -  let val depth1 = depth+1
   1.443 -  in if depth1 > !simp_depth_limit
   1.444 -     then (warning "simp_depth_limit exceeded - giving up"; None)
   1.445 -     else (if depth1 mod 10 = 0
   1.446 -           then warning("Simplification depth " ^ string_of_int depth1)
   1.447 -           else ();
   1.448 -           Some(mk_mss(rules,congs,procs,bounds,prems,mk_rews,termless,depth1))
   1.449 -          )
   1.450 +fun dest_ss (Simpset ({rules, ...}, {congs = (congs, _), procs, ...})) =
   1.451 +  {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
   1.452 +   congs = map (fn (_, {thm, ...}) => thm) congs,
   1.453 +   procs =
   1.454 +     map (fn (_, Proc {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
   1.455 +     |> partition_eq eq_snd
   1.456 +     |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
   1.457 +     |> Library.sort_wrt #1};
   1.458 +
   1.459 +fun print_ss ss =
   1.460 +  let
   1.461 +    val {simps, procs, congs} = dest_ss ss;
   1.462 +
   1.463 +    val pretty_thms = map Display.pretty_thm;
   1.464 +    fun pretty_proc (name, lhss) =
   1.465 +      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
   1.466 +  in
   1.467 +    [Pretty.big_list "simplification rules:" (pretty_thms simps),
   1.468 +      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
   1.469 +      Pretty.big_list "congruences:" (pretty_thms congs)]
   1.470 +    |> Pretty.chunks |> Pretty.writeln
   1.471    end;
   1.472  
   1.473 -datatype simproc =
   1.474 -  Simproc of string * cterm list * (simpset -> Sign.sg -> thm list -> term -> thm option) * stamp
   1.475 +
   1.476 +(* empty simpsets *)
   1.477 +
   1.478 +local
   1.479 +
   1.480 +fun init_ss mk_rews termless subgoal_tac solvers =
   1.481 +  make_simpset ((Net.empty, [], [], 0),
   1.482 +    (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
   1.483 +
   1.484 +val basic_mk_rews: mk_rews =
   1.485 + {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
   1.486 +  mk_cong = I,
   1.487 +  mk_sym = Some o Drule.symmetric_fun,
   1.488 +  mk_eq_True = K None};
   1.489 +
   1.490 +in
   1.491 +
   1.492 +val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
   1.493 +
   1.494 +fun clear_ss (Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
   1.495 +  init_ss mk_rews termless subgoal_tac solvers;
   1.496 +
   1.497 +end;
   1.498 +
   1.499 +
   1.500 +(* merge simpsets *)            (*NOTE: ignores some fields of 2nd simpset*)
   1.501  
   1.502 -fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
   1.503 +fun merge_ss (ss1, ss2) =
   1.504 +  let
   1.505 +    val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth},
   1.506 +     {congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
   1.507 +      loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
   1.508 +    val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = _},
   1.509 +     {congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
   1.510 +      loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
   1.511  
   1.512 -fun mk_simproc (name, proc, lhs, id) =
   1.513 -  {name = name, proc = proc, lhs = lhs, id = id};
   1.514 +    val rules' = Net.merge (rules1, rules2, eq_rrule);
   1.515 +    val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2;
   1.516 +    val bounds' = merge_lists bounds1 bounds2;
   1.517 +    val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2;
   1.518 +    val weak' = merge_lists weak1 weak2;
   1.519 +    val procs' = Net.merge (procs1, procs2, eq_proc);
   1.520 +    val loop_tacs' = merge_alists loop_tacs1 loop_tacs2;
   1.521 +    val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2;
   1.522 +    val solvers' = merge_solvers solvers1 solvers2;
   1.523 +  in
   1.524 +    make_simpset ((rules', prems', bounds', depth), ((congs', weak'), procs',
   1.525 +      mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
   1.526 +  end;
   1.527 +
   1.528 +
   1.529 +(* simprocs *)
   1.530 +
   1.531 +exception SIMPROC_FAIL of string * exn;
   1.532 +
   1.533 +datatype simproc = Simproc of proc list;
   1.534 +
   1.535 +fun mk_simproc name lhss proc =
   1.536 +  let val id = stamp () in
   1.537 +    Simproc (lhss |> map (fn lhs =>
   1.538 +      Proc {name = name, lhs = lhs, proc = proc, id = id}))
   1.539 +  end;
   1.540 +
   1.541 +fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg o Logic.varify);
   1.542 +fun simproc sg name = simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
   1.543 +
   1.544  
   1.545  
   1.546  (** simpset operations **)
   1.547  
   1.548 -(* term variables *)
   1.549 +(* bounds and prems *)
   1.550  
   1.551 -val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   1.552 -fun term_varnames t = add_term_varnames ([], t);
   1.553 -
   1.554 -
   1.555 -(* dest_mss *)
   1.556 +fun add_bound b = map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.557 +  (rules, prems, b :: bounds, depth));
   1.558  
   1.559 -fun dest_mss (Mss {rules, congs, procs, ...}) =
   1.560 -  {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
   1.561 -   congs = map (fn (_, {thm, ...}) => thm) (fst congs),
   1.562 -   procs =
   1.563 -     map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
   1.564 -     |> partition_eq eq_snd
   1.565 -     |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
   1.566 -     |> Library.sort_wrt #1};
   1.567 +fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.568 +  (rules, ths @ prems, bounds, depth));
   1.569 +
   1.570 +fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
   1.571  
   1.572  
   1.573 -(* merge_mss *)       (*NOTE: ignores mk_rews, termless and depth of 2nd mss*)
   1.574 +(* addsimps *)
   1.575  
   1.576 -fun merge_mss
   1.577 - (Mss {rules = rules1, congs = (congs1,weak1), procs = procs1,
   1.578 -       bounds = bounds1, prems = prems1, mk_rews, termless, depth},
   1.579 -  Mss {rules = rules2, congs = (congs2,weak2), procs = procs2,
   1.580 -       bounds = bounds2, prems = prems2, ...}) =
   1.581 -      mk_mss
   1.582 -       (Net.merge (rules1, rules2, eq_rrule),
   1.583 -        (gen_merge_lists (eq_cong o pairself snd) congs1 congs2,
   1.584 -        merge_lists weak1 weak2),
   1.585 -        Net.merge (procs1, procs2, eq_simproc),
   1.586 -        merge_lists bounds1 bounds2,
   1.587 -        gen_merge_lists eq_prem prems1 prems2,
   1.588 -        mk_rews, termless, depth);
   1.589 +fun mk_rrule2 {thm, name, lhs, elhs, perm} =
   1.590 +  let
   1.591 +    val fo = Pattern.first_order (term_of elhs) orelse not (Pattern.pattern (term_of elhs))
   1.592 +  in {thm = thm, name = name, lhs = lhs, elhs = elhs, fo = fo, perm = perm} end;
   1.593  
   1.594 -
   1.595 -(* add_simps *)
   1.596 -
   1.597 -fun mk_rrule2{thm, name, lhs, elhs, perm} =
   1.598 -  let val fo = Pattern.first_order (term_of elhs) orelse not(Pattern.pattern (term_of elhs))
   1.599 -  in {thm=thm, name=name, lhs=lhs, elhs=elhs, fo=fo, perm=perm} end
   1.600 -
   1.601 -fun insert_rrule quiet (mss as Mss {rules,...},
   1.602 -                 rrule as {thm,name,lhs,elhs,perm}) =
   1.603 -  (trace_named_thm "Adding rewrite rule" (thm, name);
   1.604 -   let val rrule2 as {elhs,...} = mk_rrule2 rrule
   1.605 -       val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule)
   1.606 -   in upd_rules(mss,rules') end
   1.607 -   handle Net.INSERT => if quiet then mss else
   1.608 -     (prthm true "Ignoring duplicate rewrite rule:" thm; mss));
   1.609 +fun insert_rrule quiet (ss, rrule as {thm, name, lhs, elhs, perm}) =
   1.610 + (trace_named_thm "Adding rewrite rule" (thm, name);
   1.611 +  ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.612 +    let
   1.613 +      val rrule2 as {elhs, ...} = mk_rrule2 rrule;
   1.614 +      val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule);
   1.615 +    in (rules', prems, bounds, depth) end)
   1.616 +  handle Net.INSERT =>
   1.617 +    (if quiet then () else warn_thm "Ignoring duplicate rewrite rule:" thm; ss));
   1.618  
   1.619  fun vperm (Var _, Var _) = true
   1.620    | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   1.621 @@ -346,36 +402,37 @@
   1.622  fun rewrite_rule_extra_vars prems elhs erhs =
   1.623    not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems))
   1.624    orelse
   1.625 -  not ((term_tvars erhs) subset
   1.626 -       (term_tvars elhs  union  List.concat(map term_tvars prems)));
   1.627 +  not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));
   1.628  
   1.629 -(*Simple test for looping rewrite rules and stupid orientations*)
   1.630 +(*simple test for looping rewrite rules and stupid orientations*)
   1.631  fun reorient sign prems lhs rhs =
   1.632 -   rewrite_rule_extra_vars prems lhs rhs
   1.633 -  orelse
   1.634 -   is_Var (head_of lhs)
   1.635 -  orelse
   1.636 -   (exists (apl (lhs, Logic.occs)) (rhs :: prems))
   1.637 -  orelse
   1.638 -   (null prems andalso
   1.639 -    Pattern.matches (Sign.tsig_of sign) (lhs, rhs))
   1.640 +  rewrite_rule_extra_vars prems lhs rhs
   1.641 +    orelse
   1.642 +  is_Var (head_of lhs)
   1.643 +    orelse
   1.644 +  exists (apl (lhs, Logic.occs)) (rhs :: prems)
   1.645 +    orelse
   1.646 +  null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs)
   1.647      (*the condition "null prems" is necessary because conditional rewrites
   1.648        with extra variables in the conditions may terminate although
   1.649 -      the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
   1.650 -  orelse
   1.651 -   (is_Const lhs andalso not(is_Const rhs))
   1.652 +      the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
   1.653 +    orelse
   1.654 +  is_Const lhs andalso not (is_Const rhs);
   1.655  
   1.656  fun decomp_simp thm =
   1.657 -  let val {sign, prop, ...} = rep_thm thm;
   1.658 -      val prems = Logic.strip_imp_prems prop;
   1.659 -      val concl = Drule.strip_imp_concl (cprop_of thm);
   1.660 -      val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
   1.661 -        raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm)
   1.662 -      val elhs = snd (Drule.dest_equals (cprop_of (Thm.eta_conversion lhs)));
   1.663 -      val elhs = if elhs=lhs then lhs else elhs (* try to share *)
   1.664 -      val erhs = Pattern.eta_contract (term_of rhs);
   1.665 -      val perm = var_perm (term_of elhs, erhs) andalso not (term_of elhs aconv erhs)
   1.666 -                 andalso not (is_Var (term_of elhs))
   1.667 +  let
   1.668 +    val {sign, prop, ...} = Thm.rep_thm thm;
   1.669 +    val prems = Logic.strip_imp_prems prop;
   1.670 +    val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
   1.671 +    val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
   1.672 +      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
   1.673 +    val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs));
   1.674 +    val elhs = if elhs = lhs then lhs else elhs;  (*share identical copies*)
   1.675 +    val erhs = Pattern.eta_contract (term_of rhs);
   1.676 +    val perm =
   1.677 +      var_perm (term_of elhs, erhs) andalso
   1.678 +      not (term_of elhs aconv erhs) andalso
   1.679 +      not (is_Var (term_of elhs));
   1.680    in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
   1.681  
   1.682  fun decomp_simp' thm =
   1.683 @@ -384,409 +441,255 @@
   1.684      else (lhs, rhs)
   1.685    end;
   1.686  
   1.687 -fun mk_eq_True (Mss{mk_rews={mk_eq_True,...},...}) (thm, name) =
   1.688 -  case mk_eq_True thm of
   1.689 +fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
   1.690 +  (case mk_eq_True thm of
   1.691      None => []
   1.692    | Some eq_True =>
   1.693 -      let val (_,_,lhs,elhs,_,_) = decomp_simp eq_True
   1.694 -      in [{thm=eq_True, name=name, lhs=lhs, elhs=elhs, perm=false}] end;
   1.695 +      let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True
   1.696 +      in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
   1.697  
   1.698 -(* create the rewrite rule and possibly also the ==True variant,
   1.699 -   in case there are extra vars on the rhs *)
   1.700 -fun rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm2) =
   1.701 -  let val rrule = {thm=thm, name=name, lhs=lhs, elhs=elhs, perm=false}
   1.702 -  in if (term_varnames rhs)  subset (term_varnames lhs) andalso
   1.703 -        (term_tvars rhs) subset (term_tvars lhs)
   1.704 -     then [rrule]
   1.705 -     else mk_eq_True mss (thm2, name) @ [rrule]
   1.706 +(*create the rewrite rule and possibly also the eq_True variant,
   1.707 +  in case there are extra vars on the rhs*)
   1.708 +fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
   1.709 +  let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
   1.710 +    if term_varnames rhs subset term_varnames lhs andalso
   1.711 +      term_tvars rhs subset term_tvars lhs then [rrule]
   1.712 +    else mk_eq_True ss (thm2, name) @ [rrule]
   1.713    end;
   1.714  
   1.715 -fun mk_rrule mss (thm, name) =
   1.716 -  let val (_,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   1.717 -  in if perm then [{thm=thm, name=name, lhs=lhs, elhs=elhs, perm=true}] else
   1.718 -     (* weak test for loops: *)
   1.719 -     if rewrite_rule_extra_vars prems lhs rhs orelse
   1.720 -        is_Var (term_of elhs)
   1.721 -     then mk_eq_True mss (thm, name)
   1.722 -     else rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm)
   1.723 +fun mk_rrule ss (thm, name) =
   1.724 +  let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
   1.725 +    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
   1.726 +    else
   1.727 +      (*weak test for loops*)
   1.728 +      if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
   1.729 +      then mk_eq_True ss (thm, name)
   1.730 +      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   1.731    end;
   1.732  
   1.733 -fun orient_rrule mss (thm, name) =
   1.734 -  let val (sign,prems,lhs,elhs,rhs,perm) = decomp_simp thm
   1.735 -  in if perm then [{thm=thm, name=name, lhs=lhs, elhs=elhs, perm=true}]
   1.736 -     else if reorient sign prems lhs rhs
   1.737 -          then if reorient sign prems rhs lhs
   1.738 -               then mk_eq_True mss (thm, name)
   1.739 -               else let val Mss{mk_rews={mk_sym,...},...} = mss
   1.740 -                    in case mk_sym thm of
   1.741 -                         None => []
   1.742 -                       | Some thm' =>
   1.743 -                           let val (_,_,lhs',elhs',rhs',_) = decomp_simp thm'
   1.744 -                           in rrule_eq_True(thm',name,lhs',elhs',rhs',mss,thm) end
   1.745 -                    end
   1.746 -          else rrule_eq_True(thm,name,lhs,elhs,rhs,mss,thm)
   1.747 +fun orient_rrule ss (thm, name) =
   1.748 +  let val (sign, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
   1.749 +    if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
   1.750 +    else if reorient sign prems lhs rhs then
   1.751 +      if reorient sign prems rhs lhs
   1.752 +      then mk_eq_True ss (thm, name)
   1.753 +      else
   1.754 +        let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in
   1.755 +          (case mk_sym thm of
   1.756 +            None => []
   1.757 +          | Some thm' =>
   1.758 +              let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
   1.759 +              in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
   1.760 +        end
   1.761 +    else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   1.762    end;
   1.763  
   1.764 -fun extract_rews(Mss{mk_rews = {mk,...},...},thms) =
   1.765 +fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
   1.766    flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
   1.767  
   1.768 -fun orient_comb_simps comb mk_rrule (mss,thms) =
   1.769 -  let val rews = extract_rews(mss,thms)
   1.770 -      val rrules = flat (map mk_rrule rews)
   1.771 -  in foldl comb (mss,rrules) end
   1.772 -
   1.773 -(* Add rewrite rules explicitly; do not reorient! *)
   1.774 -fun add_simps(mss,thms) =
   1.775 -  orient_comb_simps (insert_rrule false) (mk_rrule mss) (mss,thms);
   1.776 -
   1.777 -fun mss_of thms = foldl (insert_rrule false) (empty_mss, flat
   1.778 -  (map (fn thm => mk_rrule empty_mss (thm, Thm.name_of_thm thm)) thms));
   1.779 +fun orient_comb_simps comb mk_rrule (ss, thms) =
   1.780 +  let
   1.781 +    val rews = extract_rews (ss, thms);
   1.782 +    val rrules = flat (map mk_rrule rews);
   1.783 +  in foldl comb (ss, rrules) end;
   1.784  
   1.785 -fun extract_safe_rrules(mss,thm) =
   1.786 -  flat (map (orient_rrule mss) (extract_rews(mss,[thm])));
   1.787 -
   1.788 -(* del_simps *)
   1.789 +fun extract_safe_rrules (ss, thm) =
   1.790 +  flat (map (orient_rrule ss) (extract_rews (ss, [thm])));
   1.791  
   1.792 -fun del_rrule(mss as Mss {rules,...},
   1.793 -              rrule as {thm, elhs, ...}) =
   1.794 -  (upd_rules(mss, Net.delete_term ((term_of elhs, rrule), rules, eq_rrule))
   1.795 -   handle Net.DELETE =>
   1.796 -     (prthm true "Rewrite rule not in simpset:" thm; mss));
   1.797 -
   1.798 -fun del_simps(mss,thms) =
   1.799 -  orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule mss) (mss,thms);
   1.800 +(*add rewrite rules explicitly; do not reorient!*)
   1.801 +fun ss addsimps thms =
   1.802 +  orient_comb_simps (insert_rrule false) (mk_rrule ss) (ss, thms);
   1.803  
   1.804  
   1.805 -(* add_congs *)
   1.806 +(* delsimps *)
   1.807  
   1.808 -fun is_full_cong_prems [] varpairs = null varpairs
   1.809 -  | is_full_cong_prems (p::prems) varpairs =
   1.810 -    (case Logic.strip_assums_concl p of
   1.811 -       Const("==",_) $ lhs $ rhs =>
   1.812 -         let val (x,xs) = strip_comb lhs and (y,ys) = strip_comb rhs
   1.813 -         in is_Var x  andalso  forall is_Bound xs  andalso
   1.814 -            null(findrep(xs))  andalso xs=ys andalso
   1.815 -            (x,y) mem varpairs andalso
   1.816 -            is_full_cong_prems prems (varpairs\(x,y))
   1.817 -         end
   1.818 -     | _ => false);
   1.819 +fun del_rrule (ss, rrule as {thm, elhs, ...}) =
   1.820 +  ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
   1.821 +    (Net.delete_term ((term_of elhs, rrule), rules, eq_rrule), prems, bounds, depth))
   1.822 +  handle Net.DELETE => (warn_thm "Rewrite rule not in simpset:" thm; ss);
   1.823  
   1.824 -fun is_full_cong thm =
   1.825 -let val prems = prems_of thm
   1.826 -    and concl = concl_of thm
   1.827 -    val (lhs,rhs) = Logic.dest_equals concl
   1.828 -    val (f,xs) = strip_comb lhs
   1.829 -    and (g,ys) = strip_comb rhs
   1.830 -in
   1.831 -  f=g andalso null(findrep(xs@ys)) andalso length xs = length ys andalso
   1.832 -  is_full_cong_prems prems (xs ~~ ys)
   1.833 -end
   1.834 +fun ss delsimps thms =
   1.835 +  orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
   1.836 +
   1.837 +
   1.838 +(* congs *)
   1.839  
   1.840  fun cong_name (Const (a, _)) = Some a
   1.841    | cong_name (Free (a, _)) = Some ("Free: " ^ a)
   1.842    | cong_name _ = None;
   1.843  
   1.844 -fun add_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
   1.845 +local
   1.846 +
   1.847 +fun is_full_cong_prems [] [] = true
   1.848 +  | is_full_cong_prems [] _ = false
   1.849 +  | is_full_cong_prems (p :: prems) varpairs =
   1.850 +      (case Logic.strip_assums_concl p of
   1.851 +        Const ("==", _) $ lhs $ rhs =>
   1.852 +          let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
   1.853 +            is_Var x andalso forall is_Bound xs andalso
   1.854 +            null (findrep xs) andalso xs = ys andalso
   1.855 +            (x, y) mem varpairs andalso
   1.856 +            is_full_cong_prems prems (varpairs \ (x, y))
   1.857 +          end
   1.858 +      | _ => false);
   1.859 +
   1.860 +fun is_full_cong thm =
   1.861    let
   1.862 -    val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (cprop_of thm)) handle TERM _ =>
   1.863 -      raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.864 -(*   val lhs = Pattern.eta_contract lhs; *)
   1.865 -    val a = (case cong_name (head_of (term_of lhs)) of
   1.866 -        Some a => a
   1.867 -      | None =>
   1.868 -        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm));
   1.869 -    val (alist,weak) = congs
   1.870 -    val alist2 = overwrite_warn (alist, (a,{lhs=lhs, thm=thm}))
   1.871 -           ("Overwriting congruence rule for " ^ quote a);
   1.872 -    val weak2 = if is_full_cong thm then weak else a::weak
   1.873 +    val prems = prems_of thm and concl = concl_of thm;
   1.874 +    val (lhs, rhs) = Logic.dest_equals concl;
   1.875 +    val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
   1.876    in
   1.877 -    mk_mss (rules,(alist2,weak2),procs,bounds,prems,mk_rews,termless,depth)
   1.878 +    f = g andalso null (findrep (xs @ ys)) andalso length xs = length ys andalso
   1.879 +    is_full_cong_prems prems (xs ~~ ys)
   1.880    end;
   1.881  
   1.882 -val (op add_congs) = foldl add_cong;
   1.883 -
   1.884 -
   1.885 -(* del_congs *)
   1.886 +fun add_cong (ss, thm) = ss |>
   1.887 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.888 +    let
   1.889 +      val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
   1.890 +        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.891 +    (*val lhs = Pattern.eta_contract lhs;*)
   1.892 +      val a = the (cong_name (head_of (term_of lhs))) handle Library.OPTION =>
   1.893 +        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
   1.894 +      val (alist, weak) = congs;
   1.895 +      val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
   1.896 +        ("Overwriting congruence rule for " ^ quote a);
   1.897 +      val weak2 = if is_full_cong thm then weak else a :: weak;
   1.898 +    in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   1.899  
   1.900 -fun del_cong (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thm) =
   1.901 -  let
   1.902 -    val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ =>
   1.903 -      raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.904 -(*   val lhs = Pattern.eta_contract lhs; *)
   1.905 -    val a = (case cong_name (head_of lhs) of
   1.906 -        Some a => a
   1.907 -      | None =>
   1.908 -        raise SIMPLIFIER ("Congruence must start with a constant", thm));
   1.909 -    val (alist,_) = congs
   1.910 -    val alist2 = filter (fn (x,_)=> x<>a) alist
   1.911 -    val weak2 = mapfilter (fn(a,{thm,...}) => if is_full_cong thm then None
   1.912 -                                              else Some a)
   1.913 -                   alist2
   1.914 -  in
   1.915 -    mk_mss (rules,(alist2,weak2),procs,bounds,prems,mk_rews,termless,depth)
   1.916 -  end;
   1.917 +fun del_cong (ss, thm) = ss |>
   1.918 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.919 +    let
   1.920 +      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
   1.921 +        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
   1.922 +    (*val lhs = Pattern.eta_contract lhs;*)
   1.923 +      val a = the (cong_name (head_of lhs)) handle Library.OPTION =>
   1.924 +        raise SIMPLIFIER ("Congruence must start with a constant", thm);
   1.925 +      val (alist, _) = congs;
   1.926 +      val alist2 = filter (fn (x, _) => x <> a) alist;
   1.927 +      val weak2 = alist2 |> mapfilter (fn (a, {thm, ...}) =>
   1.928 +        if is_full_cong thm then None else Some a);
   1.929 +    in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   1.930  
   1.931 -val (op del_congs) = foldl del_cong;
   1.932 +fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f;
   1.933 +
   1.934 +in
   1.935 +
   1.936 +val (op addeqcongs) = foldl add_cong;
   1.937 +val (op deleqcongs) = foldl del_cong;
   1.938 +
   1.939 +fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
   1.940 +fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
   1.941 +
   1.942 +end;
   1.943  
   1.944  
   1.945 -(* add_simprocs *)
   1.946 +(* simprocs *)
   1.947 +
   1.948 +local
   1.949  
   1.950 -fun add_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth},
   1.951 -    (name, lhs, proc, id)) =
   1.952 -  let val {sign, t, ...} = rep_cterm lhs
   1.953 -  in (trace_term false ("Adding simplification procedure " ^ quote name ^ " for")
   1.954 -      sign t;
   1.955 -    mk_mss (rules, congs,
   1.956 -      Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.957 -        handle Net.INSERT =>
   1.958 -            (warning ("Ignoring duplicate simplification procedure \""
   1.959 -                      ^ name ^ "\"");
   1.960 -             procs),
   1.961 -        bounds, prems, mk_rews, termless,depth))
   1.962 -  end;
   1.963 -
   1.964 -fun add_simproc (mss, (name, lhss, proc, id)) =
   1.965 -  foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   1.966 -
   1.967 -val add_simprocs = foldl add_simproc;
   1.968 -
   1.969 +fun add_proc (ss, proc as Proc {name, lhs, ...}) =
   1.970 + (trace_cterm false ("Adding simplification procedure " ^ quote name ^ " for") lhs;
   1.971 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.972 +    (congs, Net.insert_term ((term_of lhs, proc), procs, eq_proc),
   1.973 +      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
   1.974 +  handle Net.INSERT =>
   1.975 +    (warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
   1.976  
   1.977 -(* del_simprocs *)
   1.978 -
   1.979 -fun del_proc (mss as Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth},
   1.980 -    (name, lhs, proc, id)) =
   1.981 -  mk_mss (rules, congs,
   1.982 -    Net.delete_term ((term_of lhs, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.983 -      handle Net.DELETE =>
   1.984 -          (warning ("Simplification procedure \"" ^ name ^
   1.985 -                       "\" not in simpset"); procs),
   1.986 -      bounds, prems, mk_rews, termless, depth);
   1.987 +fun del_proc (ss, proc as Proc {name, lhs, ...}) =
   1.988 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   1.989 +    (congs, Net.delete_term ((term_of lhs, proc), procs, eq_proc),
   1.990 +      mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
   1.991 +  handle Net.DELETE =>
   1.992 +    (warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
   1.993  
   1.994 -fun del_simproc (mss, (name, lhss, proc, id)) =
   1.995 -  foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   1.996 -
   1.997 -val del_simprocs = foldl del_simproc;
   1.998 -
   1.999 +in
  1.1000  
  1.1001 -(* prems *)
  1.1002 +val (op addsimprocs) = foldl (fn (ss, Simproc procs) => foldl add_proc (ss, procs));
  1.1003 +val (op delsimprocs) = foldl (fn (ss, Simproc procs) => foldl del_proc (ss, procs));
  1.1004  
  1.1005 -fun add_prems (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, thms) =
  1.1006 -  mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless, depth);
  1.1007 -
  1.1008 -fun prems_of_mss (Mss {prems, ...}) = prems;
  1.1009 +end;
  1.1010  
  1.1011  
  1.1012  (* mk_rews *)
  1.1013  
  1.1014 -fun set_mk_rews
  1.1015 -  (Mss {rules, congs, procs, bounds, prems, mk_rews, termless, depth}, mk) =
  1.1016 -    mk_mss (rules, congs, procs, bounds, prems,
  1.1017 -            {mk=mk, mk_sym= #mk_sym mk_rews, mk_eq_True= #mk_eq_True mk_rews},
  1.1018 -            termless, depth);
  1.1019 +local
  1.1020 +
  1.1021 +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True},
  1.1022 +      termless, subgoal_tac, loop_tacs, solvers) =>
  1.1023 +  let val (mk', mk_cong', mk_sym', mk_eq_True') = f (mk, mk_cong, mk_sym, mk_eq_True) in
  1.1024 +    (congs, procs, {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
  1.1025 +      termless, subgoal_tac, loop_tacs, solvers)
  1.1026 +  end);
  1.1027 +
  1.1028 +in
  1.1029  
  1.1030 -fun set_mk_sym
  1.1031 -  (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, mk_sym) =
  1.1032 -    mk_mss (rules, congs, procs, bounds, prems,
  1.1033 -            {mk= #mk mk_rews, mk_sym= mk_sym, mk_eq_True= #mk_eq_True mk_rews},
  1.1034 -            termless,depth);
  1.1035 +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True) =>
  1.1036 +  (mk, mk_cong, mk_sym, mk_eq_True));
  1.1037 +
  1.1038 +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True) =>
  1.1039 +  (mk, mk_cong, mk_sym, mk_eq_True));
  1.1040  
  1.1041 -fun set_mk_eq_True
  1.1042 -  (Mss {rules,congs,procs,bounds,prems,mk_rews,termless,depth}, mk_eq_True) =
  1.1043 -    mk_mss (rules, congs, procs, bounds, prems,
  1.1044 -            {mk= #mk mk_rews, mk_sym= #mk_sym mk_rews, mk_eq_True= mk_eq_True},
  1.1045 -            termless,depth);
  1.1046 +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True) =>
  1.1047 +  (mk, mk_cong, mk_sym, mk_eq_True));
  1.1048  
  1.1049 -fun get_mk_rews    (Mss {mk_rews,...}) = #mk         mk_rews
  1.1050 -fun get_mk_sym     (Mss {mk_rews,...}) = #mk_sym     mk_rews
  1.1051 -fun get_mk_eq_True (Mss {mk_rews,...}) = #mk_eq_True mk_rews
  1.1052 +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _) =>
  1.1053 +  (mk, mk_cong, mk_sym, mk_eq_True));
  1.1054 +
  1.1055 +end;
  1.1056 +
  1.1057  
  1.1058  (* termless *)
  1.1059  
  1.1060 -fun set_termless
  1.1061 -  (Mss {rules, congs, procs, bounds, prems, mk_rews, depth, ...}, termless) =
  1.1062 -    mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless, depth);
  1.1063 -
  1.1064 -
  1.1065 -
  1.1066 -(** simplification procedures **)
  1.1067 -
  1.1068 -(* datatype simproc *)
  1.1069 -
  1.1070 -fun full_mk_simproc name lhss proc =
  1.1071 -  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
  1.1072 -
  1.1073 -fun full_simproc sg name ss =
  1.1074 -  full_mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
  1.1075 -fun full_simproc_i sg name = full_mk_simproc name o map (Thm.cterm_of sg);
  1.1076 -
  1.1077 -fun mk_simproc name lhss proc =
  1.1078 -  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, K proc, stamp ());
  1.1079 -
  1.1080 -fun simproc sg name ss =
  1.1081 -  mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
  1.1082 -fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg);
  1.1083 -
  1.1084 -fun rep_simproc (Simproc args) = args;
  1.1085 -
  1.1086 -
  1.1087 -
  1.1088 -(** solvers **)
  1.1089 -
  1.1090 -fun mk_solver name solver = Solver (name, solver, stamp());
  1.1091 -fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
  1.1092 -
  1.1093 -val merge_solvers = gen_merge_lists eq_solver;
  1.1094 -
  1.1095 -fun app_sols [] _ _ = no_tac
  1.1096 -  | app_sols (Solver(_,solver,_)::sols) thms i =
  1.1097 -       solver thms i ORELSE app_sols sols thms i;
  1.1098 -
  1.1099 -
  1.1100 -
  1.1101 -(** simplification sets **)
  1.1102 -
  1.1103 -(* type simpset *)
  1.1104 -
  1.1105 -fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
  1.1106 -  Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
  1.1107 -    loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
  1.1108 -
  1.1109 -fun from_mss mss = make_ss mss I (K (K no_tac)) [] [] [];
  1.1110 -
  1.1111 -val empty_ss = from_mss (set_mk_sym (empty_mss, Some o symmetric_fun));
  1.1112 -
  1.1113 -fun rep_ss (Simpset args) = args;
  1.1114 -fun prems_of_ss (Simpset {mss, ...}) = prems_of_mss mss;
  1.1115 -
  1.1116 -
  1.1117 -(* print simpsets *)
  1.1118 -
  1.1119 -fun print_ss ss =
  1.1120 -  let
  1.1121 -    val Simpset {mss, ...} = ss;
  1.1122 -    val {simps, procs, congs} = dest_mss mss;
  1.1123 -
  1.1124 -    val pretty_thms = map Display.pretty_thm;
  1.1125 -    fun pretty_proc (name, lhss) =
  1.1126 -      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
  1.1127 -  in
  1.1128 -    [Pretty.big_list "simplification rules:" (pretty_thms simps),
  1.1129 -      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
  1.1130 -      Pretty.big_list "congruences:" (pretty_thms congs)]
  1.1131 -    |> Pretty.chunks |> Pretty.writeln
  1.1132 -  end;
  1.1133 +fun ss settermless termless = ss |>
  1.1134 +  map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
  1.1135 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  1.1136  
  1.1137  
  1.1138 -(* extend simpsets *)
  1.1139 -
  1.1140 -fun (Simpset {mss, mk_cong, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
  1.1141 -    setsubgoaler subgoal_tac =
  1.1142 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1143 -
  1.1144 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
  1.1145 -    setloop tac =
  1.1146 -  make_ss mss mk_cong subgoal_tac [("", tac)] unsafe_solvers solvers;
  1.1147 +(* tactics *)
  1.1148  
  1.1149 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1150 -    addloop tac = make_ss mss mk_cong subgoal_tac
  1.1151 -      (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
  1.1152 -        warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac))
  1.1153 -      unsafe_solvers solvers;
  1.1154 -
  1.1155 -fun (ss as Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1156 - delloop name =
  1.1157 -  let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
  1.1158 -    if null del then (warning ("No such looper in simpset: " ^ name); ss)
  1.1159 -    else make_ss mss mk_cong subgoal_tac rest unsafe_solvers solvers
  1.1160 -  end;
  1.1161 +fun ss setsubgoaler subgoal_tac = ss |>
  1.1162 +  map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
  1.1163 +   (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
  1.1164  
  1.1165 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...})
  1.1166 -    setSSolver solver =
  1.1167 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers [solver];
  1.1168 -
  1.1169 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1170 -    addSSolver sol =
  1.1171 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers (merge_solvers solvers [sol]);
  1.1172 -
  1.1173 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
  1.1174 -    setSolver unsafe_solver =
  1.1175 -  make_ss mss mk_cong subgoal_tac loop_tacs [unsafe_solver] solvers;
  1.1176 +fun ss setloop tac = ss |>
  1.1177 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
  1.1178 +   (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
  1.1179  
  1.1180 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1181 -    addSolver sol =
  1.1182 -  make_ss mss mk_cong subgoal_tac loop_tacs (merge_solvers unsafe_solvers [sol]) solvers;
  1.1183 -
  1.1184 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1185 -    setmksimps mk_simps =
  1.1186 -  make_ss (set_mk_rews (mss, mk_simps)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1187 -
  1.1188 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1189 -    setmkeqTrue mk_eq_True =
  1.1190 -  make_ss (set_mk_eq_True (mss, mk_eq_True)) mk_cong subgoal_tac loop_tacs
  1.1191 -    unsafe_solvers solvers;
  1.1192 +fun ss addloop (name, tac) = ss |>
  1.1193 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  1.1194 +    (congs, procs, mk_rews, termless, subgoal_tac,
  1.1195 +      overwrite_warn (loop_tacs, (name, tac)) ("Overwriting looper " ^ quote name),
  1.1196 +      solvers));
  1.1197  
  1.1198 -fun (Simpset {mss, mk_cong = _, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1199 -    setmkcong mk_cong =
  1.1200 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1201 -
  1.1202 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1203 -    setmksym mksym =
  1.1204 -  make_ss (set_mk_sym (mss, mksym)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1205 +fun ss delloop name = ss |>
  1.1206 +  map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
  1.1207 +    let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
  1.1208 +      if null del then warning ("No such looper in simpset: " ^ quote name) else ();
  1.1209 +      (congs, procs, mk_rews, termless, subgoal_tac, rest, solvers)
  1.1210 +    end);
  1.1211  
  1.1212 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
  1.1213 -    settermless termless =
  1.1214 -  make_ss (set_termless (mss, termless)) mk_cong subgoal_tac loop_tacs
  1.1215 -    unsafe_solvers solvers;
  1.1216 -
  1.1217 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1218 -    addsimps rews =
  1.1219 -  make_ss (add_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1220 -
  1.1221 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1222 -    delsimps rews =
  1.1223 -  make_ss (del_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1224 +fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  1.1225 +  subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
  1.1226 +    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
  1.1227  
  1.1228 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1229 -    addeqcongs newcongs =
  1.1230 -  make_ss (add_congs (mss, newcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1231 +fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  1.1232 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  1.1233 +    subgoal_tac, loop_tacs, (unsafe_solvers, merge_solvers solvers [solver])));
  1.1234  
  1.1235 -fun (Simpset {mss, subgoal_tac, mk_cong, loop_tacs, unsafe_solvers, solvers})
  1.1236 -    deleqcongs oldcongs =
  1.1237 -  make_ss (del_congs (mss, oldcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
  1.1238 -
  1.1239 -fun (ss as Simpset {mk_cong, ...}) addcongs newcongs =
  1.1240 -  ss addeqcongs map mk_cong newcongs;
  1.1241 +fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  1.1242 +  subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
  1.1243 +    subgoal_tac, loop_tacs, ([solver], solvers)));
  1.1244  
  1.1245 -fun (ss as Simpset {mk_cong, ...}) delcongs oldcongs =
  1.1246 -  ss deleqcongs map mk_cong oldcongs;
  1.1247 -
  1.1248 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1249 -    addsimprocs simprocs =
  1.1250 -  make_ss (add_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac loop_tacs
  1.1251 -    unsafe_solvers solvers;
  1.1252 +fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
  1.1253 +  subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
  1.1254 +    subgoal_tac, loop_tacs, (merge_solvers unsafe_solvers [solver], solvers)));
  1.1255  
  1.1256 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
  1.1257 -    delsimprocs simprocs =
  1.1258 -  make_ss (del_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac
  1.1259 -    loop_tacs unsafe_solvers solvers;
  1.1260 -
  1.1261 -fun clear_ss (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
  1.1262 -  make_ss (clear_mss mss) mk_cong subgoal_tac [] unsafe_solvers solvers;
  1.1263 +fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
  1.1264 +  subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
  1.1265 +  subgoal_tac, loop_tacs, (solvers, solvers)));
  1.1266  
  1.1267  
  1.1268 -(* merge simpsets *)
  1.1269 -
  1.1270 -(*ignores subgoal_tac of 2nd simpset!*)
  1.1271 -
  1.1272 -fun merge_ss
  1.1273 -   (Simpset {mss = mss1, mk_cong, loop_tacs = loop_tacs1, subgoal_tac,
  1.1274 -             unsafe_solvers = unsafe_solvers1, solvers = solvers1},
  1.1275 -    Simpset {mss = mss2, mk_cong = _, loop_tacs = loop_tacs2, subgoal_tac = _,
  1.1276 -             unsafe_solvers = unsafe_solvers2, solvers = solvers2}) =
  1.1277 -  make_ss (merge_mss (mss1, mss2)) mk_cong subgoal_tac
  1.1278 -    (merge_alists loop_tacs1 loop_tacs2)
  1.1279 -    (merge_solvers unsafe_solvers1 unsafe_solvers2)
  1.1280 -    (merge_solvers solvers1 solvers2);
  1.1281  
  1.1282  (** rewriting **)
  1.1283  
  1.1284 @@ -796,76 +699,89 @@
  1.1285      Science of Computer Programming 3 (1983), pages 119-149.
  1.1286  *)
  1.1287  
  1.1288 -val dest_eq = Drule.dest_equals o cprop_of;
  1.1289 -val lhs_of = fst o dest_eq;
  1.1290 -val rhs_of = snd o dest_eq;
  1.1291 +val dest_eq = Drule.dest_equals o Thm.cprop_of;
  1.1292 +val lhs_of = #1 o dest_eq;
  1.1293 +val rhs_of = #2 o dest_eq;
  1.1294  
  1.1295  fun check_conv msg thm thm' =
  1.1296    let
  1.1297      val thm'' = transitive thm (transitive
  1.1298        (symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm')
  1.1299 -  in (if msg then trace_thm "SUCCEEDED" thm' else (); Some thm'') end
  1.1300 +  in if msg then trace_thm "SUCCEEDED" thm' else (); Some thm'' end
  1.1301    handle THM _ =>
  1.1302 -    let val {sign, prop = _ $ _ $ prop0, ...} = rep_thm thm;
  1.1303 -    in
  1.1304 -      (trace_thm "Proved wrong thm (Check subgoaler?)" thm';
  1.1305 -       trace_term false "Should have proved:" sign prop0;
  1.1306 -       None)
  1.1307 +    let val {sign, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
  1.1308 +      trace_thm "Proved wrong thm (Check subgoaler?)" thm';
  1.1309 +      trace_term false "Should have proved:" sign prop0;
  1.1310 +      None
  1.1311      end;
  1.1312  
  1.1313  
  1.1314  (* mk_procrule *)
  1.1315  
  1.1316  fun mk_procrule thm =
  1.1317 -  let val (_,prems,lhs,elhs,rhs,_) = decomp_simp thm
  1.1318 -  in if rewrite_rule_extra_vars prems lhs rhs
  1.1319 -     then (prthm true "Extra vars on rhs:" thm; [])
  1.1320 -     else [mk_rrule2{thm=thm, name="", lhs=lhs, elhs=elhs, perm=false}]
  1.1321 +  let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
  1.1322 +    if rewrite_rule_extra_vars prems lhs rhs
  1.1323 +    then (warn_thm "Extra vars on rhs:" thm; [])
  1.1324 +    else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
  1.1325    end;
  1.1326  
  1.1327  
  1.1328 -(* conversion to apply the meta simpset to a term *)
  1.1329 +(* rewritec: conversion to apply the meta simpset to a term *)
  1.1330  
  1.1331 -(* Since the rewriting strategy is bottom-up, we avoid re-normalizing already
  1.1332 -   normalized terms by carrying around the rhs of the rewrite rule just
  1.1333 -   applied. This is called the `skeleton'. It is decomposed in parallel
  1.1334 -   with the term. Once a Var is encountered, the corresponding term is
  1.1335 -   already in normal form.
  1.1336 -   skel0 is a dummy skeleton that is to enforce complete normalization.
  1.1337 -*)
  1.1338 +(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
  1.1339 +  normalized terms by carrying around the rhs of the rewrite rule just
  1.1340 +  applied. This is called the `skeleton'. It is decomposed in parallel
  1.1341 +  with the term. Once a Var is encountered, the corresponding term is
  1.1342 +  already in normal form.
  1.1343 +  skel0 is a dummy skeleton that is to enforce complete normalization.*)
  1.1344 +
  1.1345  val skel0 = Bound 0;
  1.1346  
  1.1347 -(* Use rhs as skeleton only if the lhs does not contain unnormalized bits.
  1.1348 -   The latter may happen iff there are weak congruence rules for constants
  1.1349 -   in the lhs.
  1.1350 -*)
  1.1351 -fun uncond_skel((_,weak),(lhs,rhs)) =
  1.1352 -  if null weak then rhs (* optimization *)
  1.1353 -  else if exists_Const (fn (c,_) => c mem weak) lhs then skel0
  1.1354 -       else rhs;
  1.1355 +(*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
  1.1356 +  The latter may happen iff there are weak congruence rules for constants
  1.1357 +  in the lhs.*)
  1.1358  
  1.1359 -(* Behaves like unconditional rule if rhs does not contain vars not in the lhs.
  1.1360 -   Otherwise those vars may become instantiated with unnormalized terms
  1.1361 -   while the premises are solved.
  1.1362 -*)
  1.1363 -fun cond_skel(args as (congs,(lhs,rhs))) =
  1.1364 -  if term_varnames rhs subset term_varnames lhs then uncond_skel(args)
  1.1365 +fun uncond_skel ((_, weak), (lhs, rhs)) =
  1.1366 +  if null weak then rhs  (*optimization*)
  1.1367 +  else if exists_Const (fn (c, _) => c mem weak) lhs then skel0
  1.1368 +  else rhs;
  1.1369 +
  1.1370 +(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
  1.1371 +  Otherwise those vars may become instantiated with unnormalized terms
  1.1372 +  while the premises are solved.*)
  1.1373 +
  1.1374 +fun cond_skel (args as (congs, (lhs, rhs))) =
  1.1375 +  if term_varnames rhs subset term_varnames lhs then uncond_skel args
  1.1376    else skel0;
  1.1377  
  1.1378 +fun incr_depth ss =
  1.1379 +  let
  1.1380 +    val ss' = ss |> map_simpset1 (fn (rules, prems, bounds, depth) =>
  1.1381 +      (rules, prems, bounds, depth + 1));
  1.1382 +    val Simpset ({depth = depth', ...}, _) = ss';
  1.1383 +  in
  1.1384 +    if depth' > ! simp_depth_limit
  1.1385 +    then (warning "simp_depth_limit exceeded - giving up"; None)
  1.1386 +    else
  1.1387 +     (if depth' mod 10 = 0
  1.1388 +      then warning ("Simplification depth " ^ string_of_int depth')
  1.1389 +      else ();
  1.1390 +      Some ss')
  1.1391 +  end;
  1.1392 +
  1.1393  (*
  1.1394 -  we try in order:
  1.1395 +  Rewriting -- we try in order:
  1.1396      (1) beta reduction
  1.1397      (2) unconditional rewrite rules
  1.1398      (3) conditional rewrite rules
  1.1399      (4) simplification procedures
  1.1400  
  1.1401    IMPORTANT: rewrite rules must not introduce new Vars or TVars!
  1.1402 -
  1.1403  *)
  1.1404  
  1.1405 -fun rewritec (prover, signt, maxt)
  1.1406 -             (ss as Simpset{mss=mss as Mss{rules, procs, termless, prems, congs, depth,...},...}) t =
  1.1407 +fun rewritec (prover, signt, maxt) ss t =
  1.1408    let
  1.1409 +    val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
  1.1410      val eta_thm = Thm.eta_conversion t;
  1.1411      val eta_t' = rhs_of eta_thm;
  1.1412      val eta_t = term_of eta_t';
  1.1413 @@ -874,7 +790,7 @@
  1.1414        let
  1.1415          val {sign, prop, maxidx, ...} = rep_thm thm;
  1.1416          val _ = if Sign.subsig (sign, signt) then ()
  1.1417 -                else (prthm true "Ignoring rewrite rule from different theory:" thm;
  1.1418 +                else (warn_thm "Ignoring rewrite rule from different theory:" thm;
  1.1419                        raise Pattern.MATCH);
  1.1420          val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
  1.1421            else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
  1.1422 @@ -897,11 +813,11 @@
  1.1423                in Some (thm'', uncond_skel (congs, lr)) end)
  1.1424             else
  1.1425               (trace_thm "Trying to rewrite:" thm';
  1.1426 -              case incr_depth mss of
  1.1427 +              case incr_depth ss of
  1.1428                  None => (trace_thm "FAILED - reached depth limit" thm'; None)
  1.1429 -              | Some mss =>
  1.1430 -              (case prover mss thm' of
  1.1431 -                None       => (trace_thm "FAILED" thm'; None)
  1.1432 +              | Some ss' =>
  1.1433 +              (case prover ss' thm' of
  1.1434 +                None => (trace_thm "FAILED" thm'; None)
  1.1435                | Some thm2 =>
  1.1436                    (case check_conv true eta_thm thm2 of
  1.1437                       None => None |
  1.1438 @@ -926,12 +842,12 @@
  1.1439                                       else sort rrs (re1,rr::re2)
  1.1440      in sort rrs ([],[]) end
  1.1441  
  1.1442 -    fun proc_rews ([]:meta_simproc list) = None
  1.1443 -      | proc_rews ({name, proc, lhs, ...} :: ps) =
  1.1444 -          if Pattern.matches tsigt (term_of lhs, term_of t) then
  1.1445 +    fun proc_rews [] = None
  1.1446 +      | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
  1.1447 +          if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then
  1.1448              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
  1.1449               case transform_failure (curry SIMPROC_FAIL name)
  1.1450 -                 (fn () => proc ss signt prems eta_t) () of
  1.1451 +                 (fn () => proc signt ss eta_t) () of
  1.1452                 None => (debug false "FAILED"; proc_rews ps)
  1.1453               | Some raw_thm =>
  1.1454                   (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
  1.1455 @@ -983,49 +899,45 @@
  1.1456  fun transitive2 thm = transitive1 (Some thm);
  1.1457  fun transitive3 thm = transitive1 thm o Some;
  1.1458  
  1.1459 -fun replace_mss (Simpset{mss=_,mk_cong,subgoal_tac,loop_tacs,unsafe_solvers,solvers}) mss_new =
  1.1460 -    Simpset{mss=mss_new,mk_cong=mk_cong,subgoal_tac=subgoal_tac,loop_tacs=loop_tacs,
  1.1461 -	    unsafe_solvers=unsafe_solvers,solvers=solvers};
  1.1462 -
  1.1463 -fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) (ss as Simpset{mss,...}) =
  1.1464 +fun bottomc ((simprem, useprem, mutsimp), prover, sign, maxidx) =
  1.1465    let
  1.1466 -    fun botc skel mss t =
  1.1467 +    fun botc skel ss t =
  1.1468            if is_Var skel then None
  1.1469            else
  1.1470 -          (case subc skel mss t of
  1.1471 +          (case subc skel ss t of
  1.1472               some as Some thm1 =>
  1.1473 -               (case rewritec (prover, sign, maxidx) (replace_mss ss mss) (rhs_of thm1) of
  1.1474 +               (case rewritec (prover, sign, maxidx) ss (rhs_of thm1) of
  1.1475                    Some (thm2, skel2) =>
  1.1476                      transitive2 (transitive thm1 thm2)
  1.1477 -                      (botc skel2 mss (rhs_of thm2))
  1.1478 +                      (botc skel2 ss (rhs_of thm2))
  1.1479                  | None => some)
  1.1480             | None =>
  1.1481 -               (case rewritec (prover, sign, maxidx) (replace_mss ss mss) t of
  1.1482 +               (case rewritec (prover, sign, maxidx) ss t of
  1.1483                    Some (thm2, skel2) => transitive2 thm2
  1.1484 -                    (botc skel2 mss (rhs_of thm2))
  1.1485 +                    (botc skel2 ss (rhs_of thm2))
  1.1486                  | None => None))
  1.1487  
  1.1488 -    and try_botc mss t =
  1.1489 -          (case botc skel0 mss t of
  1.1490 +    and try_botc ss t =
  1.1491 +          (case botc skel0 ss t of
  1.1492               Some trec1 => trec1 | None => (reflexive t))
  1.1493  
  1.1494 -    and subc skel
  1.1495 -          (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless,depth}) t0 =
  1.1496 +    and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
  1.1497         (case term_of t0 of
  1.1498             Abs (a, T, t) =>
  1.1499 -             let val b = variant bounds a
  1.1500 -                 val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0
  1.1501 -                 val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless,depth)
  1.1502 -                 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0
  1.1503 -             in case botc skel' mss' t' of
  1.1504 +             let
  1.1505 +                 val b = variant bounds a;
  1.1506 +                 val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0;
  1.1507 +                 val ss' = add_bound b ss;
  1.1508 +                 val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
  1.1509 +             in case botc skel' ss' t' of
  1.1510                    Some thm => Some (abstract_rule a v thm)
  1.1511                  | None => None
  1.1512               end
  1.1513           | t $ _ => (case t of
  1.1514 -             Const ("==>", _) $ _  => impc t0 mss
  1.1515 +             Const ("==>", _) $ _  => impc t0 ss
  1.1516             | Abs _ =>
  1.1517                 let val thm = beta_conversion false t0
  1.1518 -               in case subc skel0 mss (rhs_of thm) of
  1.1519 +               in case subc skel0 ss (rhs_of thm) of
  1.1520                      None => Some thm
  1.1521                    | Some thm' => Some (transitive thm thm')
  1.1522                 end
  1.1523 @@ -1037,13 +949,13 @@
  1.1524                           | _ => (skel0, skel0);
  1.1525                         val (ct, cu) = Thm.dest_comb t0
  1.1526                       in
  1.1527 -                     (case botc tskel mss ct of
  1.1528 +                     (case botc tskel ss ct of
  1.1529                          Some thm1 =>
  1.1530 -                          (case botc uskel mss cu of
  1.1531 +                          (case botc uskel ss cu of
  1.1532                               Some thm2 => Some (combination thm1 thm2)
  1.1533                             | None => Some (combination thm1 (reflexive cu)))
  1.1534                        | None =>
  1.1535 -                          (case botc uskel mss cu of
  1.1536 +                          (case botc uskel ss cu of
  1.1537                               Some thm1 => Some (combination (reflexive ct) thm1)
  1.1538                             | None => None))
  1.1539                       end
  1.1540 @@ -1053,16 +965,16 @@
  1.1541                        (case assoc_string (fst congs, a) of
  1.1542                           None => appc ()
  1.1543                         | Some cong =>
  1.1544 -(* post processing: some partial applications h t1 ... tj, j <= length ts,
  1.1545 -   may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
  1.1546 +  (*post processing: some partial applications h t1 ... tj, j <= length ts,
  1.1547 +    may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
  1.1548                            (let
  1.1549 -                             val thm = congc (prover mss, sign, maxidx) cong t0;
  1.1550 +                             val thm = congc (prover ss, sign, maxidx) cong t0;
  1.1551                               val t = if_none (apsome rhs_of thm) t0;
  1.1552                               val (cl, cr) = Thm.dest_comb t
  1.1553                               val dVar = Var(("", 0), dummyT)
  1.1554                               val skel =
  1.1555                                 list_comb (h, replicate (length ts) dVar)
  1.1556 -                           in case botc skel mss cl of
  1.1557 +                           in case botc skel ss cl of
  1.1558                                  None => thm
  1.1559                                | Some thm' => transitive3 thm
  1.1560                                    (combination thm' (reflexive cr))
  1.1561 @@ -1072,19 +984,19 @@
  1.1562                 end)
  1.1563           | _ => None)
  1.1564  
  1.1565 -    and impc ct mss =
  1.1566 -      if mutsimp then mut_impc0 [] ct [] [] mss else nonmut_impc ct mss
  1.1567 +    and impc ct ss =
  1.1568 +      if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
  1.1569  
  1.1570 -    and rules_of_prem mss prem =
  1.1571 +    and rules_of_prem ss prem =
  1.1572        if maxidx_of_term (term_of prem) <> ~1
  1.1573        then (trace_cterm true
  1.1574          "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], None))
  1.1575        else
  1.1576          let val asm = assume prem
  1.1577 -        in (extract_safe_rrules (mss, asm), Some asm) end
  1.1578 +        in (extract_safe_rrules (ss, asm), Some asm) end
  1.1579  
  1.1580 -    and add_rrules (rrss, asms) mss =
  1.1581 -      add_prems (foldl (insert_rrule true) (mss, flat rrss), mapfilter I asms)
  1.1582 +    and add_rrules (rrss, asms) ss =
  1.1583 +      foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
  1.1584  
  1.1585      and disch r (prem, eq) =
  1.1586        let
  1.1587 @@ -1105,42 +1017,42 @@
  1.1588        end
  1.1589  
  1.1590      and rebuild [] _ _ _ _ eq = eq
  1.1591 -      | rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) mss eq =
  1.1592 +      | rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) ss eq =
  1.1593            let
  1.1594 -            val mss' = add_rrules (rev rrss, rev asms) mss;
  1.1595 +            val ss' = add_rrules (rev rrss, rev asms) ss;
  1.1596              val concl' =
  1.1597                Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl);
  1.1598              val dprem = apsome (curry (disch false) prem)
  1.1599 -          in case rewritec (prover, sign, maxidx) (replace_mss ss mss') concl' of
  1.1600 -              None => rebuild prems concl' rrss asms mss (dprem eq)
  1.1601 +          in case rewritec (prover, sign, maxidx) ss' concl' of
  1.1602 +              None => rebuild prems concl' rrss asms ss (dprem eq)
  1.1603              | Some (eq', _) => transitive2 (foldl (disch false o swap)
  1.1604                    (the (transitive3 (dprem eq) eq'), prems))
  1.1605 -                (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) mss)
  1.1606 +                (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss)
  1.1607            end
  1.1608 -          
  1.1609 -    and mut_impc0 prems concl rrss asms mss =
  1.1610 +
  1.1611 +    and mut_impc0 prems concl rrss asms ss =
  1.1612        let
  1.1613          val prems' = strip_imp_prems concl;
  1.1614 -        val (rrss', asms') = split_list (map (rules_of_prem mss) prems')
  1.1615 +        val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
  1.1616        in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
  1.1617 -        (asms @ asms') [] [] [] [] mss ~1 ~1
  1.1618 +        (asms @ asms') [] [] [] [] ss ~1 ~1
  1.1619        end
  1.1620 - 
  1.1621 -    and mut_impc [] concl [] [] prems' rrss' asms' eqns mss changed k =
  1.1622 +
  1.1623 +    and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
  1.1624          transitive1 (foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
  1.1625              (apsome (curry (disch false) prem) eq2)) (None, eqns ~~ prems'))
  1.1626            (if changed > 0 then
  1.1627               mut_impc (rev prems') concl (rev rrss') (rev asms')
  1.1628 -               [] [] [] [] mss ~1 changed
  1.1629 -           else rebuild prems' concl rrss' asms' mss
  1.1630 -             (botc skel0 (add_rrules (rev rrss', rev asms') mss) concl))
  1.1631 +               [] [] [] [] ss ~1 changed
  1.1632 +           else rebuild prems' concl rrss' asms' ss
  1.1633 +             (botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
  1.1634  
  1.1635        | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
  1.1636 -          prems' rrss' asms' eqns mss changed k =
  1.1637 +          prems' rrss' asms' eqns ss changed k =
  1.1638          case (if k = 0 then None else botc skel0 (add_rrules
  1.1639 -          (rev rrss' @ rrss, rev asms' @ asms) mss) prem) of
  1.1640 +          (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
  1.1641              None => mut_impc prems concl rrss asms (prem :: prems')
  1.1642 -              (rrs :: rrss') (asm :: asms') (None :: eqns) mss changed
  1.1643 +              (rrs :: rrss') (asm :: asms') (None :: eqns) ss changed
  1.1644                (if k = 0 then 0 else k - 1)
  1.1645            | Some eqn =>
  1.1646              let
  1.1647 @@ -1148,21 +1060,21 @@
  1.1648                val tprems = map term_of prems;
  1.1649                val i = 1 + foldl Int.max (~1, map (fn p =>
  1.1650                  find_index_eq p tprems) (#hyps (rep_thm eqn)));
  1.1651 -              val (rrs', asm') = rules_of_prem mss prem'
  1.1652 +              val (rrs', asm') = rules_of_prem ss prem'
  1.1653              in mut_impc prems concl rrss asms (prem' :: prems')
  1.1654                (rrs' :: rrss') (asm' :: asms') (Some (foldr (disch true)
  1.1655                  (take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
  1.1656 -                  (drop (i, prems), concl))))) :: eqns) mss (length prems') ~1
  1.1657 +                  (drop (i, prems), concl))))) :: eqns) ss (length prems') ~1
  1.1658              end
  1.1659  
  1.1660 -     (* legacy code - only for backwards compatibility *)
  1.1661 -     and nonmut_impc ct mss =
  1.1662 +     (*legacy code - only for backwards compatibility*)
  1.1663 +     and nonmut_impc ct ss =
  1.1664         let val (prem, conc) = dest_implies ct;
  1.1665 -           val thm1 = if simprem then botc skel0 mss prem else None;
  1.1666 +           val thm1 = if simprem then botc skel0 ss prem else None;
  1.1667             val prem1 = if_none (apsome rhs_of thm1) prem;
  1.1668 -           val mss1 = if not useprem then mss else add_rrules
  1.1669 -             (apsnd single (apfst single (rules_of_prem mss prem1))) mss
  1.1670 -       in (case botc skel0 mss1 conc of
  1.1671 +           val ss1 = if not useprem then ss else add_rrules
  1.1672 +             (apsnd single (apfst single (rules_of_prem ss prem1))) ss
  1.1673 +       in (case botc skel0 ss1 conc of
  1.1674             None => (case thm1 of
  1.1675                 None => None
  1.1676               | Some thm1' => Some (Drule.imp_cong' thm1' (reflexive conc)))
  1.1677 @@ -1175,10 +1087,10 @@
  1.1678             end)
  1.1679         end
  1.1680  
  1.1681 - in try_botc mss end;
  1.1682 + in try_botc end;
  1.1683  
  1.1684  
  1.1685 -(*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***)
  1.1686 +(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
  1.1687  
  1.1688  (*
  1.1689    Parameters:
  1.1690 @@ -1186,87 +1098,81 @@
  1.1691              use A in simplifying B,
  1.1692              use prems of B (if B is again a meta-impl.) to simplify A)
  1.1693             when simplifying A ==> B
  1.1694 -    mss: contains equality theorems of the form [|p1,...|] ==> t==u
  1.1695      prover: how to solve premises in conditional rewrites and congruences
  1.1696  *)
  1.1697  
  1.1698 -fun rewrite_cterm mode prover (ss as Simpset{mss,...}) ct =
  1.1699 -  let val {sign, t, maxidx, ...} = rep_cterm ct
  1.1700 -      val Mss{depth, ...} = mss
  1.1701 -  in trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
  1.1702 -     simp_depth := depth;
  1.1703 -     bottomc (mode, prover, sign, maxidx) ss ct
  1.1704 -  end
  1.1705 -  handle THM (s, _, thms) =>
  1.1706 +fun rewrite_cterm mode prover ss ct =
  1.1707 +  let
  1.1708 +    val Simpset ({depth, ...}, _) = ss;
  1.1709 +    val {sign, t, maxidx, ...} = Thm.rep_cterm ct;
  1.1710 +  in
  1.1711 +    trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
  1.1712 +    simp_depth := depth;
  1.1713 +    bottomc (mode, prover, sign, maxidx) ss ct
  1.1714 +  end handle THM (s, _, thms) =>
  1.1715      error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
  1.1716        Pretty.string_of (Display.pretty_thms thms));
  1.1717  
  1.1718 -val ss_of = from_mss o mss_of
  1.1719 -
  1.1720  (*Rewrite a cterm*)
  1.1721  fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct)
  1.1722 -  | rewrite_aux prover full thms = rewrite_cterm (full, false, false) prover (ss_of thms);
  1.1723 +  | rewrite_aux prover full thms =
  1.1724 +      rewrite_cterm (full, false, false) prover (empty_ss addsimps thms);
  1.1725  
  1.1726  (*Rewrite a theorem*)
  1.1727  fun simplify_aux _ _ [] = (fn th => th)
  1.1728    | simplify_aux prover full thms =
  1.1729 -      Drule.fconv_rule (rewrite_cterm (full, false, false) prover (ss_of thms));
  1.1730 +      Drule.fconv_rule (rewrite_cterm (full, false, false) prover (empty_ss addsimps thms));
  1.1731  
  1.1732 -fun rewrite_thm mode prover mss = Drule.fconv_rule (rewrite_cterm mode prover mss);
  1.1733 +(*simple term rewriting -- no proof*)
  1.1734 +fun rewrite_term sg rules procs =
  1.1735 +  Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
  1.1736 +
  1.1737 +fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
  1.1738  
  1.1739  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
  1.1740  fun rewrite_goals_rule_aux _ []   th = th
  1.1741    | rewrite_goals_rule_aux prover thms th =
  1.1742        Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, false) prover
  1.1743 -        (ss_of thms))) th;
  1.1744 +        (empty_ss addsimps thms))) th;
  1.1745  
  1.1746 -(*Rewrite the subgoal of a proof state (represented by a theorem) *)
  1.1747 +(*Rewrite the subgoal of a proof state (represented by a theorem)*)
  1.1748  fun rewrite_goal_rule mode prover ss i thm =
  1.1749    if 0 < i  andalso  i <= nprems_of thm
  1.1750    then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm
  1.1751    else raise THM("rewrite_goal_rule",i,[thm]);
  1.1752  
  1.1753 -
  1.1754 -(*simple term rewriting -- without proofs*)
  1.1755 -fun rewrite_term sg rules procs =
  1.1756 -  Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
  1.1757 +(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
  1.1758 +fun asm_rewrite_goal_tac mode prover_tac ss =
  1.1759 +  SELECT_GOAL
  1.1760 +    (PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) ss 1));
  1.1761  
  1.1762 -(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
  1.1763 -fun asm_rewrite_goal_tac mode prover_tac mss =
  1.1764 -  SELECT_GOAL
  1.1765 -    (PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) mss 1));
  1.1766 +
  1.1767  
  1.1768 -(** simplification tactics **)
  1.1769 +(** simplification tactics and rules **)
  1.1770  
  1.1771 -fun solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers) mss =
  1.1772 +fun solve_all_tac solvers ss =
  1.1773    let
  1.1774 -    val ss =
  1.1775 -      make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers unsafe_solvers;
  1.1776 -    val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
  1.1777 -  in DEPTH_SOLVE solve1_tac end;
  1.1778 -
  1.1779 -fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
  1.1780 +    val Simpset (_, {subgoal_tac, ...}) = ss;
  1.1781 +    val solve_tac = subgoal_tac (set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
  1.1782 +  in DEPTH_SOLVE (solve_tac 1) end;
  1.1783  
  1.1784 -(*note: may instantiate unknowns that appear also in other subgoals*)
  1.1785 -fun generic_simp_tac safe mode =
  1.1786 -  fn (ss as Simpset {mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
  1.1787 -    let
  1.1788 -      val solvs = app_sols (if safe then solvers else unsafe_solvers);
  1.1789 -      fun simp_loop_tac i =
  1.1790 -        asm_rewrite_goal_tac mode
  1.1791 -          (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
  1.1792 -          ss i
  1.1793 -        THEN (solvs (prems_of_ss ss) i ORELSE
  1.1794 -              TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
  1.1795 -    in simp_loop_tac end;
  1.1796 +(*NOTE: may instantiate unknowns that appear also in other subgoals*)
  1.1797 +fun generic_simp_tac safe mode ss =
  1.1798 +  let
  1.1799 +    val Simpset ({prems, ...}, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = ss;
  1.1800 +    val loop_tac = FIRST' (map #2 loop_tacs);
  1.1801 +    val solve_tac = FIRST' (map (solver prems) (if safe then solvers else unsafe_solvers));
  1.1802  
  1.1803 -(** simplification rules and conversions **)
  1.1804 +    fun simp_loop_tac i =
  1.1805 +      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
  1.1806 +      (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
  1.1807 +  in simp_loop_tac end;
  1.1808  
  1.1809 -fun simp rew mode
  1.1810 -     (ss as Simpset {mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
  1.1811 +fun simp rew mode ss thm =
  1.1812    let
  1.1813 -    val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
  1.1814 -    fun prover m th = apsome fst (Seq.pull (tacf m th));
  1.1815 +    val Simpset (_, {solvers = (unsafe_solvers, _), ...}) = ss;
  1.1816 +    val tacf = solve_all_tac unsafe_solvers;
  1.1817 +    fun prover s th = apsome #1 (Seq.pull (tacf s th));
  1.1818    in rew mode prover ss thm end;
  1.1819  
  1.1820  val simp_thm = simp rewrite_thm;