Hongjian Jiang (Mar 01 2023 at 09:42): Hongjian Jiang (Mar 01 2023 at 09:42):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.
Wolfgang Jeltsch (Mar 02 2023 at 13:52):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: Apr 20 2024 at 08:16 UTC