在 Isabelle 中证明语义函数的可达状态集是有限的

Question

考虑以下属性：

lemma "finite {t. (c,s) ⇒ t}"

其中指的是以下大步语义：

inductive gbig_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55) 
where
  Skip: "(SKIP, s) ⇒ s"
| Assign: "(x ::= a, s) ⇒ s(x := aval a s)"
| Seq: "⟦(c1, s1) ⇒ s2;  (c2, s2) ⇒ s3⟧ ⟹ (c1;;c2, s1) ⇒ s3" 
| IfBlock: "⟦(b,c) ∈ set gcs; bval b s; (c,s) ⇒ s'⟧ ⟹ (IF gcs FI, s) ⇒ s'"
| DoTrue: "⟦(b,c) ∈ set gcs; bval b s1; (c,s1) ⇒ s2;(DO gcs OD,s2) ⇒ s3⟧ 
            ⟹ (DO gcs OD, s1) ⇒ s3"
| DoFalse: "⟦(∀ (b,c) ∈ set gcs. ¬ bval b s)⟧ ⟹ (DO gcs OD, s) ⇒ s"

对我来说很明显属性通过归纳对大步关系成立。但是，我无法从集合中取出它，所以我无法有效地对其进行归纳。

我该怎么做？

Answer 1

有限性不是你可以用归纳谓词的归纳规则直接证明的。问题是看一个人运行（就像归纳规则一样）并没有说明分支行为，分支行为也必须是有限的才能成立。

我看到两种证明有限性的方法：

将派生树显式建模为Isabelle/HOL中的数据类型，并证明它充分表示归纳背后的派生树。然后证明这棵树有有限多的叶子（通过对树的归纳）。如果你设计的数据类型使得叶子中的状态是一个类型参数，那么数据类型包生成的相应集合函数就是你想要证明是有限的。（请注意，您不能通过集合函数的归纳规则来证明有限性，因为那将再次只是一个运行。）
看归纳定义的内部构造。它被定义为泛函的最小不动点。您可以通过将归纳定义放入声明了 [[inductive_internals]] 的上下文中来访问这些内部结构。然后你可以证明函数在一步中保持有限性，然后通过归纳提升它。

两种方法中的证明参数相似。 #1 中的显式数据类型只是具体化了#2 的定点参数。因此，您可以将#1 视为#2 的深度嵌入。当然，您也可以仅从引入定理和归纳定理重新推导出内部构造（以更合适的格式），然后按照方法 #2。

我会尝试准确地做到这一点，因为你的语义很小。对于大型真实世界的语义，花费精力在 ML 中自动化步骤 #2 可能是有意义的。

在 Isabelle 中证明语义函数的可达状态集是有限的

Proving the set of reachable states of semantics function is finite in Isabelle

isabelle