# Re: [isabelle] Method combinator ; restricts to first subgoal

```Hi Daniel,

On 05/06/15 07:23, Daniel Matichuk wrote:
```
```It's not really defined what it means for a subgoal to "arise" out of a method which applies to all subgoals.
In the general case a method can perform arbitrary modifications to the collection of subgoals
(including changing the number), and so the "new" subgoals would need to be all of them.
```
I see. My naive intuition was that new subgoals are those that are there but were not there before (and their relative order must be the same), but that is probably a bit too vague.
```
```
```One possible solution to your problem is to expose "ALLGOALS" as a method combinator. This can be done relatively easily with some
simple Eisbach-provided functionality (I didn't get around to including this in the release):

~~~
method_setup all =
âMethod_Closure.parse_method >> (fn m => fn ctxt => fn facts =>
let
fun tac i st' =
Goal.restrict i 1 st'
|> Method_Closure.method_evaluate m ctxt facts
|> Seq.map (Goal.unrestrict i o snd)

in EMPTY_CASES (ALLGOALS tac) end)
â

lemma
assumes B: B
shows
"A â (A â B)" "A â (A â B)" "A â (A â B)"
apply -
by (all âsafe; rule Bâ)
~~~
In this example, "safe" is executed in isolation against each subgoal, and "rule B" applied to each emerging one.
```
The all combinator is nice, thanks. Still, I am not really comfortable with it. I am used to auto and safe working on all goals. Now, if read something like
```
apply(auto intro: ... simp add: ... simp del: ...; blast elim: ...)

```
I am still tempted to think that it works on all subgoals, because the restriction operator ";" is well hidden between two method invocations (and visually not so much different from ",", which does not restrict auto). The restriction operator [3] added after the closing parenthesis is much easier to spot.
```
```
```As a side note, something like "(x; simp_all)" never makes sense, the second argument is run against each resulting subgoal in isolation.
You almost certainly mean "(x; simp)".
```
You are right, although I in fact have a few instances of "...; simp_all" in my code. This stems from transforming something like
```
apply(rule ...)
apply simp_all

into

apply(rule ...; simp_all)

I still have to get my head around to then change simp_all into simp.

Best,
Andreas

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.