src/Pure/subgoal.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 22568 ed7aa5a350ef
child 29606 fedb8be05f24
permissions -rw-r--r--
Name.uu, Name.aT;
     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') =
    33       Variable.import_thms true [MetaSimplifier.norm_hhf_protect st] ctxt;
    34     val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
    35     val asms = Drule.strip_imp_prems goal;
    36     val concl = Drule.strip_imp_concl goal;
    37     val (prems, context) = Assumption.add_assumes asms ctxt'';
    38   in
    39     ({context = context, schematics = schematics, params = params,
    40       asms = asms, concl = concl, prems = prems}, Goal.init concl)
    41   end;
    42 
    43 fun SUBPROOF tac ctxt i st =
    44   if Thm.nprems_of st < i then Seq.empty
    45   else
    46     let
    47       val (args as {context, params, ...}, st') = focus ctxt i st;
    48       fun export_closed th =
    49         let
    50           val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
    51           val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
    52         in Drule.forall_intr_list vs th' end;
    53       fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
    54     in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
    55 
    56 end;
    57 
    58 structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
    59 open BasicSubgoal;