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