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