8
$\begingroup$

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.)

$\endgroup$

2 Answers 2

6
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Your advice is good, but, in my view, it does not address the question that the OP is asking. $\endgroup$ Feb 15, 2022 at 18:47
  • $\begingroup$ @user9716869 Thanks for your sharing your view. Indeed, I was about to comment that surely there was a lower-level way to do this, but I thought it better to offer a change of perspective on the matter. $\endgroup$ Feb 15, 2022 at 18:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.