Theory NGBA_Refine

section ‹Relations on Nondeterministic Generalized Büchi Automata›

theory NGBA_Refine
imports
  "NGBA"
  "../../Transition_Systems/Transition_System_Refine"
begin

  definition ngba_rel :: "('label⇩1 × 'label⇩2) set ⇒ ('state⇩1 × 'state⇩2) set ⇒
    (('label⇩1, 'state⇩1) ngba × ('label⇩2, 'state⇩2) ngba) set" where
    [to_relAPP]: "ngba_rel L S ≡ {(A⇩1, A⇩2).
      (alphabet A⇩1, alphabet A⇩2) ∈ ⟨L⟩ set_rel ∧
      (initial A⇩1, initial A⇩2) ∈ ⟨S⟩ set_rel ∧
      (transition A⇩1, transition A⇩2) ∈ L → S → ⟨S⟩ set_rel ∧
      (accepting A⇩1, accepting A⇩2) ∈ ⟨S → bool_rel⟩ list_rel}"

  lemma ngba_param[param]:
    "(ngba, ngba) ∈ ⟨L⟩ set_rel → ⟨S⟩ set_rel → (L → S → ⟨S⟩ set_rel) → ⟨S → bool_rel⟩ list_rel →
      ⟨L, S⟩ ngba_rel"
    "(alphabet, alphabet) ∈ ⟨L, S⟩ ngba_rel → ⟨L⟩ set_rel"
    "(initial, initial) ∈ ⟨L, S⟩ ngba_rel → ⟨S⟩ set_rel"
    "(transition, transition) ∈ ⟨L, S⟩ ngba_rel → L → S → ⟨S⟩ set_rel"
    "(accepting, accepting) ∈ ⟨L, S⟩ ngba_rel → ⟨S → bool_rel⟩ list_rel"
    unfolding ngba_rel_def fun_rel_def by auto

  lemma ngba_rel_id[simp]: "⟨Id, Id⟩ ngba_rel = Id" unfolding ngba_rel_def using ngba.expand by auto

  lemma enableds_param[param]: "(ngba.enableds, ngba.enableds) ∈ ⟨L, S⟩ ngba_rel → S → ⟨L ×⇩r S⟩ set_rel"
    using ngba_param(2, 4) unfolding ngba.enableds_def fun_rel_def set_rel_def by fastforce
  lemma paths_param[param]: "(ngba.paths, ngba.paths) ∈ ⟨L, S⟩ ngba_rel → S → ⟨⟨L ×⇩r S⟩ list_rel⟩ set_rel"
    using enableds_param[param_fo] by parametricity
  lemma runs_param[param]: "(ngba.runs, ngba.runs) ∈ ⟨L, S⟩ ngba_rel → S → ⟨⟨L ×⇩r S⟩ stream_rel⟩ set_rel"
    using enableds_param[param_fo] by parametricity

  lemma reachable_param[param]: "(reachable, reachable) ∈ ⟨L, S⟩ ngba_rel → S → ⟨S⟩ set_rel"
  proof -
    have 1: "reachable A p = (λ wr. target wr p) ` ngba.paths A p" for A :: "('label, 'state) ngba" and p
      unfolding ngba.reachable_alt_def ngba.paths_def by auto
    show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity
  qed
  lemma nodes_param[param]: "(nodes, nodes) ∈ ⟨L, S⟩ ngba_rel → ⟨S⟩ set_rel"
    unfolding ngba.nodes_alt_def Collect_mem_eq by parametricity

  (* TODO: move *)
  lemma gen_param[param]: "(gen, gen) ∈ (A → B → bool_rel) → ⟨A⟩ list_rel → B → bool_rel"
    unfolding gen_def by parametricity

  lemma language_param[param]: "(language, language) ∈ ⟨L, S⟩ ngba_rel → ⟨⟨L⟩ stream_rel⟩ set_rel"
  proof -
    have 1: "language A = (⋃ p ∈ initial A. ⋃ wr ∈ ngba.runs A p.
      if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {})"
      for A :: "('label, 'state) ngba"
      unfolding ngba.language_def ngba.runs_def image_def
      by (auto iff: split_szip_ex simp del: alw_smap)
    show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity
  qed

end