src/Pure/context_tactic.ML

--- /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;