|
1 (* Title: Pure/context_tactic.ML |
|
2 Author: Makarius |
|
3 |
|
4 Tactics with proof context / cases -- as basis for Isar proof methods. |
|
5 *) |
|
6 |
|
7 infix 1 CONTEXT_THEN_ALL_NEW; |
|
8 |
|
9 signature BASIC_CONTEXT_TACTIC = |
|
10 sig |
|
11 type context_state = Proof.context * thm |
|
12 type context_tactic = context_state -> context_state Seq.result Seq.seq |
|
13 val TACTIC_CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq |
|
14 val CONTEXT_TACTIC: tactic -> context_tactic |
|
15 val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic |
|
16 val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic |
|
17 val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic |
|
18 val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic |
|
19 end; |
|
20 |
|
21 signature CONTEXT_TACTIC = |
|
22 sig |
|
23 include BASIC_CONTEXT_TACTIC |
|
24 end; |
|
25 |
|
26 structure Context_Tactic: CONTEXT_TACTIC = |
|
27 struct |
|
28 |
|
29 type context_state = Proof.context * thm; |
|
30 type context_tactic = context_state -> context_state Seq.result Seq.seq; |
|
31 |
|
32 fun TACTIC_CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq = |
|
33 Seq.map (Seq.Result o pair ctxt); |
|
34 |
|
35 fun CONTEXT_TACTIC tac : context_tactic = |
|
36 fn (ctxt, st) => TACTIC_CONTEXT ctxt (tac st); |
|
37 |
|
38 fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st = |
|
39 tac (ctxt, st) |> Seq.filter_results |> Seq.map snd; |
|
40 |
|
41 fun CONTEXT_CASES cases tac : context_tactic = |
|
42 fn (ctxt, st) => TACTIC_CONTEXT (Proof_Context.update_cases cases ctxt) (tac st); |
|
43 |
|
44 fun CONTEXT_SUBGOAL tac i : context_tactic = |
|
45 fn (ctxt, st) => |
|
46 (case try Logic.nth_prem (i, Thm.prop_of st) of |
|
47 SOME goal => tac (goal, i) (ctxt, st) |
|
48 | NONE => Seq.empty); |
|
49 |
|
50 fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic = |
|
51 fn (ctxt, st) => |
|
52 (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') => |
|
53 TACTIC_CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st')); |
|
54 |
|
55 end; |
|
56 |
|
57 structure Basic_Context_Tactic: BASIC_CONTEXT_TACTIC = Context_Tactic; |
|
58 open Basic_Context_Tactic; |