Theory Weak_Transition_Systems

theory Weak_Transition_Systems
imports Transition_Systems
```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
‹p ⟼* A pp› ‹pp ⟼* A  pp'› ‹pp' ⟼* A p'›
using steps_one_step steps_spec assms(2,3) by auto
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')›

fixes q
assumes
‹⋀ r1 r2. r1 ⟼* tau r2 ∧ r2 ⟼* tau r1 ⟹ r1 = r2› ―‹contracted cycles (anti-symmetry)›
‹finite {q'. q ⟼* tau q'}›
shows
‹∃ q' . q ⟼* tau q' ∧ tau_max q'›

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 ―‹context @{locale lts_tau}›

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