author | wenzelm |
Tue, 19 Aug 2014 15:55:06 +0200 | |
changeset 58005 | c28e6bc6635d |
parent 58004 | 1b064162ec57 |
child 58006 | 3072ff7ea472 |
permissions | -rw-r--r-- |
5824 | 1 |
(* Title: Pure/Isar/method.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
17110 | 4 |
Isar proof methods. |
5824 | 5 |
*) |
6 |
||
7 |
signature METHOD = |
|
8 |
sig |
|
58002 | 9 |
type method = thm list -> cases_tactic |
18227 | 10 |
val METHOD_CASES: (thm list -> cases_tactic) -> method |
17110 | 11 |
val METHOD: (thm list -> tactic) -> method |
12 |
val fail: method |
|
13 |
val succeed: method |
|
14 |
val insert_tac: thm list -> int -> tactic |
|
15 |
val insert: thm list -> method |
|
16 |
val insert_facts: method |
|
17 |
val SIMPLE_METHOD: tactic -> method |
|
21592 | 18 |
val SIMPLE_METHOD': (int -> tactic) -> method |
19 |
val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method |
|
52059 | 20 |
val cheating: Proof.context -> bool -> method |
17110 | 21 |
val intro: thm list -> method |
22 |
val elim: thm list -> method |
|
20289 | 23 |
val unfold: thm list -> Proof.context -> method |
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 |
17110 | 26 |
val this: method |
20289 | 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 | 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 | 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 |
25270 | 35 |
val intros_tac: thm list -> thm list -> tactic |
36093
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
36 |
val try_intros_tac: thm list -> thm list -> tactic |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
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 |
27235 | 41 |
val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
42 |
val tactic: Symbol_Pos.source -> Proof.context -> method |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
43 |
val raw_tactic: Symbol_Pos.source -> Proof.context -> method |
27729 | 44 |
type src = Args.src |
55765 | 45 |
type combinator_info |
46 |
val no_combinator_info: combinator_info |
|
58005 | 47 |
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int |
5824 | 48 |
datatype text = |
55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset
|
49 |
Source of src | |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
50 |
Basic of Proof.context -> method | |
58005 | 51 |
Combinator of combinator_info * combinator * text list |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
52 |
val primitive_text: (Proof.context -> thm -> thm) -> text |
17857 | 53 |
val succeed_text: text |
17110 | 54 |
val default_text: text |
55 |
val this_text: text |
|
56 |
val done_text: text |
|
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
val check_name: Proof.context -> xstring * Position.T -> string |
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
61 |
val method: Proof.context -> src -> Proof.context -> method |
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
62 |
val method_cmd: Proof.context -> src -> Proof.context -> method |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
63 |
val method_syntax: (Proof.context -> method) context_parser -> Args.src -> Proof.context -> method |
30512 | 64 |
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
65 |
val local_setup: binding -> (Proof.context -> method) context_parser -> string -> |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
66 |
local_theory -> local_theory |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
67 |
val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
68 |
local_theory -> local_theory |
58004 | 69 |
val evaluate: text -> Proof.context -> Proof.context -> method |
30540 | 70 |
type modifier = (Proof.context -> Proof.context) * attribute |
71 |
val section: modifier parser list -> thm list context_parser |
|
72 |
val sections: modifier parser list -> thm list list context_parser |
|
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset
|
73 |
type text_range = text * Position.range |
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset
|
74 |
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
|
75 |
val position: text_range option -> Position.T |
55795 | 76 |
val reports_of: text_range -> Position.report list |
77 |
val report: text_range -> unit |
|
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
78 |
val parse: text_range parser |
5824 | 79 |
end; |
80 |
||
81 |
structure Method: METHOD = |
|
82 |
struct |
|
83 |
||
12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
84 |
(** proof methods **) |
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
85 |
|
17110 | 86 |
(* datatype method *) |
11731 | 87 |
|
58002 | 88 |
type method = thm list -> cases_tactic; |
11731 | 89 |
|
58002 | 90 |
fun METHOD_CASES tac facts = Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); |
91 |
fun METHOD tac facts = NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); |
|
5824 | 92 |
|
93 |
val fail = METHOD (K no_tac); |
|
94 |
val succeed = METHOD (K all_tac); |
|
95 |
||
96 |
||
17110 | 97 |
(* insert facts *) |
7419 | 98 |
|
99 |
local |
|
5824 | 100 |
|
21579 | 101 |
fun cut_rule_tac rule = |
52732 | 102 |
rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl); |
6981 | 103 |
|
7419 | 104 |
in |
5824 | 105 |
|
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset
|
106 |
fun insert_tac [] _ = all_tac |
7419 | 107 |
| insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); |
6981 | 108 |
|
7555 | 109 |
val insert_facts = METHOD (ALLGOALS o insert_tac); |
7664 | 110 |
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); |
7419 | 111 |
|
9706 | 112 |
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); |
21592 | 113 |
fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); |
114 |
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL; |
|
9706 | 115 |
|
12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
116 |
end; |
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
117 |
|
9706 | 118 |
|
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
119 |
(* cheating *) |
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
120 |
|
52059 | 121 |
fun cheating ctxt int = METHOD (fn _ => fn st => |
122 |
if int orelse Config.get ctxt quick_and_dirty then |
|
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset
|
123 |
ALLGOALS Skip_Proof.cheat_tac st |
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset
|
124 |
else error "Cheating requires quick_and_dirty mode!"); |
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
125 |
|
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
126 |
|
17110 | 127 |
(* unfold intro/elim rules *) |
128 |
||
52732 | 129 |
fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths)); |
130 |
fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths)); |
|
17110 | 131 |
|
132 |
||
12384 | 133 |
(* unfold/fold definitions *) |
134 |
||
35624 | 135 |
fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths)); |
136 |
fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths)); |
|
6532 | 137 |
|
12384 | 138 |
|
12829 | 139 |
(* atomize rule statements *) |
140 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
141 |
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
|
142 |
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
|
143 |
| atomize true ctxt = |
58002 | 144 |
NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)); |
12829 | 145 |
|
146 |
||
18039 | 147 |
(* this -- resolve facts directly *) |
12384 | 148 |
|
52732 | 149 |
val this = METHOD (EVERY o map (HEADGOAL o rtac)); |
9484 | 150 |
|
151 |
||
18039 | 152 |
(* fact -- composition by facts from context *) |
153 |
||
42360 | 154 |
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
|
155 |
| fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules); |
18039 | 156 |
|
157 |
||
17110 | 158 |
(* assumption *) |
7419 | 159 |
|
160 |
local |
|
161 |
||
19778 | 162 |
fun cond_rtac cond rule = SUBGOAL (fn (prop, i) => |
163 |
if cond (Logic.strip_assums_concl prop) |
|
52732 | 164 |
then rtac rule i else no_tac); |
7419 | 165 |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset
|
166 |
in |
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset
|
167 |
|
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
|
168 |
fun assm_tac ctxt = |
17110 | 169 |
assume_tac APPEND' |
23349 | 170 |
Goal.assume_rule_tac ctxt APPEND' |
19778 | 171 |
cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND' |
172 |
cond_rtac (can Logic.dest_term) Drule.termI; |
|
17110 | 173 |
|
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
174 |
fun all_assm_tac ctxt = |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
175 |
let |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
176 |
fun tac i st = |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
|
23349 | 181 |
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
|
182 |
(fn [] => assm_tac ctxt |
23349 | 183 |
| [fact] => solve_tac [fact] |
184 |
| _ => K no_tac)); |
|
185 |
||
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
186 |
fun finish immed ctxt = |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
187 |
METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac)); |
7419 | 188 |
|
189 |
end; |
|
190 |
||
191 |
||
17110 | 192 |
(* rule etc. -- single-step refinements *) |
12347 | 193 |
|
56204 | 194 |
val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false); |
12347 | 195 |
|
17110 | 196 |
fun trace ctxt rules = |
41379 | 197 |
if Config.get ctxt rule_trace andalso not (null rules) then |
51584 | 198 |
Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules) |
21962 | 199 |
|> Pretty.string_of |> tracing |
200 |
else (); |
|
12347 | 201 |
|
202 |
local |
|
203 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
204 |
fun gen_rule_tac tac ctxt rules facts = |
18841 | 205 |
(fn i => fn st => |
206 |
if null facts then tac rules i st |
|
207 |
else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules)) |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
208 |
THEN_ALL_NEW Goal.norm_hhf_tac ctxt; |
7130 | 209 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
210 |
fun gen_arule_tac tac ctxt j rules facts = |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
211 |
EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac); |
10744 | 212 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
213 |
fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) => |
11785 | 214 |
let |
215 |
val rules = |
|
216 |
if not (null arg_rules) then arg_rules |
|
33369 | 217 |
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
|
218 |
in trace ctxt rules; tac ctxt rules facts i end); |
10309 | 219 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
220 |
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
|
221 |
fun meth' tac x y z = METHOD (HEADGOAL o tac x y z); |
8220 | 222 |
|
7419 | 223 |
in |
224 |
||
52732 | 225 |
val rule_tac = gen_rule_tac resolve_tac; |
10744 | 226 |
val rule = meth rule_tac; |
227 |
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
|
228 |
val some_rule = meth some_rule_tac; |
10744 | 229 |
|
52732 | 230 |
val erule = meth' (gen_arule_tac eresolve_tac); |
231 |
val drule = meth' (gen_arule_tac dresolve_tac); |
|
232 |
val frule = meth' (gen_arule_tac forward_tac); |
|
5824 | 233 |
|
7419 | 234 |
end; |
235 |
||
236 |
||
25270 | 237 |
(* intros_tac -- pervasive search spanned by intro rules *) |
238 |
||
36093
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
239 |
fun gen_intros_tac goals intros facts = |
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
240 |
goals (insert_tac facts THEN' |
25270 | 241 |
REPEAT_ALL_NEW (resolve_tac intros)) |
242 |
THEN Tactic.distinct_subgoals_tac; |
|
243 |
||
36093
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
244 |
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
|
245 |
val try_intros_tac = gen_intros_tac TRYALL; |
25270 | 246 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
247 |
|
8351 | 248 |
(* ML tactics *) |
249 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
250 |
structure ML_Tactic = Proof_Data |
26472
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
251 |
( |
27235 | 252 |
type T = thm list -> tactic; |
26472
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
253 |
fun init _ = undefined; |
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
254 |
); |
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
255 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
256 |
val set_tactic = ML_Tactic.put; |
8351 | 257 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
258 |
fun ml_tactic source ctxt = |
26472
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
259 |
let |
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
260 |
val ctxt' = ctxt |> Context.proof_map |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
261 |
(ML_Context.expression (#pos source) |
27235 | 262 |
"fun tactic (facts: thm list) : tactic" |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56232
diff
changeset
|
263 |
"Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source false source)); |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
264 |
in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end; |
23425 | 265 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
266 |
fun tactic source ctxt = METHOD (ml_tactic source ctxt); |
58002 | 267 |
fun raw_tactic source ctxt = NO_CASES o ml_tactic source ctxt; |
8351 | 268 |
|
269 |
||
5824 | 270 |
|
17110 | 271 |
(** method syntax **) |
272 |
||
273 |
(* method text *) |
|
274 |
||
275 |
type src = Args.src; |
|
5824 | 276 |
|
55765 | 277 |
datatype combinator_info = Combinator_Info of {keywords: Position.T list}; |
278 |
fun combinator_info keywords = Combinator_Info {keywords = keywords}; |
|
279 |
val no_combinator_info = combinator_info []; |
|
280 |
||
58005 | 281 |
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int; |
282 |
||
17110 | 283 |
datatype text = |
55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset
|
284 |
Source of src | |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
285 |
Basic of Proof.context -> method | |
58005 | 286 |
Combinator of combinator_info * combinator * text list; |
55765 | 287 |
|
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
288 |
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
|
289 |
val succeed_text = Basic (K succeed); |
56029
8bedca4bd5a3
clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents:
56026
diff
changeset
|
290 |
val default_text = Source (Args.src ("default", Position.none) []); |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
291 |
val this_text = Basic (K this); |
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
292 |
val done_text = Basic (K (SIMPLE_METHOD all_tac)); |
52059 | 293 |
fun sorry_text int = Basic (fn ctxt => cheating ctxt int); |
17110 | 294 |
|
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
295 |
fun finish_text (NONE, immed) = Basic (finish immed) |
58005 | 296 |
| finish_text (SOME txt, immed) = |
297 |
Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); |
|
17110 | 298 |
|
299 |
||
300 |
(* method definitions *) |
|
5824 | 301 |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
302 |
structure Methods = Generic_Data |
22846 | 303 |
( |
33095
bbd52d2f8696
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
wenzelm
parents:
33092
diff
changeset
|
304 |
type T = ((src -> Proof.context -> method) * string) Name_Space.table; |
33159 | 305 |
val empty : T = Name_Space.empty_table "method"; |
16448 | 306 |
val extend = I; |
33522 | 307 |
fun merge data : T = Name_Space.merge_tables data; |
22846 | 308 |
); |
5824 | 309 |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
310 |
val get_methods = Methods.get o Context.Proof; |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
311 |
|
57937 | 312 |
fun transfer_methods ctxt = |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
313 |
let |
57937 | 314 |
val meths0 = Methods.get (Context.Theory (Proof_Context.theory_of ctxt)); |
315 |
val meths' = Name_Space.merge_tables (meths0, get_methods ctxt); |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
316 |
in Context.proof_map (Methods.put 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
|
317 |
|
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
|
318 |
fun print_methods ctxt = |
22846 | 319 |
let |
55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset
|
320 |
val meths = get_methods ctxt; |
50301 | 321 |
fun prt_meth (name, (_, "")) = Pretty.mark_str name |
42813
6c841fa92fa2
optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents:
42616
diff
changeset
|
322 |
| prt_meth (name, (_, comment)) = |
50301 | 323 |
Pretty.block |
324 |
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
|
22846 | 325 |
in |
56052 | 326 |
[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
|
327 |
|> Pretty.writeln_chunks |
22846 | 328 |
end; |
7611 | 329 |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
330 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
331 |
(* define *) |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
332 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
333 |
fun define_global binding meth comment thy = |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
334 |
let |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
335 |
val context = Context.Theory thy; |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
336 |
val (name, meths') = |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
337 |
Name_Space.define context true (binding, (meth, comment)) (Methods.get context); |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
338 |
in (name, Context.the_theory (Methods.put meths' context)) end; |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
339 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
340 |
fun define binding meth comment = |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
341 |
Local_Theory.background_theory_result (define_global binding meth comment) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
342 |
#-> (fn name => |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
343 |
Local_Theory.map_contexts (K transfer_methods) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
344 |
#> Local_Theory.generic_alias Methods.map binding name |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
345 |
#> pair name); |
31304 | 346 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
347 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
348 |
(* check *) |
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
349 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
350 |
fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt); |
56232 | 351 |
fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src; |
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
352 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
353 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
354 |
(* get methods *) |
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
355 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
356 |
fun method ctxt = |
56029
8bedca4bd5a3
clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents:
56026
diff
changeset
|
357 |
let val table = get_methods ctxt |
8bedca4bd5a3
clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents:
56026
diff
changeset
|
358 |
in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end; |
55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset
|
359 |
|
57863
0c104888f1ca
avoid duplication of warnings stemming from simp/intro declarations etc.;
wenzelm
parents:
56500
diff
changeset
|
360 |
fun method_closure ctxt0 src0 = |
56232 | 361 |
let |
57863
0c104888f1ca
avoid duplication of warnings stemming from simp/intro declarations etc.;
wenzelm
parents:
56500
diff
changeset
|
362 |
val (src1, meth) = check_src ctxt0 src0; |
56232 | 363 |
val src2 = Args.init_assignable src1; |
57863
0c104888f1ca
avoid duplication of warnings stemming from simp/intro declarations etc.;
wenzelm
parents:
56500
diff
changeset
|
364 |
val ctxt = Context_Position.not_really ctxt0; |
58002 | 365 |
val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm)); |
56232 | 366 |
in Args.closure src2 end; |
367 |
||
368 |
fun method_cmd ctxt = method ctxt o method_closure ctxt; |
|
20030 | 369 |
|
5824 | 370 |
|
30512 | 371 |
(* method setup *) |
372 |
||
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
373 |
fun method_syntax scan src ctxt : method = |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
374 |
let val (m, ctxt') = Args.syntax scan src ctxt in m ctxt' end; |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
375 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
376 |
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
|
377 |
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
|
378 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
379 |
fun method_setup name source cmt = |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
380 |
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
381 |
ML_Lex.read_source false source @ |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
382 |
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
383 |
|> ML_Context.expression (#pos source) |
30544 | 384 |
"val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string" |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
385 |
"Context.map_proof (Method.local_setup name scan comment)" |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
386 |
|> Context.proof_map; |
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
387 |
|
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
388 |
|
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
389 |
(* evaluate method text *) |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
390 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
391 |
local |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
392 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
393 |
fun APPEND_CASES (meth: cases_tactic) (cases, st) = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
394 |
meth st |> Seq.map (fn (cases', st') => (cases @ cases', st')); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
395 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
396 |
fun BYPASS_CASES (tac: tactic) (cases, st) = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
397 |
tac st |> Seq.map (pair cases); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
398 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
399 |
val op THEN = Seq.THEN; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
400 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
401 |
fun SELECT_GOALS n method = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
402 |
BYPASS_CASES |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
403 |
(ALLGOALS Goal.conjunction_tac THEN PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
404 |
THEN method |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
405 |
THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1)); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
406 |
|
58005 | 407 |
fun COMBINATOR1 comb [meth] = comb meth |
408 |
| COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; |
|
409 |
||
410 |
fun combinator Then = Seq.EVERY |
|
411 |
| combinator Orelse = Seq.FIRST |
|
412 |
| combinator Try = COMBINATOR1 Seq.TRY |
|
413 |
| combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 |
|
414 |
| combinator (Select_Goals n) = COMBINATOR1 (SELECT_GOALS n); |
|
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
415 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
416 |
in |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
417 |
|
58004 | 418 |
fun evaluate text static_ctxt = |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
419 |
let |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
420 |
fun eval (Basic meth) = APPEND_CASES oo meth |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
421 |
| eval (Source src) = APPEND_CASES oo method_cmd static_ctxt src |
58005 | 422 |
| eval (Combinator (_, c, txts)) = |
423 |
let |
|
424 |
val comb = combinator c; |
|
425 |
val meths = map eval txts |
|
426 |
in fn ctxt => fn facts => comb (map (fn meth => meth ctxt facts) meths) end; |
|
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
427 |
val meth = eval text; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
428 |
in fn ctxt => fn facts => fn st => meth ctxt facts ([], st) end; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
429 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
430 |
end; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
431 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
432 |
|
5884 | 433 |
|
17110 | 434 |
(** concrete syntax **) |
5824 | 435 |
|
5884 | 436 |
(* sections *) |
5824 | 437 |
|
20289 | 438 |
type modifier = (Proof.context -> Proof.context) * attribute; |
7268 | 439 |
|
440 |
local |
|
441 |
||
24010
2ef318813e1a
method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;
wenzelm
parents:
23937
diff
changeset
|
442 |
fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
46466
diff
changeset
|
443 |
fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context); |
5824 | 444 |
|
30540 | 445 |
in |
446 |
||
24022 | 447 |
fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- |
46775
6287653e63ec
canonical argument order for attribute application;
wenzelm
parents:
46466
diff
changeset
|
448 |
(fn (m, ths) => Scan.succeed (swap (app m ths context)))); |
5884 | 449 |
|
30540 | 450 |
fun sections ss = Scan.repeat (section ss); |
5824 | 451 |
|
7268 | 452 |
end; |
453 |
||
5824 | 454 |
|
30515 | 455 |
(* extra rule methods *) |
456 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
457 |
fun xrule_meth meth = |
36950 | 458 |
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
|
459 |
(fn (n, ths) => fn ctxt => meth ctxt n ths); |
30515 | 460 |
|
461 |
||
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
462 |
(* text range *) |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
463 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
464 |
type text_range = text * Position.range; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
465 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
466 |
fun text NONE = NONE |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
467 |
| text (SOME (txt, _)) = SOME txt; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
468 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
469 |
fun position NONE = Position.none |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
470 |
| position (SOME (_, (pos, _))) = pos; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
471 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
472 |
|
55795 | 473 |
(* reports *) |
474 |
||
475 |
local |
|
476 |
||
477 |
fun keyword_positions (Source _) = [] |
|
478 |
| keyword_positions (Basic _) = [] |
|
58005 | 479 |
| keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = |
480 |
keywords @ maps keyword_positions texts; |
|
55795 | 481 |
|
482 |
in |
|
483 |
||
484 |
fun reports_of ((text, (pos, _)): text_range) = |
|
485 |
(pos, Markup.language_method) :: |
|
55917
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55828
diff
changeset
|
486 |
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
|
487 |
(keyword_positions text); |
55795 | 488 |
|
489 |
val report = Position.reports o reports_of; |
|
490 |
||
491 |
end; |
|
492 |
||
493 |
||
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
494 |
(* outer parser *) |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
495 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
496 |
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
|
497 |
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
|
498 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
499 |
local |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
500 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
501 |
fun meth4 x = |
56029
8bedca4bd5a3
clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents:
56026
diff
changeset
|
502 |
(Parse.position Parse.xname >> (fn name => Source (Args.src name [])) || |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
54883
diff
changeset
|
503 |
Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => |
56029
8bedca4bd5a3
clarified Args.src: more abstract type, position refers to name only;
wenzelm
parents:
56026
diff
changeset
|
504 |
Source (Args.src ("cartouche", Token.pos_of tok) [tok])) || |
36950 | 505 |
Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
506 |
and meth3 x = |
55765 | 507 |
(meth4 -- Parse.position (Parse.$$$ "?") |
58005 | 508 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || |
55765 | 509 |
meth4 -- Parse.position (Parse.$$$ "+") |
58005 | 510 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || |
55765 | 511 |
meth4 -- |
512 |
(Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) |
|
513 |
>> (fn (m, (((_, pos1), n), (_, pos2))) => |
|
58005 | 514 |
Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
515 |
meth4) x |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
516 |
and meth2 x = |
56201 | 517 |
(Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Args.src) || |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
518 |
meth3) x |
55765 | 519 |
and meth1 x = |
520 |
(Parse.enum1_positions "," meth2 |
|
58005 | 521 |
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x |
55765 | 522 |
and meth0 x = |
523 |
(Parse.enum1_positions "|" meth1 |
|
58005 | 524 |
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
525 |
|
49866 | 526 |
in |
527 |
||
528 |
val parse = |
|
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
529 |
Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks)); |
49866 | 530 |
|
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
531 |
end; |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
532 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
533 |
|
18708 | 534 |
(* theory setup *) |
5824 | 535 |
|
53171 | 536 |
val _ = Theory.setup |
56204 | 537 |
(setup @{binding fail} (Scan.succeed (K fail)) "force failure" #> |
538 |
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #> |
|
539 |
setup @{binding "-"} (Scan.succeed (K insert_facts)) |
|
30515 | 540 |
"do nothing (insert current facts only)" #> |
56204 | 541 |
setup @{binding insert} (Attrib.thms >> (K o insert)) |
30515 | 542 |
"insert theorems, ignoring facts (improper)" #> |
56204 | 543 |
setup @{binding intro} (Attrib.thms >> (K o intro)) |
30515 | 544 |
"repeatedly apply introduction rules" #> |
56204 | 545 |
setup @{binding elim} (Attrib.thms >> (K o elim)) |
30515 | 546 |
"repeatedly apply elimination rules" #> |
56204 | 547 |
setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #> |
548 |
setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #> |
|
549 |
setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize) |
|
30515 | 550 |
"present local premises as object-level statements" #> |
56204 | 551 |
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
|
552 |
"apply some intro/elim rule" #> |
56204 | 553 |
setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #> |
554 |
setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #> |
|
555 |
setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #> |
|
556 |
setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #> |
|
557 |
setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #> |
|
558 |
setup @{binding assumption} (Scan.succeed assumption) |
|
30515 | 559 |
"proof by assumption, preferring facts" #> |
56204 | 560 |
setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> |
52732 | 561 |
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) |
30515 | 562 |
"rename parameters of goal" #> |
56204 | 563 |
setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> |
52732 | 564 |
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) |
30515 | 565 |
"rotate assumptions of goal" #> |
56500
90f17a04567d
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
wenzelm
parents:
56334
diff
changeset
|
566 |
setup @{binding tactic} (Scan.lift Args.text_source_position >> tactic) |
30515 | 567 |
"ML tactic as proof method" #> |
56500
90f17a04567d
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
wenzelm
parents:
56334
diff
changeset
|
568 |
setup @{binding raw_tactic} (Scan.lift Args.text_source_position >> raw_tactic) |
53171 | 569 |
"ML tactic as raw proof method"); |
5824 | 570 |
|
571 |
||
16145 | 572 |
(*final declarations of this structure!*) |
573 |
val unfold = unfold_meth; |
|
574 |
val fold = fold_meth; |
|
575 |
||
5824 | 576 |
end; |
577 |
||
30508
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
578 |
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
|
579 |
val METHOD = Method.METHOD; |
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
580 |
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
|
581 |
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
|
582 |
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
|
583 |