Theory Labeled_Transition_System

(* Authors: Tassilo Lemke, Tobias Nipkow *)

section‹Labeled Transition System›

text ‹This theory could be unified with ‹AFP/Labeled_Transition_Systems››

theory Labeled_Transition_System
  imports Main
begin

text ‹Labeled Transition Systems are sets of triples of type @{typ "'s × 'a × 's"}.›

type_synonym ('s, 'l) lts = "('s × 'l × 's) set"

text‹The following lemma ensure that Isabelle can evaluate set comprehensions over triples.›
lemma Collect_triple_code[code_unfold]:
  "{(x,y,z) ∈ A. P x y z} = {p ∈ A. P (fst p) (fst (snd p)) (snd (snd p))}"
  by fastforce

subsection‹Step Relations›

text‹
  A step from a state ‹q› over a single symbol ‹c› is the set of all ‹q'›, such that ‹(q, c, q') ∈ T›:
›

definition step_lts :: "('s, 'l) lts ⇒ 'l ⇒ 's ⇒ 's set" where
  "step_lts T c s = (λ(q, c, q'). q') ` {(q, c', q') ∈ T. c = c' ∧ q = s}"

text‹
  A step of a single symbol ‹c› from a set of states ‹S› is the union of @{const step_lts} over ‹S›:
›

definition Step_lts :: "('s, 'l) lts ⇒ 'l ⇒ 's set ⇒ 's set" where
  "Step_lts T c S = ⋃(step_lts T c ` S)"

text‹
  Repeated steps of a word ‹w› consisting of multiple letters is achieved using a standard @{term fold}:
›

definition Steps_lts :: "('s, 'l) lts ⇒ 'l list ⇒ 's set ⇒ 's set" where
  "Steps_lts T w s = fold (Step_lts T) w s"

text‹Often, merely a single starting-state is of relevance:›

abbreviation steps_lts :: "('s, 'l) lts ⇒ 'l list ⇒ 's ⇒ 's set" where
  "steps_lts T w s ≡ Steps_lts T w {s}"

lemmas steps_lts_defs = step_lts_def Step_lts_def Steps_lts_def

text‹
  We now prove some key properties of this step relation:
›

lemma Step_union: "Step_lts T w (S⇩1 ∪ S⇩2) = Step_lts T w S⇩1 ∪ Step_lts T w S⇩2"
  unfolding Step_lts_def by blast

lemma Steps_lts_mono: "s⇩1 ⊆ s⇩2 ⟹ Steps_lts T w s⇩1 ⊆ Steps_lts T w s⇩2"
proof (induction w arbitrary: s⇩1 s⇩2)
  case Nil thus ?case by (simp add: Steps_lts_def)
next
  case (Cons w ws)

  define s⇩1' where [simp]: "s⇩1' ≡ Step_lts T w s⇩1"
  define s⇩2' where [simp]: "s⇩2' ≡ Step_lts T w s⇩2"
  
  have "s⇩1' ⊆ s⇩2'"
    by (simp add: Step_lts_def, use ‹s⇩1 ⊆ s⇩2› in blast)
  then have "Steps_lts T ws s⇩1' ⊆ Steps_lts T ws s⇩2'"
    by (elim Cons.IH)
  moreover have "Steps_lts T (w#ws) s⇩1 = Steps_lts T ws s⇩1'"
    by (simp add: Steps_lts_def)
  moreover have "Steps_lts T (w#ws) s⇩2 = Steps_lts T ws s⇩2'"
    by (simp add: Steps_lts_def)
  ultimately show ?case
    by simp
qed

lemma Steps_lts_mono2:
  assumes "T⇩1 ⊆ T⇩2" and "q⇩1 ⊆ q⇩2"
  shows "Steps_lts T⇩1 w q⇩1 ⊆ Steps_lts T⇩2 w q⇩2"
using assms(2) proof (induction w arbitrary: q⇩1 q⇩2)
  case Nil thus ?case by (simp add: Steps_lts_def)
next
  case (Cons w ws)
  have "Step_lts T⇩1 w q⇩1 ⊆ Step_lts T⇩2 w q⇩2"
    unfolding steps_lts_defs using assms(1) Cons(2) by blast
  then have "Steps_lts T⇩1 ws (Step_lts T⇩1 w q⇩1) ⊆ Steps_lts T⇩1 ws (Step_lts T⇩2 w q⇩2)"
    by (rule Steps_lts_mono)
  then have "Steps_lts T⇩1 ws (Step_lts T⇩1 w q⇩1) ⊆ Steps_lts T⇩2 ws (Step_lts T⇩2 w q⇩2)"
    using Cons(1) by blast
  then show ?case
    by (simp add: Steps_lts_def)
qed

lemma steps_lts_mono: "T⇩1 ⊆ T⇩2 ⟹ steps_lts T⇩1 w q ⊆ steps_lts T⇩2 w q"
  using Steps_lts_mono2[of T⇩1 T⇩2 "{q}" "{q}" w] by simp

lemma steps_lts_mono': "T⇩1 ⊆ T⇩2 ⟹ q' ∈ steps_lts T⇩1 w q ⟹ q' ∈ steps_lts T⇩2 w q"
proof -
  assume "T⇩1 ⊆ T⇩2"
  then have "steps_lts T⇩1 w q ⊆ steps_lts T⇩2 w q"
    by (rule steps_lts_mono)
  then show "q' ∈ steps_lts T⇩1 w q ⟹ q' ∈ steps_lts T⇩2 w q"
    by blast
qed

lemma steps_lts_union: "q' ∈ steps_lts T w q ⟹ q' ∈ steps_lts (T ∪ T') w q"
proof -
  have "T ⊆ (T ∪ T')"
    by simp
  then show "q' ∈ steps_lts T w q ⟹ q' ∈ steps_lts (T ∪ T') w q"
    by (rule steps_lts_mono')
qed

lemma Steps_lts_path:
  assumes "q⇩f ∈ Steps_lts T w s"
  shows "∃q⇩0 ∈ s. q⇩f ∈ steps_lts T w q⇩0"
proof (insert assms; induction w arbitrary: s)
  case Nil thus ?case by (simp add: Steps_lts_def)
next
  case (Cons w ws)
  then have "q⇩f ∈ Steps_lts T ws (Step_lts T w s)"
    by (simp add: Steps_lts_def)
  moreover obtain q⇩0 where "q⇩0 ∈ (Step_lts T w s)" and "q⇩f ∈ steps_lts T ws q⇩0"
    using Cons.IH calculation by blast
  ultimately obtain q' where "q⇩0 ∈ step_lts T w q'" and "q' ∈ s"
    unfolding steps_lts_defs by blast

  note ‹q⇩0 ∈ step_lts T w q'› and ‹q⇩f ∈ steps_lts T ws q⇩0›
  then have "q⇩f ∈ Steps_lts T ws (step_lts T w q')"
    using Steps_lts_mono[of "{q⇩0}"] by blast
  moreover have "Steps_lts T ws (step_lts T w q') = steps_lts T (w#ws) q'"
    by (simp add: steps_lts_defs)
  ultimately show ?case
    using ‹q' ∈ s› by blast
qed

lemma Steps_lts_split:
  assumes "q⇩f ∈ Steps_lts T (w⇩1@w⇩2) Q⇩0"
  shows "∃q'. q' ∈ Steps_lts T w⇩1 Q⇩0 ∧ q⇩f ∈ steps_lts T w⇩2 q'"
proof -
  define Q⇩f where [simp]: "Q⇩f = Steps_lts T (w⇩1@w⇩2) Q⇩0"
  define Q' where [simp]: "Q' = Steps_lts T w⇩1 Q⇩0"
  have "Q⇩f = Steps_lts T w⇩2 Q'"
    by (simp add: Steps_lts_def)
  then obtain q' where "q' ∈ Q'" and "q⇩f ∈ steps_lts T w⇩2 q'"
    using assms Steps_lts_path by force
  moreover have "q' ∈ Steps_lts T w⇩1 Q⇩0"
    using calculation by simp
  ultimately show ?thesis
    by blast
qed

lemma Steps_lts_join:
  assumes "q' ∈ Steps_lts T w⇩1 Q⇩0" and "q⇩f ∈ steps_lts T w⇩2 q'"
  shows "q⇩f ∈ Steps_lts T (w⇩1@w⇩2) Q⇩0"
proof -
  define Q' where [simp]: "Q' = Steps_lts T w⇩1 Q⇩0"
  define Q⇩f where [simp]: "Q⇩f = Steps_lts T w⇩2 Q'"

  have "{q'} ⊆ Q'"
    using assms(1) by simp
  then have "Steps_lts T w⇩2 {q'} ⊆ Steps_lts T w⇩2 Q'"
    using Steps_lts_mono by blast
  then have "q⇩f ∈ Steps_lts T w⇩2 Q'"
    using assms(2) by fastforce
  moreover have "Q⇩f = Steps_lts T (w⇩1@w⇩2) Q⇩0"
    by (simp add: Steps_lts_def)
  ultimately show ?thesis
    by simp
qed

lemma Steps_lts_split3:
  assumes "q⇩f ∈ Steps_lts T (w⇩1@w⇩2@w⇩3) Q⇩0"
  shows "∃q' q''. q' ∈ Steps_lts T w⇩1 Q⇩0 ∧ q'' ∈ steps_lts T w⇩2 q' ∧ q⇩f ∈ steps_lts T w⇩3 q''"
proof -
  obtain q' where "q' ∈ Steps_lts T (w⇩1@w⇩2) Q⇩0 ∧ q⇩f ∈ steps_lts T w⇩3 q'"
    using assms Steps_lts_split[where w⇩1 = "w⇩1@w⇩2"] by fastforce
  moreover then obtain q'' where "q'' ∈ Steps_lts T w⇩1 Q⇩0 ∧ q' ∈ steps_lts T w⇩2 q''"
    using Steps_lts_split by fast
  ultimately show ?thesis
    by blast
qed

lemma Steps_lts_join3:
  assumes "q' ∈ steps_lts T w⇩1 q⇩0" and "q'' ∈ steps_lts T w⇩2 q'" and "q⇩f ∈ steps_lts T w⇩3 q''"
  shows "q⇩f ∈ steps_lts T (w⇩1@w⇩2@w⇩3) q⇩0"
proof -
  have "q⇩f ∈ steps_lts T (w⇩2@w⇩3) q'"
    using assms(2) assms(3) Steps_lts_join by fast
  moreover then have "q⇩f ∈ steps_lts T (w⇩1@w⇩2@w⇩3) q⇩0"
    using assms(1) Steps_lts_join by fast
  ultimately show ?thesis
    by blast
qed

lemma Steps_lts_noState: "Steps_lts T w {} = {}"
proof (induction w)
  case Nil
  then show ?case
    by (simp add: Steps_lts_def)
next
  case (Cons w ws)
  moreover have "Steps_lts T [w] {} = {}"
    by (simp add: steps_lts_defs)
  ultimately show ?case
    by (simp add: Steps_lts_def)
qed


subsection‹Reachable States›

definition reachable_from :: "('s, 'l) lts ⇒ 's ⇒ 's set" where
  "reachable_from T q ≡ {q'. ∃w. q' ∈ steps_lts T w q}"

lemma reachable_from_computable: "reachable_from T q ⊆ {q} ∪ (snd ` snd ` T)"
proof
  fix q'
  assume "q' ∈ reachable_from T q"
  then obtain w where w_def: "q' ∈ steps_lts T w q"
    unfolding reachable_from_def by blast
  then consider "w = []" | "∃ws c. w = ws@[c]"
    by (meson rev_exhaust)
  then show "q' ∈ {q} ∪ (snd ` snd ` T)"
  proof (cases)
    case 1
    then show ?thesis
      using w_def Steps_lts_def by force
  next
    case 2
    then obtain ws c where "w = ws@[c]"
      by blast
    then obtain q1 where "q1 ∈ steps_lts T ws q" and "q' ∈ steps_lts T [c] q1"
      using Steps_lts_split w_def by fast
    then have "(q1, c, q') ∈ T"
      by (auto simp: steps_lts_defs)
    then show ?thesis
      by force
  qed
qed

lemma reachable_from_trans[trans]:
  assumes "q1 ∈ reachable_from T q0" and "q2 ∈ reachable_from T q1"
  shows "q2 ∈ reachable_from T q0"
  using assms Steps_lts_join unfolding reachable_from_def by fast

lemma reachable_add_trans:
  assumes "∀(q1, _, q2) ∈ T'. ∃w. q2 ∈ steps_lts T w q1"
  shows "reachable_from T q = reachable_from (T ∪ T') q"
proof (standard; standard)
  fix q'
  assume "q' ∈ reachable_from T q"
  then show "q' ∈ reachable_from (T ∪ T') q"
    unfolding reachable_from_def using steps_lts_union by fast
next
  fix q'
  assume "q' ∈ reachable_from (T ∪ T') q"
  then obtain w where "q' ∈ steps_lts (T ∪ T') w q"
    unfolding reachable_from_def by blast
  then have "∃w'. q' ∈ steps_lts T w' q"
  proof (induction w arbitrary: q)
    case Nil
    then have "q = q'" and "q ∈ steps_lts T [] q"
      unfolding Steps_lts_def by simp+
    then show ?case
      by blast
  next
    case (Cons c w)
    then obtain q1 where "q' ∈ steps_lts (T ∪ T') w q1" and "q1 ∈ steps_lts (T ∪ T') [c] q"
      using Steps_lts_split[where w⇩1="[c]" and w⇩2=w] by force
    then obtain w' where w'_def: "q' ∈ steps_lts T w' q1"
      using Cons by blast

    have "q1 ∈ step_lts (T ∪ T') c q"
      using ‹q1 ∈ steps_lts (T ∪ T') [c] q› by (simp add: steps_lts_defs)
    then consider "q1 ∈ step_lts T c q" | "q1 ∈ step_lts T' c q"
      unfolding step_lts_def by blast
    then show ?case
    proof (cases)
      case 1
      then have "q1 ∈ steps_lts T [c] q"
        by (simp add: steps_lts_defs)
      then have "q' ∈ steps_lts T (c#w') q"
        using w'_def Steps_lts_join by force
      then show ?thesis
        by blast
    next
      case 2
      then have "(q, c, q1) ∈ T'"
        by (auto simp: step_lts_def)
      then obtain w'' where "q1 ∈ steps_lts T w'' q"
        using assms by blast
      then have "q' ∈ steps_lts T (w''@w') q"
        using w'_def Steps_lts_join by fast
      then show ?thesis
        by blast
    qed
  qed
  then show "q' ∈ reachable_from T q"
    by (simp add: reachable_from_def)
qed


definition states_lts :: "('s,'a)lts ⇒ 's set" where
"states_lts T = (⋃(p,a,q)∈T. {p,q})"

lemma Step_states_lts: "states_lts T ⊆ Q ⟹ Q0 ⊆ Q ⟹ Step_lts T a Q0 ⊆ Q"
  unfolding Step_lts_def step_lts_def states_lts_def by auto

lemma Steps_states_lts: assumes "states_lts T ⊆ Q" shows "Q0 ⊆ Q ⟹ Steps_lts T u Q0 ⊆ Q"
  unfolding Steps_lts_def
  apply(induction u arbitrary: Q0)
   apply simp
  using assms by (simp add: Step_states_lts)

corollary steps_states_lts: "⟦ states_lts T ⊆ Q; q ∈ Q ⟧ ⟹ steps_lts T u q ⊆ Q"
  using Steps_states_lts[of T Q "{q}"] by blast

lemma states_lts_Un: "states_lts (T ∪ T') = states_lts T ∪ states_lts T'"
  unfolding states_lts_def by auto


subsection‹Language›

abbreviation accepts_lts :: "('s, 'l) lts ⇒ 's ⇒ 's set ⇒ 'l list ⇒ bool" where
  "accepts_lts T s F w ≡ (steps_lts T w s ∩ F ≠ {})"

abbreviation Lang_lts :: "('s, 'l) lts ⇒ 's ⇒ 's set ⇒ ('l list) set" where
  "Lang_lts T S F ≡ { w. accepts_lts T S F w }"

(* unused
lemma Lang_lts_trans:
  assumes "s' ∈ steps_lts T w⇩1 s" and "w⇩2 ∈ Lang_lts T s' F"
  shows "(w⇩1@w⇩2) ∈ Lang_lts T s F"
proof -
  obtain q⇩f where "q⇩f ∈ steps_lts T w⇩2 s'" and "q⇩f ∈ F"
    using assms(2) by blast
  moreover have "q⇩f ∈ steps_lts T (w⇩1@w⇩2) s"
    using assms(1) ‹q⇩f ∈ steps_lts T w⇩2 s'› by (rule Steps_lts_join)
  ultimately show ?thesis
    using ‹q⇩f ∈ F› by blast
qed

lemma Lang_lts_split:
  assumes "(w⇩1@w⇩2) ∈ Lang_lts T q F"
  obtains q' where "q' ∈ steps_lts T w⇩1 q" and "w⇩2 ∈ Lang_lts T q' F"
proof -
  obtain q⇩f where "q⇩f ∈ steps_lts T (w⇩1@w⇩2) q" and "q⇩f ∈ F"
    using assms by blast
  then obtain q' where "q' ∈ steps_lts T w⇩1 q" and "q⇩f ∈ steps_lts T w⇩2 q'"
    using Steps_lts_split by fast
  moreover then have "w⇩2 ∈ Lang_lts T q' F"
    using ‹q⇩f ∈ F› by blast
  ultimately show ?thesis
    using that by blast
qed

lemma Lang_steps_lts_mono: "T⇩1 ⊆ T⇩2 ⟹ Lang_lts T⇩1 s f ⊆ Lang_lts T⇩2 s f"
  using steps_lts_mono[of T⇩1 T⇩2] by fast
*)

end