Theory Transition_Systems

section ‹Preliminaries›

subsection ‹Labeled Transition Systems›

theory Transition_Systems
  imports Main
begin
  
locale lts =
fixes
  trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› ("_ ⟼_  _" [70, 70, 70] 80)

begin

abbreviation step_pred :: ‹'s ⇒ ('a ⇒ bool) ⇒ 's ⇒ bool›
  where
  ‹step_pred p af q ≡ ∃ a. af a ∧ trans p a q›

inductive steps :: ‹'s ⇒ ('a ⇒ bool) ⇒ 's ⇒ bool›
     ("_ ⟼* _  _" [70, 70, 70] 80)
where
  refl: ‹p ⟼* A p› | step: ‹p ⟼* A q1 ⟹ q1 ⟼a q ⟹ A a ⟹ (p ⟼* A q)›

lemma steps_one_step: 
  assumes
    ‹p ⟼a p'›
     ‹A a›
   shows
    ‹p ⟼* A p'› using steps.step[of p A p a p'] steps.refl[of p A] assms .

lemma steps_concat: 
  assumes
    ‹p' ⟼* A p''›
     ‹p ⟼* A p'›
   shows
    ‹p ⟼* A p''› using assms
proof (induct arbitrary: p)
  case (refl p'' A p')
  then show ?case by auto
next
  case (step p' A p'' a pp p)
  hence ‹p ⟼* A  p''› by simp
  show ?case using steps.step[OF `p ⟼* A  p''` step(3,4)] .
qed

lemma steps_left:
  assumes
    ‹p ≠ p'›
     ‹p ⟼* A p'›
   shows
    ‹∃p'' a . p ⟼a p'' ∧ A a ∧ p'' ⟼* A p'›
   using assms(1) 
  by (induct rule:steps.induct[OF assms(2)], blast, metis refl steps_concat steps_one_step) 

lemma steps_no_step:
  assumes
    ‹⋀ a p' . p ⟼a p' ⟹ ¬A a›
     ‹p ≠ p''›
     ‹p ⟼* A p''›
   shows
    ‹False›
   using steps_left[OF assms(2,3)] assms(1) by blast
    
lemma steps_no_step_pos:
  assumes
    ‹⋀ a p' . p ⟼a p' ⟹ ¬A a›
     ‹p ⟼* A p'›
   shows
    ‹p = p'›
   using assms steps_no_step by blast
    
lemma steps_loop:
  assumes
    ‹⋀ a p' . p ⟼a p' ⟹ p = p'›
     ‹p ≠ p''›
     ‹p ⟼* A p''›
   shows
    ‹False›
   using assms(3,1,2) by (induct, auto)

corollary steps_transp:
  ‹transp (λ p p'. p ⟼* A p')›
   using steps_concat unfolding transp_def by blast
  
lemma steps_spec: 
  assumes
    ‹p ⟼* A' p'›
     ‹⋀ a . A' a ⟹ A a›
   shows
    ‹p ⟼* A p'› using assms(1,2)
proof induct
  case (refl p)
  show ?case using steps.refl .
next
  case (step p A' pp a pp')
  hence ‹p ⟼* A  pp› by simp 
  then show ?case using step(3,4,5) steps.step by auto
qed

interpretation preorder ‹(λ p p'. p ⟼* A p')› ‹λ p p'. p ⟼* A p' ∧ ¬(p' ⟼* A p)›
  by (standard, simp, simp add: steps.refl, metis steps_concat)

text‹If one can reach only a finite portion of the graph following @{text ‹⟼* A›},
  and all cycles are loops, then there must be nodes which are maximal wrt. ‹⟼* A›.›
lemma step_max_deadlock:
  fixes A q
  assumes
    antiysmm: ‹⋀ r1 r2. r1 ⟼* A r2 ∧ r2 ⟼* A r1 ⟹ r1 = r2› and
    finite: ‹finite {q'. q ⟼* A q'}› and
    no_max: ‹∀ q'. q ⟼* A q' ⟶ (∃q''. q' ⟼* A q'' ∧ q' ≠ q'')›
   shows
    False
proof -
  interpret order ‹(λ p p'. p ⟼* A p')› ‹λ p p'. p ⟼* A p' ∧ ¬(p' ⟼* A p)›
    by (standard, simp add: assms(1))
  show ?thesis using assms order_trans order_refl finite_has_maximal2 mem_Collect_eq
    by metis
qed

end ―‹end of lts›

lemma lts_impl_steps2:
  assumes
    ‹lts.steps step1 p1 ap p2›
     ‹⋀ p1 a p2 . step1 p1 a p2 ∧ P p1 a p2 ⟹ step2 p1 a p2›
     ‹⋀ p1 a p2 . P p1 a p2›
   shows
    ‹lts.steps step2 p1 ap p2›
proof (induct rule: lts.steps.induct[OF assms(1)])
  case (1 p af)
  show ?case using lts.steps.refl[of step2 p af] by blast
next
  case (2 p af q1 a q)
  hence ‹step2 q1 a q› using assms(2,3) by blast
  thus ?case using lts.step[OF 2(2) _ 2(4)] by blast
qed 
  
lemma lts_impl_steps:
  assumes
    ‹lts.steps step1 p1 ap p2›
     ‹⋀ p1 a p2 . step1 p1 a p2 ⟹ step2 p1 a p2›
   shows
    ‹lts.steps step2 p1 ap p2›
   using assms lts_impl_steps2[OF assms] by auto
  
end