src/Pure/Isar/method.ML
author wenzelm
Thu, 02 Apr 2015 20:28:30 +0200
changeset 59914 d1ddcd8df4e4
parent 59909 fbf4d5ad500d
child 59917 9830c944670f
permissions -rw-r--r--
proper treatment of internal method name as already checked Token.src;
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
58002
0ed1e999a0fb simplified type Proof.method;
wenzelm
parents: 57941
diff changeset
     9
  type method = thm list -> cases_tactic
18227
d4cfa0fee007 moved multi_resolve(s) to drule.ML;
wenzelm
parents: 18145
diff changeset
    10
  val METHOD_CASES: (thm list -> cases_tactic) -> method
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    11
  val METHOD: (thm list -> tactic) -> method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    12
  val fail: method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    13
  val succeed: method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    14
  val insert_tac: thm list -> int -> tactic
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    15
  val insert: thm list -> method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    16
  val insert_facts: method
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    17
  val SIMPLE_METHOD: tactic -> method
21592
8831206d7f41 renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
wenzelm
parents: 21579
diff changeset
    18
  val SIMPLE_METHOD': (int -> tactic) -> method
8831206d7f41 renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
wenzelm
parents: 21579
diff changeset
    19
  val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
    20
  val cheating: Proof.context -> bool -> method
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58950
diff changeset
    21
  val intro: Proof.context -> thm list -> method
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58950
diff changeset
    22
  val elim: Proof.context -> thm list -> method
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    23
  val unfold: thm list -> Proof.context -> method
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    24
  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
    25
  val atomize: bool -> Proof.context -> method
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
    26
  val this: Proof.context -> method
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    27
  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
    28
  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
    29
  val all_assm_tac: Proof.context -> tactic
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    30
  val assumption: Proof.context -> method
46466
61c7214b4885 tuned signature, according to actual usage of these operations;
wenzelm
parents: 45375
diff changeset
    31
  val rule_trace: bool Config.T
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20224
diff changeset
    32
  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
    33
  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
    34
  val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
    35
  val intros_tac: Proof.context -> thm list -> thm list -> tactic
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
    36
  val try_intros_tac: Proof.context -> 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
    37
  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
    38
  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
    39
  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
    40
  val frule: Proof.context -> int -> thm list -> method
58018
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
    41
  val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    42
  type combinator_info
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
    43
  val no_combinator_info: combinator_info
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
    44
  datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    45
  datatype text =
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
    46
    Source of Token.src |
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
    47
    Basic of Proof.context -> method |
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
    48
    Combinator of combinator_info * combinator * text list
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
    49
  val map_source: (Token.src -> Token.src) -> text -> text
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    50
  val primitive_text: (Proof.context -> thm -> thm) -> text
17857
810a67ecbc64 added primitive_text, succeed_text;
wenzelm
parents: 17756
diff changeset
    51
  val succeed_text: text
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    52
  val default_text: text
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    53
  val this_text: text
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
    54
  val done_text: text
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
    55
  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
    56
  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
    57
  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
    58
  val check_name: Proof.context -> xstring * Position.T -> string
59907
6c0f62490699 tuned signature;
wenzelm
parents: 59666
diff changeset
    59
  val check_src: Proof.context -> Token.src -> Token.src
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
    60
  val method_syntax: (Proof.context -> method) context_parser ->
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
    61
    Token.src -> Proof.context -> method
30512
17b2aad869fa added simplified setup;
wenzelm
parents: 30508
diff changeset
    62
  val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
57935
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
    63
  val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
    64
    local_theory -> local_theory
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 58991
diff changeset
    65
  val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
    66
  val method: Proof.context -> Token.src -> Proof.context -> method
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
    67
  val method_closure: Proof.context -> Token.src -> Token.src
59909
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
    68
  val closure: bool Config.T
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
    69
  val method_cmd: Proof.context -> Token.src -> Proof.context -> method
58007
671c607fb4af just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents: 58006
diff changeset
    70
  val evaluate: text -> Proof.context -> method
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
    71
  type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
    72
  val modifier: attribute -> Position.T -> modifier
58029
2137e60b6f6d clarified Method.section: explicit declaration with static closure;
wenzelm
parents: 58026
diff changeset
    73
  val section: modifier parser list -> declaration context_parser
2137e60b6f6d clarified Method.section: explicit declaration with static closure;
wenzelm
parents: 58026
diff changeset
    74
  val sections: modifier parser list -> declaration list context_parser
49889
00ea087e83d8 more method position information, notably finished_pos after end of previous text;
wenzelm
parents: 49866
diff changeset
    75
  type text_range = text * Position.range
00ea087e83d8 more method position information, notably finished_pos after end of previous text;
wenzelm
parents: 49866
diff changeset
    76
  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
    77
  val position: text_range option -> Position.T
55795
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
    78
  val reports_of: text_range -> Position.report list
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
    79
  val report: text_range -> unit
55761
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
    80
  val parse: text_range parser
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
    81
  val parse_internal: Proof.context -> 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
58006
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
    89
(* method *)
11731
1a0c1ef86518 added trace_rules, trace;
wenzelm
parents: 10907
diff changeset
    90
58002
0ed1e999a0fb simplified type Proof.method;
wenzelm
parents: 57941
diff changeset
    91
type method = thm list -> cases_tactic;
11731
1a0c1ef86518 added trace_rules, trace;
wenzelm
parents: 10907
diff changeset
    92
58030
c6b131e651e6 made SML/NJ happy;
wenzelm
parents: 58029
diff changeset
    93
fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
c6b131e651e6 made SML/NJ happy;
wenzelm
parents: 58029
diff changeset
    94
fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    95
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    96
val fail = METHOD (K no_tac);
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    97
val succeed = METHOD (K all_tac);
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    98
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
    99
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   100
(* insert facts *)
7419
wenzelm
parents: 7367
diff changeset
   101
wenzelm
parents: 7367
diff changeset
   102
local
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   103
21579
abd2b4386a63 COMP_INCR;
wenzelm
parents: 20335
diff changeset
   104
fun cut_rule_tac rule =
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   105
  resolve0_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
6981
eaade7e398a7 export assumption_tac;
wenzelm
parents: 6951
diff changeset
   106
7419
wenzelm
parents: 7367
diff changeset
   107
in
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   108
51552
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents: 51383
diff changeset
   109
fun insert_tac [] _ = all_tac
7419
wenzelm
parents: 7367
diff changeset
   110
  | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
6981
eaade7e398a7 export assumption_tac;
wenzelm
parents: 6951
diff changeset
   111
7555
dd281afb33d7 setup for refined facts handling;
wenzelm
parents: 7526
diff changeset
   112
val insert_facts = METHOD (ALLGOALS o insert_tac);
7664
c151ac595551 insert: ignore facts;
wenzelm
parents: 7611
diff changeset
   113
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
7419
wenzelm
parents: 7367
diff changeset
   114
9706
8e48a19fc81e removed METHOD0;
wenzelm
parents: 9653
diff changeset
   115
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
   116
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
   117
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
9706
8e48a19fc81e removed METHOD0;
wenzelm
parents: 9653
diff changeset
   118
12324
5db4b4596d1a rule context and attributes moved to rule_context.ML;
wenzelm
parents: 12311
diff changeset
   119
end;
5db4b4596d1a rule context and attributes moved to rule_context.ML;
wenzelm
parents: 12311
diff changeset
   120
9706
8e48a19fc81e removed METHOD0;
wenzelm
parents: 9653
diff changeset
   121
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   122
(* cheating *)
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   123
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
   124
fun cheating ctxt int = METHOD (fn _ => fn st =>
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
   125
  if int orelse Config.get ctxt quick_and_dirty then
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   126
    ALLGOALS (Skip_Proof.cheat_tac ctxt) st
51552
c713c9505f68 clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents: 51383
diff changeset
   127
  else error "Cheating requires quick_and_dirty mode!");
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   128
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   129
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   130
(* unfold intro/elim rules *)
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   131
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58950
diff changeset
   132
fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths));
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58950
diff changeset
   133
fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths));
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   134
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   135
12384
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   136
(* unfold/fold definitions *)
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   137
35624
c4e29a0bb8c1 modernized structure Local_Defs;
wenzelm
parents: 33522
diff changeset
   138
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
   139
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
   140
12384
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   141
12829
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   142
(* atomize rule statements *)
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   143
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   144
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
   145
      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
   146
  | atomize true ctxt =
58002
0ed1e999a0fb simplified type Proof.method;
wenzelm
parents: 57941
diff changeset
   147
      NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
12829
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   148
c92128238f85 full_atomize;
wenzelm
parents: 12399
diff changeset
   149
18039
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   150
(* this -- resolve facts directly *)
12384
86e383f6bfea simple version of 'intro' and 'elim' method;
wenzelm
parents: 12359
diff changeset
   151
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   152
fun this ctxt = METHOD (EVERY o map (HEADGOAL o resolve_tac ctxt o single));
9484
3bda55143260 (un)fold: CHANGED;
wenzelm
parents: 9418
diff changeset
   153
3bda55143260 (un)fold: CHANGED;
wenzelm
parents: 9418
diff changeset
   154
18039
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   155
(* fact -- composition by facts from context *)
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   156
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42358
diff changeset
   157
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
   158
  | fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules);
18039
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   159
500b7ed7b2bd added fact method;
wenzelm
parents: 17857
diff changeset
   160
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   161
(* assumption *)
7419
wenzelm
parents: 7367
diff changeset
   162
wenzelm
parents: 7367
diff changeset
   163
local
wenzelm
parents: 7367
diff changeset
   164
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   165
fun cond_rtac ctxt cond rule = SUBGOAL (fn (prop, i) =>
19778
f0a318495ca4 assm_tac: try rule termI;
wenzelm
parents: 19482
diff changeset
   166
  if cond (Logic.strip_assums_concl prop)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   167
  then resolve_tac ctxt [rule] i else no_tac);
7419
wenzelm
parents: 7367
diff changeset
   168
29857
2cc976ed8a3c FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents: 29301
diff changeset
   169
in
2cc976ed8a3c FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents: 29301
diff changeset
   170
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
   171
fun assm_tac ctxt =
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58957
diff changeset
   172
  assume_tac ctxt APPEND'
23349
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   173
  Goal.assume_rule_tac ctxt APPEND'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   174
  cond_rtac ctxt (can Logic.dest_equals) Drule.reflexive_thm APPEND'
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   175
  cond_rtac ctxt (can Logic.dest_term) Drule.termI;
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   176
49846
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   177
fun all_assm_tac ctxt =
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   178
  let
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   179
    fun tac i st =
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   180
      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
   181
      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
   182
  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
   183
23349
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   184
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
   185
  (fn [] => assm_tac ctxt
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   186
    | [fact] => solve_tac ctxt [fact]
23349
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   187
    | _ => K no_tac));
23a8345f89f5 Basic text: include position;
wenzelm
parents: 23178
diff changeset
   188
49846
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   189
fun finish immed ctxt =
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   190
  METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt));
7419
wenzelm
parents: 7367
diff changeset
   191
wenzelm
parents: 7367
diff changeset
   192
end;
wenzelm
parents: 7367
diff changeset
   193
wenzelm
parents: 7367
diff changeset
   194
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   195
(* rule etc. -- single-step refinements *)
12347
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   196
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   197
val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false);
12347
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   198
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   199
fun trace ctxt rules =
41379
b31d7a1cd08f configuration option "rule_trace";
wenzelm
parents: 39507
diff changeset
   200
  if Config.get ctxt rule_trace andalso not (null rules) then
51584
98029ceda8ce more item markup;
wenzelm
parents: 51552
diff changeset
   201
    Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21879
diff changeset
   202
    |> Pretty.string_of |> tracing
279b129498b6 removed conditional combinator;
wenzelm
parents: 21879
diff changeset
   203
  else ();
12347
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   204
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   205
local
6ee66b76d813 added "rules" method;
wenzelm
parents: 12324
diff changeset
   206
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   207
fun gen_rule_tac tac ctxt rules facts =
18841
edecd40194c1 method (un)folded: option '(raw)';
wenzelm
parents: 18824
diff changeset
   208
  (fn i => fn st =>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   209
    if null facts then tac ctxt rules i st
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   210
    else
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   211
      Seq.maps (fn rule => (tac ctxt o single) rule i st)
58950
d07464875dd4 optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents: 58837
diff changeset
   212
        (Drule.multi_resolves (SOME ctxt) facts rules))
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   213
  THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
7130
a17f7b5ac40f added erule;
wenzelm
parents: 6981
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_arule_tac tac ctxt j rules facts =
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58957
diff changeset
   216
  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt));
10744
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   217
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   218
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
   219
  let
3087d6f19adc intro! and elim! rules;
wenzelm
parents: 11765
diff changeset
   220
    val rules =
3087d6f19adc intro! and elim! rules;
wenzelm
parents: 11765
diff changeset
   221
      if not (null arg_rules) then arg_rules
33369
470a7b233ee5 modernized structure Context_Rules;
wenzelm
parents: 33159
diff changeset
   222
      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
   223
  in trace ctxt rules; tac ctxt rules facts i end);
10309
a7f961fb62c6 intro_classes by default;
wenzelm
parents: 10034
diff changeset
   224
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   225
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
   226
fun meth' tac x y z = METHOD (HEADGOAL o tac x y z);
8220
e04928747b18 [df]rule methods;
wenzelm
parents: 8205
diff changeset
   227
7419
wenzelm
parents: 7367
diff changeset
   228
in
wenzelm
parents: 7367
diff changeset
   229
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   230
val rule_tac = gen_rule_tac resolve_tac;
10744
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   231
val rule = meth rule_tac;
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   232
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
   233
val some_rule = meth some_rule_tac;
10744
5d142ca01b8e 'erule' etc.: assm arg;
wenzelm
parents: 10541
diff changeset
   234
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   235
val erule = meth' (gen_arule_tac eresolve_tac);
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   236
val drule = meth' (gen_arule_tac dresolve_tac);
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   237
val frule = meth' (gen_arule_tac forward_tac);
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   238
7419
wenzelm
parents: 7367
diff changeset
   239
end;
wenzelm
parents: 7367
diff changeset
   240
wenzelm
parents: 7367
diff changeset
   241
25270
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   242
(* intros_tac -- pervasive search spanned by intro rules *)
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   243
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   244
fun gen_intros_tac goals ctxt intros facts =
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 33522
diff changeset
   245
  goals (insert_tac facts THEN'
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   246
      REPEAT_ALL_NEW (resolve_tac ctxt intros))
25270
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   247
    THEN Tactic.distinct_subgoals_tac;
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   248
36093
0880493627ca Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents: 33522
diff changeset
   249
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
   250
val try_intros_tac = gen_intros_tac TRYALL;
25270
2ed7b34f58e6 generic tactic Method.intros_tac
haftmann
parents: 24116
diff changeset
   251
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   252
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   253
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   254
(** method syntax **)
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   255
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   256
(* context data *)
8351
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   257
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   258
structure Data = Generic_Data
26472
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   259
(
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   260
  type T =
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   261
    ((Token.src -> Proof.context -> method) * string) Name_Space.table *  (*methods*)
58018
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   262
    (morphism -> thm list -> tactic) option;  (*ML tactic*)
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   263
  val empty : T = (Name_Space.empty_table "method", NONE);
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   264
  val extend = I;
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   265
  fun merge ((tab, tac), (tab', tac')) : T =
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   266
    (Name_Space.merge_tables (tab, tab'), merge_options (tac, tac'));
26472
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   267
);
9afdd61cf528 ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents: 26463
diff changeset
   268
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   269
val get_methods = fst o Data.get;
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   270
val map_methods = Data.map o apfst;
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   271
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   272
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   273
(* ML tactic *)
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   274
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   275
val set_tactic = Data.map o apsnd o K o SOME;
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   276
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   277
fun the_tactic context =
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   278
  (case snd (Data.get context) of
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   279
    SOME tac => tac
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   280
  | NONE => raise Fail "Undefined ML tactic");
8351
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   281
58018
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   282
val parse_tactic =
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   283
  Scan.state :|-- (fn context =>
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   284
    Scan.lift (Args.text_declaration (fn source =>
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   285
      let
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   286
        val context' = context |>
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 58991
diff changeset
   287
          ML_Context.expression (Input.range_of source)
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
   288
            "tactic" "Morphism.morphism -> thm list -> tactic"
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
   289
            "Method.set_tactic tactic"
59067
dd8ec9138112 tuned signature;
wenzelm
parents: 59064
diff changeset
   290
            (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
   291
             ML_Lex.read_source false source);
58018
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   292
        val tac = the_tactic context';
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   293
      in
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   294
        fn phi =>
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   295
          set_tactic (fn _ => Context.setmp_thread_data (SOME context) (tac phi))
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   296
      end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
8351
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   297
1b8ac0f48233 added simple_args;
wenzelm
parents: 8335
diff changeset
   298
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   299
(* method text *)
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   300
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   301
datatype combinator_info = Combinator_Info of {keywords: Position.T list};
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   302
fun combinator_info keywords = Combinator_Info {keywords = keywords};
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   303
val no_combinator_info = combinator_info [];
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   304
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   305
datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int;
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   306
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   307
datatype text =
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
   308
  Source of Token.src |
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
   309
  Basic of Proof.context -> method |
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   310
  Combinator of combinator_info * combinator * text list;
55765
ec7ca5388dea markup for method combinators;
wenzelm
parents: 55761
diff changeset
   311
58006
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   312
fun map_source f (Source src) = Source (f src)
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   313
  | map_source _ (Basic meth) = Basic meth
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   314
  | map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts);
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   315
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   316
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
   317
val succeed_text = Basic (K succeed);
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
   318
val default_text = Source (Token.src ("default", Position.none) []);
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   319
val this_text = Basic this;
32193
c314b4836031 basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents: 32091
diff changeset
   320
val done_text = Basic (K (SIMPLE_METHOD all_tac));
52059
2f970c7f722b proper option quick_and_dirty;
wenzelm
parents: 51584
diff changeset
   321
fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   322
49846
8fae089f5a0c refined Proof.the_finished_goal with more informative error;
wenzelm
parents: 48992
diff changeset
   323
fun finish_text (NONE, immed) = Basic (finish immed)
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   324
  | finish_text (SOME txt, immed) =
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   325
      Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]);
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   326
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   327
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   328
(* method definitions *)
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   329
57937
wenzelm
parents: 57935
diff changeset
   330
fun transfer_methods ctxt =
57935
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   331
  let
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   332
    val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt));
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   333
    val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt));
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   334
  in Context.proof_map (map_methods (K meths')) ctxt 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
   335
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
   336
fun print_methods ctxt =
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   337
  let
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   338
    val meths = get_methods (Context.Proof ctxt);
50301
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 49889
diff changeset
   339
    fun prt_meth (name, (_, "")) = Pretty.mark_str name
42813
6c841fa92fa2 optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents: 42616
diff changeset
   340
      | prt_meth (name, (_, comment)) =
50301
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 49889
diff changeset
   341
          Pretty.block
56b4c9afd7be print formal entities with markup;
wenzelm
parents: 49889
diff changeset
   342
            (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   343
  in
56052
4873054cd1fc tuned signature;
wenzelm
parents: 56032
diff changeset
   344
    [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
   345
    |> Pretty.writeln_chunks
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22586
diff changeset
   346
  end;
7611
5b5aba10c8f6 help: unkown theory context;
wenzelm
parents: 7601
diff changeset
   347
57935
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   348
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   349
(* define *)
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   350
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   351
fun define_global binding meth comment thy =
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   352
  let
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   353
    val context = Context.Theory thy;
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   354
    val (name, meths') =
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   355
      Name_Space.define context true (binding, (meth, comment)) (get_methods context);
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   356
  in (name, Context.the_theory (map_methods (K meths') context)) end;
57935
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   357
57941
57200bdc2aa7 localized command 'method_setup' and 'attribute_setup';
wenzelm
parents: 57938
diff changeset
   358
fun define binding meth comment =
57200bdc2aa7 localized command 'method_setup' and 'attribute_setup';
wenzelm
parents: 57938
diff changeset
   359
  Local_Theory.background_theory_result (define_global binding meth comment)
57200bdc2aa7 localized command 'method_setup' and 'attribute_setup';
wenzelm
parents: 57938
diff changeset
   360
  #-> (fn name =>
57200bdc2aa7 localized command 'method_setup' and 'attribute_setup';
wenzelm
parents: 57938
diff changeset
   361
    Local_Theory.map_contexts (K transfer_methods)
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   362
    #> Local_Theory.generic_alias map_methods binding name
57941
57200bdc2aa7 localized command 'method_setup' and 'attribute_setup';
wenzelm
parents: 57938
diff changeset
   363
    #> pair name);
31304
00a9c674cf40 eliminated old Method.add_method(s);
wenzelm
parents: 31303
diff changeset
   364
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   365
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   366
(* check *)
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   367
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   368
fun check_name ctxt =
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   369
  let val context = Context.Proof ctxt
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   370
  in #1 o Name_Space.check context (get_methods context) end;
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   371
59907
6c0f62490699 tuned signature;
wenzelm
parents: 59666
diff changeset
   372
fun check_src ctxt =
6c0f62490699 tuned signature;
wenzelm
parents: 59666
diff changeset
   373
  #1 o Token.check_src ctxt (get_methods (Context.Proof ctxt));
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   374
59914
d1ddcd8df4e4 proper treatment of internal method name as already checked Token.src;
wenzelm
parents: 59909
diff changeset
   375
fun checked_info ctxt name =
d1ddcd8df4e4 proper treatment of internal method name as already checked Token.src;
wenzelm
parents: 59909
diff changeset
   376
  let val space = Name_Space.space_of_table (get_methods (Context.Proof ctxt))
d1ddcd8df4e4 proper treatment of internal method name as already checked Token.src;
wenzelm
parents: 59909
diff changeset
   377
  in (Name_Space.kind_of space, Name_Space.markup space name) end;
d1ddcd8df4e4 proper treatment of internal method name as already checked Token.src;
wenzelm
parents: 59909
diff changeset
   378
55997
9dc5ce83202c modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents: 55917
diff changeset
   379
30512
17b2aad869fa added simplified setup;
wenzelm
parents: 30508
diff changeset
   380
(* method setup *)
17b2aad869fa added simplified setup;
wenzelm
parents: 30508
diff changeset
   381
57935
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   382
fun method_syntax scan src ctxt : method =
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
   383
  let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end;
57935
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   384
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   385
fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
c578f3a37a67 localized method definitions (see also f14c1248d064);
wenzelm
parents: 57863
diff changeset
   386
fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   387
58979
162a4c2e97bc more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58978
diff changeset
   388
fun method_setup name source comment =
162a4c2e97bc more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58978
diff changeset
   389
  ML_Lex.read_source false source
59064
a8bcb5a446c8 more abstract type Input.source;
wenzelm
parents: 58991
diff changeset
   390
  |> ML_Context.expression (Input.range_of source) "parser"
58991
92b6f4e68c5a more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58979
diff changeset
   391
    "(Proof.context -> Proof.method) context_parser"
58979
162a4c2e97bc more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58978
diff changeset
   392
    ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
162a4c2e97bc more careful ML source positions, for improved PIDE markup;
wenzelm
parents: 58978
diff changeset
   393
      " parser " ^ ML_Syntax.print_string comment ^ ")")
57941
57200bdc2aa7 localized command 'method_setup' and 'attribute_setup';
wenzelm
parents: 57938
diff changeset
   394
  |> Context.proof_map;
17356
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   395
09afdf37cdb3 added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents: 17314
diff changeset
   396
58006
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   397
(* prepare methods *)
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   398
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   399
fun method ctxt =
58016
28e5ccf4a27f more uniform data slot;
wenzelm
parents: 58011
diff changeset
   400
  let val table = get_methods (Context.Proof ctxt)
58011
bc6bced136e5 tuned signature -- moved type src to Token, without aliases;
wenzelm
parents: 58007
diff changeset
   401
  in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end;
58006
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   402
59909
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   403
fun method_closure ctxt src =
58006
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   404
  let
59909
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   405
    val src' = Token.init_assignable_src src;
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   406
    val ctxt' = Context_Position.not_really ctxt;
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   407
    val _ = Seq.pull (method ctxt' src' ctxt' [] (Goal.protect 0 Drule.dummy_thm));
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   408
  in Token.closure_src src' end;
58006
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   409
59909
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   410
val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true)));
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   411
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   412
fun method_cmd ctxt =
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   413
  check_src ctxt #>
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   414
  Config.get ctxt closure ? method_closure ctxt #>
fbf4d5ad500d clarified method_closure;
wenzelm
parents: 59907
diff changeset
   415
  method ctxt;
58006
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   416
3072ff7ea472 tuned signature;
wenzelm
parents: 58005
diff changeset
   417
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   418
(* evaluate method text *)
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   419
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   420
local
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   421
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   422
fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) =
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   423
  tac st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   424
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   425
fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) =
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   426
  tac st |> Seq.map (pair cases);
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   427
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   428
val op THEN = Seq.THEN;
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   429
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   430
val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac);
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   431
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   432
fun RESTRICT_GOAL i n method =
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   433
  BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   434
  method THEN
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   435
  BYPASS_CASES (PRIMITIVE (Goal.unrestrict i));
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   436
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   437
fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method;
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   438
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   439
fun (method1 THEN_ALL_NEW method2) i (st: cases_state) =
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   440
  st |> (method1 i THEN (fn st' =>
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   441
    Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st') - Thm.nprems_of (snd st)) st'));
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   442
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   443
fun COMBINATOR1 comb [meth] = comb meth
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   444
  | COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument";
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   445
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   446
fun combinator Then = Seq.EVERY
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   447
  | combinator Then_All_New =
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   448
      (fn [] => Seq.single
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   449
        | methods =>
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   450
            preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1)
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   451
  | combinator Orelse = Seq.FIRST
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   452
  | combinator Try = COMBINATOR1 Seq.TRY
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   453
  | combinator Repeat1 = COMBINATOR1 Seq.REPEAT1
59660
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   454
  | combinator (Select_Goals n) =
49e498cedd02 support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents: 59498
diff changeset
   455
      COMBINATOR1 (fn method => preparation THEN RESTRICT_GOAL 1 n method);
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   456
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   457
in
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   458
58007
671c607fb4af just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents: 58006
diff changeset
   459
fun evaluate text ctxt =
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   460
  let
58007
671c607fb4af just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents: 58006
diff changeset
   461
    fun eval (Basic meth) = APPEND_CASES o meth ctxt
671c607fb4af just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents: 58006
diff changeset
   462
      | eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   463
      | eval (Combinator (_, c, txts)) =
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   464
          let
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   465
            val comb = combinator c;
58007
671c607fb4af just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents: 58006
diff changeset
   466
            val meths = map eval txts;
671c607fb4af just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents: 58006
diff changeset
   467
          in fn facts => comb (map (fn meth => meth facts) meths) end;
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   468
    val meth = eval text;
58007
671c607fb4af just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents: 58006
diff changeset
   469
  in fn facts => fn st => meth facts ([], st) end;
58003
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   470
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   471
end;
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   472
250ecd2502ad clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents: 58002
diff changeset
   473
5884
113badd4dae5 several args parsers;
wenzelm
parents: 5824
diff changeset
   474
17110
4c5622d7bdbe moved before proof.ML;
wenzelm
parents: 16876
diff changeset
   475
(** concrete syntax **)
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   476
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   477
(* type modifier *)
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   478
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   479
type modifier =
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   480
  {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T};
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   481
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   482
fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos};
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   483
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   484
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   485
(* sections *)
7268
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   486
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   487
local
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   488
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 58034
diff changeset
   489
fun sect (modifier : modifier parser) = Scan.depend (fn context =>
58068
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   490
  Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier Parse.xthm) >>
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   491
    (fn ((tok, {init, attribute, pos}), xthms) =>
58029
2137e60b6f6d clarified Method.section: explicit declaration with static closure;
wenzelm
parents: 58026
diff changeset
   492
      let
58068
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   493
        val decl =
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   494
          (case Token.get_value tok of
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   495
            SOME (Token.Declaration decl) => decl
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   496
          | _ =>
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   497
              let
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   498
                val ctxt = Context.proof_of context;
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   499
                fun prep_att src =
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   500
                  let
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   501
                    val src' = Attrib.check_src ctxt src;
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   502
                    val _ = List.app (Token.assign NONE) (Token.args_of_src src');
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   503
                  in src' end;
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   504
                val thms =
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   505
                  map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms;
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   506
                val facts =
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   507
                  Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   508
                  |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   509
                val _ =
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   510
                  Context_Position.report ctxt (Token.pos_of tok)
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   511
                    (Markup.entity Markup.method_modifierN ""
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   512
                      |> Markup.properties (Position.def_properties_of pos));
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   513
                fun decl phi =
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   514
                  Context.mapping I init #>
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   515
                  Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   516
                val _ = Token.assign (SOME (Token.Declaration decl)) tok;
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   517
              in decl end);
d6f29bf9b783 intern xthm only once;
wenzelm
parents: 58048
diff changeset
   518
      in (Morphism.form decl context, decl) end));
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   519
30540
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
   520
in
5e2d9604a3d3 export section, sections;
wenzelm
parents: 30515
diff changeset
   521
58029
2137e60b6f6d clarified Method.section: explicit declaration with static closure;
wenzelm
parents: 58026
diff changeset
   522
val section = sect o Scan.first;
2137e60b6f6d clarified Method.section: explicit declaration with static closure;
wenzelm
parents: 58026
diff changeset
   523
val sections = Scan.repeat o section;
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   524
7268
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   525
end;
315655dc361b sectioned_args etc.: more general modifier;
wenzelm
parents: 7130
diff changeset
   526
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   527
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   528
(* extra rule methods *)
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   529
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53171
diff changeset
   530
fun xrule_meth meth =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36096
diff changeset
   531
  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
   532
  (fn (n, ths) => fn ctxt => meth ctxt n ths);
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   533
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   534
55761
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   535
(* text range *)
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   536
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   537
type text_range = text * Position.range;
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   538
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   539
fun text NONE = NONE
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   540
  | text (SOME (txt, _)) = SOME txt;
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   541
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   542
fun position NONE = Position.none
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   543
  | position (SOME (_, (pos, _))) = pos;
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   544
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   545
55795
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   546
(* reports *)
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   547
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   548
local
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   549
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   550
fun keyword_positions (Source _) = []
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   551
  | keyword_positions (Basic _) = []
58005
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   552
  | keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) =
c28e6bc6635d more compact datatypes;
wenzelm
parents: 58004
diff changeset
   553
      keywords @ maps keyword_positions texts;
55795
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   554
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   555
in
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   556
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   557
fun reports_of ((text, (pos, _)): text_range) =
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   558
  (pos, Markup.language_method) ::
55917
5438ed05e1c9 special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents: 55828
diff changeset
   559
    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
   560
      (keyword_positions text);
55795
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   561
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   562
val report = Position.reports o reports_of;
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   563
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   564
end;
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   565
2d4cf0005a02 more explicit method reports;
wenzelm
parents: 55765
diff changeset
   566
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   567
(* parser *)
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   568
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   569
local
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   570
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   571
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
   572
  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
   573
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   574
fun parser check_ctxt low_pri =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   575
  let
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   576
    val (meth_name, mk_src) =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   577
      (case check_ctxt of
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   578
        NONE => (Parse.xname, Token.src)
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   579
      | SOME ctxt =>
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   580
         (Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)),
59914
d1ddcd8df4e4 proper treatment of internal method name as already checked Token.src;
wenzelm
parents: 59909
diff changeset
   581
          fn (name, pos) => fn args => Token.src_checked (name, pos) args (checked_info ctxt name)));
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   582
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   583
    fun meth5 x =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   584
     (Parse.position meth_name >> (fn name => Source (mk_src name [])) ||
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   585
      Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok =>
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   586
        Source (mk_src ("cartouche", Token.pos_of tok) [tok])) ||
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   587
      Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   588
    and meth4 x =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   589
     (meth5 -- Parse.position (Parse.$$$ "?")
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   590
        >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) ||
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   591
      meth5 -- Parse.position (Parse.$$$ "+")
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   592
        >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) ||
59914
d1ddcd8df4e4 proper treatment of internal method name as already checked Token.src;
wenzelm
parents: 59909
diff changeset
   593
      meth5 -- (Parse.position (Parse.$$$ "[") --
d1ddcd8df4e4 proper treatment of internal method name as already checked Token.src;
wenzelm
parents: 59909
diff changeset
   594
          Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   595
        >> (fn (m, (((_, pos1), n), (_, pos2))) =>
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   596
            Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) ||
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   597
      meth5) x
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   598
    and meth3 x =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   599
     (Parse.position meth_name -- Parse.args1 is_symid_meth >> (Source o uncurry mk_src) ||
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   600
      meth4) x
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   601
    and meth2 x =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   602
      (Parse.enum1_positions "," meth3
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   603
        >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   604
    and meth1 x =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   605
      (Parse.enum1_positions ";" meth2
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   606
        >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   607
    and meth0 x =
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   608
      (Parse.enum1_positions "|" meth1
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   609
        >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x;
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   610
  in
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   611
    Scan.trace (if low_pri then meth0 else meth4)
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   612
      >> (fn (m, toks) => (m, Token.range_of toks))
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   613
  end;
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   614
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49865
diff changeset
   615
in
619acbd72664 more proof method text position information;
wenzelm
parents: 49865
diff changeset
   616
59666
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   617
val parse = parser NONE false;
0e9f303d1515 clarified Token.check_src: intern at most once;
wenzelm
parents: 59660
diff changeset
   618
fun parse_internal ctxt = parser (SOME ctxt) true;
49866
619acbd72664 more proof method text position information;
wenzelm
parents: 49865
diff changeset
   619
55761
213b9811f59f method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents: 55742
diff changeset
   620
end;
27813
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   621
96fbe385a0d0 unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents: 27751
diff changeset
   622
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18640
diff changeset
   623
(* theory setup *)
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   624
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53168
diff changeset
   625
val _ = Theory.setup
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   626
 (setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   627
  setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   628
  setup @{binding "-"} (Scan.succeed (K insert_facts))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   629
    "do nothing (insert current facts only)" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   630
  setup @{binding insert} (Attrib.thms >> (K o insert))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   631
    "insert theorems, ignoring facts (improper)" #>
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58950
diff changeset
   632
  setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   633
    "repeatedly apply introduction rules" #>
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58950
diff changeset
   634
  setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   635
    "repeatedly apply elimination rules" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   636
  setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   637
  setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   638
  setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize)
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   639
    "present local premises as object-level statements" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   640
  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
   641
    "apply some intro/elim rule" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   642
  setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   643
  setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   644
  setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #>
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59067
diff changeset
   645
  setup @{binding this} (Scan.succeed this) "apply current facts as rules" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   646
  setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #>
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   647
  setup @{binding assumption} (Scan.succeed assumption)
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   648
    "proof by assumption, preferring facts" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   649
  setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   650
    (fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs))))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   651
    "rename parameters of goal" #>
56204
f70e69208a8c more antiquotations;
wenzelm
parents: 56201
diff changeset
   652
  setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52059
diff changeset
   653
    (fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i))))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   654
      "rotate assumptions of goal" #>
58018
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   655
  setup @{binding tactic} (parse_tactic >> (K o METHOD))
30515
bca05b17b618 simplified method setup;
wenzelm
parents: 30512
diff changeset
   656
    "ML tactic as proof method" #>
58018
beb4b7c0bb30 proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents: 58016
diff changeset
   657
  setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => NO_CASES o tac))
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 53168
diff changeset
   658
    "ML tactic as raw proof method");
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   659
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   660
16145
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   661
(*final declarations of this structure!*)
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   662
val unfold = unfold_meth;
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   663
val fold = fold_meth;
1bb17485602f renamed cond_extern to extern;
wenzelm
parents: 15973
diff changeset
   664
5824
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   665
end;
91113aa09371 Proof methods.
wenzelm
parents:
diff changeset
   666
30508
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   667
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
   668
val METHOD = Method.METHOD;
958cc116d03b tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents: 30466
diff changeset
   669
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
   670
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
   671
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
   672