伊莎贝尔 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 步证明(，但我对证明力学的这种细微差别感兴趣。

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

Answer 1

带有rule的应用程序仅适用于最右边元含义 (==>( 之后的公式。所以你会得到如下的东西，这不是很有帮助：

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