src/Pure/subgoal.ML
author wenzelm
Wed Jul 26 19:37:42 2006 +0200 (2006-07-26)
changeset 20219 3bff4719f3d6
parent 20210 8fe4ae4360eb
child 20231 dcdd565a7fbe
permissions -rw-r--r--
focus: result record includes (fixed) schematic variables;
SUBGOAL: disallow pending subgoals, more robust re-composition;
     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, schematics: ctyp list * cterm list,
    12       params: cterm list, asms: cterm list, concl: cterm,
    13       prems: thm list} -> tactic) -> 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 [Goal.norm_hhf st] ctxt;
    33     val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
    34     val asms = Drule.strip_imp_prems goal;
    35     val concl = Drule.strip_imp_concl goal;
    36     val (prems, context) = ProofContext.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 ctxt tac 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;