added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
authorwenzelm
Sun Jul 26 20:57:19 2009 +0200 (2009-07-26)
changeset 32213f1b166317ae2
parent 32212 21d7b4524395
child 32214 6a6827bad05f
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
src/Pure/subgoal.ML
     1.1 --- a/src/Pure/subgoal.ML	Sun Jul 26 20:38:11 2009 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Sun Jul 26 20:57:19 2009 +0200
     1.3 @@ -10,9 +10,11 @@
     1.4    type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
     1.5      asms: cterm list, concl: cterm, schematics: ctyp list * cterm list}
     1.6    val focus: Proof.context -> int -> thm -> focus * thm
     1.7 +  val focus_params: Proof.context -> int -> thm -> focus * thm
     1.8    val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
     1.9      int -> thm -> thm -> thm Seq.seq
    1.10    val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.11 +  val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
    1.12    val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
    1.13  end;
    1.14  
    1.15 @@ -24,19 +26,23 @@
    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  
    1.19 -fun focus ctxt i st =
    1.20 +fun gen_focus params_only ctxt i st =
    1.21    let
    1.22      val ((schematics, [st']), ctxt') =
    1.23        Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
    1.24      val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
    1.25 -    val asms = Drule.strip_imp_prems goal;
    1.26 -    val concl = Drule.strip_imp_concl goal;
    1.27 +    val (asms, concl) =
    1.28 +      if params_only then ([], goal)
    1.29 +      else (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal);
    1.30      val (prems, context) = Assumption.add_assumes asms ctxt'';
    1.31    in
    1.32      ({context = context, params = params, prems = prems,
    1.33        asms = asms, concl = concl, schematics = schematics}, Goal.init concl)
    1.34    end;
    1.35  
    1.36 +val focus = gen_focus false;
    1.37 +val focus_params = gen_focus true;
    1.38 +
    1.39  
    1.40  (* lift and retrofit *)
    1.41  
    1.42 @@ -61,7 +67,7 @@
    1.43    in (th'', ctxt'') end;
    1.44  
    1.45  (*
    1.46 -        [A x]
    1.47 +      [x, A x]
    1.48            :
    1.49        B x ==> C
    1.50    ------------------
    1.51 @@ -79,34 +85,38 @@
    1.52      val th' = fold (Thm.elim_implies o unlift) subgoals th;
    1.53    in (subgoals, th') end;
    1.54  
    1.55 -fun retrofit ctxt1 ctxt0 params asms i state1 state0 =
    1.56 +fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
    1.57    let
    1.58      val ps = map #2 params;
    1.59 -    val res = Goal.conclude state1;
    1.60 -    val (res1, ctxt2) = lift_import ps res ctxt1;
    1.61 -    val (subgoals, res2) = lift_subgoals params asms res1;
    1.62 -    val result = res2
    1.63 +    val (st2, ctxt2) = lift_import ps st1 ctxt1;
    1.64 +    val (subgoals, st3) = lift_subgoals params asms st2;
    1.65 +    val result = st3
    1.66 +      |> Goal.conclude
    1.67        |> Drule.implies_intr_list asms
    1.68        |> Drule.forall_intr_list ps
    1.69        |> Drule.implies_intr_list subgoals
    1.70        |> singleton (Variable.export ctxt2 ctxt0)
    1.71        |> Drule.zero_var_indexes
    1.72 -      |> Drule.incr_indexes state0;
    1.73 -  in Thm.compose_no_flatten false (result, Thm.nprems_of state1) i state0 end;
    1.74 +      |> Drule.incr_indexes st0;
    1.75 +  in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end;
    1.76  
    1.77  
    1.78  (* tacticals *)
    1.79  
    1.80 -fun FOCUS tac ctxt i st =
    1.81 +fun GEN_FOCUS params_only tac ctxt i st =
    1.82    if Thm.nprems_of st < i then Seq.empty
    1.83    else
    1.84 -    let val (args as {context, params, asms, ...}, st') = focus ctxt i st;
    1.85 +    let val (args as {context, params, asms, ...}, st') = gen_focus params_only ctxt i st;
    1.86      in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end;
    1.87  
    1.88 +val FOCUS = GEN_FOCUS false;
    1.89 +val FOCUS_PARAMS = GEN_FOCUS true;
    1.90 +
    1.91  fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac);
    1.92  
    1.93  end;
    1.94  
    1.95  val FOCUS = Subgoal.FOCUS;
    1.96 +val FOCUS_PARAMS = Subgoal.FOCUS_PARAMS;
    1.97  val SUBPROOF = Subgoal.SUBPROOF;
    1.98