isabelle - Isabelle FOL 部分规则应用

Question

假设我们有这样的 Modus Ponens 变体

lemma invDed: ‹(A-->B)==>(A==>B)›
  apply(rule mp)
  apply assumption
  apply assumption
  done

可以用来证明定理吗？（我的意思是 A:=A、B:=A 和 A-->A 我们使用，就好像它之前已被证明一样）

lemma myid2: "A==>A"

如果不是，为什么？我知道证明这个定理的其他几种方法（“应用假设”或弗雷格命题演算公理的 5 步证明。），但我对证明机制的这种细微差别感兴趣。

我有一个规则，现在我想获得另一个 [admissible] 规则，有什么问题？

score 0 · Accepted Answer

应用 withrule仅适用于最右边的元蕴涵 ( ==>) 之后的公式。所以你会得到类似下面的东西，这不是很有帮助：

lemma myid2: "A==>A"
proof (rule invDed[where A=A and B=A])
  show "A ⟹ A ⟶ A"
    by (rule imp_refl)
  show "A ⟹ A"
    by assumption
qed

如果您将您的场所（使用[rotated]修饰符在下面完成）旋转为拥有A==>(A-->B)==>(B)，那么您可以将其应用于erule：

lemma myid2: "A==>A"
  apply (erule invDed[rotated])
  apply (rule imp_refl)
  done

1 回答 1