src/Pure/simplifier.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 32786 f1ac4b515af9
child 33092 c859019d3ac5
permissions -rw-r--r--
map_range (and map_index) combinator
wenzelm@16014
     1
(*  Title:      Pure/simplifier.ML
wenzelm@16014
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@16014
     3
wenzelm@16014
     4
Generic simplifier, suitable for most logics (see also
wenzelm@16014
     5
meta_simplifier.ML for the actual meta-level rewriting engine).
wenzelm@16014
     6
*)
wenzelm@16014
     7
wenzelm@16014
     8
signature BASIC_SIMPLIFIER =
wenzelm@16014
     9
sig
wenzelm@16014
    10
  include BASIC_META_SIMPLIFIER
wenzelm@17883
    11
  val change_simpset: (simpset -> simpset) -> unit
wenzelm@32148
    12
  val global_simpset_of: theory -> simpset
wenzelm@16014
    13
  val Addsimprocs: simproc list -> unit
wenzelm@16014
    14
  val Delsimprocs: simproc list -> unit
wenzelm@32148
    15
  val simpset_of: Proof.context -> simpset
wenzelm@17967
    16
  val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
wenzelm@16014
    17
  val safe_asm_full_simp_tac: simpset -> int -> tactic
wenzelm@16014
    18
  val               simp_tac: simpset -> int -> tactic
wenzelm@16014
    19
  val           asm_simp_tac: simpset -> int -> tactic
wenzelm@16014
    20
  val          full_simp_tac: simpset -> int -> tactic
wenzelm@16014
    21
  val        asm_lr_simp_tac: simpset -> int -> tactic
wenzelm@16014
    22
  val      asm_full_simp_tac: simpset -> int -> tactic
wenzelm@16014
    23
  val          simplify: simpset -> thm -> thm
wenzelm@16014
    24
  val      asm_simplify: simpset -> thm -> thm
wenzelm@16014
    25
  val     full_simplify: simpset -> thm -> thm
wenzelm@16014
    26
  val   asm_lr_simplify: simpset -> thm -> thm
wenzelm@16014
    27
  val asm_full_simplify: simpset -> thm -> thm
wenzelm@16014
    28
end;
wenzelm@16014
    29
wenzelm@16014
    30
signature SIMPLIFIER =
wenzelm@16014
    31
sig
wenzelm@16014
    32
  include BASIC_SIMPLIFIER
wenzelm@30356
    33
  val pretty_ss: Proof.context -> simpset -> Pretty.T
wenzelm@17004
    34
  val clear_ss: simpset -> simpset
wenzelm@32738
    35
  val debug_bounds: bool Unsynchronized.ref
wenzelm@17883
    36
  val inherit_context: simpset -> simpset -> simpset
wenzelm@17898
    37
  val the_context: simpset -> Proof.context
wenzelm@17898
    38
  val context: Proof.context -> simpset -> simpset
wenzelm@17898
    39
  val theory_context: theory  -> simpset -> simpset
wenzelm@16458
    40
  val simproc_i: theory -> string -> term list
wenzelm@16458
    41
    -> (theory -> simpset -> term -> thm option) -> simproc
wenzelm@16458
    42
  val simproc: theory -> string -> string list
wenzelm@16458
    43
    -> (theory -> simpset -> term -> thm option) -> simproc
wenzelm@23598
    44
  val          rewrite: simpset -> conv
wenzelm@23598
    45
  val      asm_rewrite: simpset -> conv
wenzelm@23598
    46
  val     full_rewrite: simpset -> conv
wenzelm@23598
    47
  val   asm_lr_rewrite: simpset -> conv
wenzelm@23598
    48
  val asm_full_rewrite: simpset -> conv
wenzelm@22379
    49
  val get_ss: Context.generic -> simpset
wenzelm@22379
    50
  val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
wenzelm@18728
    51
  val attrib: (simpset * thm list -> simpset) -> attribute
wenzelm@18728
    52
  val simp_add: attribute
wenzelm@18728
    53
  val simp_del: attribute
wenzelm@18728
    54
  val cong_add: attribute
wenzelm@18728
    55
  val cong_del: attribute
wenzelm@26497
    56
  val map_simpset: (simpset -> simpset) -> theory -> theory
wenzelm@24024
    57
  val get_simproc: Context.generic -> xstring -> simproc
wenzelm@22236
    58
  val def_simproc: {name: string, lhss: string list,
wenzelm@22236
    59
    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
wenzelm@22201
    60
    local_theory -> local_theory
wenzelm@22236
    61
  val def_simproc_i: {name: string, lhss: term list,
wenzelm@22236
    62
    proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
wenzelm@22201
    63
    local_theory -> local_theory
wenzelm@30513
    64
  val cong_modifiers: Method.modifier parser list
wenzelm@30513
    65
  val simp_modifiers': Method.modifier parser list
wenzelm@30513
    66
  val simp_modifiers: Method.modifier parser list
wenzelm@30513
    67
  val method_setup: Method.modifier parser list -> theory -> theory
wenzelm@18708
    68
  val easy_setup: thm -> thm list -> theory -> theory
wenzelm@16014
    69
end;
wenzelm@16014
    70
wenzelm@16014
    71
structure Simplifier: SIMPLIFIER =
wenzelm@16014
    72
struct
wenzelm@16014
    73
wenzelm@21708
    74
open MetaSimplifier;
wenzelm@21708
    75
wenzelm@21708
    76
wenzelm@30356
    77
(** pretty printing **)
wenzelm@30356
    78
wenzelm@30356
    79
fun pretty_ss ctxt ss =
wenzelm@30356
    80
  let
wenzelm@30356
    81
    val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
wenzelm@32091
    82
    val pretty_thm = Display.pretty_thm ctxt;
wenzelm@30356
    83
    fun pretty_proc (name, lhss) = Pretty.big_list (name ^ ":") (map pretty_cterm lhss);
wenzelm@30356
    84
    fun pretty_cong (name, thm) =
wenzelm@30356
    85
      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
wenzelm@30356
    86
wenzelm@30356
    87
    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
wenzelm@30356
    88
  in
wenzelm@30356
    89
    [Pretty.big_list "simplification rules:" (map (pretty_thm o #2) simps),
wenzelm@30356
    90
      Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
wenzelm@30356
    91
      Pretty.big_list "congruences:" (map pretty_cong congs),
wenzelm@30356
    92
      Pretty.strs ("loopers:" :: map quote loopers),
wenzelm@30356
    93
      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
wenzelm@30356
    94
      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
wenzelm@30356
    95
    |> Pretty.chunks
wenzelm@30356
    96
  end;
wenzelm@30356
    97
wenzelm@30356
    98
wenzelm@30356
    99
wenzelm@17883
   100
(** simpset data **)
wenzelm@16014
   101
wenzelm@26497
   102
structure SimpsetData = GenericDataFun
wenzelm@22846
   103
(
wenzelm@26497
   104
  type T = simpset;
wenzelm@26497
   105
  val empty = empty_ss;
wenzelm@26497
   106
  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
wenzelm@26497
   107
  fun merge _ = merge_ss;
wenzelm@22846
   108
);
wenzelm@16014
   109
wenzelm@26497
   110
val get_ss = SimpsetData.get;
wenzelm@26497
   111
val map_ss = SimpsetData.map;
wenzelm@26497
   112
wenzelm@26497
   113
wenzelm@26497
   114
(* attributes *)
wenzelm@26497
   115
wenzelm@26497
   116
fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));
wenzelm@16014
   117
wenzelm@26497
   118
val simp_add = attrib (op addsimps);
wenzelm@26497
   119
val simp_del = attrib (op delsimps);
wenzelm@26497
   120
val cong_add = attrib (op addcongs);
wenzelm@26497
   121
val cong_del = attrib (op delcongs);
wenzelm@26497
   122
wenzelm@16014
   123
wenzelm@26497
   124
(* global simpset *)
wenzelm@26497
   125
wenzelm@26497
   126
fun map_simpset f = Context.theory_map (map_ss f);
wenzelm@26497
   127
fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
wenzelm@32148
   128
fun global_simpset_of thy =
wenzelm@32148
   129
  MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
wenzelm@16014
   130
wenzelm@17883
   131
fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
wenzelm@17883
   132
fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
wenzelm@16014
   133
wenzelm@16014
   134
wenzelm@26497
   135
(* local simpset *)
wenzelm@16014
   136
wenzelm@32148
   137
fun simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
wenzelm@16014
   138
wenzelm@27338
   139
val _ = ML_Antiquote.value "simpset"
wenzelm@32148
   140
  (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
wenzelm@22132
   141
wenzelm@16014
   142
wenzelm@17967
   143
wenzelm@22201
   144
(** named simprocs **)
wenzelm@22201
   145
wenzelm@23655
   146
fun err_dup_simproc name = error ("Duplicate simproc: " ^ quote name);
wenzelm@22201
   147
wenzelm@22236
   148
wenzelm@22204
   149
(* data *)
wenzelm@22204
   150
wenzelm@22201
   151
structure Simprocs = GenericDataFun
wenzelm@22201
   152
(
wenzelm@22236
   153
  type T = simproc NameSpace.table;
wenzelm@22201
   154
  val empty = NameSpace.empty_table;
wenzelm@22201
   155
  val extend = I;
wenzelm@22236
   156
  fun merge _ simprocs = NameSpace.merge_tables eq_simproc simprocs
wenzelm@23655
   157
    handle Symtab.DUP dup => err_dup_simproc dup;
wenzelm@22201
   158
);
wenzelm@22201
   159
wenzelm@22204
   160
wenzelm@22204
   161
(* get simprocs *)
wenzelm@22204
   162
wenzelm@24024
   163
fun get_simproc context xname =
wenzelm@22204
   164
  let
wenzelm@24024
   165
    val (space, tab) = Simprocs.get context;
wenzelm@22204
   166
    val name = NameSpace.intern space xname;
wenzelm@22204
   167
  in
wenzelm@22204
   168
    (case Symtab.lookup tab name of
wenzelm@22236
   169
      SOME proc => proc
wenzelm@22204
   170
    | NONE => error ("Undefined simplification procedure: " ^ quote name))
wenzelm@22204
   171
  end;
wenzelm@22204
   172
wenzelm@27338
   173
val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
wenzelm@27338
   174
  "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
wenzelm@22204
   175
wenzelm@22204
   176
wenzelm@22204
   177
(* define simprocs *)
wenzelm@22201
   178
wenzelm@22201
   179
local
wenzelm@22201
   180
wenzelm@22236
   181
fun gen_simproc prep {name, lhss, proc, identifier} lthy =
wenzelm@22201
   182
  let
haftmann@28991
   183
    val b = Binding.name name;
wenzelm@22236
   184
    val naming = LocalTheory.full_naming lthy;
wenzelm@22236
   185
    val simproc = make_simproc
haftmann@28991
   186
      {name = LocalTheory.full_name lthy b,
wenzelm@22236
   187
       lhss =
wenzelm@22236
   188
        let
wenzelm@22236
   189
          val lhss' = prep lthy lhss;
wenzelm@22236
   190
          val ctxt' = lthy
wenzelm@22236
   191
            |> fold Variable.declare_term lhss'
wenzelm@22236
   192
            |> fold Variable.auto_fixes lhss';
wenzelm@22236
   193
        in Variable.export_terms ctxt' lthy lhss' end
wenzelm@22236
   194
        |> map (Thm.cterm_of (ProofContext.theory_of lthy)),
wenzelm@22236
   195
       proc = proc,
wenzelm@22236
   196
       identifier = identifier}
wenzelm@22236
   197
      |> morph_simproc (LocalTheory.target_morphism lthy);
wenzelm@22201
   198
  in
wenzelm@24024
   199
    lthy |> LocalTheory.declaration (fn phi =>
wenzelm@22201
   200
      let
haftmann@28991
   201
        val b' = Morphism.binding phi b;
wenzelm@22236
   202
        val simproc' = morph_simproc phi simproc;
wenzelm@22201
   203
      in
wenzelm@24024
   204
        Simprocs.map (fn simprocs =>
wenzelm@30466
   205
          NameSpace.define naming (b', simproc') simprocs |> snd
haftmann@28863
   206
            handle Symtab.DUP dup => err_dup_simproc dup)
wenzelm@24024
   207
        #> map_ss (fn ss => ss addsimprocs [simproc'])
wenzelm@22201
   208
      end)
wenzelm@22201
   209
  end;
wenzelm@22201
   210
wenzelm@22201
   211
in
wenzelm@22201
   212
wenzelm@24509
   213
val def_simproc = gen_simproc Syntax.read_terms;
wenzelm@24509
   214
val def_simproc_i = gen_simproc Syntax.check_terms;
wenzelm@22201
   215
wenzelm@22201
   216
end;
wenzelm@22201
   217
wenzelm@22201
   218
wenzelm@22201
   219
wenzelm@17967
   220
(** simplification tactics and rules **)
wenzelm@17967
   221
wenzelm@17967
   222
fun solve_all_tac solvers ss =
wenzelm@17967
   223
  let
wenzelm@30336
   224
    val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss;
wenzelm@17967
   225
    val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac);
wenzelm@17967
   226
  in DEPTH_SOLVE (solve_tac 1) end;
wenzelm@17967
   227
wenzelm@17967
   228
(*NOTE: may instantiate unknowns that appear also in other subgoals*)
wenzelm@17967
   229
fun generic_simp_tac safe mode ss =
wenzelm@17967
   230
  let
wenzelm@30336
   231
    val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss;
haftmann@21286
   232
    val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
wenzelm@17967
   233
    val solve_tac = FIRST' (map (MetaSimplifier.solver ss)
haftmann@22717
   234
      (rev (if safe then solvers else unsafe_solvers)));
wenzelm@17967
   235
wenzelm@17967
   236
    fun simp_loop_tac i =
wenzelm@23536
   237
      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
wenzelm@17967
   238
      (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
wenzelm@17967
   239
  in simp_loop_tac end;
wenzelm@17967
   240
wenzelm@17967
   241
local
wenzelm@17967
   242
wenzelm@17967
   243
fun simp rew mode ss thm =
wenzelm@17967
   244
  let
wenzelm@30336
   245
    val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss;
haftmann@22717
   246
    val tacf = solve_all_tac (rev unsafe_solvers);
wenzelm@17967
   247
    fun prover s th = Option.map #1 (Seq.pull (tacf s th));
wenzelm@17967
   248
  in rew mode prover ss thm end;
wenzelm@17967
   249
wenzelm@17967
   250
in
wenzelm@17967
   251
wenzelm@17967
   252
val simp_thm = simp MetaSimplifier.rewrite_thm;
wenzelm@17967
   253
val simp_cterm = simp MetaSimplifier.rewrite_cterm;
wenzelm@17967
   254
wenzelm@17967
   255
end;
wenzelm@17967
   256
wenzelm@17967
   257
wenzelm@16806
   258
(* tactics *)
wenzelm@16806
   259
wenzelm@16014
   260
val simp_tac = generic_simp_tac false (false, false, false);
wenzelm@16014
   261
val asm_simp_tac = generic_simp_tac false (false, true, false);
wenzelm@16014
   262
val full_simp_tac = generic_simp_tac false (true, false, false);
wenzelm@16014
   263
val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
wenzelm@16014
   264
val asm_full_simp_tac = generic_simp_tac false (true, true, true);
wenzelm@16014
   265
val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
wenzelm@16014
   266
wenzelm@16806
   267
wenzelm@16806
   268
(* conversions *)
wenzelm@16806
   269
wenzelm@17967
   270
val          simplify = simp_thm (false, false, false);
wenzelm@17967
   271
val      asm_simplify = simp_thm (false, true, false);
wenzelm@17967
   272
val     full_simplify = simp_thm (true, false, false);
wenzelm@17967
   273
val   asm_lr_simplify = simp_thm (true, true, false);
wenzelm@17967
   274
val asm_full_simplify = simp_thm (true, true, true);
wenzelm@16014
   275
wenzelm@17967
   276
val          rewrite = simp_cterm (false, false, false);
wenzelm@17967
   277
val      asm_rewrite = simp_cterm (false, true, false);
wenzelm@17967
   278
val     full_rewrite = simp_cterm (true, false, false);
wenzelm@17967
   279
val   asm_lr_rewrite = simp_cterm (true, true, false);
wenzelm@17967
   280
val asm_full_rewrite = simp_cterm (true, true, true);
wenzelm@16014
   281
wenzelm@16014
   282
wenzelm@16014
   283
wenzelm@16014
   284
(** concrete syntax of attributes **)
wenzelm@16014
   285
wenzelm@16014
   286
(* add / del *)
wenzelm@16014
   287
wenzelm@16014
   288
val simpN = "simp";
wenzelm@16014
   289
val congN = "cong";
wenzelm@16014
   290
val onlyN = "only";
wenzelm@16014
   291
val no_asmN = "no_asm";
wenzelm@16014
   292
val no_asm_useN = "no_asm_use";
wenzelm@16014
   293
val no_asm_simpN = "no_asm_simp";
wenzelm@16014
   294
val asm_lrN = "asm_lr";
wenzelm@16014
   295
wenzelm@16014
   296
wenzelm@24024
   297
(* simprocs *)
wenzelm@24024
   298
wenzelm@24024
   299
local
wenzelm@24024
   300
wenzelm@24024
   301
val add_del =
wenzelm@24024
   302
  (Args.del -- Args.colon >> K (op delsimprocs) ||
wenzelm@24024
   303
    Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
wenzelm@24024
   304
  >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
wenzelm@24024
   305
      (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
wenzelm@24024
   306
wenzelm@24024
   307
in
wenzelm@24024
   308
wenzelm@30528
   309
val simproc_att =
wenzelm@30528
   310
  Scan.peek (fn context =>
wenzelm@24024
   311
    add_del :|-- (fn decl =>
wenzelm@24024
   312
      Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
wenzelm@30528
   313
      >> (Library.apply o map Morphism.form)));
wenzelm@24024
   314
wenzelm@24024
   315
end;
wenzelm@24124
   316
wenzelm@24024
   317
wenzelm@16014
   318
(* conversions *)
wenzelm@16014
   319
wenzelm@16014
   320
local
wenzelm@16014
   321
wenzelm@16014
   322
fun conv_mode x =
wenzelm@16014
   323
  ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
wenzelm@16014
   324
    Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
wenzelm@16014
   325
    Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
wenzelm@16014
   326
    Scan.succeed asm_full_simplify) |> Scan.lift) x;
wenzelm@16014
   327
wenzelm@16014
   328
in
wenzelm@16014
   329
wenzelm@30528
   330
val simplified = conv_mode -- Attrib.thms >>
wenzelm@30528
   331
  (fn (f, ths) => Thm.rule_attribute (fn context =>
wenzelm@27021
   332
    f ((if null ths then I else MetaSimplifier.clear_ss)
wenzelm@32148
   333
        (simpset_of (Context.proof_of context)) addsimps ths)));
wenzelm@16014
   334
wenzelm@16014
   335
end;
wenzelm@16014
   336
wenzelm@16014
   337
wenzelm@16014
   338
(* setup attributes *)
wenzelm@16014
   339
wenzelm@26463
   340
val _ = Context.>> (Context.map_theory
wenzelm@30528
   341
 (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
wenzelm@30528
   342
    "declaration of Simplifier rewrite rule" #>
wenzelm@30528
   343
  Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
wenzelm@30528
   344
    "declaration of Simplifier congruence rule" #>
wenzelm@30528
   345
  Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
wenzelm@30528
   346
  Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
wenzelm@16014
   347
wenzelm@16014
   348
wenzelm@16014
   349
wenzelm@31300
   350
(** method syntax **)
wenzelm@16014
   351
wenzelm@16014
   352
val cong_modifiers =
wenzelm@18728
   353
 [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
wenzelm@18728
   354
  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
wenzelm@18728
   355
  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
wenzelm@16014
   356
wenzelm@16014
   357
val simp_modifiers =
wenzelm@18728
   358
 [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
wenzelm@18728
   359
  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
wenzelm@18728
   360
  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
wenzelm@17883
   361
  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon
wenzelm@26497
   362
    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
wenzelm@16014
   363
   @ cong_modifiers;
wenzelm@16014
   364
wenzelm@16014
   365
val simp_modifiers' =
wenzelm@18728
   366
 [Args.add -- Args.colon >> K (I, simp_add),
wenzelm@18728
   367
  Args.del -- Args.colon >> K (I, simp_del),
wenzelm@18688
   368
  Args.$$$ onlyN -- Args.colon
wenzelm@26497
   369
    >> K (Context.proof_map (map_ss MetaSimplifier.clear_ss), simp_add)]
wenzelm@16014
   370
   @ cong_modifiers;
wenzelm@16014
   371
wenzelm@31300
   372
val simp_options =
wenzelm@31300
   373
 (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
wenzelm@31300
   374
  Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
wenzelm@31300
   375
  Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
wenzelm@31300
   376
  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
wenzelm@31300
   377
  Scan.succeed asm_full_simp_tac);
wenzelm@16014
   378
wenzelm@31300
   379
fun simp_method more_mods meth =
wenzelm@31300
   380
  Args.bang_facts -- Scan.lift simp_options --|
wenzelm@31300
   381
    Method.sections (more_mods @ simp_modifiers') >>
wenzelm@31300
   382
    (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts)));
wenzelm@16014
   383
wenzelm@16014
   384
wenzelm@16014
   385
wenzelm@18708
   386
(** setup **)
wenzelm@18708
   387
wenzelm@31300
   388
fun method_setup more_mods =
wenzelm@31300
   389
  Method.setup (Binding.name simpN)
wenzelm@31300
   390
    (simp_method more_mods (fn ctxt => fn tac => fn facts =>
wenzelm@31300
   391
      HEADGOAL (Method.insert_tac facts THEN'
wenzelm@32148
   392
        (CHANGED_PROP oo tac) (simpset_of ctxt))))
wenzelm@31300
   393
    "simplification" #>
wenzelm@31300
   394
  Method.setup (Binding.name "simp_all")
wenzelm@31300
   395
    (simp_method more_mods (fn ctxt => fn tac => fn facts =>
wenzelm@31300
   396
      ALLGOALS (Method.insert_tac facts) THEN
wenzelm@32148
   397
        (CHANGED_PROP o ALLGOALS o tac) (simpset_of ctxt)))
wenzelm@31300
   398
    "simplification (all goals)";
wenzelm@16014
   399
wenzelm@26497
   400
fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
wenzelm@16014
   401
  let
wenzelm@16014
   402
    val trivialities = Drule.reflexive_thm :: trivs;
wenzelm@16014
   403
wenzelm@16014
   404
    fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
wenzelm@16014
   405
    val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
wenzelm@16014
   406
wenzelm@16014
   407
    (*no premature instantiation of variables during simplification*)
wenzelm@16014
   408
    fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
wenzelm@16014
   409
    val safe_solver = mk_solver "easy safe" safe_solver_tac;
wenzelm@16014
   410
wenzelm@16014
   411
    fun mk_eq thm =
wenzelm@20872
   412
      if can Logic.dest_equals (Thm.concl_of thm) then [thm]
wenzelm@16014
   413
      else [thm RS reflect] handle THM _ => [];
wenzelm@16014
   414
wenzelm@26653
   415
    fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
wenzelm@26497
   416
  in
wenzelm@26497
   417
    empty_ss setsubgoaler asm_simp_tac
wenzelm@26497
   418
    setSSolver safe_solver
wenzelm@26497
   419
    setSolver unsafe_solver
wenzelm@26497
   420
    setmksimps mksimps
wenzelm@26497
   421
  end));
wenzelm@16014
   422
wenzelm@16014
   423
end;
wenzelm@16014
   424
wenzelm@32738
   425
structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier;
wenzelm@32738
   426
open Basic_Simplifier;