subsection ‹Transition Systems with Silent Steps›
theory Weak_Transition_Systems
imports Transition_Systems
begin
locale lts_tau = lts trans for
trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› + fixes
τ :: ‹'a› begin
definition tau :: ‹'a ⇒ bool› where ‹tau a ≡ (a = τ)›
lemma tau_tau[simp]: ‹tau τ› unfolding tau_def by simp
abbreviation weak_step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool›
("_ ⇒_ _" [70, 70, 70] 80)
where
‹(p ⇒a q) ≡ (∃ pq1 pq2.
p ⟼* tau pq1 ∧
pq1 ⟼a pq2 ∧
pq2 ⟼* tau q)›
lemma step_weak_step:
assumes ‹p ⟼a p'›
shows ‹p ⇒a p'›
using assms steps.refl by auto
abbreviation weak_step_tau :: ‹'s ⇒ 'a ⇒ 's ⇒ bool›
("_ ⇒^_ _" [70, 70, 70] 80)
where
‹(p ⇒^a q) ≡
(tau a ⟶ p ⟼* tau q) ∧
(¬tau a ⟶ p ⇒a q)›
abbreviation weak_step_delay :: ‹'s ⇒ 'a ⇒ 's ⇒ bool›
("_ =⊳ _ _" [70, 70, 70] 80)
where
‹(p =⊳a q) ≡
(tau a ⟶ p ⟼* tau q) ∧
(¬tau a ⟶ (∃ pq.
p ⟼* tau pq ∧
pq ⟼a q))›
lemma weak_step_delay_implies_weak_tau:
assumes ‹p =⊳a p'›
shows ‹p ⇒^a p'›
using assms steps.refl[of p' tau] by blast
lemma weak_step_delay_left:
assumes
‹¬ p0 ⟼a p1›
‹p0 =⊳a p1›
‹¬tau a›
shows
‹∃ p0' t. tau t ∧ p0 ⟼t p0' ∧ p0' =⊳a p1›
using assms steps_left by metis
primrec weak_step_seq :: ‹'s ⇒ 'a list ⇒ 's ⇒ bool›
("_ ⇒$ _ _" [70, 70, 70] 80)
where
‹weak_step_seq p0 [] p1 = p0 ⟼* tau p1›
| ‹weak_step_seq p0 (a#A) p1 = (∃ p01 . p0 ⇒^a p01 ∧ weak_step_seq p01 A p1)›
lemma step_weak_step_tau:
assumes ‹p ⟼a p'›
shows ‹p ⇒^a p'›
using step_weak_step[OF assms] steps_one_step[OF assms]
by blast
lemma step_tau_refl:
shows ‹p ⇒^τ p›
using steps.refl[of p tau]
by simp
lemma weak_step_tau_weak_step[simp]:
assumes ‹p ⇒^a p'› ‹¬ tau a›
shows ‹p ⇒a p'›
using assms by auto
lemma weak_steps:
assumes
‹p ⇒a p'›
‹⋀ a . tau a ⟹ A a›
‹A a›
shows
‹p ⟼* A p'›
proof -
obtain pp pp' where pp:
‹p ⟼* tau pp› ‹pp ⟼a pp'› ‹pp' ⟼* tau p'›
using assms(1) by blast
then have cascade:
‹p ⟼* A pp› ‹pp ⟼* A pp'› ‹pp' ⟼* A p'›
using steps_one_step steps_spec assms(2,3) by auto
have ‹p ⟼* A pp'› using steps_concat[OF cascade(2) cascade(1)] .
show ?thesis using steps_concat[OF cascade(3) `p ⟼* A pp'`] .
qed
lemma weak_step_impl_weak_tau:
assumes
‹p ⇒a p'›
shows
‹p ⇒^a p'›
using assms weak_steps[OF assms, of tau] by auto
lemma weak_impl_strong_step:
assumes
‹p ⇒a p''›
shows
‹(∃ a' p' . tau a' ∧ p ⟼a' p') ∨ (∃ p' . p ⟼a p')›
proof -
from assms obtain pq1 pq2 where pq12:
‹p ⟼* tau pq1›
‹pq1 ⟼a pq2›
‹pq2 ⟼* tau p''› by blast
show ?thesis
proof (cases ‹p = pq1›)
case True
then show ?thesis using pq12 by blast
next
case False
then show ?thesis using pq12 steps_left[of p pq1 tau] by blast
qed
qed
lemma weak_step_extend:
assumes
‹p1 ⟼* tau p2›
‹p2 ⇒^a p3›
‹p3 ⟼* tau p4›
shows
‹p1 ⇒^a p4›
using assms steps_concat by blast
lemma weak_step_tau_tau:
assumes
‹p1 ⟼* tau p2›
‹tau a›
shows
‹p1 ⇒^a p2›
using assms by blast
lemma weak_single_step[iff]:
‹p ⇒$ [a] p' ⟷ p ⇒^a p'›
using steps.refl[of p' tau]
by (meson steps_concat weak_step_seq.simps(1) weak_step_seq.simps(2))
abbreviation weak_enabled :: ‹'s ⇒ 'a ⇒ bool› where
‹weak_enabled p a ≡
∃ pq1 pq2. p ⟼* tau pq1 ∧ pq1 ⟼a pq2›
lemma weak_enabled_step:
shows ‹weak_enabled p a = (∃ p'. p ⇒a p')›
using step_weak_step steps_concat by blast
abbreviation tau_max :: ‹'s ⇒ bool› where
‹tau_max p ≡ (∀p'. p ⟼* tau p' ⟶ p = p')›
lemma tau_max_deadlock:
fixes q
assumes
‹⋀ r1 r2. r1 ⟼* tau r2 ∧ r2 ⟼* tau r1 ⟹ r1 = r2›
‹finite {q'. q ⟼* tau q'}›
shows
‹∃ q' . q ⟼* tau q' ∧ tau_max q'›
using step_max_deadlock assms by blast
abbreviation stable_state :: ‹'s ⇒ bool› where
‹stable_state p ≡ ∄ p' . step_pred p tau p'›
lemma stable_tauclosure_only_loop:
assumes
‹stable_state p›
shows
‹tau_max p›
using assms steps_left by blast
coinductive divergent_state :: ‹'s ⇒ bool› where
omega: ‹divergent_state p' ⟹ tau t ⟹ p ⟼t p'⟹ divergent_state p›
lemma ex_divergent:
assumes ‹p ⟼a p› ‹tau a›
shows ‹divergent_state p›
using assms
proof (coinduct)
case (divergent_state p)
then show ?case using assms by auto
qed
lemma ex_not_divergent:
assumes ‹∀a q. p ⟼a q ⟶ ¬ tau a› ‹divergent_state p›
shows ‹False› using assms(2)
proof (cases rule:divergent_state.cases)
case (omega p' t)
thus ?thesis using assms(1) by auto
qed
lemma perpetual_instability_divergence:
assumes
‹∀ p' . p ⟼* tau p' ⟶ ¬ stable_state p'›
shows
‹divergent_state p›
using assms
proof (coinduct rule: divergent_state.coinduct)
case (divergent_state p)
then obtain t p' where ‹tau t› ‹p ⟼t p'› using steps.refl by blast
then moreover have ‹∀p''. p' ⟼* tau p'' ⟶ ¬ stable_state p''›
using divergent_state step_weak_step_tau steps_concat by blast
ultimately show ?case by blast
qed
corollary non_divergence_implies_eventual_stability:
assumes
‹¬ divergent_state p›
shows
‹∃ p' . p ⟼* tau p' ∧ stable_state p'›
using assms perpetual_instability_divergence by blast
end
subsection ‹Finite Transition Systems with Silent Steps›
locale lts_tau_finite = lts_tau trans τ for
trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› and
τ :: ‹'a› +
assumes
finite_state_set: ‹finite (top::'s set)›
begin
lemma finite_state_rel: ‹finite (top::('s rel))›
using finite_state_set
by (simp add: finite_prod)
end
end