# Theory Transition_System

```section ‹Transition Systems›

theory Transition_System
imports "../Basic/Sequence"
begin

subsection ‹Universal Transition Systems›

locale transition_system_universal =
fixes execute :: "'transition ⇒ 'state ⇒ 'state"
begin

abbreviation "target ≡ fold execute"
abbreviation "states ≡ scan execute"
abbreviation "trace ≡ sscan execute"

lemma target_alt_def: "target r p = last (p # states r p)" using scan_last by rule

end

subsection ‹Transition Systems›

locale transition_system =
transition_system_universal execute
for execute :: "'transition ⇒ 'state ⇒ 'state"
+
fixes enabled :: "'transition ⇒ 'state ⇒ bool"
begin

abbreviation "successors p ≡ {execute a p |a. enabled a p}"

inductive path :: "'transition list ⇒ 'state ⇒ bool" where
nil[intro!]: "path [] p" |
cons[intro!]: "enabled a p ⟹ path r (execute a p) ⟹ path (a # r) p"

inductive_cases path_cons_elim[elim!]: "path (a # r) p"

lemma path_append[intro!]:
assumes "path r p" "path s (target r p)"
shows "path (r @ s) p"
using assms by (induct r arbitrary: p) (auto)
lemma path_append_elim[elim!]:
assumes "path (r @ s) p"
obtains "path r p" "path s (target r p)"
using assms by (induct r arbitrary: p) (auto)

coinductive run :: "'transition stream ⇒ 'state ⇒ bool" where
scons[intro!]: "enabled a p ⟹ run r (execute a p) ⟹ run (a ## r) p"

inductive_cases run_scons_elim[elim!]: "run (a ## r) p"

lemma run_shift[intro!]:
assumes "path r p" "run s (target r p)"
shows "run (r @- s) p"
using assms by (induct r arbitrary: p) (auto)
lemma run_shift_elim[elim!]:
assumes "run (r @- s) p"
obtains "path r p" "run s (target r p)"
using assms by (induct r arbitrary: p) (auto)

lemma run_coinduct[case_names run, coinduct pred: run]:
assumes "R r p"
assumes "⋀ a r p. R (a ## r) p ⟹ enabled a p ∧ R r (execute a p)"
shows "run r p"
using stream.collapse run.coinduct assms by metis
lemma run_coinduct_shift[case_names run, consumes 1]:
assumes "R r p"
assumes "⋀ r p. R r p ⟹ ∃ s t. r = s @- t ∧ s ≠ [] ∧ path s p ∧ R t (target s p)"
shows "run r p"
proof -
have "∃ s t. r = s @- t ∧ path s p ∧ R t (target s p)" using assms(1) by force
then show ?thesis using assms(2) by (coinduct) (force elim: path.cases)
qed
lemma run_flat_coinduct[case_names run, consumes 1]:
assumes "R rs p"
assumes "⋀ r rs p. R (r ## rs) p ⟹ r ≠ [] ∧ path r p ∧ R rs (target r p)"
shows "run (flat rs) p"
using assms(1)
proof (coinduction arbitrary: rs p rule: run_coinduct_shift)
case (run rs p)
then show ?case using assms(2) by (metis stream.exhaust flat_Stream)
qed

inductive_set reachable :: "'state ⇒ 'state set" for p where
reflexive[intro!]: "p ∈ reachable p" |
execute[intro!]: "q ∈ reachable p ⟹ enabled a q ⟹ execute a q ∈ reachable p"

inductive_cases reachable_elim[elim]: "q ∈ reachable p"

lemma reachable_execute'[intro]:
assumes "enabled a p" "q ∈ reachable (execute a p)"
shows "q ∈ reachable p"
using assms(2, 1) by induct auto
lemma reachable_elim'[elim]:
assumes "q ∈ reachable p"
obtains "q = p" | a where "enabled a p" "q ∈ reachable (execute a p)"
using assms by induct auto

lemma reachable_target[intro]:
assumes "q ∈ reachable p" "path r q"
shows "target r q ∈ reachable p"
using assms by (induct r arbitrary: q) (auto)
lemma reachable_target_elim[elim]:
assumes "q ∈ reachable p"
obtains r
where "path r p" "q = target r p"
using assms by induct force+

lemma reachable_alt_def: "reachable p = {target r p |r. path r p}" by auto

lemma reachable_trans[trans]: "q ∈ reachable p ⟹ s ∈ reachable q ⟹ s ∈ reachable p" by auto

lemma reachable_successors[intro!]: "successors p ⊆ reachable p" by auto

lemma reachable_step: "reachable p = insert p (⋃ (reachable ` successors p))" by auto

end

subsection ‹Transition Systems with Initial States›

locale transition_system_initial =
transition_system execute enabled
for execute :: "'transition ⇒ 'state ⇒ 'state"
and enabled :: "'transition ⇒ 'state ⇒ bool"
+
fixes initial :: "'state ⇒ bool"
begin

inductive_set nodes :: "'state set" where
initial[intro]: "initial p ⟹ p ∈ nodes" |
execute[intro!]: "p ∈ nodes ⟹ enabled a p ⟹ execute a p ∈ nodes"

lemma nodes_target[intro]:
assumes "p ∈ nodes" "path r p"
shows "target r p ∈ nodes"
using assms by (induct r arbitrary: p) (auto)
lemma nodes_target_elim[elim]:
assumes "q ∈ nodes"
obtains r p
where "initial p" "path r p" "q = target r p"
using assms by induct force+

lemma nodes_alt_def: "nodes = ⋃ (reachable ` Collect initial)" by auto

lemma nodes_trans[trans]: "p ∈ nodes ⟹ q ∈ reachable p ⟹ q ∈ nodes" by auto

end

end
```