# Theory Transition_System_Traces

```section ‹Transition Systems and Trace Theory›

theory Transition_System_Traces
imports
Transition_System_Extensions
Traces
begin

lemma (in transition_system) words_infI_construct[rule_format, intro?]:
assumes "∀ v. v ≤⇩F⇩I w ⟶ path v p"
shows "run w p"
using assms by coinduct auto

lemma (in transition_system) words_infI_construct':
assumes "⋀ k. ∃ v. v ≤⇩F⇩I w ∧ k < length v ∧ path v p"
shows "run w p"
proof
fix u
assume 1: "u ≤⇩F⇩I w"
obtain v where 2: "v ≤⇩F⇩I w" "length u < length v" "path v p" using assms(1) by auto
have 3: "length u ≤ length v" using 2(2) by simp
have 4: "u ≤ v" using prefix_fininf_length 1 2(1) 3 by this
show "path u p" using 4 2(3) by auto
qed

lemma (in transition_system) words_infI_construct_chain[intro]:
assumes "chain w" "⋀ k. path (w k) p"
shows "run (limit w) p"
proof (rule words_infI_construct')
fix k
obtain l where 1: "k < length (w l)" using assms(1) by rule
show "∃ v. v ≤⇩F⇩I limit w ∧ k < length v ∧ path v p"
proof (intro exI conjI)
show "w l ≤⇩F⇩I limit w" using chain_prefix_limit assms(1) by this
show "k < length (w l)" using 1 by this
show "path (w l) p" using assms(2) by this
qed
qed

lemma (in transition_system) words_fin_blocked:
assumes "⋀ w. path w p ⟹ A ∩ set w = {} ⟹ A ∩ {a. enabled a (target w p)} ⊆ A ∩ {a. enabled a p}"
assumes "path w p" "A ∩ {a. enabled a p} ∩ set w = {}"
shows "A ∩ set w = {}"
using assms by (induct w rule: rev_induct, auto)

locale transition_system_traces =
transition_system ex en +
traces ind
for ex :: "'action ⇒ 'state ⇒ 'state"
and en :: "'action ⇒ 'state ⇒ bool"
and ind :: "'action ⇒ 'action ⇒ bool"
+
assumes en: "ind a b ⟹ en a p ⟹ en b p ⟷ en b (ex a p)"
assumes ex: "ind a b ⟹ en a p ⟹ en b p ⟹ ex b (ex a p) = ex a (ex b p)"
begin

lemma diamond_bottom:
assumes "ind a b"
assumes "en a p" "en b p"
shows "en a (ex b p)" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)"
using assms independence_symmetric en ex by metis+
lemma diamond_right:
assumes "ind a b"
assumes "en a p" "en b (ex a p)"
shows "en a (ex b p)" "en b p" "ex b (ex a p) = ex a (ex b p)"
using assms independence_symmetric en ex by metis+
lemma diamond_left:
assumes "ind a b"
assumes "en a (ex b p)" "en b p"
shows "en a p" "en b (ex a p)" "ex b (ex a p) = ex a (ex b p)"
using assms independence_symmetric en ex by metis+

lemma eq_swap_word:
assumes "w⇩1 =⇩S w⇩2" "path w⇩1 p"
shows "path w⇩2 p"
using assms diamond_right by (induct, auto)
lemma eq_fin_word:
assumes "w⇩1 =⇩F w⇩2" "path w⇩1 p"
shows "path w⇩2 p"
using assms eq_swap_word by (induct, auto)
lemma le_fin_word:
assumes "w⇩1 ≼⇩F w⇩2" "path w⇩2 p"
shows "path w⇩1 p"
using assms eq_fin_word by blast
lemma le_fininf_word:
assumes "w⇩1 ≼⇩F⇩I w⇩2" "run w⇩2 p"
shows "path w⇩1 p"
using assms le_fin_word by blast
lemma le_inf_word:
assumes "w⇩2 ≼⇩I w⇩1" "run w⇩1 p"
shows "run w⇩2 p"
using assms le_fininf_word by (blast intro: words_infI_construct)
lemma eq_inf_word:
assumes "w⇩1 =⇩I w⇩2" "run w⇩1 p"
shows "run w⇩2 p"
using assms le_inf_word by auto

lemma eq_swap_execute:
assumes "path w⇩1 p" "w⇩1 =⇩S w⇩2"
shows "fold ex w⇩1 p = fold ex w⇩2 p"
using assms(2, 1) diamond_right by (induct, auto)
lemma eq_fin_execute:
assumes "path w⇩1 p" "w⇩1 =⇩F w⇩2"
shows "fold ex w⇩1 p = fold ex w⇩2 p"
using assms(2, 1) eq_fin_word eq_swap_execute by (induct, auto)

lemma diamond_fin_word_step:
assumes "Ind {a} (set v)" "en a p" "path v p"
shows "path v (ex a p)"
using diamond_bottom assms by (induct v arbitrary: p, auto, metis)
lemma diamond_inf_word_step:
assumes "Ind {a} (sset w)" "en a p" "run w p"
shows "run w (ex a p)"
using diamond_fin_word_step assms by (fast intro: words_infI_construct)
lemma diamond_fin_word_inf_word:
assumes "Ind (set v) (sset w)" "path v p" "run w p"
shows "run w (fold ex v p)"
using diamond_inf_word_step assms by (induct v arbitrary: p, auto)
lemma diamond_fin_word_inf_word':
assumes "Ind (set v) (sset w)" "path (u @ v) p" "run (u @- w) p"
shows "run (u @- v @- w) p"
using assms diamond_fin_word_inf_word by auto

end

end
```