src/Pure/subgoal.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29606 fedb8be05f24
child 30552 58db56278478
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/subgoal.ML
     2     Author:     Makarius
     3 
     4 Tactical operations depending on local subgoal structure.
     5 *)
     6 
     7 signature BASIC_SUBGOAL =
     8 sig
     9   val SUBPROOF:
    10     ({context: Proof.context, schematics: ctyp list * cterm list,
    11       params: cterm list, asms: cterm list, concl: cterm,
    12       prems: thm list} -> tactic) -> Proof.context -> 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, schematics: ctyp list * cterm list,
    20     params: cterm list, asms: cterm list, concl: cterm, 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 ((schematics, [st']), ctxt') =
    32       Variable.import_thms true [MetaSimplifier.norm_hhf_protect 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 (Thm.dest_arg 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;