src/Pure/Isar/method.ML
author wenzelm
Mon, 31 Mar 2014 12:35:39 +0200
changeset 56334 6b3739fee456
parent 56278 2576d3a40ed6
child 56500 90f17a04567d
permissions -rw-r--r--
some shortcuts for chunks, which sometimes avoid bulky string output;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/method.ML
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
     3
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
     4
Isar proof methods.
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
     5
*)
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
     6
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
     7
signature METHOD =
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
     8
sig
30508
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
     9
  type method
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
    10
  val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
18227
d4cfa0fee007 moved multi_resolve(s) to drule.ML;
wenzelm
parents: 18145
diff changeset
    11
  val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    12
  val RAW_METHOD: (thm list -> tactic) -> method
18227
d4cfa0fee007 moved multi_resolve(s) to drule.ML;
wenzelm
parents: 18145
diff changeset
    13
  val METHOD_CASES: (thm list -> cases_tactic) -> method
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    14
  val METHOD: (thm list -> tactic) -> method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    15
  val fail: method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    16
  val succeed: method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    17
  val insert_tac: thm list -> int -> tactic
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    18
  val insert: thm list -> method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    19
  val insert_facts: method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    20
  val SIMPLE_METHOD: tactic -> method
21592
8831206d7f41 renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
wenzelm
parents: 21579
diff changeset
    21
  val SIMPLE_METHOD': (int -> tactic) -> method
8831206d7f41 renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
wenzelm
parents: 21579
diff changeset
    22
  val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
    23
  val cheating: Proof.context -> bool -> method
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    24
  val intro: thm list -> method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    25
  val elim: thm list -> method
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    26
  val unfold: thm list -> Proof.context -> method
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    27
  val fold: thm list -> Proof.context -> method
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    28
  val atomize: bool -> Proof.context -> method
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    29
  val this: method
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    30
  val fact: thm list -> Proof.context -> method
30234
7dd251bce291 renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
wenzelm
parents: 30190
diff changeset
    31
  val assm_tac: Proof.context -> int -> tactic
30567
cd8e20f86795 close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;
wenzelm
parents: 30544
diff changeset
    32
  val all_assm_tac: Proof.context -> tactic
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    33
  val assumption: Proof.context -> method
46466
61c7214b4885 tuned signature, according to actual usage of these operations;
wenzelm
parents: 45375
diff changeset
    34
  val rule_trace: bool Config.T
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    35
  val trace: Proof.context -> thm list -> unit
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    36
  val rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    37
  val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
25270
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
    38
  val intros_tac: thm list -> thm list -> tactic
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 33522
diff changeset
    39
  val try_intros_tac: thm list -> thm list -> tactic
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    40
  val rule: Proof.context -> thm list -> method
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    41
  val erule: Proof.context -> int -> thm list -> method
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    42
  val drule: Proof.context -> int -> thm list -> method
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
    43
  val frule: Proof.context -> int -> thm list -> method
27235
134991516430 ML tactic: do not abstract over context again;
wenzelm
parents: 26892
diff changeset
    44
  val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
    45
  val tactic: Symbol_Pos.source -> Proof.context -> method
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
    46
  val raw_tactic: Symbol_Pos.source -> Proof.context -> method
27729
aaf08262b177 tuned signature;
wenzelm
parents: 27383
diff changeset
    47
  type src = Args.src
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    48
  type combinator_info
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    49
  val no_combinator_info: combinator_info
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    50
  datatype text =
55742
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
    51
    Source of src |
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
    52
    Basic of Proof.context -> method |
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    53
    Then of combinator_info * text list |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    54
    Orelse of combinator_info * text list |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    55
    Try of combinator_info * text |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    56
    Repeat1 of combinator_info * text |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    57
    Select_Goals of combinator_info * int * text
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    58
  val primitive_text: (Proof.context -> thm -> thm) -> text
17857
810a67ecbc64 added primitive_text, succeed_text;
wenzelm
parents: 17756
diff changeset
    59
  val succeed_text: text
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    60
  val default_text: text
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    61
  val this_text: text
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    62
  val done_text: text
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
    63
  val sorry_text: bool -> text
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
    64
  val finish_text: text option * bool -> text
55742
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
    65
  val print_methods: Proof.context -> unit
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
    66
  val check_name: Proof.context -> xstring * Position.T -> string
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
    67
  val method: Proof.context -> src -> Proof.context -> method
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
    68
  val method_cmd: Proof.context -> src -> Proof.context -> method
30512
17b2aad869fa added simplified setup;
wenzelm
parents: 30508
diff changeset
    69
  val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
    70
  val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
30540
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
    71
  type modifier = (Proof.context -> Proof.context) * attribute
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
    72
  val section: modifier parser list -> thm list context_parser
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
    73
  val sections: modifier parser list -> thm list list context_parser
49889
00ea087e83d8 more method position information, notably finished_pos after end of previous text;
wenzelm
parents: 49866
diff changeset
    74
  type text_range = text * Position.range
00ea087e83d8 more method position information, notably finished_pos after end of previous text;
wenzelm
parents: 49866
diff changeset
    75
  val text: text_range option -> text option
00ea087e83d8 more method position information, notably finished_pos after end of previous text;
wenzelm
parents: 49866
diff changeset
    76
  val position: text_range option -> Position.T
55795
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
    77
  val reports_of: text_range -> Position.report list
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
    78
  val report: text_range -> unit
55761
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
    79
  val parse: text_range parser
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    80
end;
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    81
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    82
structure Method: METHOD =
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    83
struct
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    84
12324
5db4b4596d1a rule context and attributes moved to rule_context.ML;
wenzelm
parents: 12311
diff changeset
    85
(** proof methods **)
5db4b4596d1a rule context and attributes moved to rule_context.ML;
wenzelm
parents: 12311
diff changeset
    86
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    87
(* datatype method *)
11731
1a0c1ef86518 added trace_rules, trace;
wenzelm
parents: 10907
diff changeset
    88
18227
d4cfa0fee007 moved multi_resolve(s) to drule.ML;
wenzelm
parents: 18145
diff changeset
    89
datatype method = Meth of thm list -> cases_tactic;
11731
1a0c1ef86518 added trace_rules, trace;
wenzelm
parents: 10907
diff changeset
    90
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
    91
fun apply meth ctxt = let val Meth m = meth ctxt in m end;
11731
1a0c1ef86518 added trace_rules, trace;
wenzelm
parents: 10907
diff changeset
    92
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17587
diff changeset
    93
val RAW_METHOD_CASES = Meth;
11731
1a0c1ef86518 added trace_rules, trace;
wenzelm
parents: 10907
diff changeset
    94
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    95
fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
12144
f84eb7334d04 added RAW_METHOD, RAW_METHOD_CASES;
wenzelm
parents: 12119
diff changeset
    96
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    97
fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21592
diff changeset
    98
  Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts));
8372
7b2cec1e789c added METHOD_CASES, resolveq_cases_tac;
wenzelm
parents: 8351
diff changeset
    99
21687
f689f729afab reorganized structure Goal vs. Tactic;
wenzelm
parents: 21592
diff changeset
   100
fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Goal.conjunction_tac THEN tac facts);
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   101
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   102
val fail = METHOD (K no_tac);
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   103
val succeed = METHOD (K all_tac);
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   104
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   105
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   106
(* insert facts *)
7419
wenzelm
parents: 7367
diff changeset
   107
wenzelm
parents: 7367
diff changeset
   108
local
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   109
21579
abd2b4386a63 COMP_INCR;
wenzelm
parents: 20335
diff changeset
   110
fun cut_rule_tac rule =
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   111
  rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
6981
eaade7e398a7 export assumption_tac;
wenzelm
parents: 6951
diff changeset
   112
7419
wenzelm
parents: 7367
diff changeset
   113
in
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   114
51552
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents: 51383
diff changeset
   115
fun insert_tac [] _ = all_tac
7419
wenzelm
parents: 7367
diff changeset
   116
  | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
6981
eaade7e398a7 export assumption_tac;
wenzelm
parents: 6951
diff changeset
   117
7555
dd281afb33d7 setup for refined facts handling;
wenzelm
parents: 7526
diff changeset
   118
val insert_facts = METHOD (ALLGOALS o insert_tac);
7664
c151ac595551 insert: ignore facts;
wenzelm
parents: 7611
diff changeset
   119
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
7419
wenzelm
parents: 7367
diff changeset
   120
9706
8e48a19fc81e removed METHOD0;
wenzelm
parents: 9653
diff changeset
   121
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
21592
8831206d7f41 renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
wenzelm
parents: 21579
diff changeset
   122
fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
8831206d7f41 renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
wenzelm
parents: 21579
diff changeset
   123
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
9706
8e48a19fc81e removed METHOD0;
wenzelm
parents: 9653
diff changeset
   124
12324
5db4b4596d1a rule context and attributes moved to rule_context.ML;
wenzelm
parents: 12311
diff changeset
   125
end;
5db4b4596d1a rule context and attributes moved to rule_context.ML;
wenzelm
parents: 12311
diff changeset
   126
9706
8e48a19fc81e removed METHOD0;
wenzelm
parents: 9653
diff changeset
   127
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   128
(* cheating *)
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   129
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
   130
fun cheating ctxt int = METHOD (fn _ => fn st =>
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
   131
  if int orelse Config.get ctxt quick_and_dirty then
51552
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents: 51383
diff changeset
   132
    ALLGOALS Skip_Proof.cheat_tac st
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents: 51383
diff changeset
   133
  else error "Cheating requires quick_and_dirty mode!");
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   134
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   135
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   136
(* unfold intro/elim rules *)
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   137
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   138
fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   139
fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   140
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   141
12384
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   142
(* unfold/fold definitions *)
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   143
35624
c4e29a0bb8c1 modernized structure Local_Defs;
wenzelm
parents: 33522
diff changeset
   144
fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths));
c4e29a0bb8c1 modernized structure Local_Defs;
wenzelm
parents: 33522
diff changeset
   145
fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths));
6532
9d79a304aecc fold / unfold methods;
wenzelm
parents: 6500
diff changeset
   146
12384
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   147
12829
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   148
(* atomize rule statements *)
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   149
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   150
fun atomize false ctxt =
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   151
      SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   152
  | atomize true ctxt =
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   153
      RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)));
12829
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   154
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   155
18039
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   156
(* this -- resolve facts directly *)
12384
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   157
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   158
val this = METHOD (EVERY o map (HEADGOAL o rtac));
9484
3bda55143260 (un)fold: CHANGED;
wenzelm
parents: 9418
diff changeset
   159
3bda55143260 (un)fold: CHANGED;
wenzelm
parents: 9418
diff changeset
   160
18039
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   161
(* fact -- composition by facts from context *)
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   162
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   163
fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt)
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   164
  | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules);
18039
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   165
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   166
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   167
(* assumption *)
7419
wenzelm
parents: 7367
diff changeset
   168
wenzelm
parents: 7367
diff changeset
   169
local
wenzelm
parents: 7367
diff changeset
   170
19778
f0a318495ca4 assm_tac: try rule termI;
wenzelm
parents: 19482
diff changeset
   171
fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
f0a318495ca4 assm_tac: try rule termI;
wenzelm
parents: 19482
diff changeset
   172
  if cond (Logic.strip_assums_concl prop)
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   173
  then rtac rule i else no_tac);
7419
wenzelm
parents: 7367
diff changeset
   174
29857
2cc976ed8a3c FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents: 29301
diff changeset
   175
in
2cc976ed8a3c FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents: 29301
diff changeset
   176
30234
7dd251bce291 renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
wenzelm
parents: 30190
diff changeset
   177
fun assm_tac ctxt =
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   178
  assume_tac APPEND'
23349
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   179
  Goal.assume_rule_tac ctxt APPEND'
19778
f0a318495ca4 assm_tac: try rule termI;
wenzelm
parents: 19482
diff changeset
   180
  cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
f0a318495ca4 assm_tac: try rule termI;
wenzelm
parents: 19482
diff changeset
   181
  cond_rtac (can Logic.dest_term) Drule.termI;
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   182
49846
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   183
fun all_assm_tac ctxt =
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   184
  let
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   185
    fun tac i st =
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   186
      if i > Thm.nprems_of st then all_tac st
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   187
      else ((assm_tac ctxt i THEN tac i) ORELSE tac (i + 1)) st;
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   188
  in tac 1 end;
30567
cd8e20f86795 close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce) -- NB: ALLGOALS/THEN_ALL_NEW operate from right to left;
wenzelm
parents: 30544
diff changeset
   189
23349
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   190
fun assumption ctxt = METHOD (HEADGOAL o
30234
7dd251bce291 renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
wenzelm
parents: 30190
diff changeset
   191
  (fn [] => assm_tac ctxt
23349
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   192
    | [fact] => solve_tac [fact]
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   193
    | _ => K no_tac));
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   194
49846
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   195
fun finish immed ctxt =
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   196
  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac));
7419
wenzelm
parents: 7367
diff changeset
   197
wenzelm
parents: 7367
diff changeset
   198
end;
wenzelm
parents: 7367
diff changeset
   199
wenzelm
parents: 7367
diff changeset
   200
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   201
(* rule etc. -- single-step refinements *)
12347
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   202
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   203
val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
12347
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   204
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   205
fun trace ctxt rules =
41379
b31d7a1cd08f configuration option "rule_trace";
wenzelm
parents: 39507
diff changeset
   206
  if Config.get ctxt rule_trace andalso not (null rules) then
51584
98029ceda8ce more item markup;
wenzelm
parents: 51552
diff changeset
   207
    Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21879
diff changeset
   208
    |> Pretty.string_of |> tracing
279b129498b6 removed conditional combinator;
wenzelm
parents: 21879
diff changeset
   209
  else ();
12347
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   210
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   211
local
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   212
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   213
fun gen_rule_tac tac ctxt rules facts =
18841
edecd40194c1 method (un)folded: option '(raw)';
wenzelm
parents: 18824
diff changeset
   214
  (fn i => fn st =>
edecd40194c1 method (un)folded: option '(raw)';
wenzelm
parents: 18824
diff changeset
   215
    if null facts then tac rules i st
edecd40194c1 method (un)folded: option '(raw)';
wenzelm
parents: 18824
diff changeset
   216
    else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules))
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   217
  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
7130
a17f7b5ac40f added erule;
wenzelm
parents: 6981
diff changeset
   218
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   219
fun gen_arule_tac tac ctxt j rules facts =
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   220
  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
10744
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   221
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   222
fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
11785
3087d6f19adc intro! and elim! rules;
wenzelm
parents: 11765
diff changeset
   223
  let
3087d6f19adc intro! and elim! rules;
wenzelm
parents: 11765
diff changeset
   224
    val rules =
3087d6f19adc intro! and elim! rules;
wenzelm
parents: 11765
diff changeset
   225
      if not (null arg_rules) then arg_rules
33369
470a7b233ee5 modernized structure Context_Rules;
wenzelm
parents: 33159
diff changeset
   226
      else flat (Context_Rules.find_rules false facts goal ctxt)
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   227
  in trace ctxt rules; tac ctxt rules facts i end);
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10034
diff changeset
   228
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   229
fun meth tac x y = METHOD (HEADGOAL o tac x y);
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   230
fun meth' tac x y z = METHOD (HEADGOAL o tac x y z);
8220
e04928747b18 [df]rule methods;
wenzelm
parents: 8205
diff changeset
   231
7419
wenzelm
parents: 7367
diff changeset
   232
in
wenzelm
parents: 7367
diff changeset
   233
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   234
val rule_tac = gen_rule_tac resolve_tac;
10744
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   235
val rule = meth rule_tac;
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   236
val some_rule_tac = gen_some_rule_tac rule_tac;
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   237
val some_rule = meth some_rule_tac;
10744
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   238
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   239
val erule = meth' (gen_arule_tac eresolve_tac);
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   240
val drule = meth' (gen_arule_tac dresolve_tac);
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   241
val frule = meth' (gen_arule_tac forward_tac);
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   242
7419
wenzelm
parents: 7367
diff changeset
   243
end;
wenzelm
parents: 7367
diff changeset
   244
wenzelm
parents: 7367
diff changeset
   245
25270
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   246
(* intros_tac -- pervasive search spanned by intro rules *)
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   247
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 33522
diff changeset
   248
fun gen_intros_tac goals intros facts =
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 33522
diff changeset
   249
  goals (insert_tac facts THEN'
25270
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   250
      REPEAT_ALL_NEW (resolve_tac intros))
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   251
    THEN Tactic.distinct_subgoals_tac;
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   252
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 33522
diff changeset
   253
val intros_tac = gen_intros_tac ALLGOALS;
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 33522
diff changeset
   254
val try_intros_tac = gen_intros_tac TRYALL;
25270
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   255
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   256
8351
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   257
(* ML tactics *)
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   258
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   259
structure ML_Tactic = Proof_Data
26472
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   260
(
27235
134991516430 ML tactic: do not abstract over context again;
wenzelm
parents: 26892
diff changeset
   261
  type T = thm list -> tactic;
26472
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   262
  fun init _ = undefined;
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   263
);
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   264
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   265
val set_tactic = ML_Tactic.put;
8351
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   266
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
   267
fun ml_tactic source ctxt =
26472
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   268
  let
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   269
    val ctxt' = ctxt |> Context.proof_map
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
   270
      (ML_Context.expression (#pos source)
27235
134991516430 ML tactic: do not abstract over context again;
wenzelm
parents: 26892
diff changeset
   271
        "fun tactic (facts: thm list) : tactic"
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56232
diff changeset
   272
        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source false source));
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   273
  in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
23425
b74315510f85 added raw_tactic;
wenzelm
parents: 23395
diff changeset
   274
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
   275
fun tactic source ctxt = METHOD (ml_tactic source ctxt);
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
   276
fun raw_tactic source ctxt = RAW_METHOD (ml_tactic source ctxt);
8351
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   277
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   278
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   279
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   280
(** method syntax **)
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   281
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   282
(* method text *)
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   283
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   284
type src = Args.src;
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   285
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   286
datatype combinator_info = Combinator_Info of {keywords: Position.T list};
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   287
fun combinator_info keywords = Combinator_Info {keywords = keywords};
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   288
val no_combinator_info = combinator_info [];
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   289
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   290
datatype text =
55742
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
   291
  Source of src |
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
   292
  Basic of Proof.context -> method |
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   293
  Then of combinator_info * text list |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   294
  Orelse of combinator_info * text list |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   295
  Try of combinator_info * text |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   296
  Repeat1 of combinator_info * text |
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   297
  Select_Goals of combinator_info * int * text;
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   298
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   299
fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
   300
val succeed_text = Basic (K succeed);
56029
8bedca4bd5a3 clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents: 56026
diff changeset
   301
val default_text = Source (Args.src ("default", Position.none) []);
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
   302
val this_text = Basic (K this);
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
   303
val done_text = Basic (K (SIMPLE_METHOD all_tac));
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
   304
fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   305
49846
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   306
fun finish_text (NONE, immed) = Basic (finish immed)
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   307
  | finish_text (SOME txt, immed) = Then (no_combinator_info, [txt, Basic (finish immed)]);
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   308
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   309
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   310
(* method definitions *)
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   311
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   312
structure Methods = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   313
(
33095
bbd52d2f8696 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents: 33092
diff changeset
   314
  type T = ((src -> Proof.context -> method) * string) Name_Space.table;
33159
369da293bbd4 make SML/NJ happy;
wenzelm
parents: 33096
diff changeset
   315
  val empty : T = Name_Space.empty_table "method";
16448
6c45c5416b79 (RAW_)METHOD_CASES: RuleCases.tactic;
wenzelm
parents: 16347
diff changeset
   316
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   317
  fun merge data : T = Name_Space.merge_tables data;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   318
);
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   319
55742
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
   320
val get_methods = Methods.get o Proof_Context.theory_of;
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
   321
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
   322
fun print_methods ctxt =
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   323
  let
55742
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
   324
    val meths = get_methods ctxt;
50301
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 49889
diff changeset
   325
    fun prt_meth (name, (_, "")) = Pretty.mark_str name
42813
6c841fa92fa2 optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents: 42616
diff changeset
   326
      | prt_meth (name, (_, comment)) =
50301
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 49889
diff changeset
   327
          Pretty.block
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 49889
diff changeset
   328
            (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   329
  in
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56032
diff changeset
   330
    [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 56278
diff changeset
   331
    |> Pretty.writeln_chunks
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   332
  end;
7611
5b5aba10c8f6 help: unkown theory context;
wenzelm
parents: 7601
diff changeset
   333
33092
c859019d3ac5 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
wenzelm
parents: 32969
diff changeset
   334
fun add_method name meth comment thy = thy
47005
421760a1efe7 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents: 46775
diff changeset
   335
  |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31303
diff changeset
   336
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   337
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   338
(* check *)
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   339
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   340
fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
56232
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   341
fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   342
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   343
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   344
(* get methods *)
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   345
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   346
fun method ctxt =
56029
8bedca4bd5a3 clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents: 56026
diff changeset
   347
  let val table = get_methods ctxt
8bedca4bd5a3 clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents: 56026
diff changeset
   348
  in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
55742
a989bdaf8121 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents: 55709
diff changeset
   349
56232
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   350
fun method_closure ctxt src0 =
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   351
  let
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   352
    val (src1, meth) = check_src ctxt src0;
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   353
    val src2 = Args.init_assignable src1;
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   354
    val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   355
  in Args.closure src2 end;
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   356
31e283f606e2 more static checking of proof methods;
wenzelm
parents: 56204
diff changeset
   357
fun method_cmd ctxt = method ctxt o method_closure ctxt;
20030
e62913ef9d24 added method_i and Source_i;
wenzelm
parents: 19778
diff changeset
   358
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   359
30512
17b2aad869fa added simplified setup;
wenzelm
parents: 30508
diff changeset
   360
(* method setup *)
17b2aad869fa added simplified setup;
wenzelm
parents: 30508
diff changeset
   361
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31303
diff changeset
   362
fun setup name scan =
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31303
diff changeset
   363
  add_method name
56032
b034b9f0fa2a clarified Args.check_src: retain name space information for error output;
wenzelm
parents: 56029
diff changeset
   364
    (fn src => fn ctxt => let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end);
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   365
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
   366
fun method_setup name source cmt =
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55795
diff changeset
   367
  Context.theory_map (ML_Context.expression (#pos source)
30544
0ed8fe16331a adapted 'method_setup' command to Method.setup;
wenzelm
parents: 30540
diff changeset
   368
    "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
0ed8fe16331a adapted 'method_setup' command to Method.setup;
wenzelm
parents: 30540
diff changeset
   369
    "Context.map_theory (Method.setup name scan comment)"
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 36959
diff changeset
   370
    (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56232
diff changeset
   371
      ML_Lex.read_source false source @
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 36959
diff changeset
   372
      ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   373
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   374
5884
113badd4dae5 several args parsers;
wenzelm
parents: 5824
diff changeset
   375
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   376
(** concrete syntax **)
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   377
5884
113badd4dae5 several args parsers;
wenzelm
parents: 5824
diff changeset
   378
(* sections *)
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   379
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
   380
type modifier = (Proof.context -> Proof.context) * attribute;
7268
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   381
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   382
local
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   383
24010
2ef318813e1a method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;
wenzelm
parents: 23937
diff changeset
   384
fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 46466
diff changeset
   385
fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context);
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   386
30540
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
   387
in
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
   388
24022
wenzelm
parents: 24010
diff changeset
   389
fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|--
46775
6287653e63ec canonical argument order for attribute application;
wenzelm
parents: 46466
diff changeset
   390
  (fn (m, ths) => Scan.succeed (swap (app m ths context))));
5884
113badd4dae5 several args parsers;
wenzelm
parents: 5824
diff changeset
   391
30540
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
   392
fun sections ss = Scan.repeat (section ss);
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   393
7268
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   394
end;
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   395
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   396
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   397
(* extra rule methods *)
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   398
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   399
fun xrule_meth meth =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36096
diff changeset
   400
  Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   401
  (fn (n, ths) => fn ctxt => meth ctxt n ths);
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   402
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   403
55761
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   404
(* text range *)
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   405
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   406
type text_range = text * Position.range;
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   407
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   408
fun text NONE = NONE
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   409
  | text (SOME (txt, _)) = SOME txt;
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   410
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   411
fun position NONE = Position.none
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   412
  | position (SOME (_, (pos, _))) = pos;
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   413
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   414
55795
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   415
(* reports *)
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   416
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   417
local
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   418
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   419
fun keyword_positions (Source _) = []
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   420
  | keyword_positions (Basic _) = []
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   421
  | keyword_positions (Then (Combinator_Info {keywords}, texts)) =
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   422
      keywords @ maps keyword_positions texts
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   423
  | keyword_positions (Orelse (Combinator_Info {keywords}, texts)) =
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   424
      keywords @ maps keyword_positions texts
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   425
  | keyword_positions (Try (Combinator_Info {keywords}, text)) =
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   426
      keywords @ keyword_positions text
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   427
  | keyword_positions (Repeat1 (Combinator_Info {keywords}, text)) =
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   428
      keywords @ keyword_positions text
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   429
  | keyword_positions (Select_Goals (Combinator_Info {keywords}, _, text)) =
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   430
      keywords @ keyword_positions text;
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   431
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   432
in
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   433
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   434
fun reports_of ((text, (pos, _)): text_range) =
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   435
  (pos, Markup.language_method) ::
55917
5438ed05e1c9 special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents: 55828
diff changeset
   436
    maps (fn p => map (pair p) (Markup.keyword3 :: Completion.suppress_abbrevs ""))
5438ed05e1c9 special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents: 55828
diff changeset
   437
      (keyword_positions text);
55795
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   438
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   439
val report = Position.reports o reports_of;
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   440
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   441
end;
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   442
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   443
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   444
(* outer parser *)
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   445
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   446
fun is_symid_meth s =
36959
f5417836dbea renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents: 36950
diff changeset
   447
  s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   448
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   449
local
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   450
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   451
fun meth4 x =
56029
8bedca4bd5a3 clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents: 56026
diff changeset
   452
 (Parse.position Parse.xname >> (fn name => Source (Args.src name [])) ||
55048
ce34a2934386 implicit "cartouche" method (experimental, undocumented);
wenzelm
parents: 54883
diff changeset
   453
  Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
56029
8bedca4bd5a3 clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents: 56026
diff changeset
   454
    Source (Args.src ("cartouche", Token.pos_of tok) [tok])) ||
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36096
diff changeset
   455
  Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   456
and meth3 x =
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   457
 (meth4 -- Parse.position (Parse.$$$ "?")
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   458
    >> (fn (m, (_, pos)) => Try (combinator_info [pos], m)) ||
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   459
  meth4 -- Parse.position (Parse.$$$ "+")
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   460
    >> (fn (m, (_, pos)) => Repeat1 (combinator_info [pos], m)) ||
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   461
  meth4 --
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   462
    (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   463
    >> (fn (m, (((_, pos1), n), (_, pos2))) =>
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   464
        Select_Goals (combinator_info [pos1, pos2], n, m)) ||
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   465
  meth4) x
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   466
and meth2 x =
56201
dd2df97b379b tuned signature;
wenzelm
parents: 56052
diff changeset
   467
 (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) ||
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   468
  meth3) x
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   469
and meth1 x =
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   470
  (Parse.enum1_positions "," meth2
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   471
    >> (fn ([m], _) => m | (ms, ps) => Then (combinator_info ps, ms))) x
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   472
and meth0 x =
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   473
  (Parse.enum1_positions "|" meth1
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   474
    >> (fn ([m], _) => m | (ms, ps) => Orelse (combinator_info ps, ms))) x;
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   475
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49865
diff changeset
   476
in
619acbd72664 more proof method text position information;
wenzelm
parents: 49865
diff changeset
   477
619acbd72664 more proof method text position information;
wenzelm
parents: 49865
diff changeset
   478
val parse =
55709
4e5a83a46ded clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents: 55708
diff changeset
   479
  Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49865
diff changeset
   480
55761
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   481
end;
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   482
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   483
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18640
diff changeset
   484
(* theory setup *)
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   485
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53168
diff changeset
   486
val _ = Theory.setup
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   487
 (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   488
  setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   489
  setup @{binding "-"} (Scan.succeed (K insert_facts))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   490
    "do nothing (insert current facts only)" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   491
  setup @{binding insert} (Attrib.thms >> (K o insert))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   492
    "insert theorems, ignoring facts (improper)" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   493
  setup @{binding intro} (Attrib.thms >> (K o intro))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   494
    "repeatedly apply introduction rules" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   495
  setup @{binding elim} (Attrib.thms >> (K o elim))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   496
    "repeatedly apply elimination rules" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   497
  setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   498
  setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   499
  setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   500
    "present local premises as object-level statements" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   501
  setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths))
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   502
    "apply some intro/elim rule" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   503
  setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   504
  setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   505
  setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   506
  setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   507
  setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   508
  setup @{binding assumption} (Scan.succeed assumption)
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   509
    "proof by assumption, preferring facts" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   510
  setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   511
    (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   512
    "rename parameters of goal" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   513
  setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   514
    (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   515
      "rotate assumptions of goal" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   516
  setup @{binding tactic} (Scan.lift Args.name_source_position >> tactic)
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   517
    "ML tactic as proof method" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   518
  setup @{binding raw_tactic} (Scan.lift Args.name_source_position >> raw_tactic)
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53168
diff changeset
   519
    "ML tactic as raw proof method");
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   520
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   521
16145
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   522
(*final declarations of this structure!*)
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   523
val unfold = unfold_meth;
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   524
val fold = fold_meth;
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   525
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   526
end;
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   527
30508
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   528
val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   529
val RAW_METHOD = Method.RAW_METHOD;
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   530
val METHOD_CASES = Method.METHOD_CASES;
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   531
val METHOD = Method.METHOD;
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   532
val SIMPLE_METHOD = Method.SIMPLE_METHOD;
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   533
val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   534
val SIMPLE_METHOD'' = Method.SIMPLE_METHOD'';
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   535