Theory Acceptance_Refine

theory Acceptance_Refine
imports "Acceptance" "Refine"
begin

  abbreviation (input) "pred_rel A ≡ A → bool_rel"
  abbreviation (input) "rabin_rel A ≡ pred_rel A ×⇩r pred_rel A"

  lemma rabin_param[param]: "(rabin, rabin) ∈ rabin_rel A → pred_rel (⟨A⟩ stream_rel)"
    unfolding rabin_def by parametricity
  lemma gen_param[param]: "(gen, gen) ∈ (A → pred_rel B) → (⟨A⟩ list_rel → pred_rel B)"
    unfolding gen_def by parametricity
  lemma cogen_param[param]: "(cogen, cogen) ∈ (A → pred_rel B) → (⟨A⟩ list_rel → pred_rel B)"
    unfolding cogen_def by parametricity

end