isabelle - 是否可以在 Isar 中编写非自动形式化?
问题描述
我有以下内容:
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 中的前向证明。
解决方案
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 中提出等价的建议。
推荐阅读
- java - 如何在 Intellij ide 中设置资源文件夹 - java
- html - 将空间百分比分配给子组件的子组件
- python - 在id上合并两个不同长度的dataframe,并用数据填充空值
- java - Micronaut 控制器测试 - DefaultHttpClient (RxHttpClient) 在使用交换而不是检索时返回空正文
- amazon-web-services - Amazon Textract JSON 缺少一些页面
- javascript - 根据浏览器的潜在 jQuery 初始化问题
- google-sheets - 在谷歌表单时间戳列上查询“今天”?
- javascript - 给定一个范围列表,其中一些优先级高于其他范围,确定非重叠段
- wso2 - 如何使用 Apache Synapse 标注调解器发送给定的传输标头
- python - 如何创建中间件在url发现之前拦截请求,使未经授权的用户无法学习url?