src/Pure/context_tactic.ML

clarified modules;

(*  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;