Is there a way to do multiple apply (erule_tac x=... in allE) at once? Sometimes, when I have multiple forall in my assumptions, Isabelle reorders them after an erule_tac, which makes proving very annoying.
Eg.
lemma "forall x y. P x y ==> P a b"
apply (erule_tac x=a in allE)
apply (erule_tac x=b in allE) (* how can I do these two rules in one rule *)?
done
To the specific question, allE has only one x, so you can't do multiple instantiations at once.
The way there would be to manually introduce a lemma all2E: ‹∀x y. P x y ⟹ (P x y ⟹ R) ⟹ R› by blast.
Then, you can write apply (erule_tac x=a and y=b in all2E) in your proof.
(Alternatively, there's a HOL lemma spec2 close to what we need in this instance.)
Usually, the convenient and stable way to instantiate multiple variables in a proof step is to use the [of ...] modifier-attribute on facts instead of rule_tac.
This would read apply (erule all2E[of _ a b]) in this instance.
(In the minimal example, one can also leave out the instantiations. Isabelle will find them to finish the proof.)
For cleaner proofs, I generally prefer to have my assumptions and facts named and instantiate the variables on them (and not on the the rules as above). In this example, this would read:
lemma
assumes P_univ: ‹∀ x y. P x y›
shows ‹P a b›
using P_univ[rule_format, of a b] .
(The [rule_format] is needed to turn x,y into meta variables, which can be instantiated at the outer level.)