wenzelm@20210: (*  Title:      Pure/subgoal.ML
wenzelm@20210:     Author:     Makarius
wenzelm@20210: 
wenzelm@20210: Tactical operations depending on local subgoal structure.
wenzelm@20210: *)
wenzelm@20210: 
wenzelm@20210: signature BASIC_SUBGOAL =
wenzelm@20210: sig
wenzelm@20231:   val SUBPROOF:
wenzelm@20219:     ({context: Proof.context, schematics: ctyp list * cterm list,
wenzelm@20219:       params: cterm list, asms: cterm list, concl: cterm,
wenzelm@20231:       prems: thm list} -> tactic) -> Proof.context -> int -> tactic
wenzelm@20210: end
wenzelm@20210: 
wenzelm@20210: signature SUBGOAL =
wenzelm@20210: sig
wenzelm@20210:   include BASIC_SUBGOAL
wenzelm@20210:   val focus: Proof.context -> int -> thm ->
wenzelm@20219:    {context: Proof.context, schematics: ctyp list * cterm list,
wenzelm@20219:     params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
wenzelm@20210: 
wenzelm@20210: end;
wenzelm@20210: 
wenzelm@20210: structure Subgoal: SUBGOAL =
wenzelm@20210: struct
wenzelm@20210: 
wenzelm@20210: (* canonical proof decomposition -- similar to fix/assume/show *)
wenzelm@20210: 
wenzelm@20210: fun focus ctxt i st =
wenzelm@20210:   let
wenzelm@21605:     val ((schematics, [st']), ctxt') =
wenzelm@22568:       Variable.import_thms true [MetaSimplifier.norm_hhf_protect st] ctxt;
wenzelm@20301:     val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
wenzelm@20210:     val asms = Drule.strip_imp_prems goal;
wenzelm@20210:     val concl = Drule.strip_imp_concl goal;
wenzelm@20231:     val (prems, context) = Assumption.add_assumes asms ctxt'';
wenzelm@20210:   in
wenzelm@20219:     ({context = context, schematics = schematics, params = params,
wenzelm@20219:       asms = asms, concl = concl, prems = prems}, Goal.init concl)
wenzelm@20210:   end;
wenzelm@20210: 
wenzelm@20231: fun SUBPROOF tac ctxt i st =
wenzelm@20210:   if Thm.nprems_of st < i then Seq.empty
wenzelm@20210:   else
wenzelm@20210:     let
wenzelm@20219:       val (args as {context, params, ...}, st') = focus ctxt i st;
wenzelm@20219:       fun export_closed th =
wenzelm@20219:         let
wenzelm@20219:           val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
wenzelm@20579:           val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
wenzelm@20219:         in Drule.forall_intr_list vs th' end;
wenzelm@20219:       fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
wenzelm@20219:     in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
wenzelm@20210: 
wenzelm@20210: end;
wenzelm@20210: 
wenzelm@20210: structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
wenzelm@20210: open BasicSubgoal;