Theory Acceptance

theory Acceptance
imports Sequence_LTL
begin

  type_synonym 'a pred = "'a ⇒ bool"
  type_synonym 'a rabin = "'a pred × 'a pred"
  type_synonym 'a gen = "'a list"

  definition rabin :: "'a rabin ⇒ 'a stream pred" where
    "rabin ≡ λ (I, F) w. infs I w ∧ fins F w"

  lemma rabin[intro]:
    assumes "IF = (I, F)" "infs I w" "fins F w"
    shows "rabin IF w"
    using assms unfolding rabin_def by auto
  lemma rabin_elim[elim]:
    assumes "rabin IF w"
    obtains I F
    where "IF = (I, F)" "infs I w" "fins F w"
    using assms unfolding rabin_def by auto

  definition gen :: "('a ⇒ 'b pred) ⇒ ('a gen ⇒ 'b pred)" where
    "gen P cs w ≡ ∀ c ∈ set cs. P c w"

  lemma gen[intro]:
    assumes "⋀ c. c ∈ set cs ⟹ P c w"
    shows "gen P cs w"
    using assms unfolding gen_def by auto
  lemma gen_elim[elim]:
    assumes "gen P cs w"
    obtains "⋀ c. c ∈ set cs ⟹ P c w"
    using assms unfolding gen_def by auto

  definition cogen :: "('a ⇒ 'b pred) ⇒ ('a gen ⇒ 'b pred)" where
    "cogen P cs w ≡ ∃ c ∈ set cs. P c w"

  lemma cogen[intro]:
    assumes "c ∈ set cs" "P c w"
    shows "cogen P cs w"
    using assms unfolding cogen_def by auto
  lemma cogen_elim[elim]:
    assumes "cogen P cs w"
    obtains c
    where "c ∈ set cs" "P c w"
    using assms unfolding cogen_def by auto

  lemma cogen_alt_def: "cogen P cs w ⟷ ¬ gen (λ c w. Not (P c w)) cs w" by auto

end