author | wenzelm |
Fri, 11 Dec 2015 13:44:20 +0100 | |
changeset 61834 | 2154e6c8d52d |
parent 61814 | 1ca1142e1711 |
child 61841 | 4d3527b94f2a |
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 |
||
61834 | 7 |
infix 1 THEN_ALL_NEW_CASES; |
8 |
||
9 |
signature BASIC_METHOD = |
|
10 |
sig |
|
11 |
type cases_state = Rule_Cases.cases * thm |
|
12 |
type cases_tactic = thm -> cases_state Seq.seq |
|
13 |
val CASES: Rule_Cases.cases -> tactic -> cases_tactic |
|
14 |
val EMPTY_CASES: tactic -> cases_tactic |
|
15 |
val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic |
|
16 |
val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic |
|
17 |
end; |
|
18 |
||
5824 | 19 |
signature METHOD = |
20 |
sig |
|
61834 | 21 |
include BASIC_METHOD |
58002 | 22 |
type method = thm list -> cases_tactic |
18227 | 23 |
val METHOD_CASES: (thm list -> cases_tactic) -> method |
17110 | 24 |
val METHOD: (thm list -> tactic) -> method |
25 |
val fail: method |
|
26 |
val succeed: method |
|
27 |
val insert_tac: thm list -> int -> tactic |
|
28 |
val insert: thm list -> method |
|
29 |
val insert_facts: method |
|
30 |
val SIMPLE_METHOD: tactic -> method |
|
21592 | 31 |
val SIMPLE_METHOD': (int -> tactic) -> method |
32 |
val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method |
|
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61164
diff
changeset
|
33 |
val goal_cases_tac: Proof.context -> string list -> cases_tactic |
52059 | 34 |
val cheating: Proof.context -> bool -> method |
58957 | 35 |
val intro: Proof.context -> thm list -> method |
36 |
val elim: Proof.context -> thm list -> method |
|
20289 | 37 |
val unfold: thm list -> Proof.context -> method |
38 |
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
|
39 |
val atomize: bool -> Proof.context -> method |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
40 |
val this: Proof.context -> method |
20289 | 41 |
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
|
42 |
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
|
43 |
val all_assm_tac: Proof.context -> tactic |
20289 | 44 |
val assumption: Proof.context -> method |
46466
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45375
diff
changeset
|
45 |
val rule_trace: bool Config.T |
20289 | 46 |
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
|
47 |
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
|
48 |
val some_rule_tac: Proof.context -> thm list -> thm list -> int -> tactic |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
49 |
val intros_tac: Proof.context -> thm list -> thm list -> tactic |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
50 |
val try_intros_tac: Proof.context -> thm list -> thm list -> tactic |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
val set_tactic: (morphism -> thm list -> tactic) -> Context.generic -> Context.generic |
55765 | 56 |
type combinator_info |
57 |
val no_combinator_info: combinator_info |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
58 |
datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int |
5824 | 59 |
datatype text = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
60 |
Source of Token.src | |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
61 |
Basic of Proof.context -> method | |
58005 | 62 |
Combinator of combinator_info * combinator * text list |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
63 |
val map_source: (Token.src -> Token.src) -> text -> text |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
64 |
val primitive_text: (Proof.context -> thm -> thm) -> text |
17857 | 65 |
val succeed_text: text |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60609
diff
changeset
|
66 |
val standard_text: text |
17110 | 67 |
val this_text: text |
68 |
val done_text: text |
|
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
69 |
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
|
70 |
val finish_text: text option * bool -> text |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59914
diff
changeset
|
71 |
val print_methods: bool -> Proof.context -> unit |
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
|
72 |
val check_name: Proof.context -> xstring * Position.T -> string |
59907 | 73 |
val check_src: Proof.context -> Token.src -> Token.src |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
74 |
val check_text: Proof.context -> text -> text |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
75 |
val method_syntax: (Proof.context -> method) context_parser -> |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
76 |
Token.src -> Proof.context -> method |
30512 | 77 |
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
78 |
val local_setup: binding -> (Proof.context -> method) context_parser -> string -> |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
79 |
local_theory -> local_theory |
59064 | 80 |
val method_setup: bstring * Position.T -> Input.source -> string -> local_theory -> local_theory |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
81 |
val method: Proof.context -> Token.src -> Proof.context -> method |
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
82 |
val method_closure: Proof.context -> Token.src -> Token.src |
59909 | 83 |
val closure: bool Config.T |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
84 |
val method_cmd: Proof.context -> Token.src -> Proof.context -> method |
60553 | 85 |
val detect_closure_state: thm -> bool |
60609 | 86 |
val STATIC: (unit -> unit) -> cases_tactic |
60553 | 87 |
val RUNTIME: cases_tactic -> cases_tactic |
60554 | 88 |
val sleep: Time.time -> cases_tactic |
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset
|
89 |
val evaluate: text -> Proof.context -> method |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
90 |
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
|
91 |
val modifier: attribute -> Position.T -> modifier |
59982
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
92 |
val old_section_parser: bool Config.T |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
93 |
val sections: modifier parser list -> unit context_parser |
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset
|
94 |
type text_range = text * Position.range |
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset
|
95 |
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
|
96 |
val position: text_range option -> Position.T |
55795 | 97 |
val reports_of: text_range -> Position.report list |
98 |
val report: text_range -> unit |
|
59981 | 99 |
val parser: int -> text_range parser |
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
100 |
val parse: text_range parser |
5824 | 101 |
end; |
102 |
||
103 |
structure Method: METHOD = |
|
104 |
struct |
|
105 |
||
12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
106 |
(** proof methods **) |
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
107 |
|
61834 | 108 |
(* tactics with cases *) |
109 |
||
110 |
type cases_state = Rule_Cases.cases * thm; |
|
111 |
type cases_tactic = thm -> cases_state Seq.seq; |
|
112 |
||
113 |
fun CASES cases tac st = Seq.map (pair cases) (tac st); |
|
114 |
fun EMPTY_CASES tac = CASES [] tac; |
|
115 |
||
116 |
fun SUBGOAL_CASES tac i st = |
|
117 |
(case try Logic.nth_prem (i, Thm.prop_of st) of |
|
118 |
SOME goal => tac (goal, i) st |
|
119 |
| NONE => Seq.empty); |
|
120 |
||
121 |
fun (tac1 THEN_ALL_NEW_CASES tac2) i st = |
|
122 |
st |> tac1 i |> Seq.maps (fn (cases, st') => |
|
123 |
CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'); |
|
124 |
||
125 |
||
126 |
(* type method *) |
|
11731 | 127 |
|
58002 | 128 |
type method = thm list -> cases_tactic; |
11731 | 129 |
|
59953 | 130 |
fun METHOD_CASES tac : method = |
131 |
fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); |
|
132 |
||
133 |
fun METHOD tac : method = |
|
134 |
fn facts => EMPTY_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); |
|
5824 | 135 |
|
136 |
val fail = METHOD (K no_tac); |
|
137 |
val succeed = METHOD (K all_tac); |
|
138 |
||
139 |
||
17110 | 140 |
(* insert facts *) |
7419 | 141 |
|
142 |
local |
|
5824 | 143 |
|
21579 | 144 |
fun cut_rule_tac rule = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
145 |
resolve0_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl]; |
6981 | 146 |
|
7419 | 147 |
in |
5824 | 148 |
|
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset
|
149 |
fun insert_tac [] _ = all_tac |
7419 | 150 |
| insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); |
6981 | 151 |
|
7555 | 152 |
val insert_facts = METHOD (ALLGOALS o insert_tac); |
7664 | 153 |
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); |
7419 | 154 |
|
9706 | 155 |
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); |
21592 | 156 |
fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); |
157 |
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL; |
|
9706 | 158 |
|
12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
159 |
end; |
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset
|
160 |
|
9706 | 161 |
|
60578 | 162 |
(* goals as cases *) |
163 |
||
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61164
diff
changeset
|
164 |
fun goal_cases_tac ctxt case_names st = |
60578 | 165 |
let |
166 |
val cases = |
|
167 |
(if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names) |
|
168 |
|> map (rpair [] o rpair []) |
|
169 |
|> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st)); |
|
170 |
in Seq.single (cases, st) end; |
|
171 |
||
172 |
||
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
173 |
(* cheating *) |
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
174 |
|
52059 | 175 |
fun cheating ctxt int = METHOD (fn _ => fn st => |
176 |
if int orelse Config.get ctxt quick_and_dirty then |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
177 |
ALLGOALS (Skip_Proof.cheat_tac ctxt) st |
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset
|
178 |
else error "Cheating requires quick_and_dirty mode!"); |
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
179 |
|
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
180 |
|
17110 | 181 |
(* unfold intro/elim rules *) |
182 |
||
58957 | 183 |
fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths)); |
184 |
fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths)); |
|
17110 | 185 |
|
186 |
||
12384 | 187 |
(* unfold/fold definitions *) |
188 |
||
35624 | 189 |
fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths)); |
190 |
fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths)); |
|
6532 | 191 |
|
12384 | 192 |
|
12829 | 193 |
(* atomize rule statements *) |
194 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
195 |
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
|
196 |
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
|
197 |
| atomize true ctxt = |
59953 | 198 |
EMPTY_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)); |
12829 | 199 |
|
200 |
||
18039 | 201 |
(* this -- resolve facts directly *) |
12384 | 202 |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
203 |
fun this ctxt = METHOD (EVERY o map (HEADGOAL o resolve_tac ctxt o single)); |
9484 | 204 |
|
205 |
||
18039 | 206 |
(* fact -- composition by facts from context *) |
207 |
||
42360 | 208 |
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
|
209 |
| fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules); |
18039 | 210 |
|
211 |
||
17110 | 212 |
(* assumption *) |
7419 | 213 |
|
214 |
local |
|
215 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
216 |
fun cond_rtac ctxt cond rule = SUBGOAL (fn (prop, i) => |
19778 | 217 |
if cond (Logic.strip_assums_concl prop) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
218 |
then resolve_tac ctxt [rule] i else no_tac); |
7419 | 219 |
|
29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset
|
220 |
in |
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset
|
221 |
|
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
|
222 |
fun assm_tac ctxt = |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
223 |
assume_tac ctxt APPEND' |
23349 | 224 |
Goal.assume_rule_tac ctxt APPEND' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
225 |
cond_rtac ctxt (can Logic.dest_equals) Drule.reflexive_thm APPEND' |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
226 |
cond_rtac ctxt (can Logic.dest_term) Drule.termI; |
17110 | 227 |
|
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
228 |
fun all_assm_tac ctxt = |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
229 |
let |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
230 |
fun tac i st = |
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
231 |
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
|
232 |
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
|
233 |
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
|
234 |
|
23349 | 235 |
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
|
236 |
(fn [] => assm_tac ctxt |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
237 |
| [fact] => solve_tac ctxt [fact] |
23349 | 238 |
| _ => K no_tac)); |
239 |
||
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
240 |
fun finish immed ctxt = |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
241 |
METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt)); |
7419 | 242 |
|
243 |
end; |
|
244 |
||
245 |
||
17110 | 246 |
(* rule etc. -- single-step refinements *) |
12347 | 247 |
|
56204 | 248 |
val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false); |
12347 | 249 |
|
17110 | 250 |
fun trace ctxt rules = |
41379 | 251 |
if Config.get ctxt rule_trace andalso not (null rules) then |
61268 | 252 |
Pretty.big_list "rules:" (map (Thm.pretty_thm_item ctxt) rules) |
21962 | 253 |
|> Pretty.string_of |> tracing |
254 |
else (); |
|
12347 | 255 |
|
256 |
local |
|
257 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
258 |
fun gen_rule_tac tac ctxt rules facts = |
18841 | 259 |
(fn i => fn st => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
260 |
if null facts then tac ctxt rules i st |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
261 |
else |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
262 |
Seq.maps (fn rule => (tac ctxt o single) rule i st) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset
|
263 |
(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
|
264 |
THEN_ALL_NEW Goal.norm_hhf_tac ctxt; |
7130 | 265 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
266 |
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
|
267 |
EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt)); |
10744 | 268 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
269 |
fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) => |
11785 | 270 |
let |
271 |
val rules = |
|
272 |
if not (null arg_rules) then arg_rules |
|
61049 | 273 |
else flat (Context_Rules.find_rules ctxt false facts goal); |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
274 |
in trace ctxt rules; tac ctxt rules facts i end); |
10309 | 275 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
276 |
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
|
277 |
fun meth' tac x y z = METHOD (HEADGOAL o tac x y z); |
8220 | 278 |
|
7419 | 279 |
in |
280 |
||
52732 | 281 |
val rule_tac = gen_rule_tac resolve_tac; |
10744 | 282 |
val rule = meth rule_tac; |
283 |
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
|
284 |
val some_rule = meth some_rule_tac; |
10744 | 285 |
|
52732 | 286 |
val erule = meth' (gen_arule_tac eresolve_tac); |
287 |
val drule = meth' (gen_arule_tac dresolve_tac); |
|
288 |
val frule = meth' (gen_arule_tac forward_tac); |
|
5824 | 289 |
|
7419 | 290 |
end; |
291 |
||
292 |
||
25270 | 293 |
(* intros_tac -- pervasive search spanned by intro rules *) |
294 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
295 |
fun gen_intros_tac goals ctxt intros facts = |
36093
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
296 |
goals (insert_tac facts THEN' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
297 |
REPEAT_ALL_NEW (resolve_tac ctxt intros)) |
25270 | 298 |
THEN Tactic.distinct_subgoals_tac; |
299 |
||
36093
0880493627ca
Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset
|
300 |
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
|
301 |
val try_intros_tac = gen_intros_tac TRYALL; |
25270 | 302 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
303 |
|
58016 | 304 |
|
305 |
(** method syntax **) |
|
306 |
||
307 |
(* context data *) |
|
8351 | 308 |
|
58016 | 309 |
structure Data = Generic_Data |
26472
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
310 |
( |
58016 | 311 |
type T = |
312 |
((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
|
313 |
(morphism -> thm list -> tactic) option; (*ML tactic*) |
58016 | 314 |
val empty : T = (Name_Space.empty_table "method", NONE); |
315 |
val extend = I; |
|
316 |
fun merge ((tab, tac), (tab', tac')) : T = |
|
317 |
(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
|
318 |
); |
9afdd61cf528
ml_tactic: non-critical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset
|
319 |
|
58016 | 320 |
val get_methods = fst o Data.get; |
321 |
val map_methods = Data.map o apfst; |
|
322 |
||
323 |
||
324 |
(* ML tactic *) |
|
325 |
||
326 |
val set_tactic = Data.map o apsnd o K o SOME; |
|
327 |
||
328 |
fun the_tactic context = |
|
329 |
(case snd (Data.get context) of |
|
330 |
SOME tac => tac |
|
331 |
| NONE => raise Fail "Undefined ML tactic"); |
|
8351 | 332 |
|
58018
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
333 |
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
|
334 |
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
|
335 |
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
|
336 |
let |
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
337 |
val context' = context |> |
59064 | 338 |
ML_Context.expression (Input.range_of source) |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset
|
339 |
"tactic" "Morphism.morphism -> thm list -> tactic" |
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset
|
340 |
"Method.set_tactic tactic" |
59067 | 341 |
(ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @ |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset
|
342 |
ML_Lex.read_source false source); |
58018
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
343 |
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
|
344 |
in |
beb4b7c0bb30
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset
|
345 |
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
|
346 |
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
|
347 |
end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context)))); |
8351 | 348 |
|
349 |
||
17110 | 350 |
(* method text *) |
351 |
||
55765 | 352 |
datatype combinator_info = Combinator_Info of {keywords: Position.T list}; |
353 |
fun combinator_info keywords = Combinator_Info {keywords = keywords}; |
|
354 |
val no_combinator_info = combinator_info []; |
|
355 |
||
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
356 |
datatype combinator = Then | Then_All_New | Orelse | Try | Repeat1 | Select_Goals of int; |
58005 | 357 |
|
17110 | 358 |
datatype text = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
359 |
Source of Token.src | |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
360 |
Basic of Proof.context -> method | |
58005 | 361 |
Combinator of combinator_info * combinator * text list; |
55765 | 362 |
|
58006 | 363 |
fun map_source f (Source src) = Source (f src) |
364 |
| map_source _ (Basic meth) = Basic meth |
|
365 |
| map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts); |
|
366 |
||
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
367 |
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
|
368 |
val succeed_text = Basic (K succeed); |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
369 |
val standard_text = Source (Token.make_src ("standard", Position.none) []); |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
370 |
val this_text = Basic this; |
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset
|
371 |
val done_text = Basic (K (SIMPLE_METHOD all_tac)); |
52059 | 372 |
fun sorry_text int = Basic (fn ctxt => cheating ctxt int); |
17110 | 373 |
|
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset
|
374 |
fun finish_text (NONE, immed) = Basic (finish immed) |
58005 | 375 |
| finish_text (SOME txt, immed) = |
376 |
Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); |
|
17110 | 377 |
|
378 |
||
379 |
(* method definitions *) |
|
5824 | 380 |
|
57937 | 381 |
fun transfer_methods ctxt = |
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
382 |
let |
58016 | 383 |
val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt)); |
384 |
val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt)); |
|
385 |
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
|
386 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59914
diff
changeset
|
387 |
fun print_methods verbose ctxt = |
22846 | 388 |
let |
58016 | 389 |
val meths = get_methods (Context.Proof ctxt); |
50301 | 390 |
fun prt_meth (name, (_, "")) = Pretty.mark_str name |
42813
6c841fa92fa2
optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents:
42616
diff
changeset
|
391 |
| prt_meth (name, (_, comment)) = |
50301 | 392 |
Pretty.block |
393 |
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); |
|
22846 | 394 |
in |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59914
diff
changeset
|
395 |
[Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table verbose ctxt meths))] |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56278
diff
changeset
|
396 |
|> Pretty.writeln_chunks |
22846 | 397 |
end; |
7611 | 398 |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
399 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
400 |
(* define *) |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
401 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
402 |
fun define_global binding meth comment thy = |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
403 |
let |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
404 |
val context = Context.Theory thy; |
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
405 |
val (name, meths') = |
58016 | 406 |
Name_Space.define context true (binding, (meth, comment)) (get_methods context); |
407 |
in (name, Context.the_theory (map_methods (K meths') context)) end; |
|
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
408 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
409 |
fun define binding meth comment = |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
410 |
Local_Theory.background_theory_result (define_global binding meth comment) |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
411 |
#-> (fn name => |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
412 |
Local_Theory.map_contexts (K transfer_methods) |
58016 | 413 |
#> Local_Theory.generic_alias map_methods binding name |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
414 |
#> pair name); |
31304 | 415 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
416 |
|
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
417 |
(* check *) |
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
418 |
|
58016 | 419 |
fun check_name ctxt = |
420 |
let val context = Context.Proof ctxt |
|
421 |
in #1 o Name_Space.check context (get_methods context) end; |
|
422 |
||
59907 | 423 |
fun check_src ctxt = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
424 |
#1 o Token.check_src ctxt (get_methods o Context.Proof); |
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
425 |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
426 |
fun check_text ctxt (Source src) = Source (check_src ctxt src) |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
427 |
| check_text _ (Basic m) = Basic m |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
428 |
| check_text ctxt (Combinator (x, y, body)) = Combinator (x, y, map (check_text ctxt) body); |
59914
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset
|
429 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset
|
430 |
|
30512 | 431 |
(* method setup *) |
432 |
||
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
433 |
fun method_syntax scan src ctxt : method = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
434 |
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
|
435 |
|
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset
|
436 |
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
|
437 |
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
|
438 |
|
58979
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
439 |
fun method_setup name source comment = |
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
440 |
ML_Lex.read_source false source |
59064 | 441 |
|> ML_Context.expression (Input.range_of source) "parser" |
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset
|
442 |
"(Proof.context -> Proof.method) context_parser" |
58979
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
443 |
("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ |
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset
|
444 |
" parser " ^ ML_Syntax.print_string comment ^ ")") |
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset
|
445 |
|> Context.proof_map; |
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
446 |
|
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset
|
447 |
|
58006 | 448 |
(* prepare methods *) |
449 |
||
450 |
fun method ctxt = |
|
58016 | 451 |
let val table = get_methods (Context.Proof ctxt) |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset
|
452 |
in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end; |
58006 | 453 |
|
59909 | 454 |
fun method_closure ctxt src = |
58006 | 455 |
let |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
456 |
val src' = map Token.init_assignable src; |
59909 | 457 |
val ctxt' = Context_Position.not_really ctxt; |
458 |
val _ = Seq.pull (method ctxt' src' ctxt' [] (Goal.protect 0 Drule.dummy_thm)); |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
459 |
in map Token.closure src' end; |
58006 | 460 |
|
59909 | 461 |
val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true))); |
462 |
||
463 |
fun method_cmd ctxt = |
|
464 |
check_src ctxt #> |
|
465 |
Config.get ctxt closure ? method_closure ctxt #> |
|
466 |
method ctxt; |
|
58006 | 467 |
|
468 |
||
60609 | 469 |
(* static vs. runtime state *) |
60553 | 470 |
|
471 |
fun detect_closure_state st = |
|
472 |
(case try Logic.dest_term (Thm.concl_of (perhaps (try Goal.conclude) st)) of |
|
473 |
NONE => false |
|
474 |
| SOME t => Term.is_dummy_pattern t); |
|
475 |
||
60609 | 476 |
fun STATIC test st = |
477 |
if detect_closure_state st then (test (); Seq.single ([], st)) else Seq.empty; |
|
478 |
||
60553 | 479 |
fun RUNTIME (tac: cases_tactic) st = |
480 |
if detect_closure_state st then Seq.empty else tac st; |
|
481 |
||
60554 | 482 |
fun sleep t = RUNTIME (fn st => (OS.Process.sleep t; Seq.single ([], st))); |
483 |
||
60553 | 484 |
|
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
485 |
(* evaluate method text *) |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
486 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
487 |
local |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
488 |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
489 |
fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) = |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
490 |
tac st |> Seq.map (fn (cases', st') => (cases @ cases', st')); |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
491 |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
492 |
fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) = |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
493 |
tac st |> Seq.map (pair cases); |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
494 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
495 |
val op THEN = Seq.THEN; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
496 |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
497 |
val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac); |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
498 |
|
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
499 |
fun RESTRICT_GOAL i n method = |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
500 |
BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
501 |
method THEN |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
502 |
BYPASS_CASES (PRIMITIVE (Goal.unrestrict i)); |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
503 |
|
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
504 |
fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method; |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
505 |
|
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
506 |
fun (method1 THEN_ALL_NEW method2) i (st: cases_state) = |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
507 |
st |> (method1 i THEN (fn st' => |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
508 |
Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st') - Thm.nprems_of (snd st)) st')); |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
509 |
|
58005 | 510 |
fun COMBINATOR1 comb [meth] = comb meth |
511 |
| COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; |
|
512 |
||
513 |
fun combinator Then = Seq.EVERY |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
514 |
| combinator Then_All_New = |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
515 |
(fn [] => Seq.single |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
516 |
| methods => |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
517 |
preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1) |
58005 | 518 |
| combinator Orelse = Seq.FIRST |
519 |
| combinator Try = COMBINATOR1 Seq.TRY |
|
520 |
| combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
521 |
| combinator (Select_Goals n) = |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset
|
522 |
COMBINATOR1 (fn method => preparation THEN RESTRICT_GOAL 1 n method); |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
523 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
524 |
in |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
525 |
|
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset
|
526 |
fun evaluate text ctxt = |
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
527 |
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
|
528 |
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
|
529 |
| eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt |
58005 | 530 |
| eval (Combinator (_, c, txts)) = |
531 |
let |
|
532 |
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
|
533 |
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
|
534 |
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
|
535 |
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
|
536 |
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
|
537 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
538 |
end; |
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
539 |
|
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset
|
540 |
|
5884 | 541 |
|
17110 | 542 |
(** concrete syntax **) |
5824 | 543 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
544 |
(* type modifier *) |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
545 |
|
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
546 |
type modifier = |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
547 |
{init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}; |
5824 | 548 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
549 |
fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos}; |
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
550 |
|
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
551 |
|
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
552 |
(* sections *) |
7268 | 553 |
|
59982
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
554 |
val old_section_parser = |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
555 |
Config.bool (Config.declare ("Method.old_section_parser", @{here}) (K (Config.Bool false))); |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
556 |
|
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
557 |
local |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
558 |
|
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
559 |
fun thms ss = |
61476 | 560 |
Scan.repeats (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm); |
59982
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
561 |
|
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
562 |
fun app {init, attribute, pos = _} ths context = |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
563 |
fold_map (Thm.apply_attribute attribute) ths (Context.map_proof init context); |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
564 |
|
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
565 |
fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
566 |
(fn (m, ths) => Scan.succeed (swap (app m ths context)))); |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
567 |
|
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
568 |
in |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
569 |
|
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
570 |
fun old_sections ss = Scan.repeat (section ss) >> K (); |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
571 |
|
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
572 |
end; |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
573 |
|
7268 | 574 |
local |
575 |
||
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset
|
576 |
fun sect (modifier : modifier parser) = Scan.depend (fn context => |
60211 | 577 |
Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.xthm) |
578 |
>> (fn ((tok0, ({init, attribute, pos}, modifier_toks)), xthms) => |
|
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset
|
579 |
let |
58068 | 580 |
val decl = |
60211 | 581 |
(case Token.get_value tok0 of |
58068 | 582 |
SOME (Token.Declaration decl) => decl |
583 |
| _ => |
|
584 |
let |
|
585 |
val ctxt = Context.proof_of context; |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
586 |
val prep_att = Attrib.check_src ctxt #> map (Token.assign NONE); |
58068 | 587 |
val thms = |
588 |
map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms; |
|
589 |
val facts = |
|
590 |
Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)] |
|
591 |
|> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs)); |
|
60211 | 592 |
|
58068 | 593 |
fun decl phi = |
594 |
Context.mapping I init #> |
|
595 |
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; |
|
60211 | 596 |
|
60212 | 597 |
val modifier_report = |
598 |
(Position.set_range (Token.range_of modifier_toks), |
|
599 |
Markup.properties (Position.def_properties_of pos) |
|
600 |
(Markup.entity Markup.method_modifierN "")); |
|
60211 | 601 |
val _ = |
60212 | 602 |
Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0); |
60211 | 603 |
val _ = Token.assign (SOME (Token.Declaration decl)) tok0; |
58068 | 604 |
in decl end); |
605 |
in (Morphism.form decl context, decl) end)); |
|
5824 | 606 |
|
30540 | 607 |
in |
608 |
||
59982
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
609 |
fun sections ss = |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
610 |
Args.context :|-- (fn ctxt => |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
611 |
if Config.get ctxt old_section_parser then old_sections ss |
f402fd001429
option for old section parser (before 2137e60b6f6d) for the sake of Eisbach;
wenzelm
parents:
59981
diff
changeset
|
612 |
else Scan.repeat (sect (Scan.first ss)) >> K ()); |
5824 | 613 |
|
7268 | 614 |
end; |
615 |
||
5824 | 616 |
|
30515 | 617 |
(* extra rule methods *) |
618 |
||
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset
|
619 |
fun xrule_meth meth = |
36950 | 620 |
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
|
621 |
(fn (n, ths) => fn ctxt => meth ctxt n ths); |
30515 | 622 |
|
623 |
||
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
624 |
(* text range *) |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
625 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
626 |
type text_range = text * Position.range; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
627 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
628 |
fun text NONE = NONE |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
629 |
| text (SOME (txt, _)) = SOME txt; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
630 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
631 |
fun position NONE = Position.none |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
632 |
| position (SOME (_, (pos, _))) = pos; |
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
633 |
|
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
634 |
|
55795 | 635 |
(* reports *) |
636 |
||
637 |
local |
|
638 |
||
639 |
fun keyword_positions (Source _) = [] |
|
640 |
| keyword_positions (Basic _) = [] |
|
58005 | 641 |
| keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = |
642 |
keywords @ maps keyword_positions texts; |
|
55795 | 643 |
|
644 |
in |
|
645 |
||
646 |
fun reports_of ((text, (pos, _)): text_range) = |
|
647 |
(pos, Markup.language_method) :: |
|
55917
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55828
diff
changeset
|
648 |
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
|
649 |
(keyword_positions text); |
55795 | 650 |
|
651 |
val report = Position.reports o reports_of; |
|
652 |
||
653 |
end; |
|
654 |
||
655 |
||
59666 | 656 |
(* parser *) |
657 |
||
658 |
local |
|
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
659 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
660 |
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
|
661 |
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
|
662 |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
663 |
in |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
664 |
|
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
665 |
fun parser pri = |
59666 | 666 |
let |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
667 |
val meth_name = Parse.token Parse.xname; |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
668 |
|
59666 | 669 |
fun meth5 x = |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
670 |
(meth_name >> (Source o single) || |
59666 | 671 |
Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
672 |
Source (Token.make_src ("cartouche", Position.none) [tok])) || |
59666 | 673 |
Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x |
674 |
and meth4 x = |
|
675 |
(meth5 -- Parse.position (Parse.$$$ "?") |
|
676 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || |
|
677 |
meth5 -- Parse.position (Parse.$$$ "+") |
|
678 |
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || |
|
59914
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset
|
679 |
meth5 -- (Parse.position (Parse.$$$ "[") -- |
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset
|
680 |
Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) |
59666 | 681 |
>> (fn (m, (((_, pos1), n), (_, pos2))) => |
682 |
Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || |
|
683 |
meth5) x |
|
684 |
and meth3 x = |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61812
diff
changeset
|
685 |
(meth_name ::: Parse.args1 is_symid_meth >> Source || |
59666 | 686 |
meth4) x |
687 |
and meth2 x = |
|
688 |
(Parse.enum1_positions "," meth3 |
|
689 |
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x |
|
690 |
and meth1 x = |
|
691 |
(Parse.enum1_positions ";" meth2 |
|
692 |
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x |
|
693 |
and meth0 x = |
|
694 |
(Parse.enum1_positions "|" meth1 |
|
695 |
>> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; |
|
59981 | 696 |
|
697 |
val meth = |
|
698 |
nth [meth0, meth1, meth2, meth3, meth4, meth5] pri |
|
699 |
handle General.Subscript => raise Fail ("Bad method parser priority " ^ string_of_int pri); |
|
700 |
in Scan.trace meth >> (fn (m, toks) => (m, Token.range_of toks)) end; |
|
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
701 |
|
59981 | 702 |
val parse = parser 4; |
49866 | 703 |
|
55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset
|
704 |
end; |
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
705 |
|
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset
|
706 |
|
18708 | 707 |
(* theory setup *) |
5824 | 708 |
|
53171 | 709 |
val _ = Theory.setup |
56204 | 710 |
(setup @{binding fail} (Scan.succeed (K fail)) "force failure" #> |
711 |
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #> |
|
60554 | 712 |
setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s))) |
713 |
"succeed after delay (in seconds)" #> |
|
56204 | 714 |
setup @{binding "-"} (Scan.succeed (K insert_facts)) |
60578 | 715 |
"insert current facts, nothing else" #> |
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61164
diff
changeset
|
716 |
setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt => |
61812 | 717 |
METHOD_CASES (fn _ => fn st => |
61164 | 718 |
let |
719 |
val _ = |
|
720 |
(case drop (Thm.nprems_of st) names of |
|
721 |
[] => () |
|
722 |
| bad => |
|
723 |
if detect_closure_state st then () |
|
724 |
else |
|
725 |
(* FIXME Seq.Error *) |
|
726 |
error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^ |
|
727 |
Position.here (Position.set_range (Token.range_of bad)))); |
|
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61164
diff
changeset
|
728 |
in goal_cases_tac ctxt (map Token.content_of names) st end))) |
61164 | 729 |
"bind cases for goals" #> |
56204 | 730 |
setup @{binding insert} (Attrib.thms >> (K o insert)) |
60578 | 731 |
"insert theorems, ignoring facts" #> |
58957 | 732 |
setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths)) |
30515 | 733 |
"repeatedly apply introduction rules" #> |
58957 | 734 |
setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths)) |
30515 | 735 |
"repeatedly apply elimination rules" #> |
56204 | 736 |
setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #> |
737 |
setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #> |
|
738 |
setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize) |
|
30515 | 739 |
"present local premises as object-level statements" #> |
56204 | 740 |
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
|
741 |
"apply some intro/elim rule" #> |
56204 | 742 |
setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #> |
743 |
setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #> |
|
744 |
setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #> |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset
|
745 |
setup @{binding this} (Scan.succeed this) "apply current facts as rules" #> |
56204 | 746 |
setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #> |
747 |
setup @{binding assumption} (Scan.succeed assumption) |
|
30515 | 748 |
"proof by assumption, preferring facts" #> |
56204 | 749 |
setup @{binding rename_tac} (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >> |
52732 | 750 |
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) |
30515 | 751 |
"rename parameters of goal" #> |
56204 | 752 |
setup @{binding rotate_tac} (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >> |
52732 | 753 |
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) |
30515 | 754 |
"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
|
755 |
setup @{binding tactic} (parse_tactic >> (K o METHOD)) |
30515 | 756 |
"ML tactic as proof method" #> |
59953 | 757 |
setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => EMPTY_CASES o tac)) |
53171 | 758 |
"ML tactic as raw proof method"); |
5824 | 759 |
|
760 |
||
16145 | 761 |
(*final declarations of this structure!*) |
762 |
val unfold = unfold_meth; |
|
763 |
val fold = fold_meth; |
|
764 |
||
5824 | 765 |
end; |
766 |
||
61834 | 767 |
structure Basic_Method: BASIC_METHOD = Method; |
768 |
open Basic_Method; |
|
769 |
||
30508
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
770 |
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
|
771 |
val METHOD = Method.METHOD; |
958cc116d03b
tuned Method exports: non-pervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset
|
772 |
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
|
773 |
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
|
774 |
val SIMPLE_METHOD'' = Method.SIMPLE_METHOD''; |