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
```