# 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```