Isabelle :使用metis进行证明会导致无限循环

Question

我想证明引理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

Answer 1

我相信你指的是来自。我不会发布完整的答案，因为我担心这是一个家庭作业问题。但是，我会给你一些建议。引理21中有一个多余的假设。一旦去掉这个假设，这个引理就变得更容易证明(如前所述，使用apply-style脚本和非常标准的教科书技术)。然而，最有可能的是，仅有metis是不够的。

如果最坏的情况发生，你可能还会从Main中的Transitive_Closure.thy理论中得到一个关于如何证明这一点的想法。不过，我想强调，证明是很简单的，所以应该是没有需要的。

Nipkow T，Klein G.与Isabelle/HOL的具体语义。海德堡: Springer-Verlag；2017年。