src/Pure/subgoal.ML
author wenzelm
Wed Aug 02 22:26:55 2006 +0200 (2006-08-02)
changeset 20301 66b2a1f16bbb
parent 20231 dcdd565a7fbe
child 20579 4dc799edef89
permissions -rw-r--r--
Variable.focus_subgoal;
     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:
    11     ({context: Proof.context, schematics: ctyp list * cterm list,
    12       params: cterm list, asms: cterm list, concl: cterm,
    13       prems: thm list} -> tactic) -> Proof.context -> int -> tactic
    14 end
    15 
    16 signature SUBGOAL =
    17 sig
    18   include BASIC_SUBGOAL
    19   val focus: Proof.context -> int -> thm ->
    20    {context: Proof.context, schematics: ctyp list * cterm list,
    21     params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
    22 
    23 end;
    24 
    25 structure Subgoal: SUBGOAL =
    26 struct
    27 
    28 (* canonical proof decomposition -- similar to fix/assume/show *)
    29 
    30 fun focus ctxt i st =
    31   let
    32     val ((schematics, [st']), ctxt') = Variable.import true [norm_hhf st] ctxt;
    33     val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
    34     val asms = Drule.strip_imp_prems goal;
    35     val concl = Drule.strip_imp_concl goal;
    36     val (prems, context) = Assumption.add_assumes asms ctxt'';
    37   in
    38     ({context = context, schematics = schematics, params = params,
    39       asms = asms, concl = concl, prems = prems}, Goal.init concl)
    40   end;
    41 
    42 fun SUBPROOF tac ctxt i st =
    43   if Thm.nprems_of st < i then Seq.empty
    44   else
    45     let
    46       val (args as {context, params, ...}, st') = focus ctxt i st;
    47       fun export_closed th =
    48         let
    49           val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
    50           val vs = map (#2 o Thm.dest_comb o Drule.strip_imp_concl o Thm.cprop_of) params';
    51         in Drule.forall_intr_list vs th' end;
    52       fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
    53     in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
    54 
    55 end;
    56 
    57 structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
    58 open BasicSubgoal;