Theory DGCA

section ‹Deterministic Co-Generalized Co-Büchi Automata›

theory DGCA
imports "../Deterministic"
begin

  datatype ('label, 'state) dgca = dgca
    (alphabet: "'label set")
    (initial: "'state")
    (transition: "'label ⇒ 'state ⇒ 'state")
    (rejecting: "'state pred gen")

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

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

end