src/Pure/subgoal.ML
author wenzelm
Sun Jul 26 13:12:54 2009 +0200 (2009-07-26)
changeset 32200 2bd8ab91a426
parent 31794 71af1fd6a5e4
child 32210 a5e9d9f3e5e1
permissions -rw-r--r--
advanced retrofit, which allows new subgoals and variables;
added FOCUS -- does not require closed proof;
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@32200
    13
  val retrofit: Proof.context -> (string * cterm) list -> cterm list ->
wenzelm@32200
    14
    int -> thm -> thm -> thm Seq.seq
wenzelm@32200
    15
  val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@32200
    16
  val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
wenzelm@20210
    17
end;
wenzelm@20210
    18
wenzelm@20210
    19
structure Subgoal: SUBGOAL =
wenzelm@20210
    20
struct
wenzelm@20210
    21
wenzelm@32200
    22
(* focus *)
wenzelm@32200
    23
wenzelm@32200
    24
type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
wenzelm@32200
    25
  asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
wenzelm@20210
    26
wenzelm@20210
    27
fun focus ctxt i st =
wenzelm@20210
    28
  let
wenzelm@21605
    29
    val ((schematics, [st']), ctxt') =
wenzelm@31794
    30
      Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
wenzelm@20301
    31
    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
wenzelm@20210
    32
    val asms = Drule.strip_imp_prems goal;
wenzelm@20210
    33
    val concl = Drule.strip_imp_concl goal;
wenzelm@20231
    34
    val (prems, context) = Assumption.add_assumes asms ctxt'';
wenzelm@20210
    35
  in
wenzelm@32200
    36
    ({context = context, params = params, prems = prems,
wenzelm@32200
    37
      asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
wenzelm@20210
    38
  end;
wenzelm@20210
    39
wenzelm@32200
    40
wenzelm@32200
    41
(* lift and retrofit *)
wenzelm@32200
    42
wenzelm@32200
    43
(*
wenzelm@32200
    44
     B [?'b, ?y]
wenzelm@32200
    45
  ----------------
wenzelm@32200
    46
  B ['b, y params]
wenzelm@32200
    47
*)
wenzelm@32200
    48
fun lift_import params th ctxt =
wenzelm@32200
    49
  let
wenzelm@32200
    50
    val cert = Thm.cterm_of (Thm.theory_of_thm th);
wenzelm@32200
    51
    val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
wenzelm@32200
    52
wenzelm@32200
    53
    val Ts = map (#T o Thm.rep_cterm) params;
wenzelm@32200
    54
    val ts = map Thm.term_of params;
wenzelm@32200
    55
wenzelm@32200
    56
    val vars = rev (Term.add_vars (Thm.full_prop_of th') []);
wenzelm@32200
    57
    val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
wenzelm@32200
    58
    fun var_inst (v as (_, T)) y =
wenzelm@32200
    59
      (cert (Var v), cert (list_comb (Free (y, Ts ---> T), ts)));
wenzelm@32200
    60
    val th'' = Thm.instantiate ([], map2 var_inst vars ys) th';
wenzelm@32200
    61
  in (th'', ctxt'') end;
wenzelm@32200
    62
wenzelm@32200
    63
(*
wenzelm@32200
    64
        [A x]
wenzelm@32200
    65
          :
wenzelm@32200
    66
      B x ==> C
wenzelm@32200
    67
  ------------------
wenzelm@32200
    68
  [!!x. A x ==> B x]
wenzelm@32200
    69
         :
wenzelm@32200
    70
         C
wenzelm@32200
    71
*)
wenzelm@32200
    72
fun lift_subgoals params asms th =
wenzelm@32200
    73
  let
wenzelm@32200
    74
    val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms;
wenzelm@32200
    75
    val unlift =
wenzelm@32200
    76
      fold (Thm.elim_implies o Thm.assume) asms o
wenzelm@32200
    77
      Drule.forall_elim_list (map #2 params) o Thm.assume;
wenzelm@32200
    78
    val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
wenzelm@32200
    79
    val th' = fold (Thm.elim_implies o unlift) subgoals th;
wenzelm@32200
    80
  in (subgoals, th') end;
wenzelm@32200
    81
wenzelm@32200
    82
fun retrofit ctxt params asms i th =
wenzelm@32200
    83
  let
wenzelm@32200
    84
    val ps = map #2 params;
wenzelm@32200
    85
    val res0 = Goal.conclude th;
wenzelm@32200
    86
    val (res1, ctxt1) = lift_import ps res0 ctxt;
wenzelm@32200
    87
    val (subgoals, res2) = lift_subgoals params asms res1;
wenzelm@32200
    88
    val result = res2
wenzelm@32200
    89
      |> Drule.implies_intr_list asms
wenzelm@32200
    90
      |> Drule.forall_intr_list ps
wenzelm@32200
    91
      |> Drule.implies_intr_list subgoals
wenzelm@32200
    92
      |> singleton (Variable.export ctxt1 ctxt);
wenzelm@32200
    93
  in Thm.compose_no_flatten false (result, Thm.nprems_of res0) i end;
wenzelm@32200
    94
wenzelm@32200
    95
wenzelm@32200
    96
(* tacticals *)
wenzelm@32200
    97
wenzelm@32200
    98
fun FOCUS tac ctxt i st =
wenzelm@20210
    99
  if Thm.nprems_of st < i then Seq.empty
wenzelm@20210
   100
  else
wenzelm@32200
   101
    let val (args as {context, params, asms, ...}, st') = focus ctxt i st;
wenzelm@32200
   102
    in Seq.lifts (retrofit context params asms i) (tac args st') st end;
wenzelm@32200
   103
wenzelm@32200
   104
fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
wenzelm@20210
   105
wenzelm@20210
   106
end;
wenzelm@20210
   107
wenzelm@32200
   108
val FOCUS = Subgoal.FOCUS;
wenzelm@32200
   109
val SUBPROOF = Subgoal.SUBPROOF;
wenzelm@32200
   110