Theory DCA

section ‹Deterministic Co-Büchi Automata›

theory DCA
imports "../Deterministic"

  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 = 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"
  abbreviation states where "states  dca.states"
  abbreviation trace where "trace  dca.trace"
  abbreviation successors where "successors  dca.successors TYPE('label)"