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