src/Pure/subgoal.ML
author wenzelm
Wed Jul 26 00:44:48 2006 +0200 (2006-07-26 ago)
changeset 20210 8fe4ae4360eb
child 20219 3bff4719f3d6
permissions -rw-r--r--
Tactical operations depending on local subgoal structure.
wenzelm@20210
     1
(*  Title:      Pure/subgoal.ML
wenzelm@20210
     2
    ID:         $Id$
wenzelm@20210
     3
    Author:     Makarius
wenzelm@20210
     4
wenzelm@20210
     5
Tactical operations depending on local subgoal structure.
wenzelm@20210
     6
*)
wenzelm@20210
     7
wenzelm@20210
     8
signature BASIC_SUBGOAL =
wenzelm@20210
     9
sig
wenzelm@20210
    10
  val SUBPROOF: Proof.context ->
wenzelm@20210
    11
    ({context: Proof.context, asms: cterm list, concl: cterm,
wenzelm@20210
    12
      params: (string * typ) list, prems: thm list} -> tactic) -> int -> tactic
wenzelm@20210
    13
end
wenzelm@20210
    14
wenzelm@20210
    15
signature SUBGOAL =
wenzelm@20210
    16
sig
wenzelm@20210
    17
  include BASIC_SUBGOAL
wenzelm@20210
    18
  val focus: Proof.context -> int -> thm ->
wenzelm@20210
    19
   {context: Proof.context, asms: cterm list, concl: cterm,
wenzelm@20210
    20
    params: (string * typ) list, prems: thm list} * thm
wenzelm@20210
    21
wenzelm@20210
    22
end;
wenzelm@20210
    23
wenzelm@20210
    24
structure Subgoal: SUBGOAL =
wenzelm@20210
    25
struct
wenzelm@20210
    26
wenzelm@20210
    27
(* canonical proof decomposition -- similar to fix/assume/show *)
wenzelm@20210
    28
wenzelm@20210
    29
fun focus ctxt i st =
wenzelm@20210
    30
  let
wenzelm@20210
    31
    val ([st'], ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
wenzelm@20210
    32
    val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
wenzelm@20210
    33
    val asms = Drule.strip_imp_prems goal;
wenzelm@20210
    34
    val concl = Drule.strip_imp_concl goal;
wenzelm@20210
    35
    val (prems, context) = ProofContext.add_assumes asms ctxt'';
wenzelm@20210
    36
  in
wenzelm@20210
    37
    ({context = context, asms = asms, concl = concl, params = params, prems = prems},
wenzelm@20210
    38
      Goal.init concl)
wenzelm@20210
    39
  end;
wenzelm@20210
    40
wenzelm@20210
    41
fun SUBPROOF ctxt tac i st =
wenzelm@20210
    42
  if Thm.nprems_of st < i then Seq.empty
wenzelm@20210
    43
  else
wenzelm@20210
    44
    let
wenzelm@20210
    45
      val (args as {context, ...}, st') = focus ctxt i st
wenzelm@20210
    46
      val result = Goal.conclude #> Seq.singleton (ProofContext.goal_exports context ctxt);
wenzelm@20210
    47
    in Seq.lifts (fn res => Proof.goal_tac res i) (Seq.maps result (tac args st')) st end
wenzelm@20210
    48
wenzelm@20210
    49
end;
wenzelm@20210
    50
wenzelm@20210
    51
structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
wenzelm@20210
    52
open BasicSubgoal;