src/Pure/subgoal.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 20579 4dc799edef89
child 21605 4e7307e229b3
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
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@20231
    10
  val SUBPROOF:
wenzelm@20219
    11
    ({context: Proof.context, schematics: ctyp list * cterm list,
wenzelm@20219
    12
      params: cterm list, asms: cterm list, concl: cterm,
wenzelm@20231
    13
      prems: thm list} -> tactic) -> Proof.context -> int -> tactic
wenzelm@20210
    14
end
wenzelm@20210
    15
wenzelm@20210
    16
signature SUBGOAL =
wenzelm@20210
    17
sig
wenzelm@20210
    18
  include BASIC_SUBGOAL
wenzelm@20210
    19
  val focus: Proof.context -> int -> thm ->
wenzelm@20219
    20
   {context: Proof.context, schematics: ctyp list * cterm list,
wenzelm@20219
    21
    params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
wenzelm@20210
    22
wenzelm@20210
    23
end;
wenzelm@20210
    24
wenzelm@20210
    25
structure Subgoal: SUBGOAL =
wenzelm@20210
    26
struct
wenzelm@20210
    27
wenzelm@20210
    28
(* canonical proof decomposition -- similar to fix/assume/show *)
wenzelm@20210
    29
wenzelm@20210
    30
fun focus ctxt i st =
wenzelm@20210
    31
  let
wenzelm@20231
    32
    val ((schematics, [st']), ctxt') = Variable.import true [norm_hhf st] ctxt;
wenzelm@20301
    33
    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
wenzelm@20210
    34
    val asms = Drule.strip_imp_prems goal;
wenzelm@20210
    35
    val concl = Drule.strip_imp_concl goal;
wenzelm@20231
    36
    val (prems, context) = Assumption.add_assumes asms ctxt'';
wenzelm@20210
    37
  in
wenzelm@20219
    38
    ({context = context, schematics = schematics, params = params,
wenzelm@20219
    39
      asms = asms, concl = concl, prems = prems}, Goal.init concl)
wenzelm@20210
    40
  end;
wenzelm@20210
    41
wenzelm@20231
    42
fun SUBPROOF tac ctxt i st =
wenzelm@20210
    43
  if Thm.nprems_of st < i then Seq.empty
wenzelm@20210
    44
  else
wenzelm@20210
    45
    let
wenzelm@20219
    46
      val (args as {context, params, ...}, st') = focus ctxt i st;
wenzelm@20219
    47
      fun export_closed th =
wenzelm@20219
    48
        let
wenzelm@20219
    49
          val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
wenzelm@20579
    50
          val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
wenzelm@20219
    51
        in Drule.forall_intr_list vs th' end;
wenzelm@20219
    52
      fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
wenzelm@20219
    53
    in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
wenzelm@20210
    54
wenzelm@20210
    55
end;
wenzelm@20210
    56
wenzelm@20210
    57
structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
wenzelm@20210
    58
open BasicSubgoal;