author | wenzelm |
Mon, 10 Nov 2014 21:49:48 +0100 | |
changeset 58963 | 26bf09b95dda |
parent 58957 | c9e744ea8a38 |
child 58978 | e42da880c61e |
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 |
58957 | 21 |
val intro: Proof.context -> thm list -> method |
22 |
val elim: Proof.context -> 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 |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
70 |
type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T} |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
71 |
val modifier: attribute -> Position.T -> modifier |
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
72 |
val section: modifier parser list -> declaration context_parser |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
73 |
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
|
74 |
type text_range = text * Position.range |
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset
|
75 |
val text: text_range option -> text option |
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset
|
76 |
val position: text_range option -> Position.T |
55795 | 77 |
val reports_of: text_range -> Position.report list |
78 |
val report: text_range -> unit |
|
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
79 |
val parse: text_range parser |
5824 | 80 |
end; |
81 |
||
82 |
structure Method: METHOD = |
|
83 |
struct |
|
84 |
||
12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
85 |
(** proof methods **) |
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
86 |
|
58006 | 87 |
(* method *) |
11731 | 88 |
|
58002 | 89 |
type method = thm list -> cases_tactic; |
11731 | 90 |
|
58030 | 91 |
fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); |
92 |
fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); |
|
5824 | 93 |
|
94 |
val fail = METHOD (K no_tac); |
|
95 |
val succeed = METHOD (K all_tac); |
|
96 |
||
97 |
||
17110 | 98 |
(* insert facts *) |
7419 | 99 |
|
100 |
local |
|
5824 | 101 |
|
21579 | 102 |
fun cut_rule_tac rule = |
58837 | 103 |
resolve_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl]; |
6981 | 104 |
|
7419 | 105 |
in |
5824 | 106 |
|
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset
|
107 |
fun insert_tac [] _ = all_tac |
7419 | 108 |
| insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); |
6981 | 109 |
|
7555 | 110 |
val insert_facts = METHOD (ALLGOALS o insert_tac); |
7664 | 111 |
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); |
7419 | 112 |
|
9706 | 113 |
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); |
21592 | 114 |
fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); |
115 |
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL; |
|
9706 | 116 |
|
12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
117 |
end; |
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
118 |
|
9706 | 119 |
|
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
120 |
(* cheating *) |
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
121 |
|
52059 | 122 |
fun cheating ctxt int = METHOD (fn _ => fn st => |
123 |
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
|
124 |
ALLGOALS Skip_Proof.cheat_tac st |
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset
|
125 |
else error "Cheating requires quick_and_dirty mode!"); |
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
126 |
|
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
127 |
|
17110 | 128 |
(* unfold intro/elim rules *) |
129 |
||
58957 | 130 |
fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths)); |
131 |
fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths)); |
|
17110 | 132 |
|
133 |
||
12384 | 134 |
(* unfold/fold definitions *) |
135 |
||
35624 | 136 |
fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths)); |
137 |
fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths)); |
|
6532 | 138 |
|
12384 | 139 |
|
12829 | 140 |
(* atomize rule statements *) |
141 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
142 |
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
|
143 |
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
|
144 |
| atomize true ctxt = |
58002 | 145 |
NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)); |
12829 | 146 |
|
147 |
||
18039 | 148 |
(* this -- resolve facts directly *) |
12384 | 149 |
|
58837 | 150 |
val this = METHOD (EVERY o map (HEADGOAL o resolve_tac o single)); |
9484 | 151 |
|
152 |
||
18039 | 153 |
(* fact -- composition by facts from context *) |
154 |
||
42360 | 155 |
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
|
156 |
| fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules); |
18039 | 157 |
|
158 |
||
17110 | 159 |
(* assumption *) |
7419 | 160 |
|
161 |
local |
|
162 |
||
19778 | 163 |
fun cond_rtac cond rule = SUBGOAL (fn (prop, i) => |
164 |
if cond (Logic.strip_assums_concl prop) |
|
58837 | 165 |
then resolve_tac [rule] i else no_tac); |
7419 | 166 |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset
|
167 |
in |
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset
|
168 |
|
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
|
169 |
fun assm_tac ctxt = |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
170 |
assume_tac ctxt APPEND' |
23349 | 171 |
Goal.assume_rule_tac ctxt APPEND' |
19778 | 172 |
cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND' |
173 |
cond_rtac (can Logic.dest_term) Drule.termI; |
|
17110 | 174 |
|
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
175 |
fun all_assm_tac ctxt = |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
176 |
let |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
177 |
fun tac i st = |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
|
23349 | 182 |
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
|
183 |
(fn [] => assm_tac ctxt |
23349 | 184 |
| [fact] => solve_tac [fact] |
185 |
| _ => K no_tac)); |
|
186 |
||
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
187 |
fun finish immed ctxt = |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
188 |
METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt)); |
7419 | 189 |
|
190 |
end; |
|
191 |
||
192 |
||
17110 | 193 |
(* rule etc. -- single-step refinements *) |
12347 | 194 |
|
56204 | 195 |
val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false); |
12347 | 196 |
|
17110 | 197 |
fun trace ctxt rules = |
41379 | 198 |
if Config.get ctxt rule_trace andalso not (null rules) then |
51584 | 199 |
Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules) |
21962 | 200 |
|> Pretty.string_of |> tracing |
201 |
else (); |
|
12347 | 202 |
|
203 |
local |
|
204 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
205 |
fun gen_rule_tac tac ctxt rules facts = |
18841 | 206 |
(fn i => fn st => |
207 |
if null facts then tac rules i st |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
208 |
else |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
209 |
Seq.maps (fn rule => (tac o single) rule i st) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
210 |
(Drule.multi_resolves (SOME ctxt) facts rules)) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
211 |
THEN_ALL_NEW Goal.norm_hhf_tac ctxt; |
7130 | 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_arule_tac tac ctxt j rules facts = |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
214 |
EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt)); |
10744 | 215 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
216 |
fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) => |
11785 | 217 |
let |
218 |
val rules = |
|
219 |
if not (null arg_rules) then arg_rules |
|
33369 | 220 |
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
|
221 |
in trace ctxt rules; tac ctxt rules facts i end); |
10309 | 222 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
223 |
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
|
224 |
fun meth' tac x y z = METHOD (HEADGOAL o tac x y z); |
8220 | 225 |
|
7419 | 226 |
in |
227 |
||
52732 | 228 |
val rule_tac = gen_rule_tac resolve_tac; |
10744 | 229 |
val rule = meth rule_tac; |
230 |
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
|
231 |
val some_rule = meth some_rule_tac; |
10744 | 232 |
|
52732 | 233 |
val erule = meth' (gen_arule_tac eresolve_tac); |
234 |
val drule = meth' (gen_arule_tac dresolve_tac); |
|
235 |
val frule = meth' (gen_arule_tac forward_tac); |
|
5824 | 236 |
|
7419 | 237 |
end; |
238 |
||
239 |
||
25270 | 240 |
(* intros_tac -- pervasive search spanned by intro rules *) |
241 |
||
36093
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
242 |
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
|
243 |
goals (insert_tac facts THEN' |
25270 | 244 |
REPEAT_ALL_NEW (resolve_tac intros)) |
245 |
THEN Tactic.distinct_subgoals_tac; |
|
246 |
||
36093
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
247 |
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
|
248 |
val try_intros_tac = gen_intros_tac TRYALL; |
25270 | 249 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
250 |
|
58016 | 251 |
|
252 |
(** method syntax **) |
|
253 |
||
254 |
(* context data *) |
|
8351 | 255 |
|
58016 | 256 |
structure Data = Generic_Data |
26472
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
257 |
( |
58016 | 258 |
type T = |
259 |
((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
|
260 |
(morphism -> thm list -> tactic) option; (*ML tactic*) |
58016 | 261 |
val empty : T = (Name_Space.empty_table "method", NONE); |
262 |
val extend = I; |
|
263 |
fun merge ((tab, tac), (tab', tac')) : T = |
|
264 |
(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
|
265 |
); |
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
266 |
|
58016 | 267 |
val get_methods = fst o Data.get; |
268 |
val map_methods = Data.map o apfst; |
|
269 |
||
270 |
||
271 |
(* ML tactic *) |
|
272 |
||
273 |
val set_tactic = Data.map o apsnd o K o SOME; |
|
274 |
||
275 |
fun the_tactic context = |
|
276 |
(case snd (Data.get context) of |
|
277 |
SOME tac => tac |
|
278 |
| NONE => raise Fail "Undefined ML tactic"); |
|
8351 | 279 |
|
58018
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
280 |
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
|
281 |
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
|
282 |
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
|
283 |
let |
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
284 |
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
|
285 |
ML_Context.expression (#pos source) |
58024 | 286 |
"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
|
287 |
"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
|
288 |
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
|
289 |
in |
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
290 |
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
|
291 |
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
|
292 |
end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context)))); |
8351 | 293 |
|
294 |
||
17110 | 295 |
(* method text *) |
296 |
||
55765 | 297 |
datatype combinator_info = Combinator_Info of {keywords: Position.T list}; |
298 |
fun combinator_info keywords = Combinator_Info {keywords = keywords}; |
|
299 |
val no_combinator_info = combinator_info []; |
|
300 |
||
58005 | 301 |
datatype combinator = Then | Orelse | Try | Repeat1 | Select_Goals of int; |
302 |
||
17110 | 303 |
datatype text = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
304 |
Source of Token.src | |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
305 |
Basic of Proof.context -> method | |
58005 | 306 |
Combinator of combinator_info * combinator * text list; |
55765 | 307 |
|
58006 | 308 |
fun map_source f (Source src) = Source (f src) |
309 |
| map_source _ (Basic meth) = Basic meth |
|
310 |
| map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts); |
|
311 |
||
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
312 |
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
|
313 |
val succeed_text = Basic (K succeed); |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
314 |
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
|
315 |
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
|
316 |
val done_text = Basic (K (SIMPLE_METHOD all_tac)); |
52059 | 317 |
fun sorry_text int = Basic (fn ctxt => cheating ctxt int); |
17110 | 318 |
|
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
319 |
fun finish_text (NONE, immed) = Basic (finish immed) |
58005 | 320 |
| finish_text (SOME txt, immed) = |
321 |
Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); |
|
17110 | 322 |
|
323 |
||
324 |
(* method definitions *) |
|
5824 | 325 |
|
57937 | 326 |
fun transfer_methods ctxt = |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
327 |
let |
58016 | 328 |
val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt)); |
329 |
val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt)); |
|
330 |
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
|
331 |
|
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
|
332 |
fun print_methods ctxt = |
22846 | 333 |
let |
58016 | 334 |
val meths = get_methods (Context.Proof ctxt); |
50301 | 335 |
fun prt_meth (name, (_, "")) = Pretty.mark_str name |
42813
6c841fa92fa2
optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents:
42616
diff
changeset
|
336 |
| prt_meth (name, (_, comment)) = |
50301 | 337 |
Pretty.block |
338 |
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
|
22846 | 339 |
in |
56052 | 340 |
[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
|
341 |
|> Pretty.writeln_chunks |
22846 | 342 |
end; |
7611 | 343 |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
344 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
345 |
(* define *) |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
346 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
347 |
fun define_global binding meth comment thy = |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
348 |
let |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
349 |
val context = Context.Theory thy; |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
350 |
val (name, meths') = |
58016 | 351 |
Name_Space.define context true (binding, (meth, comment)) (get_methods context); |
352 |
in (name, Context.the_theory (map_methods (K meths') context)) end; |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
353 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
354 |
fun define binding meth comment = |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
355 |
Local_Theory.background_theory_result (define_global binding meth comment) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
356 |
#-> (fn name => |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
357 |
Local_Theory.map_contexts (K transfer_methods) |
58016 | 358 |
#> Local_Theory.generic_alias map_methods binding name |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
359 |
#> pair name); |
31304 | 360 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
361 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
362 |
(* check *) |
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
363 |
|
58016 | 364 |
fun check_name ctxt = |
365 |
let val context = Context.Proof ctxt |
|
366 |
in #1 o Name_Space.check context (get_methods context) end; |
|
367 |
||
368 |
fun check_src ctxt src = |
|
369 |
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
|
370 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
371 |
|
30512 | 372 |
(* method setup *) |
373 |
||
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
374 |
fun method_syntax scan src ctxt : method = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
375 |
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
|
376 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
377 |
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
|
378 |
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
|
379 |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55795
diff
changeset
|
380 |
fun method_setup name source cmt = |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
381 |
(ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @ |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
382 |
ML_Lex.read_source false source @ |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
383 |
ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
384 |
|> ML_Context.expression (#pos source) |
30544 | 385 |
"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
|
386 |
"Context.map_proof (Method.local_setup name scan comment)" |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
387 |
|> Context.proof_map; |
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
388 |
|
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
389 |
|
58006 | 390 |
(* prepare methods *) |
391 |
||
392 |
fun method ctxt = |
|
58016 | 393 |
let val table = get_methods (Context.Proof ctxt) |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
394 |
in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end; |
58006 | 395 |
|
396 |
fun method_closure ctxt0 src0 = |
|
397 |
let |
|
58026 | 398 |
val (src1, _) = check_src ctxt0 src0; |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
399 |
val src2 = Token.init_assignable_src src1; |
58006 | 400 |
val ctxt = Context_Position.not_really ctxt0; |
401 |
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
|
402 |
in Token.closure_src src2 end; |
58006 | 403 |
|
404 |
fun method_cmd ctxt = method ctxt o method_closure ctxt; |
|
405 |
||
406 |
||
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
407 |
(* evaluate method text *) |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
408 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
409 |
local |
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 APPEND_CASES (meth: cases_tactic) (cases, st) = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
412 |
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
|
413 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
414 |
fun BYPASS_CASES (tac: tactic) (cases, st) = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
415 |
tac st |> Seq.map (pair cases); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
416 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
417 |
val op THEN = Seq.THEN; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
418 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
419 |
fun SELECT_GOALS n method = |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
420 |
BYPASS_CASES |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
421 |
(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
|
422 |
THEN method |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
423 |
THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1)); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
424 |
|
58005 | 425 |
fun COMBINATOR1 comb [meth] = comb meth |
426 |
| COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; |
|
427 |
||
428 |
fun combinator Then = Seq.EVERY |
|
429 |
| combinator Orelse = Seq.FIRST |
|
430 |
| combinator Try = COMBINATOR1 Seq.TRY |
|
431 |
| combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 |
|
432 |
| 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
|
433 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
434 |
in |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
435 |
|
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset
|
436 |
fun evaluate text ctxt = |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
437 |
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
|
438 |
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
|
439 |
| eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt |
58005 | 440 |
| eval (Combinator (_, c, txts)) = |
441 |
let |
|
442 |
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
|
443 |
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
|
444 |
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
|
445 |
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
|
446 |
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
|
447 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
448 |
end; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
449 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
450 |
|
5884 | 451 |
|
17110 | 452 |
(** concrete syntax **) |
5824 | 453 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
454 |
(* type modifier *) |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
455 |
|
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
456 |
type modifier = |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
457 |
{init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}; |
5824 | 458 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
459 |
fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos}; |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
460 |
|
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
461 |
|
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
462 |
(* sections *) |
7268 | 463 |
|
464 |
local |
|
465 |
||
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
466 |
fun sect (modifier : modifier parser) = Scan.depend (fn context => |
58068 | 467 |
Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier Parse.xthm) >> |
468 |
(fn ((tok, {init, attribute, pos}), xthms) => |
|
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
469 |
let |
58068 | 470 |
val decl = |
471 |
(case Token.get_value tok of |
|
472 |
SOME (Token.Declaration decl) => decl |
|
473 |
| _ => |
|
474 |
let |
|
475 |
val ctxt = Context.proof_of context; |
|
476 |
fun prep_att src = |
|
477 |
let |
|
478 |
val src' = Attrib.check_src ctxt src; |
|
479 |
val _ = List.app (Token.assign NONE) (Token.args_of_src src'); |
|
480 |
in src' end; |
|
481 |
val thms = |
|
482 |
map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms; |
|
483 |
val facts = |
|
484 |
Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)] |
|
485 |
|> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs)); |
|
486 |
val _ = |
|
487 |
Context_Position.report ctxt (Token.pos_of tok) |
|
488 |
(Markup.entity Markup.method_modifierN "" |
|
489 |
|> Markup.properties (Position.def_properties_of pos)); |
|
490 |
fun decl phi = |
|
491 |
Context.mapping I init #> |
|
492 |
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; |
|
493 |
val _ = Token.assign (SOME (Token.Declaration decl)) tok; |
|
494 |
in decl end); |
|
495 |
in (Morphism.form decl context, decl) end)); |
|
5824 | 496 |
|
30540 | 497 |
in |
498 |
||
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
499 |
val section = sect o Scan.first; |
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
500 |
val sections = Scan.repeat o section; |
5824 | 501 |
|
7268 | 502 |
end; |
503 |
||
5824 | 504 |
|
30515 | 505 |
(* extra rule methods *) |
506 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
507 |
fun xrule_meth meth = |
36950 | 508 |
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
|
509 |
(fn (n, ths) => fn ctxt => meth ctxt n ths); |
30515 | 510 |
|
511 |
||
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
512 |
(* text range *) |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
513 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
514 |
type text_range = text * Position.range; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
515 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
516 |
fun text NONE = NONE |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
517 |
| text (SOME (txt, _)) = SOME txt; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
518 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
519 |
fun position NONE = Position.none |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
520 |
| position (SOME (_, (pos, _))) = pos; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
521 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
522 |
|
55795 | 523 |
(* reports *) |
524 |
||
525 |
local |
|
526 |
||
527 |
fun keyword_positions (Source _) = [] |
|
528 |
| keyword_positions (Basic _) = [] |
|
58005 | 529 |
| keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = |
530 |
keywords @ maps keyword_positions texts; |
|
55795 | 531 |
|
532 |
in |
|
533 |
||
534 |
fun reports_of ((text, (pos, _)): text_range) = |
|
535 |
(pos, Markup.language_method) :: |
|
55917
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55828
diff
changeset
|
536 |
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
|
537 |
(keyword_positions text); |
55795 | 538 |
|
539 |
val report = Position.reports o reports_of; |
|
540 |
||
541 |
end; |
|
542 |
||
543 |
||
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
544 |
(* outer parser *) |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
545 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
546 |
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
|
547 |
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
|
548 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
549 |
local |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
550 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
551 |
fun meth4 x = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
552 |
(Parse.position Parse.xname >> (fn name => Source (Token.src name [])) || |
55048
ce34a2934386
implicit "cartouche" method (experimental, undocumented);
wenzelm
parents:
54883
diff
changeset
|
553 |
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
|
554 |
Source (Token.src ("cartouche", Token.pos_of tok) [tok])) || |
36950 | 555 |
Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
556 |
and meth3 x = |
55765 | 557 |
(meth4 -- Parse.position (Parse.$$$ "?") |
58005 | 558 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || |
55765 | 559 |
meth4 -- Parse.position (Parse.$$$ "+") |
58005 | 560 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || |
55765 | 561 |
meth4 -- |
562 |
(Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) |
|
563 |
>> (fn (m, (((_, pos1), n), (_, pos2))) => |
|
58005 | 564 |
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
|
565 |
meth4) x |
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
566 |
and meth2 x = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
567 |
(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
|
568 |
meth3) x |
55765 | 569 |
and meth1 x = |
570 |
(Parse.enum1_positions "," meth2 |
|
58005 | 571 |
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x |
55765 | 572 |
and meth0 x = |
573 |
(Parse.enum1_positions "|" meth1 |
|
58005 | 574 |
>> (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
|
575 |
|
49866 | 576 |
in |
577 |
||
578 |
val parse = |
|
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
55708
diff
changeset
|
579 |
Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks)); |
49866 | 580 |
|
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
581 |
end; |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
582 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
583 |
|
18708 | 584 |
(* theory setup *) |
5824 | 585 |
|
53171 | 586 |
val _ = Theory.setup |
56204 | 587 |
(setup @{binding fail} (Scan.succeed (K fail)) "force failure" #> |
588 |
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #> |
|
589 |
setup @{binding "-"} (Scan.succeed (K insert_facts)) |
|
30515 | 590 |
"do nothing (insert current facts only)" #> |
56204 | 591 |
setup @{binding insert} (Attrib.thms >> (K o insert)) |
30515 | 592 |
"insert theorems, ignoring facts (improper)" #> |
58957 | 593 |
setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths)) |
30515 | 594 |
"repeatedly apply introduction rules" #> |
58957 | 595 |
setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths)) |
30515 | 596 |
"repeatedly apply elimination rules" #> |
56204 | 597 |
setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #> |
598 |
setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #> |
|
599 |
setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize) |
|
30515 | 600 |
"present local premises as object-level statements" #> |
56204 | 601 |
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
|
602 |
"apply some intro/elim rule" #> |
56204 | 603 |
setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #> |
604 |
setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #> |
|
605 |
setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #> |
|
606 |
setup @{binding this} (Scan.succeed (K this)) "apply current facts as rules" #> |
|
607 |
setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #> |
|
608 |
setup @{binding assumption} (Scan.succeed assumption) |
|
30515 | 609 |
"proof by assumption, preferring facts" #> |
56204 | 610 |
setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> |
52732 | 611 |
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) |
30515 | 612 |
"rename parameters of goal" #> |
56204 | 613 |
setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> |
52732 | 614 |
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) |
30515 | 615 |
"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
|
616 |
setup @{binding tactic} (parse_tactic >> (K o METHOD)) |
30515 | 617 |
"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
|
618 |
setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => NO_CASES o tac)) |
53171 | 619 |
"ML tactic as raw proof method"); |
5824 | 620 |
|
621 |
||
16145 | 622 |
(*final declarations of this structure!*) |
623 |
val unfold = unfold_meth; |
|
624 |
val fold = fold_meth; |
|
625 |
||
5824 | 626 |
end; |
627 |
||
30508
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
628 |
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
|
629 |
val METHOD = Method.METHOD; |
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
630 |
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
|
631 |
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
|
632 |
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
|
633 |