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
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