The labeled transition of Isballe is defined below, which contains the prior node and the successor node, the set represents the condition.
type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"
After the LTS, we need to define a function of the reachable from Node a to Node b. The definition of LTS_is_reachable like:
inductive LTS_is_reachable :: "('q, 'a) LTS ⇒ ('q * 'q) set ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" for Δ and Δ' where
LTS_Empty[intro!]: "LTS_is_reachable Δ Δ' q  q" |
LTS_Step1: "LTS_is_reachable Δ Δ' q l q'" if "(q, q'') ∈ Δ'" and "LTS_is_reachable Δ Δ' q'' l q'" |
LTS_Step2[intro!]: "LTS_is_reachable Δ Δ' q (a # w) q'" if "a ∈ σ" and "(q, σ, q'') ∈ Δ" and "LTS_is_reachable Δ Δ' q'' w q'"
where the LTS_empty denotes node q could arrive at self by empty list, LTS_Step1 denotes if there exists node q and p in Delta', then q could reach p no condition, and LTS_Step2 denotes that node q could reach node q'' by the alphbet sigma.
Finally, I try to prove a lemma
lemma removeFromAtoEndTrans:"LTS_is_reachable Δ (insert (ini, end) Δ') ini l end ⟹ l ≠  ⟹ ∀(q, σ, p) ∈ Δ. q ≠ ini ∧ q ≠ end ⟹ ∀(end, p) ∈ Δ'. p = end ⟹ LTS_is_reachable Δ Δ' ini l end"
This lemma said that if the list l isn't empty, we could remove ini-> end from Delta2. It obviously holds. Through the tool nitpick, it can not find any counter-examples. But I could think about any ideas to prove it. Any helps would be appreciated.
This question should be asked under Beginner Questions or perhaps General. This place here is for discussions about extending Isabelle using meta-programming in ML.
Last updated: Dec 07 2023 at 16:21 UTC