Hongjian Jiang (Mar 01 2023 at 09:44): Hongjian Jiang (Mar 01 2023 at 09:44):For some purpose, I want to prove such a lemma: if one automaton could be reachable and another automaton could be reachable, such that the concat of these two automata could be reachable. The qa is a list and x is an LTS transition.
lemma concat_lemma:"single_LTS_reachable_by_path qa x ⟹ single_LTS_reachable_by_path q xa ⟹ single_LTS_reachable_by_path (qa @ q) (x @ xa)"
sorry
lemma inverse_concat_lemma: "single_LTS_reachable_by_path q (xa @ y) ⟹ ∃p qa. q = qa @ p ∧ single_LTS_reachable_by_path qa xa ∧ single_LTS_reachable_by_path p y"
sorry
The definition of single_LTS_reachable_by_path and others are below:
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' ∨ (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')"
primrec single_LTS_reachable_by_path :: "'a list ⇒ (('q,'a) LTS * 'q * 'q) list ⇒ bool " where
"single_LTS_reachable_by_path w []= (w = [])"|
"single_LTS_reachable_by_path w (x# xs) = (∃p q. (w = p @ q ∧ LTS_is_reachable (fst x) (fst (snd x)) p (snd (snd x)) ∧ single_LTS_reachable_by_path q xs))"
For the primrec and fun in isabelle, how many tactic could be used.
Last updated: Dec 21 2024 at 16:20 UTC