Theory NBA_Refine

section ‹Relations on Nondeterministic Büchi Automata›

theory NBA_Refine
imports
  "NBA"
  "../../Transition_Systems/Transition_System_Refine"
begin

  definition nba_rel :: "('label⇩1 × 'label⇩2) set ⇒ ('state⇩1 × 'state⇩2) set ⇒
    (('label⇩1, 'state⇩1) nba × ('label⇩2, 'state⇩2) nba) set" where
    [to_relAPP]: "nba_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}"

  lemma nba_param[param]:
    "(nba, nba) ∈ ⟨L⟩ set_rel → ⟨S⟩ set_rel → (L → S → ⟨S⟩ set_rel) → (S → bool_rel) →
      ⟨L, S⟩ nba_rel"
    "(alphabet, alphabet) ∈ ⟨L, S⟩ nba_rel → ⟨L⟩ set_rel"
    "(initial, initial) ∈ ⟨L, S⟩ nba_rel → ⟨S⟩ set_rel"
    "(transition, transition) ∈ ⟨L, S⟩ nba_rel → L → S → ⟨S⟩ set_rel"
    "(accepting, accepting) ∈ ⟨L, S⟩ nba_rel → S → bool_rel"
    unfolding nba_rel_def fun_rel_def by auto

  lemma nba_rel_id[simp]: "⟨Id, Id⟩ nba_rel = Id" unfolding nba_rel_def using nba.expand by auto
  lemma nba_rel_comp[trans]:
    assumes [param]: "(A, B) ∈ ⟨L⇩1, S⇩1⟩ nba_rel" "(B, C) ∈ ⟨L⇩2, S⇩2⟩ nba_rel"
    shows "(A, C) ∈ ⟨L⇩1 O L⇩2, S⇩1 O S⇩2⟩ nba_rel"
  proof -
    have "(accepting A, accepting B) ∈ S⇩1 → bool_rel" by parametricity
    also have "(accepting B, accepting C) ∈ S⇩2 → bool_rel" by parametricity
    finally have 1: "(accepting A, accepting C) ∈ S⇩1 O S⇩2 → bool_rel" by simp
    have "(transition A, transition B) ∈ L⇩1 → S⇩1 → ⟨S⇩1⟩ set_rel" by parametricity
    also have "(transition B, transition C) ∈ L⇩2 → S⇩2 → ⟨S⇩2⟩ set_rel" by parametricity
    finally have 2: "(transition A, transition C) ∈ L⇩1 O L⇩2 → S⇩1 O S⇩2 → ⟨S⇩1⟩ set_rel O ⟨S⇩2⟩ set_rel" by simp
    show ?thesis
      unfolding nba_rel_def mem_Collect_eq prod.case set_rel_compp
      using 1 2
      using nba_param(2 - 5)[THEN fun_relD, OF assms(1)]
      using nba_param(2 - 5)[THEN fun_relD, OF assms(2)]
      by auto
  qed
  lemma nba_rel_converse[simp]: "(⟨L, S⟩ nba_rel)¯ = ⟨L¯, S¯⟩ nba_rel"
  proof -
    have 1: "⟨L⟩ set_rel = (⟨L¯⟩ set_rel)¯" by simp
    have 2: "⟨S⟩ set_rel = (⟨S¯⟩ set_rel)¯" by simp
    have 3: "L → S → ⟨S⟩ set_rel = (L¯ → S¯ → ⟨S¯⟩ set_rel)¯" by simp
    have 4: "S → bool_rel = (S¯ → bool_rel)¯" by simp
    show ?thesis unfolding nba_rel_def unfolding 3 unfolding 1 2 4 by fastforce
  qed

  lemma nba_rel_eq: "(A, A) ∈ ⟨Id_on (alphabet A), Id_on (nodes A)⟩ nba_rel"
    unfolding nba_rel_def by auto

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

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

  lemma language_param[param]: "(language, language) ∈ ⟨L, S⟩ nba_rel → ⟨⟨L⟩ stream_rel⟩ set_rel"
  proof -
    have 1: "language A = (⋃ p ∈ initial A. ⋃ wr ∈ nba.runs A p.
      if infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {})"
      for A :: "('label, 'state) nba"
      unfolding nba.language_def nba.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