src/Pure/subgoal.ML
author wenzelm
Thu Jul 30 11:23:17 2009 +0200 (2009-07-30)
changeset 32281 750101435f60
parent 32213 f1b166317ae2
child 32283 3bebc195c124
permissions -rw-r--r--
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
added FOCUS_PREMS, which may serve as full replacement for OldGoals.METAHYPS;
     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 raw_st;
    35     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
    36     val ((params, goal), ctxt2) = Variable.focus (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 params th ctxt =
    69   let
    70     val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    71 
    72     val Ts = map (#T o Thm.rep_cterm) params;
    73     val ts = map Thm.term_of params;
    74 
    75     val prop = Thm.full_prop_of th';
    76     val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
    77     val vars = rev (Term.add_vars prop []);
    78     val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
    79     fun var_inst (v as (_, T)) y =
    80       if member (op =) concl_vars v then (v, Free (y, T))
    81       else (v, list_comb (Free (y, Ts ---> T), ts));
    82     val th'' = Thm.certify_instantiate ([], map2 var_inst vars ys) th';
    83   in (th'', ctxt'') end;
    84 
    85 (*
    86        [x, A x]
    87           :
    88        B x ==> C
    89   ------------------
    90   [!!x. A x ==> B x]
    91           :
    92           C
    93 *)
    94 fun lift_subgoals params asms th =
    95   let
    96     val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms;
    97     val unlift =
    98       fold (Thm.elim_implies o Thm.assume) asms o
    99       Drule.forall_elim_list (map #2 params) o Thm.assume;
   100     val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
   101     val th' = fold (Thm.elim_implies o unlift) subgoals th;
   102   in (subgoals, th') end;
   103 
   104 fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
   105   let
   106     val ps = map #2 params;
   107     val (st2, ctxt2) = lift_import ps st1 ctxt1;
   108     val (subgoals, st3) = lift_subgoals params asms st2;
   109     val result = st3
   110       |> Goal.conclude
   111       |> Drule.implies_intr_list asms
   112       |> Drule.forall_intr_list ps
   113       |> Drule.implies_intr_list subgoals
   114       |> singleton (Variable.export ctxt2 ctxt0)
   115       |> Drule.zero_var_indexes
   116       |> Drule.incr_indexes st0;
   117   in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
   118 
   119 
   120 (* tacticals *)
   121 
   122 fun GEN_FOCUS flags tac ctxt i st =
   123   if Thm.nprems_of st < i then Seq.empty
   124   else
   125     let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st;
   126     in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
   127 
   128 val FOCUS_PARAMS = GEN_FOCUS (false, false);
   129 val FOCUS_PREMS = GEN_FOCUS (true, false);
   130 val FOCUS = GEN_FOCUS (true, true);
   131 
   132 fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
   133 
   134 end;
   135 
   136 val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
   137 val FOCUS_PREMS = Subgoal.FOCUS_PREMS;
   138 val FOCUS = Subgoal.FOCUS;
   139 val SUBPROOF = Subgoal.SUBPROOF;
   140