author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18708  4b3dadb4fe33 
child 18824  126049347167 
permissions  rwrr 
5824  1 
(* Title: Pure/Isar/method.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

17110  5 
Isar proof methods. 
5824  6 
*) 
7 

8 
signature BASIC_METHOD = 

9 
sig 

17110  10 
val FINDGOAL: (int > thm > 'a Seq.seq) > thm > 'a Seq.seq 
11 
val HEADGOAL: (int > thm > 'a Seq.seq) > thm > 'a Seq.seq 

12 
type method 

11731  13 
val trace_rules: bool ref 
5824  14 
val print_methods: theory > unit 
17110  15 
val Method: bstring > (Args.src > ProofContext.context > method) > string > unit 
5824  16 
end; 
17 

18 
signature METHOD = 

19 
sig 

20 
include BASIC_METHOD 

18227  21 
val apply: method > thm list > cases_tactic 
22 
val RAW_METHOD_CASES: (thm list > cases_tactic) > method 

17110  23 
val RAW_METHOD: (thm list > tactic) > method 
18227  24 
val METHOD_CASES: (thm list > cases_tactic) > method 
17110  25 
val METHOD: (thm list > tactic) > method 
26 
val fail: method 

27 
val succeed: method 

28 
val insert_tac: thm list > int > tactic 

29 
val insert: thm list > method 

30 
val insert_facts: method 

31 
val SIMPLE_METHOD: tactic > method 

32 
val SIMPLE_METHOD': ((int > tactic) > tactic) > (int > tactic) > method 

33 
val defer: int option > method 

34 
val prefer: int > method 

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

35 
val cheating: bool > ProofContext.context > method 
17110  36 
val intro: thm list > method 
37 
val elim: thm list > method 

38 
val unfold: thm list > method 

39 
val fold: thm list > method 

40 
val atomize: bool > method 

41 
val this: method 

18039  42 
val fact: thm list > ProofContext.context > method 
17110  43 
val assumption: ProofContext.context > method 
44 
val close: bool > ProofContext.context > method 

45 
val trace: ProofContext.context > thm list > unit 

6091  46 
val rule_tac: thm list > thm list > int > tactic 
17110  47 
val some_rule_tac: thm list > ProofContext.context > thm list > int > tactic 
48 
val rule: thm list > method 

49 
val erule: int > thm list > method 

50 
val drule: int > thm list > method 

51 
val frule: int > thm list > method 

17587  52 
val iprover_tac: ProofContext.context > int option > int > tactic 
17110  53 
val bires_inst_tac: bool > ProofContext.context > (indexname * string) list > 
54 
thm > int > tactic 

55 
val set_tactic: (ProofContext.context > thm list > tactic) > unit 

56 
val tactic: string > ProofContext.context > method 

57 
type src 

5824  58 
datatype text = 
17110  59 
Basic of (ProofContext.context > method)  
15703  60 
Source of src  
5824  61 
Then of text list  
62 
Orelse of text list  

63 
Try of text  

64 
Repeat1 of text 

17857  65 
val primitive_text: (thm > thm) > text 
66 
val succeed_text: text 

17110  67 
val default_text: text 
68 
val this_text: text 

69 
val done_text: text 

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

70 
val sorry_text: bool > text 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

71 
val finish_text: text option * bool > text 
17110  72 
exception METHOD_FAIL of (string * Position.T) * exn 
73 
val method: theory > src > ProofContext.context > method 

74 
val add_methods: (bstring * (src > ProofContext.context > method) * string) list 

75 
> theory > theory 

76 
val add_method: bstring * (src > ProofContext.context > method) * string 

77 
> theory > theory 

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

78 
val method_setup: bstring * string * string > theory > theory 
17110  79 
val syntax: (ProofContext.context * Args.T list > 'a * (ProofContext.context * Args.T list)) 
80 
> src > ProofContext.context > ProofContext.context * 'a 

81 
val simple_args: (Args.T list > 'a * Args.T list) 

82 
> ('a > ProofContext.context > method) > src > ProofContext.context > method 

83 
val ctxt_args: (ProofContext.context > method) > src > ProofContext.context > method 

84 
val no_args: method > src > ProofContext.context > method 

85 
type modifier 

86 
val sectioned_args: (ProofContext.context * Args.T list > 

87 
'a * (ProofContext.context * Args.T list)) > 

88 
(Args.T list > modifier * Args.T list) list > 

89 
('a > ProofContext.context > 'b) > src > ProofContext.context > 'b 

90 
val bang_sectioned_args: 

91 
(Args.T list > modifier * Args.T list) list > 

92 
(thm list > ProofContext.context > 'a) > src > ProofContext.context > 'a 

93 
val bang_sectioned_args': 

94 
(Args.T list > modifier * Args.T list) list > 

95 
(ProofContext.context * Args.T list > 'a * (ProofContext.context * Args.T list)) > 

96 
('a > thm list > ProofContext.context > 'b) > src > ProofContext.context > 'b 

97 
val only_sectioned_args: 

98 
(Args.T list > modifier * Args.T list) list > 

99 
(ProofContext.context > 'a) > src > ProofContext.context > 'a 

100 
val thms_ctxt_args: (thm list > ProofContext.context > 'a) > src > 

101 
ProofContext.context > 'a 

102 
val thms_args: (thm list > 'a) > src > ProofContext.context > 'a 

103 
val thm_args: (thm > 'a) > src > ProofContext.context > 'a 

9539  104 
val goal_args: (Args.T list > 'a * Args.T list) > ('a > int > tactic) 
17110  105 
> src > ProofContext.context > method 
106 
val goal_args': (ProofContext.context * Args.T list > 

107 
'a * (ProofContext.context * Args.T list)) 

108 
> ('a > int > tactic) > src > ProofContext.context > method 

109 
val goal_args_ctxt: (Args.T list > 'a * Args.T list) > 

110 
(ProofContext.context > 'a > int > tactic) > src > ProofContext.context > method 

111 
val goal_args_ctxt': (ProofContext.context * Args.T list > 

112 
'a * (ProofContext.context * Args.T list)) > 

113 
(ProofContext.context > 'a > int > tactic) > src > ProofContext.context > method 

5824  114 
end; 
115 

116 
structure Method: METHOD = 

117 
struct 

118 

17110  119 
(** generic tools **) 
120 

121 
(* goal addressing *) 

122 

123 
fun FINDGOAL tac st = 

124 
let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n) 

125 
in find 1 (Thm.nprems_of st) st end; 

126 

127 
fun HEADGOAL tac = tac 1; 

128 

129 

5824  130 

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

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

132 

17110  133 
(* datatype method *) 
11731  134 

18227  135 
datatype method = Meth of thm list > cases_tactic; 
11731  136 

17756  137 
fun apply (Meth m) = m; 
11731  138 

17756  139 
val RAW_METHOD_CASES = Meth; 
11731  140 

17110  141 
fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac); 
12144  142 

17110  143 
fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts => 
18474  144 
Seq.THEN (ALLGOALS Tactic.conjunction_tac, tac facts)); 
8372  145 

18474  146 
fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Tactic.conjunction_tac THEN tac facts); 
5824  147 

148 
val fail = METHOD (K no_tac); 

149 
val succeed = METHOD (K all_tac); 

150 

151 

17110  152 
(* insert facts *) 
7419  153 

154 
local 

5824  155 

6981  156 
fun cut_rule_tac raw_rule = 
157 
let 

158 
val rule = Drule.forall_intr_vars raw_rule; 

18039  159 
val revcut_rl = Drule.incr_indexes rule Drule.revcut_rl; 
7555  160 
in Tactic.rtac (rule COMP revcut_rl) end; 
6981  161 

7419  162 
in 
5824  163 

7419  164 
fun insert_tac [] i = all_tac 
165 
 insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts); 

6981  166 

7555  167 
val insert_facts = METHOD (ALLGOALS o insert_tac); 
7664  168 
fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms)); 
7419  169 

9706  170 
fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac); 
171 
fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac)); 

172 

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

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

174 

9706  175 

17110  176 
(* shuffle subgoals *) 
177 

178 
fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1))); 

179 
fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1))); 

180 

181 

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

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

183 

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

184 
fun cheating int ctxt = METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty) 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

185 
(SkipProof.cheat_tac (ProofContext.theory_of ctxt)))); 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

186 

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

187 

17110  188 
(* unfold intro/elim rules *) 
189 

190 
fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths)); 

191 
fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths)); 

192 

193 

12384  194 
(* unfold/fold definitions *) 
195 

16145  196 
fun unfold_meth ths = SIMPLE_METHOD (CHANGED_PROP (rewrite_goals_tac ths)); 
197 
fun fold_meth ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths)); 

6532  198 

12384  199 

12829  200 
(* atomize rule statements *) 
201 

202 
fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac) 

203 
 atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac))); 

204 

205 

18039  206 
(* this  resolve facts directly *) 
12384  207 

17110  208 
val this = METHOD (EVERY o map (HEADGOAL o Tactic.rtac)); 
9484  209 

210 

18039  211 
(* fact  composition by facts from context *) 
212 

18309  213 
fun fact [] ctxt = SIMPLE_METHOD' HEADGOAL (ProofContext.some_fact_tac ctxt) 
214 
 fact rules _ = SIMPLE_METHOD' HEADGOAL (ProofContext.fact_tac rules); 

18039  215 

216 

17110  217 
(* assumption *) 
7419  218 

219 
local 

220 

17110  221 
fun asm_tac ths = 
222 
foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths); 

223 

224 
val refl_tac = SUBGOAL (fn (prop, i) => 

225 
if can Logic.dest_equals (Logic.strip_assums_concl prop) 

226 
then Tactic.rtac Drule.reflexive_thm i else no_tac); 

7419  227 

17110  228 
fun assm_tac ctxt = 
229 
assume_tac APPEND' 

230 
asm_tac (ProofContext.prems_of ctxt) APPEND' 

231 
refl_tac; 

232 

233 
fun assumption_tac ctxt [] = assm_tac ctxt 

234 
 assumption_tac _ [fact] = asm_tac [fact] 

235 
 assumption_tac _ _ = K no_tac; 

7419  236 

237 
in 

238 

17110  239 
fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt); 
17356
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

240 
fun close immed ctxt = METHOD (K 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

241 
(FILTER Thm.no_prems ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac))); 
7419  242 

243 
end; 

244 

245 

17110  246 
(* rule etc.  singlestep refinements *) 
12347  247 

17110  248 
val trace_rules = ref false; 
12347  249 

17110  250 
fun trace ctxt rules = 
251 
conditional (! trace_rules andalso not (null rules)) (fn () => 

252 
Pretty.big_list "rules:" (map (ProofContext.pretty_thm ctxt) rules) 

253 
> Pretty.string_of > tracing); 

12347  254 

255 
local 

256 

10541
fdec07d4f047
resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;
wenzelm
parents:
10529
diff
changeset

257 
fun gen_rule_tac tac rules [] i st = tac rules i st 
12324
5db4b4596d1a
rule context and attributes moved to rule_context.ML;
wenzelm
parents:
12311
diff
changeset

258 
 gen_rule_tac tac rules facts i st = 
18227  259 
Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules); 
7130  260 

10744  261 
fun gen_arule_tac tac j rules facts = 
262 
EVERY' (gen_rule_tac tac rules facts :: replicate j Tactic.assume_tac); 

263 

11785  264 
fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) => 
265 
let 

266 
val rules = 

267 
if not (null arg_rules) then arg_rules 

15570  268 
else List.concat (ContextRules.find_rules false facts goal ctxt) 
12055  269 
in trace ctxt rules; tac rules facts i end); 
10309  270 

10744  271 
fun meth tac x = METHOD (HEADGOAL o tac x); 
272 
fun meth' tac x y = METHOD (HEADGOAL o tac x y); 

8220  273 

7419  274 
in 
275 

10744  276 
val rule_tac = gen_rule_tac Tactic.resolve_tac; 
277 
val rule = meth rule_tac; 

278 
val some_rule_tac = gen_some_rule_tac rule_tac; 

279 
val some_rule = meth' some_rule_tac; 

280 

281 
val erule = meth' (gen_arule_tac Tactic.eresolve_tac); 

282 
val drule = meth' (gen_arule_tac Tactic.dresolve_tac); 

283 
val frule = meth' (gen_arule_tac Tactic.forward_tac); 

5824  284 

7419  285 
end; 
286 

287 

17587  288 
(* iprover  intuitionistic proof search *) 
17110  289 

290 
local 

291 

292 
val remdups_tac = SUBGOAL (fn (g, i) => 

293 
let val prems = Logic.strip_assums_hyp g in 

294 
REPEAT_DETERM_N (length prems  length (gen_distinct op aconv prems)) 

295 
(Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i) 

296 
end); 

297 

298 
fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac; 

299 

300 
fun gen_eq_set e s1 s2 = 

301 
length s1 = length s2 andalso 

302 
gen_subset e (s1, s2) andalso gen_subset e (s2, s1); 

303 

304 
val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist; 

305 

306 
fun safe_step_tac ctxt = 

307 
ContextRules.Swrap ctxt 

308 
(eq_assume_tac ORELSE' 

309 
bires_tac true (ContextRules.netpair_bang ctxt)); 

8195  310 

17110  311 
fun unsafe_step_tac ctxt = 
312 
ContextRules.wrap ctxt 

313 
(assume_tac APPEND' 

314 
bires_tac false (ContextRules.netpair_bang ctxt) APPEND' 

315 
bires_tac false (ContextRules.netpair ctxt)); 

316 

317 
fun step_tac ctxt i = 

318 
REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE 

319 
REMDUPS (unsafe_step_tac ctxt) i; 

320 

321 
fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else 

322 
let 

323 
val ps = Logic.strip_assums_hyp g; 

324 
val c = Logic.strip_assums_concl g; 

325 
in 

326 
if gen_mem (fn ((ps1, c1), (ps2, c2)) => 

327 
c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) ((ps, c), gs) then no_tac 

328 
else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i 

329 
end); 

330 

331 
in 

332 

17587  333 
fun iprover_tac ctxt opt_lim = 
17110  334 
SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intprover_tac ctxt [] 0) 4 1); 
335 

336 
end; 

8195  337 

338 

17110  339 
(* rule_tac etc.  refer to dynamic goal state!! *) 
12119  340 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

341 
fun bires_inst_tac bires_flag ctxt insts thm = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

342 
let 
17110  343 
val thy = ProofContext.theory_of ctxt; 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

344 
(* Separate type and term insts *) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

345 
fun has_type_var ((x, _), _) = (case Symbol.explode x of 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

346 
"'"::cs => true  cs => false); 
15570  347 
val Tinsts = List.filter has_type_var insts; 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

348 
val tinsts = filter_out has_type_var insts; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

349 
(* Tactic *) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

350 
fun tac i st = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

351 
let 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

352 
(* Preprocess state: extract environment information: 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

353 
 variables and their types 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

354 
 type variables and their sorts 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

355 
 parameters and their types *) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

356 
val (types, sorts) = types_sorts st; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

357 
(* Process type insts: Tinsts_env *) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

358 
fun absent xi = error 
14718  359 
("No such variable in theorem: " ^ Syntax.string_of_vname xi); 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

360 
val (rtypes, rsorts) = types_sorts thm; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

361 
fun readT (xi, s) = 
15531  362 
let val S = case rsorts xi of SOME S => S  NONE => absent xi; 
17110  363 
val T = Sign.read_typ (thy, sorts) s; 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15713
diff
changeset

364 
val U = TVar (xi, S); 
17110  365 
in if Sign.typ_instance thy (T, U) then (U, T) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

366 
else error 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

367 
("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

368 
end; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

369 
val Tinsts_env = map readT Tinsts; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

370 
(* Preprocess rule: extract vars and their types, apply Tinsts *) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

371 
fun get_typ xi = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

372 
(case rtypes xi of 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15713
diff
changeset

373 
SOME T => typ_subst_atomic Tinsts_env T 
15531  374 
 NONE => absent xi); 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

375 
val (xis, ss) = Library.split_list tinsts; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

376 
val Ts = map get_typ xis; 
14718  377 
val (_, _, Bi, _) = dest_state(st,i) 
378 
val params = Logic.strip_params Bi 

379 
(* params of subgoal i as string typ pairs *) 

380 
val params = rev(Term.rename_wrt_term Bi params) 

381 
(* as they are printed: bound variables with *) 

14508
859b11514537
Experimental command for instantiation of locales in proof contexts:
ballarin
parents:
14215
diff
changeset

382 
(* the same name are renamed during printing *) 
17314  383 
fun types' (a, ~1) = (case AList.lookup (op =) params a of 
15531  384 
NONE => types (a, ~1) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

385 
 some => some) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

386 
 types' xi = types xi; 
15973  387 
fun internal x = is_some (types' (x, ~1)); 
15703  388 
val used = Drule.add_used thm (Drule.add_used st []); 
14718  389 
val (ts, envT) = 
390 
ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts); 

15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15713
diff
changeset

391 
val envT' = map (fn (ixn, T) => 
15973  392 
(TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env; 
14718  393 
val cenv = 
394 
map 

395 
(fn (xi, t) => 

17110  396 
pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t)) 
14718  397 
(gen_distinct 
398 
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) 

399 
(xis ~~ ts)); 

400 
(* Lift and instantiate rule *) 

401 
val {maxidx, ...} = rep_thm st; 

402 
val paramTs = map #2 params 

403 
and inc = maxidx+1 

404 
fun liftvar (Var ((a,j), T)) = 

16876  405 
Var((a, j+inc), paramTs > Logic.incr_tvar inc T) 
14718  406 
 liftvar t = raise TERM("Variable expected", [t]); 
407 
fun liftterm t = list_abs_free 

408 
(params, Logic.incr_indexes(paramTs,inc) t) 

409 
fun liftpair (cv,ct) = 

410 
(cterm_fun liftvar cv, cterm_fun liftterm ct) 

17110  411 
val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc); 
14718  412 
val rule = Drule.instantiate 
15798
016f3be5a5ec
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15713
diff
changeset

413 
(map lifttvar envT', map liftpair cenv) 
18145  414 
(Thm.lift_rule (Thm.cprem_of st i) thm) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

415 
in 
14718  416 
if i > nprems_of st then no_tac st 
417 
else st > 

418 
compose_tac (bires_flag, rule, nprems_of thm) i 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

419 
end 
14718  420 
handle TERM (msg,_) => (warning msg; no_tac st) 
421 
 THM (msg,_,_) => (warning msg; no_tac st); 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

422 
in 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

423 
tac 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

424 
end; 
8238  425 

17110  426 
local 
427 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

428 
fun gen_inst _ tac _ (quant, ([], thms)) = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

429 
METHOD (fn facts => quant (insert_tac facts THEN' tac thms)) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

430 
 gen_inst inst_tac _ ctxt (quant, (insts, [thm])) = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

431 
METHOD (fn facts => 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

432 
quant (insert_tac facts THEN' inst_tac ctxt insts thm)) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

433 
 gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules"; 
14718  434 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

435 
(* Preserve Var indexes of rl; increment revcut_rl instead. 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

436 
Copied from tactic.ML *) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

437 
fun make_elim_preserve rl = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

438 
let val {maxidx,...} = rep_thm rl 
17110  439 
fun cvar xi = cterm_of ProtoPure.thy (Var(xi,propT)); 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

440 
val revcut_rl' = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

441 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

442 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

443 
val arg = (false, rl, nprems_of rl) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

444 
val [th] = Seq.list_of (bicompose false arg 1 revcut_rl') 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

445 
in th end 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

446 
handle Bind => raise THM("make_elim_preserve", 1, [rl]); 
8238  447 

17110  448 
in 
449 

450 
val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac; 

451 

452 
val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac; 

453 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

454 
val cut_inst_meth = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

455 
gen_inst 
17110  456 
(fn ctxt => fn insts => bires_inst_tac false ctxt insts o make_elim_preserve) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

457 
Tactic.cut_rules_tac; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

458 

f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

459 
val dres_inst_meth = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

460 
gen_inst 
17110  461 
(fn ctxt => fn insts => bires_inst_tac true ctxt insts o make_elim_preserve) 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

462 
Tactic.dresolve_tac; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

463 

f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

464 
val forw_inst_meth = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

465 
gen_inst 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

466 
(fn ctxt => fn insts => fn rule => 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

467 
bires_inst_tac false ctxt insts (make_elim_preserve rule) THEN' 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

468 
assume_tac) 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

469 
Tactic.forward_tac; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

470 

f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

471 
fun subgoal_tac ctxt sprop = 
17110  472 
DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl; 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

473 

f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

474 
fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops); 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

475 

f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

476 
fun thin_tac ctxt s = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

477 
bires_inst_tac true ctxt [(("V", 0), s)] thin_rl; 
8238  478 

17110  479 
end; 
8329  480 

481 

8351  482 
(* ML tactics *) 
483 

17110  484 
val tactic_ref = ref ((fn _ => raise Match): ProofContext.context > thm list > tactic); 
8351  485 
fun set_tactic f = tactic_ref := f; 
486 

487 
fun tactic txt ctxt = METHOD (fn facts => 

9631  488 
(Context.use_mltext 
17110  489 
("let fun tactic (ctxt: ProofContext.context) (facts: thm list) : tactic = \ 
16500
09d43301b195
refl_tac: avoid failure of unification, i.e. confusing trace msg;
wenzelm
parents:
16448
diff
changeset

490 
\let val thm = ProofContext.get_thm_closure ctxt o PureThy.Name\n\ 
09d43301b195
refl_tac: avoid failure of unification, i.e. confusing trace msg;
wenzelm
parents:
16448
diff
changeset

491 
\ and thms = ProofContext.get_thms_closure ctxt o PureThy.Name in\n" 
09d43301b195
refl_tac: avoid failure of unification, i.e. confusing trace msg;
wenzelm
parents:
16448
diff
changeset

492 
^ txt ^ 
09d43301b195
refl_tac: avoid failure of unification, i.e. confusing trace msg;
wenzelm
parents:
16448
diff
changeset

493 
"\nend in Method.set_tactic tactic end") 
15531  494 
false NONE; 
495 
Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts)); 

8351  496 

497 

5824  498 

17110  499 
(** method syntax **) 
500 

501 
(* method text *) 

502 

503 
type src = Args.src; 

5824  504 

17110  505 
datatype text = 
506 
Basic of (ProofContext.context > method)  

507 
Source of src  

508 
Then of text list  

509 
Orelse of text list  

510 
Try of text  

511 
Repeat1 of text; 

512 

17857  513 
val primitive_text = Basic o K o SIMPLE_METHOD o PRIMITIVE; 
514 
val succeed_text = Basic (K succeed); 

17110  515 
val default_text = Source (Args.src (("default", []), Position.none)); 
516 
val this_text = Basic (K this); 

517 
val done_text = Basic (K (SIMPLE_METHOD all_tac)); 

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

518 
val sorry_text = Basic o cheating; 
17110  519 

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

520 
fun finish_text (NONE, immed) = Basic (close immed) 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

521 
 finish_text (SOME txt, immed) = Then [txt, Basic (close immed)]; 
17110  522 

523 

524 
(* method definitions *) 

5824  525 

16448  526 
structure MethodsData = TheoryDataFun 
527 
(struct 

5824  528 
val name = "Isar/methods"; 
17110  529 
type T = (((src > ProofContext.context > method) * string) * stamp) NameSpace.table; 
5824  530 

16347  531 
val empty = NameSpace.empty_table; 
6546  532 
val copy = I; 
16448  533 
val extend = I; 
17496  534 
fun merge _ tables = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups => 
16347  535 
error ("Attempt to merge different versions of method(s) " ^ commas_quote dups); 
5824  536 

16347  537 
fun print _ meths = 
5824  538 
let 
539 
fun prt_meth (name, ((_, comment), _)) = Pretty.block 

6849  540 
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; 
5824  541 
in 
16347  542 
[Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))] 
9222  543 
> Pretty.chunks > Pretty.writeln 
5824  544 
end; 
16448  545 
end); 
5824  546 

18708  547 
val _ = Context.add_setup MethodsData.init; 
5824  548 
val print_methods = MethodsData.print; 
7611  549 

5824  550 

551 
(* get methods *) 

552 

5916  553 
exception METHOD_FAIL of (string * Position.T) * exn; 
554 

5824  555 
fun method thy = 
556 
let 

16347  557 
val (space, meths) = MethodsData.get thy; 
5884  558 
fun meth src = 
559 
let 

560 
val ((raw_name, _), pos) = Args.dest_src src; 

561 
val name = NameSpace.intern space raw_name; 

562 
in 

17412  563 
(case Symtab.lookup meths name of 
15531  564 
NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) 
565 
 SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src)) 

5824  566 
end; 
567 
in meth end; 

568 

569 

17110  570 
(* add method *) 
5824  571 

572 
fun add_methods raw_meths thy = 

573 
let 

16145  574 
val new_meths = raw_meths > map (fn (name, f, comment) => 
16347  575 
(name, ((f, comment), stamp ()))); 
5824  576 

17110  577 
fun add meths = NameSpace.extend_table (Sign.naming_of thy) (meths, new_meths) 
16347  578 
handle Symtab.DUPS dups => 
579 
error ("Duplicate declaration of method(s) " ^ commas_quote dups); 

580 
in MethodsData.map add thy end; 

5824  581 

9194  582 
val add_method = add_methods o Library.single; 
583 

18728  584 
fun Method name meth cmt = Context.>> (add_method (name, meth, cmt)); 
5824  585 

586 

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

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

588 

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

589 
fun method_setup (name, txt, cmt) = 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

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

591 
"val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\ 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

592 
\val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\ 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

593 
\val method: bstring * (Method.src > ProofContext.context > Proof.method) * string" 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

594 
"Method.add_method method" 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

595 
("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")"); 
09afdf37cdb3
added cheating, sorry_text (from skip_proofs.ML);
wenzelm
parents:
17314
diff
changeset

596 

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

597 

5884  598 

17110  599 
(** concrete syntax **) 
5824  600 

5884  601 
(* basic *) 
602 

17110  603 
fun syntax (scan: 
604 
(ProofContext.context * Args.T list > 'a * (ProofContext.context * Args.T list))) = 

5884  605 
Args.syntax "method" scan; 
5824  606 

17110  607 
fun simple_args scan f src ctxt : method = 
8351  608 
#2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt); 
609 

17110  610 
fun ctxt_args (f: ProofContext.context > method) src ctxt = 
8282  611 
#2 (syntax (Scan.succeed (f ctxt)) src ctxt); 
7555  612 

613 
fun no_args m = ctxt_args (K m); 

5884  614 

615 

616 
(* sections *) 

5824  617 

18728  618 
type modifier = (ProofContext.context > ProofContext.context) * attribute; 
7268  619 

620 
local 

621 

8381  622 
fun sect ss = Scan.first (map Scan.lift ss); 
5884  623 
fun thms ss = Scan.unless (sect ss) Attrib.local_thms; 
15570  624 
fun thmss ss = Scan.repeat (thms ss) >> List.concat; 
5884  625 

18728  626 
fun apply (f, att) (ctxt, ths) = foldl_map (Thm.proof_attributes [att]) (f ctxt, ths); 
5824  627 

7268  628 
fun section ss = (sect ss  thmss ss) : (fn (m, ths) => Scan.depend (fn ctxt => 
629 
Scan.succeed (apply m (ctxt, ths)))) >> #2; 

5884  630 

7601  631 
fun sectioned args ss = args  Scan.repeat (section ss); 
5884  632 

7268  633 
in 
5824  634 

5884  635 
fun sectioned_args args ss f src ctxt = 
8282  636 
let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt 
5921  637 
in f x ctxt' end; 
5884  638 

7601  639 
fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f; 
9777  640 
fun bang_sectioned_args' ss scan f = 
641 
sectioned_args (Args.bang_facts  scan >> swap) ss (uncurry f); 

7601  642 
fun only_sectioned_args ss f = sectioned_args (Scan.succeed ()) ss (fn () => f); 
7268  643 

8093  644 
fun thms_ctxt_args f = sectioned_args (thmss []) [] f; 
645 
fun thms_args f = thms_ctxt_args (K o f); 

9706  646 
fun thm_args f = thms_args (fn [thm] => f thm  _ => error "Single theorem expected"); 
5824  647 

7268  648 
end; 
649 

5824  650 

17587  651 
(* iprover syntax *) 
12347  652 

653 
local 

654 

655 
val introN = "intro"; 

656 
val elimN = "elim"; 

657 
val destN = "dest"; 

658 
val ruleN = "rule"; 

659 

660 
fun modifier name kind kind' att = 

15531  661 
Args.$$$ name  (kind >> K NONE  kind'  Args.nat  Args.colon >> SOME) 
17110  662 
>> (pair (I: ProofContext.context > ProofContext.context) o att); 
12347  663 

17587  664 
val iprover_modifiers = 
18728  665 
[modifier destN Args.bang_colon Args.bang ContextRules.dest_bang, 
666 
modifier destN Args.colon (Scan.succeed ()) ContextRules.dest, 

667 
modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang, 

668 
modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim, 

669 
modifier introN Args.bang_colon Args.bang ContextRules.intro_bang, 

670 
modifier introN Args.colon (Scan.succeed ()) ContextRules.intro, 

671 
Args.del  Args.colon >> K (I, ContextRules.rule_del)]; 

12347  672 

673 
in 

674 

18640  675 
val iprover_meth = 
676 
bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat)) 

677 
(fn n => fn prems => fn ctxt => METHOD (fn facts => 

678 
HEADGOAL (insert_tac (prems @ facts) THEN' 

679 
ObjectLogic.atomize_tac THEN' iprover_tac ctxt n))); 

12347  680 

681 
end; 

682 

683 

9539  684 
(* tactic syntax *) 
8238  685 

10744  686 
fun nat_thms_args f = uncurry f oo 
687 
(#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0)  Attrib.local_thmss)); 

688 

8238  689 
val insts = 
9539  690 
Scan.optional 
9565
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

691 
(Args.enum1 "and" (Scan.lift (Args.name  (Args.$$$ "="  Args.!!! Args.name)))  
3eb2ea15cc69
res_inst: include noninst versions with multiple thms;
wenzelm
parents:
9539
diff
changeset

692 
Scan.lift (Args.$$$ "in")) []  Attrib.local_thmss; 
8238  693 

12119  694 
fun inst_args f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL  insts) src ctxt)); 
8537  695 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

696 
val insts_var = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

697 
Scan.optional 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

698 
(Args.enum1 "and" (Scan.lift (Args.var  (Args.$$$ "="  Args.!!! Args.name)))  
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

699 
Scan.lift (Args.$$$ "in")) []  Attrib.local_thmss; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

700 

17110  701 
fun inst_args_var f src ctxt = 
702 
f ctxt (#2 (syntax (Args.goal_spec HEADGOAL  insts_var) src ctxt)); 

8537  703 

12119  704 
fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL  args >> 
14215
ebf291f3b449
Improvements to Isar/Locales: premises generated by "includes" elements
ballarin
parents:
14174
diff
changeset

705 
(fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt); 
8537  706 

9539  707 
fun goal_args args tac = goal_args' (Scan.lift args) tac; 
8238  708 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

709 
fun goal_args_ctxt' args tac src ctxt = 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

710 
#2 (syntax (Args.goal_spec HEADGOAL  args >> 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

711 
(fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt); 
8238  712 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

713 
fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac; 
5824  714 

14718  715 

9539  716 
(* misc tactic emulations *) 
717 

14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

718 
val subgoal_meth = goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac; 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

719 
val thin_meth = goal_args_ctxt Args.name thin_tac; 
9539  720 
val rename_meth = goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac; 
9631  721 
val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac; 
9539  722 

723 

18708  724 
(* theory setup *) 
5824  725 

18708  726 
val _ = Context.add_setup (add_methods 
5824  727 
[("fail", no_args fail, "force failure"), 
728 
("succeed", no_args succeed, "succeed"), 

9587  729 
("", no_args insert_facts, "do nothing (insert current facts only)"), 
9539  730 
("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), 
16145  731 
("unfold", thms_args unfold_meth, "unfold definitions"), 
12384  732 
("intro", thms_args intro, "repeatedly apply introduction rules"), 
733 
("elim", thms_args elim, "repeatedly apply elimination rules"), 

16145  734 
("fold", thms_args fold_meth, "fold definitions"), 
12829  735 
("atomize", (atomize o #2) oo syntax (Args.mode "full"), 
11962  736 
"present local premises as objectlevel statements"), 
18640  737 
("iprover", iprover_meth, "intuitionistic proof search"), 
12384  738 
("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"), 
10744  739 
("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), 
740 
("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), 

741 
("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), 

8195  742 
("this", no_args this, "apply current facts as rules"), 
18039  743 
("fact", thms_ctxt_args fact, "composition by facts from context"), 
8238  744 
("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), 
14174
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

745 
("rule_tac", inst_args_var res_inst_meth, "apply rule (dynamic instantiation)"), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

746 
("erule_tac", inst_args_var eres_inst_meth, "apply rule in elimination manner (dynamic instantiation)"), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

747 
("drule_tac", inst_args_var dres_inst_meth, "apply rule in destruct manner (dynamic instantiation)"), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

748 
("frule_tac", inst_args_var forw_inst_meth, "apply rule in forward manner (dynamic instantiation)"), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

749 
("cut_tac", inst_args_var cut_inst_meth, "cut rule (dynamic instantiation)"), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

750 
("subgoal_tac", subgoal_meth, "insert subgoal (dynamic instantiation)"), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

751 
("thin_tac", thin_meth, "remove premise (dynamic instantiation)"), 
f3cafd2929d5
Methods rule_tac etc support static (Isar) contexts.
ballarin
parents:
13650
diff
changeset

752 
("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"), 
9631  753 
("rotate_tac", rotate_meth, "rotate assumptions of goal"), 
18708  754 
("tactic", simple_args Args.name tactic, "ML tactic as proof method")]); 
5824  755 

756 

16145  757 
(*final declarations of this structure!*) 
758 
val unfold = unfold_meth; 

759 
val fold = fold_meth; 

760 

5824  761 
end; 
762 

763 
structure BasicMethod: BASIC_METHOD = Method; 

764 
open BasicMethod; 