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