src/Pure/subgoal.ML
author wenzelm
Sun Jul 26 20:57:19 2009 +0200 (2009-07-26)
changeset 32213 f1b166317ae2
parent 32210 a5e9d9f3e5e1
child 32281 750101435f60
permissions -rw-r--r--
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm@20210
     1
(*  Title:      Pure/subgoal.ML
wenzelm@20210
     2
    Author:     Makarius
wenzelm@20210
     3
wenzelm@32200
     4
Tactical operations with explicit subgoal focus, based on
wenzelm@32200
     5
canonical proof decomposition (similar to fix/assume/show).
wenzelm@20210
     6
*)
wenzelm@20210
     7
wenzelm@20210
     8
signature SUBGOAL =
wenzelm@20210
     9
sig
wenzelm@32200
    10
  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
wenzelm@32200
    11
    asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
wenzelm@32200
    12
  val focus: Proof.context -> int -> thm -> focus * thm
wenzelm@32213
    13
  val focus_params: Proof.context -> int -> thm -> focus * thm
wenzelm@32210
    14
  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
wenzelm@32200
    15
    int -> thm -> thm -> thm Seq.seq
wenzelm@32200
    16
  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@32213
    17
  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@32200
    18
  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@20210
    19
end;
wenzelm@20210
    20
wenzelm@20210
    21
structure Subgoal: SUBGOAL =
wenzelm@20210
    22
struct
wenzelm@20210
    23
wenzelm@32200
    24
(* focus *)
wenzelm@32200
    25
wenzelm@32200
    26
type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
wenzelm@32200
    27
  asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
wenzelm@20210
    28
wenzelm@32213
    29
fun gen_focus params_only ctxt i st =
wenzelm@20210
    30
  let
wenzelm@21605
    31
    val ((schematics, [st']), ctxt') =
wenzelm@31794
    32
      Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
wenzelm@20301
    33
    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
wenzelm@32213
    34
    val (asms, concl) =
wenzelm@32213
    35
      if params_only then ([], goal)
wenzelm@32213
    36
      else (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal);
wenzelm@20231
    37
    val (prems, context) = Assumption.add_assumes asms ctxt'';
wenzelm@20210
    38
  in
wenzelm@32200
    39
    ({context = context, params = params, prems = prems,
wenzelm@32200
    40
      asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
wenzelm@20210
    41
  end;
wenzelm@20210
    42
wenzelm@32213
    43
val focus = gen_focus false;
wenzelm@32213
    44
val focus_params = gen_focus true;
wenzelm@32213
    45
wenzelm@32200
    46
wenzelm@32200
    47
(* lift and retrofit *)
wenzelm@32200
    48
wenzelm@32200
    49
(*
wenzelm@32200
    50
     B [?'b, ?y]
wenzelm@32200
    51
  ----------------
wenzelm@32200
    52
  B ['b, y params]
wenzelm@32200
    53
*)
wenzelm@32200
    54
fun lift_import params th ctxt =
wenzelm@32200
    55
  let
wenzelm@32200
    56
    val cert = Thm.cterm_of (Thm.theory_of_thm th);
wenzelm@32200
    57
    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
wenzelm@32200
    58
wenzelm@32200
    59
    val Ts = map (#T o Thm.rep_cterm) params;
wenzelm@32200
    60
    val ts = map Thm.term_of params;
wenzelm@32200
    61
wenzelm@32200
    62
    val vars = rev (Term.add_vars (Thm.full_prop_of th') []);
wenzelm@32200
    63
    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
wenzelm@32200
    64
    fun var_inst (v as (_, T)) y =
wenzelm@32200
    65
      (cert (Var v), cert (list_comb (Free (y, Ts ---> T), ts)));
wenzelm@32200
    66
    val th'' = Thm.instantiate ([], map2 var_inst vars ys) th';
wenzelm@32200
    67
  in (th'', ctxt'') end;
wenzelm@32200
    68
wenzelm@32200
    69
(*
wenzelm@32213
    70
      [x, A x]
wenzelm@32200
    71
          :
wenzelm@32200
    72
      B x ==> C
wenzelm@32200
    73
  ------------------
wenzelm@32200
    74
  [!!x. A x ==> B x]
wenzelm@32200
    75
         :
wenzelm@32200
    76
         C
wenzelm@32200
    77
*)
wenzelm@32200
    78
fun lift_subgoals params asms th =
wenzelm@32200
    79
  let
wenzelm@32200
    80
    val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms;
wenzelm@32200
    81
    val unlift =
wenzelm@32200
    82
      fold (Thm.elim_implies o Thm.assume) asms o
wenzelm@32200
    83
      Drule.forall_elim_list (map #2 params) o Thm.assume;
wenzelm@32200
    84
    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
wenzelm@32200
    85
    val th' = fold (Thm.elim_implies o unlift) subgoals th;
wenzelm@32200
    86
  in (subgoals, th') end;
wenzelm@32200
    87
wenzelm@32213
    88
fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
wenzelm@32200
    89
  let
wenzelm@32200
    90
    val ps = map #2 params;
wenzelm@32213
    91
    val (st2, ctxt2) = lift_import ps st1 ctxt1;
wenzelm@32213
    92
    val (subgoals, st3) = lift_subgoals params asms st2;
wenzelm@32213
    93
    val result = st3
wenzelm@32213
    94
      |> Goal.conclude
wenzelm@32200
    95
      |> Drule.implies_intr_list asms
wenzelm@32200
    96
      |> Drule.forall_intr_list ps
wenzelm@32200
    97
      |> Drule.implies_intr_list subgoals
wenzelm@32210
    98
      |> singleton (Variable.export ctxt2 ctxt0)
wenzelm@32210
    99
      |> Drule.zero_var_indexes
wenzelm@32213
   100
      |> Drule.incr_indexes st0;
wenzelm@32213
   101
  in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
wenzelm@32200
   102
wenzelm@32200
   103
wenzelm@32200
   104
(* tacticals *)
wenzelm@32200
   105
wenzelm@32213
   106
fun GEN_FOCUS params_only tac ctxt i st =
wenzelm@20210
   107
  if Thm.nprems_of st < i then Seq.empty
wenzelm@20210
   108
  else
wenzelm@32213
   109
    let val (args as {context, params, asms, ...}, st') = gen_focus params_only ctxt i st;
wenzelm@32210
   110
    in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
wenzelm@32200
   111
wenzelm@32213
   112
val FOCUS = GEN_FOCUS false;
wenzelm@32213
   113
val FOCUS_PARAMS = GEN_FOCUS true;
wenzelm@32213
   114
wenzelm@32200
   115
fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
wenzelm@20210
   116
wenzelm@20210
   117
end;
wenzelm@20210
   118
wenzelm@32200
   119
val FOCUS = Subgoal.FOCUS;
wenzelm@32213
   120
val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
wenzelm@32200
   121
val SUBPROOF = Subgoal.SUBPROOF;
wenzelm@32200
   122