author | wenzelm |
Thu, 21 Aug 2014 23:54:27 +0200 | |
changeset 58029 | 2137e60b6f6d |
parent 58026 | 83599179e6eb |
child 58030 | c6b131e651e6 |
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 |
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 | 42 |
type combinator_info |
43 |
val no_combinator_info: combinator_info |
|
58005 | 44 |
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int |
5824 | 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 | 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 | 51 |
val succeed_text: text |
17110 | 52 |
val default_text: text |
53 |
val this_text: text |
|
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 |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
59 |
val method_syntax: (Proof.context -> method) context_parser -> |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
60 |
Token.src -> Proof.context -> method |
30512 | 61 |
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
62 |
val local_setup: binding -> (Proof.context -> method) context_parser -> string -> |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
63 |
local_theory -> local_theory |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
64 |
val method_setup: bstring * Position.T -> Symbol_Pos.source -> string -> |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
65 |
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 |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
68 |
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
|
69 |
val evaluate: text -> Proof.context -> method |
30540 | 70 |
type modifier = (Proof.context -> Proof.context) * attribute |
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
71 |
val section: modifier parser list -> declaration context_parser |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
72 |
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
|
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 |
|
58006 | 86 |
(* 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 |
|
58016 | 248 |
|
249 |
(** method syntax **) |
|
250 |
||
251 |
(* context data *) |
|
8351 | 252 |
|
58016 | 253 |
structure Data = Generic_Data |
26472
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
254 |
( |
58016 | 255 |
type T = |
256 |
((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
|
257 |
(morphism -> thm list -> tactic) option; (*ML tactic*) |
58016 | 258 |
val empty : T = (Name_Space.empty_table "method", NONE); |
259 |
val extend = I; |
|
260 |
fun merge ((tab, tac), (tab', tac')) : T = |
|
261 |
(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
|
262 |
); |
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
263 |
|
58016 | 264 |
val get_methods = fst o Data.get; |
265 |
val map_methods = Data.map o apfst; |
|
266 |
||
267 |
||
268 |
(* ML tactic *) |
|
269 |
||
270 |
val set_tactic = Data.map o apsnd o K o SOME; |
|
271 |
||
272 |
fun the_tactic context = |
|
273 |
(case snd (Data.get context) of |
|
274 |
SOME tac => tac |
|
275 |
| NONE => raise Fail "Undefined ML tactic"); |
|
8351 | 276 |
|
58018
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
277 |
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
|
278 |
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
|
279 |
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
|
280 |
let |
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
281 |
val context' = context |> |
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
282 |
ML_Context.expression (#pos source) |
58024 | 283 |
"fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic" |
58018
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
284 |
"Method.set_tactic tactic" (ML_Lex.read_source false 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 |
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
|
286 |
in |
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
287 |
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
|
288 |
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
|
289 |
end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context)))); |
8351 | 290 |
|
291 |
||
17110 | 292 |
(* method text *) |
293 |
||
55765 | 294 |
datatype combinator_info = Combinator_Info of {keywords: Position.T list}; |
295 |
fun combinator_info keywords = Combinator_Info {keywords = keywords}; |
|
296 |
val no_combinator_info = combinator_info []; |
|
297 |
||
58005 | 298 |
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int; |
299 |
||
17110 | 300 |
datatype text = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
301 |
Source of Token.src | |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
302 |
Basic of Proof.context -> method | |
58005 | 303 |
Combinator of combinator_info * combinator * text list; |
55765 | 304 |
|
58006 | 305 |
fun map_source f (Source src) = Source (f src) |
306 |
| map_source _ (Basic meth) = Basic meth |
|
307 |
| map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts); |
|
308 |
||
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
309 |
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
|
310 |
val succeed_text = Basic (K succeed); |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
311 |
val default_text = Source (Token.src ("default", Position.none) []); |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
312 |
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
|
313 |
val done_text = Basic (K (SIMPLE_METHOD all_tac)); |
52059 | 314 |
fun sorry_text int = Basic (fn ctxt => cheating ctxt int); |
17110 | 315 |
|
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
316 |
fun finish_text (NONE, immed) = Basic (finish immed) |
58005 | 317 |
| finish_text (SOME txt, immed) = |
318 |
Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); |
|
17110 | 319 |
|
320 |
||
321 |
(* method definitions *) |
|
5824 | 322 |
|
57937 | 323 |
fun transfer_methods ctxt = |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
324 |
let |
58016 | 325 |
val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt)); |
326 |
val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt)); |
|
327 |
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
|
328 |
|
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
|
329 |
fun print_methods ctxt = |
22846 | 330 |
let |
58016 | 331 |
val meths = get_methods (Context.Proof ctxt); |
50301 | 332 |
fun prt_meth (name, (_, "")) = Pretty.mark_str name |
42813
6c841fa92fa2
optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents:
42616
diff
changeset
|
333 |
| prt_meth (name, (_, comment)) = |
50301 | 334 |
Pretty.block |
335 |
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
|
22846 | 336 |
in |
56052 | 337 |
[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
|
338 |
|> Pretty.writeln_chunks |
22846 | 339 |
end; |
7611 | 340 |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
341 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
342 |
(* define *) |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
343 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
344 |
fun define_global binding meth comment thy = |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
345 |
let |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
346 |
val context = Context.Theory thy; |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
347 |
val (name, meths') = |
58016 | 348 |
Name_Space.define context true (binding, (meth, comment)) (get_methods context); |
349 |
in (name, Context.the_theory (map_methods (K meths') context)) end; |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
350 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
351 |
fun define binding meth comment = |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
352 |
Local_Theory.background_theory_result (define_global binding meth comment) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
353 |
#-> (fn name => |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
354 |
Local_Theory.map_contexts (K transfer_methods) |
58016 | 355 |
#> Local_Theory.generic_alias map_methods binding name |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
356 |
#> pair name); |
31304 | 357 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
358 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
359 |
(* check *) |
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
360 |
|
58016 | 361 |
fun check_name ctxt = |
362 |
let val context = Context.Proof ctxt |
|
363 |
in #1 o Name_Space.check context (get_methods context) end; |
|
364 |
||
365 |
fun check_src ctxt src = |
|
366 |
Token.check_src ctxt (get_methods (Context.Proof ctxt)) src; |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
367 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
368 |
|
30512 | 369 |
(* method setup *) |
370 |
||
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
371 |
fun method_syntax scan src ctxt : method = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
372 |
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
|
373 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
374 |
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
|
375 |
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
|
376 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
377 |
fun method_setup name source cmt = |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
378 |
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
379 |
ML_Lex.read_source false source @ |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
380 |
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
381 |
|> ML_Context.expression (#pos source) |
30544 | 382 |
"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
|
383 |
"Context.map_proof (Method.local_setup name scan comment)" |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
384 |
|> Context.proof_map; |
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
385 |
|
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
386 |
|
58006 | 387 |
(* prepare methods *) |
388 |
||
389 |
fun method ctxt = |
|
58016 | 390 |
let val table = get_methods (Context.Proof ctxt) |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
391 |
in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end; |
58006 | 392 |
|
393 |
fun method_closure ctxt0 src0 = |
|
394 |
let |
|
58026 | 395 |
val (src1, _) = check_src ctxt0 src0; |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
396 |
val src2 = Token.init_assignable_src src1; |
58006 | 397 |
val ctxt = Context_Position.not_really ctxt0; |
398 |
val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm)); |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
399 |
in Token.closure_src src2 end; |
58006 | 400 |
|
401 |
fun method_cmd ctxt = method ctxt o method_closure ctxt; |
|
402 |
||
403 |
||
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
404 |
(* evaluate method text *) |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
405 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
406 |
local |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
407 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
408 |
fun APPEND_CASES (meth: cases_tactic) (cases, st) = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
409 |
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
|
410 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
411 |
fun BYPASS_CASES (tac: tactic) (cases, st) = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
412 |
tac st |> Seq.map (pair cases); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
413 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
414 |
val op THEN = Seq.THEN; |
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 |
fun SELECT_GOALS n method = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
417 |
BYPASS_CASES |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
418 |
(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
|
419 |
THEN method |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
420 |
THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1)); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
421 |
|
58005 | 422 |
fun COMBINATOR1 comb [meth] = comb meth |
423 |
| COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; |
|
424 |
||
425 |
fun combinator Then = Seq.EVERY |
|
426 |
| combinator Orelse = Seq.FIRST |
|
427 |
| combinator Try = COMBINATOR1 Seq.TRY |
|
428 |
| combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 |
|
429 |
| 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
|
430 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
431 |
in |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
432 |
|
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset
|
433 |
fun evaluate text ctxt = |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
434 |
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
|
435 |
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
|
436 |
| eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt |
58005 | 437 |
| eval (Combinator (_, c, txts)) = |
438 |
let |
|
439 |
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
|
440 |
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
|
441 |
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
|
442 |
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
|
443 |
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
|
444 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
445 |
end; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
446 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
447 |
|
5884 | 448 |
|
17110 | 449 |
(** concrete syntax **) |
5824 | 450 |
|
5884 | 451 |
(* sections *) |
5824 | 452 |
|
20289 | 453 |
type modifier = (Proof.context -> Proof.context) * attribute; |
7268 | 454 |
|
455 |
local |
|
456 |
||
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
457 |
fun sect modifier = Scan.depend (fn context => |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
458 |
let |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
459 |
val ctxt = Context.proof_of context; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
460 |
fun prep_att src = |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
461 |
let |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
462 |
val src' = Attrib.check_src ctxt src; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
463 |
val _ = List.app (Token.assign NONE) (Token.args_of_src src'); |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
464 |
in src' end; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
465 |
val parse_thm = |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
466 |
Parse.xthm >> (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)); |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
467 |
in |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
468 |
Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier parse_thm) >> |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
469 |
(fn ((tok, (init, att)), thms) => |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
470 |
let |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
471 |
val decl = |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
472 |
(case Token.get_value tok of |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
473 |
SOME (Token.Declaration decl) => decl |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
474 |
| _ => |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
475 |
let |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
476 |
val facts = |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
477 |
Attrib.partial_evaluation ctxt |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
478 |
[((Binding.empty, [Attrib.internal (K att)]), thms)]; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
479 |
fun decl phi = |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
480 |
Context.mapping I init #> |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
481 |
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
482 |
val _ = Token.assign (SOME (Token.Declaration decl)) tok; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
483 |
in decl end); |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
484 |
in (Morphism.form decl context, decl) end) |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
485 |
end); |
5824 | 486 |
|
30540 | 487 |
in |
488 |
||
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
489 |
val section = sect o Scan.first; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
490 |
val sections = Scan.repeat o section; |
5824 | 491 |
|
7268 | 492 |
end; |
493 |
||
5824 | 494 |
|
30515 | 495 |
(* extra rule methods *) |
496 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
497 |
fun xrule_meth meth = |
36950 | 498 |
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
|
499 |
(fn (n, ths) => fn ctxt => meth ctxt n ths); |
30515 | 500 |
|
501 |
||
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
502 |
(* text range *) |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
503 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
504 |
type text_range = text * Position.range; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
505 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
506 |
fun text NONE = NONE |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
507 |
| text (SOME (txt, _)) = SOME txt; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
508 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
509 |
fun position NONE = Position.none |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
510 |
| position (SOME (_, (pos, _))) = pos; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
511 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
512 |
|
55795 | 513 |
(* reports *) |
514 |
||
515 |
local |
|
516 |
||
517 |
fun keyword_positions (Source _) = [] |
|
518 |
| keyword_positions (Basic _) = [] |
|
58005 | 519 |
| keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = |
520 |
keywords @ maps keyword_positions texts; |
|
55795 | 521 |
|
522 |
in |
|
523 |
||
524 |
fun reports_of ((text, (pos, _)): text_range) = |
|
525 |
(pos, Markup.language_method) :: |
|
55917
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55828
diff
changeset
|
526 |
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
|
527 |
(keyword_positions text); |
55795 | 528 |
|
529 |
val report = Position.reports o reports_of; |
|
530 |
||
531 |
end; |
|
532 |
||
533 |
||
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
534 |
(* outer parser *) |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
535 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
536 |
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
|
537 |
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
|
538 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
539 |
local |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
540 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
541 |
fun meth4 x = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
542 |
(Parse.position Parse.xname >> (fn name => Source (Token.src name [])) || |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
54883
diff
changeset
|
543 |
Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
544 |
Source (Token.src ("cartouche", Token.pos_of tok) [tok])) || |
36950 | 545 |
Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
546 |
and meth3 x = |
55765 | 547 |
(meth4 -- Parse.position (Parse.$$$ "?") |
58005 | 548 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || |
55765 | 549 |
meth4 -- Parse.position (Parse.$$$ "+") |
58005 | 550 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || |
55765 | 551 |
meth4 -- |
552 |
(Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) |
|
553 |
>> (fn (m, (((_, pos1), n), (_, pos2))) => |
|
58005 | 554 |
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
|
555 |
meth4) x |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
556 |
and meth2 x = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
557 |
(Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) || |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
558 |
meth3) x |
55765 | 559 |
and meth1 x = |
560 |
(Parse.enum1_positions "," meth2 |
|
58005 | 561 |
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x |
55765 | 562 |
and meth0 x = |
563 |
(Parse.enum1_positions "|" meth1 |
|
58005 | 564 |
>> (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
|
565 |
|
49866 | 566 |
in |
567 |
||
568 |
val parse = |
|
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
569 |
Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks)); |
49866 | 570 |
|
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
571 |
end; |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
572 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
573 |
|
18708 | 574 |
(* theory setup *) |
5824 | 575 |
|
53171 | 576 |
val _ = Theory.setup |
56204 | 577 |
(setup @{binding fail} (Scan.succeed (K fail)) "force failure" #> |
578 |
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #> |
|
579 |
setup @{binding "-"} (Scan.succeed (K insert_facts)) |
|
30515 | 580 |
"do nothing (insert current facts only)" #> |
56204 | 581 |
setup @{binding insert} (Attrib.thms >> (K o insert)) |
30515 | 582 |
"insert theorems, ignoring facts (improper)" #> |
56204 | 583 |
setup @{binding intro} (Attrib.thms >> (K o intro)) |
30515 | 584 |
"repeatedly apply introduction rules" #> |
56204 | 585 |
setup @{binding elim} (Attrib.thms >> (K o elim)) |
30515 | 586 |
"repeatedly apply elimination rules" #> |
56204 | 587 |
setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #> |
588 |
setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #> |
|
589 |
setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize) |
|
30515 | 590 |
"present local premises as object-level statements" #> |
56204 | 591 |
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
|
592 |
"apply some intro/elim rule" #> |
56204 | 593 |
setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #> |
594 |
setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #> |
|
595 |
setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #> |
|
596 |
setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #> |
|
597 |
setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #> |
|
598 |
setup @{binding assumption} (Scan.succeed assumption) |
|
30515 | 599 |
"proof by assumption, preferring facts" #> |
56204 | 600 |
setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> |
52732 | 601 |
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) |
30515 | 602 |
"rename parameters of goal" #> |
56204 | 603 |
setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> |
52732 | 604 |
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) |
30515 | 605 |
"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
|
606 |
setup @{binding tactic} (parse_tactic >> (K o METHOD)) |
30515 | 607 |
"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
|
608 |
setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => NO_CASES o tac)) |
53171 | 609 |
"ML tactic as raw proof method"); |
5824 | 610 |
|
611 |
||
16145 | 612 |
(*final declarations of this structure!*) |
613 |
val unfold = unfold_meth; |
|
614 |
val fold = fold_meth; |
|
615 |
||
5824 | 616 |
end; |
617 |
||
30508
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
618 |
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
|
619 |
val METHOD = Method.METHOD; |
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
620 |
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
|
621 |
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
|
622 |
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
|
623 |