Is there a way to convert free variables to (meta) universally quantified variables in Isabelle?

Question

Universally quantified variables are the same as free variables in the following two lemmas from the Isabelle (2021) tutorial section 8.1.2 (with slight changes on the second one):

Given

primrec swap::"'a × 'a ⇒ 'a × 'a" where "swap (x, y) = (y, x)"

the lemma:

lemma "swap (swap p) = p"

is equivalent to:

lemma "⋀ p. swap (swap p) = p"

However, certain tactics/rules (such as apply (simp only:split_paired_all) used in that section) only work on a goal if it's stated with universal quantification using \<And> (and not in the free form).

My question is:

Is there an idiomatic way to convert the first goal to the second goal during a proof, and vice versa from lemma 2 to lemma 1?

That is, while proving lemma 1, is it possible to convert the subgoal to the quantified form of lemma 2, and then use whatever methods that work for lemma 2 to prove lemma 1 (and vice versa)?

(I originally posted this question in SO, but didn't get a definitive answer. So I am deleting the question there and posting it here for more attention.)

Answer 1

My question is:

Is there an idiomatic way to convert the first goal to the second goal during a proof, and vice versa from lemma 2 to lemma 1?

Yes, there is.

lemma "swap (swap p) = p"
  apply(Pure.rule meta_spec[where x=p])
  apply(simp only:split_paired_all)
  oops

lemma "⋀p. swap (swap p) = p" 
  subgoal for p by (cases p) simp
  done

However, overall, I prefer the methodology suggested by Pedro Sánchez Terraf in another answer for solving goals of the type swap (swap p) = p.

Answer 2

You should first note that the tutorial you're reading is in the “Old” documentation section and thus the style of the proofs is a bit dated. For instance, they would seem to recommend

lemma "swap(swap p) = p"
apply(case_tac p)
apply(simp)
done

whereas the modern way to write this would be something like this:

lemma "swap(swap p) = p"
  by (cases p) simp

In the same declarative spirit, if you try to prove the same lemma and insist to use split_paired_all, you would state what you prove and then say that your goal follows from that:

lemma "swap(swap p) = p"
proof -
  have "⋀p. swap(swap p) = p"
    by (simp add:split_paired_all)
  then
  show ?thesis .
qed

Above, ?thesis is a variable that holds your main goal, and the period after it is a trivial proof (that handles equivalent goals in the sense you state above). Finally, note that the proof command takes an opening, “initial” method that you want to apply to your goals. In this case, - corresponds to doing nothing.