证明伊莎贝尔存在无限路径

Question

考虑以下归纳谓词：

inductive terminating where
 "(⋀ s'. s → s' ⟹ terminating s') ⟹ terminating s"

我想证明，如果节点 s 没有终止，则存在形式为 s0 → s1 → s2 → ...的无限链。以下几行中的一些东西：

 lemma "¬ terminating (c,s) ⟹ 
       ∃ cfs. (cfs 0 = (c,s) ∧ (∀ n. (cfs n) → (cfs (n+1))))"

我如何在 Isabelle 中证明这一点？

编辑

最终的目标是证明以下目标：

lemma "(∀s t. (c, s) ⇒ t = (c', s) ⇒ t) ⟹
       terminating (c, s) = terminating (c', s) "

其中 ⇒ 是 GCL 的大步语义。也许需要另一种方法来证明这个定理。

Answer 1

如果您习惯使用选择运算符，您可以使用SOME 轻松构建见证，例如：

primrec infinite_trace :: ‹'s ⇒ nat ⇒ 's› where 
  ‹infinite_trace c0 0 = c0›
| ‹infinite_trace c0 (Suc n) =
    (SOME c. infinite_trace c0 n → c ∧ ¬ terminating c)›

（我不确定您的 s 和 (c,s) 值的类型，所以我只使用了 's。）

显然，如果SOME 无法选择满足约束的值，见证构造将失败。所以，仍然需要证明非终止确实传播（从定义中很明显）：

lemma terminating_suc:
  assumes ‹¬ terminating c›
  obtains c' where ‹c → c'› ‹¬ terminating c'›
  using assms terminating.intros by blast

lemma nontermination_implies_infinite_trace:
  assumes ‹¬ terminating c0›
  shows  ‹¬ terminating (infinite_trace c0 n) 
    ∧ infinite_trace c0 n → infinite_trace c0 (Suc n)›
  by (induct n,
     (simp, metis (mono_tags, lifting) terminating_suc assms exE_some)+) 

使用infinite_trace (c,s) 作为见证来证明你的存在量化是直截了当的。