如何在Isablle中标记的过渡系统中证明这种引理

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是否与集合。我希望这个版本更容易推理。