如何解决Isabelle : 使用 metis 的证明会导致无限循环
我想证明引理 1 和引理 2 以及引理 21 是引理 2 的子目标之一。然而,在证明引理 2 时它挂在应用(metis 步骤)上,我相信没有其他方法可以证明它。有什么方法可以阻止这种无限循环的发生?提前致谢。
inductive star :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl: "star r x x"|
step: "r x y ⟹star r y z⟹star r x z"
inductive star' ::"('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"for r where
refl' : "star' r x x" |
step' : "star' r x y ⟹ r y z ⟹ star' r x z"
lemma 21 : "r x y ⟹
star r y z ⟹
star' r y z ⟹
star' r x z"
apply (metis step)
lemma 1 : "star' r x y ⟹ star r x y"
apply (induction rule : star'.induct)
apply (metis refl)
done
lemma 2 : "star r x y ⟹ star' r x y"
apply (induction rule: star.induct)
apply (metis refl')
done
解决方法
我相信您指的是 [0] 中的练习。由于担心这是一个家庭作业问题,我将避免发布完整的答案。不过,我会给一个提示。引理 21 中有一个多余的假设。一旦删除了这个假设,引理就变得更容易证明(如前所述,使用 apply
风格的脚本和非常标准的教科书技术)。但是,很可能仅靠 metis
是不够的。
如果最坏的结果是最坏的,您也可以从 Main 中的理论 Transitive_Closure.thy 中了解如何证明这一点。不过,我想强调的是,证明很简单,所以应该没有这个必要。
[0] Nipkow T,Klein G. 与 Isabelle/HOL 的具体语义。海德堡:Springer-Verlag; 2017.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。