# Theory Transition_Systems

theory Transition_Systems
imports Finite_Partial_Order
```subsection ‹Labeled Transition Systems›

theory Transition_Systems
imports Finite_Partial_Order
begin

locale lts =
fixes
trans :: ‹'s ⇒ 'a ⇒ 's ⇒ bool›

begin

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

abbreviation step ::
‹'s ⇒ 'a ⇒ 's ⇒ bool›
("_ ⟼_  _" [70, 70, 70] 80)
where
‹p ⟼a  q ≡ 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›.›
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 local.finite_max assms local.order_trans 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```