Theory DCA

section ‹Deterministic Co-Büchi Automata›

theory DCA
imports "../Deterministic"
begin

  datatype ('label, 'state) dca = dca
    (alphabet: "'label set")
    (initial: "'state")
    (transition: "'label ⇒ 'state ⇒ 'state")
    (rejecting: "'state ⇒ bool")

  global_interpretation dca: automaton dca alphabet initial transition rejecting
    defines path = dca.path and run = dca.run and reachable = dca.reachable and nodes = dca.nodes
    by unfold_locales auto
  global_interpretation dca: automaton_run dca alphabet initial transition rejecting "λ P w r p. fins P (p ## r)"
    defines language = dca.language
    by standard

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

end