# Theory Partial_Order_Reduction.Transition_System_Extensions

```section ‹Transition Systems›

theory Transition_System_Extensions
imports
"Basics/Word_Prefixes"
"Extensions/Set_Extensions"
"Extensions/Relation_Extensions"
Transition_Systems_and_Automata.Transition_System
Transition_Systems_and_Automata.Transition_System_Extra
Transition_Systems_and_Automata.Transition_System_Construction
begin

context transition_system_initial
begin

definition cycles :: "'state ⇒ 'transition list set"
where "cycles p ≡ {w. path w p ∧ target w p = p}"

lemma cyclesI[intro!]:
assumes "path w p" "target w p = p"
shows "w ∈ cycles p"
using assms unfolding cycles_def by auto
lemma cyclesE[elim!]:
assumes "w ∈ cycles p"
obtains "path w p" "target w p = p"
using assms unfolding cycles_def by auto

inductive_set executable :: "'transition set"
where executable: "p ∈ nodes ⟹ enabled a p ⟹ a ∈ executable"

lemma executableI_step[intro!]:
assumes "p ∈ nodes" "enabled a p"
shows "a ∈ executable"
using executable assms by this
lemma executableI_words_fin[intro!]:
assumes "p ∈ nodes" "path w p"
shows "set w ⊆ executable"
using assms by (induct w arbitrary: p, auto del: subsetI)
lemma executableE[elim?]:
assumes "a ∈ executable"
obtains p
where "p ∈ nodes" "enabled a p"
using assms by induct auto

end

locale transition_system_interpreted =
transition_system ex en
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
begin

definition visible :: "'action set"
where "visible ≡ {a. ∃ q. en a q ∧ int q ≠ int (ex a q)}"

lemma visibleI[intro]:
assumes "en a q" "int q ≠ int (ex a q)"
shows "a ∈ visible"
using assms unfolding visible_def by auto
lemma visibleE[elim]:
assumes "a ∈ visible"
obtains q
where "en a q" "int q ≠ int (ex a q)"
using assms unfolding visible_def by auto

abbreviation "invisible ≡ - visible"

lemma execute_fin_word_invisible:
assumes "path w p" "set w ⊆ invisible"
shows "int (target w p) = int p"
using assms by (induct w arbitrary: p rule: list.induct, auto)
lemma execute_inf_word_invisible:
assumes "run w p" "k ≤ l" "⋀ i. k ≤ i ⟹ i < l ⟹ w !! i ∉ visible"
shows "int ((p ## trace w p) !! k) = int ((p ## trace w p) !! l)"
proof -
have "(p ## trace w p) !! l = target (stake l w) p" by simp
also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp
also have "target … p = target (stake (l - k) (sdrop k w)) (target (stake k w) p)"
unfolding fold_append comp_apply by rule
also have "int … = int (target (stake k w) p)"
proof (rule execute_fin_word_invisible)
have "w = stake l w @- sdrop l w" by simp
also have "stake l w = stake k w @ stake (l - k) (sdrop k w)" using assms(2) by simp
finally have 1: "run (stake k w @- stake (l - k) (sdrop k w) @- sdrop l w) p"
unfolding shift_append using assms(1) by simp
show "path (stake (l - k) (sdrop k w)) (target (stake k w) p)" using 1 by auto
show "set (stake (l - k) (sdrop k w)) ⊆ invisible" using assms(3) by (auto simp: set_stake_snth)
qed
also have "… = int ((p ## trace w p) !! k)" by simp
finally show ?thesis by rule
qed

end

locale transition_system_complete =
transition_system_initial ex en init +
transition_system_interpreted ex en int
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
begin

definition language :: "'interpretation stream set"
where "language ≡ {smap int (p ## trace w p) |p w. init p ∧ run w p}"

lemma languageI[intro!]:
assumes "w = smap int (p ## trace v p)" "init p" "run v p"
shows "w ∈ language"
using assms unfolding language_def by auto
lemma languageE[elim!]:
assumes "w ∈ language"
obtains p v
where "w = smap int (p ## trace v p)" "init p" "run v p"
using assms unfolding language_def by auto

end

locale transition_system_finite_nodes =
transition_system_initial ex en init
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
+
assumes reachable_finite: "finite nodes"

locale transition_system_cut =
transition_system_finite_nodes ex en init
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
+
fixes cuts :: "'action set"
assumes cycles_cut: "p ∈ nodes ⟹ w ∈ cycles p ⟹ w ≠ [] ⟹ set w ∩ cuts ≠ {}"
begin

inductive scut :: "'state ⇒ 'state ⇒ bool"
where scut: "p ∈ nodes ⟹ en a p ⟹ a ∉ cuts ⟹ scut p (ex a p)"

declare scut.intros[intro!]
declare scut.cases[elim!]

lemma scut_reachable:
assumes "scut p q"
shows "p ∈ nodes" "q ∈ nodes"
using assms by auto
lemma scut_trancl:
assumes "scut⇧+⇧+ p q"
obtains w
where "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []"
using assms
proof (induct arbitrary: thesis)
case (base q)
show ?case using base by force
next
case (step q r)
obtain w where 1: "path w p" "target w p = q" "set w ∩ cuts = {}" "w ≠ []"
using step(3) by this
obtain a where 2: "en a q" "a ∉ cuts" "ex a q = r" using step(2) by auto
show ?case
proof (rule step(4))
show "path (w @ [a]) p" using 1 2 by auto
show "target (w @ [a]) p = r" using 1 2 by auto
show "set (w @ [a]) ∩ cuts = {}" using 1 2 by auto
show "w @ [a] ≠ []" by auto
qed
qed

sublocale wellfounded_relation "scut¯¯"
proof (unfold_locales, intro finite_acyclic_wf_converse[to_pred] acyclicI[to_pred], safe)
have 1: "{(p, q). scut p q} ⊆ nodes × nodes" using scut_reachable by blast
have 2: "finite (nodes × nodes)"
using finite_cartesian_product reachable_finite by blast
show "finite {(p, q). scut p q}" using 1 2 by blast
next
fix p
assume 1: "scut⇧+⇧+ p p"
have 2: "p ∈ nodes" using 1 tranclE[to_pred] scut_reachable by metis
obtain w where 3: "path w p" "target w p = p" "set w ∩ cuts = {}" "w ≠ []"
using scut_trancl 1 by this
have 4: "w ∈ cycles p" using 3(1, 2) by auto
have 5: "set w ∩ cuts ≠ {}" using cycles_cut 2 4 3(4) by this
show "False" using 3(3) 5 by simp
qed

lemma no_cut_scut:
assumes "p ∈ nodes" "en a p" "a ∉ cuts"
shows "scut¯¯ (ex a p) p"
using assms by auto

end

locale transition_system_sticky =
transition_system_complete ex en init int +
transition_system_cut ex en init sticky
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and init :: "'state ⇒ bool"
and int :: "'state ⇒ 'interpretation"
and sticky :: "'action set"
+
assumes executable_visible_sticky: "executable ∩ visible ⊆ sticky"

end
```