src/Provers/simplifier.ML
author skalberg
Fri Jun 25 14:30:55 2004 +0200 (2004-06-25 ago)
changeset 15006 107e4dfd3b96
parent 14814 c6b91c8aee1d
child 15024 341cd221c3e1
permissions -rw-r--r--
Merging the meta-simplifier with the Provers-simplifier. Next step:
make the simplification procedure simpset-aware.
clasohm@1243
     1
(*  Title:      Provers/simplifier.ML
nipkow@1
     2
    ID:         $Id$
wenzelm@3557
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
nipkow@1
     4
berghofe@10412
     5
Generic simplifier, suitable for most logics.  See Pure/meta_simplifier.ML
berghofe@10412
     6
for the actual meta-level rewriting engine.
nipkow@1
     7
*)
clasohm@1260
     8
wenzelm@4795
     9
signature BASIC_SIMPLIFIER =
clasohm@0
    10
sig
skalberg@15006
    11
  type simproc = MetaSimplifier.simproc
wenzelm@3577
    12
  val mk_simproc: string -> cterm list
wenzelm@3577
    13
    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
skalberg@15006
    14
  type solver = MetaSimplifier.solver
nipkow@7568
    15
  val mk_solver: string -> (thm list -> int -> tactic) -> solver
skalberg@15006
    16
  type simpset = MetaSimplifier.simpset
wenzelm@2503
    17
  val empty_ss: simpset
wenzelm@3551
    18
  val rep_ss: simpset ->
wenzelm@11669
    19
   {mss: MetaSimplifier.meta_simpset,
wenzelm@9715
    20
    mk_cong: thm -> thm,
wenzelm@9715
    21
    subgoal_tac: simpset -> int -> tactic,
wenzelm@9715
    22
    loop_tacs: (string * (int -> tactic)) list,
nipkow@7568
    23
    unsafe_solvers: solver list,
wenzelm@9715
    24
    solvers: solver list};
wenzelm@3551
    25
  val print_ss: simpset -> unit
wenzelm@4366
    26
  val print_simpset: theory -> unit
oheimb@2629
    27
  val setsubgoaler: simpset *  (simpset -> int -> tactic) -> simpset
oheimb@2629
    28
  val setloop:      simpset *             (int -> tactic) -> simpset
nipkow@4668
    29
  val addloop:      simpset *  (string * (int -> tactic)) -> simpset
nipkow@4682
    30
  val delloop:      simpset *   string                    -> simpset
nipkow@7568
    31
  val setSSolver:   simpset * solver -> simpset
nipkow@7568
    32
  val addSSolver:   simpset * solver -> simpset
nipkow@7568
    33
  val setSolver:    simpset * solver -> simpset
nipkow@7568
    34
  val addSolver:    simpset * solver -> simpset
wenzelm@3577
    35
  val setmksimps:   simpset * (thm -> thm list) -> simpset
nipkow@4677
    36
  val setmkeqTrue:  simpset * (thm -> thm option) -> simpset
wenzelm@9715
    37
  val setmkcong:    simpset * (thm -> thm) -> simpset
nipkow@4677
    38
  val setmksym:     simpset * (thm -> thm option) -> simpset
wenzelm@3577
    39
  val settermless:  simpset * (term * term -> bool) -> simpset
wenzelm@3577
    40
  val addsimps:     simpset * thm list -> simpset
wenzelm@3577
    41
  val delsimps:     simpset * thm list -> simpset
wenzelm@3577
    42
  val addeqcongs:   simpset * thm list -> simpset
wenzelm@3577
    43
  val deleqcongs:   simpset * thm list -> simpset
wenzelm@9715
    44
  val addcongs:     simpset * thm list -> simpset
wenzelm@9715
    45
  val delcongs:     simpset * thm list -> simpset
wenzelm@3577
    46
  val addsimprocs:  simpset * simproc list -> simpset
wenzelm@3577
    47
  val delsimprocs:  simpset * simproc list -> simpset
wenzelm@3577
    48
  val merge_ss:     simpset * simpset -> simpset
wenzelm@3577
    49
  val prems_of_ss:  simpset -> thm list
wenzelm@4080
    50
  val simpset_ref_of_sg: Sign.sg -> simpset ref
wenzelm@4080
    51
  val simpset_ref_of: theory -> simpset ref
wenzelm@4080
    52
  val simpset_of_sg: Sign.sg -> simpset
wenzelm@4080
    53
  val simpset_of: theory -> simpset
wenzelm@4080
    54
  val SIMPSET: (simpset -> tactic) -> tactic
wenzelm@4080
    55
  val SIMPSET': (simpset -> 'a -> tactic) -> 'a -> tactic
wenzelm@4080
    56
  val simpset: unit -> simpset
wenzelm@4080
    57
  val simpset_ref: unit -> simpset ref
clasohm@1243
    58
  val Addsimps: thm list -> unit
clasohm@1243
    59
  val Delsimps: thm list -> unit
wenzelm@2509
    60
  val Addsimprocs: simproc list -> unit
wenzelm@2509
    61
  val Delsimprocs: simproc list -> unit
wenzelm@9715
    62
  val Addcongs: thm list -> unit
wenzelm@9715
    63
  val Delcongs: thm list -> unit
wenzelm@8879
    64
  val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
wenzelm@10004
    65
  val safe_asm_full_simp_tac: simpset -> int -> tactic
oheimb@2629
    66
  val               simp_tac: simpset -> int -> tactic
oheimb@2629
    67
  val           asm_simp_tac: simpset -> int -> tactic
oheimb@2629
    68
  val          full_simp_tac: simpset -> int -> tactic
nipkow@4722
    69
  val        asm_lr_simp_tac: simpset -> int -> tactic
oheimb@2629
    70
  val      asm_full_simp_tac: simpset -> int -> tactic
oheimb@2629
    71
  val               Simp_tac:            int -> tactic
oheimb@2629
    72
  val           Asm_simp_tac:            int -> tactic
oheimb@2629
    73
  val          Full_simp_tac:            int -> tactic
nipkow@4722
    74
  val        Asm_lr_simp_tac:            int -> tactic
oheimb@2629
    75
  val      Asm_full_simp_tac:            int -> tactic
wenzelm@3557
    76
  val          simplify: simpset -> thm -> thm
wenzelm@3557
    77
  val      asm_simplify: simpset -> thm -> thm
wenzelm@3557
    78
  val     full_simplify: simpset -> thm -> thm
schirmer@14814
    79
  val   asm_lr_simplify: simpset -> thm -> thm
wenzelm@3557
    80
  val asm_full_simplify: simpset -> thm -> thm
clasohm@0
    81
end;
clasohm@0
    82
wenzelm@4795
    83
signature SIMPLIFIER =
wenzelm@4795
    84
sig
wenzelm@4795
    85
  include BASIC_SIMPLIFIER
wenzelm@13475
    86
  val simproc: Sign.sg -> string -> string list
wenzelm@13475
    87
    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
wenzelm@13475
    88
  val simproc_i: Sign.sg -> string -> term list
wenzelm@13475
    89
    -> (Sign.sg -> thm list -> term -> thm option) -> simproc
wenzelm@5082
    90
  val          rewrite: simpset -> cterm -> thm
wenzelm@5082
    91
  val      asm_rewrite: simpset -> cterm -> thm
wenzelm@5082
    92
  val     full_rewrite: simpset -> cterm -> thm
schirmer@14814
    93
  val   asm_lr_rewrite: simpset -> cterm -> thm
wenzelm@5082
    94
  val asm_full_rewrite: simpset -> cterm -> thm
wenzelm@5842
    95
  val print_local_simpset: Proof.context -> unit
wenzelm@5842
    96
  val get_local_simpset: Proof.context -> simpset
wenzelm@5842
    97
  val put_local_simpset: simpset -> Proof.context -> Proof.context
wenzelm@8467
    98
  val change_global_ss: (simpset * thm list -> simpset) -> theory attribute
wenzelm@8467
    99
  val change_local_ss: (simpset * thm list -> simpset) -> Proof.context attribute
wenzelm@4855
   100
  val simp_add_global: theory attribute
wenzelm@4855
   101
  val simp_del_global: theory attribute
wenzelm@5842
   102
  val simp_add_local: Proof.context attribute
wenzelm@5842
   103
  val simp_del_local: Proof.context attribute
wenzelm@9715
   104
  val cong_add_global: theory attribute
wenzelm@9715
   105
  val cong_del_global: theory attribute
wenzelm@9715
   106
  val cong_add_local: Proof.context attribute
wenzelm@9715
   107
  val cong_del_local: Proof.context attribute
wenzelm@7177
   108
  val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
wenzelm@7273
   109
  val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
wenzelm@5842
   110
  val setup: (theory -> theory) list
wenzelm@8467
   111
  val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
wenzelm@8467
   112
    -> (theory -> theory) list
wenzelm@8228
   113
  val easy_setup: thm -> thm list -> (theory -> theory) list
wenzelm@4795
   114
end;
wenzelm@2503
   115
wenzelm@2503
   116
structure Simplifier: SIMPLIFIER =
clasohm@0
   117
struct
clasohm@0
   118
skalberg@15006
   119
(* Compatibility *)
skalberg@15006
   120
open MetaSimplifier;
wenzelm@8467
   121
wenzelm@5024
   122
(** global and local simpset data **)
wenzelm@4080
   123
wenzelm@5842
   124
(* theory data kind 'Provers/simpset' *)
wenzelm@4795
   125
wenzelm@5842
   126
structure GlobalSimpsetArgs =
wenzelm@5024
   127
struct
wenzelm@5842
   128
  val name = "Provers/simpset";
wenzelm@5024
   129
  type T = simpset ref;
clasohm@0
   130
wenzelm@5024
   131
  val empty = ref empty_ss;
wenzelm@6556
   132
  fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
wenzelm@6556
   133
  val prep_ext = copy;
wenzelm@5024
   134
  fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
wenzelm@5024
   135
  fun print _ (ref ss) = print_ss ss;
wenzelm@5024
   136
end;
wenzelm@4080
   137
wenzelm@5842
   138
structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
wenzelm@5842
   139
val print_simpset = GlobalSimpset.print;
wenzelm@5842
   140
val simpset_ref_of_sg = GlobalSimpset.get_sg;
wenzelm@5842
   141
val simpset_ref_of = GlobalSimpset.get;
wenzelm@4080
   142
wenzelm@4080
   143
wenzelm@4795
   144
(* access global simpset *)
clasohm@0
   145
wenzelm@4080
   146
val simpset_of_sg = ! o simpset_ref_of_sg;
wenzelm@6391
   147
val simpset_of = simpset_of_sg o Theory.sign_of;
wenzelm@4080
   148
wenzelm@6391
   149
fun SIMPSET tacf state = tacf (simpset_of_sg (Thm.sign_of_thm state)) state;
wenzelm@6391
   150
fun SIMPSET' tacf i state = tacf (simpset_of_sg (Thm.sign_of_thm state)) i state;
clasohm@0
   151
wenzelm@5028
   152
val simpset = simpset_of o Context.the_context;
wenzelm@6391
   153
val simpset_ref = simpset_ref_of_sg o Theory.sign_of o Context.the_context;
wenzelm@4080
   154
wenzelm@4080
   155
wenzelm@4795
   156
(* change global simpset *)
wenzelm@4080
   157
wenzelm@7177
   158
fun change_simpset_of f x thy =
wenzelm@7177
   159
  let val r = simpset_ref_of thy
wenzelm@7177
   160
  in r := f (! r, x); thy end;
wenzelm@7177
   161
wenzelm@7177
   162
fun change_simpset f x = (change_simpset_of f x (Context.the_context ()); ());
wenzelm@4080
   163
wenzelm@4080
   164
val Addsimps = change_simpset (op addsimps);
wenzelm@4080
   165
val Delsimps = change_simpset (op delsimps);
wenzelm@4080
   166
val Addsimprocs = change_simpset (op addsimprocs);
wenzelm@4080
   167
val Delsimprocs = change_simpset (op delsimprocs);
wenzelm@9715
   168
val Addcongs = change_simpset (op addcongs);
wenzelm@9715
   169
val Delcongs = change_simpset (op delcongs);
wenzelm@2509
   170
clasohm@0
   171
wenzelm@5842
   172
(* proof data kind 'Provers/simpset' *)
wenzelm@4795
   173
wenzelm@5842
   174
structure LocalSimpsetArgs =
wenzelm@5842
   175
struct
wenzelm@5842
   176
  val name = "Provers/simpset";
wenzelm@5842
   177
  type T = simpset;
wenzelm@5842
   178
  val init = simpset_of;
wenzelm@5842
   179
  fun print _ ss = print_ss ss;
wenzelm@5842
   180
end;
wenzelm@4795
   181
wenzelm@5842
   182
structure LocalSimpset = ProofDataFun(LocalSimpsetArgs);
wenzelm@5842
   183
val print_local_simpset = LocalSimpset.print;
wenzelm@5842
   184
val get_local_simpset = LocalSimpset.get;
wenzelm@5842
   185
val put_local_simpset = LocalSimpset.put;
wenzelm@7273
   186
fun map_local_simpset f ctxt = put_local_simpset (f (get_local_simpset ctxt)) ctxt;
wenzelm@4795
   187
wenzelm@4795
   188
wenzelm@5886
   189
(* attributes *)
wenzelm@5886
   190
wenzelm@5886
   191
fun change_global_ss f (thy, th) =
wenzelm@5886
   192
  let val r = simpset_ref_of thy
wenzelm@6096
   193
  in r := f (! r, [th]); (thy, th) end;
wenzelm@5886
   194
wenzelm@5886
   195
fun change_local_ss f (ctxt, th) =
wenzelm@6096
   196
  let val ss = f (get_local_simpset ctxt, [th])
wenzelm@5886
   197
  in (put_local_simpset ss ctxt, th) end;
wenzelm@5886
   198
wenzelm@5886
   199
val simp_add_global = change_global_ss (op addsimps);
wenzelm@5886
   200
val simp_del_global = change_global_ss (op delsimps);
wenzelm@5886
   201
val simp_add_local = change_local_ss (op addsimps);
wenzelm@5886
   202
val simp_del_local = change_local_ss (op delsimps);
wenzelm@5886
   203
wenzelm@9715
   204
val cong_add_global = change_global_ss (op addcongs);
wenzelm@9715
   205
val cong_del_global = change_global_ss (op delcongs);
wenzelm@9715
   206
val cong_add_local = change_local_ss (op addcongs);
wenzelm@9715
   207
val cong_del_local = change_local_ss (op delcongs);
wenzelm@9715
   208
wenzelm@5886
   209
wenzelm@10004
   210
val simp_tac = generic_simp_tac false (false, false, false);
wenzelm@10004
   211
val asm_simp_tac = generic_simp_tac false (false, true, false);
wenzelm@10004
   212
val full_simp_tac = generic_simp_tac false (true, false, false);
wenzelm@10004
   213
val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
wenzelm@10004
   214
val asm_full_simp_tac = generic_simp_tac false (true, true, true);
wenzelm@10004
   215
val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);
clasohm@0
   216
oheimb@2629
   217
skalberg@15006
   218
wenzelm@4795
   219
(*the abstraction over the proof state delays the dereferencing*)
wenzelm@4080
   220
fun          Simp_tac i st =          simp_tac (simpset ()) i st;
wenzelm@4080
   221
fun      Asm_simp_tac i st =      asm_simp_tac (simpset ()) i st;
wenzelm@4080
   222
fun     Full_simp_tac i st =     full_simp_tac (simpset ()) i st;
nipkow@4722
   223
fun   Asm_lr_simp_tac i st =   asm_lr_simp_tac (simpset ()) i st;
wenzelm@4080
   224
fun Asm_full_simp_tac i st = asm_full_simp_tac (simpset ()) i st;
nipkow@406
   225
wenzelm@5082
   226
val          simplify = simp_thm (false, false, false);
wenzelm@5082
   227
val      asm_simplify = simp_thm (false, true, false);
wenzelm@5082
   228
val     full_simplify = simp_thm (true, false, false);
schirmer@14814
   229
val   asm_lr_simplify = simp_thm (true, true, false);
schirmer@14814
   230
val asm_full_simplify = simp_thm (true, true, true);
wenzelm@5082
   231
wenzelm@5082
   232
val          rewrite = simp_cterm (false, false, false);
wenzelm@5082
   233
val      asm_rewrite = simp_cterm (false, true, false);
wenzelm@5082
   234
val     full_rewrite = simp_cterm (true, false, false);
schirmer@14814
   235
val   asm_lr_rewrite = simp_cterm (true, true, false);
schirmer@14814
   236
val asm_full_rewrite = simp_cterm (true, true, true);
wenzelm@3557
   237
wenzelm@3557
   238
wenzelm@4795
   239
wenzelm@5886
   240
(** concrete syntax of attributes **)
wenzelm@5842
   241
wenzelm@5886
   242
(* add / del *)
wenzelm@5842
   243
wenzelm@5928
   244
val simpN = "simp";
wenzelm@9715
   245
val congN = "cong";
berghofe@10412
   246
val addN = "add";
berghofe@10412
   247
val delN = "del";
wenzelm@6911
   248
val onlyN = "only";
wenzelm@9899
   249
val no_asmN = "no_asm";
wenzelm@9899
   250
val no_asm_useN = "no_asm_use";
wenzelm@9899
   251
val no_asm_simpN = "no_asm_simp";
berghofe@13605
   252
val asm_lrN = "asm_lr";
wenzelm@5842
   253
wenzelm@8634
   254
val simp_attr =
wenzelm@8634
   255
 (Attrib.add_del_args simp_add_global simp_del_global,
wenzelm@8634
   256
  Attrib.add_del_args simp_add_local simp_del_local);
wenzelm@5842
   257
wenzelm@9715
   258
val cong_attr =
wenzelm@9715
   259
 (Attrib.add_del_args cong_add_global cong_del_global,
wenzelm@9715
   260
  Attrib.add_del_args cong_add_local cong_del_local);
wenzelm@9715
   261
wenzelm@5842
   262
wenzelm@5842
   263
(* conversions *)
wenzelm@5842
   264
wenzelm@9899
   265
local
wenzelm@9899
   266
wenzelm@9899
   267
fun conv_mode x =
wenzelm@9899
   268
  ((Args.parens (Args.$$$ no_asmN) >> K simplify ||
wenzelm@9899
   269
    Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify ||
wenzelm@9899
   270
    Args.parens (Args.$$$ no_asm_useN) >> K full_simplify ||
wenzelm@9899
   271
    Scan.succeed asm_full_simplify) |> Scan.lift) x;
wenzelm@9899
   272
wenzelm@11938
   273
fun simplified_att get args =
wenzelm@11938
   274
  Attrib.syntax (conv_mode -- args >> (fn (f, ths) =>
wenzelm@11938
   275
    Drule.rule_attribute (fn x => f ((if null ths then I else clear_ss) (get x) addsimps ths))));
wenzelm@9899
   276
wenzelm@9899
   277
in
wenzelm@9899
   278
wenzelm@9899
   279
val simplified_attr =
wenzelm@11938
   280
 (simplified_att simpset_of Attrib.global_thmss,
wenzelm@11938
   281
  simplified_att get_local_simpset Attrib.local_thmss);
wenzelm@9899
   282
wenzelm@9899
   283
end;
wenzelm@5842
   284
wenzelm@5842
   285
wenzelm@5842
   286
(* setup_attrs *)
wenzelm@5842
   287
wenzelm@5842
   288
val setup_attrs = Attrib.add_attributes
wenzelm@9899
   289
 [(simpN, simp_attr, "declaration of simplification rule"),
wenzelm@9899
   290
  (congN, cong_attr, "declaration of Simplifier congruence rule"),
wenzelm@9899
   291
  ("simplified", simplified_attr, "simplified rule")];
wenzelm@5842
   292
wenzelm@5842
   293
wenzelm@5842
   294
wenzelm@5842
   295
(** proof methods **)
wenzelm@5842
   296
wenzelm@5842
   297
(* simplification *)
wenzelm@5842
   298
wenzelm@8700
   299
val simp_options =
wenzelm@9899
   300
 (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
wenzelm@9899
   301
  Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
wenzelm@9899
   302
  Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
berghofe@13605
   303
  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
wenzelm@8700
   304
  Scan.succeed asm_full_simp_tac);
wenzelm@8700
   305
wenzelm@9715
   306
val cong_modifiers =
wenzelm@9720
   307
 [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
wenzelm@10034
   308
  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
wenzelm@10034
   309
  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
wenzelm@9715
   310
wenzelm@5928
   311
val simp_modifiers =
wenzelm@8815
   312
 [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
wenzelm@10034
   313
  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
wenzelm@10034
   314
  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
wenzelm@9861
   315
  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
wenzelm@9861
   316
   @ cong_modifiers;
wenzelm@5928
   317
wenzelm@5928
   318
val simp_modifiers' =
wenzelm@10034
   319
 [Args.add -- Args.colon >> K (I, simp_add_local),
wenzelm@10034
   320
  Args.del -- Args.colon >> K (I, simp_del_local),
wenzelm@9861
   321
  Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
wenzelm@9861
   322
   @ cong_modifiers;
wenzelm@5928
   323
wenzelm@8700
   324
fun simp_args more_mods =
wenzelm@8700
   325
  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');
wenzelm@8700
   326
wenzelm@8170
   327
wenzelm@8700
   328
fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
wenzelm@8700
   329
  ALLGOALS (Method.insert_tac (prems @ facts)) THEN
wenzelm@10821
   330
    (CHANGED_PROP o ALLGOALS o tac) (get_local_simpset ctxt));
wenzelm@8700
   331
wenzelm@8700
   332
fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
wenzelm@10821
   333
  HEADGOAL (Method.insert_tac (prems @ facts) THEN'
wenzelm@10821
   334
      (CHANGED_PROP oo tac) (get_local_simpset ctxt)));
wenzelm@9715
   335
wenzelm@5842
   336
wenzelm@5842
   337
(* setup_methods *)
wenzelm@5842
   338
wenzelm@8467
   339
fun setup_methods more_mods = Method.add_methods
wenzelm@8700
   340
 [(simpN, simp_args more_mods simp_method', "simplification"),
wenzelm@8700
   341
  ("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
wenzelm@5842
   342
wenzelm@5842
   343
wenzelm@5842
   344
wenzelm@4795
   345
(** theory setup **)
wenzelm@4795
   346
wenzelm@8467
   347
val setup = [GlobalSimpset.init, LocalSimpset.init, setup_attrs];
wenzelm@8467
   348
fun method_setup mods = [setup_methods mods];
wenzelm@4795
   349
wenzelm@8228
   350
fun easy_setup reflect trivs =
wenzelm@8228
   351
  let
wenzelm@8228
   352
    val trivialities = Drule.reflexive_thm :: trivs;
wenzelm@8228
   353
wenzelm@8228
   354
    fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac];
wenzelm@8228
   355
    val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
wenzelm@8228
   356
wenzelm@8228
   357
    (*no premature instantiation of variables during simplification*)
wenzelm@8228
   358
    fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac];
wenzelm@8228
   359
    val safe_solver = mk_solver "easy safe" safe_solver_tac;
wenzelm@8228
   360
wenzelm@8243
   361
    fun mk_eq thm =
wenzelm@8228
   362
      if Logic.is_equals (Thm.concl_of thm) then [thm]
wenzelm@8228
   363
      else [thm RS reflect] handle THM _ => [];
wenzelm@8228
   364
wenzelm@8243
   365
    fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
wenzelm@8243
   366
wenzelm@8228
   367
    fun init_ss thy =
wenzelm@8228
   368
      (simpset_ref_of thy :=
wenzelm@8228
   369
        empty_ss setsubgoaler asm_simp_tac
wenzelm@8228
   370
        setSSolver safe_solver
wenzelm@8228
   371
        setSolver unsafe_solver
wenzelm@8228
   372
        setmksimps mksimps; thy);
wenzelm@8467
   373
  in setup @ method_setup [] @ [init_ss] end;
wenzelm@8228
   374
wenzelm@4795
   375
wenzelm@8667
   376
wenzelm@8667
   377
(** outer syntax **)
wenzelm@8667
   378
wenzelm@8667
   379
val print_simpsetP =
wenzelm@8667
   380
  OuterSyntax.improper_command "print_simpset" "print context of Simplifier"
wenzelm@8667
   381
    OuterSyntax.Keyword.diag
wenzelm@9513
   382
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep
wenzelm@9010
   383
      (Toplevel.node_case print_simpset (print_local_simpset o Proof.context_of)))));
wenzelm@8667
   384
wenzelm@8667
   385
val _ = OuterSyntax.add_parsers [print_simpsetP];
wenzelm@8667
   386
clasohm@1243
   387
end;
wenzelm@4795
   388
wenzelm@4795
   389
wenzelm@4795
   390
structure BasicSimplifier: BASIC_SIMPLIFIER = Simplifier;
wenzelm@4795
   391
open BasicSimplifier;