Theory FSM

(*  Title:       Finite state machines
    ID:
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section ‹ Finite state machines ›
theory FSM
imports DPN_Setup
begin

text ‹
  This theory models nondeterministic finite state machines with explicit set of states and alphabet. @{text ε}-transitions are not supported.
›

subsection ‹ Definitions ›

record ('s,'a) FSM_rec =
  Q :: "'s set" ― ‹The set of states›
  Σ :: "'a set" ― ‹The alphabet›
  δ :: "('s, 'a) LTS" ― ‹The transition relation›
  s0 :: "'s" ― ‹The initial state›
  F :: "'s set" ― ‹The set of final states›

locale FSM = 
  fixes A
  assumes delta_cons: "(q,l,q')∈δ A ⟹ q∈Q A ∧ l∈Σ A ∧ q'∈Q A" ― ‹The transition relation is consistent with the set of states and the alphabet›
  assumes s0_cons: "s0 A ∈ Q A" ― ‹The initial state is a state›
  assumes F_cons: "F A ⊆ Q A" ― ‹The final states are states›
  assumes finite_states: "finite (Q A)" ― ‹The set of states is finite›
  assumes finite_alphabet: "finite (Σ A)" ― ‹The alphabet is finite›

subsection ‹ Basic properties ›
lemma (in FSM) finite_delta_dom: "finite (Q A × Σ A × Q A)" proof -
  from finite_states finite_alphabet finite_cartesian_product[of "Σ A" "Q A"] have "finite (Σ A × Q A)" by fast
  with finite_states finite_cartesian_product[of "Q A" "Σ A × Q A"] show "finite (Q A × Σ A × Q A)" by fast
qed

lemma (in FSM) finite_delta: "finite (δ A)" proof -
  have "δ A ⊆ Q A × Σ A × Q A" by (auto simp add: delta_cons)
  with finite_delta_dom show ?thesis by (simp add: finite_subset)
qed

subsection ‹Constructing FSMs›

definition "fsm_empty s⇩0 ≡ ⦇ Q={s⇩0}, Σ={}, δ={}, s0=s⇩0, F={} ⦈"
definition "fsm_add_F s fsm ≡ fsm⦇ Q:=insert s (Q fsm), F:=insert s (F fsm) ⦈"
definition "fsm_add_tr q a q' fsm ≡ fsm⦇ Q:={q,q'} ∪ (Q fsm), Σ:=insert a (Σ fsm), δ := insert (q,a,q') (δ fsm) ⦈"

lemma fsm_empty_invar[simp]: "FSM (fsm_empty s)"
  apply unfold_locales unfolding fsm_empty_def by auto
  
lemma fsm_add_F_invar[simp]: assumes "FSM fsm" shows "FSM (fsm_add_F s fsm)"  
proof -
  interpret FSM fsm by fact
  show ?thesis
    apply unfold_locales
    unfolding fsm_add_F_def
    using delta_cons s0_cons F_cons finite_states finite_alphabet
    by auto
qed

lemma fsm_add_tr_invar[simp]: assumes "FSM fsm" shows "FSM (fsm_add_tr q a q' fsm)"  
proof -
  interpret FSM fsm by fact
  show ?thesis
    apply unfold_locales
    unfolding fsm_add_tr_def
    using delta_cons s0_cons F_cons finite_states finite_alphabet
    by auto
qed



subsection ‹ Reflexive, transitive closure of transition relation ›

text ‹ Reflexive transitive closure on restricted domain ›

inductive_set trclAD :: "('s,'a,'c) FSM_rec_scheme ⇒ ('s,'a) LTS ⇒ ('s,'a list) LTS" 
for A D
where
  empty[simp]: "s∈Q A ⟹ (s,[],s)∈trclAD A D" |
  cons[simp]: "⟦(s,e,s')∈D; s∈Q A; e∈Σ A; (s',w,s'')∈trclAD A D⟧ ⟹ (s,e#w,s'')∈trclAD A D"

abbreviation "trclA A == trclAD A (δ A)"
(*syntax trclA :: "('s,'a,'c) FSM_rec_scheme ⇒ ('s,'a list) LTS"
translations "trclA A" => "trclAD A (δ A)"*)

lemma trclAD_empty_cons[simp]: "(c,[],c')∈trclAD A D ⟹ c=c'" by (auto elim: trclAD.cases)
lemma trclAD_single: "(c,[a],c') ∈ trclAD A D ⟹ (c,a,c') ∈ D" by (auto elim: trclAD.cases)
lemma trclAD_elems: "(c,w,c')∈trclAD A D ⟹ c∈Q A ∧ w∈lists (Σ A) ∧ c'∈Q A" by (erule trclAD.induct, auto)
lemma trclAD_one_elem: "⟦c∈Q A; e∈Σ A; c'∈Q A; (c,e,c')∈D⟧ ⟹ (c,[e],c')∈trclAD A D" by auto


lemma trclAD_uncons: "(c,a#w,c')∈trclAD A D ⟹ ∃ch . (c,a,ch)∈D ∧ (ch,w,c') ∈ trclAD A D ∧ c∈Q A ∧ a∈Σ A" 
  by (auto elim: trclAD.cases)

lemma trclAD_concat: "!! c . ⟦ (c,w1,c')∈trclAD A D; (c',w2,c'')∈trclAD A D ⟧ ⟹ (c,w1@w2,c'')∈trclAD A D" 
proof (induct w1)
  case Nil thus ?case by (subgoal_tac "c=c'") auto
next
  case (Cons a w) thus ?case by (auto dest: trclAD_uncons)
qed    
 
lemma trclAD_unconcat: "!! c . (c,w1@w2,c')∈trclAD A D ⟹ ∃ch . (c,w1,ch)∈trclAD A D ∧ (ch,w2,c')∈trclAD A D" proof (induct w1)
  case Nil hence "(c,[],c)∈trclAD A D ∧ (c,w2,c')∈trclAD A D" by (auto dest: trclAD_elems)
  thus ?case by fast
next
  case (Cons a w1) note IHP = this
  hence "(c,a#(w1@w2),c')∈trclAD A D" by simp (* Auto/fast/blast do not get the point _#(_@_) = (_#_)@_ in next step, so making it explicit *)
  with trclAD_uncons obtain chh where "(c,a,chh)∈D ∧ (chh,w1@w2,c')∈trclAD A D ∧ c∈Q A ∧ a∈Σ A" by fast
  moreover with IHP obtain ch where "(chh,w1,ch)∈trclAD A D ∧ (ch,w2,c')∈trclAD A D" by fast
  ultimately have "(c,a#w1,ch)∈trclAD A D ∧ (ch,w2,c')∈trclAD A D" by auto
  thus ?case by fast
qed

lemma trclAD_eq: "⟦Q A = Q A'; Σ A = Σ A'⟧ ⟹ trclAD A D = trclAD A' D" 
  apply (safe)
  subgoal by (erule trclAD.induct) auto
  subgoal by (erule trclAD.induct) auto
  done

lemma trclAD_mono: "D⊆D' ⟹ trclAD A D ⊆ trclAD A D'"
  apply (clarsimp)
  apply (erule trclAD.induct)
  apply auto
  done

lemma trclAD_mono_adv: "⟦D⊆D'; Q A = Q A'; Σ A = Σ A'⟧ ⟹ trclAD A D ⊆ trclAD A' D'" by (subgoal_tac "trclAD A D = trclAD A' D") (auto dest: trclAD_eq trclAD_mono)


subsubsection ‹ Relation of @{term trclAD} and @{term LTS.trcl} ›
lemma trclAD_by_trcl1: "trclAD A D ⊆ (trcl (D ∩ (Q A × Σ A × Q A)) ∩ (Q A × lists (Σ A) × Q A))"
  by (auto 0 3 dest: trclAD_elems elim: trclAD.induct simp: trclAD_elems intro: trcl.cons)

lemma trclAD_by_trcl2: "(trcl (D ∩ (Q A × Σ A × Q A)) ∩ (Q A × lists (Σ A) × Q A)) ⊆ trclAD A D " proof -
  { fix c
    have "!! s s' . ⟦(s, c, s') ∈ trcl (D ∩ Q A × Σ A × Q A); s∈Q A; s'∈Q A; c∈lists (Σ A)⟧ ⟹ (s,c,s')∈trclAD A D" proof (induct c)
      case Nil thus ?case by (auto dest: trcl_empty_cons)
    next
      case (Cons e w) note IHP=this
      then obtain sh where SPLIT: "(s,e,sh)∈(D ∩ Q A × Σ A × Q A) ∧ (sh,w,s')∈trcl (D ∩ Q A × Σ A × Q A)" by (fast dest: trcl_uncons)
      hence "(sh,w,s')∈trcl (D ∩ Q A × Σ A × Q A) ∩ (Q A × lists (Σ A) × Q A)" by (auto elim!: trcl_structE)
      hence "(sh,w,s')∈trclAD A D" by (blast intro: IHP)
      with SPLIT show ?case by auto
    qed
  }
  thus ?thesis by (auto)
qed
    
lemma trclAD_by_trcl: "trclAD A D = (trcl (D ∩ (Q A × Σ A × Q A)) ∩ (Q A × lists (Σ A) × Q A))" 
  apply (rule equalityI)
  apply (rule trclAD_by_trcl1)
  apply (rule trclAD_by_trcl2)
  done

lemma trclAD_by_trcl': "trclAD A D = (trcl (D ∩ (Q A × Σ A × Q A)) ∩ (Q A × UNIV × UNIV))"
  by (auto iff add: trclAD_by_trcl elim!: trcl_structE)

lemma trclAD_by_trcl'': "⟦ D⊆Q A × Σ A × Q A ⟧ ⟹ trclAD A D = trcl D ∩ (Q A × UNIV × UNIV)"
  using trclAD_by_trcl'[of A D] by (simp add: Int_absorb2)

lemma trclAD_subset_trcl: "trclAD A D ⊆ trcl (D)" proof -
  have "trclAD A D ⊆ (trcl (D ∩ (Q A × Σ A × Q A)))" by (auto simp add: trclAD_by_trcl)
  also with trcl_mono[of "D ∩ (Q A × Σ A × Q A)" D] have "… ⊆ trcl D" by auto
  finally show ?thesis .
qed

subsection ‹ Language of a FSM ›
  

definition "langs A s == { w . (∃ f∈(F A) . (s,w,f) ∈ trclA A) }"
definition "lang A == langs A (s0 A)"

lemma langs_alt_def: "(w∈langs A s) == (∃f . f∈F A & (s,w,f) ∈ trclA A)" by (intro eq_reflection, unfold langs_def, auto)

subsection ‹ Example: Product automaton ›

definition "prod_fsm A1 A2 == ⦇ Q=Q A1 × Q A2, Σ=Σ A1 ∩ Σ A2, δ = { ((s,t),a,(s',t')) . (s,a,s')∈δ A1 ∧ (t,a,t')∈δ A2 }, s0=(s0 A1,s0 A2), F = {(s,t) . s∈F A1 ∧ t∈F A2} ⦈"

lemma prod_inter_1: "!! s s' f f' . ((s,s'),w,(f,f')) ∈ trclA (prod_fsm A A') ⟹ (s,w,f) ∈ trclA A ∧ (s',w,f') ∈ trclA A'" proof (induct w) 
  case Nil note P=this 
  moreover hence "s=f ∧ s'=f'" by (fast dest: trclAD_empty_cons)
  moreover from P have "s∈Q A ∧ s'∈Q A'" by (unfold prod_fsm_def, auto dest: trclAD_elems)
  ultimately show ?case by (auto)
next
  case (Cons e w)
  note IHP=this
  then obtain m m' where I: "((s,s'),e,(m,m')) ∈ δ (prod_fsm A A') ∧ (s,s')∈Q (prod_fsm A A') ∧ e∈Σ (prod_fsm A A') ∧ ((m,m'),w,(f,f'))∈trclA (prod_fsm A A')" by (fast dest: trclAD_uncons)
  hence "(s,e,m)∈δ A ∧ (s',e,m')∈δ A' ∧ s∈Q A ∧ s'∈Q A' ∧ e∈Σ A ∧ e∈Σ A'" by (unfold prod_fsm_def, simp)
  moreover from I IHP have "(m,w,f)∈trclA A ∧ (m',w,f')∈trclA A'" by auto
  ultimately show ?case by auto
qed
  
lemma prod_inter_2: "!! s s' f f' . (s,w,f) ∈ trclA A ∧ (s',w,f') ∈ trclA A' ⟹ ((s,s'),w,(f,f')) ∈ trclA (prod_fsm A A')" proof (induct w)
  case Nil note P=this
  moreover hence "s=f ∧ s'=f'" by (fast dest: trclAD_empty_cons)
  moreover from P have "(s,s')∈Q (prod_fsm A A')" by (unfold prod_fsm_def, auto dest: trclAD_elems)
  ultimately show ?case by simp
next
  case (Cons e w)
  note IHP=this
  then obtain m m' where I: "(s,e,m)∈δ A ∧ (m,w,f)∈trclA A ∧ (s',e,m')∈δ A' ∧ (m',w,f')∈trclA A' ∧ s∈Q A ∧ s'∈Q A' ∧ e∈Σ A ∧ e∈Σ A'" by (fast dest: trclAD_uncons)
  hence "((s,s'),e,(m,m')) ∈ δ (prod_fsm A A') ∧ (s,s')∈Q (prod_fsm A A') ∧ e∈Σ (prod_fsm A A')" by (unfold prod_fsm_def, simp)
  moreover from I IHP have "((m,m'),w,(f,f')) ∈ trclA (prod_fsm A A')" by auto
  ultimately show ?case by auto
qed
  
lemma prod_F: "(a,b)∈F (prod_fsm A B) = (a∈F A ∧ b∈F B)" by (unfold prod_fsm_def, auto)
lemma prod_FI: "⟦a∈F A; b∈F B⟧ ⟹ (a,b)∈F (prod_fsm A B)" by (unfold prod_fsm_def, auto)

lemma prod_fsm_langs: "langs (prod_fsm A B) (s,t) = langs A s ∩ langs B t"
  apply (unfold langs_def)
  apply (insert prod_inter_1 prod_F)
  apply (fast intro: prod_inter_2 prod_FI)
done

lemma prod_FSM_intro: "FSM A1 ⟹ FSM A2 ⟹ FSM (prod_fsm A1 A2)" by (rule FSM.intro) (auto simp add: FSM_def prod_fsm_def)


end