src/Pure/subgoal.ML
author wenzelm
Wed Jul 26 00:44:48 2006 +0200 (2006-07-26)
changeset 20210 8fe4ae4360eb
child 20219 3bff4719f3d6
permissions -rw-r--r--
Tactical operations depending on local subgoal structure.
     1 (*  Title:      Pure/subgoal.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Tactical operations depending on local subgoal structure.
     6 *)
     7 
     8 signature BASIC_SUBGOAL =
     9 sig
    10   val SUBPROOF: Proof.context ->
    11     ({context: Proof.context, asms: cterm list, concl: cterm,
    12       params: (string * typ) list, prems: thm list} -> tactic) -> int -> tactic
    13 end
    14 
    15 signature SUBGOAL =
    16 sig
    17   include BASIC_SUBGOAL
    18   val focus: Proof.context -> int -> thm ->
    19    {context: Proof.context, asms: cterm list, concl: cterm,
    20     params: (string * typ) list, prems: thm list} * thm
    21 
    22 end;
    23 
    24 structure Subgoal: SUBGOAL =
    25 struct
    26 
    27 (* canonical proof decomposition -- similar to fix/assume/show *)
    28 
    29 fun focus ctxt i st =
    30   let
    31     val ([st'], ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
    32     val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
    33     val asms = Drule.strip_imp_prems goal;
    34     val concl = Drule.strip_imp_concl goal;
    35     val (prems, context) = ProofContext.add_assumes asms ctxt'';
    36   in
    37     ({context = context, asms = asms, concl = concl, params = params, prems = prems},
    38       Goal.init concl)
    39   end;
    40 
    41 fun SUBPROOF ctxt tac i st =
    42   if Thm.nprems_of st < i then Seq.empty
    43   else
    44     let
    45       val (args as {context, ...}, st') = focus ctxt i st
    46       val result = Goal.conclude #> Seq.singleton (ProofContext.goal_exports context ctxt);
    47     in Seq.lifts (fn res => Proof.goal_tac res i) (Seq.maps result (tac args st')) st end
    48 
    49 end;
    50 
    51 structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
    52 open BasicSubgoal;