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