Merging the meta-simplifier with the Provers-simplifier. Next step:
authorskalberg
Fri Jun 25 14:30:55 2004 +0200 (2004-06-25)
changeset 15006107e4dfd3b96
parent 15005 546c8e7e28d4
child 15007 0628f38bcbcf
Merging the meta-simplifier with the Provers-simplifier. Next step:
make the simplification procedure simpset-aware.
src/Provers/simplifier.ML
src/Pure/ROOT.ML
src/Pure/meta_simplifier.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
     1.1 --- a/src/Provers/simplifier.ML	Thu Jun 24 17:54:53 2004 +0200
     1.2 +++ b/src/Provers/simplifier.ML	Fri Jun 25 14:30:55 2004 +0200
     1.3 @@ -6,19 +6,14 @@
     1.4  for the actual meta-level rewriting engine.
     1.5  *)
     1.6  
     1.7 -infix 4
     1.8 -  setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
     1.9 -  addSolver addsimps delsimps addeqcongs deleqcongs addcongs delcongs
    1.10 -  setmksimps setmkeqTrue setmkcong setmksym settermless addsimprocs delsimprocs;
    1.11 -
    1.12  signature BASIC_SIMPLIFIER =
    1.13  sig
    1.14 -  type simproc
    1.15 +  type simproc = MetaSimplifier.simproc
    1.16    val mk_simproc: string -> cterm list
    1.17      -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.18 -  type solver
    1.19 +  type solver = MetaSimplifier.solver
    1.20    val mk_solver: string -> (thm list -> int -> tactic) -> solver
    1.21 -  type simpset
    1.22 +  type simpset = MetaSimplifier.simpset
    1.23    val empty_ss: simpset
    1.24    val rep_ss: simpset ->
    1.25     {mss: MetaSimplifier.meta_simpset,
    1.26 @@ -121,195 +116,8 @@
    1.27  structure Simplifier: SIMPLIFIER =
    1.28  struct
    1.29  
    1.30 -
    1.31 -(** simplification procedures **)
    1.32 -
    1.33 -(* datatype simproc *)
    1.34 -
    1.35 -datatype simproc =
    1.36 -  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
    1.37 -
    1.38 -fun mk_simproc name lhss proc =
    1.39 -  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
    1.40 -
    1.41 -fun simproc sg name ss =
    1.42 -  mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
    1.43 -fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg);
    1.44 -
    1.45 -fun rep_simproc (Simproc args) = args;
    1.46 -
    1.47 -
    1.48 -
    1.49 -(** solvers **)
    1.50 -
    1.51 -datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
    1.52 -
    1.53 -fun mk_solver name solver = Solver (name, solver, stamp());
    1.54 -fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
    1.55 -
    1.56 -val merge_solvers = gen_merge_lists eq_solver;
    1.57 -
    1.58 -fun app_sols [] _ _ = no_tac
    1.59 -  | app_sols (Solver(_,solver,_)::sols) thms i =
    1.60 -       solver thms i ORELSE app_sols sols thms i;
    1.61 -
    1.62 -
    1.63 -
    1.64 -(** simplification sets **)
    1.65 -
    1.66 -(* type simpset *)
    1.67 -
    1.68 -datatype simpset =
    1.69 -  Simpset of {
    1.70 -    mss: MetaSimplifier.meta_simpset,
    1.71 -    mk_cong: thm -> thm,
    1.72 -    subgoal_tac: simpset -> int -> tactic,
    1.73 -    loop_tacs: (string * (int -> tactic)) list,
    1.74 -    unsafe_solvers: solver list,
    1.75 -    solvers: solver list};
    1.76 -
    1.77 -fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
    1.78 -  Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
    1.79 -    loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
    1.80 -
    1.81 -val empty_ss =
    1.82 -  let val mss = MetaSimplifier.set_mk_sym (MetaSimplifier.empty_mss, Some o symmetric_fun)
    1.83 -  in make_ss mss I (K (K no_tac)) [] [] [] end;
    1.84 -
    1.85 -fun rep_ss (Simpset args) = args;
    1.86 -fun prems_of_ss (Simpset {mss, ...}) = MetaSimplifier.prems_of_mss mss;
    1.87 -
    1.88 -
    1.89 -(* print simpsets *)
    1.90 -
    1.91 -fun print_ss ss =
    1.92 -  let
    1.93 -    val Simpset {mss, ...} = ss;
    1.94 -    val {simps, procs, congs} = MetaSimplifier.dest_mss mss;
    1.95 -
    1.96 -    val pretty_thms = map Display.pretty_thm;
    1.97 -    fun pretty_proc (name, lhss) =
    1.98 -      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
    1.99 -  in
   1.100 -    [Pretty.big_list "simplification rules:" (pretty_thms simps),
   1.101 -      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
   1.102 -      Pretty.big_list "congruences:" (pretty_thms congs)]
   1.103 -    |> Pretty.chunks |> Pretty.writeln
   1.104 -  end;
   1.105 -
   1.106 -
   1.107 -(* extend simpsets *)
   1.108 -
   1.109 -fun (Simpset {mss, mk_cong, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
   1.110 -    setsubgoaler subgoal_tac =
   1.111 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.112 -
   1.113 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
   1.114 -    setloop tac =
   1.115 -  make_ss mss mk_cong subgoal_tac [("", tac)] unsafe_solvers solvers;
   1.116 -
   1.117 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.118 -    addloop tac = make_ss mss mk_cong subgoal_tac
   1.119 -      (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
   1.120 -        warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac))
   1.121 -      unsafe_solvers solvers;
   1.122 -
   1.123 -fun (ss as Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.124 - delloop name =
   1.125 -  let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
   1.126 -    if null del then (warning ("No such looper in simpset: " ^ name); ss)
   1.127 -    else make_ss mss mk_cong subgoal_tac rest unsafe_solvers solvers
   1.128 -  end;
   1.129 -
   1.130 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...})
   1.131 -    setSSolver solver =
   1.132 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers [solver];
   1.133 -
   1.134 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.135 -    addSSolver sol =
   1.136 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers (merge_solvers solvers [sol]);
   1.137 -
   1.138 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
   1.139 -    setSolver unsafe_solver =
   1.140 -  make_ss mss mk_cong subgoal_tac loop_tacs [unsafe_solver] solvers;
   1.141 -
   1.142 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.143 -    addSolver sol =
   1.144 -  make_ss mss mk_cong subgoal_tac loop_tacs (merge_solvers unsafe_solvers [sol]) solvers;
   1.145 -
   1.146 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.147 -    setmksimps mk_simps =
   1.148 -  make_ss (MetaSimplifier.set_mk_rews (mss, mk_simps)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.149 -
   1.150 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.151 -    setmkeqTrue mk_eq_True =
   1.152 -  make_ss (MetaSimplifier.set_mk_eq_True (mss, mk_eq_True)) mk_cong subgoal_tac loop_tacs
   1.153 -    unsafe_solvers solvers;
   1.154 -
   1.155 -fun (Simpset {mss, mk_cong = _, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.156 -    setmkcong mk_cong =
   1.157 -  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.158 -
   1.159 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.160 -    setmksym mksym =
   1.161 -  make_ss (MetaSimplifier.set_mk_sym (mss, mksym)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.162 -
   1.163 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
   1.164 -    settermless termless =
   1.165 -  make_ss (MetaSimplifier.set_termless (mss, termless)) mk_cong subgoal_tac loop_tacs
   1.166 -    unsafe_solvers solvers;
   1.167 -
   1.168 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.169 -    addsimps rews =
   1.170 -  make_ss (MetaSimplifier.add_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.171 -
   1.172 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.173 -    delsimps rews =
   1.174 -  make_ss (MetaSimplifier.del_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.175 -
   1.176 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.177 -    addeqcongs newcongs =
   1.178 -  make_ss (MetaSimplifier.add_congs (mss, newcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.179 -
   1.180 -fun (Simpset {mss, subgoal_tac, mk_cong, loop_tacs, unsafe_solvers, solvers})
   1.181 -    deleqcongs oldcongs =
   1.182 -  make_ss (MetaSimplifier.del_congs (mss, oldcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.183 -
   1.184 -fun (ss as Simpset {mk_cong, ...}) addcongs newcongs =
   1.185 -  ss addeqcongs map mk_cong newcongs;
   1.186 -
   1.187 -fun (ss as Simpset {mk_cong, ...}) delcongs oldcongs =
   1.188 -  ss deleqcongs map mk_cong oldcongs;
   1.189 -
   1.190 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.191 -    addsimprocs simprocs =
   1.192 -  make_ss (MetaSimplifier.add_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac loop_tacs
   1.193 -    unsafe_solvers solvers;
   1.194 -
   1.195 -fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.196 -    delsimprocs simprocs =
   1.197 -  make_ss (MetaSimplifier.del_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac
   1.198 -    loop_tacs unsafe_solvers solvers;
   1.199 -
   1.200 -fun clear_ss (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
   1.201 -  make_ss (MetaSimplifier.clear_mss mss) mk_cong subgoal_tac [] unsafe_solvers solvers;
   1.202 -
   1.203 -
   1.204 -(* merge simpsets *)
   1.205 -
   1.206 -(*ignores subgoal_tac of 2nd simpset!*)
   1.207 -
   1.208 -fun merge_ss
   1.209 -   (Simpset {mss = mss1, mk_cong, loop_tacs = loop_tacs1, subgoal_tac,
   1.210 -             unsafe_solvers = unsafe_solvers1, solvers = solvers1},
   1.211 -    Simpset {mss = mss2, mk_cong = _, loop_tacs = loop_tacs2, subgoal_tac = _,
   1.212 -             unsafe_solvers = unsafe_solvers2, solvers = solvers2}) =
   1.213 -  make_ss (MetaSimplifier.merge_mss (mss1, mss2)) mk_cong subgoal_tac
   1.214 -    (merge_alists loop_tacs1 loop_tacs2)
   1.215 -    (merge_solvers unsafe_solvers1 unsafe_solvers2)
   1.216 -    (merge_solvers solvers1 solvers2);
   1.217 -
   1.218 -
   1.219 +(* Compatibility *)
   1.220 +open MetaSimplifier;
   1.221  
   1.222  (** global and local simpset data **)
   1.223  
   1.224 @@ -399,31 +207,6 @@
   1.225  val cong_del_local = change_local_ss (op delcongs);
   1.226  
   1.227  
   1.228 -
   1.229 -(** simplification tactics **)
   1.230 -
   1.231 -fun solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers) mss =
   1.232 -  let
   1.233 -    val ss =
   1.234 -      make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers unsafe_solvers;
   1.235 -    val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   1.236 -  in DEPTH_SOLVE solve1_tac end;
   1.237 -
   1.238 -fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
   1.239 -
   1.240 -(*note: may instantiate unknowns that appear also in other subgoals*)
   1.241 -fun generic_simp_tac safe mode =
   1.242 -  fn (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   1.243 -    let
   1.244 -      val solvs = app_sols (if safe then solvers else unsafe_solvers);
   1.245 -      fun simp_loop_tac i =
   1.246 -        asm_rewrite_goal_tac mode
   1.247 -          (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
   1.248 -          mss i
   1.249 -        THEN (solvs (MetaSimplifier.prems_of_mss mss) i ORELSE
   1.250 -              TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   1.251 -    in simp_loop_tac end;
   1.252 -
   1.253  val simp_tac = generic_simp_tac false (false, false, false);
   1.254  val asm_simp_tac = generic_simp_tac false (false, true, false);
   1.255  val full_simp_tac = generic_simp_tac false (true, false, false);
   1.256 @@ -432,6 +215,7 @@
   1.257  val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   1.258  
   1.259  
   1.260 +
   1.261  (*the abstraction over the proof state delays the dereferencing*)
   1.262  fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   1.263  fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   1.264 @@ -439,20 +223,6 @@
   1.265  fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   1.266  fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   1.267  
   1.268 -
   1.269 -
   1.270 -(** simplification rules and conversions **)
   1.271 -
   1.272 -fun simp rew mode
   1.273 -     (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   1.274 -  let
   1.275 -    val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
   1.276 -    fun prover m th = apsome fst (Seq.pull (tacf m th));
   1.277 -  in rew mode prover mss thm end;
   1.278 -
   1.279 -val simp_thm = simp MetaSimplifier.rewrite_thm;
   1.280 -val simp_cterm = simp MetaSimplifier.rewrite_cterm;
   1.281 -
   1.282  val          simplify = simp_thm (false, false, false);
   1.283  val      asm_simplify = simp_thm (false, true, false);
   1.284  val     full_simplify = simp_thm (true, false, false);
     2.1 --- a/src/Pure/ROOT.ML	Thu Jun 24 17:54:53 2004 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Fri Jun 25 14:30:55 2004 +0200
     2.3 @@ -45,9 +45,9 @@
     2.4  use "fact_index.ML";
     2.5  use "pure_thy.ML";
     2.6  use "drule.ML";
     2.7 -use "meta_simplifier.ML";
     2.8  use "tctical.ML";
     2.9  use "search.ML";
    2.10 +use "meta_simplifier.ML";
    2.11  use "tactic.ML";
    2.12  
    2.13  (*proof term operations*)
     3.1 --- a/src/Pure/meta_simplifier.ML	Thu Jun 24 17:54:53 2004 +0200
     3.2 +++ b/src/Pure/meta_simplifier.ML	Fri Jun 25 14:30:55 2004 +0200
     3.3 @@ -5,6 +5,11 @@
     3.4  Meta-level Simplification.
     3.5  *)
     3.6  
     3.7 +infix 4
     3.8 +  setsubgoaler setloop addloop delloop setSSolver addSSolver setSolver
     3.9 +  addSolver addsimps delsimps addeqcongs deleqcongs addcongs delcongs
    3.10 +  setmksimps setmkeqTrue setmkcong setmksym settermless addsimprocs delsimprocs;
    3.11 +
    3.12  signature BASIC_META_SIMPLIFIER =
    3.13  sig
    3.14    val trace_simp: bool ref
    3.15 @@ -12,12 +17,63 @@
    3.16    val simp_depth_limit: int ref
    3.17  end;
    3.18  
    3.19 +signature AUX_SIMPLIFIER =
    3.20 +sig
    3.21 +  type meta_simpset
    3.22 +  type simproc
    3.23 +  val mk_simproc: string -> cterm list
    3.24 +    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    3.25 +  type solver
    3.26 +  val mk_solver: string -> (thm list -> int -> tactic) -> solver
    3.27 +  type simpset
    3.28 +  val empty_ss: simpset
    3.29 +  val rep_ss: simpset ->
    3.30 +   {mss: meta_simpset,
    3.31 +    mk_cong: thm -> thm,
    3.32 +    subgoal_tac: simpset -> int -> tactic,
    3.33 +    loop_tacs: (string * (int -> tactic)) list,
    3.34 +    unsafe_solvers: solver list,
    3.35 +    solvers: solver list};
    3.36 +  val print_ss: simpset -> unit
    3.37 +  val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    3.38 +  val setloop:      simpset *             (int -> tactic) -> simpset
    3.39 +  val addloop:      simpset *  (string * (int -> tactic)) -> simpset
    3.40 +  val delloop:      simpset *   string                    -> simpset
    3.41 +  val setSSolver:   simpset * solver -> simpset
    3.42 +  val addSSolver:   simpset * solver -> simpset
    3.43 +  val setSolver:    simpset * solver -> simpset
    3.44 +  val addSolver:    simpset * solver -> simpset
    3.45 +  val setmksimps:   simpset * (thm -> thm list) -> simpset
    3.46 +  val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
    3.47 +  val setmkcong:    simpset * (thm -> thm) -> simpset
    3.48 +  val setmksym:     simpset * (thm -> thm option) -> simpset
    3.49 +  val settermless:  simpset * (term * term -> bool) -> simpset
    3.50 +  val addsimps:     simpset * thm list -> simpset
    3.51 +  val delsimps:     simpset * thm list -> simpset
    3.52 +  val addeqcongs:   simpset * thm list -> simpset
    3.53 +  val deleqcongs:   simpset * thm list -> simpset
    3.54 +  val addcongs:     simpset * thm list -> simpset
    3.55 +  val delcongs:     simpset * thm list -> simpset
    3.56 +  val addsimprocs:  simpset * simproc list -> simpset
    3.57 +  val delsimprocs:  simpset * simproc list -> simpset
    3.58 +  val merge_ss:     simpset * simpset -> simpset
    3.59 +  val prems_of_ss:  simpset -> thm list
    3.60 +  val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    3.61 +  val simproc: Sign.sg -> string -> string list
    3.62 +    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    3.63 +  val simproc_i: Sign.sg -> string -> term list
    3.64 +    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    3.65 +  val clear_ss  : simpset -> simpset
    3.66 +  val simp_thm  : bool * bool * bool -> simpset -> thm -> thm
    3.67 +  val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm
    3.68 +end;
    3.69 +
    3.70  signature META_SIMPLIFIER =
    3.71  sig
    3.72    include BASIC_META_SIMPLIFIER
    3.73 +  include AUX_SIMPLIFIER
    3.74    exception SIMPLIFIER of string * thm
    3.75    exception SIMPROC_FAIL of string * exn
    3.76 -  type meta_simpset
    3.77    val dest_mss          : meta_simpset ->
    3.78      {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    3.79    val empty_mss         : meta_simpset
    3.80 @@ -55,6 +111,9 @@
    3.81                            -> (meta_simpset -> thm -> thm option)
    3.82                            -> meta_simpset -> int -> thm -> thm
    3.83    val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
    3.84 +  val asm_rewrite_goal_tac: bool*bool*bool ->
    3.85 +    (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    3.86 +
    3.87  end;
    3.88  
    3.89  structure MetaSimplifier : META_SIMPLIFIER =
    3.90 @@ -122,7 +181,7 @@
    3.91         in which case there is nothing better to do.
    3.92  *)
    3.93  type cong = {thm: thm, lhs: cterm};
    3.94 -type simproc =
    3.95 +type meta_simproc =
    3.96   {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
    3.97  
    3.98  fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
    3.99 @@ -134,7 +193,7 @@
   3.100  fun eq_prem (thm1, thm2) =
   3.101    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   3.102  
   3.103 -fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
   3.104 +fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
   3.105  
   3.106  fun mk_simproc (name, proc, lhs, id) =
   3.107    {name = name, proc = proc, lhs = lhs, id = id};
   3.108 @@ -164,7 +223,7 @@
   3.109    Mss of {
   3.110      rules: rrule Net.net,
   3.111      congs: (string * cong) list * string list,
   3.112 -    procs: simproc Net.net,
   3.113 +    procs: meta_simproc Net.net,
   3.114      bounds: string list,
   3.115      prems: thm list,
   3.116      mk_rews: {mk: thm -> thm list,
   3.117 @@ -528,6 +587,193 @@
   3.118  
   3.119  
   3.120  
   3.121 +(** simplification procedures **)
   3.122 +
   3.123 +(* datatype simproc *)
   3.124 +
   3.125 +datatype simproc =
   3.126 +  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
   3.127 +
   3.128 +fun mk_simproc name lhss proc =
   3.129 +  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   3.130 +
   3.131 +fun simproc sg name ss =
   3.132 +  mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
   3.133 +fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg);
   3.134 +
   3.135 +fun rep_simproc (Simproc args) = args;
   3.136 +
   3.137 +
   3.138 +
   3.139 +(** solvers **)
   3.140 +
   3.141 +datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   3.142 +
   3.143 +fun mk_solver name solver = Solver (name, solver, stamp());
   3.144 +fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
   3.145 +
   3.146 +val merge_solvers = gen_merge_lists eq_solver;
   3.147 +
   3.148 +fun app_sols [] _ _ = no_tac
   3.149 +  | app_sols (Solver(_,solver,_)::sols) thms i =
   3.150 +       solver thms i ORELSE app_sols sols thms i;
   3.151 +
   3.152 +
   3.153 +
   3.154 +(** simplification sets **)
   3.155 +
   3.156 +(* type simpset *)
   3.157 +
   3.158 +datatype simpset =
   3.159 +  Simpset of {
   3.160 +    mss: meta_simpset,
   3.161 +    mk_cong: thm -> thm,
   3.162 +    subgoal_tac: simpset -> int -> tactic,
   3.163 +    loop_tacs: (string * (int -> tactic)) list,
   3.164 +    unsafe_solvers: solver list,
   3.165 +    solvers: solver list};
   3.166 +
   3.167 +fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
   3.168 +  Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
   3.169 +    loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
   3.170 +
   3.171 +val empty_ss =
   3.172 +  let val mss = set_mk_sym (empty_mss, Some o symmetric_fun)
   3.173 +  in make_ss mss I (K (K no_tac)) [] [] [] end;
   3.174 +
   3.175 +fun rep_ss (Simpset args) = args;
   3.176 +fun prems_of_ss (Simpset {mss, ...}) = prems_of_mss mss;
   3.177 +
   3.178 +
   3.179 +(* print simpsets *)
   3.180 +
   3.181 +fun print_ss ss =
   3.182 +  let
   3.183 +    val Simpset {mss, ...} = ss;
   3.184 +    val {simps, procs, congs} = dest_mss mss;
   3.185 +
   3.186 +    val pretty_thms = map Display.pretty_thm;
   3.187 +    fun pretty_proc (name, lhss) =
   3.188 +      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
   3.189 +  in
   3.190 +    [Pretty.big_list "simplification rules:" (pretty_thms simps),
   3.191 +      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
   3.192 +      Pretty.big_list "congruences:" (pretty_thms congs)]
   3.193 +    |> Pretty.chunks |> Pretty.writeln
   3.194 +  end;
   3.195 +
   3.196 +
   3.197 +(* extend simpsets *)
   3.198 +
   3.199 +fun (Simpset {mss, mk_cong, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
   3.200 +    setsubgoaler subgoal_tac =
   3.201 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.202 +
   3.203 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
   3.204 +    setloop tac =
   3.205 +  make_ss mss mk_cong subgoal_tac [("", tac)] unsafe_solvers solvers;
   3.206 +
   3.207 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.208 +    addloop tac = make_ss mss mk_cong subgoal_tac
   3.209 +      (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
   3.210 +        warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac))
   3.211 +      unsafe_solvers solvers;
   3.212 +
   3.213 +fun (ss as Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.214 + delloop name =
   3.215 +  let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
   3.216 +    if null del then (warning ("No such looper in simpset: " ^ name); ss)
   3.217 +    else make_ss mss mk_cong subgoal_tac rest unsafe_solvers solvers
   3.218 +  end;
   3.219 +
   3.220 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...})
   3.221 +    setSSolver solver =
   3.222 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers [solver];
   3.223 +
   3.224 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.225 +    addSSolver sol =
   3.226 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers (merge_solvers solvers [sol]);
   3.227 +
   3.228 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
   3.229 +    setSolver unsafe_solver =
   3.230 +  make_ss mss mk_cong subgoal_tac loop_tacs [unsafe_solver] solvers;
   3.231 +
   3.232 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.233 +    addSolver sol =
   3.234 +  make_ss mss mk_cong subgoal_tac loop_tacs (merge_solvers unsafe_solvers [sol]) solvers;
   3.235 +
   3.236 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.237 +    setmksimps mk_simps =
   3.238 +  make_ss (set_mk_rews (mss, mk_simps)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.239 +
   3.240 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.241 +    setmkeqTrue mk_eq_True =
   3.242 +  make_ss (set_mk_eq_True (mss, mk_eq_True)) mk_cong subgoal_tac loop_tacs
   3.243 +    unsafe_solvers solvers;
   3.244 +
   3.245 +fun (Simpset {mss, mk_cong = _, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.246 +    setmkcong mk_cong =
   3.247 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.248 +
   3.249 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.250 +    setmksym mksym =
   3.251 +  make_ss (set_mk_sym (mss, mksym)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.252 +
   3.253 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
   3.254 +    settermless termless =
   3.255 +  make_ss (set_termless (mss, termless)) mk_cong subgoal_tac loop_tacs
   3.256 +    unsafe_solvers solvers;
   3.257 +
   3.258 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.259 +    addsimps rews =
   3.260 +  make_ss (add_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.261 +
   3.262 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.263 +    delsimps rews =
   3.264 +  make_ss (del_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.265 +
   3.266 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.267 +    addeqcongs newcongs =
   3.268 +  make_ss (add_congs (mss, newcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.269 +
   3.270 +fun (Simpset {mss, subgoal_tac, mk_cong, loop_tacs, unsafe_solvers, solvers})
   3.271 +    deleqcongs oldcongs =
   3.272 +  make_ss (del_congs (mss, oldcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   3.273 +
   3.274 +fun (ss as Simpset {mk_cong, ...}) addcongs newcongs =
   3.275 +  ss addeqcongs map mk_cong newcongs;
   3.276 +
   3.277 +fun (ss as Simpset {mk_cong, ...}) delcongs oldcongs =
   3.278 +  ss deleqcongs map mk_cong oldcongs;
   3.279 +
   3.280 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.281 +    addsimprocs simprocs =
   3.282 +  make_ss (add_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac loop_tacs
   3.283 +    unsafe_solvers solvers;
   3.284 +
   3.285 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   3.286 +    delsimprocs simprocs =
   3.287 +  make_ss (del_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac
   3.288 +    loop_tacs unsafe_solvers solvers;
   3.289 +
   3.290 +fun clear_ss (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
   3.291 +  make_ss (clear_mss mss) mk_cong subgoal_tac [] unsafe_solvers solvers;
   3.292 +
   3.293 +
   3.294 +(* merge simpsets *)
   3.295 +
   3.296 +(*ignores subgoal_tac of 2nd simpset!*)
   3.297 +
   3.298 +fun merge_ss
   3.299 +   (Simpset {mss = mss1, mk_cong, loop_tacs = loop_tacs1, subgoal_tac,
   3.300 +             unsafe_solvers = unsafe_solvers1, solvers = solvers1},
   3.301 +    Simpset {mss = mss2, mk_cong = _, loop_tacs = loop_tacs2, subgoal_tac = _,
   3.302 +             unsafe_solvers = unsafe_solvers2, solvers = solvers2}) =
   3.303 +  make_ss (merge_mss (mss1, mss2)) mk_cong subgoal_tac
   3.304 +    (merge_alists loop_tacs1 loop_tacs2)
   3.305 +    (merge_solvers unsafe_solvers1 unsafe_solvers2)
   3.306 +    (merge_solvers solvers1 solvers2);
   3.307 +
   3.308  (** rewriting **)
   3.309  
   3.310  (*
   3.311 @@ -666,7 +912,7 @@
   3.312                                       else sort rrs (re1,rr::re2)
   3.313      in sort rrs ([],[]) end
   3.314  
   3.315 -    fun proc_rews ([]:simproc list) = None
   3.316 +    fun proc_rews ([]:meta_simproc list) = None
   3.317        | proc_rews ({name, proc, lhs, ...} :: ps) =
   3.318            if Pattern.matches tsigt (term_of lhs, term_of t) then
   3.319              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   3.320 @@ -965,6 +1211,47 @@
   3.321  fun rewrite_term sg rules procs =
   3.322    Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
   3.323  
   3.324 +(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
   3.325 +fun asm_rewrite_goal_tac mode prover_tac mss =
   3.326 +  SELECT_GOAL
   3.327 +    (PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) mss 1));
   3.328 +
   3.329 +(** simplification tactics **)
   3.330 +
   3.331 +fun solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers) mss =
   3.332 +  let
   3.333 +    val ss =
   3.334 +      make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers unsafe_solvers;
   3.335 +    val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   3.336 +  in DEPTH_SOLVE solve1_tac end;
   3.337 +
   3.338 +fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
   3.339 +
   3.340 +(*note: may instantiate unknowns that appear also in other subgoals*)
   3.341 +fun generic_simp_tac safe mode =
   3.342 +  fn (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   3.343 +    let
   3.344 +      val solvs = app_sols (if safe then solvers else unsafe_solvers);
   3.345 +      fun simp_loop_tac i =
   3.346 +        asm_rewrite_goal_tac mode
   3.347 +          (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
   3.348 +          mss i
   3.349 +        THEN (solvs (prems_of_mss mss) i ORELSE
   3.350 +              TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   3.351 +    in simp_loop_tac end;
   3.352 +
   3.353 +(** simplification rules and conversions **)
   3.354 +
   3.355 +fun simp rew mode
   3.356 +     (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   3.357 +  let
   3.358 +    val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
   3.359 +    fun prover m th = apsome fst (Seq.pull (tacf m th));
   3.360 +  in rew mode prover mss thm end;
   3.361 +
   3.362 +val simp_thm = simp rewrite_thm;
   3.363 +val simp_cterm = simp rewrite_cterm;
   3.364 +
   3.365  end;
   3.366  
   3.367  structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;
     4.1 --- a/src/Pure/tactic.ML	Thu Jun 24 17:54:53 2004 +0200
     4.2 +++ b/src/Pure/tactic.ML	Fri Jun 25 14:30:55 2004 +0200
     4.3 @@ -9,8 +9,6 @@
     4.4  signature BASIC_TACTIC =
     4.5  sig
     4.6    val ares_tac          : thm list -> int -> tactic
     4.7 -  val asm_rewrite_goal_tac: bool*bool*bool ->
     4.8 -    (MetaSimplifier.meta_simpset -> tactic) -> MetaSimplifier.meta_simpset -> int -> tactic
     4.9    val assume_tac        : int -> tactic
    4.10    val atac      : int ->tactic
    4.11    val bimatch_from_nets_tac:
    4.12 @@ -74,8 +72,6 @@
    4.13    val net_resolve_tac   : thm list -> int -> tactic
    4.14    val norm_hhf_rule     : thm -> thm
    4.15    val norm_hhf_tac      : int -> tactic
    4.16 -  val PRIMITIVE         : (thm -> thm) -> tactic
    4.17 -  val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic
    4.18    val prune_params_tac  : tactic
    4.19    val rename_params_tac : string list -> int -> tactic
    4.20    val rename_tac        : string -> int -> tactic
    4.21 @@ -137,12 +133,6 @@
    4.22  
    4.23  (*** Basic tactics ***)
    4.24  
    4.25 -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
    4.26 -fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
    4.27 -
    4.28 -(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
    4.29 -fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
    4.30 -
    4.31  (*** The following fail if the goal number is out of range:
    4.32       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
    4.33  
    4.34 @@ -499,24 +489,16 @@
    4.35  
    4.36  (*** Meta-Rewriting Tactics ***)
    4.37  
    4.38 -fun result1 tacf mss thm =
    4.39 -  apsome fst (Seq.pull (tacf mss thm));
    4.40 -
    4.41  val simple_prover =
    4.42 -  result1 (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
    4.43 +  SINGLE o (fn mss => ALLGOALS (resolve_tac (MetaSimplifier.prems_of_mss mss)));
    4.44  
    4.45  val rewrite = MetaSimplifier.rewrite_aux simple_prover;
    4.46  val simplify = MetaSimplifier.simplify_aux simple_prover;
    4.47  val rewrite_rule = simplify true;
    4.48  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
    4.49  
    4.50 -(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    4.51 -fun asm_rewrite_goal_tac mode prover_tac mss =
    4.52 -  SELECT_GOAL
    4.53 -    (PRIMITIVE (MetaSimplifier.rewrite_goal_rule mode (result1 prover_tac) mss 1));
    4.54 -
    4.55  fun rewrite_goal_tac rews =
    4.56 -  asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
    4.57 +  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
    4.58  
    4.59  (*Rewrite throughout proof state. *)
    4.60  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
     5.1 --- a/src/Pure/tctical.ML	Thu Jun 24 17:54:53 2004 +0200
     5.2 +++ b/src/Pure/tctical.ML	Fri Jun 25 14:30:55 2004 +0200
     5.3 @@ -39,6 +39,8 @@
     5.4    val ORELSE'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
     5.5    val pause_tac         : tactic
     5.6    val print_tac         : string -> tactic
     5.7 +  val PRIMITIVE         : (thm -> thm) -> tactic
     5.8 +  val PRIMSEQ           : (thm -> thm Seq.seq) -> tactic
     5.9    val RANGE             : (int -> tactic) list -> int -> tactic
    5.10    val REPEAT            : tactic -> tactic
    5.11    val REPEAT1           : tactic -> tactic
    5.12 @@ -51,6 +53,7 @@
    5.13    val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
    5.14    val DETERM_UNTIL      : (thm -> bool) -> tactic -> tactic
    5.15    val SELECT_GOAL       : tactic -> int -> tactic
    5.16 +  val SINGLE            : tactic -> thm -> thm option
    5.17    val SOMEGOAL          : (int -> tactic) -> tactic
    5.18    val strip_context     : term -> (string * typ) list * term list * term
    5.19    val SUBGOAL           : ((term*int) -> tactic) -> int -> tactic
    5.20 @@ -491,6 +494,15 @@
    5.21  
    5.22  fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf);
    5.23  
    5.24 +(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
    5.25 +fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
    5.26 +
    5.27 +(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)
    5.28 +fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);
    5.29 +
    5.30 +(* Inverse (more or less) of PRIMITIVE *)
    5.31 +fun SINGLE tacf = apsome fst o Seq.pull o tacf
    5.32 +		  
    5.33  end;
    5.34  
    5.35  open Tactical;