src/Pure/subgoal.ML
author blanchet
Wed, 03 Nov 2010 22:33:23 +0100
changeset 40342 3154f63e2bda
parent 34075 451b0c8a15cf
child 42360 da8817d01e7c
permissions -rw-r--r--
don't be overly verbose in Sledgehammer's minimizer
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
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
     4
Tactical operations with explicit subgoal focus, based on canonical
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
     5
proof decomposition.  The "visible" part of the text within the
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
     6
context is fixed, the remaining goal may be schematic.
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     7
*)
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     8
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
     9
signature SUBGOAL =
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    10
sig
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    11
  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    12
    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    13
  val focus_params: Proof.context -> int -> thm -> focus * thm
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    14
  val focus_prems: Proof.context -> int -> thm -> focus * thm
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    15
  val focus: Proof.context -> int -> thm -> focus * thm
32210
a5e9d9f3e5e1 retrofit: actually handle schematic variables -- need to export into original context;
wenzelm
parents: 32200
diff changeset
    16
  val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    17
    int -> thm -> thm -> thm Seq.seq
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    18
  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    19
  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    20
  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    21
  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
20210
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
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    27
(* focus *)
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    28
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    29
type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    30
  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    31
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    32
fun gen_focus (do_prems, do_concl) ctxt i raw_st =
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    33
  let
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    34
    val st = Simplifier.norm_hhf_protect raw_st;
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    35
    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    36
    val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    37
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
    38
    val (asms, concl) =
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    39
      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    40
      else ([], goal);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    41
    val text = asms @ (if do_concl then [concl] else []);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    42
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    43
    val ((_, schematic_terms), ctxt3) =
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    44
      Variable.import_inst true (map Thm.term_of text) ctxt2
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    45
      |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    46
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    47
    val schematics = (schematic_types, schematic_terms);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    48
    val asms' = map (Thm.instantiate_cterm schematics) asms;
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    49
    val concl' = Thm.instantiate_cterm schematics concl;
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    50
    val (prems, context) = Assumption.add_assumes asms' ctxt3;
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    51
  in
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    52
    ({context = context, params = params, prems = prems,
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    53
      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    54
  end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
    55
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    56
val focus_params = gen_focus (false, false);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    57
val focus_prems = gen_focus (true, false);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    58
val focus = gen_focus (true, true);
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
    59
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    60
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    61
(* lift and retrofit *)
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    62
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    63
(*
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    64
     B [?'b, ?y]
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    65
  ----------------
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    66
  B ['b, y params]
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    67
*)
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    68
fun lift_import idx params th ctxt =
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    69
  let
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    70
    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    71
    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    72
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    73
    val Ts = map (#T o Thm.rep_cterm) params;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    74
    val ts = map Thm.term_of params;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    75
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    76
    val prop = Thm.full_prop_of th';
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    77
    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    78
    val vars = rev (Term.add_vars prop []);
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    79
    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    80
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    81
    fun var_inst v y =
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    82
      let
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    83
        val ((x, i), T) = v;
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    84
        val (U, args) =
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    85
          if member (op =) concl_vars v then (T, [])
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    86
          else (Ts ---> T, ts);
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    87
        val u = Free (y, U);
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    88
        in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    89
    val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys));
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    90
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    91
    val th'' = Thm.instantiate ([], inst1) th';
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
    92
  in ((inst2, th''), ctxt'') end;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    93
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    94
(*
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    95
       [x, A x]
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    96
          :
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
    97
       B x ==> C
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    98
  ------------------
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
    99
  [!!x. A x ==> B x]
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   100
          :
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   101
          C
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   102
*)
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   103
fun lift_subgoals params asms th =
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   104
  let
32329
1527ff8c2dfb SUBPROOF: recovered Goal.check_finished;
wenzelm
parents: 32284
diff changeset
   105
    fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   106
    val unlift =
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   107
      fold (Thm.elim_implies o Thm.assume) asms o
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   108
      Drule.forall_elim_list (map #2 params) o Thm.assume;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   109
    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   110
    val th' = fold (Thm.elim_implies o unlift) subgoals th;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   111
  in (subgoals, th') end;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   112
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   113
fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   114
  let
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   115
    val idx = Thm.maxidx_of st0 + 1;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   116
    val ps = map #2 params;
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   117
    val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   118
    val (subgoals, st3) = lift_subgoals params asms st2;
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   119
    val result = st3
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   120
      |> Goal.conclude
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   121
      |> Drule.implies_intr_list asms
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   122
      |> Drule.forall_intr_list ps
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   123
      |> Drule.implies_intr_list subgoals
32284
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   124
      |> fold_rev (Thm.forall_intr o #1) subgoal_inst
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   125
      |> fold (Thm.forall_elim o #2) subgoal_inst
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   126
      |> Thm.adjust_maxidx_thm idx
d8ee8a956f19 retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents: 32283
diff changeset
   127
      |> singleton (Variable.export ctxt2 ctxt0);
34075
451b0c8a15cf Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
wenzelm
parents: 32329
diff changeset
   128
  in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   129
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   130
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   131
(* tacticals *)
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   132
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   133
fun GEN_FOCUS flags tac ctxt i st =
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   134
  if Thm.nprems_of st < i then Seq.empty
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   135
  else
32329
1527ff8c2dfb SUBPROOF: recovered Goal.check_finished;
wenzelm
parents: 32284
diff changeset
   136
    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
1527ff8c2dfb SUBPROOF: recovered Goal.check_finished;
wenzelm
parents: 32284
diff changeset
   137
    in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   138
32281
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   139
val FOCUS_PARAMS = GEN_FOCUS (false, false);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   140
val FOCUS_PREMS = GEN_FOCUS (true, false);
750101435f60 focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents: 32213
diff changeset
   141
val FOCUS = GEN_FOCUS (true, true);
32213
f1b166317ae2 added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents: 32210
diff changeset
   142
32329
1527ff8c2dfb SUBPROOF: recovered Goal.check_finished;
wenzelm
parents: 32284
diff changeset
   143
fun SUBPROOF tac ctxt = FOCUS (Seq.map (tap (Goal.check_finished ctxt)) oo tac) ctxt;
20210
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   144
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   145
end;
8fe4ae4360eb Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff changeset
   146
32200
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   147
val SUBPROOF = Subgoal.SUBPROOF;
2bd8ab91a426 advanced retrofit, which allows new subgoals and variables;
wenzelm
parents: 31794
diff changeset
   148