Theory LTS_Automata

(* Authors: Tassilo Lemke, Tobias Nipkow *)

section‹LTS-based Automata›

theory LTS_Automata
imports Labeled_Transition_System
begin

text‹An automaton ‹M› is a triple ‹(T, S, F)›, where ‹T› is the transition system,
  ‹S› is the start state and ‹F› are the final states.
  This is just a thin layer on top of ‹lts›.
  NB: ‹T› may be infinite (but we require to finiteness in crucial places).›

record ('s, 't) auto =
  lts :: "('s, 't) lts"
  start :: 's
  finals :: "'s set"

text‹
  The language ‹L(M)› of an automaton ‹M› is defined as the set of words that
  reach at least one final state from the start state:
›

abbreviation accepts_auto :: "('s, 't) auto ⇒ 't list ⇒ bool" where
  "accepts_auto M ≡ accepts_lts (lts M) (start M) (finals M)"

abbreviation Lang_auto :: "('s, 't) auto ⇒ 't list set" where
  "Lang_auto M ≡ Lang_lts (lts M) (start M) (finals M)"


subsection ‹Sequential Composition of Automata›

text ‹We will later provide concrete example of automata accepting specific languages.
While proving that an automaton accepts a certain language often is straightforward,
proving that the automaton only accepts that language is a much more difficult task.
The lemma below provides a powerful tool to make these proofs manageable. It shows that
if two automata over disjoint state sets are connected via a single uni-directional bridge,
every word that reaches from the first set of states to a state within the second set of state must,
at some point, pass this bridge, and have a prefix within the first set of states
and a suffix within the second set.›

lemma auto_merge:
  assumes "sA ∈ A" and "fA ∈ A" and "sB ∈ B" and "fB ∈ B" and "A ∩ B = {}"
    and sideA: "∀(q,c,q') ∈ TA. q ∈ A ∧ q' ∈ A"
    and sideB: "∀(q,c,q') ∈ TB. q ∈ B ∧ q' ∈ B"
    and "fB ∈ steps_lts (TA ∪ {(fA, c, sB)} ∪ TB) w sA"
  shows "∃wA wB. w = wA@[c]@wB ∧ fA ∈ steps_lts TA wA sA ∧ fB ∈ steps_lts TB wB sB"
using assms(1,8) proof (induction w arbitrary: sA)
  case Nil
  then have "steps_lts (TA ∪ {(fA, c, sB)} ∪ TB) [] sA = {sA}"
    by (simp add: Steps_lts_def)
  then show ?case
    using Nil.prems assms(4,5) by fast
next
  case (Cons a w)
  define T where "T ≡ TA ∪ {(fA, c, sB)} ∪ TB"

  ― ‹Obtain intermediate state after reading ‹a›:›
  note ‹fB ∈ steps_lts (TA ∪ {(fA, c, sB)} ∪ TB) (a#w) sA›
  then obtain q where a_step: "q ∈ steps_lts T [a] sA"
    and w_step: "fB ∈ steps_lts T w q"
    unfolding T_def using Steps_lts_split by force

  ― ‹There are now two options:›
  ― ‹1. ‹a› directly traverses the bridge to ‹B›, so ‹a = c›.›
  ― ‹2. ‹a› remains within ‹A› and we can use the IH.›
  then show ?case
  proof (cases "(sA, a, q) ∉ TA")
    case True
    moreover have "(sA, a, q) ∉ TB"
      using Cons.prems(1) assms(5,7) by fast
    moreover have "(sA, a, q) ∈ T"
      using a_step by (auto simp: steps_lts_defs)
    ultimately have "sA = fA" and "a = c" and "q = sB"
      unfolding T_def by simp+

    have inB: "sB ∈ B ⟹ fB ∈ steps_lts T w sB ⟹ fB ∈ steps_lts TB w sB"
    proof (induction w arbitrary: sB)
      case Nil
      then show ?case
        by (simp add: Steps_lts_def)
    next
      case (Cons x xs)
      then obtain q where "fB ∈ steps_lts T xs q" and "q ∈ steps_lts T [x] sB"
        using Steps_lts_split by force
      then have "(sB, x, q) ∈ T"
        by (auto simp: steps_lts_defs)
      moreover have "sB ∈ B"
        using Cons by simp
      ultimately have "(sB, x, q) ∈ TB" and "q ∈ B"
        unfolding T_def using assms(2,5,6,7) by blast+
      then have "q ∈ steps_lts TB [x] sB"
        by (auto simp: steps_lts_defs) force
      moreover have "fB ∈ steps_lts TB xs q"
        using ‹fB ∈ steps_lts T xs q› ‹q ∈ B› Cons by simp
      ultimately show ?case
        using Steps_lts_join by force
    qed

    ― ‹The bridge is directly traversed, so ‹A› can be ignored:›
    have "a#w = []@[c]@w"
      by (simp add: ‹a = c›)
    moreover have "fA ∈ steps_lts TA [] sA"
      by (simp add: ‹sA = fA› Steps_lts_def)
    moreover have "fB ∈ steps_lts TB w sB"
      using w_step assms(3) inB by (simp add: ‹q = sB›)
    ultimately show ?thesis
      by blast
  next
    case False
    then have a_step': "q ∈ steps_lts TA [a] sA"
      by (auto simp: steps_lts_defs) (force)
    then have "q ∈ A"
      using False Cons.prems(1) assms(6) by fast

    ― ‹Introduce the IH:›
    then have "∃wA wB. w = wA @[c]@wB ∧ fA ∈ steps_lts TA wA q ∧ fB ∈ steps_lts TB wB sB"
      by (rule Cons.IH; use Cons.prems w_step[unfolded T_def] in simp)
    then obtain wA wB where "w = wA @[c]@wB" and "fA ∈ steps_lts TA wA q" and "fB ∈ steps_lts TB wB sB"
      by blast
    moreover then have "fA ∈ steps_lts TA (a#wA) sA"
      using a_step' Steps_lts_join by force
    ultimately have "a#w = a#wA@[c]@wB ∧ fA ∈ steps_lts TA (a#wA) sA ∧ fB ∈ steps_lts TB wB sB"
      by simp
    then show ?thesis
      by (intro exI) auto
  qed
qed


subsection‹Concrete Automata›

text ‹We now present three concrete automata that accept certain languages.›

subsubsection ‹Universe over specific Alphabet›

text‹This automaton accepts exactly the words that only contains letters from a given alphabet ‹Σ›.›

definition loop_lts :: "'s ⇒ 'a set ⇒ ('s × 'a × 's) set" where
  "loop_lts q Σ ≡ {q} × Σ × {q}"

lemma loop_lts_fin: "finite Σ ⟹ finite (loop_lts q Σ)"
  by (simp add: loop_lts_def)

lemma loop_lts_correct1: "set w ⊆ Σ ⟹ steps_lts (loop_lts q Σ) w q = {q}"
proof (induction w)
  case Nil
  then show ?case
    by (simp add: Steps_lts_def)
next
  case (Cons w ws)
  then have "steps_lts (loop_lts q Σ) [w] q = {q}"
    unfolding loop_lts_def steps_lts_defs by fastforce
  moreover have "steps_lts (loop_lts q Σ) ws q = {q}"
    using Cons by simp
  ultimately show ?case
    by (simp add: Steps_lts_def)
qed

lemma loop_lts_correct2: "¬ set w ⊆ Σ ⟹ steps_lts (loop_lts q Σ) w q = {}"
proof (induction w)
  case Nil
  then show ?case 
    by simp
next
  case (Cons w ws)
  then consider "w ∉ Σ" | "¬ set ws ⊆ Σ"
    by auto
  then show ?case
  proof (cases)
    case 1
    then have "steps_lts (loop_lts q Σ) [w] q = {}"
      by (auto simp: loop_lts_def steps_lts_defs)
    moreover have "Steps_lts (loop_lts q Σ) ws {} = {}"
      by (meson Steps_lts_path ex_in_conv)
    ultimately show ?thesis
      by (metis Steps_lts_split all_not_in_conv append_Cons append_Nil)
  next
    case 2
    then have "steps_lts (loop_lts q Σ) ws q = {}"
      using Cons by simp
    moreover have "steps_lts (loop_lts q Σ) [w] q ⊆ {q}"
      by (auto simp: loop_lts_def steps_lts_defs)
    ultimately show ?thesis
      by (metis Steps_lts_def Steps_lts_mono Un_insert_right ex_in_conv fold_simps(1,2) insert_absorb insert_not_empty sup.absorb_iff1)
  qed
qed

lemmas loop_lts_correct = loop_lts_correct1 loop_lts_correct2

definition auto_univ :: "'a set ⇒ (unit, 'a) auto" where
  "auto_univ Σ ≡ ⦇
    lts = loop_lts () Σ,
    start = (),
    finals = {()}
  ⦈"

lemma auto_univ_lang[simp]: "Lang_auto (auto_univ Σ) = {w. set w ⊆ Σ}"
proof -
  define T where "T ≡ loop_lts () Σ"
  have "⋀w. set w ⊆ Σ ⟷ () ∈ steps_lts T w ()"
    unfolding T_def using loop_lts_correct by fast
  then show ?thesis
    by (auto simp: T_def auto_univ_def)
qed


subsubsection‹Fixed Character with Arbitrary Prefix/Suffix›

text‹
  This automaton accepts exactly those words that contain a specific letter ‹c› at some point,
  and whose prefix and suffix are contained within the alphabets ‹Σp› and ‹Σs›.
›

definition pcs_lts :: "'a set ⇒ 'a ⇒ 'a set ⇒ (nat × 'a × nat) set" where
  "pcs_lts Σp c Σs ≡ loop_lts 0 Σp ∪ {(0, c, 1)} ∪ loop_lts 1 Σs"

lemma pcs_lts_fin: "finite Σp ⟹ finite Σs ⟹ finite (pcs_lts Σp c Σs)"
  by (auto intro: loop_lts_fin simp: pcs_lts_def)

lemma pcs_lts_correct1:
  "(∃p s. w = p@[c]@s ∧ set p ⊆ Σp ∧ set s ⊆ Σs) ⟹ 1 ∈ steps_lts (pcs_lts Σp c Σs) w 0"
proof -
  assume "∃p s. w = p@[c]@s ∧ set p ⊆ Σp ∧ set s ⊆ Σs"
  then obtain p s where "w = p@[c]@s" and "set p ⊆ Σp" and "set s ⊆ Σs"
    by blast
  moreover hence "0 ∈ steps_lts (pcs_lts Σp c Σs) p 0"
    by (metis pcs_lts_def steps_lts_union loop_lts_correct1 singletonI)
  moreover have "1 ∈ steps_lts (pcs_lts Σp c Σs) [c] 0"
    unfolding pcs_lts_def steps_lts_defs by force
  moreover have "1 ∈ steps_lts (pcs_lts Σp c Σs) s 1"
    by (metis calculation(3) inf_sup_ord(3) insertI1 pcs_lts_def steps_lts_mono' loop_lts_correct1 sup_commute)
  ultimately show "1 ∈ steps_lts (pcs_lts Σp c Σs) w 0"
    using Steps_lts_join by meson
qed

lemma pcs_lts_correct2:
  assumes "1 ∈ steps_lts (pcs_lts Σp c Σs) w 0"
  shows "∃p s. w = p@[c]@s ∧ set p ⊆ Σp ∧ set s ⊆ Σs"
proof -
  define TA where [simp]: "TA ≡ loop_lts (0::nat) Σp"
  define TB where [simp]: "TB ≡ loop_lts (1::nat) Σs"

  have "1 ∈ steps_lts (TA ∪ {(0, c, 1)} ∪ TB) w 0"
    using assms by (simp add: pcs_lts_def)
  then have "∃wA wB. w = wA@[c]@wB ∧ 0 ∈ steps_lts TA wA 0 ∧ 1 ∈ steps_lts TB wB 1"
    by (intro auto_merge[where A="{0}" and B="{1}"]) (simp add: loop_lts_def)+
  then obtain wA wB where w_split: "w = wA@[c]@wB" and "0 ∈ steps_lts TA wA 0" and "1 ∈ steps_lts TB wB 1"
    by blast
  then have "set wA ⊆ Σp" and "set wB ⊆ Σs"
    using loop_lts_correct2 by fastforce+
  then show ?thesis
    using w_split by blast
qed

lemmas pcs_lts_correct = pcs_lts_correct1 pcs_lts_correct2

definition cps_auto :: "'a ⇒ 'a set ⇒ (nat, 'a) auto" where
  "cps_auto c Σ ≡ ⦇
    lts = pcs_lts Σ c Σ,
    start = 0,
    finals = {1}
  ⦈"

lemma cps_auto_lang: "Lang_auto (cps_auto c U) = { α@[c]@β | α β. set α ⊆ U ∧ set β ⊆ U }"
  using pcs_lts_correct unfolding cps_auto_def
  by (metis (lifting) disjoint_insert(2) inf_bot_right select_convs(1,2,3))


subsubsection‹Singleton Language›

text‹
  Last but not least, the automaton accepting exactly a single word can be inductively defined.
›

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

fun word_lts :: "'a list ⇒ (nat × 'a × nat) set" where
  "word_lts (w#ws) = word_lts ws ∪ {(Suc (length ws), w, length ws)}" |
  "word_lts [] = {}"

lemma word_lts_domain:
  "(q, c, q') ∈ word_lts ws ⟹ q ≤ length ws ∧ q' ≤ length ws"
  by (induction ws) auto

definition word_auto :: "'a list ⇒ (nat, 'a) auto" where
  "word_auto ws ≡ ⦇ lts = word_lts ws, start = length ws, finals = {0} ⦈"

lemma word_lts_correct1:
  "0 ∈ steps_lts (word_lts ws) ws (length ws)"
proof (induction ws)
  case Nil
  then show ?case
    by (simp add: Steps_lts_def)
next
  case (Cons w ws)
  have "0 ∈ steps_lts (word_lts ws) ws (length ws)"
    using Cons.IH(1) by blast
  then have "0 ∈ steps_lts (word_lts (w#ws)) ws (length ws)"
    using steps_lts_mono' by (metis word_lts.simps(1) sup_ge1)
  moreover have "length ws ∈ steps_lts (word_lts (w#ws)) [w] (Suc (length ws))"
  proof -
    have "(Suc (length ws), w, length ws) ∈ word_lts (w#ws)"
      by simp
    then show ?thesis
      unfolding steps_lts_defs by force
  qed
  ultimately show ?case
    using Steps_lts_join by force
qed

lemma word_lts_correct2:
  "0 ∈ steps_lts (word_lts ws) ws' (length ws) ⟹ ws = ws'"
proof (induction ws arbitrary: ws')
  case Nil
  then show ?case
    by (simp, metis equals0D steps_lts_empty_lts)
next
  case (Cons w ws)

  ― ‹Preparation to use @{thm [source] auto_merge}:›
  define TB where [simp]: "TB ≡ word_lts ws"
  define B where [simp]: "B ≡ {n. n ≤ length ws}"
  define T where [simp]: "T ≡ {} ∪ {(Suc (length ws), w, length ws)} ∪ TB"

  ― ‹Apply @{thm [source] auto_merge}:›
  have "0 ∈ steps_lts T ws' (length (w#ws))"
    using Cons.prems by simp
  moreover have "∀(q, c, q')∈TB. q ∈ B ∧ q' ∈ B"
    using word_lts_domain by force
  ultimately have "∃wA wB. ws' = wA@[w]@wB ∧ (Suc (length ws)) ∈ steps_lts {} wA (Suc (length ws)) ∧ 0 ∈ steps_lts TB wB (length ws)"
    by (intro auto_merge[where A="{Suc (length ws)}" and B=B]) simp+
  then obtain wA wB where ws'_split: "ws' = wA@[w]@wB"
      and wA_step: "(length (w#ws)) ∈ steps_lts {} wA (length (w#ws))"
      and wB_step: "0 ∈ steps_lts TB wB (length ws)"
    by force

  have "wA = []"
    using wA_step steps_lts_empty_lts by fast

  ― ‹Use IH to show that ‹wB = ws›:›
  have "ws = wB"
    by (intro Cons.IH, use wB_step in simp)

  then show ?case
    using ws'_split by (simp add: ‹wA = []› ‹ws = wB›)
qed

lemmas word_lts_correct = word_lts_correct1 word_lts_correct2

lemma word_auto_lang[simp]: "Lang_auto (word_auto w) = {w}"
  unfolding word_auto_def using word_lts_correct[of w] by auto

lemma word_auto_finite_lts: "finite (lts (word_auto w))"
proof -
  have "finite (word_lts w)"
    by (induction w) simp+
  then show ?thesis
    by (simp add: word_auto_def)
qed

hide_const (open) lts start finals (* hide common names *)
term auto.start (* qualified names still work *)

end