How to prove such a lemma in labeled transition system in Isablle

user_13276122 0
Viewed 52

I have defined such a labled transition system as below, and a function to judge given a list whether it could be reached.


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')"

But the problem is that i don't know how to prove below lemma.

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

In order to use the definition you have to make a case distinction on x to make the definition patterns appear:

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

EDIT: as a side remark, it feels more natural to me to first define a function returning the set of all reachable states and then check if v is with the set. I expect this version to be easier to reason with.

user_128242070
Related