src/Pure/goal.ML
changeset 19184 3e30297e1300
parent 18678 dd0c569fa43d
child 19191 56cda3ec2ef8
     1.1 --- a/src/Pure/goal.ML	Sat Mar 04 21:10:07 2006 +0100
     1.2 +++ b/src/Pure/goal.ML	Sat Mar 04 21:10:08 2006 +0100
     1.3 @@ -26,6 +26,8 @@
     1.4      (thm list -> tactic) -> thm list
     1.5    val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
     1.6    val prove_raw: cterm list -> cterm -> (thm list -> tactic) -> thm
     1.7 +  val extract: int -> int -> thm -> thm Seq.seq
     1.8 +  val retrofit: int -> int -> thm -> thm -> thm Seq.seq
     1.9  end;
    1.10  
    1.11  structure Goal: GOAL =
    1.12 @@ -168,30 +170,23 @@
    1.13    | NONE => error "Tactic failed.");
    1.14  
    1.15  
    1.16 -(* SELECT_GOAL *)
    1.17  
    1.18 -(*Tactical for restricting the effect of a tactic to subgoal i.  Works
    1.19 -  by making a new state from subgoal i, applying tac to it, and
    1.20 -  composing the resulting thm with the original state.*)
    1.21 -
    1.22 -local
    1.23 +(** local goal states **)
    1.24  
    1.25 -fun SELECT tac i st =
    1.26 -  init (Thm.adjust_maxidx (Thm.cprem_of st i))
    1.27 -  |> tac
    1.28 -  |> Seq.maps (fn st' =>
    1.29 -    Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i st);
    1.30 +fun extract i n st =
    1.31 +  (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    1.32 +   else if n = 1 then Seq.single (Thm.cprem_of st i)
    1.33 +   else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
    1.34 +  |> Seq.map (Thm.adjust_maxidx #> init);
    1.35  
    1.36 -in
    1.37 +fun retrofit i n st' =
    1.38 +  (if n = 1 then I
    1.39 +   else Drule.rotate_prems (i - 1) #> Drule.conj_uncurry n #> Drule.rotate_prems (1 - i))
    1.40 +  #> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
    1.41  
    1.42  fun SELECT_GOAL tac i st =
    1.43 -  let val n = Thm.nprems_of st in
    1.44 -    if 1 <= i andalso i <= n then
    1.45 -      if n = 1 then tac st else SELECT tac i st
    1.46 -    else Seq.empty
    1.47 -  end;
    1.48 -
    1.49 -end;
    1.50 +  if Thm.nprems_of st = 1 then tac st
    1.51 +  else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
    1.52  
    1.53  end;
    1.54