Search code examples
isabelle

How can I prove "(⋀x. PROP ?P x) ⟹ PROP ?P ?x" in Isabelle?

This is lemma meta_spec from the theory Pure.thy. It is proven by:

lemma meta_spec:
  assumes "⋀x. PROP P x"
  shows "PROP P x"
  by(rule ‹⋀x. PROP P x›)

My question is how is this method rule working. Does it lift over parameters and then unify with the assumption? How is this actually carried out? I don't think that the theorem forall_elim of the kernel is used.

Solution

  • I decided to post my comments as an answer in an attempt to close this thread. Of course, I would be happy for anyone more knowledgeable to provide amendments/further information.

    Pure.rule is similar to classical rule and both are described in the document Isar-ref (more specifically, see sections 6.4.3 and 9.4.3 in Isar-ref). Further explanation can also be found in the (slightly outdated) textbook A Proof Assistant for Higher-Order Logic written by Tobias Nipkow, Lawrence Paulson, and Markus Wenzel.

    Indeed, as you have stated, the rule application works by unifying the subgoal with the conclusion of the rule (however, I am not familiar with all the details of the implementation). Also, to the best of my knowledge, the outer meta-quantifiers are not made implicit via the use of the schematic variables in the implementation of the method. Therefore, of course, there is no need to invoke forall_elim for such purpose in the implementation. In fact, if you were to provide the theorem ⋀x. PROP P x directly to the method, it would fail on your goal PROP P x.

    I believe, however, the reason for your question was not the lack of understanding of the main principles behind the application of the method rule, but the confusion related to the form of the literal fact ‹⋀x. PROP P x›. In the context of your application, this literal fact corresponds to the theorem PROP P ?x in the relevant context. You can verify this by typing thm ‹⋀x. PROP P x› like this:

    lemma meta_spec:
  assumes "⋀x. PROP P x"
  shows "PROP P x"
  thm ‹⋀x. PROP P x› (*PROP P ?x*)
  by(rule ‹⋀x. PROP P x›)

    Thus, there is nothing special about this use case from the perspective of the rule application, as ?x is schematic in PROP P ?x.