时间戳

首页 > 解决方案 > 证明伊莎贝尔存在无限路径

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

问题描述

考虑以下归纳谓词：

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 的大步语义。也许需要另一种方法来证明这个定理。

标签： isabelle

解决方案

如果您习惯使用选择运算符，则可以使用 轻松构建见证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)是直截了当的。

推荐阅读