如何在标记跃迁系统中证明这个引理

Question

我定义了这样一个有标记的过渡系统如下，并定义了一个函数来判断给定的列表是否可以到达。

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"

primrec LTS_is_reachable :: "('q, 'a) LTS <Rightarrow> 'q <Rightarrow> 'a list <Rightarrow> 'q <Rightarrow> bool" where
"LTS_is_reachable <Delta> q [] q' = (q = q')"|
"LTS_is_reachable <Delta> q (a # w) q' =
(<exists>q'' <sigma>. a <in> <sigma> <and> (q, <sigma>, q'') <in> <Delta> <and> LTS_is_reachable <Delta> q'' w q')"

但问题是我不知道如何证明以下引理。

lemma "LTS_is_reachable {([], {v}, [v])} [] x [v] <Longrightarrow> x = [v]"

Answer 1

为了使用该定义，您必须在x上进行大小写区分，以使定义模式出现:

lemma "LTS_is_reachable {([], {v}, [v])} [] x [v] ⟹ x = [v]"
apply (cases x; cases ‹tl x›)
apply auto
done

编辑:作为旁注，我觉得更自然的是首先定义一个函数返回所有可达状态的集合，然后检查v是否与集合。我希望这个版本更容易理解。