src/Provers/clasimp.ML
author wenzelm
Wed, 23 May 2012 16:22:27 +0200
changeset 47967 c422128d3889
parent 45375 7fe19930dfc9
child 50107 289181e3e524
permissions -rw-r--r--
discontinued obsolete method fastsimp / tactic fast_simp_tac;
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
26497
1873915c64a9 purely functional setup of claset/simpset/clasimpset;
wenzelm
parents: 26425
diff changeset
    34
  val clasimp_setup: theory -> theory
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    35
end;
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    36
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    37
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
    38
struct
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    39
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    40
structure Splitter = Data.Splitter;
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    41
structure Classical = Data.Classical;
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    42
structure Blast = Data.Blast;
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
    43
26497
1873915c64a9 purely functional setup of claset/simpset/clasimpset;
wenzelm
parents: 26425
diff changeset
    44
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    45
(* simp as classical wrapper *)
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
    46
9402
480a1b40fdd6 strengthened force_tac by using new first_best_tac
oheimb
parents: 8639
diff changeset
    47
(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    48
val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
9402
480a1b40fdd6 strengthened force_tac by using new first_best_tac
oheimb
parents: 8639
diff changeset
    49
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    50
fun clasimp f name tac ctxt =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    51
  Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
    52
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    53
(*Add a simpset to the claset!*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    54
(*Caution: only one simpset added can be added by each of addSss and addss*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    55
val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
    56
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
    57
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    58
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    59
(* iffs: addition of rules to simpsets and clasets simultaneously *)
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    60
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    61
local
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    62
11344
57b7ad51971c streamlined addIffs/delIffs, added warnings
oheimb
parents: 11181
diff changeset
    63
(*Takes (possibly conditional) theorems of the form A<->B to
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    64
        the Safe Intr     rule B==>A and
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    65
        the Safe Destruct rule A==>B.
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    66
  Also ~A goes to the Safe Elim rule A ==> ?R
11462
cf3e7f5ad0e1 removed the warning from [iff]
paulson
parents: 11344
diff changeset
    67
  Failing other cases, A is added as a Safe Intr rule*)
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    68
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    69
fun add_iff safe unsafe =
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    70
  Thm.declaration_attribute (fn th =>
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    71
    let
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    72
      val n = nprems_of th;
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    73
      val (elim, intro) = if n = 0 then safe else unsafe;
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    74
      val zero_rotate = zero_var_indexes o rotate_prems n;
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    75
    in
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    76
      Thm.attribute_declaration intro (zero_rotate (th RS Data.iffD2)) #>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    77
      Thm.attribute_declaration elim (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    78
      handle THM _ =>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    79
        (Thm.attribute_declaration elim (zero_rotate (th RS Data.notE))
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    80
          handle THM _ => Thm.attribute_declaration intro th)
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    81
    end);
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    82
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    83
fun del_iff del = Thm.declaration_attribute (fn th =>
11902
db207d68392c iff: always rotate prems;
wenzelm
parents: 11496
diff changeset
    84
  let val zero_rotate = zero_var_indexes o rotate_prems (nprems_of th) in
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    85
    Thm.attribute_declaration del (zero_rotate (th RS Data.iffD2)) #>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    86
    Thm.attribute_declaration del (Tactic.make_elim (zero_rotate (th RS Data.iffD1)))
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    87
    handle THM _ =>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    88
      (Thm.attribute_declaration del (zero_rotate (th RS Data.notE))
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    89
        handle THM _ => Thm.attribute_declaration del th)
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    90
  end);
18630
69fe387b3b6e generic attributes;
wenzelm
parents: 18529
diff changeset
    91
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    92
in
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
    93
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
    94
val iff_add =
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    95
  Thm.declaration_attribute (fn th =>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    96
    Thm.attribute_declaration (add_iff
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    97
      (Classical.safe_elim NONE, Classical.safe_intro NONE)
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    98
      (Classical.haz_elim NONE, Classical.haz_intro NONE)) th
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
    99
    #> Thm.attribute_declaration Simplifier.simp_add th);
10033
fc4e7432b2b1 added iff_add_global', iff_add_local' (syntax "iff?");
wenzelm
parents: 9952
diff changeset
   100
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   101
val iff_add' =
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   102
  add_iff
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   103
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE)
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   104
    (Context_Rules.elim_query NONE, Context_Rules.intro_query NONE);
12375
539a32568db3 iff?: refer to Pure/ContextRules;
wenzelm
parents: 11902
diff changeset
   105
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   106
val iff_del =
45375
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
   107
  Thm.declaration_attribute (fn th =>
7fe19930dfc9 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents: 44890
diff changeset
   108
    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
   109
    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
   110
    Thm.attribute_declaration Simplifier.simp_del th);
12375
539a32568db3 iff?: refer to Pure/ContextRules;
wenzelm
parents: 11902
diff changeset
   111
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   112
end;
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   113
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   114
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   115
(* tactics *)
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   116
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   117
fun clarsimp_tac ctxt =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   118
  safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   119
  Classical.clarify_tac (addSss ctxt);
12375
539a32568db3 iff?: refer to Pure/ContextRules;
wenzelm
parents: 11902
diff changeset
   120
5483
2fc3f4450fe8 added clarsimp_tac and Clarsimp_tac
oheimb
parents: 5219
diff changeset
   121
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   122
(* auto_tac *)
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   123
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   124
(* a variant of depth_tac that avoids interference of the simplifier
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   125
   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
   126
local
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   127
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   128
fun slow_step_tac' ctxt =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   129
  Classical.appWrappers ctxt
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   130
    (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt);
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   131
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   132
in
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   133
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   134
fun nodup_depth_tac ctxt m i st =
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   135
  SELECT_GOAL
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   136
    (Classical.safe_steps_tac ctxt 1 THEN_ELSE
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   137
      (DEPTH_SOLVE (nodup_depth_tac ctxt m 1),
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   138
        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
   139
          (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (nodup_depth_tac ctxt (m - 1) 1)))) i st;
42479
wenzelm
parents: 42478
diff changeset
   140
5756
8ef5288c24b0 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5567
diff changeset
   141
end;
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   142
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
(*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
   144
  in some of the subgoals*)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   145
fun mk_auto_tac ctxt m n =
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   146
  let
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   147
    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
   148
      Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   149
      ORELSE'
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   150
      (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   151
  in
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   152
    PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   153
    TRY (Classical.safe_tac ctxt) THEN
42479
wenzelm
parents: 42478
diff changeset
   154
    REPEAT_DETERM (FIRSTGOAL main_tac) THEN
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   155
    TRY (Classical.safe_tac (addSss ctxt)) THEN
42479
wenzelm
parents: 42478
diff changeset
   156
    prune_params_tac
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   157
  end;
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   158
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   159
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
   160
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   161
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   162
(* force_tac *)
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   163
4659
a78ecc7341e3 added smart_tac
oheimb
parents: 4652
diff changeset
   164
(* aimed to solve the given subgoal totally, using whatever tools possible *)
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   165
fun force_tac ctxt =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   166
  let val ctxt' = addss ctxt in
42479
wenzelm
parents: 42478
diff changeset
   167
    SELECT_GOAL
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   168
     (Classical.clarify_tac ctxt' 1 THEN
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   169
      IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   170
      ALLGOALS (Classical.first_best_tac ctxt'))
42478
8a526c010c3b modernized Clasimp setup;
wenzelm
parents: 42373
diff changeset
   171
  end;
4659
a78ecc7341e3 added smart_tac
oheimb
parents: 4652
diff changeset
   172
5219
924359415f09 functorized Clasimp module;
wenzelm
parents: 4888
diff changeset
   173
9805
10b617bdd028 added "slowsimp", "bestsimp";
wenzelm
parents: 9772
diff changeset
   174
(* basic combinations *)
10b617bdd028 added "slowsimp", "bestsimp";
wenzelm
parents: 9772
diff changeset
   175
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 43331
diff changeset
   176
val fast_force_tac = Classical.fast_tac o addss;
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   177
val slow_simp_tac = Classical.slow_tac o addss;
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   178
val best_simp_tac = Classical.best_tac o addss;
9591
590d36e059d1 added "fastsimp";
wenzelm
parents: 9506
diff changeset
   179
47967
c422128d3889 discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents: 45375
diff changeset
   180
c422128d3889 discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents: 45375
diff changeset
   181
42784
a2dca9a3d0da simplified clasimpset declarations -- prefer attributes;
wenzelm
parents: 42479
diff changeset
   182
(** concrete syntax **)
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   183
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   184
(* attributes *)
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   185
30528
7173bf123335 simplified attribute setup;
wenzelm
parents: 30513
diff changeset
   186
fun iff_att x = (Scan.lift
18688
abf0f018b5ec generic attributes;
wenzelm
parents: 18630
diff changeset
   187
 (Args.del >> K iff_del ||
abf0f018b5ec generic attributes;
wenzelm
parents: 18630
diff changeset
   188
  Scan.option Args.add -- Args.query >> K iff_add' ||
30528
7173bf123335 simplified attribute setup;
wenzelm
parents: 30513
diff changeset
   189
  Scan.option Args.add >> K iff_add)) x;
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   190
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   191
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   192
(* method modifiers *)
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   193
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   194
val iffN = "iff";
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   195
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   196
val iff_modifiers =
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   197
 [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   198
  Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   199
  Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   200
8469
482c301041b4 include Splitter.split_modifiers;
wenzelm
parents: 8168
diff changeset
   201
val clasimp_modifiers =
9860
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   202
  Simplifier.simp_modifiers @ Splitter.split_modifiers @
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   203
  Classical.cla_modifiers @ iff_modifiers;
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   204
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   205
5c5efed691b9 added 'iff' declarations;
wenzelm
parents: 9805
diff changeset
   206
(* methods *)
5926
58f9ca06b76b method setup;
wenzelm
parents: 5756
diff changeset
   207
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   208
fun clasimp_method' tac =
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   209
  Method.sections clasimp_modifiers >> K (SIMPLE_METHOD' o tac);
9772
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   210
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   211
val auto_method =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36601
diff changeset
   212
  Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
35613
9d3ff36ad4e1 eliminated Args.bang_facts (legacy feature);
wenzelm
parents: 33369
diff changeset
   213
    Method.sections clasimp_modifiers >>
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   214
  (fn NONE => SIMPLE_METHOD o CHANGED_PROP o auto_tac
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42784
diff changeset
   215
    | 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
   216
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   217
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   218
(* theory setup *)
c07777210a69 auto method: opt args;
wenzelm
parents: 9591
diff changeset
   219
26497
1873915c64a9 purely functional setup of claset/simpset/clasimpset;
wenzelm
parents: 26425
diff changeset
   220
val clasimp_setup =
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   221
  Attrib.setup @{binding iff} iff_att "declaration of Simplifier / Classical rules" #>
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 43331
diff changeset
   222
  Method.setup @{binding fastforce} (clasimp_method' fast_force_tac) "combined fast and simp" #>
30541
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   223
  Method.setup @{binding slowsimp} (clasimp_method' slow_simp_tac) "combined slow and simp" #>
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   224
  Method.setup @{binding bestsimp} (clasimp_method' best_simp_tac) "combined best and simp" #>
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   225
  Method.setup @{binding force} (clasimp_method' force_tac) "force" #>
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   226
  Method.setup @{binding auto} auto_method "auto" #>
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   227
  Method.setup @{binding clarsimp} (clasimp_method' (CHANGED_PROP oo clarsimp_tac))
9f168bdc468a simplified method setup;
wenzelm
parents: 30528
diff changeset
   228
    "clarify simplified goal";
5926
58f9ca06b76b method setup;
wenzelm
parents: 5756
diff changeset
   229
4652
d24cca140eeb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
oheimb
parents:
diff changeset
   230
end;