Convert an Isar proof of forall-statement to apply-style

Question

I'm trying to build a very short proof for a given fact. I would like to just use apply-style commands. Now my theorem's structure looks like this:

theorem 
  statement
  apply(some commands)
  proof -
    fix t assume "some predicate"
    from some assumptions "some_theorem"
    by(some commands)  
  qed

So, if I want to do my proof minimal, I should really attack the lines:

fix t assume "some predicate"
from some assumptions "some_theorem"

which is basically implementing the proof of a forall statement:

⋀ param. A ⟹ B

My question is is there a hack that will let me encode the proof of such an statement in apply-style instead of Isar proof language?

There is a way using subgoal for param, but this cannot be combined with apply, is there a command to combine it with apply? — user1868607
Why can you not use subgoal in an apply script, e.g. subgoal for x? Also, see section 2.3.6 in 'The Isabelle/Isar Reference Manual'. — user9716869 - supports Ukraine
@xanonec i mean you can, but you cannot write apply( command ; subgoal for x ; command ; ...) which would save me some tokens (i need the shortest proof) — user1868607