问题描述
这是Meta_spec理论中的引理Pure.thy。事实证明：
lemma Meta_spec:
assumes "⋀x. PROP P x"
shows "PROP P x"
by(rule ‹⋀x. PROP P x›)
我的问题是rule方法如何工作。它会超越参数然后与假设统一吗？这实际上是如何进行的？我不认为使用了内核的定理forall_elim。
解决方法
我决定发表我的评论作为答案，以试图关闭此主题。当然，如果有更多知识的人士提供修订/更多信息，我将感到高兴。
Pure.rule与经典rule相似，并且两者均在文档Isar-ref中进行了描述（更具体地说，请参见Isar-ref中的6.4.3和9.4.3节）。进一步的解释也可以在由Tobias Nipkow，Lawrence Paulson和Markus Wenzel编写的（略过时）教科书高阶逻辑证明助手中找到。
实际上，正如您已经指出的那样，规则应用程序的工作原理是将子目标与规则的结论统一起来（但是，我对实现的所有细节都不熟悉）。而且，据我所知，在方法的实现中，通过使用示意变量不会使外部元量化器隐式化。因此，当然，在实现中无需为此目的调用forall_elim。实际上，如果直接将定理⋀x. PROP P x提供给方法，则定理PROP P x会失败。
但是，我相信，您提出问题的原因不是对方法rule的应用背后的主要原理缺乏理解，而是与文字事实{{1}”的形式有关}。
在您的应用程序上下文中，该文字事实与相关上下文中的定理‹⋀x. PROP P x›相对应。您可以这样输入PROP P ?x来验证这一点：
thm ‹⋀x. PROP P x›因此，从规则应用程序的角度来看，此用例没有什么特别之处，因为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›)
在?x中是示意图。