src/Provers/clasimp.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 64556 851ae0e7b09c
child 69593 3dda49e08b9d
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@9772
     1
(*  Title:      Provers/clasimp.ML
oheimb@4652
     2
    Author:     David von Oheimb, TU Muenchen
oheimb@4652
     3
wenzelm@5219
     4
Combination of classical reasoner and simplifier (depends on
wenzelm@16019
     5
splitter.ML, classical.ML, blast.ML).
oheimb@4652
     6
*)
oheimb@4652
     7
wenzelm@5219
     8
signature CLASIMP_DATA =
wenzelm@5219
     9
sig
wenzelm@8469
    10
  structure Splitter: SPLITTER
wenzelm@5219
    11
  structure Classical: CLASSICAL
wenzelm@5219
    12
  structure Blast: BLAST
wenzelm@9860
    13
  val notE: thm
wenzelm@9860
    14
  val iffD1: thm
wenzelm@9860
    15
  val iffD2: thm
wenzelm@42784
    16
end;
wenzelm@5219
    17
oheimb@4652
    18
signature CLASIMP =
oheimb@4652
    19
sig
wenzelm@42793
    20
  val addSss: Proof.context -> Proof.context
wenzelm@42793
    21
  val addss: Proof.context -> Proof.context
wenzelm@42793
    22
  val clarsimp_tac: Proof.context -> int -> tactic
wenzelm@42793
    23
  val mk_auto_tac: Proof.context -> int -> int -> tactic
wenzelm@42793
    24
  val auto_tac: Proof.context -> tactic
wenzelm@42793
    25
  val force_tac: Proof.context -> int -> tactic
nipkow@44890
    26
  val fast_force_tac: Proof.context -> int -> tactic
wenzelm@42793
    27
  val slow_simp_tac: Proof.context -> int -> tactic
wenzelm@42793
    28
  val best_simp_tac: Proof.context -> int -> tactic
wenzelm@18728
    29
  val iff_add: attribute
wenzelm@18728
    30
  val iff_add': attribute
wenzelm@18728
    31
  val iff_del: attribute
wenzelm@30513
    32
  val iff_modifiers: Method.modifier parser list
wenzelm@30513
    33
  val clasimp_modifiers: Method.modifier parser list
oheimb@4652
    34
end;
oheimb@4652
    35
wenzelm@42478
    36
functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
oheimb@4652
    37
struct
oheimb@4652
    38
wenzelm@42478
    39
structure Splitter = Data.Splitter;
wenzelm@42478
    40
structure Classical = Data.Classical;
wenzelm@42478
    41
structure Blast = Data.Blast;
wenzelm@5219
    42
wenzelm@26497
    43
wenzelm@42784
    44
(* simp as classical wrapper *)
oheimb@4652
    45
wenzelm@51717
    46
(* FIXME !? *)
wenzelm@51717
    47
fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
wenzelm@42478
    48
wenzelm@42793
    49
(*Add a simpset to the claset!*)
wenzelm@42793
    50
(*Caution: only one simpset added can be added by each of addSss and addss*)
wenzelm@50111
    51
val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
wenzelm@42793
    52
val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
oheimb@4652
    53
wenzelm@42784
    54
wenzelm@9860
    55
(* iffs: addition of rules to simpsets and clasets simultaneously *)
wenzelm@9860
    56
wenzelm@42784
    57
local
wenzelm@42784
    58
oheimb@11344
    59
(*Takes (possibly conditional) theorems of the form A<->B to
wenzelm@9860
    60
        the Safe Intr     rule B==>A and
wenzelm@9860
    61
        the Safe Destruct rule A==>B.
wenzelm@9860
    62
  Also ~A goes to the Safe Elim rule A ==> ?R
paulson@11462
    63
  Failing other cases, A is added as a Safe Intr rule*)
wenzelm@9860
    64
wenzelm@42784
    65
fun add_iff safe unsafe =
wenzelm@60366
    66
  Thm.declaration_attribute (fn th => fn context =>
wenzelm@42784
    67
    let
wenzelm@59582
    68
      val n = Thm.nprems_of th;
wenzelm@42784
    69
      val (elim, intro) = if n = 0 then safe else unsafe;
wenzelm@42784
    70
      val zero_rotate = zero_var_indexes o rotate_prems n;
wenzelm@60366
    71
      val decls =
wenzelm@60366
    72
        [(intro, zero_rotate (th RS Data.iffD2)),
wenzelm@60366
    73
         (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))]
wenzelm@60366
    74
        handle THM _ => [(elim, zero_rotate (th RS Data.notE))]
wenzelm@60366
    75
        handle THM _ => [(intro, th)];
wenzelm@60366
    76
    in fold (uncurry Thm.attribute_declaration) decls context end);
wenzelm@42784
    77
wenzelm@60366
    78
fun del_iff del = Thm.declaration_attribute (fn th => fn context =>
wenzelm@60366
    79
  let
wenzelm@60366
    80
    val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th);
wenzelm@60366
    81
    val rls =
wenzelm@60366
    82
      [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))]
wenzelm@60366
    83
        handle THM _ => [zero_rotate (th RS Data.notE)]
wenzelm@60366
    84
        handle THM _ => [th];
wenzelm@60366
    85
  in fold (Thm.attribute_declaration del) rls context end);
wenzelm@18630
    86
wenzelm@9860
    87
in
wenzelm@9860
    88
wenzelm@42784
    89
val iff_add =
wenzelm@45375
    90
  Thm.declaration_attribute (fn th =>
wenzelm@45375
    91
    Thm.attribute_declaration (add_iff
wenzelm@45375
    92
      (Classical.safe_elim NONE, Classical.safe_intro NONE)
wenzelm@60943
    93
      (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th
wenzelm@45375
    94
    #> Thm.attribute_declaration Simplifier.simp_add th);
wenzelm@10033
    95
wenzelm@42784
    96
val iff_add' =
wenzelm@42784
    97
  add_iff
wenzelm@42784
    98
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
wenzelm@42784
    99
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
wenzelm@12375
   100
wenzelm@42784
   101
val iff_del =
wenzelm@45375
   102
  Thm.declaration_attribute (fn th =>
wenzelm@45375
   103
    Thm.attribute_declaration (del_iff Classical.rule_del) th #>
wenzelm@45375
   104
    Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
wenzelm@45375
   105
    Thm.attribute_declaration Simplifier.simp_del th);
wenzelm@12375
   106
wenzelm@9860
   107
end;
wenzelm@9860
   108
wenzelm@9860
   109
wenzelm@42478
   110
(* tactics *)
wenzelm@5219
   111
wenzelm@42793
   112
fun clarsimp_tac ctxt =
wenzelm@51717
   113
  Simplifier.safe_asm_full_simp_tac ctxt THEN_ALL_NEW
wenzelm@42793
   114
  Classical.clarify_tac (addSss ctxt);
wenzelm@12375
   115
oheimb@5483
   116
wenzelm@5219
   117
(* auto_tac *)
oheimb@4652
   118
wenzelm@9772
   119
(* a variant of depth_tac that avoids interference of the simplifier
wenzelm@5219
   120
   with dup_step_tac when they are combined by auto_tac *)
oheimb@5756
   121
local
wenzelm@42478
   122
wenzelm@42793
   123
fun slow_step_tac' ctxt =
wenzelm@42793
   124
  Classical.appWrappers ctxt
wenzelm@60943
   125
    (Classical.instp_step_tac ctxt APPEND' Classical.unsafe_step_tac ctxt);
wenzelm@42478
   126
wenzelm@42478
   127
in
wenzelm@42478
   128
wenzelm@42793
   129
fun nodup_depth_tac ctxt m i st =
wenzelm@42478
   130
  SELECT_GOAL
wenzelm@42793
   131
    (Classical.safe_steps_tac ctxt 1 THEN_ELSE
wenzelm@42793
   132
      (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
wenzelm@42793
   133
        Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
wenzelm@42793
   134
          (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
wenzelm@42479
   135
oheimb@5756
   136
end;
oheimb@4652
   137
wenzelm@43331
   138
(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
oheimb@4652
   139
  in some of the subgoals*)
wenzelm@42793
   140
fun mk_auto_tac ctxt m n =
wenzelm@42478
   141
  let
wenzelm@42478
   142
    val main_tac =
wenzelm@43331
   143
      Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
wenzelm@42478
   144
      ORELSE'
wenzelm@42793
   145
      (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
wenzelm@42478
   146
  in
wenzelm@58008
   147
    PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN
wenzelm@42793
   148
    TRY (Classical.safe_tac ctxt) THEN
wenzelm@42479
   149
    REPEAT_DETERM (FIRSTGOAL main_tac) THEN
wenzelm@42793
   150
    TRY (Classical.safe_tac (addSss ctxt)) THEN
wenzelm@54742
   151
    prune_params_tac ctxt
wenzelm@42478
   152
  end;
oheimb@4652
   153
wenzelm@42793
   154
fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
oheimb@4652
   155
wenzelm@9772
   156
wenzelm@5219
   157
(* force_tac *)
wenzelm@5219
   158
oheimb@4659
   159
(* aimed to solve the given subgoal totally, using whatever tools possible *)
wenzelm@42793
   160
fun force_tac ctxt =
wenzelm@42793
   161
  let val ctxt' = addss ctxt in
wenzelm@42479
   162
    SELECT_GOAL
wenzelm@42793
   163
     (Classical.clarify_tac ctxt' 1 THEN
wenzelm@51717
   164
      IF_UNSOLVED (Simplifier.asm_full_simp_tac ctxt 1) THEN
wenzelm@42793
   165
      ALLGOALS (Classical.first_best_tac ctxt'))
wenzelm@42478
   166
  end;
oheimb@4659
   167
wenzelm@5219
   168
wenzelm@9805
   169
(* basic combinations *)
wenzelm@9805
   170
nipkow@44890
   171
val fast_force_tac = Classical.fast_tac o addss;
wenzelm@42793
   172
val slow_simp_tac = Classical.slow_tac o addss;
wenzelm@42793
   173
val best_simp_tac = Classical.best_tac o addss;
wenzelm@9591
   174
wenzelm@47967
   175
wenzelm@47967
   176
wenzelm@42784
   177
(** concrete syntax **)
wenzelm@9860
   178
wenzelm@9860
   179
(* attributes *)
wenzelm@9860
   180
wenzelm@58826
   181
val _ =
wenzelm@58826
   182
  Theory.setup
wenzelm@58826
   183
    (Attrib.setup @{binding iff}
wenzelm@58826
   184
      (Scan.lift
wenzelm@58826
   185
        (Args.del >> K iff_del ||
wenzelm@58826
   186
          Scan.option Args.add -- Args.query >> K iff_add' ||
wenzelm@58826
   187
          Scan.option Args.add >> K iff_add))
wenzelm@58826
   188
      "declaration of Simplifier / Classical rules");
wenzelm@9860
   189
wenzelm@9860
   190
wenzelm@9860
   191
(* method modifiers *)
wenzelm@9860
   192
wenzelm@9860
   193
val iffN = "iff";
wenzelm@9860
   194
wenzelm@9860
   195
val iff_modifiers =
wenzelm@64556
   196
 [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
wenzelm@64556
   197
  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>),
wenzelm@64556
   198
  Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
wenzelm@9860
   199
wenzelm@8469
   200
val clasimp_modifiers =
wenzelm@9860
   201
  Simplifier.simp_modifiers @ Splitter.split_modifiers @
wenzelm@9860
   202
  Classical.cla_modifiers @ iff_modifiers;
wenzelm@9860
   203
wenzelm@9860
   204
wenzelm@9860
   205
(* methods *)
wenzelm@5926
   206
wenzelm@30541
   207
fun clasimp_method' tac =
wenzelm@42793
   208
  Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
wenzelm@9772
   209
wenzelm@30541
   210
val auto_method =
wenzelm@36960
   211
  Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
wenzelm@35613
   212
    Method.sections clasimp_modifiers >>
wenzelm@42793
   213
  (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
wenzelm@42793
   214
    | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
wenzelm@9772
   215
wenzelm@58826
   216
val _ =
wenzelm@58826
   217
  Theory.setup
wenzelm@58826
   218
   (Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
wenzelm@58826
   219
    Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
wenzelm@58826
   220
    Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
wenzelm@58826
   221
    Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
wenzelm@58826
   222
    Method.setup @{binding auto} auto_method "auto" #>
wenzelm@58826
   223
    Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
wenzelm@58826
   224
      "clarify simplified goal");
wenzelm@5926
   225
oheimb@4652
   226
end;