37 val insert_tac: thm list -> int -> tactic |
37 val insert_tac: thm list -> int -> tactic |
38 val insert: thm list -> Proof.method |
38 val insert: thm list -> Proof.method |
39 val insert_facts: Proof.method |
39 val insert_facts: Proof.method |
40 val unfold: thm list -> Proof.method |
40 val unfold: thm list -> Proof.method |
41 val fold: thm list -> Proof.method |
41 val fold: thm list -> Proof.method |
|
42 val rewrite_goal_tac: thm list -> int -> tactic |
42 val atomize_tac: thm list -> int -> tactic |
43 val atomize_tac: thm list -> int -> tactic |
43 val atomize_goal: thm list -> int -> thm -> thm |
44 val atomize_goal: thm list -> int -> thm -> thm |
44 val multi_resolve: thm list -> thm -> thm Seq.seq |
45 val multi_resolve: thm list -> thm -> thm Seq.seq |
45 val multi_resolves: thm list -> thm list -> thm Seq.seq |
46 val multi_resolves: thm list -> thm list -> thm Seq.seq |
46 val resolveq_tac: thm Seq.seq -> int -> tactic |
47 val resolveq_tac: thm Seq.seq -> int -> tactic |
47 val resolveq_cases_tac: bool -> (thm * string list) Seq.seq |
48 val resolveq_cases_tac: (thm -> string list -> (string * RuleCases.T) list) |
48 -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq |
49 -> (thm * string list) Seq.seq -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq |
49 val rule_tac: thm list -> thm list -> int -> tactic |
50 val rule_tac: thm list -> thm list -> int -> tactic |
50 val erule_tac: thm list -> thm list -> int -> tactic |
51 val erule_tac: thm list -> thm list -> int -> tactic |
51 val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic |
52 val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic |
52 val rule: thm list -> Proof.method |
53 val rule: thm list -> Proof.method |
53 val erule: thm list -> Proof.method |
54 val erule: thm list -> Proof.method |
275 fun fold thms = SIMPLE_METHOD (CHANGED (fold_goals_tac thms)); |
276 fun fold thms = SIMPLE_METHOD (CHANGED (fold_goals_tac thms)); |
276 |
277 |
277 |
278 |
278 (* atomize meta-connectives *) |
279 (* atomize meta-connectives *) |
279 |
280 |
280 fun atomize_tac rews i thm = |
281 fun rewrite_goal_tac rews = |
281 if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then |
282 Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews); |
282 Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews) i thm |
283 |
283 else all_tac thm; |
284 fun atomize_tac rews = |
284 |
285 let val rew_tac = rewrite_goal_tac rews in |
285 fun atomize_goal rews i thm = |
286 fn i => fn thm => |
286 (case Seq.pull (atomize_tac rews i thm) of |
287 if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then rew_tac i thm |
287 None => thm |
288 else all_tac thm |
288 | Some (thm', _) => thm'); |
289 end; |
|
290 |
|
291 fun atomize_goal rews = |
|
292 let val tac = atomize_tac rews |
|
293 in fn i => fn thm => (case Seq.pull (tac i thm) of None => thm | Some (thm', _) => thm') end; |
289 |
294 |
290 |
295 |
291 (* multi_resolve *) |
296 (* multi_resolve *) |
292 |
297 |
293 local |
298 local |
311 fun gen_resolveq_tac tac rules i st = |
316 fun gen_resolveq_tac tac rules i st = |
312 Seq.flat (Seq.map (fn rule => tac rule i st) rules); |
317 Seq.flat (Seq.map (fn rule => tac rule i st) rules); |
313 |
318 |
314 val resolveq_tac = gen_resolveq_tac Tactic.rtac; |
319 val resolveq_tac = gen_resolveq_tac Tactic.rtac; |
315 |
320 |
316 fun resolveq_cases_tac open_parms = gen_resolveq_tac (fn (rule, cases) => fn i => fn st => |
321 fun resolveq_cases_tac make = gen_resolveq_tac (fn (rule, cases) => fn i => fn st => |
317 Seq.map (rpair (RuleCases.make (not open_parms) rule cases)) (Tactic.rtac rule i st)); |
322 Seq.map (rpair (make rule cases)) (Tactic.rtac rule i st)); |
318 |
323 |
319 |
324 |
320 (* simple rule *) |
325 (* simple rule *) |
321 |
326 |
322 local |
327 local |
357 (* assumption *) |
362 (* assumption *) |
358 |
363 |
359 fun asm_tac ths = |
364 fun asm_tac ths = |
360 foldr (op APPEND') (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths, K no_tac); |
365 foldr (op APPEND') (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths, K no_tac); |
361 |
366 |
362 fun assm_tac ctxt = assume_tac APPEND' asm_tac (ProofContext.prems_of ctxt); |
367 fun assm_tac ctxt = |
|
368 assume_tac APPEND' |
|
369 asm_tac (ProofContext.prems_of ctxt) APPEND' |
|
370 Tactic.rtac Drule.reflexive_thm; |
363 |
371 |
364 fun assumption_tac ctxt [] = assm_tac ctxt |
372 fun assumption_tac ctxt [] = assm_tac ctxt |
365 | assumption_tac _ [fact] = asm_tac [fact] |
373 | assumption_tac _ [fact] = asm_tac [fact] |
366 | assumption_tac _ _ = K no_tac; |
374 | assumption_tac _ _ = K no_tac; |
367 |
375 |