# Theory Transition_Systems_and_Automata.Transition_System_Extra

```section ‹Additional Theorems for Transition Systems›

theory Transition_System_Extra
imports
"../Basic/Sequence_LTL"
"Transition_System"
begin

context transition_system
begin

definition "enableds p ≡ {a. enabled a p}"
definition "paths p ≡ {r. path r p}"
definition "runs p ≡ {r. run r p}"

lemma stake_run:
assumes "⋀ k. path (stake k r) p"
shows "run r p"
using assms by (coinduction arbitrary: r p) (force elim: path.cases)
lemma snth_run:
assumes "⋀ k. enabled (r !! k) (target (stake k r) p)"
shows "run r p"
using assms by (coinduction arbitrary: r p) (metis stream.sel fold_simps snth.simps stake.simps)

lemma run_stake:
assumes "run r p"
shows "path (stake k r) p"
using assms by (metis run_shift_elim stake_sdrop)
lemma run_sdrop:
assumes "run r p"
shows "run (sdrop k r) (target (stake k r) p)"
using assms by (metis run_shift_elim stake_sdrop)
lemma run_snth:
assumes "run r p"
shows "enabled (r !! k) (target (stake k r) p)"
using assms by (metis stream.collapse sdrop_simps(1) run_scons_elim run_sdrop)

lemma run_alt_def_snth: "run r p ⟷ (∀ k. enabled (r !! k) (target (stake k r) p))"
using snth_run run_snth by blast

lemma reachable_states:
assumes "q ∈ reachable p" "path r q"
shows "set (states r q) ⊆ reachable p"
using assms by (induct r arbitrary: q) (auto)
lemma reachable_trace:
assumes "q ∈ reachable p" "run r q"
shows "sset (trace r q) ⊆ reachable p"
using assms unfolding sset_subset_stream_pred
by (coinduction arbitrary: r q) (force elim: run.cases)

end

context transition_system_initial
begin

lemma nodes_states:
assumes "p ∈ nodes" "path r p"
shows "set (states r p) ⊆ nodes"
using reachable_states assms by blast
lemma nodes_trace:
assumes "p ∈ nodes" "run r p"
shows "sset (trace r p) ⊆ nodes"
using reachable_trace assms by blast

end

end```