# Re: [isabelle] apply proof method to all subgoals

```You could use "intro":

apply (intro conjI allI impI)

which apply all introduction rules you give to it until no more is applicable.

Mathieu Giorgino

On Sunday 10 April 2011, Alex Katovsky wrote:
> This works very well in the example I gave, but it appears that
> sometimes "apply safe" can do more goal splitting than I want it to.
> For example, if "F" below is "x = y" where x and y are sets then "apply
> safe" will use set_eqI to generate these goals
>
> 1. ⋀x xa. ⟦E; xa ∈ x⟧ ⟹ xa ∈ y
> 2. ⋀x xa. ⟦E; xa ∈ y⟧ ⟹ xa ∈ x
>
> and in some instances it would be preferable to keep equality as the
> goal.  Is there some way that I can limit "apply safe", for example
> something like "apply (safe only: conjI allI impI)"?
>
> On 04/10/2011 01:50 PM, Lawrence Paulson wrote:
> > Probably you should try
> >
> > apply safe
> >
> > This performs all so-called safe inferences: those that cannot lead to
> > information loss.
> >
> > Larry Paulson
> >
> > On 10 Apr 2011, at 12:48, Alex Katovsky wrote:
> >> Hi,
> >>
> >> This is probably a very basic question, so I apologize if I'm not
> >> reading the tutorial carefully enough. I have this lemma
> >>
> >> lemma "(∀ x . A ⟶ B) ∧ (∀ y . C ⟶ D) ∧ (∀ x . E ⟶ F)"
> >>
> >> and from this I want to generate the three subgoals
> >>
> >> 1. ⋀x. A ⟹ B
> >> 2. ⋀y. C ⟹ D
> >> 3. ⋀x. E ⟹ F
> >>
> >> The only way I know how to do this at the moment is
> >>
> >> apply(rule conjI, rule_tac [2] conjI)
> >> apply(rule_tac [1] allI, rule_tac [2] allI, rule_tac [3] allI)
> >> apply(rule_tac [1] impI, rule_tac [2] impI, rule_tac [3] impI)
> >>
> >> What I would like to do is repeatedly apply "(rule conjI)|(rule
> >> allI)|(rule impI)" to all subgoals until no further progress can be