Tactical operations depending on local subgoal structure.
authorwenzelm
Wed Jul 26 00:44:48 2006 +0200 (2006-07-26)
changeset 202108fe4ae4360eb
parent 20209 974d98969ba6
child 20211 c7f907f41f7c
Tactical operations depending on local subgoal structure.
src/Pure/subgoal.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/subgoal.ML	Wed Jul 26 00:44:48 2006 +0200
     1.3 @@ -0,0 +1,52 @@
     1.4 +(*  Title:      Pure/subgoal.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Tactical operations depending on local subgoal structure.
     1.9 +*)
    1.10 +
    1.11 +signature BASIC_SUBGOAL =
    1.12 +sig
    1.13 +  val SUBPROOF: Proof.context ->
    1.14 +    ({context: Proof.context, asms: cterm list, concl: cterm,
    1.15 +      params: (string * typ) list, prems: thm list} -> tactic) -> int -> tactic
    1.16 +end
    1.17 +
    1.18 +signature SUBGOAL =
    1.19 +sig
    1.20 +  include BASIC_SUBGOAL
    1.21 +  val focus: Proof.context -> int -> thm ->
    1.22 +   {context: Proof.context, asms: cterm list, concl: cterm,
    1.23 +    params: (string * typ) list, prems: thm list} * thm
    1.24 +
    1.25 +end;
    1.26 +
    1.27 +structure Subgoal: SUBGOAL =
    1.28 +struct
    1.29 +
    1.30 +(* canonical proof decomposition -- similar to fix/assume/show *)
    1.31 +
    1.32 +fun focus ctxt i st =
    1.33 +  let
    1.34 +    val ([st'], ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
    1.35 +    val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
    1.36 +    val asms = Drule.strip_imp_prems goal;
    1.37 +    val concl = Drule.strip_imp_concl goal;
    1.38 +    val (prems, context) = ProofContext.add_assumes asms ctxt'';
    1.39 +  in
    1.40 +    ({context = context, asms = asms, concl = concl, params = params, prems = prems},
    1.41 +      Goal.init concl)
    1.42 +  end;
    1.43 +
    1.44 +fun SUBPROOF ctxt tac i st =
    1.45 +  if Thm.nprems_of st < i then Seq.empty
    1.46 +  else
    1.47 +    let
    1.48 +      val (args as {context, ...}, st') = focus ctxt i st
    1.49 +      val result = Goal.conclude #> Seq.singleton (ProofContext.goal_exports context ctxt);
    1.50 +    in Seq.lifts (fn res => Proof.goal_tac res i) (Seq.maps result (tac args st')) st end
    1.51 +
    1.52 +end;
    1.53 +
    1.54 +structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
    1.55 +open BasicSubgoal;