src/Pure/subgoal.ML
author wenzelm
Wed, 24 Jun 2009 21:28:02 +0200
changeset 31794 71af1fd6a5e4
parent 30552 58db56278478
child 32200 2bd8ab91a426
permissions -rw-r--r--
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/subgoal.ML
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     3
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     4
Tactical operations depending on local subgoal structure.
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     5
*)
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     6
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     7
signature BASIC_SUBGOAL =
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     8
sig
20231
dcdd565a7fbe tuned interfaces;
wenzelm
parents: 20219
diff changeset
     9
  val SUBPROOF:
20219
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    10
    ({context: Proof.context, schematics: ctyp list * cterm list,
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    11
      params: cterm list, asms: cterm list, concl: cterm,
20231
dcdd565a7fbe tuned interfaces;
wenzelm
parents: 20219
diff changeset
    12
      prems: thm list} -> tactic) -> Proof.context -> int -> tactic
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    13
end
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    14
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    15
signature SUBGOAL =
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    16
sig
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    17
  include BASIC_SUBGOAL
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    18
  val focus: Proof.context -> int -> thm ->
20219
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    19
   {context: Proof.context, schematics: ctyp list * cterm list,
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    20
    params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    21
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    22
end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    23
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    24
structure Subgoal: SUBGOAL =
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    25
struct
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    26
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    27
(* canonical proof decomposition -- similar to fix/assume/show *)
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    28
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    29
fun focus ctxt i st =
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    30
  let
21605
4e7307e229b3 qualified MetaSimplifier.norm_hhf(_protect);
wenzelm
parents: 20579
diff changeset
    31
    val ((schematics, [st']), ctxt') =
31794
71af1fd6a5e4 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
wenzelm
parents: 30552
diff changeset
    32
      Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
20301
66b2a1f16bbb Variable.focus_subgoal;
wenzelm
parents: 20231
diff changeset
    33
    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    34
    val asms = Drule.strip_imp_prems goal;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    35
    val concl = Drule.strip_imp_concl goal;
20231
dcdd565a7fbe tuned interfaces;
wenzelm
parents: 20219
diff changeset
    36
    val (prems, context) = Assumption.add_assumes asms ctxt'';
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    37
  in
20219
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    38
    ({context = context, schematics = schematics, params = params,
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    39
      asms = asms, concl = concl, prems = prems}, Goal.init concl)
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    40
  end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    41
20231
dcdd565a7fbe tuned interfaces;
wenzelm
parents: 20219
diff changeset
    42
fun SUBPROOF tac ctxt i st =
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    43
  if Thm.nprems_of st < i then Seq.empty
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    44
  else
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    45
    let
20219
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    46
      val (args as {context, params, ...}, st') = focus ctxt i st;
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    47
      fun export_closed th =
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    48
        let
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    49
          val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
20579
4dc799edef89 Thm.dest_arg;
wenzelm
parents: 20301
diff changeset
    50
          val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
20219
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    51
        in Drule.forall_intr_list vs th' end;
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    52
      fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
3bff4719f3d6 focus: result record includes (fixed) schematic variables;
wenzelm
parents: 20210
diff changeset
    53
    in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    54
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    55
end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    56
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    57
structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    58
open BasicSubgoal;