Theory Weak_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› (‹_ ⟼_  _› [70, 70, 70] 80) + 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

lemma step_tau_concat: 
  assumes 
    ‹q ⇒^a q'›
    ‹q' ⇒^τ q1›
  shows ‹q ⇒^a q1›
proof - 
  show ?thesis using assms steps_concat tau_tau by blast 
qed

lemma tau_step_concat: 
  assumes 
    ‹q ⇒^τ q'›
    ‹q' ⇒^a q1›
  shows ‹q ⇒^a q1›
proof - 
  show ?thesis using assms steps_concat tau_tau by blast 
qed


lemma tau_word_concat: 
  assumes
    ‹q ⇒^τ q'› 
    ‹q' ⇒$A q1› 
  shows ‹q ⇒$A q1›
  using assms
proof (cases A)
  case Nil
  hence ‹q' ⇒^τ q1› using assms by auto
  thus ?thesis using Nil assms steps_concat tau_tau weak_step_seq.simps by blast
next
  case (Cons a A)
  then obtain q'' where  ‹q' ⇒^a q''› and A_step:  ‹q'' ⇒$A q1 › using assms by auto
  hence ‹q ⇒^a q''› using tau_step_concat[OF assms(1)] by auto
  then show ?thesis using Cons A_step  ‹q ⇒^a q''› by auto 
qed

lemma strong_weak_transition_system:
  assumes
    ‹⋀ p q a. p ⟼ a q ⟹ ¬ tau a›
    ‹¬ tau a›
  shows
    ‹p ⇒^a p' = p ⟼ a p'›
proof
  assume ‹p ⇒^a  p'›
  then obtain p0 p1 where ‹p ⟼* tau p0› ‹p0 ⟼a p1› ‹p1 ⟼* tau p'› using assms by blast
  then have ‹p = p0› ‹p1 = p'› using assms(1) steps_no_step by blast+
  with ‹p0 ⟼a p1› show ‹p ⟼a  p'› by blast
next
  assume ‹p ⟼a  p'›
  thus ‹p ⇒^a  p'› using step_weak_step_tau by blast
qed

lemma rev_seq_split : 
  assumes ‹q ⇒$ (xs @ [x])  q1›
  shows ‹∃q'. q ⇒$xs q' ∧ q' ⇒^x q1›
  using assms
proof (induct xs arbitrary: q)
  case Nil
  hence ‹q ⇒$ [x]  q1› by auto
  hence x_succ: ‹q ⇒^x q1› by blast 
  have ‹q ⇒$[] q› by (simp add: steps.refl) 
  then show ?case using x_succ by auto
next
  case (Cons a xs)
  then obtain q' where q'_def: ‹q ⇒^a q' ∧ q' ⇒$(xs@[x]) q1› by auto
  then obtain q'' where ‹q' ⇒$ xs  q'' ∧ q'' ⇒^x  q1› using Cons.hyps[of ‹q'›] by auto
  then show ?case using q'_def by auto
qed

lemma rev_seq_concat: 
  assumes 
    ‹q ⇒$as q'› 
    ‹q'⇒$A q1›
  shows ‹q ⇒$(as@A) q1›
  using assms
proof (induct as arbitrary: A q' rule: rev_induct)
  case Nil
  hence ‹q ⇒^τ q'› by auto
  hence ‹q ⇒^τ q' ∧ q' ⇒$A q1› using Nil.prems(2) by blast 
  hence ‹q ⇒$A q1› using tau_word_concat by auto 
  then show ?case by simp
next
  case (snoc x xs)
  hence ‹∃q''. q ⇒$xs q'' ∧ q'' ⇒^x q'› using rev_seq_split by simp
  then obtain q'' where q_def: ‹q ⇒$xs q''› ‹q'' ⇒^x q'› by auto
  from snoc.prems(2) have ‹q' ⇒$A q1› by blast
  hence ‹q'' ⇒$(x#A) q1› using q_def by auto
  hence ‹q'' ⇒$([x]@A) q1› by auto
  then show ?case using snoc.hyps[of ‹q''› ‹[x]@A›] q_def by auto
qed

lemma rev_seq_step_concat : 
  assumes 
    ‹q ⇒$as q'› 
    ‹q'⇒^a q1›
  shows ‹q ⇒$(as@[a]) q1›
proof - 
  from assms(2) have ‹q'⇒$[a] q1› by blast
  thus ?thesis using rev_seq_concat assms(1) by auto
qed

lemma rev_seq_dstep_concat : 
  assumes 
    ‹q ⇒$as q'› 
    ‹q'=⊳a q1›
  shows ‹q ⇒$(as@[a]) q1›
proof - 
  from assms(2) have ‹q' ⇒^a q1› using steps.refl by auto
  thus ?thesis using assms rev_seq_step_concat by auto
qed

lemma word_tau_concat: 
  assumes 
    ‹q ⇒$A q'›
    ‹q' ⇒^τ q1› 
  shows ‹q ⇒$A q1› 
proof - 
  from assms(2) have ‹q' ⇒$[] q1›
    using tau_tau weak_step_seq.simps(1) by blast 
  thus ?thesis using assms(1) rev_seq_concat
    by (metis append.right_neutral) 
qed

lemma list_rev_split : 
  assumes ‹A ≠ []›
  shows ‹∃as a. A = as@[a]›
proof - 
  show ?thesis using assms rev_exhaust by blast 
qed

primrec taufree :: ‹'a list ⇒ 'a list›
  where
    ‹taufree [] = []›
  | ‹taufree (a#A) = (if tau a then taufree A else a#(taufree A))›

lemma weak_step_over_tau : 
  assumes 
    ‹p ⇒$A p'›
  shows ‹p ⇒$(taufree A) p'› using assms
proof (induct A arbitrary: p)
  case Nil
  thus ?case by auto
next
  case (Cons a as)
  then obtain p0 where ‹p ⇒^a p0› ‹p0⇒$as p'› by auto
  then show ?case
  proof (cases ‹tau a›)
    case True
    hence ‹p ⇒$as p'› using tau_word_concat ‹p ⇒^a p0› ‹p0 ⇒$ as p'› tau_tau by blast
    hence ‹p ⇒$ (taufree as)  p'› using Cons by auto
    thus ‹p ⇒$ (taufree (a#as))  p'› using True by auto
  next
    case False
    hence rec: ‹taufree (a#as) = a#(taufree as)› by auto
    hence ‹p0 ⇒$ (taufree as)  p'› using ‹p0⇒$as p'› Cons by auto
    hence ‹p ⇒$(a#(taufree as)) p'› using  ‹p ⇒^a p0› by auto
    then show ?thesis using rec by auto
  qed
qed

lemma app_tau_taufree_list : 
  assumes 
    ‹∀a ∈ set A. ¬tau a›
    ‹b = τ›
  shows ‹A = taufree (A@[b])› using assms(1)
proof (induct A)
  case Nil
  then show ?case using assms by simp
next
  case (Cons x xs)
  have ‹∀a∈set xs. ¬ tau a› ‹¬tau x› using assms(1) butlast_snoc Cons by auto 
  hence last: ‹xs = taufree (xs @ [b])› using Cons by auto
  have ‹taufree (x#xs@[b]) = x#taufree (xs @ [b])› using ‹¬tau x› by auto
  hence ‹x # xs = x# taufree (xs@ [b])› using last by auto
  then show ?case using Cons.prems last by auto
qed

lemma word_steps_ignore_tau_addition:
  assumes
    ‹∀a∈set A. a ≠ τ›
    ‹p ⇒$ A p'›
    ‹filter (λa. a ≠ τ) A' = A›
  shows
    ‹p ⇒$ A' p'›
  using assms
proof (induct A' arbitrary: p A)
  case Nil': Nil
  then show ?case by simp
next
  case Cons': (Cons a' A' p)
  show ?case proof (cases ‹a' = τ›)
    case True
    with Cons'.prems have ‹filter (λa. a ≠ τ) A' = A› by simp
    with Cons' have ‹p ⇒$ A' p'› by blast
    with True show ?thesis using steps.refl by fastforce
  next
    case False
    with Cons'.prems obtain A'' where
      A''_spec: ‹A = a'#A''› ‹filter (λa. a ≠ τ) A' = A''› ‹∀a∈set A''. a ≠ τ › by auto
    with Cons'.prems obtain p0 where
      p0_spec: ‹p ⇒^a' p0› ‹p0 ⇒$ A'' p'› by auto
    with Cons'.hyps A''_spec(2,3) have ‹p0 ⇒$ A'  p'› by blast
    with p0_spec show ?thesis by auto
  qed
qed

lemma word_steps_ignore_tau_removal:
  assumes
    ‹p ⇒$ A p'›
  shows
    ‹p ⇒$ (filter (λa. a ≠ τ) A) p'›
  using assms
proof (induct A arbitrary: p)
  case Nil
  then show ?case by simp
next
  case (Cons a A)
  show ?case proof (cases ‹a = τ›)
    case True
    with Cons show ?thesis using tau_word_concat by auto
  next
    case False
    with Cons.prems obtain p0 where p0_spec: ‹p ⇒^a p0› ‹p0 ⇒$ A p'› by auto
    with Cons.hyps have ‹p0 ⇒$ (filter (λa. a ≠ τ) A) p'› by blast
    with ‹p ⇒^a p0› False show ?thesis by auto
  qed
qed

definition weak_tau_succs :: "'s set ⇒ 's set" where
  ‹weak_tau_succs Q  = {q1. ∃q∈ Q. q ⇒^τ q1}› 

definition dsuccs :: "'a ⇒ 's set ⇒ 's set" where
  ‹dsuccs a Q  = {q1. ∃q∈ Q. q =⊳a q1}› 

definition word_reachable_via_delay :: "'a list ⇒ 's ⇒ 's ⇒ 's ⇒ bool" where
  ‹word_reachable_via_delay A p p0 p1 = (∃p00. p ⇒$(butlast A) p00 ∧ p00 =⊳(last A) p0 ∧ p0 ⇒^τ p1)›

primrec dsuccs_seq_rec :: "'a list ⇒ 's set ⇒ 's set" where
  ‹dsuccs_seq_rec [] Q  = Q› | 
  ‹dsuccs_seq_rec (a#as) Q  = dsuccs a (dsuccs_seq_rec as Q)›

lemma in_dsuccs_implies_word_reachable:
  assumes 
    ‹q' ∈ dsuccs_seq_rec (rev A) {q}›
  shows
    ‹q ⇒$A q'›
  using assms
proof (induct arbitrary: q' rule: rev_induct) 
  case Nil
  hence ‹q' = q› by auto
  hence ‹q ⇒^τ q'› by (simp add: steps.refl) 
  thus ‹q ⇒$[] q'› by simp
next
  case (snoc a as)
  hence ‹q' ∈ dsuccs_seq_rec (a#(rev as)) {q}› by simp
  hence ‹q' ∈ dsuccs a (dsuccs_seq_rec (rev as) {q})› by simp
  then obtain q0 where ‹q0 ∈ dsuccs_seq_rec (rev as) {q}› 
    and ‹q0 =⊳a q'› using dsuccs_def  by auto
  hence ‹q ⇒$as q0› using snoc.hyps by auto
  thus ‹q ⇒$(as @ [a]) q'› 
    using ‹q0 =⊳a q'› steps.refl rev_seq_step_concat by blast 
qed

lemma word_reachable_implies_in_dsuccs : 
  assumes 
    ‹q ⇒$A q'›
  shows ‹q' ∈ weak_tau_succs (dsuccs_seq_rec (rev A) {q})› using assms
proof (induct A arbitrary: q' rule: rev_induct)
  case Nil
  hence ‹q ⇒^τ q'› using tau_tau weak_step_seq.simps(1) by blast 
  hence ‹q' ∈ weak_tau_succs {q}› using weak_tau_succs_def by auto
  thus ?case using dsuccs_seq_rec.simps(1) by auto
next
  case (snoc a as)
  then obtain q1 where ‹q ⇒$as q1› and ‹q1 ⇒^a q'› using rev_seq_split by blast 
  hence in_succs: ‹q1 ∈ weak_tau_succs (dsuccs_seq_rec (rev as) {q})› using snoc.hyps by auto
  then obtain q0 where q0_def: ‹q0 ∈ dsuccs_seq_rec (rev as) {q}› ‹q0 ⇒^τ q1› 
    using weak_tau_succs_def[of‹dsuccs_seq_rec (rev as) {q}›] by auto
  hence ‹q0 ⇒^a q'› using ‹q1 ⇒^a q'› steps_concat tau_tau by blast 
  then obtain q2 where ‹q0 =⊳a q2› ‹q2 ⇒^τ q'› using steps.refl by auto 
  hence ‹∃q0 ∈ dsuccs_seq_rec (rev as) {q}. q0 =⊳a q2› using q0_def by auto
  hence ‹q2 ∈ dsuccs a (dsuccs_seq_rec (rev as) {q})›  using dsuccs_def by auto
  hence ‹q2 ∈ dsuccs_seq_rec (a#(rev as)) {q}› by auto
  hence ‹q2 ∈ dsuccs_seq_rec (rev (as@[a])) {q}› by auto
  hence ‹∃q2 ∈ dsuccs_seq_rec (rev (as@[a])) {q}. q2 ⇒^τ q'› using ‹q2 ⇒^τ q'› by auto
  thus ?case using weak_tau_succs_def[of ‹dsuccs_seq_rec (rev (as@[a])) {q}›] by auto
qed

lemma simp_dsuccs_seq_rev: 
  assumes 
    ‹Q = dsuccs_seq_rec (rev A) {q0}›
  shows 
    ‹dsuccs a Q = dsuccs_seq_rec (rev (A@[a])) {q0}›
proof - 
  show ?thesis by (simp add: assms) 
qed

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› ―‹contracted cycles (anti-symmetry)›
    ‹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 ―‹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
  by (simp add: finite_prod)

end

end