--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/context_tactic.ML Tue Aug 13 10:27:21 2019 +0200
@@ -0,0 +1,58 @@
+(* Title: Pure/context_tactic.ML
+ Author: Makarius
+
+Tactics with proof context / cases -- as basis for Isar proof methods.
+*)
+
+infix 1 CONTEXT_THEN_ALL_NEW;
+
+signature BASIC_CONTEXT_TACTIC =
+sig
+ type context_state = Proof.context * thm
+ type context_tactic = context_state -> context_state Seq.result Seq.seq
+ val TACTIC_CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq
+ val CONTEXT_TACTIC: tactic -> context_tactic
+ val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic
+ val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
+ val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
+ val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
+end;
+
+signature CONTEXT_TACTIC =
+sig
+ include BASIC_CONTEXT_TACTIC
+end;
+
+structure Context_Tactic: CONTEXT_TACTIC =
+struct
+
+type context_state = Proof.context * thm;
+type context_tactic = context_state -> context_state Seq.result Seq.seq;
+
+fun TACTIC_CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq =
+ Seq.map (Seq.Result o pair ctxt);
+
+fun CONTEXT_TACTIC tac : context_tactic =
+ fn (ctxt, st) => TACTIC_CONTEXT ctxt (tac st);
+
+fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st =
+ tac (ctxt, st) |> Seq.filter_results |> Seq.map snd;
+
+fun CONTEXT_CASES cases tac : context_tactic =
+ fn (ctxt, st) => TACTIC_CONTEXT (Proof_Context.update_cases cases ctxt) (tac st);
+
+fun CONTEXT_SUBGOAL tac i : context_tactic =
+ fn (ctxt, st) =>
+ (case try Logic.nth_prem (i, Thm.prop_of st) of
+ SOME goal => tac (goal, i) (ctxt, st)
+ | NONE => Seq.empty);
+
+fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic =
+ fn (ctxt, st) =>
+ (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
+ TACTIC_CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));
+
+end;
+
+structure Basic_Context_Tactic: BASIC_CONTEXT_TACTIC = Context_Tactic;
+open Basic_Context_Tactic;