src/Provers/clasimp.ML
author wenzelm
Sun, 13 Dec 2020 23:11:41 +0100
changeset 72907 3883f536d84d
parent 69593 3dda49e08b9d
permissions -rw-r--r--
unused (see 29566b6810f7);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
     1
(*  Title:      Provers/clasimp.ML
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
     2
    Author:     David von Oheimb, TU Muenchen
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
     3
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
     4
Combination of classical reasoner and simplifier (depends on
16019
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15570
diff changeset
     5
splitter.ML, classical.ML, blast.ML).
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
     6
*)
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
     7
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
     8
signature CLASIMP_DATA =
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
     9
sig
8469
482c301041b4 include Splitter.split_modifiers;
wenzelm
parents: 8168
diff changeset
    10
  structure Splitter: SPLITTER
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
    11
  structure Classical: CLASSICAL
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
    12
  structure Blast: BLAST
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    13
  val notE: thm
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    14
  val iffD1: thm
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    15
  val iffD2: thm
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    16
end;
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
    17
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    18
signature CLASIMP =
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    19
sig
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    20
  val addSss: Proof.context -> Proof.context
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    21
  val addss: Proof.context -> Proof.context
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    22
  val clarsimp_tac: Proof.context -> int -> tactic
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    23
  val mk_auto_tac: Proof.context -> int -> int -> tactic
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    24
  val auto_tac: Proof.context -> tactic
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    25
  val force_tac: Proof.context -> int -> tactic
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 43331
diff changeset
    26
  val fast_force_tac: Proof.context -> int -> tactic
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    27
  val slow_simp_tac: Proof.context -> int -> tactic
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    28
  val best_simp_tac: Proof.context -> int -> tactic
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    29
  val iff_add: attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    30
  val iff_add': attribute
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    31
  val iff_del: attribute
30513
1796b8ea88aa eliminated type Args.T;
wenzelm
parents: 30510
diff changeset
    32
  val iff_modifiers: Method.modifier parser list
1796b8ea88aa eliminated type Args.T;
wenzelm
parents: 30510
diff changeset
    33
  val clasimp_modifiers: Method.modifier parser list
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    34
end;
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    35
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    36
functor Clasimp(Data: CLASIMP_DATA): CLASIMP =
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    37
struct
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    38
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    39
structure Splitter = Data.Splitter;
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    40
structure Classical = Data.Classical;
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    41
structure Blast = Data.Blast;
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
    42
26497
1873915c64a9 purely functional setup of claset/simpset/clasimpset;
wenzelm
parents: 26425
diff changeset
    43
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    44
(* simp as classical wrapper *)
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    45
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51703
diff changeset
    46
(* FIXME !? *)
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51703
diff changeset
    47
fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    48
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    49
(*Add a simpset to the claset!*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    50
(*Caution: only one simpset added can be added by each of addSss and addss*)
50111
wenzelm
parents: 50107
diff changeset
    51
val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    52
val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    53
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    54
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    55
(* iffs: addition of rules to simpsets and clasets simultaneously *)
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    56
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    57
local
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    58
11344
57b7ad51971c streamlined addIffs/delIffs, added warnings
oheimb
parents: 11181
diff changeset
    59
(*Takes (possibly conditional) theorems of the form A<->B to
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    60
        the Safe Intr     rule B==>A and
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    61
        the Safe Destruct rule A==>B.
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    62
  Also ~A goes to the Safe Elim rule A ==> ?R
11462
cf3e7f5ad0e1 removed the warning from [iff]
paulson
parents: 11344
diff changeset
    63
  Failing other cases, A is added as a Safe Intr rule*)
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    64
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    65
fun add_iff safe unsafe =
60366
wenzelm
parents: 59582
diff changeset
    66
  Thm.declaration_attribute (fn th => fn context =>
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    67
    let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58826
diff changeset
    68
      val n = Thm.nprems_of th;
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    69
      val (elim, intro) = if n = 0 then safe else unsafe;
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    70
      val zero_rotate = zero_var_indexes o rotate_prems n;
60366
wenzelm
parents: 59582
diff changeset
    71
      val decls =
wenzelm
parents: 59582
diff changeset
    72
        [(intro, zero_rotate (th RS Data.iffD2)),
wenzelm
parents: 59582
diff changeset
    73
         (elim, Tactic.make_elim (zero_rotate (th RS Data.iffD1)))]
wenzelm
parents: 59582
diff changeset
    74
        handle THM _ => [(elim, zero_rotate (th RS Data.notE))]
wenzelm
parents: 59582
diff changeset
    75
        handle THM _ => [(intro, th)];
wenzelm
parents: 59582
diff changeset
    76
    in fold (uncurry Thm.attribute_declaration) decls context end);
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    77
60366
wenzelm
parents: 59582
diff changeset
    78
fun del_iff del = Thm.declaration_attribute (fn th => fn context =>
wenzelm
parents: 59582
diff changeset
    79
  let
wenzelm
parents: 59582
diff changeset
    80
    val zero_rotate = zero_var_indexes o rotate_prems (Thm.nprems_of th);
wenzelm
parents: 59582
diff changeset
    81
    val rls =
wenzelm
parents: 59582
diff changeset
    82
      [zero_rotate (th RS Data.iffD2), Tactic.make_elim (zero_rotate (th RS Data.iffD1))]
wenzelm
parents: 59582
diff changeset
    83
        handle THM _ => [zero_rotate (th RS Data.notE)]
wenzelm
parents: 59582
diff changeset
    84
        handle THM _ => [th];
wenzelm
parents: 59582
diff changeset
    85
  in fold (Thm.attribute_declaration del) rls context end);
18630
69fe387b3b6e generic attributes;
wenzelm
parents: 18529
diff changeset
    86
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    87
in
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    88
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    89
val iff_add =
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    90
  Thm.declaration_attribute (fn th =>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    91
    Thm.attribute_declaration (add_iff
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    92
      (Classical.safe_elim NONE, Classical.safe_intro NONE)
60943
7cf1ea00a020 tuned signature;
wenzelm
parents: 60366
diff changeset
    93
      (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    94
    #> Thm.attribute_declaration Simplifier.simp_add th);
10033
fc4e7432b2b1 added iff_add_global', iff_add_local' (syntax "iff?");
wenzelm
parents: 9952
diff changeset
    95
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    96
val iff_add' =
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    97
  add_iff
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    98
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    99
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
12375
539a32568db3 iff?: refer to Pure/ContextRules;
wenzelm
parents: 11902
diff changeset
   100
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   101
val iff_del =
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
   102
  Thm.declaration_attribute (fn th =>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
   103
    Thm.attribute_declaration (del_iff Classical.rule_del) th #>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
   104
    Thm.attribute_declaration (del_iff Context_Rules.rule_del) th #>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
   105
    Thm.attribute_declaration Simplifier.simp_del th);
12375
539a32568db3 iff?: refer to Pure/ContextRules;
wenzelm
parents: 11902
diff changeset
   106
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   107
end;
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   108
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   109
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   110
(* tactics *)
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   111
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   112
fun clarsimp_tac ctxt =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51703
diff changeset
   113
  Simplifier.safe_asm_full_simp_tac ctxt THEN_ALL_NEW
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   114
  Classical.clarify_tac (addSss ctxt);
12375
539a32568db3 iff?: refer to Pure/ContextRules;
wenzelm
parents: 11902
diff changeset
   115
5483
2fc3f4450fe8 added clarsimp_tac and Clarsimp_tac
oheimb
parents: 5219
diff changeset
   116
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   117
(* auto_tac *)
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   118
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   119
(* a variant of depth_tac that avoids interference of the simplifier
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   120
   with dup_step_tac when they are combined by auto_tac *)
5756
8ef5288c24b0 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5567
diff changeset
   121
local
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   122
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   123
fun slow_step_tac' ctxt =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   124
  Classical.appWrappers ctxt
60943
7cf1ea00a020 tuned signature;
wenzelm
parents: 60366
diff changeset
   125
    (Classical.instp_step_tac ctxt APPEND' Classical.unsafe_step_tac ctxt);
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   126
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   127
in
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   128
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   129
fun nodup_depth_tac ctxt m i st =
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   130
  SELECT_GOAL
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   131
    (Classical.safe_steps_tac ctxt 1 THEN_ELSE
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   132
      (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   133
        Classical.inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   134
          (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
42479
wenzelm
parents: 42478
diff changeset
   135
5756
8ef5288c24b0 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5567
diff changeset
   136
end;
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   137
43331
01f051619eee clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents: 42805
diff changeset
   138
(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   139
  in some of the subgoals*)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   140
fun mk_auto_tac ctxt m n =
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   141
  let
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   142
    val main_tac =
43331
01f051619eee clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
wenzelm
parents: 42805
diff changeset
   143
      Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   144
      ORELSE'
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   145
      (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   146
  in
58008
aa72531f972f added PARALLEL_ALLGOALS convenience;
wenzelm
parents: 54742
diff changeset
   147
    PARALLEL_ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   148
    TRY (Classical.safe_tac ctxt) THEN
42479
wenzelm
parents: 42478
diff changeset
   149
    REPEAT_DETERM (FIRSTGOAL main_tac) THEN
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   150
    TRY (Classical.safe_tac (addSss ctxt)) THEN
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 51717
diff changeset
   151
    prune_params_tac ctxt
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   152
  end;
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   153
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   154
fun auto_tac ctxt = mk_auto_tac ctxt 4 2;
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   155
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   156
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   157
(* force_tac *)
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   158
4659
a78ecc7341e3 added smart_tac
oheimb
parents: 4652
diff changeset
   159
(* aimed to solve the given subgoal totally, using whatever tools possible *)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   160
fun force_tac ctxt =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   161
  let val ctxt' = addss ctxt in
42479
wenzelm
parents: 42478
diff changeset
   162
    SELECT_GOAL
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   163
     (Classical.clarify_tac ctxt' 1 THEN
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51703
diff changeset
   164
      IF_UNSOLVED (Simplifier.asm_full_simp_tac ctxt 1) THEN
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   165
      ALLGOALS (Classical.first_best_tac ctxt'))
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   166
  end;
4659
a78ecc7341e3 added smart_tac
oheimb
parents: 4652
diff changeset
   167
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   168
9805
10b617bdd028 added "slowsimp", "bestsimp";
wenzelm
parents: 9772
diff changeset
   169
(* basic combinations *)
10b617bdd028 added "slowsimp", "bestsimp";
wenzelm
parents: 9772
diff changeset
   170
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 43331
diff changeset
   171
val fast_force_tac = Classical.fast_tac o addss;
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   172
val slow_simp_tac = Classical.slow_tac o addss;
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   173
val best_simp_tac = Classical.best_tac o addss;
9591
590d36e059d1 added "fastsimp";
wenzelm
parents: 9506
diff changeset
   174
47967
c422128d3889 discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents: 45375
diff changeset
   175
c422128d3889 discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents: 45375
diff changeset
   176
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   177
(** concrete syntax **)
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   178
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   179
(* attributes *)
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   180
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   181
val _ =
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   182
  Theory.setup
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 64556
diff changeset
   183
    (Attrib.setup \<^binding>\<open>iff\<close>
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   184
      (Scan.lift
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   185
        (Args.del >> K iff_del ||
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   186
          Scan.option Args.add -- Args.query >> K iff_add' ||
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   187
          Scan.option Args.add >> K iff_add))
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   188
      "declaration of Simplifier / Classical rules");
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   189
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   190
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   191
(* method modifiers *)
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   192
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   193
val iffN = "iff";
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   194
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   195
val iff_modifiers =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 60943
diff changeset
   196
 [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add \<^here>),
851ae0e7b09c more symbols;
wenzelm
parents: 60943
diff changeset
   197
  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' \<^here>),
851ae0e7b09c more symbols;
wenzelm
parents: 60943
diff changeset
   198
  Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del \<^here>)];
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   199
8469
482c301041b4 include Splitter.split_modifiers;
wenzelm
parents: 8168
diff changeset
   200
val clasimp_modifiers =
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   201
  Simplifier.simp_modifiers @ Splitter.split_modifiers @
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   202
  Classical.cla_modifiers @ iff_modifiers;
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   203
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   204
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   205
(* methods *)
5926
58f9ca06b76b method setup;
wenzelm
parents: 5756
diff changeset
   206
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   207
fun clasimp_method' tac =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   208
  Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   209
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   210
val auto_method =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36601
diff changeset
   211
  Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
35613
9d3ff36ad4e1 eliminated Args.bang_facts (legacy feature);
wenzelm
parents: 33369
diff changeset
   212
    Method.sections clasimp_modifiers >>
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   213
  (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   214
    | SOME (m, n) => (fn ctxt => SIMPLE_METHOD (CHANGED_PROP (mk_auto_tac ctxt m n))));
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   215
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   216
val _ =
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   217
  Theory.setup
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 64556
diff changeset
   218
   (Method.setup \<^binding>\<open>fastforce\<close> (clasimp_method' fast_force_tac) "combined fast and simp" #>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 64556
diff changeset
   219
    Method.setup \<^binding>\<open>slowsimp\<close> (clasimp_method' slow_simp_tac) "combined slow and simp" #>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 64556
diff changeset
   220
    Method.setup \<^binding>\<open>bestsimp\<close> (clasimp_method' best_simp_tac) "combined best and simp" #>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 64556
diff changeset
   221
    Method.setup \<^binding>\<open>force\<close> (clasimp_method' force_tac) "force" #>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 64556
diff changeset
   222
    Method.setup \<^binding>\<open>auto\<close> auto_method "auto" #>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 64556
diff changeset
   223
    Method.setup \<^binding>\<open>clarsimp\<close> (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 58048
diff changeset
   224
      "clarify simplified goal");
5926
58f9ca06b76b method setup;
wenzelm
parents: 5756
diff changeset
   225
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   226
end;