Stream: Beginner Questions

Topic: a lemma prove


view this post on Zulip 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: Mar 28 2024 at 12:29 UTC