src/Pure/subgoal.ML
changeset 32281 750101435f60
parent 32213 f1b166317ae2
child 32283 3bebc195c124
     1.1 --- a/src/Pure/subgoal.ML	Thu Jul 30 01:14:40 2009 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Thu Jul 30 11:23:17 2009 +0200
     1.3 @@ -1,20 +1,23 @@
     1.4  (*  Title:      Pure/subgoal.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Tactical operations with explicit subgoal focus, based on
     1.8 -canonical proof decomposition (similar to fix/assume/show).
     1.9 +Tactical operations with explicit subgoal focus, based on canonical
    1.10 +proof decomposition.  The "visible" part of the text within the
    1.11 +context is fixed, the remaining goal may be schematic.
    1.12  *)
    1.13  
    1.14  signature SUBGOAL =
    1.15  sig
    1.16    type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    1.17 -    asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
    1.18 +    asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
    1.19 +  val focus_params: Proof.context -> int -> thm -> focus * thm
    1.20 +  val focus_prems: Proof.context -> int -> thm -> focus * thm
    1.21    val focus: Proof.context -> int -> thm -> focus * thm
    1.22 -  val focus_params: Proof.context -> int -> thm -> focus * thm
    1.23    val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
    1.24      int -> thm -> thm -> thm Seq.seq
    1.25 +  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.26 +  val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.27    val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.28 -  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.29    val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
    1.30  end;
    1.31  
    1.32 @@ -24,24 +27,35 @@
    1.33  (* focus *)
    1.34  
    1.35  type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
    1.36 -  asms: cterm list, concl: cterm, schematics: ctyp list * cterm list};
    1.37 +  asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
    1.38  
    1.39 -fun gen_focus params_only ctxt i st =
    1.40 +fun gen_focus (do_prems, do_concl) ctxt i raw_st =
    1.41    let
    1.42 -    val ((schematics, [st']), ctxt') =
    1.43 -      Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
    1.44 -    val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
    1.45 +    val st = Simplifier.norm_hhf_protect raw_st;
    1.46 +    val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
    1.47 +    val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1;
    1.48 +
    1.49      val (asms, concl) =
    1.50 -      if params_only then ([], goal)
    1.51 -      else (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal);
    1.52 -    val (prems, context) = Assumption.add_assumes asms ctxt'';
    1.53 +      if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
    1.54 +      else ([], goal);
    1.55 +    val text = asms @ (if do_concl then [concl] else []);
    1.56 +
    1.57 +    val ((_, schematic_terms), ctxt3) =
    1.58 +      Variable.import_inst true (map Thm.term_of text) ctxt2
    1.59 +      |>> Thm.certify_inst (Thm.theory_of_thm raw_st);
    1.60 +
    1.61 +    val schematics = (schematic_types, schematic_terms);
    1.62 +    val asms' = map (Thm.instantiate_cterm schematics) asms;
    1.63 +    val concl' = Thm.instantiate_cterm schematics concl;
    1.64 +    val (prems, context) = Assumption.add_assumes asms' ctxt3;
    1.65    in
    1.66      ({context = context, params = params, prems = prems,
    1.67 -      asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
    1.68 +      asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
    1.69    end;
    1.70  
    1.71 -val focus = gen_focus false;
    1.72 -val focus_params = gen_focus true;
    1.73 +val focus_params = gen_focus (false, false);
    1.74 +val focus_prems = gen_focus (true, false);
    1.75 +val focus = gen_focus (true, true);
    1.76  
    1.77  
    1.78  (* lift and retrofit *)
    1.79 @@ -53,27 +67,29 @@
    1.80  *)
    1.81  fun lift_import params th ctxt =
    1.82    let
    1.83 -    val cert = Thm.cterm_of (Thm.theory_of_thm th);
    1.84      val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    1.85  
    1.86      val Ts = map (#T o Thm.rep_cterm) params;
    1.87      val ts = map Thm.term_of params;
    1.88  
    1.89 -    val vars = rev (Term.add_vars (Thm.full_prop_of th') []);
    1.90 +    val prop = Thm.full_prop_of th';
    1.91 +    val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
    1.92 +    val vars = rev (Term.add_vars prop []);
    1.93      val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
    1.94      fun var_inst (v as (_, T)) y =
    1.95 -      (cert (Var v), cert (list_comb (Free (y, Ts ---> T), ts)));
    1.96 -    val th'' = Thm.instantiate ([], map2 var_inst vars ys) th';
    1.97 +      if member (op =) concl_vars v then (v, Free (y, T))
    1.98 +      else (v, list_comb (Free (y, Ts ---> T), ts));
    1.99 +    val th'' = Thm.certify_instantiate ([], map2 var_inst vars ys) th';
   1.100    in (th'', ctxt'') end;
   1.101  
   1.102  (*
   1.103 -      [x, A x]
   1.104 +       [x, A x]
   1.105            :
   1.106 -      B x ==> C
   1.107 +       B x ==> C
   1.108    ------------------
   1.109    [!!x. A x ==> B x]
   1.110 -         :
   1.111 -         C
   1.112 +          :
   1.113 +          C
   1.114  *)
   1.115  fun lift_subgoals params asms th =
   1.116    let
   1.117 @@ -103,20 +119,22 @@
   1.118  
   1.119  (* tacticals *)
   1.120  
   1.121 -fun GEN_FOCUS params_only tac ctxt i st =
   1.122 +fun GEN_FOCUS flags tac ctxt i st =
   1.123    if Thm.nprems_of st < i then Seq.empty
   1.124    else
   1.125 -    let val (args as {context, params, asms, ...}, st') = gen_focus params_only ctxt i st;
   1.126 +    let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st;
   1.127      in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
   1.128  
   1.129 -val FOCUS = GEN_FOCUS false;
   1.130 -val FOCUS_PARAMS = GEN_FOCUS true;
   1.131 +val FOCUS_PARAMS = GEN_FOCUS (false, false);
   1.132 +val FOCUS_PREMS = GEN_FOCUS (true, false);
   1.133 +val FOCUS = GEN_FOCUS (true, true);
   1.134  
   1.135  fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
   1.136  
   1.137  end;
   1.138  
   1.139 +val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
   1.140 +val FOCUS_PREMS = Subgoal.FOCUS_PREMS;
   1.141  val FOCUS = Subgoal.FOCUS;
   1.142 -val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
   1.143  val SUBPROOF = Subgoal.SUBPROOF;
   1.144