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

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) 作为证人证明你的存在量化是直截了当的。

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

Proving existence of an infinite path in Isabelle

isabelle