Theory NFA

section ‹Nondeterministic Finite Automata›

theory NFA
imports "../Nondeterministic"
begin

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

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

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

  (* TODO: going from target to last requires states as intermediate step, used in other places too *)
  global_interpretation nfa: automaton_intersection_path
    nfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    nfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    nfa 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 = nfa.product
    by (unfold_locales) (auto simp: zip_eq_Nil_iff)

  global_interpretation nfa: automaton_union_path
    nfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    nfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    nfa alphabet initial transition accepting "λ P w r p. P (last (p # r))"
    case_sum
    defines union = nfa.sum
    by (unfold_locales) (auto simp: last_map)

end