Tactical operations depending on local subgoal structure.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/subgoal.ML	Wed Jul 26 00:44:48 2006 +0200
@@ -0,0 +1,52 @@
+(*  Title:      Pure/subgoal.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Tactical operations depending on local subgoal structure.
+*)
+
+signature BASIC_SUBGOAL =
+sig
+  val SUBPROOF: Proof.context ->
+    ({context: Proof.context, asms: cterm list, concl: cterm,
+      params: (string * typ) list, prems: thm list} -> tactic) -> int -> tactic
+end
+
+signature SUBGOAL =
+sig
+  include BASIC_SUBGOAL
+  val focus: Proof.context -> int -> thm ->
+   {context: Proof.context, asms: cterm list, concl: cterm,
+    params: (string * typ) list, prems: thm list} * thm
+
+end;
+
+structure Subgoal: SUBGOAL =
+struct
+
+(* canonical proof decomposition -- similar to fix/assume/show *)
+
+fun focus ctxt i st =
+  let
+    val ([st'], ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
+    val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
+    val asms = Drule.strip_imp_prems goal;
+    val concl = Drule.strip_imp_concl goal;
+    val (prems, context) = ProofContext.add_assumes asms ctxt'';
+  in
+    ({context = context, asms = asms, concl = concl, params = params, prems = prems},
+      Goal.init concl)
+  end;
+
+fun SUBPROOF ctxt tac i st =
+  if Thm.nprems_of st < i then Seq.empty
+  else
+    let
+      val (args as {context, ...}, st') = focus ctxt i st
+      val result = Goal.conclude #> Seq.singleton (ProofContext.goal_exports context ctxt);
+    in Seq.lifts (fn res => Proof.goal_tac res i) (Seq.maps result (tac args st')) st end
+
+end;
+
+structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
+open BasicSubgoal;