伊莎贝尔：使用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

我相信您指的是 [0] 中的一个练习。由于担心这是一个家庭作业问题，我将避免发布完整的答案。不过，我会给小费。引理 21 中有一个多余的假设。一旦你删除了这个假设，这个引理就变得更容易证明（如前所述，使用apply 风格的脚本和非常标准的教科书技术）。但是，很可能仅metis 是不够的。

如果最坏的情况出现在最坏的情况下，您还可以从 Main 中的理论 Transitive_Closure.thy 中了解如何证明这一点。不过，我想强调一下，证明很简单，所以这不是必须的。

[0] Nipkow T，Klein G. 与 Isabelle/HOL 的具体语义。海德堡：施普林格出版社； 2017.