Theory DFA

section ‹Deterministic Finite Automata›

theory DFA
imports "../Deterministic"
begin

  datatype ('label, 'state) dfa = dfa
    (alphabet: "'label set")
    (initial: "'state")
    (transition: "'label ⇒ 'state ⇒ 'state")
    (accepting: "'state pred")

  global_interpretation dfa: automaton dfa alphabet initial transition accepting
    defines path = dfa.path and run = dfa.run and reachable = dfa.reachable and nodes = dfa.nodes
    by unfold_locales auto
  global_interpretation dfa: automaton_path dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    defines language = dfa.language
    by standard

  abbreviation target where "target ≡ dfa.target"
  abbreviation states where "states ≡ dfa.states"
  abbreviation trace where "trace ≡ dfa.trace"
  abbreviation successors where "successors ≡ dfa.successors TYPE('label)"

  global_interpretation intersection: automaton_intersection_path
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    "λ c⇩1 c⇩2 (p, q). c⇩1 p ∧ c⇩2 q"
    defines intersect = intersection.product
    by (unfold_locales) (auto simp: zip_eq_Nil_iff)

  global_interpretation union: automaton_union_path
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    "λ c⇩1 c⇩2 (p, q). c⇩1 p ∨ c⇩2 q"
    defines union = union.product
    by (unfold_locales) (auto simp: zip_eq_Nil_iff)

  global_interpretation complement: automaton_complement_path
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    dfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    "λ c p. ¬ c p"
    defines complement = complement.complement
    by unfold_locales auto

end