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: Sep 11 2024 at 16:22 UTC