1

我有以下内容：

lemma 
  assumes p: "P"
  assumes pimpq: "P⟶Q"
  shows "P∧Q"
proof -
  from pimpq p have q: "Q" by (rule impE)
  from p q show ?thesis by (rule conjI)
qed

我认为这取决于基本推理规则，但阅读Isar 参考手册rule部分的文档9.4.3 Structured Methods后发现，它使用了具有各种规则的 Classical Reasoner。并且，将by子句替换为..也解决了目标，因此不需要提及隐含消除和连词介绍。

是否可以在 Isar 中编写严格的形式化，即不使用程序文本中未明确的任何自动化和额外规则？类似于 HOL4 中的前向证明。

4

1 回答 1

2

Pure.rule如果您不想使用该classical模块，则可以使用。

lemma 
  assumes p: "P"
  assumes pimpq: "P⟶Q"
  shows "P∧Q"
proof -
  from pimpq p have q: "Q" by (Pure.rule impE)
  from p q show ?thesis by (Pure.rule conjI)
qed

如果您编写..Isabelle 将自动选择基于标有[intro]or[elim]属性的引理的规则。

也许您也可以分享您想要在 Isabelle 中重现的 HOL4 证明，以便我们可以在 Isabelle/HOL 中提出等价的建议。

于 2020-03-04T10:45:21.463 回答