Is it possible to "free" top-level universally quantified variables using tactics in Isabelle?

Question

In short, I would like to go from this:

 proof (prove)
 goal (1 subgoal):
  1. ⋀ myVar . somePredicate myVar

to this:

 proof (prove)
 goal (1 subgoal):
  1. somePredicate myVar

by using tactics. The only solution I can find is to write a new lemma for example:

 lemma myPredicateHolds_aux : "somePredicate myVar"
   sorry

and then the original ⋀ myVar . somePredicate myVar usually can be solved by writing:

 using myPredicateHolds_aux by blast

but I wonder whether there is a better way (using tactics), for convenience, and because, if the property is very intricate, blast may fail.

Answer 1

The proof (prove) suggests you're writing a proof script, in which case you can use subgoal for myVar. The "isar-ref" manual says a little more about it, I think (though it may be a bit dense).

You can also, and I believe this is usually the "preferred" way to do it, go into structured Isar proof mode and use fix:

proof -
  fix myVar
  show "somePredicate myVar"
  proof ...