证明 Isabelle 中顺序组合的结合性

Question

考虑以下描述受保护命令语言的小步语义的归纳定义：

inductive small_step :: "com × state ⇒ com × state ⇒ bool" (infix "→" 55)
where
 Assign:  "(x ::= a, s) → (SKIP, s(x := aval a s))" |
 Seq1:    "(SKIP;;c2,s) → (c2,s)" |
 Seq2:    "(c1,s) → (c1',s') ⟹ (c1;;c2,s) → (c1';;c2,s')" |
 IfBlock: "(b,c) ∈ set gcs ⟹ bval b s ⟹ (IF gcs FI,s) → (c,s)" |
 DoTrue:  "(b,c) ∈ set gcs ⟹ bval b s ⟹ (DO gcs OD,s) → (c;;DO gcs OD,s)" |
 DoFalse: "(∀ b c. (b,c) ∈ set gcs ⟶ ¬ bval b s) ⟹ (DO gcs OD,s) → (SKIP,s)"

我要证明：

lemma "((c1 ;; c2) ;; c3) ~ (c1 ;; (c2 ;; c3))"

其中：

definition equiv_c :: "com ⇒ com ⇒ bool" (infix "~" 50) where
 "c ~ c' ≡ ∀ s c0 s0. (c,s) → (c0,s0) = (c',s) → (c0,s0)"

而且越来越难做到这一点。 Johan J. Lukkien 在 "An operational semantics for the Guarded Command Language" 中给出了我找到的最接近的解决方案。然而，在那篇文章中，程序被建模为状态序列，而在这里我将它们建模为命令配置和状态。或许，两者之间有关系，但我的尝试到目前为止都失败了。

你在 Isabelle 中找到了证明这个引理的方法吗？

Answer 1

所述的所需引理不成立。所以你将无法证明这一点。我可以看到两个主要问题：

→表示执行的一步，但等价应该是整个行为，而不是一步。一步之后，很可能得到的程序还是不一样。
某些程序的语义可能会卡住，例如 IF [] FI。如果您想对剩余的程序说些什么 c0，那么这种卡住的状态就很难说明等价性。例如，在你的引理中取 c1 = SKIP;; IF [] FI 和 c2 = c3 = SKIP。然后，从 (c1 ;; c2) ;; c3 到达的部分评估的命令与从 c1 ;; (c2 ;; c3) 到达的命令相同。

我建议您首先弄清楚程序的行为应该是什么。对于一段时间的语言，这通常是一组可到达的最终状态，并且可能是非终止状态。然后，您必须决定您对哪种等价性感兴趣。通常，人们会关注迹等价性或双模拟，这对于非确定性程序来说是不同的。而等价概念将决定如何证明这样的引理。

证明 Isabelle 中顺序组合的结合性

Proving associativity of sequential composition in Isabelle

semantics

isabelle