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