src/Pure/simplifier.ML
changeset 16014 85f4b0f81f62
child 16458 4c6fd0c01d28
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/simplifier.ML	Sun May 22 16:51:03 2005 +0200
     1.3 @@ -0,0 +1,550 @@
     1.4 +(*  Title:      Pure/simplifier.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Generic simplifier, suitable for most logics (see also
     1.9 +meta_simplifier.ML for the actual meta-level rewriting engine).
    1.10 +*)
    1.11 +
    1.12 +(* added: put_delta_simpset, get_delta_simpset
    1.13 +   changed: simp_add_local
    1.14 +   07/01/05
    1.15 +*)
    1.16 +
    1.17 +
    1.18 +signature BASIC_SIMPLIFIER =
    1.19 +sig
    1.20 +  include BASIC_META_SIMPLIFIER
    1.21 +  type context_solver
    1.22 +  val mk_context_solver: string -> (Proof.context -> thm list -> int -> tactic)
    1.23 +    -> context_solver
    1.24 +  type context_simproc
    1.25 +  val mk_context_simproc: string -> cterm list ->
    1.26 +    (Proof.context -> simpset -> term -> thm option) -> context_simproc
    1.27 +  val print_simpset: theory -> unit
    1.28 +  val simpset_ref_of_sg: Sign.sg -> simpset ref
    1.29 +  val simpset_ref_of: theory -> simpset ref
    1.30 +  val simpset_of_sg: Sign.sg -> simpset
    1.31 +  val simpset_of: theory -> simpset
    1.32 +  val SIMPSET: (simpset -> tactic) -> tactic
    1.33 +  val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
    1.34 +  val simpset: unit -> simpset
    1.35 +  val simpset_ref: unit -> simpset ref
    1.36 +  val Addsimps: thm list -> unit
    1.37 +  val Delsimps: thm list -> unit
    1.38 +  val Addsimprocs: simproc list -> unit
    1.39 +  val Delsimprocs: simproc list -> unit
    1.40 +  val Addcongs: thm list -> unit
    1.41 +  val Delcongs: thm list -> unit
    1.42 +  val local_simpset_of: Proof.context -> simpset
    1.43 +  val safe_asm_full_simp_tac: simpset -> int -> tactic
    1.44 +  val               simp_tac: simpset -> int -> tactic
    1.45 +  val           asm_simp_tac: simpset -> int -> tactic
    1.46 +  val          full_simp_tac: simpset -> int -> tactic
    1.47 +  val        asm_lr_simp_tac: simpset -> int -> tactic
    1.48 +  val      asm_full_simp_tac: simpset -> int -> tactic
    1.49 +  val               Simp_tac:            int -> tactic
    1.50 +  val           Asm_simp_tac:            int -> tactic
    1.51 +  val          Full_simp_tac:            int -> tactic
    1.52 +  val        Asm_lr_simp_tac:            int -> tactic
    1.53 +  val      Asm_full_simp_tac:            int -> tactic
    1.54 +  val          simplify: simpset -> thm -> thm
    1.55 +  val      asm_simplify: simpset -> thm -> thm
    1.56 +  val     full_simplify: simpset -> thm -> thm
    1.57 +  val   asm_lr_simplify: simpset -> thm -> thm
    1.58 +  val asm_full_simplify: simpset -> thm -> thm
    1.59 +end;
    1.60 +
    1.61 +signature SIMPLIFIER =
    1.62 +sig
    1.63 +  include BASIC_SIMPLIFIER
    1.64 +  val simproc_i: Sign.sg -> string -> term list
    1.65 +    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    1.66 +  val simproc: Sign.sg -> string -> string list
    1.67 +    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    1.68 +  val context_simproc_i: Sign.sg -> string -> term list
    1.69 +    -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    1.70 +  val context_simproc: Sign.sg -> string -> string list
    1.71 +    -> (Proof.context -> simpset -> term -> thm option) -> context_simproc
    1.72 +  val          rewrite: simpset -> cterm -> thm
    1.73 +  val      asm_rewrite: simpset -> cterm -> thm
    1.74 +  val     full_rewrite: simpset -> cterm -> thm
    1.75 +  val   asm_lr_rewrite: simpset -> cterm -> thm
    1.76 +  val asm_full_rewrite: simpset -> cterm -> thm
    1.77 +  val add_context_simprocs: context_simproc list -> theory -> theory
    1.78 +  val del_context_simprocs: context_simproc list -> theory -> theory
    1.79 +  val set_context_subgoaler: (Proof.context -> simpset -> int -> tactic) -> theory -> theory
    1.80 +  val reset_context_subgoaler: theory -> theory
    1.81 +  val add_context_looper: string * (Proof.context -> int -> Tactical.tactic) ->
    1.82 +    theory -> theory
    1.83 +  val del_context_looper: string -> theory -> theory
    1.84 +  val add_context_unsafe_solver: context_solver -> theory -> theory
    1.85 +  val add_context_safe_solver: context_solver -> theory -> theory
    1.86 +  val print_local_simpset: Proof.context -> unit
    1.87 +  val get_local_simpset: Proof.context -> simpset
    1.88 +  val put_local_simpset: simpset -> Proof.context -> Proof.context
    1.89 +  val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
    1.90 +  val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
    1.91 +  val simp_add_global: theory attribute
    1.92 +  val simp_del_global: theory attribute
    1.93 +  val simp_add_local: Proof.context attribute
    1.94 +  val simp_del_local: Proof.context attribute
    1.95 +  val cong_add_global: theory attribute
    1.96 +  val cong_del_global: theory attribute
    1.97 +  val cong_add_local: Proof.context attribute
    1.98 +  val cong_del_local: Proof.context attribute
    1.99 +  val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
   1.100 +  val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   1.101 +  val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
   1.102 +    -> (theory -> theory) list
   1.103 +  val easy_setup: thm -> thm list -> (theory -> theory) list
   1.104 +
   1.105 +  val get_delta_simpset: ProofContext.context -> Thm.thm list
   1.106 +  val put_delta_simpset: Thm.thm list -> ProofContext.context -> ProofContext.context
   1.107 +end;
   1.108 +
   1.109 +structure Simplifier: SIMPLIFIER =
   1.110 +struct
   1.111 +
   1.112 +open MetaSimplifier;
   1.113 +
   1.114 +
   1.115 +(** context dependent simpset components **)
   1.116 +
   1.117 +(* datatype context_solver *)
   1.118 +
   1.119 +datatype context_solver =
   1.120 +  ContextSolver of (string * (Proof.context -> thm list -> int -> tactic)) * stamp;
   1.121 +
   1.122 +fun mk_context_solver name f = ContextSolver ((name, f), stamp ());
   1.123 +fun eq_context_solver (ContextSolver (_, id1), ContextSolver (_, id2)) = (id1 = id2);
   1.124 +val merge_context_solvers = gen_merge_lists eq_context_solver;
   1.125 +
   1.126 +
   1.127 +(* datatype context_simproc *)
   1.128 +
   1.129 +datatype context_simproc = ContextSimproc of
   1.130 +  (string * cterm list * (Proof.context -> simpset -> term -> thm option)) * stamp;
   1.131 +
   1.132 +fun mk_context_simproc name lhss f = ContextSimproc ((name, lhss, f), stamp ());
   1.133 +fun eq_context_simproc (ContextSimproc (_, id1), ContextSimproc (_, id2)) = (id1 = id2);
   1.134 +val merge_context_simprocs = gen_merge_lists eq_context_simproc;
   1.135 +
   1.136 +fun context_simproc_i sg name =
   1.137 +  mk_context_simproc name o map (Thm.cterm_of sg o Logic.varify);
   1.138 +
   1.139 +fun context_simproc sg name =
   1.140 +  context_simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
   1.141 +
   1.142 +
   1.143 +(* datatype context_ss *)
   1.144 +
   1.145 +datatype context_ss = ContextSS of
   1.146 + {simprocs: context_simproc list,
   1.147 +  subgoal_tac: (Proof.context -> simpset -> int -> tactic) option,
   1.148 +  loop_tacs: (string * (Proof.context -> int -> tactic)) list,
   1.149 +  unsafe_solvers: context_solver list,
   1.150 +  solvers: context_solver list};
   1.151 +
   1.152 +fun context_ss ctxt ss ctxt_ss =
   1.153 +  let
   1.154 +    val ContextSS {simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers} = ctxt_ss;
   1.155 +    fun prep_simproc (ContextSimproc ((name, lhss, f), _)) =
   1.156 +      mk_simproc name lhss (K (f ctxt));
   1.157 +    fun add_loop (name, f) simpset = simpset addloop (name, f ctxt);
   1.158 +    fun add_solver add (ContextSolver ((name, f), _)) simpset =
   1.159 +      add (simpset, mk_solver name (f ctxt));
   1.160 +  in
   1.161 +    ((case subgoal_tac of NONE => ss | SOME tac => ss setsubgoaler tac ctxt)
   1.162 +      addsimprocs map prep_simproc simprocs)
   1.163 +    |> fold_rev add_loop loop_tacs
   1.164 +    |> fold_rev (add_solver (op addSolver)) unsafe_solvers
   1.165 +    |> fold_rev (add_solver (op addSSolver)) solvers
   1.166 +  end;
   1.167 +
   1.168 +fun make_context_ss (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =
   1.169 +  ContextSS {simprocs = simprocs, subgoal_tac = subgoal_tac, loop_tacs = loop_tacs,
   1.170 +    unsafe_solvers = unsafe_solvers, solvers = solvers};
   1.171 +
   1.172 +val empty_context_ss = make_context_ss ([], NONE, [], [], []);
   1.173 +
   1.174 +fun merge_context_ss (ctxt_ss1, ctxt_ss2) =
   1.175 +  let
   1.176 +    val ContextSS {simprocs = simprocs1, subgoal_tac = subgoal_tac1, loop_tacs = loop_tacs1,
   1.177 +      unsafe_solvers = unsafe_solvers1, solvers = solvers1} = ctxt_ss1;
   1.178 +    val ContextSS {simprocs = simprocs2, subgoal_tac = subgoal_tac2, loop_tacs = loop_tacs2,
   1.179 +      unsafe_solvers = unsafe_solvers2, solvers = solvers2} = ctxt_ss2;
   1.180 +
   1.181 +    val simprocs' = merge_context_simprocs simprocs1 simprocs2;
   1.182 +    val subgoal_tac' = (case subgoal_tac1 of NONE => subgoal_tac2 | some => some);
   1.183 +    val loop_tacs' = merge_alists loop_tacs1 loop_tacs2;
   1.184 +    val unsafe_solvers' = merge_context_solvers unsafe_solvers1 unsafe_solvers2;
   1.185 +    val solvers' = merge_context_solvers solvers1 solvers2;
   1.186 +  in make_context_ss (simprocs', subgoal_tac', loop_tacs', unsafe_solvers', solvers') end;
   1.187 +
   1.188 +
   1.189 +
   1.190 +(** global and local simpset data **)
   1.191 +
   1.192 +(* theory data kind 'Pure/simpset' *)
   1.193 +
   1.194 +structure GlobalSimpsetArgs =
   1.195 +struct
   1.196 +  val name = "Pure/simpset";
   1.197 +  type T = simpset ref * context_ss;
   1.198 +
   1.199 +  val empty = (ref empty_ss, empty_context_ss);
   1.200 +  fun copy (ref ss, ctxt_ss) = (ref ss, ctxt_ss): T;            (*create new reference!*)
   1.201 +  val prep_ext = copy;
   1.202 +  fun merge ((ref ss1, ctxt_ss1), (ref ss2, ctxt_ss2)) =
   1.203 +    (ref (merge_ss (ss1, ss2)), merge_context_ss (ctxt_ss1, ctxt_ss2));
   1.204 +  fun print _ (ref ss, _) = print_ss ss;
   1.205 +end;
   1.206 +
   1.207 +structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
   1.208 +val _ = Context.add_setup [GlobalSimpset.init];
   1.209 +val print_simpset = GlobalSimpset.print;
   1.210 +
   1.211 +val simpset_ref_of_sg = #1 o GlobalSimpset.get_sg;
   1.212 +val simpset_ref_of = #1 o GlobalSimpset.get;
   1.213 +val get_context_ss = #2 o GlobalSimpset.get o ProofContext.theory_of;
   1.214 +
   1.215 +fun map_context_ss f = GlobalSimpset.map (apsnd
   1.216 +  (fn ContextSS {simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers} =>
   1.217 +    make_context_ss (f (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers))));
   1.218 +
   1.219 +
   1.220 +(* access global simpset *)
   1.221 +
   1.222 +val simpset_of_sg = ! o simpset_ref_of_sg;
   1.223 +val simpset_of = simpset_of_sg o Theory.sign_of;
   1.224 +
   1.225 +fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
   1.226 +fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
   1.227 +
   1.228 +val simpset = simpset_of o Context.the_context;
   1.229 +val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
   1.230 +
   1.231 +
   1.232 +(* change global simpset *)
   1.233 +
   1.234 +fun change_simpset_of f x thy =
   1.235 +  let val r = simpset_ref_of thy
   1.236 +  in r := f (! r, x); thy end;
   1.237 +
   1.238 +fun change_simpset f x = (change_simpset_of f x (Context.the_context ()); ());
   1.239 +
   1.240 +val Addsimps = change_simpset (op addsimps);
   1.241 +val Delsimps = change_simpset (op delsimps);
   1.242 +val Addsimprocs = change_simpset (op addsimprocs);
   1.243 +val Delsimprocs = change_simpset (op delsimprocs);
   1.244 +val Addcongs = change_simpset (op addcongs);
   1.245 +val Delcongs = change_simpset (op delcongs);
   1.246 +
   1.247 +
   1.248 +(* change context dependent components *)
   1.249 +
   1.250 +fun add_context_simprocs procs =
   1.251 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   1.252 +    (merge_context_simprocs procs simprocs, subgoal_tac, loop_tacs,
   1.253 +      unsafe_solvers, solvers));
   1.254 +
   1.255 +fun del_context_simprocs procs =
   1.256 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   1.257 +    (gen_rems eq_context_simproc (simprocs, procs), subgoal_tac, loop_tacs,
   1.258 +      unsafe_solvers, solvers));
   1.259 +
   1.260 +fun set_context_subgoaler tac =
   1.261 +  map_context_ss (fn (simprocs, _, loop_tacs, unsafe_solvers, solvers) =>
   1.262 +    (simprocs, SOME tac, loop_tacs, unsafe_solvers, solvers));
   1.263 +
   1.264 +val reset_context_subgoaler =
   1.265 +  map_context_ss (fn (simprocs, _, loop_tacs, unsafe_solvers, solvers) =>
   1.266 +    (simprocs, NONE, loop_tacs, unsafe_solvers, solvers));
   1.267 +
   1.268 +fun add_context_looper (name, tac) =
   1.269 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   1.270 +    (simprocs, subgoal_tac, merge_alists [(name, tac)] loop_tacs,
   1.271 +      unsafe_solvers, solvers));
   1.272 +
   1.273 +fun del_context_looper name =
   1.274 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   1.275 +    (simprocs, subgoal_tac, filter_out (equal name o #1) loop_tacs,
   1.276 +      unsafe_solvers, solvers));
   1.277 +
   1.278 +fun add_context_unsafe_solver solver =
   1.279 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   1.280 +    (simprocs, subgoal_tac, loop_tacs,
   1.281 +      merge_context_solvers [solver] unsafe_solvers, solvers));
   1.282 +
   1.283 +fun add_context_safe_solver solver =
   1.284 +  map_context_ss (fn (simprocs, subgoal_tac, loop_tacs, unsafe_solvers, solvers) =>
   1.285 +    (simprocs, subgoal_tac, loop_tacs, unsafe_solvers,
   1.286 +      merge_context_solvers [solver] solvers));
   1.287 +
   1.288 +
   1.289 +(* proof data kind 'Pure/simpset' *)
   1.290 +
   1.291 +structure LocalSimpsetArgs =
   1.292 +struct
   1.293 +  val name = "Pure/simpset";
   1.294 +  type T = simpset;
   1.295 +  val init = simpset_of;
   1.296 +  fun print ctxt ss = print_ss (context_ss ctxt ss (get_context_ss ctxt));
   1.297 +end;
   1.298 +
   1.299 +structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
   1.300 +val _ = Context.add_setup [LocalSimpset.init];
   1.301 +val print_local_simpset = LocalSimpset.print;
   1.302 +
   1.303 +val get_local_simpset = LocalSimpset.get;
   1.304 +val put_local_simpset = LocalSimpset.put;
   1.305 +fun map_local_simpset f ctxt = put_local_simpset (f (get_local_simpset ctxt)) ctxt;
   1.306 +
   1.307 +fun local_simpset_of ctxt =
   1.308 +  context_ss ctxt (get_local_simpset ctxt) (get_context_ss ctxt);
   1.309 +
   1.310 +
   1.311 +(* Jia: added DeltaSimpsetArgs and DeltaSimpset for delta_simpset
   1.312 +	also added methods to retrieve them. *)
   1.313 +(* CB: changed "delta simpsets" to context data,
   1.314 +       moved counter to here, it is no longer a ref *)
   1.315 +
   1.316 +structure DeltaSimpsetArgs =
   1.317 +struct
   1.318 +  val name = "Pure/delta_simpset";
   1.319 +  type T = Thm.thm list * int;  (*the type is thm list * int*)
   1.320 +  fun init _ = ([], 0);
   1.321 +  fun print ctxt thms = ();
   1.322 +end;
   1.323 +
   1.324 +structure DeltaSimpsetData = ProofDataFun(DeltaSimpsetArgs);
   1.325 +val _ = Context.add_setup [DeltaSimpsetData.init];
   1.326 +
   1.327 +val get_delta_simpset = #1 o DeltaSimpsetData.get;
   1.328 +fun put_delta_simpset ss = DeltaSimpsetData.map (fn (_, i) => (ss, i));
   1.329 +fun delta_increment ctxt =
   1.330 +  let val ctxt' = DeltaSimpsetData.map (fn (ss, i) => (ss, i+1)) ctxt
   1.331 +  in (ctxt', #2 (DeltaSimpsetData.get ctxt'))
   1.332 +  end;
   1.333 +
   1.334 +(* Jia: added to rename a local thm if necessary *) 
   1.335 +local 
   1.336 +fun rename_thm' (ctxt,thm) =
   1.337 +  let val (new_ctxt, new_id) = delta_increment ctxt
   1.338 +      val new_name = "anon_simp_" ^ (string_of_int new_id)
   1.339 +  in
   1.340 +    (new_ctxt, Thm.name_thm(new_name,thm))
   1.341 +end;
   1.342 +
   1.343 +in
   1.344 +
   1.345 +fun rename_thm (ctxt,thm) = if (!Proof.call_atp) then rename_thm' (ctxt,thm) else (ctxt, thm);
   1.346 +
   1.347 +end
   1.348 +
   1.349 +(* attributes *)
   1.350 +
   1.351 +fun change_global_ss f (thy, th) =
   1.352 +  let val r = simpset_ref_of thy
   1.353 +  in r := f (! r, [th]); (thy, th) end;
   1.354 +
   1.355 +fun change_local_ss f (ctxt, th) =
   1.356 +  let val ss = f (get_local_simpset ctxt, [th])
   1.357 +  in (put_local_simpset ss ctxt, th) end;
   1.358 +
   1.359 +val simp_add_global = change_global_ss (op addsimps);
   1.360 +val simp_del_global = change_global_ss (op delsimps);
   1.361 +
   1.362 +
   1.363 +
   1.364 +
   1.365 +
   1.366 +(* Jia: note: when simplifier rules are added to local_simpset, they are also added to delta_simpset in ProofContext.context, but not removed if simp_del_local is called *)
   1.367 +fun simp_add_local (ctxt,th) = 
   1.368 +    let val delta_ss = get_delta_simpset ctxt
   1.369 +	val thm_name = Thm.name_of_thm th
   1.370 +        val (ctxt', th') =
   1.371 +          if (thm_name = "") then rename_thm (ctxt,th)  else (ctxt, th)
   1.372 +	val new_dss = th'::delta_ss
   1.373 +	val ctxt'' = put_delta_simpset new_dss ctxt' 
   1.374 +    in
   1.375 +	change_local_ss (op addsimps) (ctxt'',th)
   1.376 +    end;
   1.377 +
   1.378 +val simp_del_local = change_local_ss (op delsimps);
   1.379 +
   1.380 +val cong_add_global = change_global_ss (op addcongs);
   1.381 +val cong_del_global = change_global_ss (op delcongs);
   1.382 +val cong_add_local = change_local_ss (op addcongs);
   1.383 +val cong_del_local = change_local_ss (op delcongs);
   1.384 +
   1.385 +
   1.386 +val simp_tac = generic_simp_tac false (false, false, false);
   1.387 +val asm_simp_tac = generic_simp_tac false (false, true, false);
   1.388 +val full_simp_tac = generic_simp_tac false (true, false, false);
   1.389 +val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
   1.390 +val asm_full_simp_tac = generic_simp_tac false (true, true, true);
   1.391 +val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
   1.392 +
   1.393 +
   1.394 +
   1.395 +(*the abstraction over the proof state delays the dereferencing*)
   1.396 +fun          Simp_tac i st =          simp_tac (simpset ()) i st;
   1.397 +fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
   1.398 +fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
   1.399 +fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
   1.400 +fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
   1.401 +
   1.402 +val          simplify = simp_thm (false, false, false);
   1.403 +val      asm_simplify = simp_thm (false, true, false);
   1.404 +val     full_simplify = simp_thm (true, false, false);
   1.405 +val   asm_lr_simplify = simp_thm (true, true, false);
   1.406 +val asm_full_simplify = simp_thm (true, true, true);
   1.407 +
   1.408 +val          rewrite = simp_cterm (false, false, false);
   1.409 +val      asm_rewrite = simp_cterm (false, true, false);
   1.410 +val     full_rewrite = simp_cterm (true, false, false);
   1.411 +val   asm_lr_rewrite = simp_cterm (true, true, false);
   1.412 +val asm_full_rewrite = simp_cterm (true, true, true);
   1.413 +
   1.414 +
   1.415 +
   1.416 +(** concrete syntax of attributes **)
   1.417 +
   1.418 +(* add / del *)
   1.419 +
   1.420 +val simpN = "simp";
   1.421 +val congN = "cong";
   1.422 +val addN = "add";
   1.423 +val delN = "del";
   1.424 +val onlyN = "only";
   1.425 +val no_asmN = "no_asm";
   1.426 +val no_asm_useN = "no_asm_use";
   1.427 +val no_asm_simpN = "no_asm_simp";
   1.428 +val asm_lrN = "asm_lr";
   1.429 +
   1.430 +val simp_attr =
   1.431 + (Attrib.add_del_args simp_add_global simp_del_global,
   1.432 +  Attrib.add_del_args simp_add_local simp_del_local);
   1.433 +
   1.434 +val cong_attr =
   1.435 + (Attrib.add_del_args cong_add_global cong_del_global,
   1.436 +  Attrib.add_del_args cong_add_local cong_del_local);
   1.437 +
   1.438 +
   1.439 +(* conversions *)
   1.440 +
   1.441 +local
   1.442 +
   1.443 +fun conv_mode x =
   1.444 +  ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
   1.445 +    Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
   1.446 +    Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
   1.447 +    Scan.succeed asm_full_simplify) |> Scan.lift) x;
   1.448 +
   1.449 +fun simplified_att get args =
   1.450 +  Attrib.syntax (conv_mode -- args >> (fn (f, ths) =>
   1.451 +    Drule.rule_attribute (fn x => f ((if null ths then I else clear_ss) (get x) addsimps ths))));
   1.452 +
   1.453 +in
   1.454 +
   1.455 +val simplified_attr =
   1.456 + (simplified_att simpset_of Attrib.global_thmss,
   1.457 +  simplified_att local_simpset_of Attrib.local_thmss);
   1.458 +
   1.459 +end;
   1.460 +
   1.461 +
   1.462 +(* setup attributes *)
   1.463 +
   1.464 +val _ = Context.add_setup
   1.465 + [Attrib.add_attributes
   1.466 +   [(simpN, simp_attr, "declaration of simplification rule"),
   1.467 +    (congN, cong_attr, "declaration of Simplifier congruence rule"),
   1.468 +    ("simplified", simplified_attr, "simplified rule")]];
   1.469 +
   1.470 +
   1.471 +
   1.472 +(** proof methods **)
   1.473 +
   1.474 +(* simplification *)
   1.475 +
   1.476 +val simp_options =
   1.477 + (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   1.478 +  Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   1.479 +  Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
   1.480 +  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   1.481 +  Scan.succeed asm_full_simp_tac);
   1.482 +
   1.483 +val cong_modifiers =
   1.484 + [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
   1.485 +  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
   1.486 +  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
   1.487 +
   1.488 +val simp_modifiers =
   1.489 + [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
   1.490 +  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
   1.491 +  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
   1.492 +  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
   1.493 +   @ cong_modifiers;
   1.494 +
   1.495 +val simp_modifiers' =
   1.496 + [Args.add -- Args.colon >> K (I, simp_add_local),
   1.497 +  Args.del -- Args.colon >> K (I, simp_del_local),
   1.498 +  Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
   1.499 +   @ cong_modifiers;
   1.500 +
   1.501 +fun simp_args more_mods =
   1.502 +  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');
   1.503 +
   1.504 +
   1.505 +fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
   1.506 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN
   1.507 +    (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
   1.508 +
   1.509 +fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
   1.510 +  HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   1.511 +      (CHANGED_PROP oo tac) (local_simpset_of ctxt)));
   1.512 +
   1.513 +
   1.514 +(* setup methods *)
   1.515 +
   1.516 +fun setup_methods more_mods = Method.add_methods
   1.517 + [(simpN, simp_args more_mods simp_method', "simplification"),
   1.518 +  ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
   1.519 +
   1.520 +fun method_setup mods = [setup_methods mods];
   1.521 +
   1.522 +
   1.523 +(** easy_setup **)
   1.524 +
   1.525 +fun easy_setup reflect trivs =
   1.526 +  let
   1.527 +    val trivialities = Drule.reflexive_thm :: trivs;
   1.528 +
   1.529 +    fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
   1.530 +    val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   1.531 +
   1.532 +    (*no premature instantiation of variables during simplification*)
   1.533 +    fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
   1.534 +    val safe_solver = mk_solver "easy safe" safe_solver_tac;
   1.535 +
   1.536 +    fun mk_eq thm =
   1.537 +      if Logic.is_equals (Thm.concl_of thm) then [thm]
   1.538 +      else [thm RS reflect] handle THM _ => [];
   1.539 +
   1.540 +    fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
   1.541 +
   1.542 +    fun init_ss thy =
   1.543 +      (simpset_ref_of thy :=
   1.544 +        empty_ss setsubgoaler asm_simp_tac
   1.545 +        setSSolver safe_solver
   1.546 +        setSolver unsafe_solver
   1.547 +        setmksimps mksimps; thy);
   1.548 +  in method_setup [] @ [init_ss] end;
   1.549 +
   1.550 +end;
   1.551 +
   1.552 +structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
   1.553 +open BasicSimplifier;