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