src/Pure/meta_simplifier.ML
changeset 15006 107e4dfd3b96
parent 15001 fb2141a9f8c0
child 15011 35be762f58f9
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Jun 24 17:54:53 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Jun 25 14:30:55 2004 +0200
     1.3 @@ -5,6 +5,11 @@
     1.4  Meta-level Simplification.
     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_META_SIMPLIFIER =
    1.13  sig
    1.14    val trace_simp: bool ref
    1.15 @@ -12,12 +17,63 @@
    1.16    val simp_depth_limit: int ref
    1.17  end;
    1.18  
    1.19 +signature AUX_SIMPLIFIER =
    1.20 +sig
    1.21 +  type meta_simpset
    1.22 +  type simproc
    1.23 +  val mk_simproc: string -> cterm list
    1.24 +    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.25 +  type solver
    1.26 +  val mk_solver: string -> (thm list -> int -> tactic) -> solver
    1.27 +  type simpset
    1.28 +  val empty_ss: simpset
    1.29 +  val rep_ss: simpset ->
    1.30 +   {mss: meta_simpset,
    1.31 +    mk_cong: thm -> thm,
    1.32 +    subgoal_tac: simpset -> int -> tactic,
    1.33 +    loop_tacs: (string * (int -> tactic)) list,
    1.34 +    unsafe_solvers: solver list,
    1.35 +    solvers: solver list};
    1.36 +  val print_ss: simpset -> unit
    1.37 +  val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
    1.38 +  val setloop:      simpset *             (int -> tactic) -> simpset
    1.39 +  val addloop:      simpset *  (string * (int -> tactic)) -> simpset
    1.40 +  val delloop:      simpset *   string                    -> simpset
    1.41 +  val setSSolver:   simpset * solver -> simpset
    1.42 +  val addSSolver:   simpset * solver -> simpset
    1.43 +  val setSolver:    simpset * solver -> simpset
    1.44 +  val addSolver:    simpset * solver -> simpset
    1.45 +  val setmksimps:   simpset * (thm -> thm list) -> simpset
    1.46 +  val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
    1.47 +  val setmkcong:    simpset * (thm -> thm) -> simpset
    1.48 +  val setmksym:     simpset * (thm -> thm option) -> simpset
    1.49 +  val settermless:  simpset * (term * term -> bool) -> simpset
    1.50 +  val addsimps:     simpset * thm list -> simpset
    1.51 +  val delsimps:     simpset * thm list -> simpset
    1.52 +  val addeqcongs:   simpset * thm list -> simpset
    1.53 +  val deleqcongs:   simpset * thm list -> simpset
    1.54 +  val addcongs:     simpset * thm list -> simpset
    1.55 +  val delcongs:     simpset * thm list -> simpset
    1.56 +  val addsimprocs:  simpset * simproc list -> simpset
    1.57 +  val delsimprocs:  simpset * simproc list -> simpset
    1.58 +  val merge_ss:     simpset * simpset -> simpset
    1.59 +  val prems_of_ss:  simpset -> thm list
    1.60 +  val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    1.61 +  val simproc: Sign.sg -> string -> string list
    1.62 +    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.63 +  val simproc_i: Sign.sg -> string -> term list
    1.64 +    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
    1.65 +  val clear_ss  : simpset -> simpset
    1.66 +  val simp_thm  : bool * bool * bool -> simpset -> thm -> thm
    1.67 +  val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm
    1.68 +end;
    1.69 +
    1.70  signature META_SIMPLIFIER =
    1.71  sig
    1.72    include BASIC_META_SIMPLIFIER
    1.73 +  include AUX_SIMPLIFIER
    1.74    exception SIMPLIFIER of string * thm
    1.75    exception SIMPROC_FAIL of string * exn
    1.76 -  type meta_simpset
    1.77    val dest_mss          : meta_simpset ->
    1.78      {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    1.79    val empty_mss         : meta_simpset
    1.80 @@ -55,6 +111,9 @@
    1.81                            -> (meta_simpset -> thm -> thm option)
    1.82                            -> meta_simpset -> int -> thm -> thm
    1.83    val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
    1.84 +  val asm_rewrite_goal_tac: bool*bool*bool ->
    1.85 +    (meta_simpset -> tactic) -> meta_simpset -> int -> tactic
    1.86 +
    1.87  end;
    1.88  
    1.89  structure MetaSimplifier : META_SIMPLIFIER =
    1.90 @@ -122,7 +181,7 @@
    1.91         in which case there is nothing better to do.
    1.92  *)
    1.93  type cong = {thm: thm, lhs: cterm};
    1.94 -type simproc =
    1.95 +type meta_simproc =
    1.96   {name: string, proc: Sign.sg -> thm list -> term -> thm option, lhs: cterm, id: stamp};
    1.97  
    1.98  fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
    1.99 @@ -134,7 +193,7 @@
   1.100  fun eq_prem (thm1, thm2) =
   1.101    #prop (rep_thm thm1) aconv #prop (rep_thm thm2);
   1.102  
   1.103 -fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
   1.104 +fun eq_simproc ({id = s1, ...}:meta_simproc, {id = s2, ...}:meta_simproc) = (s1 = s2);
   1.105  
   1.106  fun mk_simproc (name, proc, lhs, id) =
   1.107    {name = name, proc = proc, lhs = lhs, id = id};
   1.108 @@ -164,7 +223,7 @@
   1.109    Mss of {
   1.110      rules: rrule Net.net,
   1.111      congs: (string * cong) list * string list,
   1.112 -    procs: simproc Net.net,
   1.113 +    procs: meta_simproc Net.net,
   1.114      bounds: string list,
   1.115      prems: thm list,
   1.116      mk_rews: {mk: thm -> thm list,
   1.117 @@ -528,6 +587,193 @@
   1.118  
   1.119  
   1.120  
   1.121 +(** simplification procedures **)
   1.122 +
   1.123 +(* datatype simproc *)
   1.124 +
   1.125 +datatype simproc =
   1.126 +  Simproc of string * cterm list * (Sign.sg -> thm list -> term -> thm option) * stamp;
   1.127 +
   1.128 +fun mk_simproc name lhss proc =
   1.129 +  Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
   1.130 +
   1.131 +fun simproc sg name ss =
   1.132 +  mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
   1.133 +fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg);
   1.134 +
   1.135 +fun rep_simproc (Simproc args) = args;
   1.136 +
   1.137 +
   1.138 +
   1.139 +(** solvers **)
   1.140 +
   1.141 +datatype solver = Solver of string * (thm list -> int -> tactic) * stamp;
   1.142 +
   1.143 +fun mk_solver name solver = Solver (name, solver, stamp());
   1.144 +fun eq_solver (Solver (_, _, s1), Solver(_, _, s2)) = s1 = s2;
   1.145 +
   1.146 +val merge_solvers = gen_merge_lists eq_solver;
   1.147 +
   1.148 +fun app_sols [] _ _ = no_tac
   1.149 +  | app_sols (Solver(_,solver,_)::sols) thms i =
   1.150 +       solver thms i ORELSE app_sols sols thms i;
   1.151 +
   1.152 +
   1.153 +
   1.154 +(** simplification sets **)
   1.155 +
   1.156 +(* type simpset *)
   1.157 +
   1.158 +datatype simpset =
   1.159 +  Simpset of {
   1.160 +    mss: meta_simpset,
   1.161 +    mk_cong: thm -> thm,
   1.162 +    subgoal_tac: simpset -> int -> tactic,
   1.163 +    loop_tacs: (string * (int -> tactic)) list,
   1.164 +    unsafe_solvers: solver list,
   1.165 +    solvers: solver list};
   1.166 +
   1.167 +fun make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers =
   1.168 +  Simpset {mss = mss, mk_cong = mk_cong, subgoal_tac = subgoal_tac,
   1.169 +    loop_tacs = loop_tacs, unsafe_solvers = unsafe_solvers, solvers = solvers};
   1.170 +
   1.171 +val empty_ss =
   1.172 +  let val mss = set_mk_sym (empty_mss, Some o symmetric_fun)
   1.173 +  in make_ss mss I (K (K no_tac)) [] [] [] end;
   1.174 +
   1.175 +fun rep_ss (Simpset args) = args;
   1.176 +fun prems_of_ss (Simpset {mss, ...}) = prems_of_mss mss;
   1.177 +
   1.178 +
   1.179 +(* print simpsets *)
   1.180 +
   1.181 +fun print_ss ss =
   1.182 +  let
   1.183 +    val Simpset {mss, ...} = ss;
   1.184 +    val {simps, procs, congs} = dest_mss mss;
   1.185 +
   1.186 +    val pretty_thms = map Display.pretty_thm;
   1.187 +    fun pretty_proc (name, lhss) =
   1.188 +      Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss);
   1.189 +  in
   1.190 +    [Pretty.big_list "simplification rules:" (pretty_thms simps),
   1.191 +      Pretty.big_list "simplification procedures:" (map pretty_proc procs),
   1.192 +      Pretty.big_list "congruences:" (pretty_thms congs)]
   1.193 +    |> Pretty.chunks |> Pretty.writeln
   1.194 +  end;
   1.195 +
   1.196 +
   1.197 +(* extend simpsets *)
   1.198 +
   1.199 +fun (Simpset {mss, mk_cong, subgoal_tac = _, loop_tacs, unsafe_solvers, solvers})
   1.200 +    setsubgoaler subgoal_tac =
   1.201 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.202 +
   1.203 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers})
   1.204 +    setloop tac =
   1.205 +  make_ss mss mk_cong subgoal_tac [("", tac)] unsafe_solvers solvers;
   1.206 +
   1.207 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.208 +    addloop tac = make_ss mss mk_cong subgoal_tac
   1.209 +      (case assoc_string (loop_tacs, (#1 tac)) of None => () | Some x =>
   1.210 +        warning ("overwriting looper " ^ quote (#1 tac)); overwrite (loop_tacs, tac))
   1.211 +      unsafe_solvers solvers;
   1.212 +
   1.213 +fun (ss as Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.214 + delloop name =
   1.215 +  let val (del, rest) = partition (fn (n, _) => n = name) loop_tacs in
   1.216 +    if null del then (warning ("No such looper in simpset: " ^ name); ss)
   1.217 +    else make_ss mss mk_cong subgoal_tac rest unsafe_solvers solvers
   1.218 +  end;
   1.219 +
   1.220 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...})
   1.221 +    setSSolver solver =
   1.222 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers [solver];
   1.223 +
   1.224 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.225 +    addSSolver sol =
   1.226 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers (merge_solvers solvers [sol]);
   1.227 +
   1.228 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers = _, solvers})
   1.229 +    setSolver unsafe_solver =
   1.230 +  make_ss mss mk_cong subgoal_tac loop_tacs [unsafe_solver] solvers;
   1.231 +
   1.232 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.233 +    addSolver sol =
   1.234 +  make_ss mss mk_cong subgoal_tac loop_tacs (merge_solvers unsafe_solvers [sol]) solvers;
   1.235 +
   1.236 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.237 +    setmksimps mk_simps =
   1.238 +  make_ss (set_mk_rews (mss, mk_simps)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.239 +
   1.240 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.241 +    setmkeqTrue mk_eq_True =
   1.242 +  make_ss (set_mk_eq_True (mss, mk_eq_True)) mk_cong subgoal_tac loop_tacs
   1.243 +    unsafe_solvers solvers;
   1.244 +
   1.245 +fun (Simpset {mss, mk_cong = _, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.246 +    setmkcong mk_cong =
   1.247 +  make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.248 +
   1.249 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.250 +    setmksym mksym =
   1.251 +  make_ss (set_mk_sym (mss, mksym)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.252 +
   1.253 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs,  unsafe_solvers, solvers})
   1.254 +    settermless termless =
   1.255 +  make_ss (set_termless (mss, termless)) mk_cong subgoal_tac loop_tacs
   1.256 +    unsafe_solvers solvers;
   1.257 +
   1.258 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.259 +    addsimps rews =
   1.260 +  make_ss (add_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.261 +
   1.262 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.263 +    delsimps rews =
   1.264 +  make_ss (del_simps (mss, rews)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.265 +
   1.266 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.267 +    addeqcongs newcongs =
   1.268 +  make_ss (add_congs (mss, newcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.269 +
   1.270 +fun (Simpset {mss, subgoal_tac, mk_cong, loop_tacs, unsafe_solvers, solvers})
   1.271 +    deleqcongs oldcongs =
   1.272 +  make_ss (del_congs (mss, oldcongs)) mk_cong subgoal_tac loop_tacs unsafe_solvers solvers;
   1.273 +
   1.274 +fun (ss as Simpset {mk_cong, ...}) addcongs newcongs =
   1.275 +  ss addeqcongs map mk_cong newcongs;
   1.276 +
   1.277 +fun (ss as Simpset {mk_cong, ...}) delcongs oldcongs =
   1.278 +  ss deleqcongs map mk_cong oldcongs;
   1.279 +
   1.280 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.281 +    addsimprocs simprocs =
   1.282 +  make_ss (add_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac loop_tacs
   1.283 +    unsafe_solvers solvers;
   1.284 +
   1.285 +fun (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers})
   1.286 +    delsimprocs simprocs =
   1.287 +  make_ss (del_simprocs (mss, map rep_simproc simprocs)) mk_cong subgoal_tac
   1.288 +    loop_tacs unsafe_solvers solvers;
   1.289 +
   1.290 +fun clear_ss (Simpset {mss, mk_cong, subgoal_tac, loop_tacs = _, unsafe_solvers, solvers}) =
   1.291 +  make_ss (clear_mss mss) mk_cong subgoal_tac [] unsafe_solvers solvers;
   1.292 +
   1.293 +
   1.294 +(* merge simpsets *)
   1.295 +
   1.296 +(*ignores subgoal_tac of 2nd simpset!*)
   1.297 +
   1.298 +fun merge_ss
   1.299 +   (Simpset {mss = mss1, mk_cong, loop_tacs = loop_tacs1, subgoal_tac,
   1.300 +             unsafe_solvers = unsafe_solvers1, solvers = solvers1},
   1.301 +    Simpset {mss = mss2, mk_cong = _, loop_tacs = loop_tacs2, subgoal_tac = _,
   1.302 +             unsafe_solvers = unsafe_solvers2, solvers = solvers2}) =
   1.303 +  make_ss (merge_mss (mss1, mss2)) mk_cong subgoal_tac
   1.304 +    (merge_alists loop_tacs1 loop_tacs2)
   1.305 +    (merge_solvers unsafe_solvers1 unsafe_solvers2)
   1.306 +    (merge_solvers solvers1 solvers2);
   1.307 +
   1.308  (** rewriting **)
   1.309  
   1.310  (*
   1.311 @@ -666,7 +912,7 @@
   1.312                                       else sort rrs (re1,rr::re2)
   1.313      in sort rrs ([],[]) end
   1.314  
   1.315 -    fun proc_rews ([]:simproc list) = None
   1.316 +    fun proc_rews ([]:meta_simproc list) = None
   1.317        | proc_rews ({name, proc, lhs, ...} :: ps) =
   1.318            if Pattern.matches tsigt (term_of lhs, term_of t) then
   1.319              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   1.320 @@ -965,6 +1211,47 @@
   1.321  fun rewrite_term sg rules procs =
   1.322    Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
   1.323  
   1.324 +(*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
   1.325 +fun asm_rewrite_goal_tac mode prover_tac mss =
   1.326 +  SELECT_GOAL
   1.327 +    (PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) mss 1));
   1.328 +
   1.329 +(** simplification tactics **)
   1.330 +
   1.331 +fun solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers) mss =
   1.332 +  let
   1.333 +    val ss =
   1.334 +      make_ss mss mk_cong subgoal_tac loop_tacs unsafe_solvers unsafe_solvers;
   1.335 +    val solve1_tac = (subgoal_tac ss THEN_ALL_NEW (K no_tac)) 1
   1.336 +  in DEPTH_SOLVE solve1_tac end;
   1.337 +
   1.338 +fun loop_tac loop_tacs = FIRST'(map snd loop_tacs);
   1.339 +
   1.340 +(*note: may instantiate unknowns that appear also in other subgoals*)
   1.341 +fun generic_simp_tac safe mode =
   1.342 +  fn (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, solvers, ...}) =>
   1.343 +    let
   1.344 +      val solvs = app_sols (if safe then solvers else unsafe_solvers);
   1.345 +      fun simp_loop_tac i =
   1.346 +        asm_rewrite_goal_tac mode
   1.347 +          (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
   1.348 +          mss i
   1.349 +        THEN (solvs (prems_of_mss mss) i ORELSE
   1.350 +              TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
   1.351 +    in simp_loop_tac end;
   1.352 +
   1.353 +(** simplification rules and conversions **)
   1.354 +
   1.355 +fun simp rew mode
   1.356 +     (Simpset {mss, mk_cong, subgoal_tac, loop_tacs, unsafe_solvers, ...}) thm =
   1.357 +  let
   1.358 +    val tacf = solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers);
   1.359 +    fun prover m th = apsome fst (Seq.pull (tacf m th));
   1.360 +  in rew mode prover mss thm end;
   1.361 +
   1.362 +val simp_thm = simp rewrite_thm;
   1.363 +val simp_cterm = simp rewrite_cterm;
   1.364 +
   1.365  end;
   1.366  
   1.367  structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier;