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