author  wenzelm 
Thu, 02 Apr 2015 20:28:30 +0200  
changeset 59914  d1ddcd8df4e4 
parent 59909  fbf4d5ad500d 
child 59917  9830c944670f 
permissions  rwrr 
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 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

26 
val this: Proof.context > method 
20289  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 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

35 
val intros_tac: Proof.context > thm list > thm list > tactic 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

36 
val try_intros_tac: Proof.context > thm list > thm list > tactic 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

37 
val rule: Proof.context > thm list > method 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

38 
val erule: Proof.context > int > thm list > method 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

39 
val drule: Proof.context > int > thm list > method 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

40 
val frule: Proof.context > int > thm list > method 
58018
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

41 
val set_tactic: (morphism > thm list > tactic) > Context.generic > Context.generic 
55765  42 
type combinator_info 
43 
val no_combinator_info: combinator_info 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

44 
datatype combinator = Then  Then_All_New  Orelse  Try  Repeat1  Select_Goals of int 
5824  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 
59907  59 
val check_src: Proof.context > Token.src > Token.src 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

60 
val method_syntax: (Proof.context > method) context_parser > 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

61 
Token.src > Proof.context > method 
30512  62 
val setup: binding > (Proof.context > method) context_parser > string > theory > theory 
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

63 
val local_setup: binding > (Proof.context > method) context_parser > string > 
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

64 
local_theory > local_theory 
59064  65 
val method_setup: bstring * Position.T > Input.source > string > local_theory > local_theory 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

66 
val method: Proof.context > Token.src > Proof.context > method 
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

67 
val method_closure: Proof.context > Token.src > Token.src 
59909  68 
val closure: bool Config.T 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

69 
val method_cmd: Proof.context > Token.src > Proof.context > method 
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset

70 
val evaluate: text > Proof.context > method 
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

71 
type modifier = {init: Proof.context > Proof.context, attribute: attribute, pos: Position.T} 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

72 
val modifier: attribute > Position.T > modifier 
58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset

73 
val section: modifier parser list > declaration context_parser 
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset

74 
val sections: modifier parser list > declaration list context_parser 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset

75 
type text_range = text * Position.range 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset

76 
val text: text_range option > text option 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49866
diff
changeset

77 
val position: text_range option > Position.T 
55795  78 
val reports_of: text_range > Position.report list 
79 
val report: text_range > unit 

55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

80 
val parse: text_range parser 
59666  81 
val parse_internal: Proof.context > text_range parser 
5824  82 
end; 
83 

84 
structure Method: METHOD = 

85 
struct 

86 

12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset

87 
(** proof methods **) 
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset

88 

58006  89 
(* method *) 
11731  90 

58002  91 
type method = thm list > cases_tactic; 
11731  92 

58030  93 
fun METHOD_CASES tac : method = fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts); 
94 
fun METHOD tac : method = fn facts => NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts); 

5824  95 

96 
val fail = METHOD (K no_tac); 

97 
val succeed = METHOD (K all_tac); 

98 

99 

17110  100 
(* insert facts *) 
7419  101 

102 
local 

5824  103 

21579  104 
fun cut_rule_tac rule = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

105 
resolve0_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl]; 
6981  106 

7419  107 
in 
5824  108 

51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset

109 
fun insert_tac [] _ = all_tac 
7419  110 
 insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); 
6981  111 

7555  112 
val insert_facts = METHOD (ALLGOALS o insert_tac); 
7664  113 
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); 
7419  114 

9706  115 
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); 
21592  116 
fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); 
117 
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL; 

9706  118 

12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset

119 
end; 
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset

120 

9706  121 

17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

122 
(* cheating *) 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

123 

52059  124 
fun cheating ctxt int = METHOD (fn _ => fn st => 
125 
if int orelse Config.get ctxt quick_and_dirty then 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

126 
ALLGOALS (Skip_Proof.cheat_tac ctxt) st 
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
51383
diff
changeset

127 
else error "Cheating requires quick_and_dirty mode!"); 
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

128 

09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

129 

17110  130 
(* unfold intro/elim rules *) 
131 

58957  132 
fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths)); 
133 
fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths)); 

17110  134 

135 

12384  136 
(* unfold/fold definitions *) 
137 

35624  138 
fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths)); 
139 
fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths)); 

6532  140 

12384  141 

12829  142 
(* atomize rule statements *) 
143 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

144 
fun atomize false ctxt = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

145 
SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt) 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

146 
 atomize true ctxt = 
58002  147 
NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)); 
12829  148 

149 

18039  150 
(* this  resolve facts directly *) 
12384  151 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

152 
fun this ctxt = METHOD (EVERY o map (HEADGOAL o resolve_tac ctxt o single)); 
9484  153 

154 

18039  155 
(* fact  composition by facts from context *) 
156 

42360  157 
fun fact [] ctxt = SIMPLE_METHOD' (Proof_Context.some_fact_tac ctxt) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

158 
 fact rules ctxt = SIMPLE_METHOD' (Proof_Context.fact_tac ctxt rules); 
18039  159 

160 

17110  161 
(* assumption *) 
7419  162 

163 
local 

164 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

165 
fun cond_rtac ctxt cond rule = SUBGOAL (fn (prop, i) => 
19778  166 
if cond (Logic.strip_assums_concl prop) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

167 
then resolve_tac ctxt [rule] i else no_tac); 
7419  168 

29857
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset

169 
in 
2cc976ed8a3c
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
kleing
parents:
29301
diff
changeset

170 

30234
7dd251bce291
renamed Method.assumption_tac back to Method.assm_tac  as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
wenzelm
parents:
30190
diff
changeset

171 
fun assm_tac ctxt = 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

172 
assume_tac ctxt APPEND' 
23349  173 
Goal.assume_rule_tac ctxt APPEND' 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

174 
cond_rtac ctxt (can Logic.dest_equals) Drule.reflexive_thm APPEND' 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

175 
cond_rtac ctxt (can Logic.dest_term) Drule.termI; 
17110  176 

49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

177 
fun all_assm_tac ctxt = 
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

178 
let 
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

179 
fun tac i st = 
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

180 
if i > Thm.nprems_of st then all_tac st 
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

181 
else ((assm_tac ctxt i THEN tac i) ORELSE tac (i + 1)) st; 
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

182 
in tac 1 end; 
30567
cd8e20f86795
close/all_assm_tac: finish all subgoals from left to right (cf. Proof.goal_tac a28d83e903ce)  NB: ALLGOALS/THEN_ALL_NEW operate from right to left;
wenzelm
parents:
30544
diff
changeset

183 

23349  184 
fun assumption ctxt = METHOD (HEADGOAL o 
30234
7dd251bce291
renamed Method.assumption_tac back to Method.assm_tac  as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
wenzelm
parents:
30190
diff
changeset

185 
(fn [] => assm_tac ctxt 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

186 
 [fact] => solve_tac ctxt [fact] 
23349  187 
 _ => K no_tac)); 
188 

49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

189 
fun finish immed ctxt = 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset

190 
METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt)); 
7419  191 

192 
end; 

193 

194 

17110  195 
(* rule etc.  singlestep refinements *) 
12347  196 

56204  197 
val rule_trace = Attrib.setup_config_bool @{binding rule_trace} (fn _ => false); 
12347  198 

17110  199 
fun trace ctxt rules = 
41379  200 
if Config.get ctxt rule_trace andalso not (null rules) then 
51584  201 
Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules) 
21962  202 
> Pretty.string_of > tracing 
203 
else (); 

12347  204 

205 
local 

206 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

207 
fun gen_rule_tac tac ctxt rules facts = 
18841  208 
(fn i => fn st => 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

209 
if null facts then tac ctxt rules i st 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset

210 
else 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

211 
Seq.maps (fn rule => (tac ctxt o single) rule i st) 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58837
diff
changeset

212 
(Drule.multi_resolves (SOME ctxt) facts rules)) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

213 
THEN_ALL_NEW Goal.norm_hhf_tac ctxt; 
7130  214 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

215 
fun gen_arule_tac tac ctxt j rules facts = 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

216 
EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt)); 
10744  217 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

218 
fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) => 
11785  219 
let 
220 
val rules = 

221 
if not (null arg_rules) then arg_rules 

33369  222 
else flat (Context_Rules.find_rules false facts goal ctxt) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

223 
in trace ctxt rules; tac ctxt rules facts i end); 
10309  224 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

225 
fun meth tac x y = METHOD (HEADGOAL o tac x y); 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

226 
fun meth' tac x y z = METHOD (HEADGOAL o tac x y z); 
8220  227 

7419  228 
in 
229 

52732  230 
val rule_tac = gen_rule_tac resolve_tac; 
10744  231 
val rule = meth rule_tac; 
232 
val some_rule_tac = gen_some_rule_tac rule_tac; 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

233 
val some_rule = meth some_rule_tac; 
10744  234 

52732  235 
val erule = meth' (gen_arule_tac eresolve_tac); 
236 
val drule = meth' (gen_arule_tac dresolve_tac); 

237 
val frule = meth' (gen_arule_tac forward_tac); 

5824  238 

7419  239 
end; 
240 

241 

25270  242 
(* intros_tac  pervasive search spanned by intro rules *) 
243 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

244 
fun gen_intros_tac goals ctxt intros facts = 
36093
0880493627ca
Graceful treatment of nonlocale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset

245 
goals (insert_tac facts THEN' 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

246 
REPEAT_ALL_NEW (resolve_tac ctxt intros)) 
25270  247 
THEN Tactic.distinct_subgoals_tac; 
248 

36093
0880493627ca
Graceful treatment of nonlocale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset

249 
val intros_tac = gen_intros_tac ALLGOALS; 
0880493627ca
Graceful treatment of nonlocale subgoals by methods unfold_locales and intro_locales.
ballarin
parents:
33522
diff
changeset

250 
val try_intros_tac = gen_intros_tac TRYALL; 
25270  251 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

252 

58016  253 

254 
(** method syntax **) 

255 

256 
(* context data *) 

8351  257 

58016  258 
structure Data = Generic_Data 
26472
9afdd61cf528
ml_tactic: noncritical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset

259 
( 
58016  260 
type T = 
261 
((Token.src > Proof.context > method) * string) Name_Space.table * (*methods*) 

58018
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

262 
(morphism > thm list > tactic) option; (*ML tactic*) 
58016  263 
val empty : T = (Name_Space.empty_table "method", NONE); 
264 
val extend = I; 

265 
fun merge ((tab, tac), (tab', tac')) : T = 

266 
(Name_Space.merge_tables (tab, tab'), merge_options (tac, tac')); 

26472
9afdd61cf528
ml_tactic: noncritical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset

267 
); 
9afdd61cf528
ml_tactic: noncritical version via proof data and thread data;
wenzelm
parents:
26463
diff
changeset

268 

58016  269 
val get_methods = fst o Data.get; 
270 
val map_methods = Data.map o apfst; 

271 

272 

273 
(* ML tactic *) 

274 

275 
val set_tactic = Data.map o apsnd o K o SOME; 

276 

277 
fun the_tactic context = 

278 
(case snd (Data.get context) of 

279 
SOME tac => tac 

280 
 NONE => raise Fail "Undefined ML tactic"); 

8351  281 

58018
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

282 
val parse_tactic = 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

283 
Scan.state : (fn context => 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

284 
Scan.lift (Args.text_declaration (fn source => 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

285 
let 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

286 
val context' = context > 
59064  287 
ML_Context.expression (Input.range_of source) 
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset

288 
"tactic" "Morphism.morphism > thm list > tactic" 
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset

289 
"Method.set_tactic tactic" 
59067  290 
(ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @ 
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset

291 
ML_Lex.read_source false source); 
58018
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

292 
val tac = the_tactic context'; 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

293 
in 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

294 
fn phi => 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

295 
set_tactic (fn _ => Context.setmp_thread_data (SOME context) (tac phi)) 
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

296 
end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context)))); 
8351  297 

298 

17110  299 
(* method text *) 
300 

55765  301 
datatype combinator_info = Combinator_Info of {keywords: Position.T list}; 
302 
fun combinator_info keywords = Combinator_Info {keywords = keywords}; 

303 
val no_combinator_info = combinator_info []; 

304 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

305 
datatype combinator = Then  Then_All_New  Orelse  Try  Repeat1  Select_Goals of int; 
58005  306 

17110  307 
datatype text = 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

308 
Source of Token.src  
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset

309 
Basic of Proof.context > method  
58005  310 
Combinator of combinator_info * combinator * text list; 
55765  311 

58006  312 
fun map_source f (Source src) = Source (f src) 
313 
 map_source _ (Basic meth) = Basic meth 

314 
 map_source f (Combinator (info, comb, txts)) = Combinator (info, comb, map (map_source f) txts); 

315 

54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset

316 
fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r); 
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset

317 
val succeed_text = Basic (K succeed); 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

318 
val default_text = Source (Token.src ("default", Position.none) []); 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

319 
val this_text = Basic this; 
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32091
diff
changeset

320 
val done_text = Basic (K (SIMPLE_METHOD all_tac)); 
52059  321 
fun sorry_text int = Basic (fn ctxt => cheating ctxt int); 
17110  322 

49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
48992
diff
changeset

323 
fun finish_text (NONE, immed) = Basic (finish immed) 
58005  324 
 finish_text (SOME txt, immed) = 
325 
Combinator (no_combinator_info, Then, [txt, Basic (finish immed)]); 

17110  326 

327 

328 
(* method definitions *) 

5824  329 

57937  330 
fun transfer_methods ctxt = 
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

331 
let 
58016  332 
val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt)); 
333 
val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt)); 

334 
in Context.proof_map (map_methods (K meths')) ctxt end; 

55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset

335 

a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset

336 
fun print_methods ctxt = 
22846  337 
let 
58016  338 
val meths = get_methods (Context.Proof ctxt); 
50301  339 
fun prt_meth (name, (_, "")) = Pretty.mark_str name 
42813
6c841fa92fa2
optional description for 'attribute_setup' and 'method_setup';
wenzelm
parents:
42616
diff
changeset

340 
 prt_meth (name, (_, comment)) = 
50301  341 
Pretty.block 
342 
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); 

22846  343 
in 
56052  344 
[Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))] 
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56278
diff
changeset

345 
> Pretty.writeln_chunks 
22846  346 
end; 
7611  347 

57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

348 

c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

349 
(* define *) 
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

350 

c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

351 
fun define_global binding meth comment thy = 
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

352 
let 
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

353 
val context = Context.Theory thy; 
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

354 
val (name, meths') = 
58016  355 
Name_Space.define context true (binding, (meth, comment)) (get_methods context); 
356 
in (name, Context.the_theory (map_methods (K meths') context)) end; 

57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

357 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset

358 
fun define binding meth comment = 
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset

359 
Local_Theory.background_theory_result (define_global binding meth comment) 
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset

360 
#> (fn name => 
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset

361 
Local_Theory.map_contexts (K transfer_methods) 
58016  362 
#> Local_Theory.generic_alias map_methods binding name 
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset

363 
#> pair name); 
31304  364 

55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset

365 

9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset

366 
(* check *) 
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset

367 

58016  368 
fun check_name ctxt = 
369 
let val context = Context.Proof ctxt 

370 
in #1 o Name_Space.check context (get_methods context) end; 

371 

59907  372 
fun check_src ctxt = 
373 
#1 o Token.check_src ctxt (get_methods (Context.Proof ctxt)); 

55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset

374 

59914
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset

375 
fun checked_info ctxt name = 
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset

376 
let val space = Name_Space.space_of_table (get_methods (Context.Proof ctxt)) 
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset

377 
in (Name_Space.kind_of space, Name_Space.markup space name) end; 
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset

378 

55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55917
diff
changeset

379 

30512  380 
(* method setup *) 
381 

57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

382 
fun method_syntax scan src ctxt : method = 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

383 
let val (m, ctxt') = Token.syntax scan src ctxt in m ctxt' end; 
57935
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

384 

c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

385 
fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd; 
c578f3a37a67
localized method definitions (see also f14c1248d064);
wenzelm
parents:
57863
diff
changeset

386 
fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd; 
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

387 

58979
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset

388 
fun method_setup name source comment = 
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset

389 
ML_Lex.read_source false source 
59064  390 
> ML_Context.expression (Input.range_of source) "parser" 
58991
92b6f4e68c5a
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58979
diff
changeset

391 
"(Proof.context > Proof.method) context_parser" 
58979
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset

392 
("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^ 
162a4c2e97bc
more careful ML source positions, for improved PIDE markup;
wenzelm
parents:
58978
diff
changeset

393 
" parser " ^ ML_Syntax.print_string comment ^ ")") 
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57938
diff
changeset

394 
> Context.proof_map; 
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

395 

09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

396 

58006  397 
(* prepare methods *) 
398 

399 
fun method ctxt = 

58016  400 
let val table = get_methods (Context.Proof ctxt) 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

401 
in fn src => #1 (Name_Space.get table (#1 (Token.name_of_src src))) src end; 
58006  402 

59909  403 
fun method_closure ctxt src = 
58006  404 
let 
59909  405 
val src' = Token.init_assignable_src src; 
406 
val ctxt' = Context_Position.not_really ctxt; 

407 
val _ = Seq.pull (method ctxt' src' ctxt' [] (Goal.protect 0 Drule.dummy_thm)); 

408 
in Token.closure_src src' end; 

58006  409 

59909  410 
val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true))); 
411 

412 
fun method_cmd ctxt = 

413 
check_src ctxt #> 

414 
Config.get ctxt closure ? method_closure ctxt #> 

415 
method ctxt; 

58006  416 

417 

58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

418 
(* evaluate method text *) 
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

419 

250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

420 
local 
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

421 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

422 
fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) = 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

423 
tac st > Seq.map (fn (cases', st') => (cases @ cases', st')); 
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

424 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

425 
fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) = 
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

426 
tac st > Seq.map (pair cases); 
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

427 

250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

428 
val op THEN = Seq.THEN; 
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

429 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

430 
val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac); 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

431 

49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

432 
fun RESTRICT_GOAL i n method = 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

433 
BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

434 
method THEN 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

435 
BYPASS_CASES (PRIMITIVE (Goal.unrestrict i)); 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

436 

49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

437 
fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method; 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

438 

49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

439 
fun (method1 THEN_ALL_NEW method2) i (st: cases_state) = 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

440 
st > (method1 i THEN (fn st' => 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

441 
Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st')  Thm.nprems_of (snd st)) st')); 
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

442 

58005  443 
fun COMBINATOR1 comb [meth] = comb meth 
444 
 COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument"; 

445 

446 
fun combinator Then = Seq.EVERY 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

447 
 combinator Then_All_New = 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

448 
(fn [] => Seq.single 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

449 
 methods => 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

450 
preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1) 
58005  451 
 combinator Orelse = Seq.FIRST 
452 
 combinator Try = COMBINATOR1 Seq.TRY 

453 
 combinator Repeat1 = COMBINATOR1 Seq.REPEAT1 

59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

454 
 combinator (Select_Goals n) = 
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
59498
diff
changeset

455 
COMBINATOR1 (fn method => preparation THEN RESTRICT_GOAL 1 n method); 
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

456 

250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

457 
in 
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

458 

58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset

459 
fun evaluate text ctxt = 
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

460 
let 
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset

461 
fun eval (Basic meth) = APPEND_CASES o meth ctxt 
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset

462 
 eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt 
58005  463 
 eval (Combinator (_, c, txts)) = 
464 
let 

465 
val comb = combinator c; 

58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset

466 
val meths = map eval txts; 
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset

467 
in fn facts => comb (map (fn meth => meth facts) meths) end; 
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

468 
val meth = eval text; 
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58006
diff
changeset

469 
in fn facts => fn st => meth facts ([], st) end; 
58003
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

470 

250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

471 
end; 
250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

472 

250ecd2502ad
clarifed Method.evaluate: turn text into semantic method (like Basic);
wenzelm
parents:
58002
diff
changeset

473 

5884  474 

17110  475 
(** concrete syntax **) 
5824  476 

58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

477 
(* type modifier *) 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

478 

aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

479 
type modifier = 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

480 
{init: Proof.context > Proof.context, attribute: attribute, pos: Position.T}; 
5824  481 

58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

482 
fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos}; 
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

483 

aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

484 

aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

485 
(* sections *) 
7268  486 

487 
local 

488 

58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58034
diff
changeset

489 
fun sect (modifier : modifier parser) = Scan.depend (fn context => 
58068  490 
Scan.ahead Parse.not_eof  modifier  Scan.repeat (Scan.unless modifier Parse.xthm) >> 
491 
(fn ((tok, {init, attribute, pos}), xthms) => 

58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset

492 
let 
58068  493 
val decl = 
494 
(case Token.get_value tok of 

495 
SOME (Token.Declaration decl) => decl 

496 
 _ => 

497 
let 

498 
val ctxt = Context.proof_of context; 

499 
fun prep_att src = 

500 
let 

501 
val src' = Attrib.check_src ctxt src; 

502 
val _ = List.app (Token.assign NONE) (Token.args_of_src src'); 

503 
in src' end; 

504 
val thms = 

505 
map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms; 

506 
val facts = 

507 
Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)] 

508 
> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs)); 

509 
val _ = 

510 
Context_Position.report ctxt (Token.pos_of tok) 

511 
(Markup.entity Markup.method_modifierN "" 

512 
> Markup.properties (Position.def_properties_of pos)); 

513 
fun decl phi = 

514 
Context.mapping I init #> 

515 
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd; 

516 
val _ = Token.assign (SOME (Token.Declaration decl)) tok; 

517 
in decl end); 

518 
in (Morphism.form decl context, decl) end)); 

5824  519 

30540  520 
in 
521 

58029
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset

522 
val section = sect o Scan.first; 
2137e60b6f6d
clarified Method.section: explicit declaration with static closure;
wenzelm
parents:
58026
diff
changeset

523 
val sections = Scan.repeat o section; 
5824  524 

7268  525 
end; 
526 

5824  527 

30515  528 
(* extra rule methods *) 
529 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

530 
fun xrule_meth meth = 
36950  531 
Scan.lift (Scan.optional (Args.parens Parse.nat) 0)  Attrib.thms >> 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

532 
(fn (n, ths) => fn ctxt => meth ctxt n ths); 
30515  533 

534 

55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

535 
(* text range *) 
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

536 

213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

537 
type text_range = text * Position.range; 
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

538 

213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

539 
fun text NONE = NONE 
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

540 
 text (SOME (txt, _)) = SOME txt; 
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

541 

213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

542 
fun position NONE = Position.none 
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

543 
 position (SOME (_, (pos, _))) = pos; 
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

544 

213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

545 

55795  546 
(* reports *) 
547 

548 
local 

549 

550 
fun keyword_positions (Source _) = [] 

551 
 keyword_positions (Basic _) = [] 

58005  552 
 keyword_positions (Combinator (Combinator_Info {keywords}, _, texts)) = 
553 
keywords @ maps keyword_positions texts; 

55795  554 

555 
in 

556 

557 
fun reports_of ((text, (pos, _)): text_range) = 

558 
(pos, Markup.language_method) :: 

55917
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55828
diff
changeset

559 
maps (fn p => map (pair p) (Markup.keyword3 :: Completion.suppress_abbrevs "")) 
5438ed05e1c9
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents:
55828
diff
changeset

560 
(keyword_positions text); 
55795  561 

562 
val report = Position.reports o reports_of; 

563 

564 
end; 

565 

566 

59666  567 
(* parser *) 
568 

569 
local 

27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset

570 

96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset

571 
fun is_symid_meth s = 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset

572 
s <> "" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s; 
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset

573 

59666  574 
fun parser check_ctxt low_pri = 
575 
let 

576 
val (meth_name, mk_src) = 

577 
(case check_ctxt of 

578 
NONE => (Parse.xname, Token.src) 

579 
 SOME ctxt => 

580 
(Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)), 

59914
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset

581 
fn (name, pos) => fn args => Token.src_checked (name, pos) args (checked_info ctxt name))); 
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset

582 

59666  583 
fun meth5 x = 
584 
(Parse.position meth_name >> (fn name => Source (mk_src name []))  

585 
Scan.ahead Parse.cartouche  Parse.not_eof >> (fn tok => 

586 
Source (mk_src ("cartouche", Token.pos_of tok) [tok]))  

587 
Parse.$$$ "("  Parse.!!! (meth0  Parse.$$$ ")")) x 

588 
and meth4 x = 

589 
(meth5  Parse.position (Parse.$$$ "?") 

590 
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m]))  

591 
meth5  Parse.position (Parse.$$$ "+") 

592 
>> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m]))  

59914
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset

593 
meth5  (Parse.position (Parse.$$$ "[")  
d1ddcd8df4e4
proper treatment of internal method name as already checked Token.src;
wenzelm
parents:
59909
diff
changeset

594 
Scan.optional Parse.nat 1  Parse.position (Parse.$$$ "]")) 
59666  595 
>> (fn (m, (((_, pos1), n), (_, pos2))) => 
596 
Combinator (combinator_info [pos1, pos2], Select_Goals n, [m]))  

597 
meth5) x 

598 
and meth3 x = 

599 
(Parse.position meth_name  Parse.args1 is_symid_meth >> (Source o uncurry mk_src)  

600 
meth4) x 

601 
and meth2 x = 

602 
(Parse.enum1_positions "," meth3 

603 
>> (fn ([m], _) => m  (ms, ps) => Combinator (combinator_info ps, Then, ms))) x 

604 
and meth1 x = 

605 
(Parse.enum1_positions ";" meth2 

606 
>> (fn ([m], _) => m  (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x 

607 
and meth0 x = 

608 
(Parse.enum1_positions "" meth1 

609 
>> (fn ([m], _) => m  (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; 

610 
in 

611 
Scan.trace (if low_pri then meth0 else meth4) 

612 
>> (fn (m, toks) => (m, Token.range_of toks)) 

613 
end; 

27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset

614 

49866  615 
in 
616 

59666  617 
val parse = parser NONE false; 
618 
fun parse_internal ctxt = parser (SOME ctxt) true; 

49866  619 

55761
213b9811f59f
method language markup, e.g. relevant to prevent outer keyword completion;
wenzelm
parents:
55742
diff
changeset

620 
end; 
27813
96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset

621 

96fbe385a0d0
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27751
diff
changeset

622 

18708  623 
(* theory setup *) 
5824  624 

53171  625 
val _ = Theory.setup 
56204  626 
(setup @{binding fail} (Scan.succeed (K fail)) "force failure" #> 
627 
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #> 

628 
setup @{binding ""} (Scan.succeed (K insert_facts)) 

30515  629 
"do nothing (insert current facts only)" #> 
56204  630 
setup @{binding insert} (Attrib.thms >> (K o insert)) 
30515  631 
"insert theorems, ignoring facts (improper)" #> 
58957  632 
setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths)) 
30515  633 
"repeatedly apply introduction rules" #> 
58957  634 
setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths)) 
30515  635 
"repeatedly apply elimination rules" #> 
56204  636 
setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #> 
637 
setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #> 

638 
setup @{binding atomize} (Scan.lift (Args.mode "full") >> atomize) 

30515  639 
"present local premises as objectlevel statements" #> 
56204  640 
setup @{binding rule} (Attrib.thms >> (fn ths => fn ctxt => some_rule ctxt ths)) 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53171
diff
changeset

641 
"apply some intro/elim rule" #> 
56204  642 
setup @{binding erule} (xrule_meth erule) "apply rule in elimination manner (improper)" #> 
643 
setup @{binding drule} (xrule_meth drule) "apply rule in destruct manner (improper)" #> 

644 
setup @{binding frule} (xrule_meth frule) "apply rule in forward manner (improper)" #> 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59067
diff
changeset

645 
setup @{binding this} (Scan.succeed this) "apply current facts as rules" #> 
56204  646 
setup @{binding fact} (Attrib.thms >> fact) "composition by facts from context" #> 
647 
setup @{binding assumption} (Scan.succeed assumption) 

30515  648 
"proof by assumption, preferring facts" #> 
56204  649 
setup @{binding rename_tac} (Args.goal_spec  Scan.lift (Scan.repeat1 Args.name) >> 
52732  650 
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (rename_tac xs)))) 
30515  651 
"rename parameters of goal" #> 
56204  652 
setup @{binding rotate_tac} (Args.goal_spec  Scan.lift (Scan.optional Parse.int 1) >> 
52732  653 
(fn (quant, i) => K (SIMPLE_METHOD'' quant (rotate_tac i)))) 
30515  654 
"rotate assumptions of goal" #> 
58018
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

655 
setup @{binding tactic} (parse_tactic >> (K o METHOD)) 
30515  656 
"ML tactic as proof method" #> 
58018
beb4b7c0bb30
proper static closure of ML tactic  data slot is used twice, for ML compiler and transformed declaration;
wenzelm
parents:
58016
diff
changeset

657 
setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => NO_CASES o tac)) 
53171  658 
"ML tactic as raw proof method"); 
5824  659 

660 

16145  661 
(*final declarations of this structure!*) 
662 
val unfold = unfold_meth; 

663 
val fold = fold_meth; 

664 

5824  665 
end; 
666 

30508
958cc116d03b
tuned Method exports: nonpervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset

667 
val METHOD_CASES = Method.METHOD_CASES; 
958cc116d03b
tuned Method exports: nonpervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset

668 
val METHOD = Method.METHOD; 
958cc116d03b
tuned Method exports: nonpervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset

669 
val SIMPLE_METHOD = Method.SIMPLE_METHOD; 
958cc116d03b
tuned Method exports: nonpervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset

670 
val SIMPLE_METHOD' = Method.SIMPLE_METHOD'; 
958cc116d03b
tuned Method exports: nonpervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset

671 
val SIMPLE_METHOD'' = Method.SIMPLE_METHOD''; 
958cc116d03b
tuned Method exports: nonpervasive type method (cf. Proof.method), pervasive METHOD combinators;
wenzelm
parents:
30466
diff
changeset

672 