Theory Labeled_Transition_Systems

section ‹Labeled Transition Systems›

theory Labeled_Transition_Systems
  imports
    Main
begin

subsection ‹Labeled Transition Systems›

text ‹A locale for Labeled Transition Systems,
  parameterized over action type ‹'a› and state type ‹'s›.
›
locale lts = 
  fixes step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› 
    (‹_ ⟼_ _› [70, 70, 70] 80)
begin

text ‹Example definitions for derivatives and deadlock.›

abbreviation derivatives :: ‹'s ⇒ 'a ⇒ 's set› 
  where ‹derivatives p α ≡ {p'. p ⟼α p'}›

abbreviation deadlocked :: ‹'s ⇒ bool›
  where ‹deadlocked s ≡ ∀α. derivatives s α = {}›

definition image_finite :: ‹bool›
  where ‹image_finite ≡ (∀ p α. finite (derivatives p α))›

subsection ‹Paths and Traces›

text ‹Step sequences as inductive definition›

text ‹Teaching Hint: Inductive definitions!›
inductive step_sequence :: ‹'s ⇒ 'a list ⇒ 's ⇒ bool›
    ("_ ⟼$ _ _" [70, 70, 70] 80)
  where
  srefl: ‹p ⟼$ [] p› |
  sstep: ‹p ⟼$ (a#tr) p''› if ‹∃p'. p ⟼ a p' ∧ p' ⟼$ tr p''›

text ‹Traces as enabled step sequences›
abbreviation traces :: ‹'s ⇒ 'a list set› 
  where ‹traces p ≡ {tr. ∃p'. p ⟼$ tr p'}›

lemma empty_trace_trivial:
  fixes p
  shows ‹[] ∈ traces p›
  using step_sequence.srefl by blast

inductive path :: ‹'s list ⇒ bool›
  where
  init: ‹path [p]› |
  step: ‹path (p # (p' # pp))› if ‹∃α. p ⟼ α p' ∧ path (p' # pp)›

lemma no_empty_paths:
  assumes ‹path []›
  shows ‹False›
  using assms path.cases by blast

lemma path_implies_trace:
  assumes ‹path pp›
  shows ‹∃tr. (hd pp) ⟼$ tr (last pp)›
  using assms
proof induct
  case (init p)
  then show ?case using step_sequence.srefl by force
next
  case (step p p' pp)
  then show ?case by (metis last_ConsR list.distinct(1) list.sel(1) step_sequence.simps) 
qed

lemma trace_implies_path:
  assumes ‹p ⟼$ tr p'›
  shows ‹∃pp. path pp ∧ hd pp = p ∧ last pp = p'›
  using assms
proof induct
  case (srefl p)
  then show ?case using path.init by fastforce
next
  case (sstep p a tr p'')
  then show ?case by (metis last.simps list.collapse list.sel(1) no_empty_paths path.step)
qed

end ― ‹of ‹locale lts››

subsection ‹Transition Systems with Internal Behavior›

locale lts_tau =
  lts step
  for
    step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› (‹_ ⟼_ _› [70, 70, 70] 80) +
  fixes
    τ :: 'a 
begin

text ‹Define silent-reachability ‹↠› and prove its transitivity›
inductive silent_reachable :: ‹'s ⇒ 's ⇒ bool› (infix ‹↠› 80) where
  refl: ‹p ↠ p› |
  step: ‹p ↠ p''› if ‹p ⟼ τ p'› and ‹p' ↠ p''›

thm silent_reachable.induct

lemma silent_reachable_compose:
  fixes
    p p' p''
  assumes
    ‹p ↠ p'›
    ‹p' ↠ p''›
  shows 
    ‹p ↠ p''›
  using assms
proof induct
  fix p
  assume ‹p ↠ p''›
  thus ‹p ↠ p''› .
next
  fix p p' p'''
  assume ‹p ⟼τ p'› ‹p''' ↠ p'' ⟹ p' ↠ p''› ‹p''' ↠ p''›
  from this(2,3) have ‹p' ↠ p''› .
  with silent_reachable.step ‹p ⟼τ p'› show ‹p ↠ p''› .
qed

lemma silent_reachable_preorder:
   ‹reflp (↠)›
   ‹transp (↠)›
  using silent_reachable.refl silent_reachable_compose
  unfolding reflp_def transp_def by blast+

text ‹A weak step ‹↠⟼› is ‹⟼› wrapped in ‹↠› (or just ‹↠› for ‹τ›)›
definition weak_step (‹_ ↠⟼ _ _› [70,70,70] 80) where
  ‹p ↠⟼ α p''' ≡
    if α = τ then p ↠ p''' else
    (∃p' p''. p ↠ p' ∧ p' ⟼ α p'' ∧ p'' ↠ p''')›

text ‹weak step sequence ‹↠⟼$› and traces analogous to strong steps.›
inductive weak_step_sequence :: ‹'s ⇒ 'a list ⇒ 's ⇒ bool›
    ("_ ↠⟼$ _ _" [70, 70, 70] 80)
  where
  internal: ‹p ↠⟼$ [] p'› if ‹p ↠ p'› |
  step: ‹p ↠⟼$ (α#tr) p''› if ‹∃p'. p ↠⟼ α p' ∧ p' ↠⟼$ tr p''›

abbreviation weak_traces :: ‹'s ⇒ 'a list set› 
  where ‹weak_traces p ≡ {tr. ∃p'. p ↠⟼$ tr p'}›

lemma empty_weak_trace_trivial:
  fixes p
  shows ‹[] ∈ weak_traces p›
  using weak_step_sequence.internal silent_reachable.refl by blast

lemma weak_seq_tau_transparent:
  assumes ‹p ↠⟼$ tr p'›
  shows ‹p ↠⟼$ (filter (λα. α ≠ τ) tr) p'›
  using assms
proof (induct tr arbitrary: p p')
  case Nil
  then show ?case by simp
next
  case (Cons α tr p p'')
  from this(2) obtain p' where step1: ‹p ↠⟼ α p'› ‹p' ↠⟼$ tr p''›
    using weak_step_sequence.cases by force
  then have step2: ‹p' ↠⟼$ (filter (λα. α ≠ τ) tr) p''› using Cons(1) by blast
  show ?case
  proof (cases ‹α ≠ τ›)
    case True
    then show ?thesis using step1(1) step2
      using weak_step_sequence.step by fastforce
  next
    case False
    hence ‹α = τ› by blast
    hence ‹p ↠ p'› using step1(1) unfolding weak_step_def by auto
    hence ‹p ↠⟼$ tr p''› using step1(2) weak_step_def silent_reachable_compose
      by (smt (verit, best)
        weak_step_sequence.internal weak_step_sequence.cases weak_step_sequence.step)
    hence ‹p ↠⟼$ (filter (λα. α ≠ τ) tr) p''› using Cons.hyps by blast
    then show ?thesis using ‹α = τ› by auto
  qed
qed

end

end